Nuprl - Proof: hanoi step at sym 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hanoi step at sym 1

1. n :

2. f : {1...n}

Peg
3. g : {1...n}

Peg
4. k : {1...n}
5. Moving disk k of n takes f to g

Moving disk k of n takes g to f

By:	SimilarTo Hyp:-1

Generated subgoals:

1 5. i : {1...n}
6. f(i) = g(i)  i  k
  g(i) = f(i)  i  k
1 step

2 5. i : {1...k-1}
6. f(i)  f(k) & g(i)  g(k)
  g(i)  g(k) & f(i)  f(k)
Auto

About:

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

1	5. i : {1...n} 6. f(i) = g(i) i k g(i) = f(i) i k	1 step
2	5. i : {1...k-1} 6. f(i) f(k) & g(i) g(k) g(i) g(k) & f(i) f(k)	Auto