---

Step * 2 2 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. y : Unit
6. strict-majority(IntDeq;L) = (inr y ) ∈ (ℤ?)
⊢ (if null(L) then 0 else imax-list(L) fi  ∈ L)
BY
{ (DVar `L' THEN All Reduce THEN Auto) }

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

---

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.  y  :  Unit
6.  strict-majority(IntDeq;L)  =  (inr  y  )
\mvdash{}  (if  null(L)  then  0  else  imax-list(L)  fi    \mmember{}  L)


By

---

Latex:
(DVar  `L'  THEN  All  Reduce  THEN  Auto)

---

Home Index