---

Step * 1 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
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
BY
{ (DVar `T' THEN DoSubsume THEN Auto THEN Unfold `pi-process` 0 THEN Auto)⋅ }

---

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
6.  T  :  \{T:Type|  Process(T.piM(T))  \msubseteq{}r  T\} 
7.  pi-guarded-trans  :  Id  {}\mrightarrow{}  Name  {}\mrightarrow{}  (Name  List)  {}\mrightarrow{}  T@i
8.  l1  :  Id@i
9.  s1  :  Name@i
10.  a1  :  Name  List@i
11.  m  :  piM(T)@i
12.  pDVfire?(m)  \mmember{}  \mBbbB{}
13.  \muparrow{}pDVfire?(m)
\mvdash{}  pi-guarded-aux(compList;g)  l1  s1  a1  \mmember{}  T


By

---

Latex:
(DVar  `T'  THEN  DoSubsume  THEN  Auto  THEN  Unfold  `pi-process`  0  THEN  Auto)\mcdot{}

---

Home Index