Step * of Lemma bag-filter-no-repeats

No Annotations
[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)].  bag-no-repeats(T;[x∈bs|p[x]]) supposing bag-no-repeats(T;bs)
BY
((Unfold `bag-no-repeats` THEN Auto)
   THEN BagToList 3
   THEN Auto
   THEN Try ((DoSubsume THEN Auto))
   THEN (SquashExRepD THEN (EqTypeHD (-2) THENA Auto))⋅}

1
1. Type
2. T ⟶ 𝔹
3. bs List
4. L@0 List
5. L@0 bs ∈ (as,bs:T List//permutation(T;as;bs))
6. L@0 ∈ List
7. bs ∈ List
8. permutation(T;L@0;bs)
9. no_repeats(T;L@0)
⊢ ↓∃L@0:T List. ((L@0 [x∈bs|p[x]] ∈ bag(T)) ∧ no_repeats(T;L@0))


Latex:


Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[p:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[bs:bag(T)].    bag-no-repeats(T;[x\mmember{}bs|p[x]])  supposing  bag-no-repeats(T;bs)


By


Latex:
((Unfold  `bag-no-repeats`  0  THEN  Auto)
  THEN  BagToList  3
  THEN  Auto
  THEN  Try  ((DoSubsume  THEN  Auto))
  THEN  (SquashExRepD  THEN  (EqTypeHD  (-2)  THENA  Auto))\mcdot{})




Home Index