:: REAL_LAT semantic presentation begin definitionfunc :::"minreal"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: REAL_LAT:def 1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_square_1 :::"min"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))); func :::"maxreal"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: REAL_LAT:def 2 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_square_1 :::"max"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))); end; :: deftheorem defines :::"minreal"::: REAL_LAT:def 1 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_real_lat :::"minreal"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "b1")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_square_1 :::"min"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))) ")" )); :: deftheorem defines :::"maxreal"::: REAL_LAT:def 2 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k2_real_lat :::"maxreal"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "b1")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_square_1 :::"max"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))) ")" )); definitionfunc :::"Real_Lattice"::: -> ($#v3_lattices :::"strict"::: ) ($#l3_lattices :::"LattStr"::: ) equals :: REAL_LAT:def 3 (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k2_real_lat :::"maxreal"::: ) ) "," (Set ($#k1_real_lat :::"minreal"::: ) ) "#)" ); end; :: deftheorem defines :::"Real_Lattice"::: REAL_LAT:def 3 : (Bool (Set ($#k3_real_lat :::"Real_Lattice"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k2_real_lat :::"maxreal"::: ) ) "," (Set ($#k1_real_lat :::"minreal"::: ) ) "#)" )); registration cluster (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k3_real_lat :::"Real_Lattice"::: ) )) -> ($#v3_membered :::"real-membered"::: ) ; end; registration cluster (Set ($#k3_real_lat :::"Real_Lattice"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattices :::"strict"::: ) ; end; registrationlet "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_real_lat :::"Real_Lattice"::: ) ); identify ; identify ; end; registration cluster (Set ($#k3_real_lat :::"Real_Lattice"::: ) ) -> ($#v3_lattices :::"strict"::: ) ($#v10_lattices :::"Lattice-like"::: ) ; end; theorem :: REAL_LAT:1 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_real_lat :::"Real_Lattice"::: ) ) "holds" (Bool (Set (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" ))) ; theorem :: REAL_LAT:2 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_real_lat :::"Real_Lattice"::: ) ) "holds" (Bool (Set (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" ))) ; theorem :: REAL_LAT:3 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_real_lat :::"Real_Lattice"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) "," (Set (Var "p")) ")" )) & (Bool (Set (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) "," (Set (Var "r")) ")" )) & (Bool (Set (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "r")) ")" )) & (Bool (Set (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "q")) ")" )) & (Bool (Set (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set (Var "q")) ")" ")" ) "," (Set (Var "p")) ")" )) & (Bool (Set (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ")" ) "," (Set (Var "q")) ")" )) ")" )) ; theorem :: REAL_LAT:4 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_real_lat :::"Real_Lattice"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) "," (Set (Var "p")) ")" )) & (Bool (Set (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) "," (Set (Var "r")) ")" )) & (Bool (Set (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "r")) ")" )) & (Bool (Set (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "q")) ")" )) & (Bool (Set (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set (Var "q")) ")" ")" ) "," (Set (Var "p")) ")" )) & (Bool (Set (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ")" ) "," (Set (Var "q")) ")" )) ")" )) ; theorem :: REAL_LAT:5 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_real_lat :::"Real_Lattice"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set "(" (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set "(" (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" )) ; theorem :: REAL_LAT:6 (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_real_lat :::"Real_Lattice"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set "(" (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set "(" (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" )) ; theorem :: REAL_LAT:7 (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_real_lat :::"Real_Lattice"::: ) ) "holds" (Bool (Set (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set "(" (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" ")" ) "," (Set "(" (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ))) ; registration cluster (Set ($#k3_real_lat :::"Real_Lattice"::: ) ) -> ($#v3_lattices :::"strict"::: ) ($#v11_lattices :::"distributive"::: ) ; end; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"maxfuncreal"::: "A" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) means :: REAL_LAT:def 4 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set it ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k3_funcsdom :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ))); func :::"minfuncreal"::: "A" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) means :: REAL_LAT:def 5 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set it ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k3_funcsdom :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ))); end; :: deftheorem defines :::"maxfuncreal"::: REAL_LAT:def 4 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set ($#k2_real_lat :::"maxreal"::: ) ) ($#k3_funcsdom :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ))) ")" ))); :: deftheorem defines :::"minfuncreal"::: REAL_LAT:def 5 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set ($#k1_real_lat :::"minreal"::: ) ) ($#k3_funcsdom :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ))) ")" ))); theorem :: REAL_LAT:8 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "f")) ")" )))) ; theorem :: REAL_LAT:9 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "f")) ")" )))) ; theorem :: REAL_LAT:10 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) "," (Set (Var "h")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "h")) ")" ")" ) ")" )))) ; theorem :: REAL_LAT:11 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) "," (Set (Var "h")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "h")) ")" ")" ) ")" )))) ; theorem :: REAL_LAT:12 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))))) ; theorem :: REAL_LAT:13 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) "," (Set (Var "f")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))))) ; theorem :: REAL_LAT:14 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "f")) ")" ")" ) "," (Set (Var "f")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))))) ; theorem :: REAL_LAT:15 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "f")) ")" ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))))) ; theorem :: REAL_LAT:16 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))))) ; theorem :: REAL_LAT:17 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "f")) ")" ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))))) ; theorem :: REAL_LAT:18 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "f")) ")" ")" ) "," (Set (Var "f")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))))) ; theorem :: REAL_LAT:19 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) "," (Set (Var "f")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))))) ; theorem :: REAL_LAT:20 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "h")) ")" ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) "," (Set "(" (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ")" )))) ; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"RealFunc_Lattice"::: "A" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattices :::"strict"::: ) ($#l3_lattices :::"LattStr"::: ) equals :: REAL_LAT:def 6 (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) "," (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) "A" ")" ) "," (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) "A" ")" ) "#)" ); end; :: deftheorem defines :::"RealFunc_Lattice"::: REAL_LAT:def 6 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_real_lat :::"RealFunc_Lattice"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) "," (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) "#)" ))); registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k6_real_lat :::"RealFunc_Lattice"::: ) "A") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v7_lattices :::"meet-associative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) for ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) ; end; theorem :: REAL_LAT:21 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k6_real_lat :::"RealFunc_Lattice"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" )))) ; theorem :: REAL_LAT:22 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k6_real_lat :::"RealFunc_Lattice"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" )))) ; theorem :: REAL_LAT:23 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k6_real_lat :::"RealFunc_Lattice"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) "," (Set (Var "p")) ")" )) & (Bool (Set (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) "," (Set (Var "r")) ")" )) & (Bool (Set (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "r")) ")" )) & (Bool (Set (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "q")) ")" )) & (Bool (Set (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set (Var "q")) ")" ")" ) "," (Set (Var "p")) ")" )) & (Bool (Set (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ")" ) "," (Set (Var "q")) ")" )) ")" ))) ; theorem :: REAL_LAT:24 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k6_real_lat :::"RealFunc_Lattice"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) "," (Set (Var "p")) ")" )) & (Bool (Set (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) "," (Set (Var "r")) ")" )) & (Bool (Set (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "r")) ")" )) & (Bool (Set (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "q")) ")" )) & (Bool (Set (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set (Var "q")) ")" ")" ) "," (Set (Var "p")) ")" )) & (Bool (Set (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set "(" (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ")" ) "," (Set (Var "q")) ")" )) ")" ))) ; theorem :: REAL_LAT:25 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k6_real_lat :::"RealFunc_Lattice"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set "(" (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set "(" (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" ))) ; theorem :: REAL_LAT:26 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k6_real_lat :::"RealFunc_Lattice"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set "(" (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set "(" (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" ))) ; theorem :: REAL_LAT:27 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k6_real_lat :::"RealFunc_Lattice"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set "(" (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_real_lat :::"maxfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" ")" ) "," (Set "(" (Set "(" ($#k5_real_lat :::"minfuncreal"::: ) (Set (Var "A")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" ) ")" )))) ; theorem :: REAL_LAT:28 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_real_lat :::"RealFunc_Lattice"::: ) (Set (Var "A"))) "is" ($#l3_lattices :::"D_Lattice":::))) ;