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