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