Associativity of Append Function
We want to prove
L1,L2,L3:List (append(append(L1, L2), L3) = append(L1, append(L2, L3)))
.
We use induction on
List
to prove this goal. For this, we use the induction scheme based on signature
{nil, cons}
for
List
. Induction requires that we do the following:
Base case : prove assertion for
L1 = nil
.
Quantifier elimination introduces new
constants l2 l3 :List
.
Show
append(append(nil, l2), l3) = append(nil, append(l2, l3))
by reduction.
Induction case : prove assertion for
L1 = cons(M,L)
assume it for
L1 = L
.
Quantifier elimination introduces new
constants m :Nat and l :List
.
Implication elimination assumes
L2,L3:List (append(append(l, L2), L3) = append(l, append(L2, L3)))
.
Change hypothesis
L2,L3:List (append(append(l, L2), L3) = append(l, append(L2, L3)))
to rewritng rule.
Quantifier elimination introduces new
constants l2 l3 :List
.
Show
append(append(cons(m,l), l2), l3) = append(cons(m,l), append(l2, l3))
by reduction.
This page was generated
by Kumo on
Mon Jun 01 16:18:55 PDT 1998