---

Step * 1 of Lemma pi-guarded-aux_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
⊢ pi-guarded-aux(compList;g) l ∈ Name ─→ (Name List) ─→ pi-process()
BY
{ (Auto
   THEN (ExtWith [`serial'] [⌈Top ─→ Top⌉]⋅ THENA Auto THEN RecUnfold `pi-guarded-aux` 0 THEN Reduce 0 THEN Auto)⋅
   THEN (ExtWith [`avoid'] [⌈Top ─→ Top⌉]⋅ THENA Auto THEN RecUnfold `pi-guarded-aux` 0 THEN Reduce 0 THEN Auto)⋅
   THEN (Unfold `pi-guarded-aux` 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-aux,l,serial,avoid,m. if pDVmsg?(m)
                                   then let val = pDVmsg-val(m) in
                                         let i = pDVmsg-index(m) in
                                         if i <z ||compList||
                                         then let pre_i,P_i = compList[i] 
                                              in let P' = if pircv?(pre_i)
                                                          then pi-simple-subst(val;pircv-var(pre_i);P_i)
                                                          else P_i
                                                          fi  in
                                                     <g P' l serial avoid ∪ pi-names(P')
                                                     , make-lg([<l, mk-tagged("msg";pDVfire())>])
                                                     >
                                         else <pi-guarded-aux l serial avoid, make-lg([])>
                                         fi 
                                   else <pi-guarded-aux 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
\mvdash{}  pi-guarded-aux(compList;g)  l  \mmember{}  Name  {}\mrightarrow{}  (Name  List)  {}\mrightarrow{}  pi-process()


By

---

Latex:
(Auto
  THEN  (ExtWith  [`serial']  [\mkleeneopen{}Top  {}\mrightarrow{}  Top\mkleeneclose{}]\mcdot{}
  THENA  Auto
              THEN  RecUnfold  `pi-guarded-aux`  0
              THEN  Reduce  0
              THEN  Auto
  )\mcdot{}
  THEN  (ExtWith  [`avoid']  [\mkleeneopen{}Top  {}\mrightarrow{}  Top\mkleeneclose{}]\mcdot{}
  THENA  Auto
              THEN  RecUnfold  `pi-guarded-aux`  0
              THEN  Reduce  0
              THEN  Auto
  )\mcdot{}
  THEN  (Unfold  `pi-guarded-aux`  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)))\mcdot{})\mcdot{}

---

Home Index