Nuprl - Proof: hanoi peg perm is inj 1 1 1

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=

r ; a1=

s else 6-(r+s) fi
9. =
9. if a2=

r ; a2=

s 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