---

Step * of Lemma Comm-process-q_aux_wf

∀[q:(Id × (pi_prefix() List)) List]
  (Comm-process-q_aux(q) ∈ Id
   ─→ st:Id fp-> pi_prefix() List
   ─→ ((Id × (pi_prefix() List)) List × st:Id fp-> pi_prefix() List × Id × ((ℕ × Id × ℕ × Name) List)))
BY
{ InductionOnList
THEN Unfold `Comm-process-q_aux` 0
THEN Reduce 0
THEN Auto⋅ }

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
⊢ 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)

---

Latex:

---

Latex:
\mforall{}[q:(Id  \mtimes{}  (pi\_prefix()  List))  List]
    (Comm-process-q\_aux(q)  \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)))


By

---

Latex:
InductionOnList
THEN  Unfold  `Comm-process-q\_aux`  0
THEN  Reduce  0
THEN  Auto\mcdot{}

---

Home Index