---

Step * of Lemma st-length-encrypt

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

---

Latex:


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


By

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

---

Home Index