---

st-key-match(tab;k1;k2) ==
  case k1
  of inl(n) => case k2
               of inl(m) => ff
                | inr(a) => (n <z ptr(tab)  n <z ||tab|| )
                             st-atom(tab;n) =a1 a
   | inr(a) => case k2
               of inl(n) => (n <z ptr(tab)  n <z ||tab|| )
                             st-atom(tab;n) =a1 a
                | inr(b) => ff

---

Definitions :  decide: case b of inl(x) => s[x] | inr(y) => t[y],  band: p  q,  st-ptr: ptr(tab),  lt_int: i <z j,  st-length: ||tab|| ,  eq_atom: eq_atom$n(x;y),  st-atom: st-atom(tab;n),  bfalse: ff
FDL editor aliases :  st-key-match

---

st-key-match(tab;k1;k2)  ==
    case  k1
    of  inl(n)  =>  case  k2
                              of  inl(m)  =>  ff
                                |  inr(a)  =>  (n  <z  ptr(tab)  \mwedge{}\msubb{}  n  <z  ||tab||  )  \mwedge{}\msubb{}  st-atom(tab;n)  =a1  a
      |  inr(a)  =>  case  k2
                              of  inl(n)  =>  (n  <z  ptr(tab)  \mwedge{}\msubb{}  n  <z  ||tab||  )  \mwedge{}\msubb{}  st-atom(tab;n)  =a1  a
                                |  inr(b)  =>  ff


Date html generated: 2010_08_27-AM-09_34_00
Last ObjectModification: 2009_12_16-AM-01_15_06

Home Index