---

{ [eq,L:Top].
    (rec-case(L) of
     [] => []
     a::_ =>
      r.[a / 
         rec-case(r) of
         [] => []
         a@0::_ =>
          r.if eq a@0 a then r else [a@0 / r] fi ] ~ remove-repeats(eq;L)) }

{ Proof }

---

Definitions occuring in Statement :  ifthenelse: if b then t else f fi ,  uall: [x:A]. B[x],  top: Top,  apply: f a,  list_ind: list_ind def,  cons: [car / cdr],  nil: [],  sqequal: s ~ t,  remove-repeats: remove-repeats(eq;L)
Definitions :  uall: [x:A]. B[x],  ifthenelse: if b then t else f fi ,  remove-repeats: remove-repeats(eq;L),  member: t  T,  filter: filter(P;l),  bnot: b,  reduce: reduce(f;k;as),  bfalse: ff,  btrue: tt
Lemmas :  top_wf

---

\mforall{}[eq,L:Top].
    (rec-case(L)  of
      []  =>  []
      a::$_{}$  =>
        r.[a  /  rec-case(r)  of  []  =>  []  |  a@0::$_{}$  =>  r.if  eq  a@0  a  then  r  else  [a@\000C0  /  r]  fi  ] 
    \msim{}  remove-repeats(eq;L))


Date html generated: 2011_08_10-AM-07_52_53
Last ObjectModification: 2011_06_18-AM-08_14_50

Home Index