General
- Existential quantifiers in Type
- General purpose tools in Type
- Constructions for inductive proofs about derivations (1)
- Constructions for inductive proofs about derivations (2)
- Lemmas about lists in Type
- Reflexive transitive closure, in Type
- Strong induction on natural numbers
- Definition of swapped, and lemmas
- Derivations in Type
- General elements about sequents
- General tactics
- General tools
- Derivations as data structures
- Export file for General
Definition of the sequent calculus G4iSLT
Preliminaries of G4iSLT
- Lemmas on lists of formulae
- Lemmas on the removal of formulas from lists
- Decidability of the application of rules
Admissibility of exchange
- Definition and And and Or rules
- AtomImpL1 Rule
- AtomImpL2 Rule
- ImpR and BoxImpL Rules
- Remaining Rules
- Admissibility
Admissibility of weakening
Admissibility of rules
- Admissibility of left-unboxing rule
- Invertibility of And rules
- Invertibility of OrL rule
- Invertibility of ImpR rule
- Invertibility of AtomImpL1 and AtomImpL2 rules
- Invertibility of AndImpL rule
- Invertibility of OrImpL rule
- Right-invertibility of ImpImpL rule
- Right-invertibility of BoxImpL rule
- Right-invertibility of ImpL rule
- Admissibility of ImpL rule
- Almost-left-invertibility of ImpImpL rule
- Admissibility of general identity rule
Admissibility of contraction
Strong termination
- The shortlex order
- Preliminaries
- Definition of the measure
- Decrease in the And rules
- Decrease in the Or rules
- Decrease in the ImpR rule
- Decrease in left implication rules
- Decrease in the SLR rule
- Decrease in all rules