Next Prev Up
FDiamondEqvNowOrNextDiamond

⊢ f ≡ f ∨ f FDiamondEqvNowOrNextDiamond

Proof:

1
f ≡⟨skip∗⟩f
FL3
2
⟨skip∗⟩f ≡ f ∨⟨skip ; skip∗⟩f
FL8
3
⟨skip ; skip∗⟩f ≡⟨skip⟩⟨skip∗⟩f
FL6
4
⟨skip∗⟩f ≡⟨skip⟩⟨skip∗⟩f
FL2
5
f ≡⟨skip∗⟩X
1,FNextEqvNextRule
6
f ≡ f ∨ f
1–5,Prop

qed

Next Prev Up

2023-09-12
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2023