---

Step * 1 of Lemma pi-bar-trans_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()
⊢ λl,serial,avoid. RecProcess(0;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())>;\000C <l_loc, mk-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())>]\000C);0;1)
                          >
                  else <s, make-lg([])>
                  fi ) ∈ Id ─→ Name ─→ (Name List) ─→ pi-process()
BY
{ RepeatFor 3 ((MemCD⋅ THENA Auto)) }

1
.....subterm..... T:t
1:n
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
⊢ RecProcess(0;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, mk-ta\000Cgged("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 ) ∈ pi-process()

---

Latex:

---

Latex:

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()
\mvdash{}  \mlambda{}l,serial,avoid.  RecProcess(0;s,m.if  (s  =\msubz{}  0)  \mwedge{}\msubb{}  pDVfire?(m)
                                                                            then  ə,  make-lg([<l$_{loc}$,  mk-tagged("m\000Csg";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\000C))>]);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{}  Id  {}\mrightarrow{}  Name  {}\mrightarrow{}  (Name  List)  {}\mrightarrow{}  pi-process()


By

---

Latex:
RepeatFor  3  ((MemCD\mcdot{}  THENA  Auto))

---

Home Index