Nuprl - Proof: before-map 2

(13steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: before-map 2

1. T : Type
2. T' : Type
3. f : T

T'
4. T List
5. u : T
6. v : T List
7.

x',y':T'.
7. x' before y'

map(f;v)

(

x,y:T. x before y

v & f(x) = x' & f(y) = y')

x',y':T'.

x' before y'

[(f(u)) / map(f;v)]

(

x,y:T. x before y

[u / v] & f(x) = x' & f(y) = y')

By:	UnivCD THEN RWO Thm* l:T List, a,x,y:T. Thm* x before y [a / l] x = a & (y l) x before y l 0 THEN ExRepD

Generated subgoals:

1 8. x' : T'
9. y' : T'
10. x' = f(u) & (y'  map(f;v))  x' before y'  map(f;v)
  x,y:T. x = u & (y  v)  x before y  v & f(x) = x' & f(y) = y'
5 steps

2 8. x' : T'
9. y' : T'
10. x : T
11. y : T
12. x = u & (y  v)  x before y  v
13. f(x) = x'
14. f(y) = y'
  x' = f(u) & (y'  map(f;v))  x' before y'  map(f;v)
5 steps

About:

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

(13steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc

1	8. x' : T' 9. y' : T' 10. x' = f(u) & (y' map(f;v)) x' before y' map(f;v) x,y:T. x = u & (y v) x before y v & f(x) = x' & f(y) = y'	5 steps
2	8. x' : T' 9. y' : T' 10. x : T 11. y : T 12. x = u & (y v) x before y v 13. f(x) = x' 14. f(y) = y' x' = f(u) & (y' map(f;v)) x' before y' map(f;v)	5 steps