| ⊢ | empty | DiamondEmpty |
Proof:
qed
Here are some use derived rules for linear time temporal logic. We omit their proofs:
| ⊢ | f ≡ g ⇒ ⊢ f ≡ g | NextEqvNext |
| ⊢ | f ∧ g ⊃ h ⇒ ⊢ f ∧ g ⊃ h | NextAndNextImpNextRule |
| ⊢ | f ∧ g ≡ h ⇒ ⊢ f ∧ g ≡ h | NextAndNextEqvNextRule |
| ⊢ | f ≡ g ⇒ ⊢ f ≡ g | WeakNextEqvWeakNext |
| ⊢ | f ⊃ g ⇒ ⊢ f ⊃ g | DiamondImpDiamond |
| ⊢ | f ≡ g ⇒ ⊢ f ≡ g | DiamondEqvDiamond |
| ⊢ | f ≡ g ⇒ ⊢ f ≡ g | BoxEqvBox |
| ⊢ | f ∧ g ⊃ h ⇒ ⊢ f ∧ g ⊃ h | BoxAndBoxImpBoxRule |
| ⊢ | f ∧ g ≡ h ⇒ ⊢ f ∧ g ≡ h | BoxAndBoxEqvBoxRule |
| ⊢ | f ⊃ g, ⊢more ∧ f ⊃ f ⇒ ⊢ f ⊃ g | BoxIntro |
| ⊢ | (f ∧¬g) ⊃ f ⇒ ⊢ f ⊃ g | DiamondIntro |
| ⊢ | f ⊃ f ⇒ ⊢¬f | NextLoop |
| ⊢ | f ∧¬g ⊃ f ∧¬ g ⇒ ⊢ f ⊃ g | NextContra |
| ⊢ | f ⊃ f ⇒ ⊢ f | WeakNextBoxInduct |
| ⊢ | empty ⊃ f, ⊢ f ⊃ f ⇒ ⊢ f | EmptyNextInducta |
| ⊢ | empty ∧ f ⊃ g,⊢ (f ⊃ g) ∧ f ⊃ g ⇒ ⊢ f ⊃ g | EmptyNextInductb |
| ⊢ | f ⊃ g ⇒ ⊢fin f ⊃ fin g | FinImpFin |
| ⊢ | f ≡ g ⇒ ⊢fin f ≡fin g | FinEqvFin |
| ⊢ | f ∧ g ⊃ h ⇒ ⊢fin f ∧fin g ⊃ fin h | FinAndFinImpFinRule |
| ⊢ | f ∧ g ≡ h ⇒ ⊢fin f ∧fin g ≡fin h | FinAndFinEqvFinRule |
| ⊢ | f ≡ g ⇒ ⊢halt f ≡halt g | HaltEqvHalt |
Note that ImpChain can be viewed as a special case of Prop. If desired, a deduction theorem can also be proved.
We now give proofs of some derived inference rules and theorems: