---

Step * 2 of Lemma poss-maj-invariant


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)])))))
BY
{ (ParallelLast'
   THEN MoveToConcl (-1)
   THEN GenConclAtAddr [1;1;2]
   THEN Thin (-1)
   THEN RenameVar `ys' (-1)
   THEN (GenConcl ⌜last(L) = y ∈ T⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN (Unfold `poss-maj` 0 THEN (RWO "list_accum_append" 0 THENA Auto) THEN Fold `poss-maj` 0 THEN Reduce 0)⋅)⋅ }

1
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. ¬↑null(L)
5. ||L|| ≥ 1 
6. x : T
7. ys : T List
8. y : T
⊢ let n,z = poss-maj(eq;ys;x) 
  in ((count(eq z;ys) - count(λt.(¬b(eq z t));ys)) ≤ n)
     ∧ (∀y:T. ((¬↑(eq z y)) ⇒ (n ≤ (count(λt.(¬b(eq y t));ys) - count(eq y;ys)))))
⇒ let n,z@0 = let n,x = poss-maj(eq;ys;x) 
               in if eq y x then <n + 1, x>
                  if (n =z 0) then <1, y>
                  else <n - 1, x>
                  fi  
   in ((count(eq z@0;ys @ [y]) - count(λt.(¬b(eq z@0 t));ys @ [y])) ≤ n)
      ∧ (∀y@0:T. ((¬↑(eq z@0 y@0)) ⇒ (n ≤ (count(λt.(¬b(eq y@0 t));ys @ [y]) - count(eq y@0;ys @ [y])))))

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
4.  \mneg{}\muparrow{}null(L)
5.  ||L||  \mgeq{}  1 
6.  \mforall{}x:T
          let  n,z  =  poss-maj(eq;firstn(||L||  -  1;L);x) 
          in  ((count(eq  z;firstn(||L||  -  1;L))  -  count(\mlambda{}t.(\mneg{}\msubb{}(eq  z  t));firstn(||L||  -  1;L)))  \mleq{}  n)
                \mwedge{}  (\mforall{}y:T
                          ((\mneg{}\muparrow{}(eq  z  y))
                          {}\mRightarrow{}  (n  \mleq{}  (count(\mlambda{}t.(\mneg{}\msubb{}(eq  y  t));firstn(||L||  -  1;L))  -  count(eq  y;firstn(||L|| 
                                  -  1;L))))))
\mvdash{}  \mforall{}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(\mlambda{}t.(\mneg{}\msubb{}(eq  z@0  t));firstn(||L||  -  1;L)
                @  [last(L)]))  \mleq{}  n)
              \mwedge{}  (\mforall{}y:T
                        ((\mneg{}\muparrow{}(eq  z@0  y))
                        {}\mRightarrow{}  (n  \mleq{}  (count(\mlambda{}t.(\mneg{}\msubb{}(eq  y  t));firstn(||L||  -  1;L)  @  [last(L)])  -  count(eq 
                                                                                                                                                                        y;firstn(||L|| 
                                -  1;L)
                                @  [last(L)])))))


By

---

Latex:
(ParallelLast'
  THEN  MoveToConcl  (-1)
  THEN  GenConclAtAddr  [1;1;2]
  THEN  Thin  (-1)
  THEN  RenameVar  `ys'  (-1)
  THEN  (GenConcl  \mkleeneopen{}last(L)  =  y\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  (Unfold  `poss-maj`  0
              THEN  (RWO  "list\_accum\_append"  0  THENA  Auto)
              THEN  Fold  `poss-maj`  0
              THEN  Reduce  0)\mcdot{})\mcdot{}

---

Home Index