---

Step * of Lemma st-decrypt_wf

∀[T:Id ─→ Type]. ∀[tab:secret-table(T)]. ∀[kx:ℕ + Atom1 × Atom1].  (decrypt(tab;kx) ∈ data(T)?)
BY
{ (Auto
   THEN (D (-1))
   THEN Unfold `st-decrypt` 0
   THEN Reduce 0
   THEN SplitOnConclITE
   THEN Auto
   THEN Unfold `bfalse` 0
   THEN Auto) }

---

Latex:


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


By

(Auto
  THEN  (D  (-1))
  THEN  Unfold  `st-decrypt`  0
  THEN  Reduce  0
  THEN  SplitOnConclITE
  THEN  Auto
  THEN  Unfold  `bfalse`  0
  THEN  Auto)

---

Home Index