(4steps total) PrintForm Definitions HanoiTowers Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hanoi peg perm is inj 1 1 1

1. p : {1...3}
2. r : {1...3}
3. q : {1...3}
4. s : {1...3}
5. p  q
6. r  s
7. a1 : {1...3}
8. a2 : {1...3}
9. if a1=p r ; a1=q s else 6-(r+s) fi
9. =
9. if a2=p r ; a2=q s else 6-(r+s) fi
  a1 = a2


By: Repeat (SplitITE Hyp:9)


Generated subgoals:

None

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

(4steps total) PrintForm Definitions HanoiTowers Sections NuprlLIB Doc