Nuprl Lemma : kind-member-normal-form
∀[k,L:Top].
(rec-case(L) of
[] => ff
a::_ =>
r.case a
of inl(pa) =>
case k
of inl(qa) =>
let x,y = pa
in let x1,y1 = x
in if x1=2 let x,y = qa
in let x,y = x
in x
then let x2,y2 = y1
in if x2=2 let x,y = qa
in let x,y = x
in let x,y = y
in x
then if y2=2 let x,y = qa
in let x,y = x
in let x,y = y
in y
then if y=2 let x,y = qa
in y
then inl Ax
else r
else r
else r
else r
| inr(_) =>
r
| inr(pb) =>
case k of inl(_) => r | inr(qb) => if pb=2 qb then tt else r ~ k ∈b L))
Proof
Definitions occuring in Statement :
Kind-deq: KindDeq,
deq-member: x ∈b L),
list_ind: list_ind,
atom_eq: atomeqn def,
bfalse: ff,
btrue: tt,
uall: ∀[x:A]. B[x],
top: Top,
spread: spread def,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inl: inl x,
sqequal: s ~ t,
axiom: Ax
Lemmas :
lifting-strict-decide,
has-value_wf_base,
base_wf,
base_sq,
lifting-strict-atom_eq2,
lifting-strict-spread,
value-type-has-value,
atom2-value-type,
strict4-spread,
top_wf,
pair-eta
\mforall{}[k,L:Top].
(rec-case(L) of
[] => ff
a::$_{}$ =>
r.case a
of inl(pa) =>
case k
of inl(qa) =>
let x,y = pa
in let x1,y1 = x
in if x1=2 let x,y = qa
in let x,y = x
in x
then let x2,y2 = y1
in if x2=2 let x,y = qa
in let x,y = x
in let x,y = y
in x
then if y2=2 let x,y = qa
in let x,y = x
in let x,y = y
in y
then if y=2 let x,y = qa
in y
then inl Ax
else r
else r
else r
else r
| inr($_{}$) =>
r
| inr(pb) =>
case k of inl($_{}$) => r | inr(qb) => if pb=2 qb then tt else r \msim{} k \mmember{}\msubb{} L))
Date html generated:
2015_07_17-AM-09_15_09
Last ObjectModification:
2015_04_23-PM-10_57_44
Home
Index