'a,'b:S, P:('b), rep:('a'b), abs:('b'a), a:'a, r:'b.
  iso_pair('a;'b;P;rep;abs)  rep(a) = r  a = abs(r)

1

1. 'a : S 2. 'b : S 3. P : 'b 4. rep : 'a'b 5. abs : 'b'a 6. a : 'a 7. r : 'b 8. iso_pair('a;'b;P;rep;abs) 9. rep(a) = r   a = abs(r)

3 steps

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