---

Step * of Lemma poss-maj-invariant

∀T:Type. ∀eq:EqDecider(T). ∀L:T List. ∀x:T.
  let n,z = poss-maj(eq;L;x) 
  in ((count(eq z;L) - count(λt.(¬b(eq z t));L)) ≤ n)
     ∧ (∀y:T. ((¬↑(eq z y)) ⇒ (n ≤ (count(λt.(¬b(eq y t));L) - count(eq y;L)))))
BY
{ InductionOnLast }

1
1. T : Type
2. eq : EqDecider(T)
⊢ ∀x:T
    let n,z@0 = poss-maj(eq;[];x) 
    in ((count(eq z@0;[]) - count(λt.(¬b(eq z@0 t));[])) ≤ n)
       ∧ (∀y:T. ((¬↑(eq z@0 y)) ⇒ (n ≤ (count(λt.(¬b(eq y t));[]) - count(eq y;[])))))

2
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. ¬↑null(L)
5. ||L|| ≥ 1 
6. ∀x:T
     let n,z = poss-maj(eq;firstn(||L|| - 1;L);x) 
     in ((count(eq z;firstn(||L|| - 1;L)) - count(λt.(¬b(eq z t));firstn(||L|| - 1;L))) ≤ n)
        ∧ (∀y:T. ((¬↑(eq z y)) ⇒ (n ≤ (count(λt.(¬b(eq y t));firstn(||L|| - 1;L)) - count(eq y;firstn(||L|| - 1;L))))))
⊢ ∀x:T
    let n,z@0 = poss-maj(eq;firstn(||L|| - 1;L) @ [last(L)];x) 
    in ((count(eq z@0;firstn(||L|| - 1;L) @ [last(L)]) - count(λt.(¬b(eq z@0 t));firstn(||L|| - 1;L) @ [last(L)])) ≤ n)
       ∧ (∀y:T
            ((¬↑(eq z@0 y))
            ⇒ (n ≤ (count(λt.(¬b(eq y t));firstn(||L|| - 1;L) @ [last(L)]) - count(eq y;firstn(||L|| - 1;L)
                @ [last(L)])))))

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}eq:EqDecider(T).  \mforall{}L:T  List.  \mforall{}x:T.
    let  n,z  =  poss-maj(eq;L;x) 
    in  ((count(eq  z;L)  -  count(\mlambda{}t.(\mneg{}\msubb{}(eq  z  t));L))  \mleq{}  n)
          \mwedge{}  (\mforall{}y:T.  ((\mneg{}\muparrow{}(eq  z  y))  {}\mRightarrow{}  (n  \mleq{}  (count(\mlambda{}t.(\mneg{}\msubb{}(eq  y  t));L)  -  count(eq  y;L)))))


By

---

Latex:
InductionOnLast

---

Home Index