Next Prev Up
DiMoreEqvMore

⊢ more ≡more DiMoreEqvMore

Proof for ⊃ :

1
⊢ ( skip) ≡true
DiNext
2
⊢ skip ⊃more
PTL
3
⊢ skip ⊃more
1, 2,ImpChain
4
⊢ more ⊃more
3, def. of more

qed

Proof of ⊂:

1
⊢ more ⊃more
ImpDi

qed

Next Prev Up

2024-08-03
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2024