helphome pageduck scriptspecificationfirst proof pagepage 3page 2 1 2 3 xclosing page

Inductive Properties of Lists, Part 1
Associativity of Append

We want to prove
( L1  L2  L3  : List  ) append(append(L1 , L2) , L3) = append(L1 , append(L2 , L3)) .
We use induction on L1 to prove this goal. For this, we use the induction scheme based on the signature { nil, cons } for List. Induction requires that we do the following:
  1. Base case: prove the assertion for L1 = nil .
    • Quantifier elimination introduces the new constant(s) l2, l3 : List  .
    • We show append(append(nil , l2) , l3) = append(nil , append(l2 , l3)) by reduction.
  2. Induction case: assume the assertion for L1 = L0 , and then prove it for L1 = cons(N0 , L0) .

And thus the main goal is proved.


Since this proof attempt succeeds, our quest for a proof of the original goal would appear to be finished. This impression is confirmed by our second proof website for this goal, where trying to prove the three results in the reverse order of that in which they were discovered does in fact prove the original goal.

BOBJ proof scoreLeft    Up    Down    Right   

       This page was generated by Kumo on Mon Nov 20 10:18:44 PST 2000.