Def  P  Q == (P  Q) & (P  Q)

is mentioned by

Def  Moving disk k of n takes f to g Def  == (i:{1...n}. f(i) = g(i)  Peg  i  k) Def  == & (i:{1...k-1}. f(i)  f(k)  Peg & g(i)  g(k)  Peg)

[hanoi_step_at]

In prior sections: core fun 1 well fnd int 1 bool 1 int 2

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