IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hanoi peg perm is inj111 1. p : {1...3}
2. r : {1...3}
3. q : {1...3}
4. s : {1...3}
5. pq 6. rs 7. a1 : {1...3}
8. a2 : {1...3}
9. if a1=pr ; a1=qs else 6-(r+s) fi
9. =
9. if a2=pr ; a2=qs else 6-(r+s) fi
a1 = a2
By:
Repeat (SplitITE Hyp:9)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html