Next Prev Up
CSAndMoreEqvAndMoreChop

⊢ f∗∧more ≡ (f ∧more) ; f∗ CSAndMoreEqvAndMoreChop

Proof for ⊃ :

1
⊢ (empty ∨ (f ∧more) ; f∗) ∧more ⊃ (f ∧more) ; f∗
PTL
2
⊢ f∗∧more ⊃ (f ∧more) ; f∗
1, def. of ∗

qed

Proof for ⊂:

1
⊢ f∗≡empty ∨ (f ∧more) ; f∗
CSEqv
2
⊢ (f ∧more) ; f∗⊃ f∗
1,Prop
3
⊢ (f ∧more) ; f∗⊃more
MoreChopImpMore
4
⊢ (f ∧more) ; f∗⊃ f∗∧more
2, 3,Prop

qed

Next Prev Up

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