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

is mentioned by

Thm* ds,ds':ltg:Id fp-> Type. ds  ds'  State(ds')  State(ds)	[ma-state-subtype2]
Thm* ds,ds':ltg:Id fp-> Type. ds  ds'  (State(ds') r State(ds))	[ma-state-subtype]
Thm* eq:EqDecider(T), f,g,h:x:T fp-> Type. Thm* f || g Thm*  Thm* h || f Thm*  Thm* h || g Thm*  Thm* g  h  f  g & f  h  f  g & h  g  h  f  g & h  f  h  f  g	[fpf-compatible-triple]
Thm* B:(AType), x:A, v:B(x), eqa:EqDecider(A). x : v  x : v	[fpf-single-sub-reflexive]
Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a). f || g  g  f  g	[fpf-sub-join-right]
Thm* B1,B2:(AType), eq:EqDecider(A), f:a:A fp-> B1(a), g:a:A fp-> B2(a). Thm* f  f  g	[fpf-sub-join-left]
Thm* eq:EqDecider(X), f,g:x:X fp-> Type, x:X. f  g  (f(x)?Void r g(x)?T)	[subtype-fpf-cap-void]
Thm* eq:EqDecider(X), f,g:x:X fp-> Type, x:X. g  f  (f(x)?T r g(x)?Top)	[subtype-fpf-cap-top]
Thm* eq:EqDecider(X), f,g:x:X fp-> Type. g  f  (x:X. f(x)?Top r g(x)?Top)	[subtype-fpf-cap]
Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a). f = g  f  g	[fpf-sub_weakening]
Thm* B:(AType), eq:EqDecider(A), f,g,h:a:A fp-> B(a). f  g  g  h  f  h	[fpf-sub_transitivity]
Thm* strong-subtype(A;A') Thm*  Thm* (B:(AType), C:(A'Type), eq:EqDecider(A), eq':EqDecider(A'), Thm* (f,g:a:A fp-> B(a). (a:A. B(a) r C(a))  f  g  f  g)	[fpf-sub_functionality]
Thm* strong-subtype(A;A') Thm*  Thm* (B:(AType), C:(A'Type), eq:EqDecider(A), eq':EqDecider(A'), Thm* (f,g:a:A fp-> B(a). (a:A. B(a) r C(a))  f  g  f  g)	[fpf-sub-functionality]

In prior sections: mb event system 3 mb event system 4

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