### Nuprl Lemma : st-lookup-outl

`∀[T:Id ─→ Type]`
`  ∀tab:secret-table(T). ∀x:Atom1.`
`    ∃n:ℕ||tab|| `
`     ((n ≤ ptr(tab))`
`     ∧ (st-atom(tab;n) = x ∈ Atom1)`
`     ∧ (outl(st-lookup(tab;x)) = <key(tab;n), data(tab;n)> ∈ (ℕ + Atom1 × data(T)))) `
`    supposing ↑isl(st-lookup(tab;x))`

Proof

Definitions occuring in Statement :  st-lookup: `st-lookup(tab;x)` st-data: `data(tab;n)` st-key: `key(tab;n)` st-atom: `st-atom(tab;n)` st-ptr: `ptr(tab)` st-length: `||tab|| ` secret-table: `secret-table(T)` data: `data(T)` Id: `Id` int_seg: `{i..j-}` nat: `ℕ` atom: `Atom\$n` outl: `outl(x)` assert: `↑b` isl: `isl(x)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` le: `A ≤ B` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` and: `P ∧ Q` function: `x:A ─→ B[x]` pair: `<a, b>` product: `x:A × B[x]` union: `left + right` natural_number: `\$n` universe: `Type` equal: `s = t ∈ T`
Lemmas :  mu_wf le_int_wf bool_wf eqtt_to_assert assert_of_le_int bor_wf lt_int_wf btrue_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot le_wf eq_atom_wf1 decidable__lt false_wf not-le-2 condition-implies-le minus-add minus-one-mul add-swap add-commutes add_functionality_wrt_le le-add-cancel lelt_wf data_wf nat_wf iff_transitivity assert_wf or_wf less_than_wf true_wf iff_weakening_uiff assert_of_bor assert_of_lt_int add-mul-special zero-mul add-zero add-associates mu-property set_subtype_base int_subtype_base equal-wf-T-base bnot_wf uiff_transitivity assert_functionality_wrt_uiff bnot_thru_bor band_wf squash_wf bnot_of_lt_int bnot_of_le_int assert_of_band pair_eta_rw iff_weakening_equal atom1_subtype_base less_than_transitivity1 less_than_irreflexivity uall_wf isect_wf not_wf assert_of_eq_atom1
\mforall{}[T:Id  {}\mrightarrow{}  Type]
\mforall{}tab:secret-table(T).  \mforall{}x:Atom1.
\mexists{}n:\mBbbN{}||tab||
((n  \mleq{}  ptr(tab))  \mwedge{}  (st-atom(tab;n)  =  x)  \mwedge{}  (outl(st-lookup(tab;x))  =  <key(tab;n),  data(tab;n)>))
supposing  \muparrow{}isl(st-lookup(tab;x))

Date html generated: 2015_07_17-AM-08_57_02
Last ObjectModification: 2015_02_04-PM-06_28_19

Home Index