From time to time, when changes in its content have accumulated, the numerical identifiers of the theorems appearing in it must be renumbered by means of the program "renumber_scenario.stl"; (see [Click]), which will obtain from it the files
Opened, read and analyzed, and then closed, by the procedure verifier_invoker of the SETL package verifier_top_level; internally associated with the command_handle.
Only used in server running modality: it serves as a surrogate for the activation command line, as an intermediate file between
the PHP script and the SETL user-associated program.
These are (for a suffix > 1) opened/closed and generated by the procedures set_output_phase and printy of the SETL package prynter, and internally associated with the ohandle.
Generated by the SETL procedure ???, and internally associated with the dump_theorems_handle
Generated by the SETL procedure ???, and internally associated with the dump_defs_handle
Generated by the SETL procedure ???, and internally associated with the dump_theories_handle
Generated by the SETL procedure ???, and internally associated with the dump_theorems_handle2
Only used in standalone running modality, for dump in unpretty form.
Generated by the SETL procedure ???, and internally associated with the dump_defs_handle2
Only used in standalone running modality, for dump in unpretty form.
Generated by the SETL procedure ???, and internally associated with the dump_theories_handle2
Only used in standalone running modality, for dump in unpretty form.
Generated by the SETL procedure citation_analysis(uid), and internally associated with the citations_handle
Opened/closed and generated by the procedures set_output_phase and verifier_invoker of the SETL packages prynter and verifier_top_level, and internally associated with the ohandle. Its content will consist of "Good" HTML-table entries.
Only used in standalone running modality.
Entirely handled by the SETL procedures set_output_phase and printer within SETL the package prynter, and internally associated with the ferr_ohandle. Its content will consist of "Bad" HTML-table entries.
Only used in standalone running modality.
Generated by the SETL procedure parse_file(lines_tup), and internally associated with the digested_proof_handle
digested_proof_file is a large list of tuples of tuples, each one of the upper-level tuples representing a proof and each one of the lower-level tuples representing one of the successive lines of a proof as a pair [step_descriptor,formula], for example ["ELEM", "{z} * s_inf /= 0 & {z} * s_inf = {z}"]. The labels of internally labeled statements are left in the "formula" part of this pair, for example ["a --> Stat1", "Stat2: (a in {cdr([x,f(x)]): x in s} & a notin {f(x) : x in s}) or (a notin {cdr([x,f(x)]): x in s} & a in {f(x) : x in s})"]
******* Note however ******* that each proof-representing tuple is prefixed by an integer, which is the "section number" of the corresponding proof. This number is one more than the section number of the corresponding theorem statement, which is used in the theorem_sno_map_file
Generated by the SETL procedure suppose_not_file(lines_tup), and internally associated with the suppose_not_handle
suppose_not_file is a list of triples
[subst_list,statement_in_suppose_not,statement_in_theorem]
Generated by the SETL procedure parse_file(lines_tup), and internally associated with the theorem_map_handle
theorem_map_file contains a set of pairs giving a map of abbreviated theorem names (often of the form Tnnn) into the corresponding theorem statement.
Generated by the SETL procedure parse_file(lines_tup), and internally associated with the theorem_sno_map_handle
theorem_sno_map_file contains a set of pairs giving a map of abbreviated theorem names (often of the form Tnnn) into the corresponding theorem section numbers. It also contains pairs which map symbol definition names into their associated section numbers, and which map theory names into their section numbers.
Generated by the SETL procedure parse_file(lines_tup), and internally associated with the definitions_handle
definition_tup_file contains a set of triples, each giving the name of a definition, the body of the definition, and the theory to which it belongs
Generated by the SETL procedure parse_file(lines_tup), and internally associated with the theory_data_handle
theory_data_file is comprised of three subparts. The first is a map of theories into their parent theories. The second maps the name of each theory into the list of names of all the theorems and definitions belonging to the theory. The third maps the name of each theory into a pair giving the assumed function and the assumptions of the theory.