---

Step * of Lemma pv11_p1_leq_bnum_or

∀ldrs_uid:Id ⟶ ℤ. ∀b1,b2:pv11_p1_Ballot_Num().
  ((↑(pv11_p1_leq_bnum(ldrs_uid) b1 b2)) ∨ (↑(pv11_p1_leq_bnum(ldrs_uid) b2 b1)))
BY
{ (Auto
   THEN All (RepUR ``pv11_p1_leq_bnum pv11_p1_Ballot_Num``)
   THEN DVar `b1'⋅
   THEN DVar `b2'⋅
   THEN Reduce 0
   THEN Try (Complete ((OrLeft THEN Auto)))
   THEN Try (Complete ((OrRight THEN Auto)))
   THEN DVar `x'
   THEN DVar `x1'
   THEN RepUR ``pv11_p1_leq_bnum'`` 0
   THEN (BoolCase ⌜x2 <z x4⌝⋅ THENA Auto)
   THEN Try (Complete ((OrLeft THEN Auto)))
   THEN (BoolCase ⌜(x2 =z x4)⌝⋅ THENA Auto)
   THEN Try (Complete (((OrRight THENA Auto) THEN AllPushDown THEN OrLeft THEN Auto)))
   THEN (BoolCase ⌜ldrs_uid x3 ≤z ldrs_uid x5⌝⋅ THENA Auto)
   THEN Try (Complete ((OrLeft THEN Auto)))
   THEN (OrRight THENA Auto)
   THEN AllPushDown
   THEN OrRight
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}ldrs$_{uid}$:Id  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}b1,b2:pv11\_p1\_Ballot\_Num().
    ((\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  b1  b2))  \mvee{}  (\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$\mbackslash{}ff5\000Cf{uid}$)  b2  b1)))


By

---

Latex:
(Auto
  THEN  All  (RepUR  ``pv11\_p1\_leq\_bnum  pv11\_p1\_Ballot\_Num``)
  THEN  DVar  `b1'\mcdot{}
  THEN  DVar  `b2'\mcdot{}
  THEN  Reduce  0
  THEN  Try  (Complete  ((OrLeft  THEN  Auto)))
  THEN  Try  (Complete  ((OrRight  THEN  Auto)))
  THEN  DVar  `x'
  THEN  DVar  `x1'
  THEN  RepUR  ``pv11\_p1\_leq\_bnum'``  0
  THEN  (BoolCase  \mkleeneopen{}x2  <z  x4\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  (Complete  ((OrLeft  THEN  Auto)))
  THEN  (BoolCase  \mkleeneopen{}(x2  =\msubz{}  x4)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  (Complete  (((OrRight  THENA  Auto)  THEN  AllPushDown  THEN  OrLeft  THEN  Auto)))
  THEN  (BoolCase  \mkleeneopen{}ldrs$_{uid}$  x3  \mleq{}z  ldrs$_{uid}$  x5\mkleeneclose{}\mcdot{}  THENA  \000CAuto)
  THEN  Try  (Complete  ((OrLeft  THEN  Auto)))
  THEN  (OrRight  THENA  Auto)
  THEN  AllPushDown
  THEN  OrRight
  THEN  Auto)

---

Home Index