---

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

∀t:ℕ. ∀L:ℤ List.
  ((∀v:ℤ
      (strict-majority-or-max(L) = v ∈ ℤ) supposing 
         (((t + 1) ≤ ||filter(λx.(x =z v);L)||) and 
         (||L|| = ((2 * t) + 1) ∈ ℤ)))
  ∧ (strict-majority-or-max(L) ∈ L) supposing ||L|| ≥ 1 )
BY
{ ((UnivCD THENA Auto) THEN Unfold `strict-majority-or-max` 0 THEN Auto) }

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

2
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 
⊢ (case strict-majority(IntDeq;L) of inl(x) => x | inr(z) => if null(L) then 0 else imax-list(L) fi  ∈ L)

---

Latex:

---

Latex:
\mforall{}t:\mBbbN{}.  \mforall{}L:\mBbbZ{}  List.
    ((\mforall{}v:\mBbbZ{}
            (strict-majority-or-max(L)  =  v)  supposing 
                  (((t  +  1)  \mleq{}  ||filter(\mlambda{}x.(x  =\msubz{}  v);L)||)  and 
                  (||L||  =  ((2  *  t)  +  1))))
    \mwedge{}  (strict-majority-or-max(L)  \mmember{}  L)  supposing  ||L||  \mgeq{}  1  )


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `strict-majority-or-max`  0  THEN  Auto)

---

Home Index