---

Step * of Lemma new_23_sig_update_replica_wf

∀[Cmd:ValueAllType]. ∀[slots:set-sig{i:l}(ℤ)].
  (new_23_sig_update_replica(Cmd;slots) ∈ Id ─→ (ℤ × Cmd) ─→ set-sig-set(slots) ─→ set-sig-set(slots))
BY
{ ProveEmlWfLemma }

---

Latex:

---

Latex:
\mforall{}[Cmd:ValueAllType].  \mforall{}[slots:set-sig\{i:l\}(\mBbbZ{})].
    (new\_23\_sig\_update\_replica(Cmd;slots)  \mmember{}  Id
      {}\mrightarrow{}  (\mBbbZ{}  \mtimes{}  Cmd)
      {}\mrightarrow{}  set-sig-set(slots)
      {}\mrightarrow{}  set-sig-set(slots))


By

---

Latex:
ProveEmlWfLemma

---

Home Index