---

Step * 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 
⊢ (case strict-majority(IntDeq;L) of inl(x) => x | inr(z) => if null(L) then 0 else imax-list(L) fi  ∈ L)
BY
{ (GenConclAtAddr [1;1] THEN D -2 THEN Reduce 0) }

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. strict-majority(IntDeq;L) = (inl x) ∈ (ℤ?)
⊢ (x ∈ L)

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 
5. y : Unit
6. strict-majority(IntDeq;L) = (inr y ) ∈ (ℤ?)
⊢ (if null(L) then 0 else imax-list(L) fi  ∈ 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 
\mvdash{}  (case  strict-majority(IntDeq;L)  of  inl(x)  =>  x  |  inr(z)  =>  if  null(L)  then  0  else  imax-list(L)  fi 
        \mmember{}  L)


By

---

Latex:
(GenConclAtAddr  [1;1]  THEN  D  -2  THEN  Reduce  0)

---

Home Index