ITL
© 1996-2018







7 Properties of chop-plus


f f+ ImpChopPlus


Proof:

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


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


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

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


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+


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


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


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+


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







2018-02-26
Contact | Home | ITL home | Course | Proofs | Algebra | FL