ITL
© 1996-2018







8 Properties of chop-star


f empty (f more) ; f CSEqv


Proof:

1
f+ f (f more) ; f+
2
empty ≡¬more
3
empty f+ empty (f more) (f more) ; f+
1, 2,Prop
4
(f more) ; empty f more
5
(f more) ; (empty f+)
(f more) ; empty (f more) ; f+
6
empty f+ empty ((f more) ; (empty f+))
3, 4, 5,Prop
7
f empty (f more) ; f
6, def. of 


empty f EmptyImpCS


Proof:

1
f empty f+
def. of 
2
empty f
1,Prop

Here is an straightforward corollary:


¬f more NotCSImpMore



f+ f ChopPlusImpCS


Proof:

1
f+ empty f+
2
f+ f
1, def. of 


f f ImpCS


Proof:

1
f f+
2
f empty f+
1,Prop
3
f f
2, def. of 


f ; g g f+ ; g CSChopEqvOrChopPlusChop


Proof:

1
f empty f+
def. of 
2
f ; g g f+ ; g


f empty (f ; f) CSEqvOrChopCS


Proof for :

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

Proof for :

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


f ; f f ChopCSImpCS


Proof:

1
f empty (f ; f)
2
f ; f f
1,Prop


f more f+ CSAndMoreImpChopPlus


Proof:

1
f more f ; f
2
f more f+
1, def. of +


f more (f more) ; f CSAndMoreEqvAndMoreChop


Proof for :

1
(empty (f more) ; f) more (f more) ; f
2
f more (f more) ; f
1, def. of 

Proof for :

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


f more f ; f CSAndMoreImpChopCS


Proof:

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


f more f ; f CSAndMoreImpCSChop


Proof:

1
f more (f more) ; f
2
empty more
3
f empty (f more)
2,Prop
4
(f more) ; f (f more) ((f more) ; (f more))
5
f more ¬f (f more) ; (f more)
6
f empty (f more) ; f
7
f ; f f ((f more) ; f) ; f
8
((f more) ; f) ; f (f more) ; (f ; f)
9
(f more) ¬(f ; f)
(f more) ; (f more) ¬((f more) ; (f ; f))
5, 7, 8,Prop
10
f more more
11
f more f ; f
9, 10,ChopContra

The following lemma is used in the proof of CSAndMoreImpCSChop:


f more ¬f (f more) ; (f more) CSMoreNotImpChopCSAndMore


Proof:

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


f ; f f CSChopCSImpCS


Proof:

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


f ; f f CSChopImpCS


Proof:

1
f f
2
f ; f f ; f
3
f ; f f
4
f ; f f
2, 3,ImpChain


(f) f CSCSImpCS


Proof:

1
empty f
2
(f more) ; f f ; f
3
f ; f f
4
(f more) ; f f
2, 3,ImpChain
5
(f) f
1, 4,CSElim


f g ⇒ ⊢ fg CSImpCS


Proof:

1
f g
given
2
f+ g+
3
empty f+ empty g+
2,Prop
4
f g
3, def. of 


f g ⇒ ⊢ fg CSEqvCS


Proof:

1
f g
given
2
f+ g+
3
empty f+ empty g+
2,Prop
4
fg
3, def. of 


(f g) f AndCSA


Proof:

1
f g f
2
(f g) f


(f g) g AndCSB


Proof:

1
f g g
2
(f g) g


f more (g more) ; f ⇒ ⊢ f g CSIntro


Proof:

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


empty g, (f more) ; g g ⇒ ⊢ fg CSElim


Proof:

1
f empty (f more) ; f
2
empty 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


empty g, f ; g g ⇒ ⊢ fg CSElimWithoutMore


Proof:

1
empty g
given
2
f ; g g
given
3
(f more) ; g f ; g
4
(f more) ; g g
5
f g
1, 4,CSElim


f g ; h ⇒ ⊢ f (g ; f) h CSChopEqvChopOrRule


Proof:

1
f g ; h
given
2
g empty (g ; g)
3
g ; h h ((g ; g) ; h)
4
(g ; g) ; h g ; (g ; h)
ChopAssoc
5
g ; f g ; (g ; h)
6
f (g ; f) h
1, 3, 4, 5,Prop


f ¬h g ; f, g more f g ; h CSChopIntroRule


Proof:

1
f ¬h g ; f
given
2
g more
given
3
g g more
2,Prop
4
g ; f (g more) ; f
5
f (g more) ; f h
1, 4,Prop
6
g empty (g more) ; g
7
g ; h h ((g more) ; g) ; h
8
((g more) ; g) ; h (g more) ; (g ; h)
9
g ; h h (g more) ; (g ; h)
7, 8,Prop
10
f ¬(g ; h) (g more) ; f ¬((g more) ; (g ; h))
5, 9,Prop
11
g more more
12
f g ; h
10, 11,ChopContra


f empty ( w more) ; f ⇒ ⊢ w f w CSImpBox


Proof:

1
f empty ( w more) ; f
given
2
w ¬w ¬empty
3
w f ¬w ( w more) ; f
1, 2,Prop
4
w more ( w more) fin w
5
( w more) ; f (( w more) fin w) ; f
6
(( w more) fin w) ; f ( w more) ; (w f)
7
⊢ ¬w ( w) ¬w
8
( w) ¬w ( w more) ¬w
9
( w more) ; (w f) ( w more) ¬w
( w more) ; ((w f) ¬w)
10
(w f) ¬w ( w more) ; ((w f) ¬w)
3, 5, 6, 7, 8, 9,Prop
11
( w more) ; ((w f) ¬w) more ; ((w f) ¬w)
12
(w f) ¬w more ; ((w f) ¬w)
10, 11,ImpChain
13
w f w


w ( w)w BoxCSEqvBox


Proof for :

1
( w) empty ( w more) ; ( w)
2
( w) empty ( w more) ; ( w)
1,Prop
3
w ( w)w

Proof for :

1
w w
2
w ( w)
3
w w ( w)
1, 2,Prop


w fw ( w f) BoxStateAndCSEqvCS


Proof for :

1
w w
2
f more (f more) ; f
3
w ((f more) ; f) ( w f more) ; ( w f)
4
w f more ( w f) more
5
( w f more) ; ( w f)
(( w f) more) ; ( w f)
6
( w f) more (( w f) more) ; ( w f)
2, 3, 5,Prop
7
w f ( w f)
8
w f w ( w f)
1, 7,Prop

Proof for :

1
( w f) ( w)
2
w ( w)w
3
( w f) f
4
w ( w f)w f
1, 2, 3,Prop

See also the lemma BoxStateAndChopEqvChop for chop.


(f g) fg BaCSImpCS


Proof:

1
f empty (f more) ; f
2
g empty (g more) ; g
3
f¬(g) (f more) ; f¬((g more) ; g)
1, 2,Prop
4
(f g) (f more g more)
5
(f g) (f more g more)
6
(f more g more) (f more) ; f
(g more) ; f
7
(f g) (f more) ; f (g more) ; f
5, 6,Prop
8
(g more) ; f¬((g more) ; g)
(g more) ; (f¬(g))
9
(g more) ; (f¬(g)) more ; (f¬(g))
10
(f g) more ; (f¬(g))
more ; ((f g) f¬(g))
11
(f g) f¬(g)
more ; ((f g) f¬(g))
3, 7, 8, 9, 10,Prop
12
⊢ ¬((f g) f¬(g))
13
(f g) fg
12,Prop

The following corollary can be readily verified:


(f g) fg BaCSEqvCS



f g (f g) BaAndCSImport


Proof:

1
f (g f g)
2
f (g f g)
3
(g f g) g(f g)
4
f g (f g)
2, 3,Prop







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