---

Step * 1 of Lemma Comm-process-q_aux_wf


1. u : Id × (pi_prefix() List)
2. v : (Id × (pi_prefix() List)) List
3. Comm-process-q_aux(v) ∈ Id
   ─→ st:Id fp-> pi_prefix() List
   ─→ ((Id × (pi_prefix() List)) List × st:Id fp-> pi_prefix() List × Id × ((ℕ × Id × ℕ × Name) List))
4. id : Id@i
5. st : st:Id fp-> pi_prefix() List@i
6. loc : Id@i
7. preList : pi_prefix() List@i
⊢ rec-case(v) of
  [] => λid,st. <[], st, id, []>
  h::t =>
   r.λid,st. let loc = fst(h) in
              let preList = snd(h) in
              let mList = get-triples(preList;st) in
              if null(mList) then r id loc : preList ⊕ st else <t, st, loc, mList> fi  
  id 
  loc : preList ⊕ st ∈ (Id × (pi_prefix() List)) List × st:Id fp-> pi_prefix() List × Id × ((ℕ × Id × ℕ × Name) List)
BY
{ Fold `Comm-process-q_aux` 0 }

1
1. u : Id × (pi_prefix() List)
2. v : (Id × (pi_prefix() List)) List
3. Comm-process-q_aux(v) ∈ Id
   ─→ st:Id fp-> pi_prefix() List
   ─→ ((Id × (pi_prefix() List)) List × st:Id fp-> pi_prefix() List × Id × ((ℕ × Id × ℕ × Name) List))
4. id : Id@i
5. st : st:Id fp-> pi_prefix() List@i
6. loc : Id@i
7. preList : pi_prefix() List@i
⊢ Comm-process-q_aux(v) id loc : preList ⊕ st ∈ (Id × (pi_prefix() List)) List
  × st:Id fp-> pi_prefix() List
  × Id
  × ((ℕ × Id × ℕ × Name) List)

---

Latex:

---

Latex:

1.  u  :  Id  \mtimes{}  (pi\_prefix()  List)
2.  v  :  (Id  \mtimes{}  (pi\_prefix()  List))  List
3.  Comm-process-q\_aux(v)  \mmember{}  Id
      {}\mrightarrow{}  st:Id  fp->  pi\_prefix()  List
      {}\mrightarrow{}  ((Id  \mtimes{}  (pi\_prefix()  List))  List
            \mtimes{}  st:Id  fp->  pi\_prefix()  List
            \mtimes{}  Id
            \mtimes{}  ((\mBbbN{}  \mtimes{}  Id  \mtimes{}  \mBbbN{}  \mtimes{}  Name)  List))
4.  id  :  Id@i
5.  st  :  st:Id  fp->  pi\_prefix()  List@i
6.  loc  :  Id@i
7.  preList  :  pi\_prefix()  List@i
\mvdash{}  rec-case(v)  of
    []  =>  \mlambda{}id,st.  <[],  st,  id,  []>
    h::t  =>
      r.\mlambda{}id,st.  let  loc  =  fst(h)  in
                            let  preList  =  snd(h)  in
                            let  mList  =  get-triples(preList;st)  in
                            if  null(mList)  then  r  id  loc  :  preList  \moplus{}  st  else  <t,  st,  loc,  mList>  fi   
    id 
    loc  :  preList  \moplus{}  st  \mmember{}  (Id  \mtimes{}  (pi\_prefix()  List))  List
    \mtimes{}  st:Id  fp->  pi\_prefix()  List
    \mtimes{}  Id
    \mtimes{}  ((\mBbbN{}  \mtimes{}  Id  \mtimes{}  \mBbbN{}  \mtimes{}  Name)  List)


By

---

Latex:
Fold  `Comm-process-q\_aux`  0

---

Home Index