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
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
list_ind: list_ind, 
btrue: tt
, 
it: ⋅
, 
bfalse: ff
, 
deq-member: x ∈b L
, 
reduce: reduce(f;k;as)
, 
bor: p ∨bq
, 
ifthenelse: if b then t else f fi 
, 
Kind-deq: KindDeq
, 
union-deq: union-deq(A;B;a;b)
, 
sumdeq: sumdeq(a;b)
, 
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
, 
product-deq: product-deq(A;B;a;b)
, 
proddeq: proddeq(a;b)
, 
band: p ∧b q
, 
idlnk-deq: IdLnkDeq
, 
id-deq: IdDeq
, 
atom2-deq: Atom2Deq
, 
eq_atom: eq_atom$n(x;y)
, 
pi1: fst(t)
, 
so_lambda: λ2x y.t[x; y]
, 
so_apply: x[s1;s2]
, 
pi2: snd(t)
Latex:
\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:
2016_05_16-AM-11_02_03
Last ObjectModification:
2016_01_17-PM-03_48_38
Theory : event-ordering
Home
Index