Nuprl - Proof: find property

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: find property

T:Type, P:(T

), as:T List, d:T.

((first a

as s.t. P(a) else d)

as)

(first a

as s.t. P(a) else d) = d

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

Generated subgoals:

1 1. T : Type
2. P : T
3. T List
4. u : T
5. v : T List
6. d:T.
6. ((first a  v s.t. P(a) else d)  v)  (first a  v s.t. P(a) else d) = d
7. P(u)
  d:T. (u  [u / v])  u = d
1 step

2 1. T : Type
2. P : T
3. T List
4. u : T
5. v : T List
6. d:T.
6. ((first a  v s.t. P(a) else d)  v)  (first a  v s.t. P(a) else d) = d
7. P(u)
  d:T.
  ((first a  v s.t. P(a) else d)  [u / v])
   (first a  v s.t. P(a) else d) = d
1 step

About:

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

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

1	1. T : Type 2. P : T 3. T List 4. u : T 5. v : T List 6. d:T. 6. ((first a v s.t. P(a) else d) v) (first a v s.t. P(a) else d) = d 7. P(u) d:T. (u [u / v]) u = d	1 step
2	1. T : Type 2. P : T 3. T List 4. u : T 5. v : T List 6. d:T. 6. ((first a v s.t. P(a) else d) v) (first a v s.t. P(a) else d) = d 7. P(u) d:T. ((first a v s.t. P(a) else d) [u / v]) (first a v s.t. P(a) else d) = d	1 step