---

Step * of Lemma st-lookup-property

∀[T:Id ─→ Type]
  ∀tab:secret-table(T). ∀x:Atom1.
    (↑isl(st-lookup(tab;x)) ⇐⇒ ∃n:ℕ||tab|| . ((n ≤ ptr(tab)) ∧ (st-atom(tab;n) = x ∈ Atom1)))
BY
{ ((UnivCD THENA Auto)
   THEN DVar `tab'
   THEN DVar `t1'
   THEN RepUR ``st-lookup st-length st-ptr st-atom `` 0
   THEN (GenConclAtAddr [1; 1; 1; 1])
   THEN Try (Complete (Auto))) }

1
.....wf..... 
1. [T] : Id ─→ Type
2. K : ℕ@i
3. t2 : ℕ@i
4. t3 : ℕK ─→ (Atom1 × ℕ + Atom1 × data(T))@i
5. x : Atom1@i
⊢ mu(λn.(t2 <z n ∨bK ≤z n ∨bfst((t3 n)) =a1 x)) ∈ ℕ

2
1. [T] : Id ─→ Type
2. K : ℕ@i
3. t2 : ℕ@i
4. t3 : ℕK ─→ (Atom1 × ℕ + Atom1 × data(T))@i
5. x : Atom1@i
6. v : ℕ@i
7. mu(λn.(t2 <z n ∨bK ≤z n ∨bfst((t3 n)) =a1 x)) = v ∈ ℕ@i
⊢ ↑isl(let n = v in
           if t2 <z n ∨bK ≤z n then inr ⋅  else inl (snd((t3 n))) fi )
⇐⇒ ∃n:ℕK. ((n ≤ t2) ∧ ((fst((t3 n))) = x ∈ Atom1))

---

Latex:


\mforall{}[T:Id  {}\mrightarrow{}  Type]
    \mforall{}tab:secret-table(T).  \mforall{}x:Atom1.
        (\muparrow{}isl(st-lookup(tab;x))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}||tab||  .  ((n  \mleq{}  ptr(tab))  \mwedge{}  (st-atom(tab;n)  =  x)))


By

((UnivCD  THENA  Auto)
  THEN  DVar  `tab'
  THEN  DVar  `t1'
  THEN  RepUR  ``st-lookup  st-length  st-ptr  st-atom  ``  0
  THEN  (GenConclAtAddr  [1;  1;  1;  1])
  THEN  Try  (Complete  (Auto)))

---

Home Index