Duck Source Code:
Associativity of Append Function


title:> Associativity of Append Function
spec:> /net/beowulf/grad/klin/tmp/list.obj
dir:>  /net/cs/htdocs/groups/tatami/demos/list/appendass
<>
********************************************************
goal:> forall L1:List forall L2:List forall L3:List append(append(L1, L2), L3) = append(L1, append(L2, L3))
********************************************************
:> Induction(nil, cons)
:> Simplify
:> Simplify
<>


[Back]
Mon Jun 01 16:18:53 PDT 1998