ITL
© 1996-2018







8.7 Some Properties of Chop-Star

We now consider some theorems and derived rules concerning chop-star.

f more ⇒ ⊢ f empty (f f) ImpMoreChopStarEqvRule

Proof:

1
f more
Assump
2
f more f
1,Prop
3
(f more) f f f
4
f empty ((f more) f)
5
f empty (f f)
3, 4,Prop

qed

f more ⇒ ⊢ f g g (f (f g)) ImpMoreChopStarChopEqvRule

Proof:

1
f more
Assump
2
f empty (f f)
3
f g (empty (f f)) g
4
(empty (f f)) g (empty g) ((f f) g)
5
empty g g
6
(f f) g f (f g)
7
f g g (f (f g))
3 −−6,Prop

qed

f (f empty) fω SChopStarEqvSChopstarChopEmptyOrChopOmega

Proof:

1
finite ¬finite
2
finite inf
1, def. of inf
3
finite (f empty) f
4
inf f (f inf)
5
inf f fω
4, def. of chop-omega
6
f (f empty) fω
2, 3, 5,Prop

qed







2018-10-21
Contact | Home | ITL home | Course | Proofs | Algebra | FL