---

Step * 1 1 1 2 of Lemma list-to-set_functionality_wrt_permutation


1. T : Type
2. eq : EqDecider(T)
3. L1 : T List
4. L2 : T List
5. permutation(T;L1;L2)
6. x : T
7. no_repeats(T;list-to-set(eq;L1))
8. no_repeats(T;list-to-set(eq;L2))
9. no_repeats(T;list-to-set(eq;L2))
10. no_repeats(T;list-to-set(eq;L1))
11. ||filter(eq x;list-to-set(eq;L1))|| = 1 ∈ ℤ supposing 1 ≤ ||filter(eq x;list-to-set(eq;L1))||
12. 1 ≤ ||filter(eq x;list-to-set(eq;L1))|| supposing ||filter(eq x;list-to-set(eq;L1))|| = 1 ∈ ℤ
13. (x ∈ list-to-set(eq;L2)) ⇒ (x ∈ L2)
14. (x ∈ list-to-set(eq;L2)) ⇐ (x ∈ L2)
15. (x ∈ list-to-set(eq;L1)) ⇒ (x ∈ L1)
16. (x ∈ list-to-set(eq;L1)) ⇐ (x ∈ L1)
17. ∀a:T. ((a ∈ L1) ⇐⇒ (a ∈ L2))
18. ¬(1 ≤ ||filter(eq x;list-to-set(eq;L1))||)
19. 1 ≤ ||filter(eq x;list-to-set(eq;L2))||
20. ||filter(eq x;list-to-set(eq;L2))|| = 1 ∈ ℤ
21. 1 ≤ ||filter(eq x;list-to-set(eq;L2))||
⊢ ||filter(eq x;list-to-set(eq;L1))|| = ||filter(eq x;list-to-set(eq;L2))|| ∈ ℤ
BY
{ (∀h:hyp. (RWO  "l_member-iff-length-filter" h THENA Auto)  THEN ThinTrivial THEN OnSomeHyp DNot THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L1  :  T  List
4.  L2  :  T  List
5.  permutation(T;L1;L2)
6.  x  :  T
7.  no\_repeats(T;list-to-set(eq;L1))
8.  no\_repeats(T;list-to-set(eq;L2))
9.  no\_repeats(T;list-to-set(eq;L2))
10.  no\_repeats(T;list-to-set(eq;L1))
11.  ||filter(eq  x;list-to-set(eq;L1))||  =  1  supposing  1  \mleq{}  ||filter(eq  x;list-to-set(eq;L1))||
12.  1  \mleq{}  ||filter(eq  x;list-to-set(eq;L1))||  supposing  ||filter(eq  x;list-to-set(eq;L1))||  =  1
13.  (x  \mmember{}  list-to-set(eq;L2))  {}\mRightarrow{}  (x  \mmember{}  L2)
14.  (x  \mmember{}  list-to-set(eq;L2))  \mLeftarrow{}{}  (x  \mmember{}  L2)
15.  (x  \mmember{}  list-to-set(eq;L1))  {}\mRightarrow{}  (x  \mmember{}  L1)
16.  (x  \mmember{}  list-to-set(eq;L1))  \mLeftarrow{}{}  (x  \mmember{}  L1)
17.  \mforall{}a:T.  ((a  \mmember{}  L1)  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  L2))
18.  \mneg{}(1  \mleq{}  ||filter(eq  x;list-to-set(eq;L1))||)
19.  1  \mleq{}  ||filter(eq  x;list-to-set(eq;L2))||
20.  ||filter(eq  x;list-to-set(eq;L2))||  =  1
21.  1  \mleq{}  ||filter(eq  x;list-to-set(eq;L2))||
\mvdash{}  ||filter(eq  x;list-to-set(eq;L1))||  =  ||filter(eq  x;list-to-set(eq;L2))||


By

---

Latex:
(\mforall{}h:hyp.  (RWO    "l\_member-iff-length-filter"  h  THENA  Auto) 
  THEN  ThinTrivial
  THEN  OnSomeHyp  DNot
  THEN  Auto)

---

Home Index