1. p : {1...3}
2. r : {1...3}
3. q : {1...3}
4. s : {1...3}
5. p  q
6. r  s
  Inj({1...3}; {1...3};
  Inj(u.if if u=p true ; false fi r
  Inj(u.i; if u=q true ; false fi s
  Inj(u.else 6-(r+s) fi)

By:	(Analyze THEN Reduce Concl ; Def of <int>=<int>) THEN Analyze THEN Reduce Concl

1

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 9.  {1...3}   a1 = a2

1 step

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