---

Step * 1 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
⊢ ↑isl(st-lookup(tab;x))
BY
{ (RWO "st-lookup-property" 0 THEN Auto THEN (InstConcl [n])⋅ 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
\mvdash{}  \muparrow{}isl(st-lookup(tab;x))


By

(RWO  "st-lookup-property"  0  THEN  Auto  THEN  (InstConcl  [n])\mcdot{}  THEN  Auto)

---

Home Index