:: OSALG_2 semantic presentation begin theorem :: OSALG_2:1 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"OrderSortedSet":::) "of" (Set (Var "R")) "holds" (Bool (Set (Set (Var "X")) ($#k3_pboole :::"/\"::: ) (Set (Var "Y"))) "is" ($#m1_hidden :::"OrderSortedSet":::) "of" (Set (Var "R"))))) ; theorem :: OSALG_2:2 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"OrderSortedSet":::) "of" (Set (Var "R")) "holds" (Bool (Set (Set (Var "X")) ($#k2_pboole :::"\/"::: ) (Set (Var "Y"))) "is" ($#m1_hidden :::"OrderSortedSet":::) "of" (Set (Var "R"))))) ; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); let "M" be ($#m1_hidden :::"OrderSortedSet":::) "of" (Set (Const "R")); mode :::"OrderSortedSubset"::: "of" "M" -> ($#m3_pboole :::"ManySortedSubset"::: ) "of" "M" means :: OSALG_2:def 1 (Bool it "is" ($#m1_hidden :::"OrderSortedSet":::) "of" "R"); end; :: deftheorem defines :::"OrderSortedSubset"::: OSALG_2:def 1 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"OrderSortedSet":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "b3")) "being" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_osalg_2 :::"OrderSortedSubset"::: ) "of" (Set (Var "M"))) "iff" (Bool (Set (Var "b3")) "is" ($#m1_hidden :::"OrderSortedSet":::) "of" (Set (Var "R"))) ")" )))); registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); let "M" be bbbadV2_RELAT_1() ($#m1_hidden :::"OrderSortedSet":::) "of" (Set (Const "R")); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) bbbadV2_RELAT_1() (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R")) for ($#m1_osalg_2 :::"OrderSortedSubset"::: ) "of" "M"; end; begin definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "U0" be ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S")); mode :::"OSSubset"::: "of" "U0" -> ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "U0") means :: OSALG_2:def 2 (Bool it "is" ($#m1_hidden :::"OrderSortedSet":::) "of" "S"); end; :: deftheorem defines :::"OSSubset"::: OSALG_2:def 2 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b3")) "being" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U0"))) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "U0"))) "iff" (Bool (Set (Var "b3")) "is" ($#m1_hidden :::"OrderSortedSet":::) "of" (Set (Var "S"))) ")" )))); registrationlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); cluster ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v12_osalg_1 :::"order-sorted"::: ) ($#v13_osalg_1 :::"monotone"::: ) for ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S"; end; registrationlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "U0" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S")); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) bbbadV2_RELAT_1() (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S")) for ($#m2_osalg_2 :::"OSSubset"::: ) "of" "U0"; end; theorem :: OSALG_2:3 (Bool "for" (Set (Var "S0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v2_msualg_2 :::"all-with_const_op"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool (Set ($#k1_osalg_1 :::"OSSign"::: ) (Set (Var "S0"))) "is" ($#v2_msualg_2 :::"all-with_const_op"::: ) )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) bbbadV14_STRUCT_0() ($#v2_msualg_2 :::"all-with_const_op"::: ) bbbadV3_ORDERS_2() bbbadV4_ORDERS_2() bbbadV5_ORDERS_2() ($#v3_osalg_1 :::"strict"::: ) ($#v4_osalg_1 :::"order-sorted"::: ) ($#v5_osalg_1 :::"discernable"::: ) for ($#l3_osalg_1 :::"OverloadedRSSign"::: ) ; end; begin theorem :: OSALG_2:4 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U0"))) "," (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "U0"))) "#)" ) "is" ($#v12_osalg_1 :::"order-sorted"::: ) ))) ; registrationlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "U0" be ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S")); cluster ($#v12_osalg_1 :::"order-sorted"::: ) for ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" "U0"; end; definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "U0" be ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S")); mode OSSubAlgebra of "U0" is ($#v12_osalg_1 :::"order-sorted"::: ) ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" "U0"; end; registrationlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "U0" be ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S")); cluster ($#v3_msualg_1 :::"strict"::: ) ($#v12_osalg_1 :::"order-sorted"::: ) for ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" "U0"; end; registrationlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "U0" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S")); cluster ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v12_osalg_1 :::"order-sorted"::: ) for ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" "U0"; end; theorem :: OSALG_2:5 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "U1")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "U1")) "is" ($#m1_msualg_2 :::"OSSubAlgebra":::) "of" (Set (Var "U0"))) "iff" (Bool "(" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U1"))) "is" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "U0"))) & (Bool "(" "for" (Set (Var "B")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "U0")) "st" (Bool (Bool (Set (Var "B")) ($#r8_pboole :::"="::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U1"))))) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#v3_msualg_2 :::"opers_closed"::: ) ) & (Bool (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "U1"))) ($#r8_pboole :::"="::: ) (Set ($#k4_msualg_2 :::"Opers"::: ) "(" (Set (Var "U0")) "," (Set (Var "B")) ")" )) ")" ) ")" ) ")" ) ")" )))) ; definitionlet "S1" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "OU0" be ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")); let "s" be ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "S1")); func :::"OSConstants"::: "(" "OU0" "," "s" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "OU0") ($#k1_funct_1 :::"."::: ) "s" ")" ) equals :: OSALG_2:def 3 (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k1_msualg_2 :::"Constants"::: ) "(" "OU0" "," (Set (Var "s2")) ")" ")" ) where s2 "is" ($#m1_subset_1 :::"SortSymbol":::) "of" "S1" : (Bool (Set (Var "s2")) ($#r3_orders_2 :::"<="::: ) "s") "}" ); end; :: deftheorem defines :::"OSConstants"::: OSALG_2:def 3 : (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S1")) "holds" (Bool (Set ($#k1_osalg_2 :::"OSConstants"::: ) "(" (Set (Var "OU0")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k1_msualg_2 :::"Constants"::: ) "(" (Set (Var "OU0")) "," (Set (Var "s2")) ")" ")" ) where s2 "is" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S1")) : (Bool (Set (Var "s2")) ($#r3_orders_2 :::"<="::: ) (Set (Var "s"))) "}" ))))); theorem :: OSALG_2:6 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S1")) "holds" (Bool (Set ($#k1_msualg_2 :::"Constants"::: ) "(" (Set (Var "OU0")) "," (Set (Var "s")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k1_osalg_2 :::"OSConstants"::: ) "(" (Set (Var "OU0")) "," (Set (Var "s")) ")" ))))) ; definitionlet "S1" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S1"))); func :::"OSCl"::: "M" -> ($#m1_hidden :::"OrderSortedSet":::) "of" "S1" means :: OSALG_2:def 4 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" "S1" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" "M" ($#k1_funct_1 :::"."::: ) (Set (Var "s1")) ")" ) where s1 "is" ($#m1_subset_1 :::"SortSymbol":::) "of" "S1" : (Bool (Set (Var "s1")) ($#r3_orders_2 :::"<="::: ) (Set (Var "s"))) "}" ))); end; :: deftheorem defines :::"OSCl"::: OSALG_2:def 4 : (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"OrderSortedSet":::) "of" (Set (Var "S1")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_osalg_2 :::"OSCl"::: ) (Set (Var "M")))) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S1")) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set (Var "s1")) ")" ) where s1 "is" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S1")) : (Bool (Set (Var "s1")) ($#r3_orders_2 :::"<="::: ) (Set (Var "s"))) "}" ))) ")" )))); theorem :: OSALG_2:7 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))) "holds" (Bool (Set (Var "M")) ($#r2_pboole :::"c="::: ) (Set ($#k2_osalg_2 :::"OSCl"::: ) (Set (Var "M")))))) ; theorem :: OSALG_2:8 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"OrderSortedSet":::) "of" (Set (Var "S1")) "st" (Bool (Bool (Set (Var "M")) ($#r2_pboole :::"c="::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k2_osalg_2 :::"OSCl"::: ) (Set (Var "M"))) ($#r2_pboole :::"c="::: ) (Set (Var "A")))))) ; theorem :: OSALG_2:9 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"OrderSortedSet":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k2_osalg_2 :::"OSCl"::: ) (Set (Var "X"))) ($#r8_pboole :::"="::: ) (Set (Var "X"))))) ; definitionlet "S1" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "OU0" be ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")); func :::"OSConstants"::: "OU0" -> ($#m2_osalg_2 :::"OSSubset"::: ) "of" "OU0" means :: OSALG_2:def 5 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" "S1" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k1_osalg_2 :::"OSConstants"::: ) "(" "OU0" "," (Set (Var "s")) ")" ))); end; :: deftheorem defines :::"OSConstants"::: OSALG_2:def 5 : (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "b3")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU0")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_osalg_2 :::"OSConstants"::: ) (Set (Var "OU0")))) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S1")) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k1_osalg_2 :::"OSConstants"::: ) "(" (Set (Var "OU0")) "," (Set (Var "s")) ")" ))) ")" )))); theorem :: OSALG_2:10 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) "holds" (Bool (Set ($#k2_msualg_2 :::"Constants"::: ) (Set (Var "OU0"))) ($#r2_pboole :::"c="::: ) (Set ($#k3_osalg_2 :::"OSConstants"::: ) (Set (Var "OU0")))))) ; theorem :: OSALG_2:11 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU0")) "st" (Bool (Bool (Set ($#k2_msualg_2 :::"Constants"::: ) (Set (Var "OU0"))) ($#r2_pboole :::"c="::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k3_osalg_2 :::"OSConstants"::: ) (Set (Var "OU0"))) ($#r2_pboole :::"c="::: ) (Set (Var "A")))))) ; theorem :: OSALG_2:12 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU0")) "holds" (Bool (Set ($#k3_osalg_2 :::"OSConstants"::: ) (Set (Var "OU0"))) ($#r8_pboole :::"="::: ) (Set ($#k2_osalg_2 :::"OSCl"::: ) (Set "(" ($#k2_msualg_2 :::"Constants"::: ) (Set (Var "OU0")) ")" )))))) ; theorem :: OSALG_2:13 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "OU1")) "being" ($#m1_msualg_2 :::"OSSubAlgebra":::) "of" (Set (Var "OU0")) "holds" (Bool (Set ($#k3_osalg_2 :::"OSConstants"::: ) (Set (Var "OU0"))) "is" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU1")))))) ; theorem :: OSALG_2:14 (Bool "for" (Set (Var "S")) "being" ($#v2_msualg_2 :::"all-with_const_op"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "OU1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#m1_msualg_2 :::"OSSubAlgebra":::) "of" (Set (Var "OU0")) "holds" (Bool (Set ($#k3_osalg_2 :::"OSConstants"::: ) (Set (Var "OU0"))) "is" bbbadV2_RELAT_1() ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU1")))))) ; begin theorem :: OSALG_2:15 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "M"))) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k1_mboolean :::"bool"::: ) (Set (Var "M")) ")" ))) ")" )))) ; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); let "M" be ($#m1_hidden :::"OrderSortedSet":::) "of" (Set (Const "R")); func :::"OSbool"::: "M" -> ($#m1_hidden :::"set"::: ) means :: OSALG_2:def 6 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) "is" ($#m1_osalg_2 :::"OrderSortedSubset"::: ) "of" "M") ")" )); end; :: deftheorem defines :::"OSbool"::: OSALG_2:def 6 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"OrderSortedSet":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_osalg_2 :::"OSbool"::: ) (Set (Var "M")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool (Set (Var "x")) "is" ($#m1_osalg_2 :::"OrderSortedSubset"::: ) "of" (Set (Var "M"))) ")" )) ")" )))); definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "U0" be ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S")); let "A" be ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Const "U0")); func :::"OSSubSort"::: "A" -> ($#m1_hidden :::"set"::: ) equals :: OSALG_2:def 7 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_msualg_2 :::"SubSort"::: ) "A") : (Bool (Set (Var "x")) "is" ($#m1_hidden :::"OrderSortedSet":::) "of" "S") "}" ; end; :: deftheorem defines :::"OSSubSort"::: OSALG_2:def 7 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "A")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "U0")) "holds" (Bool (Set ($#k5_osalg_2 :::"OSSubSort"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_msualg_2 :::"SubSort"::: ) (Set (Var "A"))) : (Bool (Set (Var "x")) "is" ($#m1_hidden :::"OrderSortedSet":::) "of" (Set (Var "S"))) "}" )))); theorem :: OSALG_2:16 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU0")) "holds" (Bool (Set ($#k5_osalg_2 :::"OSSubSort"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_msualg_2 :::"SubSort"::: ) (Set (Var "A"))))))) ; theorem :: OSALG_2:17 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU0")) "holds" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "OU0"))) ($#r2_hidden :::"in"::: ) (Set ($#k5_osalg_2 :::"OSSubSort"::: ) (Set (Var "A"))))))) ; registrationlet "S1" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "OU0" be ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")); let "A" be ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Const "OU0")); cluster (Set ($#k5_osalg_2 :::"OSSubSort"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "S1" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "OU0" be ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")); func :::"OSSubSort"::: "OU0" -> ($#m1_hidden :::"set"::: ) equals :: OSALG_2:def 8 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_msualg_2 :::"SubSort"::: ) "OU0") : (Bool (Set (Var "x")) "is" ($#m1_hidden :::"OrderSortedSet":::) "of" "S1") "}" ; end; :: deftheorem defines :::"OSSubSort"::: OSALG_2:def 8 : (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) "holds" (Bool (Set ($#k6_osalg_2 :::"OSSubSort"::: ) (Set (Var "OU0"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_msualg_2 :::"SubSort"::: ) (Set (Var "OU0"))) : (Bool (Set (Var "x")) "is" ($#m1_hidden :::"OrderSortedSet":::) "of" (Set (Var "S1"))) "}" ))); theorem :: OSALG_2:18 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU0")) "holds" (Bool (Set ($#k5_osalg_2 :::"OSSubSort"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k6_osalg_2 :::"OSSubSort"::: ) (Set (Var "OU0"))))))) ; registrationlet "S1" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "OU0" be ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")); cluster (Set ($#k6_osalg_2 :::"OSSubSort"::: ) "OU0") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "S1" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "OU0" be ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")); let "e" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_osalg_2 :::"OSSubSort"::: ) (Set (Const "OU0"))); func :::"@"::: "e" -> ($#m2_osalg_2 :::"OSSubset"::: ) "of" "OU0" equals :: OSALG_2:def 9 "e"; end; :: deftheorem defines :::"@"::: OSALG_2:def 9 : (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_osalg_2 :::"OSSubSort"::: ) (Set (Var "OU0"))) "holds" (Bool (Set ($#k7_osalg_2 :::"@"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "e")))))); theorem :: OSALG_2:19 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU0")) "holds" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set ($#k5_osalg_2 :::"OSSubSort"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool (Set (Var "B")) "is" ($#v3_msualg_2 :::"opers_closed"::: ) ) & (Bool (Set ($#k3_osalg_2 :::"OSConstants"::: ) (Set (Var "OU0"))) ($#r2_pboole :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r2_pboole :::"c="::: ) (Set (Var "B"))) ")" ) ")" )))) ; theorem :: OSALG_2:20 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "B")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU0")) "holds" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set ($#k6_osalg_2 :::"OSSubSort"::: ) (Set (Var "OU0")))) "iff" (Bool (Set (Var "B")) "is" ($#v3_msualg_2 :::"opers_closed"::: ) ) ")" )))) ; definitionlet "S1" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "OU0" be ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")); let "A" be ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Const "OU0")); let "s" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S1")); func :::"OSSubSort"::: "(" "A" "," "s" ")" -> ($#m1_hidden :::"set"::: ) means :: OSALG_2:def 10 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" "OU0" "st" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set ($#k5_osalg_2 :::"OSSubSort"::: ) "A")) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k1_funct_1 :::"."::: ) "s")) ")" )) ")" )); end; :: deftheorem defines :::"OSSubSort"::: OSALG_2:def 10 : (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU0")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "b5")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k8_osalg_2 :::"OSSubSort"::: ) "(" (Set (Var "A")) "," (Set (Var "s")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b5"))) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU0")) "st" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set ($#k5_osalg_2 :::"OSSubSort"::: ) (Set (Var "A")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) ")" )) ")" )) ")" )))))); theorem :: OSALG_2:21 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU0")) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S1")) "st" (Bool (Bool (Set (Var "s1")) ($#r3_orders_2 :::"<="::: ) (Set (Var "s2")))) "holds" (Bool (Set ($#k8_osalg_2 :::"OSSubSort"::: ) "(" (Set (Var "A")) "," (Set (Var "s2")) ")" ) ($#r2_setfam_1 :::"is_coarser_than"::: ) (Set ($#k8_osalg_2 :::"OSSubSort"::: ) "(" (Set (Var "A")) "," (Set (Var "s1")) ")" )))))) ; theorem :: OSALG_2:22 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU0")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S1")) "holds" (Bool (Set ($#k8_osalg_2 :::"OSSubSort"::: ) "(" (Set (Var "A")) "," (Set (Var "s")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k8_msualg_2 :::"SubSort"::: ) "(" (Set (Var "A")) "," (Set (Var "s")) ")" )))))) ; theorem :: OSALG_2:23 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU0")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S1")) "holds" (Bool (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "OU0"))) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r2_hidden :::"in"::: ) (Set ($#k8_osalg_2 :::"OSSubSort"::: ) "(" (Set (Var "A")) "," (Set (Var "s")) ")" )))))) ; registrationlet "S1" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "OU0" be ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")); let "A" be ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Const "OU0")); let "s" be ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "S1")); cluster (Set ($#k8_osalg_2 :::"OSSubSort"::: ) "(" "A" "," "s" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "S1" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "OU0" be ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")); let "A" be ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Const "OU0")); func :::"OSMSubSort"::: "A" -> ($#m2_osalg_2 :::"OSSubset"::: ) "of" "OU0" means :: OSALG_2:def 11 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" "S1" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) (Set "(" ($#k8_osalg_2 :::"OSSubSort"::: ) "(" "A" "," (Set (Var "s")) ")" ")" )))); end; :: deftheorem defines :::"OSMSubSort"::: OSALG_2:def 11 : (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A")) "," (Set (Var "b4")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU0")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k9_osalg_2 :::"OSMSubSort"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S1")) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) (Set "(" ($#k8_osalg_2 :::"OSSubSort"::: ) "(" (Set (Var "A")) "," (Set (Var "s")) ")" ")" )))) ")" )))); registrationlet "S1" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "OU0" be ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S1") ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S1")) ($#v3_msualg_2 :::"opers_closed"::: ) for ($#m2_osalg_2 :::"OSSubset"::: ) "of" "OU0"; end; theorem :: OSALG_2:24 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU0")) "holds" (Bool (Set (Set "(" ($#k3_osalg_2 :::"OSConstants"::: ) (Set (Var "OU0")) ")" ) ($#k2_pboole :::"\/"::: ) (Set (Var "A"))) ($#r2_pboole :::"c="::: ) (Set ($#k9_osalg_2 :::"OSMSubSort"::: ) (Set (Var "A"))))))) ; theorem :: OSALG_2:25 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU0")) "st" (Bool (Bool (Set (Set "(" ($#k3_osalg_2 :::"OSConstants"::: ) (Set (Var "OU0")) ")" ) ($#k2_pboole :::"\/"::: ) (Set (Var "A"))) "is" bbbadV2_RELAT_1())) "holds" (Bool (Set ($#k9_osalg_2 :::"OSMSubSort"::: ) (Set (Var "A"))) "is" bbbadV2_RELAT_1())))) ; theorem :: OSALG_2:26 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU0")) "st" (Bool (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set ($#k5_osalg_2 :::"OSSubSort"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" ($#k9_osalg_2 :::"OSMSubSort"::: ) (Set (Var "A")) ")" ) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S1"))) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "o"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" (Set (Var "B")) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S1"))) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "o")))))))) ; theorem :: OSALG_2:27 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU0")) "st" (Bool (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set ($#k5_osalg_2 :::"OSSubSort"::: ) (Set (Var "A"))))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set (Var "OU0")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" (Set "(" (Set "(" ($#k9_osalg_2 :::"OSMSubSort"::: ) (Set (Var "A")) ")" ) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S1"))) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "o")) ")" ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "B")) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S1"))) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "o")))))))) ; theorem :: OSALG_2:28 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU0")) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set (Var "OU0")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" (Set "(" (Set "(" ($#k9_osalg_2 :::"OSMSubSort"::: ) (Set (Var "A")) ")" ) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S1"))) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "o")) ")" ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k9_osalg_2 :::"OSMSubSort"::: ) (Set (Var "A")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S1"))) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "o")))))))) ; theorem :: OSALG_2:29 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU0")) "holds" (Bool "(" (Bool (Set ($#k9_osalg_2 :::"OSMSubSort"::: ) (Set (Var "A"))) "is" ($#v3_msualg_2 :::"opers_closed"::: ) ) & (Bool (Set (Var "A")) ($#r2_pboole :::"c="::: ) (Set ($#k9_osalg_2 :::"OSMSubSort"::: ) (Set (Var "A")))) ")" )))) ; registrationlet "S1" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "OU0" be ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")); let "A" be ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Const "OU0")); cluster (Set ($#k9_osalg_2 :::"OSMSubSort"::: ) "A") -> ($#v3_msualg_2 :::"opers_closed"::: ) ; end; begin registrationlet "S1" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "OU0" be ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")); let "A" be ($#v3_msualg_2 :::"opers_closed"::: ) ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Const "OU0")); cluster (Set "OU0" ($#k10_msualg_2 :::"|"::: ) "A") -> ($#v12_osalg_1 :::"order-sorted"::: ) ; end; registrationlet "S1" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "OU0" be ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")); let "OU1", "OU2" be ($#m1_msualg_2 :::"OSSubAlgebra":::) "of" (Set (Const "OU0")); cluster (Set "OU1" ($#k11_msualg_2 :::"/\"::: ) "OU2") -> ($#v12_osalg_1 :::"order-sorted"::: ) ; end; definitionlet "S1" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "OU0" be ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")); let "A" be ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Const "OU0")); func :::"GenOSAlg"::: "A" -> ($#v3_msualg_1 :::"strict"::: ) ($#m1_msualg_2 :::"OSSubAlgebra":::) "of" "OU0" means :: OSALG_2:def 12 (Bool "(" (Bool "A" "is" ($#m2_osalg_2 :::"OSSubset"::: ) "of" it) & (Bool "(" "for" (Set (Var "OU1")) "being" ($#m1_msualg_2 :::"OSSubAlgebra":::) "of" "OU0" "st" (Bool (Bool "A" "is" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU1")))) "holds" (Bool it "is" ($#m1_msualg_2 :::"OSSubAlgebra":::) "of" (Set (Var "OU1"))) ")" ) ")" ); end; :: deftheorem defines :::"GenOSAlg"::: OSALG_2:def 12 : (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU0")) (Bool "for" (Set (Var "b4")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#m1_msualg_2 :::"OSSubAlgebra":::) "of" (Set (Var "OU0")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k10_osalg_2 :::"GenOSAlg"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool (Set (Var "A")) "is" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "b4"))) & (Bool "(" "for" (Set (Var "OU1")) "being" ($#m1_msualg_2 :::"OSSubAlgebra":::) "of" (Set (Var "OU0")) "st" (Bool (Bool (Set (Var "A")) "is" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU1")))) "holds" (Bool (Set (Var "b4")) "is" ($#m1_msualg_2 :::"OSSubAlgebra":::) "of" (Set (Var "OU1"))) ")" ) ")" ) ")" ))))); theorem :: OSALG_2:30 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU0")) "holds" (Bool "(" (Bool (Set ($#k10_osalg_2 :::"GenOSAlg"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "OU0")) ($#k10_msualg_2 :::"|"::: ) (Set "(" ($#k9_osalg_2 :::"OSMSubSort"::: ) (Set (Var "A")) ")" ))) & (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k10_osalg_2 :::"GenOSAlg"::: ) (Set (Var "A")) ")" )) ($#r8_pboole :::"="::: ) (Set ($#k9_osalg_2 :::"OSMSubSort"::: ) (Set (Var "A")))) ")" )))) ; theorem :: OSALG_2:31 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U0")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "A")) "being" ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "U0")) "holds" (Bool "(" (Bool (Set ($#k12_msualg_2 :::"GenMSAlg"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "U0")) ($#k10_msualg_2 :::"|"::: ) (Set "(" ($#k9_msualg_2 :::"MSSubSort"::: ) (Set (Var "A")) ")" ))) & (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k12_msualg_2 :::"GenMSAlg"::: ) (Set (Var "A")) ")" )) ($#r8_pboole :::"="::: ) (Set ($#k9_msualg_2 :::"MSSubSort"::: ) (Set (Var "A")))) ")" )))) ; theorem :: OSALG_2:32 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU0")) "holds" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k12_msualg_2 :::"GenMSAlg"::: ) (Set (Var "A")) ")" )) ($#r2_pboole :::"c="::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k10_osalg_2 :::"GenOSAlg"::: ) (Set (Var "A")) ")" )))))) ; theorem :: OSALG_2:33 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "A")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU0")) "holds" (Bool (Set ($#k12_msualg_2 :::"GenMSAlg"::: ) (Set (Var "A"))) "is" ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set ($#k10_osalg_2 :::"GenOSAlg"::: ) (Set (Var "A"))))))) ; theorem :: OSALG_2:34 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "B")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU0")) "st" (Bool (Bool (Set (Var "B")) ($#r8_pboole :::"="::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "OU0"))))) "holds" (Bool (Set ($#k10_osalg_2 :::"GenOSAlg"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "OU0")))))) ; theorem :: OSALG_2:35 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "OU1")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#m1_msualg_2 :::"OSSubAlgebra":::) "of" (Set (Var "OU0")) (Bool "for" (Set (Var "B")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "OU0")) "st" (Bool (Bool (Set (Var "B")) ($#r8_pboole :::"="::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "OU1"))))) "holds" (Bool (Set ($#k10_osalg_2 :::"GenOSAlg"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "OU1"))))))) ; theorem :: OSALG_2:36 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U0")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "U1")) "being" ($#m1_msualg_2 :::"OSSubAlgebra":::) "of" (Set (Var "U0")) "holds" (Bool (Set (Set "(" ($#k10_osalg_2 :::"GenOSAlg"::: ) (Set "(" ($#k3_osalg_2 :::"OSConstants"::: ) (Set (Var "U0")) ")" ) ")" ) ($#k11_msualg_2 :::"/\"::: ) (Set (Var "U1"))) ($#r1_hidden :::"="::: ) (Set ($#k10_osalg_2 :::"GenOSAlg"::: ) (Set "(" ($#k3_osalg_2 :::"OSConstants"::: ) (Set (Var "U0")) ")" )))))) ; definitionlet "S1" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "U0" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")); let "U1", "U2" be ($#m1_msualg_2 :::"OSSubAlgebra":::) "of" (Set (Const "U0")); func "U1" :::""\/"_os"::: "U2" -> ($#v3_msualg_1 :::"strict"::: ) ($#m1_msualg_2 :::"OSSubAlgebra":::) "of" "U0" means :: OSALG_2:def 13 (Bool "for" (Set (Var "A")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" "U0" "st" (Bool (Bool (Set (Var "A")) ($#r8_pboole :::"="::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "U1") ($#k2_pboole :::"\/"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "U2")))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k10_osalg_2 :::"GenOSAlg"::: ) (Set (Var "A"))))); end; :: deftheorem defines :::""\/"_os"::: OSALG_2:def 13 : (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U0")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#m1_msualg_2 :::"OSSubAlgebra":::) "of" (Set (Var "U0")) (Bool "for" (Set (Var "b5")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#m1_msualg_2 :::"OSSubAlgebra":::) "of" (Set (Var "U0")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "U1")) ($#k11_osalg_2 :::""\/"_os"::: ) (Set (Var "U2")))) "iff" (Bool "for" (Set (Var "A")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "U0")) "st" (Bool (Bool (Set (Var "A")) ($#r8_pboole :::"="::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U1"))) ($#k2_pboole :::"\/"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U2")))))) "holds" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k10_osalg_2 :::"GenOSAlg"::: ) (Set (Var "A"))))) ")" ))))); theorem :: OSALG_2:37 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U0")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "U1")) "being" ($#m1_msualg_2 :::"OSSubAlgebra":::) "of" (Set (Var "U0")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "U0")) "st" (Bool (Bool (Set (Var "B")) ($#r8_pboole :::"="::: ) (Set (Set (Var "A")) ($#k2_pboole :::"\/"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U1")))))) "holds" (Bool (Set (Set "(" ($#k10_osalg_2 :::"GenOSAlg"::: ) (Set (Var "A")) ")" ) ($#k11_osalg_2 :::""\/"_os"::: ) (Set (Var "U1"))) ($#r1_hidden :::"="::: ) (Set ($#k10_osalg_2 :::"GenOSAlg"::: ) (Set (Var "B")))))))) ; theorem :: OSALG_2:38 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U0")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "U1")) "being" ($#m1_msualg_2 :::"OSSubAlgebra":::) "of" (Set (Var "U0")) (Bool "for" (Set (Var "B")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "U0")) "st" (Bool (Bool (Set (Var "B")) ($#r8_pboole :::"="::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U0"))))) "holds" (Bool (Set (Set "(" ($#k10_osalg_2 :::"GenOSAlg"::: ) (Set (Var "B")) ")" ) ($#k11_osalg_2 :::""\/"_os"::: ) (Set (Var "U1"))) ($#r1_hidden :::"="::: ) (Set ($#k10_osalg_2 :::"GenOSAlg"::: ) (Set (Var "B")))))))) ; theorem :: OSALG_2:39 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U0")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#m1_msualg_2 :::"OSSubAlgebra":::) "of" (Set (Var "U0")) "holds" (Bool (Set (Set (Var "U1")) ($#k11_osalg_2 :::""\/"_os"::: ) (Set (Var "U2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "U2")) ($#k11_osalg_2 :::""\/"_os"::: ) (Set (Var "U1"))))))) ; theorem :: OSALG_2:40 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U0")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#m1_msualg_2 :::"OSSubAlgebra":::) "of" (Set (Var "U0")) "holds" (Bool (Set (Set (Var "U1")) ($#k11_msualg_2 :::"/\"::: ) (Set "(" (Set (Var "U1")) ($#k11_osalg_2 :::""\/"_os"::: ) (Set (Var "U2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "U1")))))) ; theorem :: OSALG_2:41 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U0")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#m1_msualg_2 :::"OSSubAlgebra":::) "of" (Set (Var "U0")) "holds" (Bool (Set (Set "(" (Set (Var "U1")) ($#k11_msualg_2 :::"/\"::: ) (Set (Var "U2")) ")" ) ($#k11_osalg_2 :::""\/"_os"::: ) (Set (Var "U2"))) ($#r1_hidden :::"="::: ) (Set (Var "U2")))))) ; begin definitionlet "S1" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "OU0" be ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")); func :::"OSSub"::: "OU0" -> ($#m1_hidden :::"set"::: ) means :: OSALG_2:def 14 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) "is" ($#v3_msualg_1 :::"strict"::: ) ($#m1_msualg_2 :::"OSSubAlgebra":::) "of" "OU0") ")" )); end; :: deftheorem defines :::"OSSub"::: OSALG_2:def 14 : (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k12_osalg_2 :::"OSSub"::: ) (Set (Var "OU0")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool (Set (Var "x")) "is" ($#v3_msualg_1 :::"strict"::: ) ($#m1_msualg_2 :::"OSSubAlgebra":::) "of" (Set (Var "OU0"))) ")" )) ")" )))); theorem :: OSALG_2:42 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "OU0")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) "holds" (Bool (Set ($#k12_osalg_2 :::"OSSub"::: ) (Set (Var "OU0"))) ($#r1_tarski :::"c="::: ) (Set ($#k14_msualg_2 :::"MSSub"::: ) (Set (Var "OU0")))))) ; registrationlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "U0" be ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S")); cluster (Set ($#k12_osalg_2 :::"OSSub"::: ) "U0") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "S1" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "OU0" be ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")); :: original: :::"OSSub"::: redefine func :::"OSSub"::: "OU0" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_msualg_2 :::"MSSub"::: ) "OU0" ")" ); end; definitionlet "S1" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "U0" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")); func :::"OSAlg_join"::: "U0" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k13_osalg_2 :::"OSSub"::: ) "U0" ")" ) means :: OSALG_2:def 15 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k13_osalg_2 :::"OSSub"::: ) "U0") (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#m1_msualg_2 :::"OSSubAlgebra":::) "of" "U0" "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "U1"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "U2")))) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "U1")) ($#k11_osalg_2 :::""\/"_os"::: ) (Set (Var "U2")))))); end; :: deftheorem defines :::"OSAlg_join"::: OSALG_2:def 15 : (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U0")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k13_osalg_2 :::"OSSub"::: ) (Set (Var "U0")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k14_osalg_2 :::"OSAlg_join"::: ) (Set (Var "U0")))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k13_osalg_2 :::"OSSub"::: ) (Set (Var "U0"))) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#m1_msualg_2 :::"OSSubAlgebra":::) "of" (Set (Var "U0")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "U1"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "U2")))) "holds" (Bool (Set (Set (Var "b3")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "U1")) ($#k11_osalg_2 :::""\/"_os"::: ) (Set (Var "U2")))))) ")" )))); definitionlet "S1" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "U0" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")); func :::"OSAlg_meet"::: "U0" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k13_osalg_2 :::"OSSub"::: ) "U0" ")" ) means :: OSALG_2:def 16 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k13_osalg_2 :::"OSSub"::: ) "U0") (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#m1_msualg_2 :::"OSSubAlgebra":::) "of" "U0" "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "U1"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "U2")))) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "U1")) ($#k11_msualg_2 :::"/\"::: ) (Set (Var "U2")))))); end; :: deftheorem defines :::"OSAlg_meet"::: OSALG_2:def 16 : (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U0")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k13_osalg_2 :::"OSSub"::: ) (Set (Var "U0")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k15_osalg_2 :::"OSAlg_meet"::: ) (Set (Var "U0")))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k13_osalg_2 :::"OSSub"::: ) (Set (Var "U0"))) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#m1_msualg_2 :::"OSSubAlgebra":::) "of" (Set (Var "U0")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "U1"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "U2")))) "holds" (Bool (Set (Set (Var "b3")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "U1")) ($#k11_msualg_2 :::"/\"::: ) (Set (Var "U2")))))) ")" )))); theorem :: OSALG_2:43 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U0")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k13_osalg_2 :::"OSSub"::: ) (Set (Var "U0"))) "holds" (Bool (Set (Set "(" ($#k15_osalg_2 :::"OSAlg_meet"::: ) (Set (Var "U0")) ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k16_msualg_2 :::"MSAlg_meet"::: ) (Set (Var "U0")) ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))))) ; theorem :: OSALG_2:44 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U0")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) "holds" (Bool (Set ($#k14_osalg_2 :::"OSAlg_join"::: ) (Set (Var "U0"))) "is" ($#v1_binop_1 :::"commutative"::: ) ))) ; theorem :: OSALG_2:45 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U0")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) "holds" (Bool (Set ($#k14_osalg_2 :::"OSAlg_join"::: ) (Set (Var "U0"))) "is" ($#v2_binop_1 :::"associative"::: ) ))) ; theorem :: OSALG_2:46 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U0")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) "holds" (Bool (Set ($#k15_osalg_2 :::"OSAlg_meet"::: ) (Set (Var "U0"))) "is" ($#v1_binop_1 :::"commutative"::: ) ))) ; theorem :: OSALG_2:47 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U0")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) "holds" (Bool (Set ($#k15_osalg_2 :::"OSAlg_meet"::: ) (Set (Var "U0"))) "is" ($#v2_binop_1 :::"associative"::: ) ))) ; definitionlet "S1" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "U0" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")); func :::"OSSubAlLattice"::: "U0" -> ($#v3_lattices :::"strict"::: ) ($#l3_lattices :::"Lattice":::) equals :: OSALG_2:def 17 (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k13_osalg_2 :::"OSSub"::: ) "U0" ")" ) "," (Set "(" ($#k14_osalg_2 :::"OSAlg_join"::: ) "U0" ")" ) "," (Set "(" ($#k15_osalg_2 :::"OSAlg_meet"::: ) "U0" ")" ) "#)" ); end; :: deftheorem defines :::"OSSubAlLattice"::: OSALG_2:def 17 : (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U0")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) "holds" (Bool (Set ($#k16_osalg_2 :::"OSSubAlLattice"::: ) (Set (Var "U0"))) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k13_osalg_2 :::"OSSub"::: ) (Set (Var "U0")) ")" ) "," (Set "(" ($#k14_osalg_2 :::"OSAlg_join"::: ) (Set (Var "U0")) ")" ) "," (Set "(" ($#k15_osalg_2 :::"OSAlg_meet"::: ) (Set (Var "U0")) ")" ) "#)" )))); theorem :: OSALG_2:48 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U0")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) "holds" (Bool (Set ($#k16_osalg_2 :::"OSSubAlLattice"::: ) (Set (Var "U0"))) "is" ($#v15_lattices :::"bounded"::: ) ))) ; registrationlet "S1" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "U0" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")); cluster (Set ($#k16_osalg_2 :::"OSSubAlLattice"::: ) "U0") -> ($#v3_lattices :::"strict"::: ) ($#v15_lattices :::"bounded"::: ) ; end; theorem :: OSALG_2:49 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U0")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) "holds" (Bool (Set ($#k5_lattices :::"Bottom"::: ) (Set "(" ($#k16_osalg_2 :::"OSSubAlLattice"::: ) (Set (Var "U0")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_osalg_2 :::"GenOSAlg"::: ) (Set "(" ($#k3_osalg_2 :::"OSConstants"::: ) (Set (Var "U0")) ")" ))))) ; theorem :: OSALG_2:50 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U0")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "B")) "being" ($#m2_osalg_2 :::"OSSubset"::: ) "of" (Set (Var "U0")) "st" (Bool (Bool (Set (Var "B")) ($#r8_pboole :::"="::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U0"))))) "holds" (Bool (Set ($#k6_lattices :::"Top"::: ) (Set "(" ($#k16_osalg_2 :::"OSSubAlLattice"::: ) (Set (Var "U0")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_osalg_2 :::"GenOSAlg"::: ) (Set (Var "B"))))))) ; theorem :: OSALG_2:51 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U0")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) "holds" (Bool (Set ($#k6_lattices :::"Top"::: ) (Set "(" ($#k16_osalg_2 :::"OSSubAlLattice"::: ) (Set (Var "U0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "U0"))))) ;