---

Step * of Lemma pv11_p1_add_if_new_iff

∀Cmd:ValueAllType. ∀p,x:ℤ × Cmd. ∀proposals:(ℤ × Cmd) List.
  ((p ∈ pv11_p1_add_if_new() pv11_p1_same_proposal(Cmd) x proposals)
  ⇐⇒ (p ∈ proposals) ∨ if (∃z∈proposals.pv11_p1_same_proposal(Cmd) x z)_b then False else p = x ∈ (ℤ × Cmd) fi )
BY
{ (Unfold `vatype` 0
   THEN (UnivCD THENA Auto)
   THEN D 0
   THEN (UnivCD THENA Auto)
   THEN ((Repeat (GenListD (-1)) THEN Auto)
         THEN Repeat (GenListD 0)
         THEN (SplitOrHyps THEN Auto THEN (SplitOnHypITE (-2)⋅ THEN Auto)⋅)⋅)⋅) }

---

Latex:

---

Latex:
\mforall{}Cmd:ValueAllType.  \mforall{}p,x:\mBbbZ{}  \mtimes{}  Cmd.  \mforall{}proposals:(\mBbbZ{}  \mtimes{}  Cmd)  List.
    ((p  \mmember{}  pv11\_p1\_add\_if\_new()  pv11\_p1\_same\_proposal(Cmd)  x  proposals)
    \mLeftarrow{}{}\mRightarrow{}  (p  \mmember{}  proposals)
            \mvee{}  if  (\mexists{}z\mmember{}proposals.pv11\_p1\_same\_proposal(Cmd)  x  z)\_b  then  False  else  p  =  x  fi  )


By

---

Latex:
(Unfold  `vatype`  0
  THEN  (UnivCD  THENA  Auto)
  THEN  D  0
  THEN  (UnivCD  THENA  Auto)
  THEN  ((Repeat  (GenListD  (-1))  THEN  Auto)
              THEN  Repeat  (GenListD  0)
              THEN  (SplitOrHyps  THEN  Auto  THEN  (SplitOnHypITE  (-2)\mcdot{}  THEN  Auto)\mcdot{})\mcdot{})\mcdot{})

---

Home Index