Step * 1 2 1 1 1 1 1 of Lemma sum-count-repeats


1. Type
2. eq EqDecider(T)
3. List
4. : ℤ
5. 0 < j
6. j ≤ ||count-repeats(L,eq)||
7. 0 < j
8. v1 T
9. v2 : ℕ+
10. count-repeats(L,eq)[j 1] = <v1, v2> ∈ (T × ℕ+)
11. v2 ||filter(λy.(eq v1);L)|| ∈ ℤ
12. : ℕ
13. i < 1
14. i < ||map(λp.(fst(p));count-repeats(L,eq))||
15. v1 ((λp.(fst(p))) count-repeats(L,eq)[i]) ∈ T
16. ¬(((λp.(fst(p))) count-repeats(L,eq)[i]) ((λp.(fst(p))) count-repeats(L,eq)[j 1]) ∈ T)
⊢ False
BY
(All Reduce THEN -1 THEN Auto) }


Latex:


Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
4.  j  :  \mBbbZ{}
5.  0  <  j
6.  j  \mleq{}  ||count-repeats(L,eq)||
7.  0  <  j
8.  v1  :  T
9.  v2  :  \mBbbN{}\msupplus{}
10.  count-repeats(L,eq)[j  -  1]  =  <v1,  v2>
11.  v2  =  ||filter(\mlambda{}y.(eq  y  v1);L)||
12.  i  :  \mBbbN{}
13.  i  <  j  -  1
14.  i  <  ||map(\mlambda{}p.(fst(p));count-repeats(L,eq))||
15.  v1  =  ((\mlambda{}p.(fst(p)))  count-repeats(L,eq)[i])
16.  \mneg{}(((\mlambda{}p.(fst(p)))  count-repeats(L,eq)[i])  =  ((\mlambda{}p.(fst(p)))  count-repeats(L,eq)[j  -  1]))
\mvdash{}  False


By


Latex:
(All  Reduce  THEN  D  -1  THEN  Auto)




Home Index