Nuprl - Proof: member map filter

(9steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: member map filter

T:Type, P:(T

), T':Type, f:({x:T| P(x) }

T'), L:T List, x:T'.

mapfilter(f;P;L))

(

y:T. (y

L) & P(y) & x = f(y))

By:	InductionOnList THEN Unfold `mapfilter` 0 THEN Reduce 0 THEN Try (SplitOnConclITE THEN Reduce 0) THEN Try (Fold `mapfilter` 0)

Generated subgoals:

1 1. T : Type
2. P : T
3. T' : Type
4. f : {x:T| P(x) }T'
5. T List
  x:T'. (x  nil)  (y:T. (y  nil) & P(y) & x = f(y))
1 step

2 1. T : Type
2. P : T
3. T' : Type
4. f : {x:T| P(x) }T'
5. T List
6. u : T
7. v : T List
8. x:T'. (x  mapfilter(f;P;v))  (y:T. (y  v) & P(y) & x = f(y))
9. P(u)
  x@0:T'.
  (x@0  [(f(u)) / mapfilter(f;P;v)])

  (y:T. (y  [u / v]) & P(y) & x@0 = f(y))
5 steps

3 1. T : Type
2. P : T
3. T' : Type
4. f : {x:T| P(x) }T'
5. T List
6. u : T
7. v : T List
8. x:T'. (x  mapfilter(f;P;v))  (y:T. (y  v) & P(y) & x = f(y))
9. P(u)
  x:T'. (x  mapfilter(f;P;v))  (y:T. (y  [u / v]) & P(y) & x = f(y))
2 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(9steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc

1	1. T : Type 2. P : T 3. T' : Type 4. f : {x:T\| P(x) }T' 5. T List x:T'. (x nil) (y:T. (y nil) & P(y) & x = f(y))	1 step
2	1. T : Type 2. P : T 3. T' : Type 4. f : {x:T\| P(x) }T' 5. T List 6. u : T 7. v : T List 8. x:T'. (x mapfilter(f;P;v)) (y:T. (y v) & P(y) & x = f(y)) 9. P(u) x@0:T'. (x@0 [(f(u)) / mapfilter(f;P;v)]) (y:T. (y [u / v]) & P(y) & x@0 = f(y))	5 steps
3	1. T : Type 2. P : T 3. T' : Type 4. f : {x:T\| P(x) }T' 5. T List 6. u : T 7. v : T List 8. x:T'. (x mapfilter(f;P;v)) (y:T. (y v) & P(y) & x = f(y)) 9. P(u) x:T'. (x mapfilter(f;P;v)) (y:T. (y [u / v]) & P(y) & x = f(y))	2 steps