---

Step * 2 of Lemma st-lookup-distinct


1. T : Id ─→ Type
2. tab : secret-table(T)
3. atoms-distinct(tab)
4. x : Atom1
5. n : ℕ||tab|| 
6. n ≤ ptr(tab)
7. st-atom(tab;n) = x ∈ Atom1
8. ↑isl(st-lookup(tab;x))
⊢ outl(st-lookup(tab;x)) = <key(tab;n), data(tab;n)> ∈ (ℕ + Atom1 × data(T))
BY
{ ((FLemma `st-lookup-outl` [(-1)]) THEN Auto THEN ExRepD THEN Subst' n = n1 ∈ ℤ 0⋅ THEN Auto) }

---

Latex:



1.  T  :  Id  {}\mrightarrow{}  Type
2.  tab  :  secret-table(T)
3.  atoms-distinct(tab)
4.  x  :  Atom1
5.  n  :  \mBbbN{}||tab|| 
6.  n  \mleq{}  ptr(tab)
7.  st-atom(tab;n)  =  x
8.  \muparrow{}isl(st-lookup(tab;x))
\mvdash{}  outl(st-lookup(tab;x))  =  <key(tab;n),  data(tab;n)>


By

((FLemma  `st-lookup-outl`  [(-1)])  THEN  Auto  THEN  ExRepD  THEN  Subst'  n  =  n1  0\mcdot{}  THEN  Auto)

---

Home Index