---

Step * of Lemma noncelike-signatures_wf

∀[s:SES]. ∀[es:EO+(Info)]. ∀[thr:Thread].  (noncelike-signatures(s;es;thr) ∈ ℙ)
BY
{ ProveWfLemma }

1
1. s : SES
2. es : EO+(Info)
3. thr : Thread
4. e1 : E(Sign)@i
5. e2 : E(Sign)@i
6. signature(e1) = signature(e2) ∈ Atom1
⊢ e1 ∈ Act

---

Latex:

---

Latex:
\mforall{}[s:SES].  \mforall{}[es:EO+(Info)].  \mforall{}[thr:Thread].    (noncelike-signatures(s;es;thr)  \mmember{}  \mBbbP{})


By

---

Latex:
ProveWfLemma

---

Home Index