Nuprl Lemma : remove-repeats-normal-form
∀[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 : 
remove-repeats: remove-repeats(eq;L)
, 
list_ind: list_ind, 
cons: [a / b]
, 
nil: []
, 
ifthenelse: if b then t else f fi 
, 
uall: ∀[x:A]. B[x]
, 
top: Top
, 
apply: f a
, 
sqequal: s ~ t
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
list_ind: list_ind, 
cons: [a / b]
, 
ifthenelse: if b then t else f fi 
, 
nil: []
, 
it: ⋅
, 
remove-repeats: remove-repeats(eq;L)
, 
filter: filter(P;l)
, 
reduce: reduce(f;k;as)
, 
bnot: ¬bb
, 
so_lambda: so_lambda(x,y,z,w.t[x; y; z; w])
, 
so_apply: x[s1;s2;s3;s4]
, 
so_lambda: λ2x.t[x]
, 
top: Top
, 
so_apply: x[s]
, 
uimplies: b supposing a
, 
strict4: strict4(F)
, 
and: P ∧ Q
, 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
has-value: (a)↓
, 
prop: ℙ
, 
guard: {T}
, 
or: P ∨ Q
, 
squash: ↓T
, 
bfalse: ff
, 
btrue: tt
Latex:
\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:
2016_05_16-AM-11_02_17
Last ObjectModification:
2016_01_17-PM-03_47_33
Theory : event-ordering
Home
Index