ITL
© 1996-2018







2.6 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 

qed

empty f EmptyImpCS

Proof:

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

qed

Here is an straightforward corollary:

¬f more NotCSImpMore

f+ f ChopPlusImpCS

Proof:

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

qed

f f ImpCS

Proof:

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

qed

f ; g g f+ ; g CSChopEqvOrChopPlusChop

Proof:

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

qed

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

qed

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

qed

f ; f f ChopCSImpCS

Proof:

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

qed

f more f+ CSAndMoreImpChopPlus

Proof:

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

qed

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 

qed

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

qed

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

qed

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

qed

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

qed

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

qed

f ; f f CSChopImpCS

Proof:

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

qed

(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

qed

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 

qed

f g ⇒ ⊢ fg CSEqvCS

Proof:

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

qed

(f g) f AndCSA

Proof:

1
f g f
2
(f g) f

qed

(f g) g AndCSB

Proof:

1
f g g
2
(f g) g

qed

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

qed

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

qed

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

qed

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

qed

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

qed

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

qed

w ( w)w BoxCSEqvBox

Proof for :

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

qed

Proof for :

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

qed

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

qed

Proof for :

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

qed

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

qed

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

qed







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