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