Def f  g == x:A. x  dom(f)  x  dom(g) & f(x) = g(x)  B(x)

is mentioned by

Def M1  M2 Def == 1of(M1)  1of(M2) & 1of(2of(M1))  1of(2of(M2)) Def == & 1of(2of(2of(M1)))  1of(2of(2of(M2))) Def == & & 1of(2of(2of(2of(M1))))  1of(2of(2of(2of(M2)))) Def == & & 1of(2of(2of(2of(2of(M1)))))  1of(2of(2of(2of(2of(M2))))) Def == & & 1of(2of(2of(2of(2of(2of(M1))))))  1of(2of(2of(2of(2of(2of(M2)))))) Def == & & 1of(2of(2of(2of(2of(2of(2of(M1)))))))  1of(2of(2of(2of(2of(2of(2of( Def == & & 1of(2of(2of(2of(2of(2of(2of(M1)))))))  1of(M2))))))) Def == & & 1of(2of(2of(2of(2of(2of(2of(2of( Def == & & 1of(M1))))))))  1of(2of(2of(2of(2of(2of(2of(2of(M2))))))))

[ma-sub]

In prior sections: mb event system 3

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html