---

Step * of Lemma member-fset-filter2

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. ∀[P:{x:T| x ∈ s}  ⟶ 𝔹]. ∀[x:T].  uiff(x ∈ {x ∈ s | P[x]};{x ∈ s ∧ (↑P[x])}\000C)
BY
{ (RepeatFor 5 (Intro)
   THEN (Assert {x ∈ s | P[x]} ∈ fset(T) BY
               ((SubsumeC ⌜fset({z:T| z ∈ s} )⌝⋅ THEN Auto) THEN BLemma `fset-subtype2` THEN Auto))
   THEN Auto
   THEN All (Unfold `guard`)
   THEN SupposeNot
   THEN Assert ⌜0 = 1 ∈ ℤ⌝⋅
   THEN Auto
   THEN Dquotient2 3
   THEN All
   (\h. Unfolds ``fset-filter fset-member`` h)⋅
   THEN (All (RW assert_pushdownC)  THENA Auto)
   THEN D -1
   THEN Auto) }

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. b : Base
8. c : a = b ∈ (x,y:T List//set-equal(T;x;y))
9. a ∈ T List
10. b ∈ T List
11. set-equal(T;a;b)
12. P : {x:T| ↑x ∈b a}  ⟶ 𝔹
13. x : T
14. filter(λx.P[x];a) ∈ fset(T)
15. (x ∈ filter(λx.P[x];a))
16. (x ∈ a)
⊢ ↑P[x]

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. b : Base
8. c : a = b ∈ (x,y:T List//set-equal(T;x;y))
9. a ∈ T List
10. b ∈ T List
11. set-equal(T;a;b)
12. P : {x:T| ↑x ∈b a}  ⟶ 𝔹
13. x : T
14. filter(λx.P[x];a) ∈ fset(T)
15. (x ∈ a)
16. ↑P[x]
⊢ (x ∈ filter(λx.P[x];a))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[s:fset(T)].  \mforall{}[P:\{x:T|  x  \mmember{}  s\}    {}\mrightarrow{}  \mBbbB{}].  \mforall{}[x:T].
    uiff(x  \mmember{}  \{x  \mmember{}  s  |  P[x]\};\{x  \mmember{}  s  \mwedge{}  (\muparrow{}P[x])\})


By

---

Latex:
(RepeatFor  5  (Intro)
  THEN  (Assert  \{x  \mmember{}  s  |  P[x]\}  \mmember{}  fset(T)  BY
                          ((SubsumeC  \mkleeneopen{}fset(\{z:T|  z  \mmember{}  s\}  )\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  BLemma  `fset-subtype2`  THEN  Auto))
  THEN  Auto
  THEN  All  (Unfold  `guard`)
  THEN  SupposeNot
  THEN  Assert  \mkleeneopen{}0  =  1\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Dquotient2  3
  THEN  All
  (\mbackslash{}h.  Unfolds  ``fset-filter  fset-member``  h)\mcdot{}
  THEN  (All  (RW  assert\_pushdownC)    THENA  Auto)
  THEN  D  -1
  THEN  Auto)

---

Home Index