| ⊢ | Substitution instances of valid PTL formulas | | VPTL
|
| ⊢ | (f ⌢ g) ⌢ h ≡ f ⌢ (g ⌢ h) | | ChopAssoc
|
| ⊢ | (f0 ∨ f1) ⌢ g ⊃ (f0 ⌢ g) ∨ (f1 ⌢ g) | | OrChopImp
|
| ⊢ | f ⌢ (g0 ∨ g1) ⊃ (f ⌢ g0) ∨ (f ⌢ g1) | | ChopOrImp
|
| ⊢ | empty ⌢ f ≡ f | | EmptyChop
|
| ⊢ | finite ⊃ (f ⌢ empty ≡ f) | | FiniteImpChopEmpty
|
| ⊢ | w ⊃ w | | StateImpBf
|
| ⊢ | (f0 ⊃ f1) ∧ (g0 ⊃ g1) ⊃ (f0 ⌢ g0) ⊃ (f1 ⌢ g1) | |
BfAndBoxImpChopImpChop
|
| ⊢ | f⋆ ≡empty ∨ (f ∧more) ⌢ f⋆ | | SChopStarEqv
|
| ⊢ | f ∧ (f ⊃ (g ∧more) ⌢ f) ⊃ gω | | ChopOmegaInduct
|
| ⊢ | f ⊃ g, ⊢ f ⇒ ⊢ g | | MP
|
| ⊢ | finite ⊃ f ⇒ ⊢ f | | BfFGen
|
| ⊢ | f ⇒ ⊢ f | | BoxGen
|
| ⊢ | ((fin P) ≡ g) ⊃ f ⇒ ⊢ f | | BfAux |