---

Step * 1 of Lemma pi-new-trans_wf


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))))
BY
{ (RepUR ``let`` 0 THEN 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
7. T : {T:Type| pi-process() ⊆r T} 
8. pi-new-trans : Id ─→ Name ─→ (Name List) ─→ T@i
9. l1 : Id@i
10. s1 : Name@i
11. a1 : Name List@i
12. m : piM(T)@i
13. pDVfire?(m) ∈ 𝔹
14. ↑pDVfire?(m)
⊢ pi-simple-subst(maybe-new-local(s1;x;a1);x;P) ∈ {Q:pi_term()| pi-rank(Q) < pi-rank(pinew(x;P))} 

2
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
7. T : {T:Type| pi-process() ⊆r T} 
8. pi-new-trans : Id ─→ Name ─→ (Name List) ─→ T@i
9. l1 : Id@i
10. s1 : Name@i
11. a1 : Name List@i
12. m : piM(T)@i
13. pDVfire?(m) ∈ 𝔹
14. ↑pDVfire?(m)
⊢ Process(T.piM(T)) ⊆r T

---

Latex:

---

Latex:

1.  x  :  Name
2.  P  :  pi\_term()
3.  g  :  \{Q:pi\_term()|  pi-rank(Q)  <  pi-rank(pinew(x;P))\}    {}\mrightarrow{}  Id  {}\mrightarrow{}  Name  {}\mrightarrow{}  (Name  List)  {}\mrightarrow{}  pi-process()
4.  l  :  Id
5.  serial  :  Name
6.  avoid  :  Name  List
\mvdash{}  \mlambda{}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  \mcup{}  pi-names(P)
                                                                              ,  make-lg([<l,  mk-tagged("msg";pDVfire())>])
                                                                              >
                                                                  else  <pi-new-trans  l  serial  avoid,  make-lg([])>
                                                                  fi    \mmember{}  \mcap{}T:\{T:Type|  pi-process()  \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:
(RepUR  ``let``  0  THEN  Auto)

---

Home Index