Def  AB == B<A

is mentioned by

Thm*  n:, p,q:Peg. Thm*  p  q Thm*   Thm*  (a:, z:{a...}, s:({a...z}{1...n}Peg). Thm*  (s is a Hanoi(n disk) seq on a..z & s(a) = (i.p) & s(z) = (i.q) Thm*  ( Thm*  ((2^n)z-a+1)	[hanoi_sol2_lb]
Thm*  a,z:, n:, s:({a...z}{1...n}Peg), n':. Thm*  nn' Thm*   Thm*  (h:({n+1...n'}Peg).  Thm*  (s is a Hanoi(n disk) seq on a..z Thm*  ( Thm*  ((s(?) {to n}  h {to n'}) is a Hanoi(n' disk) seq on a..z)	[hanoi_seq_deepen_seq]
Thm*  a,z:, n:, s:({a...z}{1...n}Peg), n':. Thm*  nn' Thm*   Thm*  (h:({n+1...n'}Peg), i:{1...n'}. Thm*  (in  (x:{a...z}. (s(?) {to n}  h {to n'})(x,i) = s(x,i)))	[hanoi_seq_deepen_loweq]
Thm*  a,z:, n:, s:({a...z}{1...n}Peg), n':. Thm*  nn' Thm*   Thm*  (h:({n+1...n'}Peg), i:{1...n'}. Thm*  (n<i  (x:{a...z}. (s(?) {to n}  h {to n'})(x,i) = h(i)))	[hanoi_seq_deepen_higheq]
Thm*  a,z:, n:, s:({a...z}{1...n}Peg), n':. Thm*  nn' Thm*   Thm*  (h:({n+1...n'}Peg). (s(?) {to n}  h {to n'})  {a...z}{1...n'}Peg)	[hanoi_seq_deepen_wf]
Thm*  n:, f:({1...n}Peg), n':. Thm*  nn' Thm*   Thm*  (f':({n+1...n'}Peg), i:{1...n'}. Thm*  (n<i  (f {to n}  f' {to n'})(i) = f'(i))	[hanoi_extend_higheq]
Thm*  n:, f:({1...n}Peg), n':. Thm*  nn' Thm*   Thm*  (f':({n+1...n'}Peg), i:{1...n'}. Thm*  (in  (f {to n}  f' {to n'})(i) = f(i))	[hanoi_extend_loweq]
Thm*  n:, f:({1...n}Peg), n':. Thm*  nn'  (f':({n+1...n'}Peg). (f {to n}  f' {to n'})  {1...n'}Peg)	[hanoi_extend_wf]

In prior sections: int 1 bool 1 int 2 core

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