---

Step * of Lemma pv11_p1_upd_right

∀Cmd:ValueAllType. ∀proposals1,proposals2:(ℤ × Cmd) List. ∀s:ℤ. ∀c:Cmd.
  ((<s, c> ∈ proposals2) ⇒ (∃c':Cmd. (<s, c'> ∈ pv11_p1_update_proposals(Cmd) proposals1 proposals2)))
BY
{ ((Unfold `vatype` 0 THEN Auto)
   THEN (InstConcl [⌜c⌝]⋅ THEN Auto)
   THEN BLemma `pv11_p1_upd_desc_iff`
   THEN Auto
   THEN OrLeft
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}Cmd:ValueAllType.  \mforall{}proposals1,proposals2:(\mBbbZ{}  \mtimes{}  Cmd)  List.  \mforall{}s:\mBbbZ{}.  \mforall{}c:Cmd.
    ((<s,  c>  \mmember{}  proposals2)
    {}\mRightarrow{}  (\mexists{}c':Cmd.  (<s,  c'>  \mmember{}  pv11\_p1\_update\_proposals(Cmd)  proposals1  proposals2)))


By

---

Latex:
((Unfold  `vatype`  0  THEN  Auto)
  THEN  (InstConcl  [\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  BLemma  `pv11\_p1\_upd\_desc\_iff`
  THEN  Auto
  THEN  OrLeft
  THEN  Auto)

---

Home Index