---

Step * of Lemma pi-rep-trans_wf

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

1
1. l_loc : Id
2. P : pi_term()
3. g : {Q:pi_term()| pi-rank(Q) < pi-rank(pirep(P))}  ─→ 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
                          <0
                          , lg-add(make-lg([<l1, mk-tagged("create";g P l1 n1 avoid)>; <l1, mk-tagged("msg";pDVfire())>;\000C <l, mk-tagged("msg";pDVfire())>]);0;1)
                          >
                  else <s, make-lg([])>
                  fi ) ∈ Id ─→ Name ─→ (Name List) ─→ pi-process()

---

Latex:

---

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


By

---

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

---

Home Index