---

Step * of Lemma st-atom-encrypt

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

1
1. T : Id ─→ Type
2. K : ℕ
3. t2 : ℕ
4. t3 : ℕK ─→ (Atom1 × ℕ + Atom1 × data(T))
5. k1 : ℕ + Atom1
6. k2 : data(T)
7. n : ℕK
8. t2 < K
⊢ (fst(((λy.if (y =z t2) then <fst((t3 t2)), k1, k2> else t3 y fi ) n))) = (fst((t3 n))) ∈ Atom1

---

Latex:


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


By

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

---

Home Index