---

Step * of Lemma pv11_p1_upd_left

∀Cmd:ValueAllType. ∀proposals1,proposals2:(ℤ × Cmd) List. ∀s:ℤ. ∀c:Cmd.
  ((<s, c> ∈ proposals1) ⇒ (∃c':Cmd. (<s, c'> ∈ pv11_p1_update_proposals(Cmd) proposals1 proposals2)))
BY
{ (Unfold `vatype` 0
   THEN Auto
   THEN (Decide ↑(∃z∈proposals2.(s =z fst(z)))_b THENA Auto)
   THEN Repeat (AllPushDown)
   THEN All (\i.RWO "l_exists_iff" i THENA Auto)
   THEN ExRepD
   THEN Try (AllPushDown)) }

1
1. Cmd : {T:Type| valueall-type(T)} @i'
2. proposals1 : (ℤ × Cmd) List@i
3. proposals2 : (ℤ × Cmd) List@i
4. s : ℤ@i
5. c : Cmd@i
6. (<s, c> ∈ proposals1)@i
7. z : ℤ × Cmd
8. (z ∈ proposals2)
9. s = (fst(z)) ∈ ℤ
⊢ ∃c':Cmd. (<s, c'> ∈ pv11_p1_update_proposals(Cmd) proposals1 proposals2)

2
1. Cmd : {T:Type| valueall-type(T)} @i'
2. proposals1 : (ℤ × Cmd) List@i
3. proposals2 : (ℤ × Cmd) List@i
4. s : ℤ@i
5. c : Cmd@i
6. (<s, c> ∈ proposals1)@i
7. ¬(∃z:ℤ × Cmd. ((z ∈ proposals2) ∧ (s = (fst(z)) ∈ ℤ)))
⊢ ∃c':Cmd. (<s, c'> ∈ pv11_p1_update_proposals(Cmd) proposals1 proposals2)

---

Latex:

---

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


By

---

Latex:
(Unfold  `vatype`  0
  THEN  Auto
  THEN  (Decide  \muparrow{}(\mexists{}z\mmember{}proposals2.(s  =\msubz{}  fst(z)))\_b  THENA  Auto)
  THEN  Repeat  (AllPushDown)
  THEN  All  (\mbackslash{}i.RWO  "l\_exists\_iff"  i  THENA  Auto)
  THEN  ExRepD
  THEN  Try  (AllPushDown))

---

Home Index