Def EqDecider(T) == eq:TTx,y:T. x = y  (eq(x,y))

is mentioned by

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* eq:EqDecider(A), P:(ATypeProp), f,g:x:A fp-> Type. Thm* ydom(f). w=f(y)   P(y,w) Thm*  Thm* ydom(g). w=g(y)   P(y,w)  ydom(f  g). w=f  g(y)   P(y,w)	[fpf-all-join-decl]
Thm* eq:EqDecider(A), B:(AType), f,g,h:a:A fp-> B(a). Thm* f || h  g || h  f  g || h	[fpf-compatible-join2]
Thm* eq:EqDecider(A), B:(AType), f,g:a:A fp-> B(a). f || g  g || f	[fpf-compatible-symmetry]
Thm* eq:EqDecider(A), B:(AType), f,g,h:a:A fp-> B(a). Thm* h || f  h || g  h || f  g	[fpf-compatible-join]
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(A), f,g:a:A fp-> Top, x:A, z:Top. Thm* f  g(x)?z ~ if x  dom(f) f(x)?z else g(x)?z fi	[fpf-join-cap-sq]
Thm* B,C:(AType), eq:EqDecider(A), f:a:A fp-> B(a), g:a:A fp-> C(a), x:A. Thm* x  dom(f)  f  g(x) = f(x)  B(x)	[fpf-join-ap-left]
Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A. Thm* x  dom(f  g)  f  g(x) = if x  dom(f) f(x) else g(x) fi  B(x)	[fpf-join-ap]
Thm* A:Type, B:(AType), f,g:a:A fp-> B(a), eq:EqDecider(A). Thm* f  g  a:A fp-> B(a)	[fpf-join_wf]
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(A), ds:x:A fp-> Type, x:A. ds(x)?Void r ds(x)?Top	[fpf-cap-void-subtype]
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]
Thm* A:Type, f:a:A fp-> Type, eq:EqDecider(A), x:A, z:Type. f(x)?z  Type	[fpf-cap-wf-univ]
Thm* A:Type, B:(AType), f:a:A fp-> B(a), eq:EqDecider(A), x:A, z:B(x). Thm* f(x)?z  B(x)	[fpf-cap_wf]
Thm* A:Type, B:(AType), f:a:A fp-> B(a), eq:EqDecider(A), x:A, Thm* P:(a:{a:A| a  dom(f) }B(a)Prop). z != f(x) ==> P(x,z)  Prop	[fpf-val_wf]
Thm* eq:EqDecider(A), B:(AType), x,y:A, v:B(x), u:B(y). Thm* (x = y  v = u  B(x))  x : v || y : u	[fpf-compatible-singles]

In prior sections: mb event system 2 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