The work of this procedure is complete when these files have been written. All the files are written in readable "plain text" format.
The main file read to check various kinds of inferences in the verifier is "digested_proof_file".
Once syntax analysis is successful, this routine does various more detailed semi-syntactic, semi-semantic checks.
We allow segments of the scenario file input to be indicated by special lines starting with --BEGIN HERE and --PAUSE HERE (which suspends analysis of scenario lines); also --END HERE, which terminates scenario processing.
Lines can be grouped together into single logical lines by including a "Â" (option l) mark at the end. Over the web this is å
Comment lines starting with -- are ignored.
Definitions must start with either "Def " or "Def:".
Theorems must start with either "Theorem " or "Theorem:".
Theorem statements can contain a prefixed comment in square brackets, as in
Theorem 251: [Zorn's Lemma] .... Proof:...
Proofs must start with "Proof:"
We now start to assemble (extended) lines into sections, which can be either definition_sections, theorem_sections, proof_sections, etc., or unused_sections. Section starts are marked by the appearance of one of the significant marks "Def ","Def:","Theorem ","Theorem:", or "Proof:" Definition and theorem sections are also terminated by the first empty line after their opening, and all following lines without one of the above headers are skipped.
These sections are collected into an overall tuple called "sections"; the indices of elements of various kinds (theorems, definitions, proofs, etc.) are collected into auxiliary tuples called
This routine also keeps track of incomplete or missing proofs.