---

Step * 2 1 1 1 4 of Lemma poss-maj-invariant


1. T : Type
2. eq : EqDecider(T)
3. x : T
4. ys : T List
5. y : T
6. n : {1...}
7. z : T
8. ¬(y = z ∈ T)
9. (count(eq z;ys) - count(λt.(¬b(eq z t));ys)) ≤ n
10. ∀y:T. ((¬↑(eq z y)) ⇒ (n ≤ (count(λt.(¬b(eq y t));ys) - count(eq y;ys))))
11. (count(eq z;ys @ [y]) - count(λt.(¬b(eq z t));ys @ [y])) ≤ (n - 1)
12. y@0 : T
13. ¬↑(eq z y@0)
14. y@0 = y ∈ T
⊢ (n - 1) ≤ ((count(λt.(¬b(eq y@0 t));ys) + 0) - count(eq y@0;ys) + 1)
BY
{ (RenameVar `w' (-3)
   THEN OnMaybeHyp 11 (\h. ((InstHyp [⌜w⌝] h⋅ THEN Auto') THEN RW assert_pushdownC 0 THEN Complete (Auto)))
   )⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  T
4.  ys  :  T  List
5.  y  :  T
6.  n  :  \{1...\}
7.  z  :  T
8.  \mneg{}(y  =  z)
9.  (count(eq  z;ys)  -  count(\mlambda{}t.(\mneg{}\msubb{}(eq  z  t));ys))  \mleq{}  n
10.  \mforall{}y:T.  ((\mneg{}\muparrow{}(eq  z  y))  {}\mRightarrow{}  (n  \mleq{}  (count(\mlambda{}t.(\mneg{}\msubb{}(eq  y  t));ys)  -  count(eq  y;ys))))
11.  (count(eq  z;ys  @  [y])  -  count(\mlambda{}t.(\mneg{}\msubb{}(eq  z  t));ys  @  [y]))  \mleq{}  (n  -  1)
12.  y@0  :  T
13.  \mneg{}\muparrow{}(eq  z  y@0)
14.  y@0  =  y
\mvdash{}  (n  -  1)  \mleq{}  ((count(\mlambda{}t.(\mneg{}\msubb{}(eq  y@0  t));ys)  +  0)  -  count(eq  y@0;ys)  +  1)


By

---

Latex:
(RenameVar  `w'  (-3)
  THEN  OnMaybeHyp  11  (\mbackslash{}h.  ((InstHyp  [\mkleeneopen{}w\mkleeneclose{}]  h\mcdot{}  THEN  Auto')
                                                    THEN  RW  assert\_pushdownC  0
                                                    THEN  Complete  (Auto)))
  )\mcdot{}

---

Home Index