---

Step * of 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))
BY
{ (Auto
   THEN (MoveToConcl (-1))
   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)
     ∧ (outl(let n = v in
                 if t2 <z n ∨bK ≤z n then inr ⋅  else inl (snd((t3 n))) fi )
       = <key(<K, t2, t3>;n), data(<K, t2, t3>;n)>
       ∈ (ℕ + Atom1 × data(T)))))

---

Latex:


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


By

(Auto
  THEN  (MoveToConcl  (-1))
  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