---

Step * 1 1 of Lemma pi-guarded-trans_wf


1. compList : (pi_prefix() × pi_term()) List
2. g : {Q:pi_term()| (∃C∈compList. pi-rank(Q) ≤ pi-rank(snd(C)))}  ─→ Id ─→ Name ─→ (Name List) ─→ pi-process()
3. l : Id
4. serial : Name
5. avoid : Name List
⊢ λpi-guarded-trans,l,serial,avoid,m. if pDVfire?(m)
                                     then <pi-guarded-aux(compList;g) l serial avoid
                                          , make-lg([<l, mk-tagged("msg";pDVfire())>])
                                          >
                                     else <pi-guarded-trans l serial avoid, make-lg([])>
                                     fi  ∈ ∩T:{T:Type| Process(T.piM(T)) ⊆r T} 
           ((Id ─→ Name ─→ (Name List) ─→ T)
           ─→ Id
           ─→ Name
           ─→ (Name List)
           ─→ piM(T)
           ─→ (T × LabeledDAG(Id × (Com(T.piM(T)) T))))
BY
{ Auto }

1
1. compList : (pi_prefix() × pi_term()) List
2. g : {Q:pi_term()| (∃C∈compList. pi-rank(Q) ≤ pi-rank(snd(C)))}  ─→ Id ─→ Name ─→ (Name List) ─→ pi-process()
3. l : Id
4. serial : Name
5. avoid : Name List
6. T : {T:Type| Process(T.piM(T)) ⊆r T} 
7. pi-guarded-trans : Id ─→ Name ─→ (Name List) ─→ T@i
8. l1 : Id@i
9. s1 : Name@i
10. a1 : Name List@i
11. m : piM(T)@i
12. pDVfire?(m) ∈ 𝔹
13. ↑pDVfire?(m)
⊢ pi-guarded-aux(compList;g) l1 s1 a1 ∈ T

---

Latex:

---

Latex:

1.  compList  :  (pi\_prefix()  \mtimes{}  pi\_term())  List
2.  g  :  \{Q:pi\_term()|  (\mexists{}C\mmember{}compList.  pi-rank(Q)  \mleq{}  pi-rank(snd(C)))\} 
{}\mrightarrow{}  Id
{}\mrightarrow{}  Name
{}\mrightarrow{}  (Name  List)
{}\mrightarrow{}  pi-process()
3.  l  :  Id
4.  serial  :  Name
5.  avoid  :  Name  List
\mvdash{}  \mlambda{}pi-guarded-trans,l,serial,avoid,m.  if  pDVfire?(m)
                                                                          then  <pi-guarded-aux(compList;g)  l  serial  avoid
                                                                                    ,  make-lg([<l,  mk-tagged("msg";pDVfire())>])
                                                                                    >
                                                                          else  <pi-guarded-trans  l  serial  avoid,  make-lg([])>
                                                                          fi    \mmember{}  \mcap{}T:\{T:Type|  Process(T.piM(T))  \msubseteq{}r  T\} 
                      ((Id  {}\mrightarrow{}  Name  {}\mrightarrow{}  (Name  List)  {}\mrightarrow{}  T)
                      {}\mrightarrow{}  Id
                      {}\mrightarrow{}  Name
                      {}\mrightarrow{}  (Name  List)
                      {}\mrightarrow{}  piM(T)
                      {}\mrightarrow{}  (T  \mtimes{}  LabeledDAG(Id  \mtimes{}  (Com(T.piM(T))  T))))


By

---

Latex:
Auto

---

Home Index