---

Step * 1 1 of Lemma pi-guarded-aux_wf


1. compList : (pi_prefix() × pi_term()) List
2. g : {Q:pi_term()| (∃C∈compList. pi-rank(Q) ≤ pi-rank(snd(C)))}  ─→ Id ─→ Name ─→ (Name List) ─→ pi-process()
3. l : Id
4. serial : Name
5. avoid : Name List
⊢ λpi-guarded-aux,l,serial,avoid,m. if pDVmsg?(m)
                                   then let val = pDVmsg-val(m) in
                                         let i = pDVmsg-index(m) in
                                         if i <z ||compList||
                                         then let pre_i,P_i = compList[i] 
                                              in let P' = if pircv?(pre_i)
                                                          then pi-simple-subst(val;pircv-var(pre_i);P_i)
                                                          else P_i
                                                          fi  in
                                                     <g P' l serial avoid ∪ pi-names(P')
                                                     , make-lg([<l, mk-tagged("msg";pDVfire())>])
                                                     >
                                         else <pi-guarded-aux l serial avoid, make-lg([])>
                                         fi 
                                   else <pi-guarded-aux l serial avoid, make-lg([])>
                                   fi  ∈ ∩T:{T:Type| Process(T.piM(T)) ⊆r T} 
           ((Id ─→ Name ─→ (Name List) ─→ T)
           ─→ Id
           ─→ Name
           ─→ (Name List)
           ─→ piM(T)
           ─→ (T × LabeledDAG(Id × (Com(T.piM(T)) T))))
BY
{ (MemTypeCD
   THEN D -1
   THEN RepeatFor 5 ((MemCD THENA Auto))
   THEN AutoSplit
   THEN RepeatFor 2 (GenConclLet [2] ⋅⋅)
   THEN AutoSplit
   THEN GenConclAtAddr [2;1]
   THEN D -2
   THEN Reduce 0
   THEN AutoSplit
   THEN ((GenConclLetType pi_term() [2]⋅ THENA Auto)
         THEN Auto
         THEN (MemTypeCD THEN Auto THEN With ⌈i⌉ (D 0)⋅ THEN Auto)⋅)⋅) }

1
1. compList : (pi_prefix() × pi_term()) List
2. g : {Q:pi_term()| (∃C∈compList. pi-rank(Q) ≤ pi-rank(snd(C)))}  ─→ Id ─→ Name ─→ (Name List) ─→ pi-process()
3. l : Id
4. serial : Name
5. avoid : Name List
6. T : Type
7. Process(T.piM(T)) ⊆r T
8. pi-guarded-aux : Id ─→ Name ─→ (Name List) ─→ T@i
9. l1 : Id@i
10. s1 : Name@i
11. a1 : Name List@i
12. m : piM(T)@i
13. ↑pDVmsg?(m)
14. val : Name@i
15. pDVmsg-val(m) = val ∈ Name@i
16. i : ℕ@i
17. pDVmsg-index(m) = i ∈ ℕ@i
18. i < ||compList||
19. v1 : pi_prefix()@i
20. v2 : pi_term()@i
21. compList[i] = <v1, v2> ∈ (pi_prefix() × pi_term())@i
22. ↑pircv?(v1)
23. P' : pi_term()@i
24. pi-simple-subst(val;pircv-var(v1);v2) = P' ∈ pi_term()@i
⊢ pi-rank(P') ≤ pi-rank(snd(compList[i]))

---

Latex:

---

Latex:

1.  compList  :  (pi\_prefix()  \mtimes{}  pi\_term())  List
2.  g  :  \{Q:pi\_term()|  (\mexists{}C\mmember{}compList.  pi-rank(Q)  \mleq{}  pi-rank(snd(C)))\} 
{}\mrightarrow{}  Id
{}\mrightarrow{}  Name
{}\mrightarrow{}  (Name  List)
{}\mrightarrow{}  pi-process()
3.  l  :  Id
4.  serial  :  Name
5.  avoid  :  Name  List
\mvdash{}  \mlambda{}pi-guarded-aux,l,serial,avoid,m.  if  pDVmsg?(m)
                                                                      then  let  val  =  pDVmsg-val(m)  in
                                                                                  let  i  =  pDVmsg-index(m)  in
                                                                                  if  i  <z  ||compList||
                                                                                  then  let  pre$_{i}$,P$_{i\mbackslash{}ff\000C7d$  =  compList[i] 
                                                                                            in  let  P'  =  if  pircv?(pre$_{i}$)
                                                                                                                    then  pi-simple-subst(val;...;P$_\mbackslash{}f\000Cf7bi}$)
                                                                                                                    else  P$_{i}$
                                                                                                                    fi    in
                                                                                                          <g  P'  l  serial  avoid  \mcup{}  pi-names(P')
                                                                                                          ,  make-lg([<l,  mk-tagged("msg";pDVfire())>])
                                                                                                          >
                                                                                  else  <pi-guarded-aux  l  serial  avoid,  make-lg([])>
                                                                                  fi 
                                                                      else  <pi-guarded-aux  l  serial  avoid,  make-lg([])>
                                                                      fi    \mmember{}  \mcap{}T:\{T:Type|  Process(T.piM(T))  \msubseteq{}r  T\} 
                      ((Id  {}\mrightarrow{}  Name  {}\mrightarrow{}  (Name  List)  {}\mrightarrow{}  T)
                      {}\mrightarrow{}  Id
                      {}\mrightarrow{}  Name
                      {}\mrightarrow{}  (Name  List)
                      {}\mrightarrow{}  piM(T)
                      {}\mrightarrow{}  (T  \mtimes{}  LabeledDAG(Id  \mtimes{}  (Com(T.piM(T))  T))))


By

---

Latex:
(MemTypeCD
  THEN  D  -1
  THEN  RepeatFor  5  ((MemCD  THENA  Auto))
  THEN  AutoSplit
  THEN  RepeatFor  2  (GenConclLet  [2]  \mcdot{}\mcdot{})
  THEN  AutoSplit
  THEN  GenConclAtAddr  [2;1]
  THEN  D  -2
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  ((GenConclLetType  pi\_term()  [2]\mcdot{}  THENA  Auto)
              THEN  Auto
              THEN  (MemTypeCD  THEN  Auto  THEN  With  \mkleeneopen{}i\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)\mcdot{})\mcdot{})

---

Home Index