---

Step * of Lemma st-lookup-distinct

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

1
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
⊢ ↑isl(st-lookup(tab;x))

2
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))

---

Latex:


\mforall{}[T:Id  {}\mrightarrow{}  Type].  \mforall{}[tab:secret-table(T)].
    \mforall{}[x:Atom1].  \mforall{}[n:\mBbbN{}||tab||  ].
        ((\muparrow{}isl(st-lookup(tab;x)))  c\mwedge{}  (outl(st-lookup(tab;x))  =  <key(tab;n),  data(tab;n)>))  supposing 
              ((st-atom(tab;n)  =  x)  and 
              (n  \mleq{}  ptr(tab))) 
    supposing  atoms-distinct(tab)


By

Auto

---

Home Index