---

Step * of 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))
BY
{ (UniformUnivCD Auto THEN SymbCompNormalize 2 0 THEN EqCD) }

---

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))


By

(UniformUnivCD  Auto  THEN  SymbCompNormalize  2  0  THEN  EqCD)

---

Home Index