---

Step * of Lemma pi-new-trans_wf

∀[x:Name]. ∀[P:pi_term()]. ∀[g:{Q:pi_term()| pi-rank(Q) < pi-rank(pinew(x;P))} 
                               ⟶ Id
                               ⟶ Name
                               ⟶ (Name List)
                               ⟶ pi-process()].
  (pi-new-trans(x;P;g) ∈ Id ⟶ Name ⟶ (Name List) ⟶ pi-process())
BY
{ (Auto
   THEN (ExtWith [`l'] [⌜Top ⟶ Top⌝]⋅ THENA Auto THEN RecUnfold `pi-new-trans` 0 THEN Auto)
   THEN Auto
   THEN (ExtWith [`serial'] [⌜Top ⟶ Top⌝]⋅ THENA Auto THEN RecUnfold `pi-new-trans` 0 THEN Reduce 0 THEN Auto)⋅
   THEN (ExtWith [`avoid'] [⌜Top ⟶ Top⌝]⋅ THENA Auto THEN RecUnfold `pi-new-trans` 0 THEN Reduce 0 THEN Auto)⋅
   THEN Unfold `pi-new-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 THEN Fold `pi-process` 0) ORELSE Auto))) }

1
1. x : Name
2. P : pi_term()
3. g : {Q:pi_term()| pi-rank(Q) < pi-rank(pinew(x;P))}  ⟶ Id ⟶ Name ⟶ (Name List) ⟶ pi-process()
4. l : Id
5. serial : Name
6. avoid : Name List
⊢ λpi-new-trans,l,serial,avoid,m. if pDVfire?(m)
                                 then let n = maybe-new-local(serial;x;avoid) in
                                       let P' = pi-simple-subst(n;x;P) in
                                       <g P' l serial avoid ⋃ pi-names(P), make-lg([<l, mk-tagged("msg";pDVfire())>])>
                                 else <pi-new-trans l serial avoid, make-lg([])>
                                 fi  ∈ ⋂T:{T:Type| pi-process() ⊆r T} 
           ((Id ⟶ Name ⟶ (Name List) ⟶ T)
           ⟶ Id
           ⟶ Name
           ⟶ (Name List)
           ⟶ piM(T)
           ⟶ (T × LabeledDAG(Id × (Com(T.piM(T)) T))))

---

Latex:

---

Latex:
\mforall{}[x:Name].  \mforall{}[P:pi\_term()].  \mforall{}[g:\{Q:pi\_term()|  pi-rank(Q)  <  pi-rank(pinew(x;P))\} 
                                                              {}\mrightarrow{}  Id
                                                              {}\mrightarrow{}  Name
                                                              {}\mrightarrow{}  (Name  List)
                                                              {}\mrightarrow{}  pi-process()].
    (pi-new-trans(x;P;g)  \mmember{}  Id  {}\mrightarrow{}  Name  {}\mrightarrow{}  (Name  List)  {}\mrightarrow{}  pi-process())


By

---

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

---

Home Index