Nuprl - Proof: member filter 2

(15steps total) PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc

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

1. T : Type
2. P : T

3. T List
4. u : T
5. v : T List
6.

x:T. (x

filter(P;v))

(x

v) & P(x)

x:T.

(x

if P(u)

[u / filter(P;v)] else filter(P;v) fi)

(x

[u / v]) & P(x)

By:	SplitOnConclITE THEN RWO Thm* l:T List, a,x:T. (x [a / l]) x = a (x l) 0

Generated subgoals:

1 7. P(u)
8. x@0 : T
9. x@0 = u  (x@0  filter(P;v))
  x@0 = u  (x@0  v)
2 steps

2 7. P(u)
8. x@0 : T
9. x@0 = u  (x@0  filter(P;v))
  P(x@0)
3 steps

3 7. P(u)
8. x@0 : T
9. x@0 = u  (x@0  v)
10. P(x@0)
  x@0 = u  (x@0  filter(P;v))
2 steps

4 7. P(u)
8. x : T
9. (x  filter(P;v))
  x = u  (x  v)
1 step

5 7. P(u)
8. x : T
9. (x  filter(P;v))
  P(x)
1 step

6 7. P(u)
8. x : T
9. x = u  (x  v)
10. P(x)
  (x  filter(P;v))
3 steps

About:

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

(15steps total) PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc