---

Step * 1 1 1 of Lemma bag-no-repeats-count


1. T : Type
2. L : T List
3. eq : EqDecider(T)
4. bs : bag(T)
5. L = bs ∈ bag(T)
6. no_repeats(T;L)
7. x : T
8. 1 ≤ ||filter(λy.(eq x y);L)||
⊢ ||filter(λy.(eq x y);L)|| = 1 ∈ ℤ
BY
{ ((InstLemma `no-repeats-iff-count` [⌜T⌝;⌜eq⌝;⌜L⌝]⋅ THENA Auto)
   THEN (D -1 THEN D -2)
   THEN Auto
   THEN InstHyp [⌜x⌝] (-2)⋅
   THEN Auto
   THEN D -2) }

1
.....antecedent..... 
1. T : Type
2. L : T List
3. eq : EqDecider(T)
4. bs : bag(T)
5. L = bs ∈ bag(T)
6. no_repeats(T;L)
7. x : T
8. 1 ≤ ||filter(λy.(eq x y);L)||
9. ∀[x:T]. uiff(1 ≤ ||filter(eq x;L)||;||filter(eq x;L)|| = 1 ∈ ℤ)
10. no_repeats(T;L)
11. 1 ≤ ||filter(eq x;L)|| supposing ||filter(eq x;L)|| = 1 ∈ ℤ
⊢ 1 ≤ ||filter(eq x;L)||

2
1. T : Type
2. L : T List
3. eq : EqDecider(T)
4. bs : bag(T)
5. L = bs ∈ bag(T)
6. no_repeats(T;L)
7. x : T
8. 1 ≤ ||filter(λy.(eq x y);L)||
9. ∀[x:T]. uiff(1 ≤ ||filter(eq x;L)||;||filter(eq x;L)|| = 1 ∈ ℤ)
10. no_repeats(T;L)
11. 1 ≤ ||filter(eq x;L)|| supposing ||filter(eq x;L)|| = 1 ∈ ℤ
12. ||filter(eq x;L)|| = 1 ∈ ℤ
⊢ ||filter(λy.(eq x y);L)|| = 1 ∈ ℤ

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
3.  eq  :  EqDecider(T)
4.  bs  :  bag(T)
5.  L  =  bs
6.  no\_repeats(T;L)
7.  x  :  T
8.  1  \mleq{}  ||filter(\mlambda{}y.(eq  x  y);L)||
\mvdash{}  ||filter(\mlambda{}y.(eq  x  y);L)||  =  1


By

---

Latex:
((InstLemma  `no-repeats-iff-count`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (D  -1  THEN  D  -2)
  THEN  Auto
  THEN  InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-2)\mcdot{}
  THEN  Auto
  THEN  D  -2)

---

Home Index