---

Step * 1 1 1 of Lemma pi-bar-trans_wf

.....wf..... 
1. l_loc : Id
2. P : pi_term()
3. Q : pi_term()
4. g : {R:pi_term()| pi-rank(R) < pi-rank(pipar(P;Q))}  ⟶ Id ⟶ Name ⟶ (Name List) ⟶ pi-process()
5. l : Id@i
6. serial : Name@i
7. avoid : Name List@i
⊢ λs,m. if (s =z 0) ∧b pDVfire?(m) then <1, make-lg([<l_loc, mk-tagged("msg";pDVloc(l))>])>
       if (s =z 1) ∧b pDVloc_tag?(m)
         then let l1 = pDVloc_tag-id(m) in
               let n1 = pDVloc_tag-name(m) in
               <2, lg-add(make-lg([<l1, mk-tagged("create";g P l1 n1 avoid)>; <l1, mk-tagged("msg";pDVfire())>; <l_loc, \000Cmk-tagged("msg";pDVloc(l))>]);0;1)>
       if (s =z 2) ∧b pDVloc_tag?(m)
         then let l2 = pDVloc_tag-id(m) in
               let n2 = pDVloc_tag-name(m) in
               <3, lg-add(make-lg([<l2, mk-tagged("create";g Q l2 n2 avoid)>; <l2, mk-tagged("msg";pDVfire())>]);0;1)>
       else <s, make-lg([])>
       fi  ∈ ⋂T:{T:Type| pi-process() ⊆r T} . (ℕ4 ⟶ piM(T) ⟶ (ℕ4 × LabeledDAG(Id × (Com(T.piM(T)) T))))
BY
{ ((MemTypeCD THENA Auto)
   THEN D -1
   THEN RepeatFor 2 ((MemCD THENA Auto))
   THEN IntSegCases (-2)
   THEN Reduce 0
   THEN Try (AutoSplit)
   THEN RepUR ``let`` 0
   THEN Auto
   THEN Try ((Fold `pi-process` 0 THEN Auto))
   THEN (RepUR ``lg-size make-lg pMsg piM`` 0 THEN Auto THEN Auto)⋅) }

1
1. l_loc : Id
2. P : pi_term()
3. Q : pi_term()
4. g : {R:pi_term()| pi-rank(R) < pi-rank(pipar(P;Q))}  ⟶ Id ⟶ Name ⟶ (Name List) ⟶ pi-process()
5. l : Id@i
6. serial : Name@i
7. avoid : Name List@i
8. T : Type
9. pi-process() ⊆r T
10. s : ℤ
11. m : piM(T)@i
12. s = 1 ∈ ℤ
13. ↑pDVloc_tag?(m)
⊢ P ∈ {R:pi_term()| pi-rank(R) < pi-rank(pipar(P;Q))} 

2
1. l_loc : Id
2. P : pi_term()
3. Q : pi_term()
4. g : {R:pi_term()| pi-rank(R) < pi-rank(pipar(P;Q))}  ⟶ Id ⟶ Name ⟶ (Name List) ⟶ pi-process()
5. l : Id@i
6. serial : Name@i
7. avoid : Name List@i
8. T : Type
9. pi-process() ⊆r T
10. s : ℤ
11. m : piM(T)@i
12. s = 2 ∈ ℤ
13. ↑pDVloc_tag?(m)
⊢ Q ∈ {R:pi_term()| pi-rank(R) < pi-rank(pipar(P;Q))} 

---

Latex:

---

Latex:
.....wf..... 
1.  l$_{loc}$  :  Id
2.  P  :  pi\_term()
3.  Q  :  pi\_term()
4.  g  :  \{R:pi\_term()|  pi-rank(R)  <  pi-rank(pipar(P;Q))\}    {}\mrightarrow{}  Id  {}\mrightarrow{}  Name  {}\mrightarrow{}  (Name  List)  {}\mrightarrow{}  pi-process()
5.  l  :  Id@i
6.  serial  :  Name@i
7.  avoid  :  Name  List@i
\mvdash{}  \mlambda{}s,m.  if  (s  =\msubz{}  0)  \mwedge{}\msubb{}  pDVfire?(m)  then  ə,  make-lg([<l$_{loc}$,  mk-tagged("msg"\000C;pDVloc(l))>])>
              if  (s  =\msubz{}  1)  \mwedge{}\msubb{}  pDVloc\_tag?(m)
                  then  let  l1  =  pDVloc\_tag-id(m)  in
                              let  n1  =  pDVloc\_tag-name(m)  in
                              ɚ
                              ,  lg-add(make-lg([<l1,  mk-tagged("create";g  P  l1  n1  avoid)>
                                                                  <l1,  mk-tagged("msg";pDVfire())>
                                                                  <l$_{loc}$,  mk-tagged("msg";pDVloc(l))>]);0;1)
                              >
              if  (s  =\msubz{}  2)  \mwedge{}\msubb{}  pDVloc\_tag?(m)
                  then  let  l2  =  pDVloc\_tag-id(m)  in
                              let  n2  =  pDVloc\_tag-name(m)  in
                              ɛ
                              ,  lg-add(make-lg([<l2,  mk-tagged("create";g  Q  l2  n2  avoid)>
                                                                  <l2,  mk-tagged("msg";pDVfire())>]);0;1)
                              >
              else  <s,  make-lg([])>
              fi    \mmember{}  \mcap{}T:\{T:Type|  pi-process()  \msubseteq{}r  T\}  .  (\mBbbN{}4  {}\mrightarrow{}  piM(T)  {}\mrightarrow{}  (\mBbbN{}4  \mtimes{}  LabeledDAG(Id  \mtimes{}  (Com(T.piM(T))  \000CT))))


By

---

Latex:
((MemTypeCD  THENA  Auto)
  THEN  D  -1
  THEN  RepeatFor  2  ((MemCD  THENA  Auto))
  THEN  IntSegCases  (-2)
  THEN  Reduce  0
  THEN  Try  (AutoSplit)
  THEN  RepUR  ``let``  0
  THEN  Auto
  THEN  Try  ((Fold  `pi-process`  0  THEN  Auto))
  THEN  (RepUR  ``lg-size  make-lg  pMsg  piM``  0  THEN  Auto  THEN  Auto)\mcdot{})

---

Home Index