---

Step * 2 1 of Lemma strict-majority-or-max-property


1. t : ℕ
2. L : ℤ List
3. ∀v:ℤ
     (case strict-majority(IntDeq;L) of inl(x) => x | inr(z) => if null(L) then 0 else imax-list(L) fi 
        = v
        ∈ ℤ) supposing 
        (((t + 1) ≤ ||filter(λx.(x =z v);L)||) and 
        (||L|| = ((2 * t) + 1) ∈ ℤ))
4. ||L|| ≥ 1 
5. x : ℤ
6. strict-majority(IntDeq;L) = (inl x) ∈ (ℤ?)
⊢ (x ∈ L)
BY
{ ((RWO "strict-majority-property<" (-1)⋅ THENA Auto) THEN RepUR ``int-deq eqof`` -1) }

1
1. t : ℕ
2. L : ℤ List
3. ∀v:ℤ
     (case strict-majority(IntDeq;L) of inl(x) => x | inr(z) => if null(L) then 0 else imax-list(L) fi 
        = v
        ∈ ℤ) supposing 
        (((t + 1) ≤ ||filter(λx.(x =z v);L)||) and 
        (||L|| = ((2 * t) + 1) ∈ ℤ))
4. ||L|| ≥ 1 
5. x : ℤ
6. ||L|| < 2 * ||filter(λy.(y =z x);L)||
⊢ (x ∈ L)

---

Latex:

---

Latex:

1.  t  :  \mBbbN{}
2.  L  :  \mBbbZ{}  List
3.  \mforall{}v:\mBbbZ{}
          (case  strict-majority(IntDeq;L)
                  of  inl(x)  =>
                  x
                  |  inr(z)  =>
                  if  null(L)  then  0  else  imax-list(L)  fi 
                =  v)  supposing 
                (((t  +  1)  \mleq{}  ||filter(\mlambda{}x.(x  =\msubz{}  v);L)||)  and 
                (||L||  =  ((2  *  t)  +  1)))
4.  ||L||  \mgeq{}  1 
5.  x  :  \mBbbZ{}
6.  strict-majority(IntDeq;L)  =  (inl  x)
\mvdash{}  (x  \mmember{}  L)


By

---

Latex:
((RWO  "strict-majority-property<"  (-1)\mcdot{}  THENA  Auto)  THEN  RepUR  ``int-deq  eqof``  -1)

---

Home Index