:: OSALG_3 semantic presentation begin definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); let "F" be ($#m1_hidden :::"ManySortedFunction":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "R"))); attr "F" is :::"order-sorted"::: means :: OSALG_3:def 1 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element":::) "of" "R" "st" (Bool (Bool (Set (Var "s1")) ($#r3_orders_2 :::"<="::: ) (Set (Var "s2")))) "holds" (Bool "for" (Set (Var "a1")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" "F" ($#k1_funct_1 :::"."::: ) (Set (Var "s1")) ")" )))) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" "F" ($#k1_funct_1 :::"."::: ) (Set (Var "s2")) ")" ))) & (Bool (Set (Set "(" "F" ($#k1_funct_1 :::"."::: ) (Set (Var "s1")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "F" ($#k1_funct_1 :::"."::: ) (Set (Var "s2")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a1")))) ")" ))); end; :: deftheorem defines :::"order-sorted"::: OSALG_3:def 1 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_osalg_3 :::"order-sorted"::: ) ) "iff" (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "s1")) ($#r3_orders_2 :::"<="::: ) (Set (Var "s2")))) "holds" (Bool "for" (Set (Var "a1")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "s1")) ")" )))) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "s2")) ")" ))) & (Bool (Set (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "s1")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "s2")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a1")))) ")" ))) ")" ))); theorem :: OSALG_3:1 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_osalg_3 :::"order-sorted"::: ) )) "holds" (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "s1")) ($#r3_orders_2 :::"<="::: ) (Set (Var "s2")))) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "s1")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "s2")) ")" ))) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "s1"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "s2")))) ")" )))) ; theorem :: OSALG_3:2 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"OrderSortedSet":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "B")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"OrderSortedSet":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_osalg_3 :::"order-sorted"::: ) ) "iff" (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "s1")) ($#r3_orders_2 :::"<="::: ) (Set (Var "s2")))) "holds" (Bool "for" (Set (Var "a1")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "s1"))))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k1_msualg_3 :::"."::: ) (Set (Var "s1")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k1_msualg_3 :::"."::: ) (Set (Var "s2")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a1")))))) ")" ))))) ; theorem :: OSALG_3:3 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_osalg_3 :::"order-sorted"::: ) )) "holds" (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "w1")) ($#r2_osalg_1 :::"<="::: ) (Set (Var "w2")))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "w1"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "F")) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "w2"))))))) ; theorem :: OSALG_3:4 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"OrderSortedSet":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k2_msualg_3 :::"id"::: ) (Set (Var "A"))) "is" ($#v1_osalg_3 :::"order-sorted"::: ) ))) ; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); let "A" be ($#m1_hidden :::"OrderSortedSet":::) "of" (Set (Const "R")); cluster (Set ($#k2_msualg_3 :::"id"::: ) "A") -> ($#v1_osalg_3 :::"order-sorted"::: ) ; end; theorem :: OSALG_3:5 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"OrderSortedSet":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"OrderSortedSet":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_osalg_3 :::"order-sorted"::: ) ) & (Bool (Set (Var "G")) "is" ($#v1_osalg_3 :::"order-sorted"::: ) )) "holds" (Bool (Set (Set (Var "G")) ($#k3_msualg_3 :::"**"::: ) (Set (Var "F"))) "is" ($#v1_osalg_3 :::"order-sorted"::: ) )))))) ; theorem :: OSALG_3:6 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"OrderSortedSet":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_msualg_3 :::""1-1""::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_msualg_3 :::""onto""::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_osalg_3 :::"order-sorted"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k4_msualg_3 :::""""::: ) ) "is" ($#v1_osalg_3 :::"order-sorted"::: ) )))) ; theorem :: OSALG_3:7 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"OrderSortedSet":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_osalg_3 :::"order-sorted"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k9_pboole :::".:.:"::: ) (Set (Var "A"))) "is" ($#m1_hidden :::"OrderSortedSet":::) "of" (Set (Var "R")))))) ; definitionlet "S1" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "U1", "U2" be ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")); pred "U1" "," "U2" :::"are_os_isomorphic"::: means :: OSALG_3:def 2 (Bool "ex" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" "U1" "," "U2" "st" (Bool "(" (Bool (Set (Var "F")) ($#r4_msualg_3 :::"is_isomorphism"::: ) "U1" "," "U2") & (Bool (Set (Var "F")) "is" ($#v1_osalg_3 :::"order-sorted"::: ) ) ")" )); end; :: deftheorem defines :::"are_os_isomorphic"::: OSALG_3:def 2 : (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) "holds" (Bool "(" (Bool (Set (Var "U1")) "," (Set (Var "U2")) ($#r1_osalg_3 :::"are_os_isomorphic"::: ) ) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) "st" (Bool "(" (Bool (Set (Var "F")) ($#r4_msualg_3 :::"is_isomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2"))) & (Bool (Set (Var "F")) "is" ($#v1_osalg_3 :::"order-sorted"::: ) ) ")" )) ")" ))); theorem :: OSALG_3:8 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U1")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) "holds" (Bool (Set (Var "U1")) "," (Set (Var "U1")) ($#r1_osalg_3 :::"are_os_isomorphic"::: ) ))) ; theorem :: OSALG_3:9 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) "st" (Bool (Bool (Set (Var "U1")) "," (Set (Var "U2")) ($#r1_osalg_3 :::"are_os_isomorphic"::: ) )) "holds" (Bool (Set (Var "U2")) "," (Set (Var "U1")) ($#r1_osalg_3 :::"are_os_isomorphic"::: ) ))) ; definitionlet "S1" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "U1", "U2" be ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")); :: original: :::"are_os_isomorphic"::: redefine pred "U1" "," "U2" :::"are_os_isomorphic"::: ; reflexivity (Bool "for" (Set (Var "U1")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")) "holds" (Bool ((Set (Const "S1")) "," (Set (Var "b1")) "," (Set (Var "b1"))))) ; end; definitionlet "S1" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "U1", "U2" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")); :: original: :::"are_os_isomorphic"::: redefine pred "U1" "," "U2" :::"are_os_isomorphic"::: ; symmetry (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")) "st" (Bool (Bool ((Set (Const "S1")) "," (Set (Var "b1")) "," (Set (Var "b2"))))) "holds" (Bool ((Set (Const "S1")) "," (Set (Var "b2")) "," (Set (Var "b1"))))) ; end; theorem :: OSALG_3:10 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "," (Set (Var "U3")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) "st" (Bool (Bool (Set (Var "U1")) "," (Set (Var "U2")) ($#r3_osalg_3 :::"are_os_isomorphic"::: ) ) & (Bool (Set (Var "U2")) "," (Set (Var "U3")) ($#r3_osalg_3 :::"are_os_isomorphic"::: ) )) "holds" (Bool (Set (Var "U1")) "," (Set (Var "U3")) ($#r3_osalg_3 :::"are_os_isomorphic"::: ) ))) ; theorem :: OSALG_3:11 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_osalg_3 :::"order-sorted"::: ) ) & (Bool (Set (Var "F")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2")))) "holds" (Bool (Set ($#k6_msualg_3 :::"Image"::: ) (Set (Var "F"))) "is" ($#v12_osalg_1 :::"order-sorted"::: ) )))) ; theorem :: OSALG_3:12 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_osalg_3 :::"order-sorted"::: ) )) "holds" (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S1")) "st" (Bool (Bool (Set (Var "o1")) ($#r6_osalg_1 :::"<="::: ) (Set (Var "o2")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o1")) "," (Set (Var "U1")) ")" ) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o2")) "," (Set (Var "U1")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) "holds" (Bool (Set (Set (Var "F")) ($#k5_msualg_3 :::"#"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_msualg_3 :::"#"::: ) (Set (Var "x1")))))))))) ; theorem :: OSALG_3:13 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v13_osalg_1 :::"monotone"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "U2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_osalg_3 :::"order-sorted"::: ) ) & (Bool (Set (Var "F")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2")))) "holds" (Bool "(" (Bool (Set ($#k6_msualg_3 :::"Image"::: ) (Set (Var "F"))) "is" ($#v12_osalg_1 :::"order-sorted"::: ) ) & (Bool (Set ($#k6_msualg_3 :::"Image"::: ) (Set (Var "F"))) "is" ($#v13_osalg_1 :::"monotone"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1"))) ")" ))))) ; theorem :: OSALG_3:14 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U1")) "being" ($#v13_osalg_1 :::"monotone"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "U2")) "being" ($#m1_msualg_2 :::"OSSubAlgebra":::) "of" (Set (Var "U1")) "holds" (Bool (Set (Var "U2")) "is" ($#v13_osalg_1 :::"monotone"::: ) )))) ; registrationlet "S1" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "U1" be ($#v13_osalg_1 :::"monotone"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")); cluster ($#v12_osalg_1 :::"order-sorted"::: ) ($#v13_osalg_1 :::"monotone"::: ) for ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" "U1"; end; registrationlet "S1" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "U1" be ($#v13_osalg_1 :::"monotone"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")); cluster ($#v12_osalg_1 :::"order-sorted"::: ) -> ($#v13_osalg_1 :::"monotone"::: ) for ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" "U1"; end; theorem :: OSALG_3:15 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) "st" (Bool (Bool (Set (Var "F")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2"))) & (Bool (Set (Var "F")) "is" ($#v1_osalg_3 :::"order-sorted"::: ) )) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set "(" ($#k6_msualg_3 :::"Image"::: ) (Set (Var "F")) ")" ) "st" (Bool "(" (Bool (Set (Var "F")) ($#r8_pboole :::"="::: ) (Set (Var "G"))) & (Bool (Set (Var "G")) "is" ($#v1_osalg_3 :::"order-sorted"::: ) ) & (Bool (Set (Var "G")) ($#r2_msualg_3 :::"is_epimorphism"::: ) (Set (Var "U1")) "," (Set ($#k6_msualg_3 :::"Image"::: ) (Set (Var "F")))) ")" ))))) ; theorem :: OSALG_3:16 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) "st" (Bool (Bool (Set (Var "F")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U1")) "," (Set (Var "U2"))) & (Bool (Set (Var "F")) "is" ($#v1_osalg_3 :::"order-sorted"::: ) )) "holds" (Bool "ex" (Set (Var "F1")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set "(" ($#k6_msualg_3 :::"Image"::: ) (Set (Var "F")) ")" )(Bool "ex" (Set (Var "F2")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" ($#k6_msualg_3 :::"Image"::: ) (Set (Var "F")) ")" ) "," (Set (Var "U2")) "st" (Bool "(" (Bool (Set (Var "F1")) ($#r2_msualg_3 :::"is_epimorphism"::: ) (Set (Var "U1")) "," (Set ($#k6_msualg_3 :::"Image"::: ) (Set (Var "F")))) & (Bool (Set (Var "F2")) ($#r3_msualg_3 :::"is_monomorphism"::: ) (Set ($#k6_msualg_3 :::"Image"::: ) (Set (Var "F"))) "," (Set (Var "U2"))) & (Bool (Set (Var "F")) ($#r8_pboole :::"="::: ) (Set (Set (Var "F2")) ($#k3_msualg_3 :::"**"::: ) (Set (Var "F1")))) & (Bool (Set (Var "F1")) "is" ($#v1_osalg_3 :::"order-sorted"::: ) ) & (Bool (Set (Var "F2")) "is" ($#v1_osalg_3 :::"order-sorted"::: ) ) ")" )))))) ; registrationlet "S1" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "U1" be ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S1")); cluster (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "U1") "," (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" "U1") "#)" ) -> ($#v12_osalg_1 :::"order-sorted"::: ) ; end; theorem :: OSALG_3:17 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U1")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) "holds" (Bool "(" (Bool (Set (Var "U1")) "is" ($#v13_osalg_1 :::"monotone"::: ) ) "iff" (Bool (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U1"))) "," (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "U1"))) "#)" ) "is" ($#v13_osalg_1 :::"monotone"::: ) ) ")" ))) ; theorem :: OSALG_3:18 (Bool "for" (Set (Var "S1")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S1")) "st" (Bool (Bool (Set (Var "U1")) "," (Set (Var "U2")) ($#r3_osalg_3 :::"are_os_isomorphic"::: ) )) "holds" (Bool "(" (Bool (Set (Var "U1")) "is" ($#v13_osalg_1 :::"monotone"::: ) ) "iff" (Bool (Set (Var "U2")) "is" ($#v13_osalg_1 :::"monotone"::: ) ) ")" ))) ;