---

Step * 1 of Lemma fset-size-remove


1. T : Type
2. eq : EqDecider(T)
3. istype(T List)
4. ∀x1,y:T List.  istype(set-equal(T;x1;y))
5. ∀x1:T List. set-equal(T;x1;x1)
6. a : Base
7. b : Base
8. c : a = b ∈ pertype(λx,y. ((x ∈ T List) ∧ (y ∈ T List) ∧ set-equal(T;x;y)))
9. a ∈ T List
10. b ∈ T List
11. set-equal(T;a;b)
12. x : T
13. x ∈ a
⊢ ||fset-remove(eq;x;a)|| = (||a|| - 1) ∈ ℤ
BY
{ (ThinVar `b'
   THEN Unfold `fset-member` (-1)
   THEN RW assert_pushdownC (-1)
   THEN Auto
   THEN RepUR ``fset-size fset-remove fset-filter`` 0
   THEN (RWO "remove-repeats-filter" 0 THENA Auto)
   THEN (InstLemma `length-remove-first` [⌜T⌝;⌜remove-repeats(eq;a)⌝;⌜λy.(eq y x)⌝]⋅ THENA Auto)
   THEN RepeatFor 2 (D -1))⋅ }

1
1. T : Type
2. eq : EqDecider(T)
3. istype(T List)
4. ∀x1,y:T List.  istype(set-equal(T;x1;y))
5. ∀x1:T List. set-equal(T;x1;x1)
6. a : Base
7. a ∈ T List
8. x : T
9. (x ∈ a)
10. (∀x@0∈remove-repeats(eq;a).¬↑((λy.(eq y x)) x@0))
11. remove-first(λy.(eq y x);remove-repeats(eq;a)) ~ remove-repeats(eq;a)
⊢ ||filter(λx@0.(¬b(eq x@0 x));remove-repeats(eq;a))|| = (||remove-repeats(eq;a)|| - 1) ∈ ℤ

2
1. T : Type
2. eq : EqDecider(T)
3. istype(T List)
4. ∀x1,y:T List.  istype(set-equal(T;x1;y))
5. ∀x1:T List. set-equal(T;x1;x1)
6. a : Base
7. a ∈ T List
8. x : T
9. (x ∈ a)
10. (∃x@0∈remove-repeats(eq;a). ↑((λy.(eq y x)) x@0))
11. ||remove-first(λy.(eq y x);remove-repeats(eq;a))|| = (||remove-repeats(eq;a)|| - 1) ∈ ℤ
⊢ ||filter(λx@0.(¬b(eq x@0 x));remove-repeats(eq;a))|| = (||remove-repeats(eq;a)|| - 1) ∈ ℤ

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  istype(T  List)
4.  \mforall{}x1,y:T  List.    istype(set-equal(T;x1;y))
5.  \mforall{}x1:T  List.  set-equal(T;x1;x1)
6.  a  :  Base
7.  b  :  Base
8.  c  :  a  =  b
9.  a  \mmember{}  T  List
10.  b  \mmember{}  T  List
11.  set-equal(T;a;b)
12.  x  :  T
13.  x  \mmember{}  a
\mvdash{}  ||fset-remove(eq;x;a)||  =  (||a||  -  1)


By

---

Latex:
(ThinVar  `b'
  THEN  Unfold  `fset-member`  (-1)
  THEN  RW  assert\_pushdownC  (-1)
  THEN  Auto
  THEN  RepUR  ``fset-size  fset-remove  fset-filter``  0
  THEN  (RWO  "remove-repeats-filter"  0  THENA  Auto)
  THEN  (InstLemma  `length-remove-first`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}remove-repeats(eq;a)\mkleeneclose{};\mkleeneopen{}\mlambda{}y.(eq  y  x)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (D  -1))\mcdot{}

---

Home Index