---

Step * of Lemma encryption-key-free-from-atom

∀[k:Key]. ∀[a:Atom1].  uiff(¬(a ∈ encryption-key-atoms(k));a#k:Key)
BY
{ ((D 0 THENA Auto)
   THEN D 1
   THEN Try (D 1)
   THEN RepUR ``encryption-key encryption-key-atoms`` 0
   THEN (At ⌜Type⌝ (D 0)⋅ THENA Auto)
   THEN D 0
   THEN (At ⌜Type⌝ (D 0)⋅ THENA Auto)
   THEN All (RWO "nil_member member_singleton")⋅
   THEN Auto
   THEN Try ((FreeFromAtomApElim ⌜x⌝⋅ THEN Auto))
   THEN Try ((FreeFromAtomApElim ⌜y⌝⋅ THEN Auto))
   THEN Try ((FreeFromAtomApElim ⌜y1⌝⋅ THEN Auto))
   THEN Try (((D 0 THENA Auto) THEN RevHypSubst'(-1) (-2))⋅)
   THEN ((FLemma `free-from-atom-outr2` [-2] THENA (Reduce 0 THEN Auto)) THEN Reduce (-1))
   THEN ((FLemma `free-from-atom-outl2` [-1] THENA (Reduce 0 THEN Complete (Auto)))
   ORELSE (FLemma `free-from-atom-outr2` [-1] THENA (Reduce 0 THEN Complete (Auto)))
   )
   THEN Reduce (-1)
   THEN FreeFromAtomAbsurd) }

---

Latex:

---

Latex:
\mforall{}[k:Key].  \mforall{}[a:Atom1].    uiff(\mneg{}(a  \mmember{}  encryption-key-atoms(k));a\#k:Key)


By

---

Latex:
((D  0  THENA  Auto)
  THEN  D  1
  THEN  Try  (D  1)
  THEN  RepUR  ``encryption-key  encryption-key-atoms``  0
  THEN  (At  \mkleeneopen{}Type\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto)
  THEN  D  0
  THEN  (At  \mkleeneopen{}Type\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto)
  THEN  All  (RWO  "nil\_member  member\_singleton")\mcdot{}
  THEN  Auto
  THEN  Try  ((FreeFromAtomApElim  \mkleeneopen{}x\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  Try  ((FreeFromAtomApElim  \mkleeneopen{}y\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  Try  ((FreeFromAtomApElim  \mkleeneopen{}y1\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  Try  (((D  0  THENA  Auto)  THEN  RevHypSubst'(-1)  (-2))\mcdot{})
  THEN  ((FLemma  `free-from-atom-outr2`  [-2]  THENA  (Reduce  0  THEN  Auto))  THEN  Reduce  (-1))
  THEN  ((FLemma  `free-from-atom-outl2`  [-1]  THENA  (Reduce  0  THEN  Complete  (Auto)))
  ORELSE  (FLemma  `free-from-atom-outr2`  [-1]  THENA  (Reduce  0  THEN  Complete  (Auto)))
  )
  THEN  Reduce  (-1)
  THEN  FreeFromAtomAbsurd)

---

Home Index