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