Nuprl - Proof: hanoi seq deepen loweq 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hanoi seq deepen loweq 1

1. a :

2. z :

3. n :

4. s : {a...z}

{1...n}

Peg
5. n' :

6. n

n'
7. h : {n+1...n'}

Peg
8. i : {1...n'}
9. i

n
10. x : {a...z}

(s(x) {to n}

h {to n'})(i) = s(x,i)

By:	BackThru: Thm* n:, f:({1...n}Peg), n':. Thm* nn' Thm* Thm* (f':({n+1...n'}Peg), i:{1...n'}. Thm* (in (f {to n} f' {to n'})(i) = f(i))

Generated subgoals:

None

About:

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