The mc_flatten function provided in lists_or_trees theory is a generalization of flatten which was invented by John Mc Carthy (one of early LISP inventors). It not only flattens a tree, but also concatenates a list to the right of the flattening: mc_flatten is thus a combination of flatten and append (called app here) which reduces to flatten when the input list is empty. It is more efficient than flatten, as it contains fewer non tail recursive calls (one instead of two), and uses cons to build up the result instead of using append: it actually reduces the number of conses to the strict minimum, which is the number of leaves in the input tree. Here is the PVS implementation :

mc_flatten(t: bintree[T], l: list[T]): RECURSIVE list[T]
  = CASES t OF
      leaf(data): cons(data, l),
      kons(tl, tr): mc_flatten(tl, mc_flatten(tr, l))
    ENDCASES
  MEASURE t
  BY <<

Here is a graphic idea of mc_flatten algorithm:

The lemma to be proved is

mc_flatten_app_flatten: LEMMA
  (FORALL (t: bintree[T], l: list[T]):
     mc_flatten(t, l) = app(flatten(t), l)) 

Hint: Use well founded induction: (INDUCT "t") proof command. Why?

Note that the leading parameter in mc_flatten recursive function is the tree t (the first parameter):

• Arguments in favor of this claim: 
• t participates in the MEASURE, whereas l is discarded;
• t is subject to a CASES analysis and decomposed, whereas l is not;
• t (first parameter) is changed into tl (resp. tr) in each one of the two recursive calls, whereas l is changed into mc_flatten(tr, l) in the sole outermost recursive call;
• Argument against this claim:
• l is changed into mc_flatten(tr, l) in the outermost recursive call.

Of course t is the leading parameter in flatten recursive function, since it is its sole parameter. Recall that the leading parameter for app is the first one.

Now look at the LEMMA:

• t occurs three times in a leading position (mc_flatten, flatten and app);
• l never occurs in a leading position.

Hence the induction should be tempted on t; it is not sure whether it would be a good idea to skolemize l before performing the induction, as this weakens the induction hypothesis. We did not try to do this partial skolemization in the proof given below. Don't immediately look at this proof!