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