ITL
© 1996-2018







2.9 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 >

qed

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

qed

(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

qed

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

qed

f ; f ; ; f f ChopGroupImpCS

The proof is by induction on the number of <chops>.

Proof when no <chops>:

1
f f

qed

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

qed

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

qed

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

qed

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

qed

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)

qed







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