Nuprl - Proof: hanoi seq deepen higheq

(2steps total) PrintForm Definitions Lemmas HanoiTowers Sections NuprlLIB Doc

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

a,z:

, n:

, s:({a...z}

{1...n}

Peg), n':

.

n

n'

(

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

Peg), i:{1...n'}.

(n<i

(

x:{a...z}. (s(?) {to n}

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

By:	Compute (s(?) {to n} h {to n'})(x,i) * (s(x) {to n} h {to n'})(i)

Generated subgoal:

1 1. a :
2. z :
3. n :
4. s : {a...z}{1...n}Peg
5. n' :
6. nn'
7. h : {n+1...n'}Peg
8. i : {1...n'}
9. n<i
10. x : {a...z}
(s(x) {to n} h {to n'})(i) = h(i)
1 step

About:

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

(2steps total) PrintForm Definitions Lemmas HanoiTowers Sections NuprlLIB Doc