In Table 15 we list the propositional axioms and rules for finite and infinite ITL.
ChopAssoc |
⊢ (f0 ; f1) ; f2 ≡ f0 ; (f1 ; f2) |
OrChopImp |
⊢ (f0 ∨ f1) ; f2 ⊃ (f0 ; f2) ∨ (f1 ; f2) |
ChopOrImp |
⊢ f0 ; (f1 ∨ f2) ⊃ (f0 ; f1) ∨ (f0 ; f2) |
EmptyChop |
⊢ empty ; f ≡ f |
ChopEmpty |
⊢ f ; empty ≡ f |
BiBoxChopImpChop |
⊢ (f0 ⊃ f1) ∧ (f2 ⊃ f3) ⊃ (f0 ; f2) ⊃ (f1 ; f3) |
StateImpBi |
⊢ w ⊃ w |
NextImpNotNextNot | ⊢ f ⊃ ¬¬f |
BoxInduct |
⊢ f ∧ (f ⊃ f) ⊃ f |
InfChop |
⊢ (f ∧ inf) ; g ≡ (f ∧ inf) |
ChopStarEqv |
⊢ f∗≡ (empty ∨ ((f ∧ more) ; f∗)) |
ChopstarInduct |
⊢ (inf ∧ f ∧ (f ⊃ (g ∧ fmore) ; f)) ⊃ g∗ |
MP |
⊢ f0 ⊃ f1, ⊢ f0 ⇒ ⊢ f1 |
BoxGen |
⊢ f0 ⇒ ⊢ f0 |
BiGen |
⊢ f0 ⇒ ⊢ f0 |