---

Step * of Lemma accum_filter_rel_wf

∀[T,A:Type]. ∀[a,b:A]. ∀[X:T List]. ∀[P:{x:T| (x ∈ X)}  ⟶ ℙ]. ∀[f:A ⟶ {x:T| (x ∈ X)}  ⟶ A].
  (b = accum(z,x.f[z;x],a,{x∈X|P[x]}) ∈ ℙ)
BY
{ (Unfold `accum_filter_rel` 0
   THEN Repeat ((D 0 THENA Complete (Auto)))
   THEN Unfold `and` 0
   THEN Fold `cand` 0
   THEN RepeatFor 3 ((MemCD THEN Try (Complete (Auto))))
   THEN Assert ⌜L ∈ {x:T| (x ∈ X)}  List⌝⋅
   THEN Auto) }

1
.....assertion..... 
1. T : Type
2. A : Type
3. a : A
4. b : A
5. X : T List
6. P : {x:T| (x ∈ X)}  ⟶ ℙ
7. f : A ⟶ {x:T| (x ∈ X)}  ⟶ A
8. L : T List@i
9. L ⊆ X c∧ (∀x:T. ((x ∈ L) ⇐⇒ (x ∈ X) c∧ P[x]))
⊢ L ∈ {x:T| (x ∈ X)}  List

---

Latex:

---

Latex:
\mforall{}[T,A:Type].  \mforall{}[a,b:A].  \mforall{}[X:T  List].  \mforall{}[P:\{x:T|  (x  \mmember{}  X)\}    {}\mrightarrow{}  \mBbbP{}].  \mforall{}[f:A  {}\mrightarrow{}  \{x:T|  (x  \mmember{}  X)\}    {}\mrightarrow{}  A].
    (b  =  accum(z,x.f[z;x],a,\{x\mmember{}X|P[x]\})  \mmember{}  \mBbbP{})


By

---

Latex:
(Unfold  `accum\_filter\_rel`  0
  THEN  Repeat  ((D  0  THENA  Complete  (Auto)))
  THEN  Unfold  `and`  0
  THEN  Fold  `cand`  0
  THEN  RepeatFor  3  ((MemCD  THEN  Try  (Complete  (Auto))))
  THEN  Assert  \mkleeneopen{}L  \mmember{}  \{x:T|  (x  \mmember{}  X)\}    List\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index