---

Step * of Lemma st-key-match_wf

∀[T:Id ─→ Type]. ∀[tab:secret-table(T)]. ∀[k1,k2:ℕ + Atom1].  (st-key-match(tab;k1;k2) ∈ 𝔹)
BY
{ (Auto
   THEN Unfold `st-key-match` 0
   THEN DVar `k1'
   THEN DVar `k2'
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN AutoBoolCase x <z ptr(tab)⋅
   THEN AutoBoolCase x <z ||tab|| ⋅) }

---

Latex:


\mforall{}[T:Id  {}\mrightarrow{}  Type].  \mforall{}[tab:secret-table(T)].  \mforall{}[k1,k2:\mBbbN{}  +  Atom1].    (st-key-match(tab;k1;k2)  \mmember{}  \mBbbB{})


By

(Auto
  THEN  Unfold  `st-key-match`  0
  THEN  DVar  `k1'
  THEN  DVar  `k2'
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  AutoBoolCase  x  <z  ptr(tab)\mcdot{}
  THEN  AutoBoolCase  x  <z  ||tab||  \mcdot{})

---

Home Index