---

Step * of Lemma st-next_wf

∀[T:Id ─→ Type]. ∀[tab:secret-table(T)].  (next(tab) ∈ ℕ||tab||  × Atom1?)
BY
{ (Auto THEN Unfolds ``secret-table st-next`` 0 THEN SplitOnConclITE THEN Auto' THEN Unfold `bfalse` 0 THEN Auto) }

---

Latex:


\mforall{}[T:Id  {}\mrightarrow{}  Type].  \mforall{}[tab:secret-table(T)].    (next(tab)  \mmember{}  \mBbbN{}||tab||    \mtimes{}  Atom1?)


By

(Auto
  THEN  Unfolds  ``secret-table  st-next``  0
  THEN  SplitOnConclITE
  THEN  Auto'
  THEN  Unfold  `bfalse`  0
  THEN  Auto)

---

Home Index