---

Step * of Lemma st-encrypt_wf

∀[T:Id ─→ Type]. ∀[tab:secret-table(T)]. ∀[keyv:ℕ + Atom1 × data(T)].  (encrypt(tab;keyv) ∈ secret-table(T))
BY
{ (Auto
   THEN DVar `tab'
   THEN DVar `t1'
   THEN DVar `keyv'
   THEN RepUR ``st-encrypt secret-table`` 0
   THEN SplitOnConclITE
   THEN Auto) }

---

Latex:


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


By

(Auto
  THEN  DVar  `tab'
  THEN  DVar  `t1'
  THEN  DVar  `keyv'
  THEN  RepUR  ``st-encrypt  secret-table``  0
  THEN  SplitOnConclITE
  THEN  Auto)

---

Home Index