ITL
© 1996-2018







2.5 Properties of chop-plus

f f+ ImpChopPlus

Proof:

1
f+ f (f more) ; f+
2
f f+
1,Prop

qed

f ; f+ f+ ChopChopPlusImpChopPlus

Proof:

1
empty more
2
f empty (f more)
1,Prop
3
f ; f+ f+ (f more) ; f+
4
f+ f (f more) ; f+
5
(f more) ; f+ f+
4,Prop
6
f ; f+ f+
3, 5,Prop

qed

f+ f (f ; f+) ChopPlusEqvOrChopChopPlus

Proof for :

1
f+ f (f more) ; f+
2
(f more) ; f+ f ; f+
3
f+ f f ; f+
1, 2,Prop

qed

Proof for :

1
f f+
2
empty more
3
f empty (f more)
2,Prop
4
f ; f+ f+ (f more) ; f+
5
f+ f (f more) ; f+
6
(f more) ; f+ f+
5,Prop
7
f (f ; f+) f+
1, 6,Prop

qed

f ¬g (g more) ; f ⇒ ⊢ f g+ ChopPlusIntro

Proof:

1
f ¬g (g more) ; f
given
2
g+ g (g more) ; g+
3
f ¬(g+) (g more) ; f ¬((g more) ; g+)
1, 2,Prop
4
g more more
5
f g+

qed

f g, (f more) ; g g ⇒ ⊢ f+ g ChopPlusElim

Proof:

1
f+ f (f more) ; f+
2
f g
given
3
(f more) ; g g
given
4
f+ ¬g (f more) ; f+ ¬((f more) ; g)
1, 2, 3,Prop
5
f more more
6
f+ g

qed

f g, f ; g g ⇒ ⊢ f+ g ChopPlusElimWithoutMore

Proof:

1
f g
given
2
f ; g g
given
3
(f more) ; g f ; g
4
(f more) ; g g
2, 3,ImpChain
5
f+ g

qed

f g ⇒ ⊢ f+ g+ ChopPlusImpChopPlus

Proof:

1
f g
given
2
f+ f (f more) ; f+
3
g+ g (g more) ; g+
4
f+ ¬(g+) ((f more) ; f+) ¬((g more) ; g+)
1, 2, 3,Prop
5
f more g more
1,Prop
6
(f more) ; f+ (g more) ; f+
7
f+ ¬(g+) ((g more) ; f+) ¬((g more) ; g+)
4, 6,Prop
8
g more more
9
f+ g+

qed

f g ⇒ ⊢ f+ g+ ChopPlusEqvChopPlus

Proof:

1
f g
given
2
f g
1,Prop
3
f+ g+
4
g f
1,Prop
5
g+ f+
6
f+ g+
3, 5,Prop

qed







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