ITL
© 1996-2018







11 Properties of groups of chops


(f1 ; ; fm) ; (g1 ; ; gn) f1 ; ; fm ; g1 ; ; gn ChopGroupMerge


We prove this by induction on m.
Proof for m=1:

1
f1 ; (g1 ; ; gn) f1 ; g1 ; ; gn
def. of  < chop >

Proof for m > 1:

1
(f1 ; f2 ; ; fm) ; (g1 ; ; gn)
f1 ; ((f2 ; ; fm) ; (g1 ; ; gn))
2
(f2 ; ; fm) ; (g1 ; ; gn)
f2 ; ; fm ; g1 ; ; gn
induction hypothesis
3
f1 ; ((f2 ; ; fm) ; (g1 ; ; gn))
f1 ; (f2 ; ; fm ; g1 ; ; gn)
4
(f1 ; f2 ; ; fm) ; (g1 ; ; gn)
f1 ; f2 ; ; fm ; g1 ; ; gn
1, 3,EqvChain


(f1,1 ; ; f1,l1) ; ; (fn,1 ; ; fn,ln) ChopGroupGroupMerge
f1,1 ; ; f1,l1 ; ; fn,1 ; ; fn,ln,


where there are n groups and for each group 1 i < n, there are li formulas. Proof is by induction on n.
Proof for n = 1:

1
f1,1 ; ; f1,l1 f1,1 ; ; f1,l1

Proof for n > 1:

1
(f2,1 ; ; f2,l2) ; ; (fn,1 ; ; fn,ln)
f2,1 ; ; f2,l2 ; ; fn,1 ; ; fn,ln
induction hypothesis
2
(f1,1 ; ; f1,l1) ; (f2,1 ; ; f2,l2) ; ; (fn,1 ; ; fn,ln)
(f1,1 ; ; f1,l1) ; (f2,1 ; ; f2,l2 ; ; fn,1 ; ; fn,ln)
3
(f1,1 ; ; f1,l1) ; (f2,1 ; ; f2,l2 ; ; fn,1 ; ; fn,ln)
f1,1 ; ; f1,l1 ; f2,1 ; ; f2,l2 ; ; fn,1 ; ; fn,ln
4
(f1,1 ; ; f1,l1) ; (f2,1 ; ; f2,l2) ; ; (fn,1 ; fn,2 ; ; fn,ln)
f1,1 ; ; f1,l1 ; f2,1 ; ; f2,l2 ; ; fn,1 ; ; fn,ln
2, 3,EqvChain


f ; f ; ; f f ChopGroupImpCS


The proof is by induction on the number of <chops>.
Proof when no <chops>:

1
f f

Proof for at n occurrences of <chops> where n 1:

1
f ; ; f f
induction for n 1 <chops>
2
f ; f ; ; f f ; f
3
f ; f f
4
f ; f ; ; f f
2, 3,ImpChain


f1 g, , fn g ⇒ ⊢ (f1 ; ; fn) g MultChopImpCS


Proof:

1
fi g, for 1 i n
given
2
f1 ; ; fn g ; ; g
3
g ; ; g g
4
f1 ; ; fn g
2, 3,ImpChain


w f g ; (w1 f1), w1 f1 g1 ; (w2 f2) NestedChopImpChop
⇒ ⊢ w f g ; g1 ; (w2 f2)


Proof:

1
w f g ; (w1 f1)
given
2
w1 f1 g1 ; (w2 f2)
given
3
g ; (w1 f1) g ; g1 ; (w2 f2)
4
w f g ; g1 ; (w2 f2)
1, 3,ImpChain


w1 f1 g1 ; (w2 f2),,wn1 fn1 gn1 ; (wn fn) MultNestedChopImpChop
⇒ ⊢ w1 f1 g1 ; ; gn1 ; (wn gn)


The proof is by induction on n.
Proof for n = 1:

1
w1 f1 w1 f1

Proof for n > 1:

1
w1 f1 g1 ; (w2 f2)
given
2
wi fi gi ; (wi+1 fi+1), for each i: 1 < i < n
given
3
w2 f2 g2 ; ; gn1 ; (wn gn)
2, induction hypothesis
4
w1 f1 g1 ; g2 ; ; gn1 ; (wn gn)







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