---

Step * of Lemma ses-fresh-sequence_wf

∀[f:SecurityData ─→ (Atom1?)]. ∀[A:Id]. ∀[pas:ProtocolAction List].  (ses-fresh-sequence(f;A;pas) ∈ ℙ)
BY
{ ((UnivCD THENA Auto)
   THEN (Subst' ses-fresh-sequence(f;A;pas) ~ ∀i:ℕ||pas||
                                                pa-is-sign-implies(pas[i];v.((fst(snd(v))) = A ∈ Id)
                                                ∧ (∃j:ℕi
                                                    pa-is-new-and(pas[j];n.((↑isl(f (fst(v))))
                                                    ∧ (outl(f (fst(v))) = n ∈ Atom1))
                                                    ∧ (∀k:{j + 1..i-}
                                                         pa-is-sign-implies(pas[k];v'.(↑isl(f (fst(v'))))
                                                         ⇒ (¬(outl(f (fst(v'))) = n ∈ Atom1))))))) 0
         THENA (RepUR ``ses-fresh-sequence pa-is-sign-implies pa-is-new-and`` 0 THEN Auto)
         )
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f:SecurityData  {}\mrightarrow{}  (Atom1?)].  \mforall{}[A:Id].  \mforall{}[pas:ProtocolAction  List].
    (ses-fresh-sequence(f;A;pas)  \mmember{}  \mBbbP{})


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Subst'  ses-fresh-sequence(f;A;pas) 
              \msim{}  \mforall{}i:\mBbbN{}||pas||
                      pa-is-sign-implies(pas[i];v.((fst(snd(v)))  =  A)
                      \mwedge{}  (\mexists{}j:\mBbbN{}i
                              pa-is-new-and(pas[j];n.((\muparrow{}isl(f  (fst(v))))  \mwedge{}  (outl(f  (fst(v)))  =  n))
                              \mwedge{}  (\mforall{}k:\{j  +  1..i\msupminus{}\}
                                        pa-is-sign-implies(pas[k];v'.(\muparrow{}isl(f  (fst(v'))))
                                        {}\mRightarrow{}  (\mneg{}(outl(f  (fst(v')))  =  n)))))))  0
              THENA  (RepUR  ``ses-fresh-sequence  pa-is-sign-implies  pa-is-new-and``  0  THEN  Auto)
              )
  THEN  Auto)

---

Home Index