---

{ [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 let x,y2 = qa 
             in let x2,y3 = x 
                in if x1=2 x2
                    then let x@0,y2@0 = y1 
                         in let x,y4 = y3 
                            in if x@0=2 x
                                then if y2@0=2 y4
                                      then if y=2 y2
                                            then tt
                                            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 
    ~ deq-member(KindDeq;k;L)) }

{ Proof }

---

Definitions occuring in Statement :  Kind-deq: KindDeq,  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],  list_ind: list_ind def,  sqequal: s ~ t,  deq-member: deq-member(eq;x;L),  atom_eq: atomeqn def
Definitions :  atom_eq: atomeqn def,  spread: spread def,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x ,  deq-member: deq-member(eq;x;L),  strong-subtype: strong-subtype(A;B),  le: A  B,  ge: i  j ,  not: A,  less_than: a < b,  product: x:A  B[x],  and: P  Q,  uiff: uiff(P;Q),  guard: {T},  implies: P  Q,  bool: ,  bfalse: ff,  list_ind: list_ind def,  sq_type: SQType(T),  uimplies: b supposing a,  universe: Type,  subtype_rel: A r B,  isect: x:A. B[x],  uall: [x:A]. B[x],  top: Top,  all: x:A. B[x],  function: x:A  B[x],  equal: s = t,  sqequal: s ~ t,  member: t  T,  lambda: x.A[x],  eqof: eqof(d),  id-deq: IdDeq,  product-deq: product-deq(A;B;a;b),  CollapseTHEN: Error :CollapseTHEN,  tactic: Error :tactic
Lemmas :  top_wf,  bfalse_wf,  deq-member_wf,  bool_subtype_base,  bool_wf,  subtype_base_sq

---

\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  let  x,y2  =  qa 
                      in  let  x2,y3  =  x 
                            in  if  x1=2  x2
                                    then  let  x@0,y2@0  =  y1 
                                              in  let  x,y4  =  y3 
                                                    in  if  x@0=2  x
                                                            then  if  y2@0=2  y4
                                                                        then  if  y=2  y2
                                                                                    then  tt
                                                                                    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{}  deq-membe\000Cr(KindDeq;k;L))


Date html generated: 2011_08_10-AM-07_52_45
Last ObjectModification: 2011_06_18-AM-08_14_44

Home Index