---

inning_test(t) ==
  s,x.
   let vs,i = s in
     case x
    of inl(v) => (i = 0)
     | inr(p) => let j,v = p in
                   i z j ((j = i - 1)  (||vs|| = 2 * t))

---

Definitions :  lambda: x.A[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  spread: spread def,  bor: p q,  le_int: i z j,  band: p  q,  subtract: n - m,  eq_int: (i = j),  length: ||as||,  multiply: n * m,  natural_number: $n
FDL editor aliases :  inning_test

---

inning\_test(t)  ==
    \mlambda{}s,x.
      let  vs,i  =  s  in
          case  x
        of  inl(v)  =>  (i  =\msubz{}  0)
          |  inr(p)  =>  let  j,v  =  p  in
                                      i  \mleq{}z  j  \mvee{}\msubb{}((j  =\msubz{}  i  -  1)  \mwedge{}\msubb{}  (||vs||  =\msubz{}  2  *  t))


Date html generated: 2010_08_27-PM-08_30_04
Last ObjectModification: 2010_06_23-PM-11_54_57

Home Index