---

Step * 1 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
⊢ Comm-process-q_aux(v) id loc : preList ⊕ st ∈ (Id × (pi_prefix() List)) List
  × st:Id fp-> pi_prefix() List
  × Id
  × ((ℕ × Id × ℕ × Name) List)
BY
{ (RepUR ``let`` 0 THEN Auto) }

---

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{}  Comm-process-q\_aux(v)  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:
(RepUR  ``let``  0  THEN  Auto)

---

Home Index