Nuprl - Proof: intseg shift 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: intseg shift 1

1. a :

2. b :

3. a' :

4. b' :

5. b-a = b'-a'

f:({a..b

}

{a'..b'

}), g:({a'..b'

}

{a..b

}).

InvFuns({a..b

};{a'..b'

};f;g)

By:	Witness: x.x+a'-a \| x.x+a-a' THEN Analyze

Generated subgoals:

1 6. x : {a..b}
(x.x+a-a')((x.x+a'-a)(x)) = x
1 step

2 6. y : {a'..b'}
(x.x+a'-a)((x.x+a-a')(y)) = y
1 step

About:

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

1	6. x : {a..b} (x.x+a-a')((x.x+a'-a)(x)) = x	1 step
2	6. y : {a'..b'} (x.x+a'-a)((x.x+a-a')(y)) = y	1 step