fof(reserved_2Earity0, axiom, ![X0_0, X1_0, X2_0]: s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),f3149_0_2(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),X0_0),s(ty_2Erealax_2Ereal,X1_0))) = s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))),f3149_0_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),X0_0))),s(ty_2Erealax_2Ereal,X1_0)))).
fof(reserved_2Earity1, axiom, ![X0_0, X1_0, X2_0]: s(ty_2Erealax_2Ereal,f3149_0_3(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),X0_0),s(ty_2Erealax_2Ereal,X1_0),s(ty_2Erealax_2Ereal,X2_0))) = s(ty_2Erealax_2Ereal,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))),f3149_0_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),X0_0))),s(ty_2Erealax_2Ereal,X1_0))),s(ty_2Erealax_2Ereal,X2_0)))).
fof(reserved_2Earity2, axiom, ![X0_0, X1_0, X2_0]: s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),f3149_1_2(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),X0_0),s(ty_2Erealax_2Ereal,X1_0))) = s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))),f3149_1_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),X0_0))),s(ty_2Erealax_2Ereal,X1_0)))).
fof(reserved_2Earity3, axiom, ![X0_0, X1_0, X2_0]: s(ty_2Erealax_2Ereal,f3149_1_3(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),X0_0),s(ty_2Erealax_2Ereal,X1_0),s(ty_2Erealax_2Ereal,X2_0))) = s(ty_2Erealax_2Ereal,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))),f3149_1_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),X0_0))),s(ty_2Erealax_2Ereal,X1_0))),s(ty_2Erealax_2Ereal,X2_0)))).
fof(reserved_2Earity4, axiom, ![X0_0, X1_0, X2_0]: s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),f4638_0_2(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X0_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X1_0))) = s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))),f4638_0_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X0_0))),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X1_0)))).
fof(reserved_2Earity5, axiom, ![X0_0, X1_0, X2_0]: s(ty_2Erealax_2Ereal,f4638_0_3(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X0_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X1_0),s(ty_2Erealax_2Ereal,X2_0))) = s(ty_2Erealax_2Ereal,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))),f4638_0_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X0_0))),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X1_0))),s(ty_2Erealax_2Ereal,X2_0)))).
fof(reserved_2Earity6, axiom, ![X0_0, X1_0, X2_0, X3_0]: s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),f4639_0_3(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),X0_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X1_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X2_0))) = s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)))),f4639_0_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),X0_0))),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X1_0))),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X2_0)))).
fof(reserved_2Earity7, axiom, ![X0_0, X1_0, X2_0, X3_0]: s(ty_2Erealax_2Ereal,f4639_0_4(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),X0_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X1_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X2_0),s(ty_2Erealax_2Ereal,X3_0))) = s(ty_2Erealax_2Ereal,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)))),f4639_0_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),X0_0))),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X1_0))),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X2_0))),s(ty_2Erealax_2Ereal,X3_0)))).
fof(reserved_2Earity8, axiom, ![X0_0]: s(ty_2Enum_2Enum,c1_2Earithmetic_2EBIT1(s(ty_2Enum_2Enum,X0_0))) = s(ty_2Enum_2Enum,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Enum_2Enum,ty_2Enum_2Enum),c0_2Earithmetic_2EBIT1),s(ty_2Enum_2Enum,X0_0)))).
fof(reserved_2Earity9, axiom, ![X0_0, X1_0, X2_0]: s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),c2_2Epred__set_2EIMAGE(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X0_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),X1_0))) = s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool)),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool))),c0_2Epred__set_2EIMAGE),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X0_0))),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),X1_0)))).
fof(reserved_2Earity10, axiom, ![A_27a,A_27b]: ![X0_0, X1_0]: s(A_27b,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(A_27a,A_27b),X0_0),s(A_27a,X1_0))) = s(A_27b,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(A_27a,A_27b),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Emin_2Efun(A_27a,A_27b),ty_2Emin_2Efun(A_27a,A_27b)),c0_2Ebool_2ELET),s(ty_2Emin_2Efun(A_27a,A_27b),X0_0))),s(A_27a,X1_0)))).
fof(reserved_2Earity11, axiom, ![A_27a]: ![X0_0, X1_0]: s(ty_2Emin_2Ebool,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(A_27a,ty_2Emin_2Ebool),X0_0),s(A_27a,X1_0))) = s(ty_2Emin_2Ebool,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(A_27a,ty_2Emin_2Ebool),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Emin_2Efun(A_27a,ty_2Emin_2Ebool),ty_2Emin_2Efun(A_27a,ty_2Emin_2Ebool)),c0_2Ebool_2ELET),s(ty_2Emin_2Efun(A_27a,ty_2Emin_2Ebool),X0_0))),s(A_27a,X1_0)))).
fof(reserved_2Earity12, axiom, ![X0_0, X1_0, X2_0]: s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),X0_0),s(ty_2Erealax_2Ereal,X1_0))) = s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))),c0_2Ebool_2ELET),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),X0_0))),s(ty_2Erealax_2Ereal,X1_0)))).
fof(reserved_2Earity13, axiom, ![X0_0, X1_0]: s(ty_2Erealax_2Ereal,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X0_0),s(ty_2Erealax_2Ereal,X1_0))) = s(ty_2Erealax_2Ereal,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),c0_2Ebool_2ELET),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X0_0))),s(ty_2Erealax_2Ereal,X1_0)))).
fof(reserved_2Earity14, axiom, ![X0_0]: s(ty_2Enum_2Enum,c1_2Earithmetic_2ENUMERAL(s(ty_2Enum_2Enum,X0_0))) = s(ty_2Enum_2Enum,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Enum_2Enum,ty_2Enum_2Enum),c0_2Earithmetic_2ENUMERAL),s(ty_2Enum_2Enum,X0_0)))).
fof(reserved_2Earity15, axiom, ![X0_0]: s(ty_2Emin_2Ebool,c1_2Ereal__topology_2Ebilinear(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),X0_0))) = s(ty_2Emin_2Ebool,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),ty_2Emin_2Ebool),c0_2Ereal__topology_2Ebilinear),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),X0_0)))).
fof(reserved_2Earity16, axiom, ![X0_0]: s(ty_2Emin_2Ebool,c1_2Ereal__topology_2Ebounded__def(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),X0_0))) = s(ty_2Emin_2Ebool,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),ty_2Emin_2Ebool),c0_2Ereal__topology_2Ebounded__def),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),X0_0)))).
fof(reserved_2Earity17, axiom, ![X0_0]: s(ty_2Emin_2Ebool,c1_2Ereal__topology_2Elinear(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X0_0))) = s(ty_2Emin_2Ebool,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Emin_2Ebool),c0_2Ereal__topology_2Elinear),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X0_0)))).
fof(reserved_2Earity18, axiom, ![X0_0, X1_0]: s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__add(s(ty_2Erealax_2Ereal,X0_0),s(ty_2Erealax_2Ereal,X1_0))) = s(ty_2Erealax_2Ereal,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),c0_2Erealax_2Ereal__add),s(ty_2Erealax_2Ereal,X0_0))),s(ty_2Erealax_2Ereal,X1_0)))).
fof(reserved_2Earity19, axiom, ![X0_0, X1_0]: s(ty_2Emin_2Ebool,c2_2Erealax_2Ereal__lt(s(ty_2Erealax_2Ereal,X0_0),s(ty_2Erealax_2Ereal,X1_0))) = s(ty_2Emin_2Ebool,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool)),c0_2Erealax_2Ereal__lt),s(ty_2Erealax_2Ereal,X0_0))),s(ty_2Erealax_2Ereal,X1_0)))).
fof(reserved_2Earity20, axiom, ![X0_0, X1_0]: s(ty_2Emin_2Ebool,c2_2Ereal_2Ereal__lte(s(ty_2Erealax_2Ereal,X0_0),s(ty_2Erealax_2Ereal,X1_0))) = s(ty_2Emin_2Ebool,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool)),c0_2Ereal_2Ereal__lte),s(ty_2Erealax_2Ereal,X0_0))),s(ty_2Erealax_2Ereal,X1_0)))).
fof(reserved_2Earity21, axiom, ![X0_0, X1_0]: s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__mul(s(ty_2Erealax_2Ereal,X0_0),s(ty_2Erealax_2Ereal,X1_0))) = s(ty_2Erealax_2Ereal,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),c0_2Erealax_2Ereal__mul),s(ty_2Erealax_2Ereal,X0_0))),s(ty_2Erealax_2Ereal,X1_0)))).
fof(reserved_2Earity22, axiom, ![X0_0]: s(ty_2Erealax_2Ereal,c1_2Erealax_2Ereal__neg(s(ty_2Erealax_2Ereal,X0_0))) = s(ty_2Erealax_2Ereal,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),c0_2Erealax_2Ereal__neg),s(ty_2Erealax_2Ereal,X0_0)))).
fof(reserved_2Earity23, axiom, ![X0_0]: s(ty_2Erealax_2Ereal,c1_2Ereal_2Ereal__of__num(s(ty_2Enum_2Enum,X0_0))) = s(ty_2Erealax_2Ereal,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Enum_2Enum,ty_2Erealax_2Ereal),c0_2Ereal_2Ereal__of__num),s(ty_2Enum_2Enum,X0_0)))).
fof(reserved_2Earity24, axiom, ![X0_0, X1_0]: s(ty_2Emin_2Ebool,c2_2Ereal__topology_2Euniformly__continuous__on(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X0_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),X1_0))) = s(ty_2Emin_2Ebool,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),ty_2Emin_2Ebool),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Emin_2Efun(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),ty_2Emin_2Ebool)),c0_2Ereal__topology_2Euniformly__continuous__on),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),X0_0))),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),X1_0)))).
fof(reserved_2Etruth_2E0, axiom, p(s(ty_2Emin_2Ebool,c0_2Ebool_2ET))).
fof(reserved_2Enotfalse_2E0, axiom, ~ (p(s(ty_2Emin_2Ebool,c0_2Ebool_2EF)))).
fof(reserved_2Ebool__cases__ax_2E0, axiom, ![V0t_0]: (s(ty_2Emin_2Ebool,V0t_0) = s(ty_2Emin_2Ebool,c0_2Ebool_2ET) | s(ty_2Emin_2Ebool,V0t_0) = s(ty_2Emin_2Ebool,c0_2Ebool_2EF))).
fof(reserved_2Eeq__ext_2E0, axiom, ![A_27a,A_27b]: ![V0f_0, V1g_0]: (![V2x_0]: s(A_27b,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(A_27a,A_27b),V0f_0),s(A_27a,V2x_0))) = s(A_27b,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(A_27a,A_27b),V1g_0),s(A_27a,V2x_0))) => s(ty_2Emin_2Efun(A_27a,A_27b),V0f_0) = s(ty_2Emin_2Efun(A_27a,A_27b),V1g_0))).
fof(thm_2EboolTheory_2ETRUTH_2E0, axiom, p(s(ty_2Emin_2Ebool,c0_2Ebool_2ET))).
fof(thm_2EboolTheory_2EAND__CLAUSES_2E0, axiom, ![V0t_0]: (((p(s(ty_2Emin_2Ebool,c0_2Ebool_2ET)) & p(s(ty_2Emin_2Ebool,V0t_0))) <=> p(s(ty_2Emin_2Ebool,V0t_0))) & (((p(s(ty_2Emin_2Ebool,V0t_0)) & p(s(ty_2Emin_2Ebool,c0_2Ebool_2ET))) <=> p(s(ty_2Emin_2Ebool,V0t_0))) & (((p(s(ty_2Emin_2Ebool,c0_2Ebool_2EF)) & p(s(ty_2Emin_2Ebool,V0t_0))) <=> p(s(ty_2Emin_2Ebool,c0_2Ebool_2EF))) & (((p(s(ty_2Emin_2Ebool,V0t_0)) & p(s(ty_2Emin_2Ebool,c0_2Ebool_2EF))) <=> p(s(ty_2Emin_2Ebool,c0_2Ebool_2EF))) & ((p(s(ty_2Emin_2Ebool,V0t_0)) & p(s(ty_2Emin_2Ebool,V0t_0))) <=> p(s(ty_2Emin_2Ebool,V0t_0)))))))).
fof(thm_2EboolTheory_2EIMP__CLAUSES_2E0, axiom, ![V0t_0]: (((p(s(ty_2Emin_2Ebool,c0_2Ebool_2ET)) => p(s(ty_2Emin_2Ebool,V0t_0))) <=> p(s(ty_2Emin_2Ebool,V0t_0))) & (((p(s(ty_2Emin_2Ebool,V0t_0)) => p(s(ty_2Emin_2Ebool,c0_2Ebool_2ET))) <=> p(s(ty_2Emin_2Ebool,c0_2Ebool_2ET))) & (((p(s(ty_2Emin_2Ebool,c0_2Ebool_2EF)) => p(s(ty_2Emin_2Ebool,V0t_0))) <=> p(s(ty_2Emin_2Ebool,c0_2Ebool_2ET))) & (((p(s(ty_2Emin_2Ebool,V0t_0)) => p(s(ty_2Emin_2Ebool,V0t_0))) <=> p(s(ty_2Emin_2Ebool,c0_2Ebool_2ET))) & ((p(s(ty_2Emin_2Ebool,V0t_0)) => p(s(ty_2Emin_2Ebool,c0_2Ebool_2EF))) <=> ~ (p(s(ty_2Emin_2Ebool,V0t_0))))))))).
fof(thm_2EboolTheory_2ENOT__CLAUSES_2E0, axiom, (![V0t_0]: (~ (~ (p(s(ty_2Emin_2Ebool,V0t_0)))) <=> p(s(ty_2Emin_2Ebool,V0t_0))) & ((~ (p(s(ty_2Emin_2Ebool,c0_2Ebool_2ET))) <=> p(s(ty_2Emin_2Ebool,c0_2Ebool_2EF))) & (~ (p(s(ty_2Emin_2Ebool,c0_2Ebool_2EF))) <=> p(s(ty_2Emin_2Ebool,c0_2Ebool_2ET)))))).
fof(thm_2EboolTheory_2EREFL__CLAUSE_2E0, axiom, ![A_27a]: ![V0x_0]: (s(A_27a,V0x_0) = s(A_27a,V0x_0) <=> p(s(ty_2Emin_2Ebool,c0_2Ebool_2ET)))).
fof(thm_2EboolTheory_2EEQ__SYM__EQ_2E0, axiom, ![A_27a]: ![V0x_0, V1y_0]: (s(A_27a,V0x_0) = s(A_27a,V1y_0) <=> s(A_27a,V1y_0) = s(A_27a,V0x_0))).
fof(thm_2EboolTheory_2EEQ__CLAUSES_2E0, axiom, ![V0t_0]: ((s(ty_2Emin_2Ebool,c0_2Ebool_2ET) = s(ty_2Emin_2Ebool,V0t_0) <=> p(s(ty_2Emin_2Ebool,V0t_0))) & ((s(ty_2Emin_2Ebool,V0t_0) = s(ty_2Emin_2Ebool,c0_2Ebool_2ET) <=> p(s(ty_2Emin_2Ebool,V0t_0))) & ((s(ty_2Emin_2Ebool,c0_2Ebool_2EF) = s(ty_2Emin_2Ebool,V0t_0) <=> ~ (p(s(ty_2Emin_2Ebool,V0t_0)))) & (s(ty_2Emin_2Ebool,V0t_0) = s(ty_2Emin_2Ebool,c0_2Ebool_2EF) <=> ~ (p(s(ty_2Emin_2Ebool,V0t_0)))))))).
fof(thm_2EboolTheory_2EFORALL__AND__THM_2E0, axiom, ![A_27a]: ![V0P_0, V1Q_0]: (![V2x_0]: (p(s(ty_2Emin_2Ebool,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(A_27a,ty_2Emin_2Ebool),V0P_0),s(A_27a,V2x_0)))) & p(s(ty_2Emin_2Ebool,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(A_27a,ty_2Emin_2Ebool),V1Q_0),s(A_27a,V2x_0))))) <=> (![V3x_0]: p(s(ty_2Emin_2Ebool,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(A_27a,ty_2Emin_2Ebool),V0P_0),s(A_27a,V3x_0)))) & ![V4x_0]: p(s(ty_2Emin_2Ebool,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(A_27a,ty_2Emin_2Ebool),V1Q_0),s(A_27a,V4x_0))))))).
fof(thm_2EboolTheory_2EDISJ__ASSOC_2E0, axiom, ![V0A_0, V1B_0, V2C_0]: ((p(s(ty_2Emin_2Ebool,V0A_0)) | (p(s(ty_2Emin_2Ebool,V1B_0)) | p(s(ty_2Emin_2Ebool,V2C_0)))) <=> ((p(s(ty_2Emin_2Ebool,V0A_0)) | p(s(ty_2Emin_2Ebool,V1B_0))) | p(s(ty_2Emin_2Ebool,V2C_0))))).
fof(thm_2EboolTheory_2EDE__MORGAN__THM_2E0, axiom, ![V0A_0, V1B_0]: ((~ ((p(s(ty_2Emin_2Ebool,V0A_0)) & p(s(ty_2Emin_2Ebool,V1B_0)))) <=> (~ (p(s(ty_2Emin_2Ebool,V0A_0))) | ~ (p(s(ty_2Emin_2Ebool,V1B_0))))) & (~ ((p(s(ty_2Emin_2Ebool,V0A_0)) | p(s(ty_2Emin_2Ebool,V1B_0)))) <=> (~ (p(s(ty_2Emin_2Ebool,V0A_0))) & ~ (p(s(ty_2Emin_2Ebool,V1B_0))))))).
fof(thm_2EboolTheory_2EAND__IMP__INTRO_2E0, axiom, ![V0t1_0, V1t2_0, V2t3_0]: ((p(s(ty_2Emin_2Ebool,V0t1_0)) => (p(s(ty_2Emin_2Ebool,V1t2_0)) => p(s(ty_2Emin_2Ebool,V2t3_0)))) <=> ((p(s(ty_2Emin_2Ebool,V0t1_0)) & p(s(ty_2Emin_2Ebool,V1t2_0))) => p(s(ty_2Emin_2Ebool,V2t3_0))))).
fof(thm_2EboolTheory_2EIMP__CONG_2E0, axiom, ![V0x_0, V1x_27_0, V2y_0, V3y_27_0]: ((s(ty_2Emin_2Ebool,V0x_0) = s(ty_2Emin_2Ebool,V1x_27_0) & (p(s(ty_2Emin_2Ebool,V1x_27_0)) => s(ty_2Emin_2Ebool,V2y_0) = s(ty_2Emin_2Ebool,V3y_27_0))) => ((p(s(ty_2Emin_2Ebool,V0x_0)) => p(s(ty_2Emin_2Ebool,V2y_0))) <=> (p(s(ty_2Emin_2Ebool,V1x_27_0)) => p(s(ty_2Emin_2Ebool,V3y_27_0)))))).
fof(thm_2ErealTheory_2EREAL__ADD__SYM_2E0, axiom, ![V0x_0, V1y_0]: s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__add(s(ty_2Erealax_2Ereal,V0x_0),s(ty_2Erealax_2Ereal,V1y_0))) = s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__add(s(ty_2Erealax_2Ereal,V1y_0),s(ty_2Erealax_2Ereal,V0x_0)))).
fof(thm_2ErealTheory_2EREAL__ADD__ASSOC_2E0, axiom, ![V0x_0, V1y_0, V2z_0]: s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__add(s(ty_2Erealax_2Ereal,V0x_0),s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__add(s(ty_2Erealax_2Ereal,V1y_0),s(ty_2Erealax_2Ereal,V2z_0))))) = s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__add(s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__add(s(ty_2Erealax_2Ereal,V0x_0),s(ty_2Erealax_2Ereal,V1y_0))),s(ty_2Erealax_2Ereal,V2z_0)))).
fof(thm_2ErealTheory_2EREAL__ADD__LINV_2E0, axiom, ![V0x_0]: s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__add(s(ty_2Erealax_2Ereal,c1_2Erealax_2Ereal__neg(s(ty_2Erealax_2Ereal,V0x_0))),s(ty_2Erealax_2Ereal,V0x_0))) = s(ty_2Erealax_2Ereal,c1_2Ereal_2Ereal__of__num(s(ty_2Enum_2Enum,c0_2Enum_2E0)))).
fof(thm_2ErealTheory_2EREAL__MUL__SYM_2E0, axiom, ![V0x_0, V1y_0]: s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__mul(s(ty_2Erealax_2Ereal,V0x_0),s(ty_2Erealax_2Ereal,V1y_0))) = s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__mul(s(ty_2Erealax_2Ereal,V1y_0),s(ty_2Erealax_2Ereal,V0x_0)))).
fof(thm_2ErealTheory_2EREAL__MUL__ASSOC_2E0, axiom, ![V0x_0, V1y_0, V2z_0]: s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__mul(s(ty_2Erealax_2Ereal,V0x_0),s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__mul(s(ty_2Erealax_2Ereal,V1y_0),s(ty_2Erealax_2Ereal,V2z_0))))) = s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__mul(s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__mul(s(ty_2Erealax_2Ereal,V0x_0),s(ty_2Erealax_2Ereal,V1y_0))),s(ty_2Erealax_2Ereal,V2z_0)))).
fof(thm_2ErealTheory_2EREAL__MUL__LID_2E0, axiom, ![V0x_0]: s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__mul(s(ty_2Erealax_2Ereal,c1_2Ereal_2Ereal__of__num(s(ty_2Enum_2Enum,c1_2Earithmetic_2ENUMERAL(s(ty_2Enum_2Enum,c1_2Earithmetic_2EBIT1(s(ty_2Enum_2Enum,c0_2Earithmetic_2EZERO))))))),s(ty_2Erealax_2Ereal,V0x_0))) = s(ty_2Erealax_2Ereal,V0x_0)).
fof(thm_2ErealTheory_2EREAL__ADD__RID_2E0, axiom, ![V0x_0]: s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__add(s(ty_2Erealax_2Ereal,V0x_0),s(ty_2Erealax_2Ereal,c1_2Ereal_2Ereal__of__num(s(ty_2Enum_2Enum,c0_2Enum_2E0))))) = s(ty_2Erealax_2Ereal,V0x_0)).
fof(thm_2ErealTheory_2EREAL__ADD__RINV_2E0, axiom, ![V0x_0]: s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__add(s(ty_2Erealax_2Ereal,V0x_0),s(ty_2Erealax_2Ereal,c1_2Erealax_2Ereal__neg(s(ty_2Erealax_2Ereal,V0x_0))))) = s(ty_2Erealax_2Ereal,c1_2Ereal_2Ereal__of__num(s(ty_2Enum_2Enum,c0_2Enum_2E0)))).
fof(thm_2ErealTheory_2EREAL__NEG__ADD_2E0, axiom, ![V0x_0, V1y_0]: s(ty_2Erealax_2Ereal,c1_2Erealax_2Ereal__neg(s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__add(s(ty_2Erealax_2Ereal,V0x_0),s(ty_2Erealax_2Ereal,V1y_0))))) = s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__add(s(ty_2Erealax_2Ereal,c1_2Erealax_2Ereal__neg(s(ty_2Erealax_2Ereal,V0x_0))),s(ty_2Erealax_2Ereal,c1_2Erealax_2Ereal__neg(s(ty_2Erealax_2Ereal,V1y_0)))))).
fof(thm_2ErealTheory_2EREAL__MUL__LZERO_2E0, axiom, ![V0x_0]: s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__mul(s(ty_2Erealax_2Ereal,c1_2Ereal_2Ereal__of__num(s(ty_2Enum_2Enum,c0_2Enum_2E0))),s(ty_2Erealax_2Ereal,V0x_0))) = s(ty_2Erealax_2Ereal,c1_2Ereal_2Ereal__of__num(s(ty_2Enum_2Enum,c0_2Enum_2E0)))).
fof(thm_2ErealTheory_2EREAL__LE__REFL_2E0, axiom, ![V0x_0]: p(s(ty_2Emin_2Ebool,c2_2Ereal_2Ereal__lte(s(ty_2Erealax_2Ereal,V0x_0),s(ty_2Erealax_2Ereal,V0x_0))))).
fof(thm_2ErealTheory_2EREAL__LE__ANTISYM_2E0, axiom, ![V0x_0, V1y_0]: ((p(s(ty_2Emin_2Ebool,c2_2Ereal_2Ereal__lte(s(ty_2Erealax_2Ereal,V0x_0),s(ty_2Erealax_2Ereal,V1y_0)))) & p(s(ty_2Emin_2Ebool,c2_2Ereal_2Ereal__lte(s(ty_2Erealax_2Ereal,V1y_0),s(ty_2Erealax_2Ereal,V0x_0))))) <=> s(ty_2Erealax_2Ereal,V0x_0) = s(ty_2Erealax_2Ereal,V1y_0))).
fof(thm_2ErealTheory_2EREAL__MUL__LNEG_2E0, axiom, ![V0x_0, V1y_0]: s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__mul(s(ty_2Erealax_2Ereal,c1_2Erealax_2Ereal__neg(s(ty_2Erealax_2Ereal,V0x_0))),s(ty_2Erealax_2Ereal,V1y_0))) = s(ty_2Erealax_2Ereal,c1_2Erealax_2Ereal__neg(s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__mul(s(ty_2Erealax_2Ereal,V0x_0),s(ty_2Erealax_2Ereal,V1y_0)))))).
fof(thm_2ErealTheory_2Ereal__lt_2E0, axiom, ![V0y_0, V1x_0]: (p(s(ty_2Emin_2Ebool,c2_2Erealax_2Ereal__lt(s(ty_2Erealax_2Ereal,V1x_0),s(ty_2Erealax_2Ereal,V0y_0)))) <=> ~ (p(s(ty_2Emin_2Ebool,c2_2Ereal_2Ereal__lte(s(ty_2Erealax_2Ereal,V0y_0),s(ty_2Erealax_2Ereal,V1x_0))))))).
fof(thm_2ErealTheory_2EREAL__LE__LNEG_2E0, axiom, ![V0x_0, V1y_0]: s(ty_2Emin_2Ebool,c2_2Ereal_2Ereal__lte(s(ty_2Erealax_2Ereal,c1_2Erealax_2Ereal__neg(s(ty_2Erealax_2Ereal,V0x_0))),s(ty_2Erealax_2Ereal,V1y_0))) = s(ty_2Emin_2Ebool,c2_2Ereal_2Ereal__lte(s(ty_2Erealax_2Ereal,c1_2Ereal_2Ereal__of__num(s(ty_2Enum_2Enum,c0_2Enum_2E0))),s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__add(s(ty_2Erealax_2Ereal,V0x_0),s(ty_2Erealax_2Ereal,V1y_0)))))).
fof(thm_2ErealTheory_2EREAL__LE__NEG2_2E0, axiom, ![V0x_0, V1y_0]: s(ty_2Emin_2Ebool,c2_2Ereal_2Ereal__lte(s(ty_2Erealax_2Ereal,c1_2Erealax_2Ereal__neg(s(ty_2Erealax_2Ereal,V0x_0))),s(ty_2Erealax_2Ereal,c1_2Erealax_2Ereal__neg(s(ty_2Erealax_2Ereal,V1y_0))))) = s(ty_2Emin_2Ebool,c2_2Ereal_2Ereal__lte(s(ty_2Erealax_2Ereal,V1y_0),s(ty_2Erealax_2Ereal,V0x_0)))).
fof(thm_2ErealTheory_2EREAL__NEG__NEG_2E0, axiom, ![V0x_0]: s(ty_2Erealax_2Ereal,c1_2Erealax_2Ereal__neg(s(ty_2Erealax_2Ereal,c1_2Erealax_2Ereal__neg(s(ty_2Erealax_2Ereal,V0x_0))))) = s(ty_2Erealax_2Ereal,V0x_0)).
fof(thm_2ErealTheory_2EREAL__LE__RNEG_2E0, axiom, ![V0x_0, V1y_0]: s(ty_2Emin_2Ebool,c2_2Ereal_2Ereal__lte(s(ty_2Erealax_2Ereal,V0x_0),s(ty_2Erealax_2Ereal,c1_2Erealax_2Ereal__neg(s(ty_2Erealax_2Ereal,V1y_0))))) = s(ty_2Emin_2Ebool,c2_2Ereal_2Ereal__lte(s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__add(s(ty_2Erealax_2Ereal,V0x_0),s(ty_2Erealax_2Ereal,V1y_0))),s(ty_2Erealax_2Ereal,c1_2Ereal_2Ereal__of__num(s(ty_2Enum_2Enum,c0_2Enum_2E0)))))).
fof(thm_2ErealTheory_2EREAL__ADD__LDISTRIB_2E0, axiom, ![V0x_0, V1y_0, V2z_0]: s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__mul(s(ty_2Erealax_2Ereal,V0x_0),s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__add(s(ty_2Erealax_2Ereal,V1y_0),s(ty_2Erealax_2Ereal,V2z_0))))) = s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__add(s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__mul(s(ty_2Erealax_2Ereal,V0x_0),s(ty_2Erealax_2Ereal,V1y_0))),s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__mul(s(ty_2Erealax_2Ereal,V0x_0),s(ty_2Erealax_2Ereal,V2z_0)))))).
fof(thm_2ErealTheory_2EREAL__ADD__RDISTRIB_2E0, axiom, ![V0x_0, V1y_0, V2z_0]: s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__mul(s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__add(s(ty_2Erealax_2Ereal,V0x_0),s(ty_2Erealax_2Ereal,V1y_0))),s(ty_2Erealax_2Ereal,V2z_0))) = s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__add(s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__mul(s(ty_2Erealax_2Ereal,V0x_0),s(ty_2Erealax_2Ereal,V2z_0))),s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__mul(s(ty_2Erealax_2Ereal,V1y_0),s(ty_2Erealax_2Ereal,V2z_0)))))).
fof(thm_2Ereal__topologyTheory_2Elinear_2E0, axiom, ![V0f_0]: (p(s(ty_2Emin_2Ebool,c1_2Ereal__topology_2Elinear(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V0f_0)))) <=> (![V1x_0, V2y_0]: s(ty_2Erealax_2Ereal,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V0f_0),s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__add(s(ty_2Erealax_2Ereal,V1x_0),s(ty_2Erealax_2Ereal,V2y_0))))) = s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__add(s(ty_2Erealax_2Ereal,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V0f_0),s(ty_2Erealax_2Ereal,V1x_0))),s(ty_2Erealax_2Ereal,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V0f_0),s(ty_2Erealax_2Ereal,V2y_0))))) & ![V3c_0, V4x_0]: s(ty_2Erealax_2Ereal,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V0f_0),s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__mul(s(ty_2Erealax_2Ereal,V3c_0),s(ty_2Erealax_2Ereal,V4x_0))))) = s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__mul(s(ty_2Erealax_2Ereal,V3c_0),s(ty_2Erealax_2Ereal,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V0f_0),s(ty_2Erealax_2Ereal,V4x_0)))))))).
fof(thm_2Ereal__topologyTheory_2Ebilinear_2E0, axiom, ![V0f_0]: (p(s(ty_2Emin_2Ebool,c1_2Ereal__topology_2Ebilinear(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),V0f_0)))) <=> (![V1x_0]: p(s(ty_2Emin_2Ebool,c1_2Ereal__topology_2Elinear(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),f3149_0_2(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),V0f_0),s(ty_2Erealax_2Ereal,V1x_0)))))) & ![V3y_0]: p(s(ty_2Emin_2Ebool,c1_2Ereal__topology_2Elinear(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),f3149_1_2(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),V0f_0),s(ty_2Erealax_2Ereal,V3y_0))))))))).
fof(thm_2Ereal__topologyTheory_2Ebilinear_2E1, axiom, ![V0f_0, V3y_0, V4x_0]: s(ty_2Erealax_2Ereal,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),V0f_0),s(ty_2Erealax_2Ereal,V4x_0))),s(ty_2Erealax_2Ereal,V3y_0))) = s(ty_2Erealax_2Ereal,f3149_1_3(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),V0f_0),s(ty_2Erealax_2Ereal,V3y_0),s(ty_2Erealax_2Ereal,V4x_0)))).
fof(thm_2Ereal__topologyTheory_2Ebilinear_2E2, axiom, ![V0f_0, V1x_0, V2y_0]: s(ty_2Erealax_2Ereal,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),V0f_0),s(ty_2Erealax_2Ereal,V1x_0))),s(ty_2Erealax_2Ereal,V2y_0))) = s(ty_2Erealax_2Ereal,f3149_0_3(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),V0f_0),s(ty_2Erealax_2Ereal,V1x_0),s(ty_2Erealax_2Ereal,V2y_0)))).
fof(thm_2Ereal__topologyTheory_2EBILINEAR__UNIFORMLY__CONTINUOUS__ON__COMPOSE_2E0, axiom, ![V0f_0, V1g_0, V2h_0, V3s_0]: ((p(s(ty_2Emin_2Ebool,c2_2Ereal__topology_2Euniformly__continuous__on(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V0f_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),V3s_0)))) & (p(s(ty_2Emin_2Ebool,c2_2Ereal__topology_2Euniformly__continuous__on(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V1g_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),V3s_0)))) & (p(s(ty_2Emin_2Ebool,c1_2Ereal__topology_2Ebilinear(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),V2h_0)))) & (p(s(ty_2Emin_2Ebool,c1_2Ereal__topology_2Ebounded__def(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),c2_2Epred__set_2EIMAGE(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V0f_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),V3s_0)))))) & p(s(ty_2Emin_2Ebool,c1_2Ereal__topology_2Ebounded__def(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),c2_2Epred__set_2EIMAGE(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V1g_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),V3s_0)))))))))) => p(s(ty_2Emin_2Ebool,c2_2Ereal__topology_2Euniformly__continuous__on(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),f4639_0_3(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),V2h_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V0f_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V1g_0))),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),V3s_0)))))).
fof(thm_2Ereal__topologyTheory_2EBILINEAR__UNIFORMLY__CONTINUOUS__ON__COMPOSE_2E1, axiom, ![V2h_0, V0f_0, V1g_0, V4x_0]: s(ty_2Erealax_2Ereal,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),V2h_0),s(ty_2Erealax_2Ereal,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V0f_0),s(ty_2Erealax_2Ereal,V4x_0))))),s(ty_2Erealax_2Ereal,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V1g_0),s(ty_2Erealax_2Ereal,V4x_0))))) = s(ty_2Erealax_2Ereal,f4639_0_4(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),V2h_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V0f_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V1g_0),s(ty_2Erealax_2Ereal,V4x_0)))).
fof(thm_2EsatTheory_2ENOT__NOT_2E0, axiom, ![V0t_0]: (~ (~ (p(s(ty_2Emin_2Ebool,V0t_0)))) <=> p(s(ty_2Emin_2Ebool,V0t_0)))).
fof(thm_2EsatTheory_2EAND__INV__IMP_2E0, axiom, ![V0A_0]: (p(s(ty_2Emin_2Ebool,V0A_0)) => (~ (p(s(ty_2Emin_2Ebool,V0A_0))) => p(s(ty_2Emin_2Ebool,c0_2Ebool_2EF))))).
fof(thm_2EsatTheory_2EOR__DUAL2_2E0, axiom, ![V0A_0, V1B_0]: ((~ ((p(s(ty_2Emin_2Ebool,V0A_0)) | p(s(ty_2Emin_2Ebool,V1B_0)))) => p(s(ty_2Emin_2Ebool,c0_2Ebool_2EF))) <=> ((p(s(ty_2Emin_2Ebool,V0A_0)) => p(s(ty_2Emin_2Ebool,c0_2Ebool_2EF))) => (~ (p(s(ty_2Emin_2Ebool,V1B_0))) => p(s(ty_2Emin_2Ebool,c0_2Ebool_2EF)))))).
fof(thm_2EsatTheory_2EOR__DUAL3_2E0, axiom, ![V0A_0, V1B_0]: ((~ ((~ (p(s(ty_2Emin_2Ebool,V0A_0))) | p(s(ty_2Emin_2Ebool,V1B_0)))) => p(s(ty_2Emin_2Ebool,c0_2Ebool_2EF))) <=> (p(s(ty_2Emin_2Ebool,V0A_0)) => (~ (p(s(ty_2Emin_2Ebool,V1B_0))) => p(s(ty_2Emin_2Ebool,c0_2Ebool_2EF)))))).
fof(thm_2EsatTheory_2EAND__INV2_2E0, axiom, ![V0A_0]: ((~ (p(s(ty_2Emin_2Ebool,V0A_0))) => p(s(ty_2Emin_2Ebool,c0_2Ebool_2EF))) => ((p(s(ty_2Emin_2Ebool,V0A_0)) => p(s(ty_2Emin_2Ebool,c0_2Ebool_2EF))) => p(s(ty_2Emin_2Ebool,c0_2Ebool_2EF))))).
fof(thm_2EsatTheory_2Edc__eq_2E0, axiom, ![V0p_0, V1q_0, V2r_0]: ((p(s(ty_2Emin_2Ebool,V0p_0)) <=> s(ty_2Emin_2Ebool,V1q_0) = s(ty_2Emin_2Ebool,V2r_0)) <=> ((p(s(ty_2Emin_2Ebool,V0p_0)) | (p(s(ty_2Emin_2Ebool,V1q_0)) | p(s(ty_2Emin_2Ebool,V2r_0)))) & ((p(s(ty_2Emin_2Ebool,V0p_0)) | (~ (p(s(ty_2Emin_2Ebool,V2r_0))) | ~ (p(s(ty_2Emin_2Ebool,V1q_0))))) & ((p(s(ty_2Emin_2Ebool,V1q_0)) | (~ (p(s(ty_2Emin_2Ebool,V2r_0))) | ~ (p(s(ty_2Emin_2Ebool,V0p_0))))) & (p(s(ty_2Emin_2Ebool,V2r_0)) | (~ (p(s(ty_2Emin_2Ebool,V1q_0))) | ~ (p(s(ty_2Emin_2Ebool,V0p_0)))))))))).
fof(thm_2EsatTheory_2Edc__conj_2E0, axiom, ![V0p_0, V1q_0, V2r_0]: ((p(s(ty_2Emin_2Ebool,V0p_0)) <=> (p(s(ty_2Emin_2Ebool,V1q_0)) & p(s(ty_2Emin_2Ebool,V2r_0)))) <=> ((p(s(ty_2Emin_2Ebool,V0p_0)) | (~ (p(s(ty_2Emin_2Ebool,V1q_0))) | ~ (p(s(ty_2Emin_2Ebool,V2r_0))))) & ((p(s(ty_2Emin_2Ebool,V1q_0)) | ~ (p(s(ty_2Emin_2Ebool,V0p_0)))) & (p(s(ty_2Emin_2Ebool,V2r_0)) | ~ (p(s(ty_2Emin_2Ebool,V0p_0)))))))).
fof(thm_2EsatTheory_2Edc__disj_2E0, axiom, ![V0p_0, V1q_0, V2r_0]: ((p(s(ty_2Emin_2Ebool,V0p_0)) <=> (p(s(ty_2Emin_2Ebool,V1q_0)) | p(s(ty_2Emin_2Ebool,V2r_0)))) <=> ((p(s(ty_2Emin_2Ebool,V0p_0)) | ~ (p(s(ty_2Emin_2Ebool,V1q_0)))) & ((p(s(ty_2Emin_2Ebool,V0p_0)) | ~ (p(s(ty_2Emin_2Ebool,V2r_0)))) & (p(s(ty_2Emin_2Ebool,V1q_0)) | (p(s(ty_2Emin_2Ebool,V2r_0)) | ~ (p(s(ty_2Emin_2Ebool,V0p_0))))))))).
fof(thm_2EsatTheory_2Edc__neg_2E0, axiom, ![V0p_0, V1q_0]: ((p(s(ty_2Emin_2Ebool,V0p_0)) <=> ~ (p(s(ty_2Emin_2Ebool,V1q_0)))) <=> ((p(s(ty_2Emin_2Ebool,V0p_0)) | p(s(ty_2Emin_2Ebool,V1q_0))) & (~ (p(s(ty_2Emin_2Ebool,V1q_0))) | ~ (p(s(ty_2Emin_2Ebool,V0p_0))))))).
fof(reserved_2Ecj__def0, axiom, ![V0f_0, V1g_0, V3x_0]: s(ty_2Erealax_2Ereal,c2_2Erealax_2Ereal__mul(s(ty_2Erealax_2Ereal,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V0f_0),s(ty_2Erealax_2Ereal,V3x_0))),s(ty_2Erealax_2Ereal,c2_2Ebool_2ELET(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V1g_0),s(ty_2Erealax_2Ereal,V3x_0))))) = s(ty_2Erealax_2Ereal,f4638_0_3(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V0f_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V1g_0),s(ty_2Erealax_2Ereal,V3x_0)))).
fof(conjecture, conjecture, ![V0f_0, V1g_0, V2s_0]: ((p(s(ty_2Emin_2Ebool,c2_2Ereal__topology_2Euniformly__continuous__on(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V0f_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),V2s_0)))) & (p(s(ty_2Emin_2Ebool,c2_2Ereal__topology_2Euniformly__continuous__on(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V1g_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),V2s_0)))) & (p(s(ty_2Emin_2Ebool,c1_2Ereal__topology_2Ebounded__def(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),c2_2Epred__set_2EIMAGE(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V0f_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),V2s_0)))))) & p(s(ty_2Emin_2Ebool,c1_2Ereal__topology_2Ebounded__def(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),c2_2Epred__set_2EIMAGE(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V1g_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),V2s_0))))))))) => p(s(ty_2Emin_2Ebool,c2_2Ereal__topology_2Euniformly__continuous__on(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),f4638_0_2(s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V0f_0),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V1g_0))),s(ty_2Emin_2Efun(ty_2Erealax_2Ereal,ty_2Emin_2Ebool),V2s_0)))))).