---

Step * 1 1 of Lemma pi-rep-trans_wf

.....subterm..... T:t
1:n
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()
4. l : Id@i
5. serial : Name@i
6. 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
          <0, lg-add(make-lg([<l1, mk-tagged("create";g P l1 n1 avoid)>; <l1, mk-tagged("msg";pDVfire())>; <l, mk-tagged\000C("msg";pDVfire())>]);0;1)>
  else <s, make-lg([])>
  fi ) ∈ pi-process()
BY
{ (Using [`S',⌈ℕ4⌉] (BLemma `rec-process_wf_pi_simple_state`)⋅ THENA Try (Complete (Auto)))⋅ }

1
.....wf..... 
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()
4. l : Id@i
5. serial : Name@i
6. 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
               <0, lg-add(make-lg([<l1, mk-tagged("create";g P l1 n1 avoid)>; <l1, mk-tagged("msg";pDVfire())>; <l, mk-t\000Cagged("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))))

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  l$_{loc}$  :  Id
2.  P  :  pi\_term()
3.  g  :  \{Q:pi\_term()|  pi-rank(Q)  <  pi-rank(pirep(P))\}    {}\mrightarrow{}  Id  {}\mrightarrow{}  Name  {}\mrightarrow{}  (Name  List)  {}\mrightarrow{}  pi-process()
4.  l  :  Id@i
5.  serial  :  Name@i
6.  avoid  :  Name  List@i
\mvdash{}  RecProcess(0;s,m.if  (s  =\msubz{}  0)  \mwedge{}\msubb{}  pDVfire?(m)  then  ə,  make-lg([<l$_{loc}$,  mk-t\000Cagged("msg";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,  mk-tagged("msg";pDVfire())>]);0;1)
                    >
    else  <s,  make-lg([])>
    fi  )  \mmember{}  pi-process()


By

---

Latex:
(Using  [`S',\mkleeneopen{}\mBbbN{}4\mkleeneclose{}]  (BLemma  `rec-process\_wf\_pi\_simple\_state`)\mcdot{}  THENA  Try  (Complete  (Auto)))\mcdot{}

---

Home Index