⊢ | 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: