Next Prev Up
DiSkipEqvMore

⊢ skip ≡more DiSkipEqvMore

Proof:

1
⊢ skip ; true ≡true
SkipChopEqvNext,DiAndB
2
⊢ true ≡more
PTL
3
⊢ skip ; true ≡more
1, 2,Prop
4
⊢ skip ≡more
3, def. of 

qed

Next Prev Up

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