---

Step * 2 1 1 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. ||L|| < 2 * ||filter(λy.(y =z x);L)||
7. ¬(x ∈ L)
8. i : ℕ||L||
⊢ ¬↑(L[i] =z x)
BY
{ (RW assert_pushdownC 0 THEN Auto) }

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)||
7. ¬(x ∈ L)
8. i : ℕ||L||
⊢ L[i] ≠ x

---

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.  ||L||  <  2  *  ||filter(\mlambda{}y.(y  =\msubz{}  x);L)||
7.  \mneg{}(x  \mmember{}  L)
8.  i  :  \mBbbN{}||L||
\mvdash{}  \mneg{}\muparrow{}(L[i]  =\msubz{}  x)


By

---

Latex:
(RW  assert\_pushdownC  0  THEN  Auto)

---

Home Index