Duck Source Code:
Doubly Reverse List


title:> Doubly Reverse List
spec:> /net/beowulf/grad/klin/tmp/list.obj
dir:>  /net/cs/htdocs/groups/tatami/demos/list/revrev
<>
********************************************************
goal:> forall L1:List rev(rev(L1)) = L1 
********************************************************
:> Induction (nil,cons)
:> Simplify
:> Lemma-Introduction http://www.cs.ucsd.edu/users/klin/tmp/apprev
:> Rewriting-Rule
:> Simplify
<>


[Back]
Mon Jun 01 16:26:04 PDT 1998