Next Prev Up
SkipYieldsEqvWeakNext

⊢ skip f ≡ f SkipYieldsEqvWeakNext

Proof:

1
⊢ skip ; ¬f ≡¬f
SkipChopEqvNext
2
⊢ ¬(skip ; ¬f) ≡¬¬f
1,Prop
3
⊢ ¬¬f ≡ f
PTL
4
⊢ ¬(skip ; ¬f) ≡ f
2, 3,EqvChain
5
⊢ skip f ≡ f
4, def. of 

qed

Next Prev Up

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