---

Step * of Lemma pi-bar-trans_wf

∀[l_loc:Id]. ∀[P,Q:pi_term()]. ∀[g:{R:pi_term()| pi-rank(R) < pi-rank(pipar(P;Q))} 
                                   ─→ Id
                                   ─→ Name
                                   ─→ (Name List)
                                   ─→ pi-process()].
  (pi-bar-trans(l_loc;P;Q;g) ∈ Id ─→ Name ─→ (Name List) ─→ pi-process())
BY
{ (UnivCD THENA Auto)
THEN Unfold `pi-bar-trans` 0 }

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()
⊢ λ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()

---

Latex:

---

Latex:
\mforall{}[l$_{loc}$:Id].  \mforall{}[P,Q:pi\_term()].  \mforall{}[g:\{R:pi\_term()|  pi-rank(R)  <  pi-rank(pipar(\000CP;Q))\} 
                                                                    {}\mrightarrow{}  Id
                                                                    {}\mrightarrow{}  Name
                                                                    {}\mrightarrow{}  (Name  List)
                                                                    {}\mrightarrow{}  pi-process()].
    (pi-bar-trans(l$_{loc}$;P;Q;g)  \mmember{}  Id  {}\mrightarrow{}  Name  {}\mrightarrow{}  (Name  List)  {}\mrightarrow{}  pi-process())


By

---

Latex:
(UnivCD  THENA  Auto)
THEN  Unfold  `pi-bar-trans`  0

---

Home Index