---

Step * 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(compList;g) l serial avoid ∈ pi-process()
BY
{ (Unfold `pi-guarded-trans` 0⋅
   THEN RepUR ``pi-process Process process`` 0
   THEN Using [`A', ⌈λ2T.Id⌉; `B', ⌈λ2T.Name⌉; `C',⌈λ2T.Name List⌉] (BLemma `fix_wf_corec_3parameter`)⋅
   THEN (Try (Complete (Auto)) THEN Isect2CD THEN ((Fold `process` 0 THEN Fold `Process` 0) ORELSE 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
⊢ λ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))))

---

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{}  pi-guarded-trans(compList;g)  l  serial  avoid  \mmember{}  pi-process()


By

---

Latex:
(Unfold  `pi-guarded-trans`  0\mcdot{}
  THEN  RepUR  ``pi-process  Process  process``  0
  THEN  Using  [`A',  \mkleeneopen{}\mlambda{}\msubtwo{}T.Id\mkleeneclose{};  `B',  \mkleeneopen{}\mlambda{}\msubtwo{}T.Name\mkleeneclose{};  `C',\mkleeneopen{}\mlambda{}\msubtwo{}T.Name  List\mkleeneclose{}]  (BLemma  `fix\_wf\_corec\_3parameter`)
  \mcdot{}
  THEN  (Try  (Complete  (Auto))
              THEN  Isect2CD
              THEN  ((Fold  `process`  0  THEN  Fold  `Process`  0)  ORELSE  Auto)))

---

Home Index