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
Lemmas :
lifting-strict-decide,
has-value_wf_base,
base_wf,
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:
2015_07_17-AM-09_15_14
Last ObjectModification:
2015_01_28-AM-07_53_09
Home
Index