---

Step * of Lemma ses-flow_wf

∀[s:SES]. ∀[es:EO+(Info)]. ∀[e1,e2:E]. ∀[a:Atom1].  (ses-flow(s;es;a;e1;e2) ∈ ℙ)
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN Assert
        ⌜∀n:ℕ. ∀e1,e2:E.  (((es-rank(es;e2) - es-rank(es;e1)) ≤ n) ⇒ (∀a:Atom1. (ses-flow(s;es;a;e1;e2) ∈ Type)))⌝⋅
   )⋅ }

1
.....assertion..... 
1. s : SES
2. es : EO+(Info)
⊢ ∀n:ℕ. ∀e1,e2:E.  (((es-rank(es;e2) - es-rank(es;e1)) ≤ n) ⇒ (∀a:Atom1. (ses-flow(s;es;a;e1;e2) ∈ Type)))

2
1. s : SES
2. es : EO+(Info)
3. ∀n:ℕ. ∀e1,e2:E.  (((es-rank(es;e2) - es-rank(es;e1)) ≤ n) ⇒ (∀a:Atom1. (ses-flow(s;es;a;e1;e2) ∈ Type)))
⊢ ∀[e1,e2:E]. ∀[a:Atom1].  (ses-flow(s;es;a;e1;e2) ∈ ℙ)

---

Latex:

---

Latex:
\mforall{}[s:SES].  \mforall{}[es:EO+(Info)].  \mforall{}[e1,e2:E].  \mforall{}[a:Atom1].    (ses-flow(s;es;a;e1;e2)  \mmember{}  \mBbbP{})


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  Assert
            \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}e1,e2:E.
                  (((es-rank(es;e2)  -  es-rank(es;e1))  \mleq{}  n)  {}\mRightarrow{}  (\mforall{}a:Atom1.  (ses-flow(s;es;a;e1;e2)  \mmember{}  Type)))\mkleeneclose{}\mcdot{}
  )\mcdot{}

---

Home Index