---

Step * of Lemma st-ptr-wf2

∀[T:Id ─→ Type]. ∀[tab:secret-table(T)].  ptr(tab) ∈ ℕ||tab||  supposing ↑isl(next(tab))
BY
{ (Auto
   THEN All (\h. RepUR ``st-next st-length secret-table st-ptr`` h)⋅
   THEN Try (AutoSplit)
   THEN (DVar `tab' THEN Reduce 0)
   THEN Auto
   THEN SplitOnHypITE -1 
   THEN All Reduce
   THEN Auto) }

---

Latex:


\mforall{}[T:Id  {}\mrightarrow{}  Type].  \mforall{}[tab:secret-table(T)].    ptr(tab)  \mmember{}  \mBbbN{}||tab||    supposing  \muparrow{}isl(next(tab))


By

(Auto
  THEN  All  (\mbackslash{}h.  RepUR  ``st-next  st-length  secret-table  st-ptr``  h)\mcdot{}
  THEN  Try  (AutoSplit)
  THEN  (DVar  `tab'  THEN  Reduce  0)
  THEN  Auto
  THEN  SplitOnHypITE  -1 
  THEN  All  Reduce
  THEN  Auto)

---

Home Index