Step * 1 of Lemma accum_filter_rel_nil


1. Type
2. Type
3. A
4. A
5. Top
6. Top
7. accum(z,x.f[z;x],a,{x∈[]|P[x]})
⊢ a ∈ A
BY
((Unfold `accum_filter_rel` (-1)) THEN (InstHyp [⌜[]⌝(-1))⋅ THEN (Reduce (-1)) THEN Try (Complete (Auto)))⋅ }


Latex:


Latex:

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


By


Latex:
((Unfold  `accum\_filter\_rel`  (-1))
  THEN  (InstHyp  [\mkleeneopen{}[]\mkleeneclose{}]  (-1))\mcdot{}
  THEN  (Reduce  (-1))
  THEN  Try  (Complete  (Auto)))\mcdot{}




Home Index