| ⊢ | Substitution instances of conventional (nonmodal) tautologies | | Taut
|
| ⊢ | (f ⌢ g) ⌢ h ≡ f ⌢ (g ⌢ h) | | FChopAssoc
|
| ⊢ | (f0 ∨ f1) ⌢ g ⊃ (f0 ⌢ g) ∨ (f1 ⌢ g) | | FOrChopImp
|
| ⊢ | f ⌢ (g0 ∨ g1) ⊃ (f ⌢ g0) ∨ (f ⌢ g1) | | FChopOrImp
|
| ⊢ | empty ⌢ f ≡ f | | FEmptyChop
|
| ⊢ | f ⌢ empty ≡ f | | FChopEmpty
|
| ⊢ | w ⊃ w | | FStateImpBf
|
| ⊢ | (f0 ⊃ f1) ∧ (g0 ⊃ g1) ⊃ (f0 ⌢ g0) ⊃ (f1 ⌢ g1) | |
FBfAndBoxImpChopImpChop
|
| ⊢ | f⋆ ≡empty ∨ (f ∧more) ⌢ f⋆ | | FChopStarEqv
|
| ⊢ | f ⊃ f | | FNextImpWeakNext
|
| ⊢ | f ∧ (f ⊃ f) ⊃ f | | FBoxInduct
|
| ⊢ | f ⊃ g, ⊢ f ⇒ ⊢ g | | FMP
|
| ⊢ | f ⇒ ⊢ f | | FBfGen
|
| ⊢ | f ⇒ ⊢ f | | FBoxGen
|
| | |