---

Step * of Lemma pv11_p1_add_if_new_if

∀Cmd:ValueAllType. ∀p:ℤ × Cmd. ∀proposals:(ℤ × Cmd) List.
  ((¬↑(pv11_p1_in_domain(Cmd) (fst(p)) proposals)) ⇒ (p ∈ pv11_p1_add_if_new() pv11_p1_same_proposal(Cmd) p proposals))
BY
{ (Unfold `vatype` 0
   THEN (UnivCD THENA Auto)
   THEN (RWO "pv11_p1_add_if_new_iff" 0 THENA Auto)
   THEN OrRight
   THEN Auto
   THEN AutoSplit
   THEN D (-2)
   THEN (RWO "l_exists_iff" (-1) THENA Auto)
   THEN ExRepD
   THEN DVar `p'⋅
   THEN DVar `z'
   THEN RepUR ``pv11_p1_in_domain`` 0
   THEN RepUR ``pv11_p1_same_proposal`` (-1)
   THEN Repeat (AllPushDown⋅)
   THEN GenListD 0
   THEN Auto
   THEN InstConcl [⌜<z1, z2>⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}Cmd:ValueAllType.  \mforall{}p:\mBbbZ{}  \mtimes{}  Cmd.  \mforall{}proposals:(\mBbbZ{}  \mtimes{}  Cmd)  List.
    ((\mneg{}\muparrow{}(pv11\_p1\_in\_domain(Cmd)  (fst(p))  proposals))
    {}\mRightarrow{}  (p  \mmember{}  pv11\_p1\_add\_if\_new()  pv11\_p1\_same\_proposal(Cmd)  p  proposals))


By

---

Latex:
(Unfold  `vatype`  0
  THEN  (UnivCD  THENA  Auto)
  THEN  (RWO  "pv11\_p1\_add\_if\_new\_iff"  0  THENA  Auto)
  THEN  OrRight
  THEN  Auto
  THEN  AutoSplit
  THEN  D  (-2)
  THEN  (RWO  "l\_exists\_iff"  (-1)  THENA  Auto)
  THEN  ExRepD
  THEN  DVar  `p'\mcdot{}
  THEN  DVar  `z'
  THEN  RepUR  ``pv11\_p1\_in\_domain``  0
  THEN  RepUR  ``pv11\_p1\_same\_proposal``  (-1)
  THEN  Repeat  (AllPushDown\mcdot{})
  THEN  GenListD  0
  THEN  Auto
  THEN  InstConcl  [\mkleeneopen{}<z1,  z2>\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index