This folder contains different versions of proof scripts for the same theorem.
There are several types of files:
- txt files that are describing coherent logic proofs scripts
- all other files are products of our framework and are described at the end of this file

**************************************************
   DESCRIPTION OF PROOF SCRIPTS   - TXT FILES
**************************************************

These files are singled out in the folder "PROOF_SCRIPTS"
For each theorem number, we provide proof scripts of different levels of granularity:

- - letter "n" denotes "no proof script" (a minimal proof script) and just contains the premise and the conclusion of a theorem
(using only "infer goal" tactic)

- - theorem without a number is used for "direct proof scripts" (non empty proof script without any case split tactics)
- - letter "c" denotes "case split proofs" (a skeleton proof script), i.e. proof script that contain at least one case split tactic
- - in case there are several versions of a proof (with different levels of granularity), we add numbers after the letter c

For example, for theorem 5 we provide the following proof scripts: th_5c_proof.txt, th_5c1_proof.txt, th_5c2_proof.txt, th_5c3_proof.txt, th_5c4_proof.txt, to demonstrate different levels of granularity and backtracking with branching.

For example, for theorem 1 we provide th_5n_proof.txt, th_5_proof.txt, th_5c_proof.txt to demonstrate different levels of granularity (no proof, direct proof script and a skeleton proof script).


**************************************************
         DESCRIPTION OF GENERATED FILES
**************************************************

Example: for input file th_1c_proof.txt, framework generates the following files:

- th_1c_goals.p - set of intermediate lemmas that will be verified individually
- th_1c_formalize.p - the set of lemmas with definitions and axiomatic system used

The following files are generated even if the system is not able to find a proof of a theorem, those proofs will be labeled with "sorry" in Isabelle and "Admitted" in Rocq/Coq

- th_1c_complete_proof.thy - Isabelle version of proofs of all lemmas
- th_1c_complete_proof.v - Rocq/Coq version of proofs of all lemmas
- th_1c_complete_proof.tex, th_1c_complete_proof.pdf - English version of proofs of all lemmas
- th_1c_kompletan_dokaz.tex, th_1c_kompletan_dokaz.tex - Serbian version of proofs of all lemmas