Next Prev Up
SkipChopEqvNext

⊢ skip ; f ≡ f SkipChopEqvNext

Proof:

1
⊢ ( empty) ; f ≡ (empty ; f)
NextChop
2
⊢ empty ; f ≡ f
EmptyChop
3
⊢ (empty ; f) ≡ f
2,NextEqvNext
4
⊢ ( empty) ; f ≡ f
1, 3,Prop
5
⊢ skip ; f ≡ f
4, def. of skip

qed

Next Prev Up

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