Step * 2 of Lemma accum_filter_rel_nil


1. Type
2. Type
3. A
4. A
5. Top
6. Top
7. a ∈ A
⊢ accum(z,x.f[z;x],a,{x∈[]|P[x]})
BY
(((Unfold `accum_filter_rel` THEN 0) THENA Auto)
   THEN Unfold `and` 0
   THEN Fold `cand` 0
   THEN (D (-1))
   THEN Reduce 0
   THEN Auto
   THEN Try (((D (-1)) THEN (Reduce (-1)) THEN ExRepD THEN Complete (Auto)))
   THEN ExRepD) }

1
1. Type
2. Type
3. A
4. A
5. Top
6. Top
7. a ∈ A
8. T
9. List
10. [u v] ⊆ []@i
11. ∀x:T. ((x ∈ [u v]) ⇐⇒ (x ∈ []) c∧ P[x])@i
⊢ accumulate (with value and list item x): f[z;x]over list:  vwith starting value: f[a;u]) ∈ A


Latex:


Latex:

1.  T  :  Type
2.  A  :  Type
3.  a  :  A
4.  b  :  A
5.  P  :  Top
6.  f  :  Top
7.  b  =  a
\mvdash{}  b  =  accum(z,x.f[z;x],a,\{x\mmember{}[]|P[x]\})


By


Latex:
(((Unfold  `accum\_filter\_rel`  0  THEN  D  0)  THENA  Auto)
  THEN  Unfold  `and`  0
  THEN  Fold  `cand`  0
  THEN  (D  (-1))
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  (((D  (-1))  THEN  (Reduce  (-1))  THEN  ExRepD  THEN  Complete  (Auto)))
  THEN  ExRepD)




Home Index