Nuprl - Proof: sublist filter

(24steps 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: sublist filter

T:Type, L1,L2:T List, P:(T

). L2

filter(P;L1)

L1 & (

L2.P(x))

By:	InductionOnList THEN InductionOnList THEN Reduce 0

Generated subgoals:

1 1. T : Type
2. T List
3. T List
  P:(T). nil  nil  nil  nil & (xnil.P(x))
1 step

2 1. T : Type
2. T List
3. T List
4. u : T
5. v : T List
6. P:(T). v  filter(P;nil)  v  nil & (xv.P(x))
  P:(T). [u / v]  nil  [u / v]  nil & (x[u / v].P(x))
1 step

3 1. T : Type
2. T List
3. u : T
4. v : T List
5. L2:T List, P:(T). L2  filter(P;v)  L2  v & (xL2.P(x))
6. T List
  P:(T).
  nil  if P(u) [u / filter(P;v)] else filter(P;v) fi

  nil  [u / v] & (xnil.P(x))
1 step

4 1. T : Type
2. T List
3. u : T
4. v : T List
5. L2:T List, P:(T). L2  filter(P;v)  L2  v & (xL2.P(x))
6. T List
7. u1 : T
8. v1 : T List
9. P:(T). v1  filter(P;[u / v])  v1  [u / v] & (xv1.P(x))
  P:(T).
  [u1 / v1]  if P(u) [u / filter(P;v)] else filter(P;v) fi

  [u1 / v1]  [u / v] & (x[u1 / v1].P(x))
20 steps

About:

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

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

1	1. T : Type 2. T List 3. T List P:(T). nil nil nil nil & (xnil.P(x))	1 step
2	1. T : Type 2. T List 3. T List 4. u : T 5. v : T List 6. P:(T). v filter(P;nil) v nil & (xv.P(x)) P:(T). [u / v] nil [u / v] nil & (x[u / v].P(x))	1 step
3	1. T : Type 2. T List 3. u : T 4. v : T List 5. L2:T List, P:(T). L2 filter(P;v) L2 v & (xL2.P(x)) 6. T List P:(T). nil if P(u) [u / filter(P;v)] else filter(P;v) fi nil [u / v] & (xnil.P(x))	1 step
4	1. T : Type 2. T List 3. u : T 4. v : T List 5. L2:T List, P:(T). L2 filter(P;v) L2 v & (xL2.P(x)) 6. T List 7. u1 : T 8. v1 : T List 9. P:(T). v1 filter(P;[u / v]) v1 [u / v] & (xv1.P(x)) P:(T). [u1 / v1] if P(u) [u / filter(P;v)] else filter(P;v) fi [u1 / v1] [u / v] & (x[u1 / v1].P(x))	20 steps