\x.x !pretty \x.x !def O = (\x. x x) (\x. x x) (\x.x) y O !def K = \xy.x K !pretty K !def K = \x y.x K (\w.w) ((\x y.y) (z z)) !trace (\w.w) ((\x y.y) (z z)) !pretty (\w.w) ((\x y.y) (z z)) K2 Omega !parallel_innermost K2 Omega