---

Step * 1 of Lemma noncelike-signatures_wf


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
BY
{ (MemTypeCD THEN Auto) }

1
.....set predicate..... 
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
⊢ Action(e1)

---

Latex:

---

Latex:

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)
\mvdash{}  e1  \mmember{}  Act


By

---

Latex:
(MemTypeCD  THEN  Auto)

---

Home Index