---

Step * of Lemma st-lookup_wf

∀[T:Id ⟶ Type]. ∀[tab:secret-table(T)]. ∀[x:Atom1].  (st-lookup(tab;x) ∈ ℕ + Atom1 × data(T)?)
BY
{ (Auto
   THEN DVar `tab'
   THEN DVar `t1'
   THEN RepUR ``st-lookup st-length `` 0
   THEN (GenConclAtAddr [2; 1])
   THEN Try (Complete (Auto))) }

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

---

Latex:

---

Latex:
\mforall{}[T:Id  {}\mrightarrow{}  Type].  \mforall{}[tab:secret-table(T)].  \mforall{}[x:Atom1].    (st-lookup(tab;x)  \mmember{}  \mBbbN{}  +  Atom1  \mtimes{}  data(T)?)


By

---

Latex:
(Auto
  THEN  DVar  `tab'
  THEN  DVar  `t1'
  THEN  RepUR  ``st-lookup  st-length  ``  0
  THEN  (GenConclAtAddr  [2;  1])
  THEN  Try  (Complete  (Auto)))

---

Home Index