Nuprl Definition : 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) ∧b n <z ||tab|| ) ∧b st-atom(tab;n) =a1 a
| inr(a) =>
case k2 of inl(n) => (n <z ptr(tab) ∧b n <z ||tab|| ) ∧b st-atom(tab;n) =a1 a | inr(b) => ff
Definitions occuring in Statement :
st-atom: st-atom(tab;n),
st-ptr: ptr(tab),
st-length: ||tab|| ,
band: p ∧b q,
eq_atom: eq_atom$n(x;y),
lt_int: i <z j,
bfalse: ff,
decide: case b of inl(x) => s[x] | inr(y) => t[y]
FDL editor aliases :
st-key-match
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:
2015_07_17-AM-08_56_03
Last ObjectModification:
2013_03_25-PM-01_53_08
Home
Index