:: OSALG_1 semantic presentation begin registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "I")); cluster (Set "p" ($#k3_relat_1 :::"*"::: ) "f") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; mode SortSymbol of "S" is ($#m1_subset_1 :::"Element":::) "of" "S"; end; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; mode OperSymbol of "S" is ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S"); end; definitionattr "c1" is :::"strict"::: ; struct :::"OverloadedMSSign"::: -> ($#l1_msualg_1 :::"ManySortedSign"::: ) ; aggr :::"OverloadedMSSign":::(# :::"carrier":::, :::"carrier'":::, :::"Overloading":::, :::"Arity":::, :::"ResultSort"::: #) -> ($#l1_osalg_1 :::"OverloadedMSSign"::: ) ; sel :::"Overloading"::: "c1" -> ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "c1"); end; definitionattr "c1" is :::"strict"::: ; struct :::"RelSortedSign"::: -> ($#l1_msualg_1 :::"ManySortedSign"::: ) "," ($#l1_orders_2 :::"RelStr"::: ) ; aggr :::"RelSortedSign":::(# :::"carrier":::, :::"InternalRel":::, :::"carrier'":::, :::"Arity":::, :::"ResultSort"::: #) -> ($#l2_osalg_1 :::"RelSortedSign"::: ) ; end; definitionattr "c1" is :::"strict"::: ; struct :::"OverloadedRSSign"::: -> ($#l1_osalg_1 :::"OverloadedMSSign"::: ) "," ($#l2_osalg_1 :::"RelSortedSign"::: ) ; aggr :::"OverloadedRSSign":::(# :::"carrier":::, :::"InternalRel":::, :::"carrier'":::, :::"Overloading":::, :::"Arity":::, :::"ResultSort"::: #) -> ($#l3_osalg_1 :::"OverloadedRSSign"::: ) ; end; theorem :: OSALG_1:1 (Bool "for" (Set (Var "A")) "," (Set (Var "O")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Order":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "Ol")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "O")) "," (Set "(" (Set (Var "A")) ($#k3_finseq_2 :::"*"::: ) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "O")) "," (Set (Var "A")) "holds" (Bool "(" (Bool (Bool "not" (Set ($#g3_osalg_1 :::"OverloadedRSSign"::: ) "(#" (Set (Var "A")) "," (Set (Var "R")) "," (Set (Var "O")) "," (Set (Var "Ol")) "," (Set (Var "f")) "," (Set (Var "g")) "#)" ) "is" ($#v2_struct_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set ($#g3_osalg_1 :::"OverloadedRSSign"::: ) "(#" (Set (Var "A")) "," (Set (Var "R")) "," (Set (Var "O")) "," (Set (Var "Ol")) "," (Set (Var "f")) "," (Set (Var "g")) "#)" ) "is" ($#v11_struct_0 :::"void"::: ) )) & (Bool (Set ($#g3_osalg_1 :::"OverloadedRSSign"::: ) "(#" (Set (Var "A")) "," (Set (Var "R")) "," (Set (Var "O")) "," (Set (Var "Ol")) "," (Set (Var "f")) "," (Set (Var "g")) "#)" ) "is" ($#v3_orders_2 :::"reflexive"::: ) ) & (Bool (Set ($#g3_osalg_1 :::"OverloadedRSSign"::: ) "(#" (Set (Var "A")) "," (Set (Var "R")) "," (Set (Var "O")) "," (Set (Var "Ol")) "," (Set (Var "f")) "," (Set (Var "g")) "#)" ) "is" ($#v4_orders_2 :::"transitive"::: ) ) & (Bool (Set ($#g3_osalg_1 :::"OverloadedRSSign"::: ) "(#" (Set (Var "A")) "," (Set (Var "R")) "," (Set (Var "O")) "," (Set (Var "Ol")) "," (Set (Var "f")) "," (Set (Var "g")) "#)" ) "is" ($#v5_orders_2 :::"antisymmetric"::: ) ) ")" )))))) ; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Order":::) "of" (Set (Const "A")); let "O" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Ol" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "O")); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "O")) "," (Set "(" (Set (Const "A")) ($#k3_finseq_2 :::"*"::: ) ")" ); let "g" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "O")) "," (Set (Const "A")); cluster (Set ($#g3_osalg_1 :::"OverloadedRSSign"::: ) "(#" "A" "," "R" "," "O" "," "Ol" "," "f" "," "g" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ; end; begin definitionlet "S" be ($#l3_osalg_1 :::"OverloadedRSSign"::: ) ; attr "S" is :::"order-sorted"::: means :: OSALG_1:def 1 (Bool "(" (Bool "S" "is" ($#v3_orders_2 :::"reflexive"::: ) ) & (Bool "S" "is" ($#v4_orders_2 :::"transitive"::: ) ) & (Bool "S" "is" ($#v5_orders_2 :::"antisymmetric"::: ) ) ")" ); end; :: deftheorem defines :::"order-sorted"::: OSALG_1:def 1 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OverloadedRSSign"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v4_osalg_1 :::"order-sorted"::: ) ) "iff" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_orders_2 :::"reflexive"::: ) ) & (Bool (Set (Var "S")) "is" ($#v4_orders_2 :::"transitive"::: ) ) & (Bool (Set (Var "S")) "is" ($#v5_orders_2 :::"antisymmetric"::: ) ) ")" ) ")" )); registration cluster ($#v4_osalg_1 :::"order-sorted"::: ) -> ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) for ($#l3_osalg_1 :::"OverloadedRSSign"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v3_osalg_1 :::"strict"::: ) ($#v4_osalg_1 :::"order-sorted"::: ) for ($#l3_osalg_1 :::"OverloadedRSSign"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) for ($#l1_osalg_1 :::"OverloadedMSSign"::: ) ; end; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_osalg_1 :::"OverloadedMSSign"::: ) ; let "x", "y" be ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); pred "x" :::"~="::: "y" means :: OSALG_1:def 2 (Bool (Set ($#k4_tarski :::"["::: ) "x" "," "y" ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_osalg_1 :::"Overloading"::: ) "of" "S")); symmetry (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_osalg_1 :::"Overloading"::: ) "of" (Set (Const "S"))))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_osalg_1 :::"Overloading"::: ) "of" (Set (Const "S"))))) ; reflexivity (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_osalg_1 :::"Overloading"::: ) "of" (Set (Const "S"))))) ; end; :: deftheorem defines :::"~="::: OSALG_1:def 2 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_osalg_1 :::"OverloadedMSSign"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_osalg_1 :::"~="::: ) (Set (Var "y"))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_osalg_1 :::"Overloading"::: ) "of" (Set (Var "S")))) ")" ))); theorem :: OSALG_1:2 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_osalg_1 :::"OverloadedMSSign"::: ) (Bool "for" (Set (Var "o")) "," (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "o")) ($#r1_osalg_1 :::"~="::: ) (Set (Var "o1"))) & (Bool (Set (Var "o1")) ($#r1_osalg_1 :::"~="::: ) (Set (Var "o2")))) "holds" (Bool (Set (Var "o")) ($#r1_osalg_1 :::"~="::: ) (Set (Var "o2"))))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_osalg_1 :::"OverloadedMSSign"::: ) ; attr "S" is :::"discernable"::: means :: OSALG_1:def 3 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" "S" "st" (Bool (Bool (Set (Var "x")) ($#r1_osalg_1 :::"~="::: ) (Set (Var "y"))) & (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "y")))) & (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))); attr "S" is :::"op-discrete"::: means :: OSALG_1:def 4 (Bool (Set "the" ($#u1_osalg_1 :::"Overloading"::: ) "of" "S") ($#r2_relset_1 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S"))); end; :: deftheorem defines :::"discernable"::: OSALG_1:def 3 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_osalg_1 :::"OverloadedMSSign"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v5_osalg_1 :::"discernable"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r1_osalg_1 :::"~="::: ) (Set (Var "y"))) & (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "y")))) & (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ")" )); :: deftheorem defines :::"op-discrete"::: OSALG_1:def 4 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_osalg_1 :::"OverloadedMSSign"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v6_osalg_1 :::"op-discrete"::: ) ) "iff" (Bool (Set "the" ($#u1_osalg_1 :::"Overloading"::: ) "of" (Set (Var "S"))) ($#r2_relset_1 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))))) ")" )); theorem :: OSALG_1:3 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_osalg_1 :::"OverloadedMSSign"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v6_osalg_1 :::"op-discrete"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r1_osalg_1 :::"~="::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ")" )) ; theorem :: OSALG_1:4 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_osalg_1 :::"OverloadedMSSign"::: ) "st" (Bool (Bool (Set (Var "S")) "is" ($#v6_osalg_1 :::"op-discrete"::: ) )) "holds" (Bool (Set (Var "S")) "is" ($#v5_osalg_1 :::"discernable"::: ) )) ; begin definitionlet "S0" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; func :::"OSSign"::: "S0" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v3_osalg_1 :::"strict"::: ) ($#v4_osalg_1 :::"order-sorted"::: ) ($#l3_osalg_1 :::"OverloadedRSSign"::: ) means :: OSALG_1:def 5 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S0") ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it)) & (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S0")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" it)) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S0") ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" it)) & (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S0")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_osalg_1 :::"Overloading"::: ) "of" it)) & (Bool (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" "S0") ($#r1_funct_2 :::"="::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" it)) & (Bool (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" "S0") ($#r1_funct_2 :::"="::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" it)) ")" ); end; :: deftheorem defines :::"OSSign"::: OSALG_1:def 5 : (Bool "for" (Set (Var "S0")) "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 "b2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v3_osalg_1 :::"strict"::: ) ($#v4_osalg_1 :::"order-sorted"::: ) ($#l3_osalg_1 :::"OverloadedRSSign"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_osalg_1 :::"OSSign"::: ) (Set (Var "S0")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S0"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2")))) & (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S0")))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "b2")))) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S0"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "b2")))) & (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S0")))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_osalg_1 :::"Overloading"::: ) "of" (Set (Var "b2")))) & (Bool (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S0"))) ($#r1_funct_2 :::"="::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "b2")))) & (Bool (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S0"))) ($#r1_funct_2 :::"="::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "b2")))) ")" ) ")" ))); theorem :: OSALG_1:5 (Bool "for" (Set (Var "S0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set ($#k1_osalg_1 :::"OSSign"::: ) (Set (Var "S0"))) "is" ($#v1_orders_3 :::"discrete"::: ) ) & (Bool (Set ($#k1_osalg_1 :::"OSSign"::: ) (Set (Var "S0"))) "is" ($#v6_osalg_1 :::"op-discrete"::: ) ) ")" )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) bbbadV14_STRUCT_0() ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_orders_3 :::"discrete"::: ) ($#v3_osalg_1 :::"strict"::: ) ($#v4_osalg_1 :::"order-sorted"::: ) ($#v5_osalg_1 :::"discernable"::: ) ($#v6_osalg_1 :::"op-discrete"::: ) for ($#l3_osalg_1 :::"OverloadedRSSign"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v6_osalg_1 :::"op-discrete"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v5_osalg_1 :::"discernable"::: ) for ($#l3_osalg_1 :::"OverloadedRSSign"::: ) ; end; registrationlet "S0" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster (Set ($#k1_osalg_1 :::"OSSign"::: ) "S0") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_orders_3 :::"discrete"::: ) ($#v3_osalg_1 :::"strict"::: ) ($#v4_osalg_1 :::"order-sorted"::: ) ($#v6_osalg_1 :::"op-discrete"::: ) ; end; definitionmode OrderSortedSign is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v4_osalg_1 :::"order-sorted"::: ) ($#v5_osalg_1 :::"discernable"::: ) ($#l3_osalg_1 :::"OverloadedRSSign"::: ) ; end; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); let "w1", "w2" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))) ($#k3_finseq_2 :::"*"::: ) ); pred "w1" :::"<="::: "w2" means :: OSALG_1:def 6 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "w1") ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "w2")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "w1"))) "holds" (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element":::) "of" "S" "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set "w1" ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set "w2" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Var "s1")) ($#r3_orders_2 :::"<="::: ) (Set (Var "s2")))) ")" ) ")" ); reflexivity (Bool "for" (Set (Var "w1")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "w1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "w1")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "w1"))))) "holds" (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "w1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "w1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Var "s1")) ($#r3_orders_2 :::"<="::: ) (Set (Var "s2")))) ")" ) ")" )) ; end; :: deftheorem defines :::"<="::: OSALG_1:def 6 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool "(" (Bool (Set (Var "w1")) ($#r2_osalg_1 :::"<="::: ) (Set (Var "w2"))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "w1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "w2")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "w1"))))) "holds" (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "w1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "w2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Var "s1")) ($#r3_orders_2 :::"<="::: ) (Set (Var "s2")))) ")" ) ")" ) ")" ))); theorem :: OSALG_1:6 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "w1")) ($#r2_osalg_1 :::"<="::: ) (Set (Var "w2"))) & (Bool (Set (Var "w2")) ($#r2_osalg_1 :::"<="::: ) (Set (Var "w1")))) "holds" (Bool (Set (Var "w1")) ($#r1_hidden :::"="::: ) (Set (Var "w2"))))) ; theorem :: OSALG_1:7 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "S")) "is" ($#v1_orders_3 :::"discrete"::: ) ) & (Bool (Set (Var "w1")) ($#r2_osalg_1 :::"<="::: ) (Set (Var "w2")))) "holds" (Bool (Set (Var "w1")) ($#r1_hidden :::"="::: ) (Set (Var "w2"))))) ; theorem :: OSALG_1:8 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v1_orders_3 :::"discrete"::: ) ) & (Bool (Set (Var "o1")) ($#r1_osalg_1 :::"~="::: ) (Set (Var "o2"))) & (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o1"))) ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o2")))) & (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o1"))) ($#r3_orders_2 :::"<="::: ) (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o2"))))) "holds" (Bool (Set (Var "o1")) ($#r1_hidden :::"="::: ) (Set (Var "o2"))))) ; definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "o" be ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); attr "o" is :::"monotone"::: means :: OSALG_1:def 7 (Bool "for" (Set (Var "o2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" "S" "st" (Bool (Bool "o" ($#r1_osalg_1 :::"~="::: ) (Set (Var "o2"))) & (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) "o") ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o2"))))) "holds" (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) "o") ($#r3_orders_2 :::"<="::: ) (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o2"))))); end; :: deftheorem defines :::"monotone"::: OSALG_1:def 7 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "o")) "is" ($#v7_osalg_1 :::"monotone"::: ) ) "iff" (Bool "for" (Set (Var "o2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "o")) ($#r1_osalg_1 :::"~="::: ) (Set (Var "o2"))) & (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o"))) ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o2"))))) "holds" (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o"))) ($#r3_orders_2 :::"<="::: ) (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o2"))))) ")" ))); definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); attr "S" is :::"monotone"::: means :: OSALG_1:def 8 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" "S" "holds" (Bool (Set (Var "o")) "is" ($#v7_osalg_1 :::"monotone"::: ) )); end; :: deftheorem defines :::"monotone"::: OSALG_1:def 8 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v8_osalg_1 :::"monotone"::: ) ) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "o")) "is" ($#v7_osalg_1 :::"monotone"::: ) )) ")" )); theorem :: OSALG_1:9 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) "st" (Bool (Bool (Set (Var "S")) "is" ($#v6_osalg_1 :::"op-discrete"::: ) )) "holds" (Bool (Set (Var "S")) "is" ($#v8_osalg_1 :::"monotone"::: ) )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) bbbadV14_STRUCT_0() ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v4_osalg_1 :::"order-sorted"::: ) ($#v5_osalg_1 :::"discernable"::: ) ($#v8_osalg_1 :::"monotone"::: ) for ($#l3_osalg_1 :::"OverloadedRSSign"::: ) ; end; registrationlet "S" be ($#v8_osalg_1 :::"monotone"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); cluster ($#v7_osalg_1 :::"monotone"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S"); end; registrationlet "S" be ($#v8_osalg_1 :::"monotone"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); cluster -> ($#v7_osalg_1 :::"monotone"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S"); end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v4_osalg_1 :::"order-sorted"::: ) ($#v5_osalg_1 :::"discernable"::: ) ($#v6_osalg_1 :::"op-discrete"::: ) -> ($#v8_osalg_1 :::"monotone"::: ) for ($#l3_osalg_1 :::"OverloadedRSSign"::: ) ; end; theorem :: OSALG_1:10 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v8_osalg_1 :::"monotone"::: ) ) & (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "o1")) ($#r1_osalg_1 :::"~="::: ) (Set (Var "o2"))) & (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "o1")) ($#r1_hidden :::"="::: ) (Set (Var "o2"))))) ; definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "o", "o1" be ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); let "w1" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))) ($#k3_finseq_2 :::"*"::: ) ); pred "o1" :::"has_least_args_for"::: "o" "," "w1" means :: OSALG_1:def 9 (Bool "(" (Bool "o" ($#r1_osalg_1 :::"~="::: ) "o1") & (Bool "w1" ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) "o1")) & (Bool "(" "for" (Set (Var "o2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" "S" "st" (Bool (Bool "o" ($#r1_osalg_1 :::"~="::: ) (Set (Var "o2"))) & (Bool "w1" ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o2"))))) "holds" (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) "o1") ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o2")))) ")" ) ")" ); pred "o1" :::"has_least_sort_for"::: "o" "," "w1" means :: OSALG_1:def 10 (Bool "(" (Bool "o" ($#r1_osalg_1 :::"~="::: ) "o1") & (Bool "w1" ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) "o1")) & (Bool "(" "for" (Set (Var "o2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" "S" "st" (Bool (Bool "o" ($#r1_osalg_1 :::"~="::: ) (Set (Var "o2"))) & (Bool "w1" ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o2"))))) "holds" (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) "o1") ($#r3_orders_2 :::"<="::: ) (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o2")))) ")" ) ")" ); end; :: deftheorem defines :::"has_least_args_for"::: OSALG_1:def 9 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "o")) "," (Set (Var "o1")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "w1")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool "(" (Bool (Set (Var "o1")) ($#r3_osalg_1 :::"has_least_args_for"::: ) (Set (Var "o")) "," (Set (Var "w1"))) "iff" (Bool "(" (Bool (Set (Var "o")) ($#r1_osalg_1 :::"~="::: ) (Set (Var "o1"))) & (Bool (Set (Var "w1")) ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o1")))) & (Bool "(" "for" (Set (Var "o2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "o")) ($#r1_osalg_1 :::"~="::: ) (Set (Var "o2"))) & (Bool (Set (Var "w1")) ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o2"))))) "holds" (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o1"))) ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o2")))) ")" ) ")" ) ")" )))); :: deftheorem defines :::"has_least_sort_for"::: OSALG_1:def 10 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "o")) "," (Set (Var "o1")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "w1")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool "(" (Bool (Set (Var "o1")) ($#r4_osalg_1 :::"has_least_sort_for"::: ) (Set (Var "o")) "," (Set (Var "w1"))) "iff" (Bool "(" (Bool (Set (Var "o")) ($#r1_osalg_1 :::"~="::: ) (Set (Var "o1"))) & (Bool (Set (Var "w1")) ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o1")))) & (Bool "(" "for" (Set (Var "o2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "o")) ($#r1_osalg_1 :::"~="::: ) (Set (Var "o2"))) & (Bool (Set (Var "w1")) ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o2"))))) "holds" (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o1"))) ($#r3_orders_2 :::"<="::: ) (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o2")))) ")" ) ")" ) ")" )))); definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "o", "o1" be ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); let "w1" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))) ($#k3_finseq_2 :::"*"::: ) ); pred "o1" :::"has_least_rank_for"::: "o" "," "w1" means :: OSALG_1:def 11 (Bool "(" (Bool "o1" ($#r3_osalg_1 :::"has_least_args_for"::: ) "o" "," "w1") & (Bool "o1" ($#r4_osalg_1 :::"has_least_sort_for"::: ) "o" "," "w1") ")" ); end; :: deftheorem defines :::"has_least_rank_for"::: OSALG_1:def 11 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "o")) "," (Set (Var "o1")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "w1")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool "(" (Bool (Set (Var "o1")) ($#r5_osalg_1 :::"has_least_rank_for"::: ) (Set (Var "o")) "," (Set (Var "w1"))) "iff" (Bool "(" (Bool (Set (Var "o1")) ($#r3_osalg_1 :::"has_least_args_for"::: ) (Set (Var "o")) "," (Set (Var "w1"))) & (Bool (Set (Var "o1")) ($#r4_osalg_1 :::"has_least_sort_for"::: ) (Set (Var "o")) "," (Set (Var "w1"))) ")" ) ")" )))); definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "o" be ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); attr "o" is :::"regular"::: means :: OSALG_1:def 12 (Bool "(" (Bool "o" "is" ($#v7_osalg_1 :::"monotone"::: ) ) & (Bool "(" "for" (Set (Var "w1")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "w1")) ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) "o"))) "holds" (Bool "ex" (Set (Var "o1")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" "S" "st" (Bool (Set (Var "o1")) ($#r3_osalg_1 :::"has_least_args_for"::: ) "o" "," (Set (Var "w1")))) ")" ) ")" ); end; :: deftheorem defines :::"regular"::: OSALG_1:def 12 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "o")) "is" ($#v9_osalg_1 :::"regular"::: ) ) "iff" (Bool "(" (Bool (Set (Var "o")) "is" ($#v7_osalg_1 :::"monotone"::: ) ) & (Bool "(" "for" (Set (Var "w1")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "w1")) ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o"))))) "holds" (Bool "ex" (Set (Var "o1")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Set (Var "o1")) ($#r3_osalg_1 :::"has_least_args_for"::: ) (Set (Var "o")) "," (Set (Var "w1")))) ")" ) ")" ) ")" ))); definitionlet "SM" be ($#v8_osalg_1 :::"monotone"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); attr "SM" is :::"regular"::: means :: OSALG_1:def 13 (Bool "for" (Set (Var "om")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" "SM" "holds" (Bool (Set (Var "om")) "is" ($#v9_osalg_1 :::"regular"::: ) )); end; :: deftheorem defines :::"regular"::: OSALG_1:def 13 : (Bool "for" (Set (Var "SM")) "being" ($#v8_osalg_1 :::"monotone"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) "holds" (Bool "(" (Bool (Set (Var "SM")) "is" ($#v10_osalg_1 :::"regular"::: ) ) "iff" (Bool "for" (Set (Var "om")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "SM")) "holds" (Bool (Set (Var "om")) "is" ($#v9_osalg_1 :::"regular"::: ) )) ")" )); theorem :: OSALG_1:11 (Bool "for" (Set (Var "SM")) "being" ($#v8_osalg_1 :::"monotone"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) "holds" (Bool "(" (Bool (Set (Var "SM")) "is" ($#v10_osalg_1 :::"regular"::: ) ) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "SM")) (Bool "for" (Set (Var "w1")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "SM"))) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "w1")) ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o"))))) "holds" (Bool "ex" (Set (Var "o1")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "SM")) "st" (Bool (Set (Var "o1")) ($#r5_osalg_1 :::"has_least_rank_for"::: ) (Set (Var "o")) "," (Set (Var "w1")))))) ")" )) ; theorem :: OSALG_1:12 (Bool "for" (Set (Var "SM")) "being" ($#v8_osalg_1 :::"monotone"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) "st" (Bool (Bool (Set (Var "SM")) "is" ($#v6_osalg_1 :::"op-discrete"::: ) )) "holds" (Bool (Set (Var "SM")) "is" ($#v10_osalg_1 :::"regular"::: ) )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) bbbadV14_STRUCT_0() ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v4_osalg_1 :::"order-sorted"::: ) ($#v5_osalg_1 :::"discernable"::: ) ($#v8_osalg_1 :::"monotone"::: ) ($#v10_osalg_1 :::"regular"::: ) for ($#l3_osalg_1 :::"OverloadedRSSign"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v4_osalg_1 :::"order-sorted"::: ) ($#v5_osalg_1 :::"discernable"::: ) ($#v6_osalg_1 :::"op-discrete"::: ) ($#v8_osalg_1 :::"monotone"::: ) -> ($#v8_osalg_1 :::"monotone"::: ) ($#v10_osalg_1 :::"regular"::: ) for ($#l3_osalg_1 :::"OverloadedRSSign"::: ) ; end; registrationlet "SR" be ($#v8_osalg_1 :::"monotone"::: ) ($#v10_osalg_1 :::"regular"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); cluster -> ($#v9_osalg_1 :::"regular"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "SR"); end; theorem :: OSALG_1:13 (Bool "for" (Set (Var "SR")) "being" ($#v8_osalg_1 :::"monotone"::: ) ($#v10_osalg_1 :::"regular"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "o3")) "," (Set (Var "o")) "," (Set (Var "o4")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "SR")) (Bool "for" (Set (Var "w1")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "SR"))) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "o3")) ($#r3_osalg_1 :::"has_least_args_for"::: ) (Set (Var "o")) "," (Set (Var "w1"))) & (Bool (Set (Var "o4")) ($#r3_osalg_1 :::"has_least_args_for"::: ) (Set (Var "o")) "," (Set (Var "w1")))) "holds" (Bool (Set (Var "o3")) ($#r1_hidden :::"="::: ) (Set (Var "o4")))))) ; definitionlet "SR" be ($#v8_osalg_1 :::"monotone"::: ) ($#v10_osalg_1 :::"regular"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); let "o" be ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "SR")); let "w1" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "SR"))) ($#k3_finseq_2 :::"*"::: ) ); assume (Bool (Set (Const "w1")) ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Const "o")))) ; func :::"LBound"::: "(" "o" "," "w1" ")" -> ($#m1_subset_1 :::"OperSymbol":::) "of" "SR" means :: OSALG_1:def 14 (Bool it ($#r3_osalg_1 :::"has_least_args_for"::: ) "o" "," "w1"); end; :: deftheorem defines :::"LBound"::: OSALG_1:def 14 : (Bool "for" (Set (Var "SR")) "being" ($#v8_osalg_1 :::"monotone"::: ) ($#v10_osalg_1 :::"regular"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "SR")) (Bool "for" (Set (Var "w1")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "SR"))) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "w1")) ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o"))))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "SR")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_osalg_1 :::"LBound"::: ) "(" (Set (Var "o")) "," (Set (Var "w1")) ")" )) "iff" (Bool (Set (Var "b4")) ($#r3_osalg_1 :::"has_least_args_for"::: ) (Set (Var "o")) "," (Set (Var "w1"))) ")" ))))); theorem :: OSALG_1:14 (Bool "for" (Set (Var "SR")) "being" ($#v8_osalg_1 :::"monotone"::: ) ($#v10_osalg_1 :::"regular"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "SR")) (Bool "for" (Set (Var "w1")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "SR"))) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "w1")) ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o"))))) "holds" (Bool (Set ($#k2_osalg_1 :::"LBound"::: ) "(" (Set (Var "o")) "," (Set (Var "w1")) ")" ) ($#r5_osalg_1 :::"has_least_rank_for"::: ) (Set (Var "o")) "," (Set (Var "w1")))))) ; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); let "z" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"ConstOSSet"::: "(" "R" "," "z" ")" -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") equals :: OSALG_1:def 15 (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") ($#k7_funcop_1 :::"-->"::: ) "z"); end; :: deftheorem defines :::"ConstOSSet"::: OSALG_1:def 15 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_osalg_1 :::"ConstOSSet"::: ) "(" (Set (Var "R")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "z")))))); theorem :: OSALG_1:15 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k3_osalg_1 :::"ConstOSSet"::: ) "(" (Set (Var "R")) "," (Set (Var "z")) ")" ) "is" bbbadV2_RELAT_1()) & (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 (Set (Set "(" ($#k3_osalg_1 :::"ConstOSSet"::: ) "(" (Set (Var "R")) "," (Set (Var "z")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s1"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k3_osalg_1 :::"ConstOSSet"::: ) "(" (Set (Var "R")) "," (Set (Var "z")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s2")))) ")" ) ")" ))) ; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "R")); attr "M" is :::"order-sorted"::: means :: OSALG_1:def 16 (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 (Set "M" ($#k1_funct_1 :::"."::: ) (Set (Var "s1"))) ($#r1_tarski :::"c="::: ) (Set "M" ($#k1_funct_1 :::"."::: ) (Set (Var "s2"))))); end; :: deftheorem defines :::"order-sorted"::: OSALG_1:def 16 : (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 :::"ManySortedSet":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v11_osalg_1 :::"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 (Set (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set (Var "s1"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set (Var "s2"))))) ")" ))); theorem :: OSALG_1:16 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_osalg_1 :::"ConstOSSet"::: ) "(" (Set (Var "R")) "," (Set (Var "z")) ")" ) "is" ($#v11_osalg_1 :::"order-sorted"::: ) ))) ; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (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")) ($#v11_osalg_1 :::"order-sorted"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); let "z" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_osalg_1 :::"ConstOSSet"::: ) "(" "R" "," "z" ")" ) -> ($#v11_osalg_1 :::"order-sorted"::: ) ; end; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); mode OrderSortedSet of "R" is ($#v11_osalg_1 :::"order-sorted"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" "R"; end; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); 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")) ($#v11_osalg_1 :::"order-sorted"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "M" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); attr "M" is :::"order-sorted"::: means :: OSALG_1:def 17 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" "S" "st" (Bool (Bool (Set (Var "s1")) ($#r3_orders_2 :::"<="::: ) (Set (Var "s2")))) "holds" (Bool (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "M") ($#k1_funct_1 :::"."::: ) (Set (Var "s1"))) ($#r1_tarski :::"c="::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "M") ($#k1_funct_1 :::"."::: ) (Set (Var "s2"))))); end; :: deftheorem defines :::"order-sorted"::: OSALG_1:def 17 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "M")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v12_osalg_1 :::"order-sorted"::: ) ) "iff" (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "s1")) ($#r3_orders_2 :::"<="::: ) (Set (Var "s2")))) "holds" (Bool (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "M"))) ($#k1_funct_1 :::"."::: ) (Set (Var "s1"))) ($#r1_tarski :::"c="::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "M"))) ($#k1_funct_1 :::"."::: ) (Set (Var "s2"))))) ")" ))); theorem :: OSALG_1:17 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "M")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v12_osalg_1 :::"order-sorted"::: ) ) "iff" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "M"))) "is" ($#m1_hidden :::"OrderSortedSet":::) "of" (Set (Var "S"))) ")" ))) ; definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "z" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "CH" be ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Set "(" (Set "(" ($#k3_osalg_1 :::"ConstOSSet"::: ) "(" (Set (Const "S")) "," (Set (Const "z")) ")" ")" ) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Const "S")))) "," (Set (Set "(" ($#k3_osalg_1 :::"ConstOSSet"::: ) "(" (Set (Const "S")) "," (Set (Const "z")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Const "S")))); func :::"ConstOSA"::: "(" "S" "," "z" "," "CH" ")" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S" means :: OSALG_1:def 18 (Bool "(" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" it) ($#r8_pboole :::"="::: ) (Set ($#k3_osalg_1 :::"ConstOSSet"::: ) "(" "S" "," "z" ")" )) & (Bool (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" it) ($#r8_pboole :::"="::: ) "CH") ")" ); end; :: deftheorem defines :::"ConstOSA"::: OSALG_1:def 18 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "CH")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Set "(" (Set "(" ($#k3_osalg_1 :::"ConstOSSet"::: ) "(" (Set (Var "S")) "," (Set (Var "z")) ")" ")" ) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S")))) "," (Set (Set "(" ($#k3_osalg_1 :::"ConstOSSet"::: ) "(" (Set (Var "S")) "," (Set (Var "z")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S")))) (Bool "for" (Set (Var "b4")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_osalg_1 :::"ConstOSA"::: ) "(" (Set (Var "S")) "," (Set (Var "z")) "," (Set (Var "CH")) ")" )) "iff" (Bool "(" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "b4"))) ($#r8_pboole :::"="::: ) (Set ($#k3_osalg_1 :::"ConstOSSet"::: ) "(" (Set (Var "S")) "," (Set (Var "z")) ")" )) & (Bool (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "b4"))) ($#r8_pboole :::"="::: ) (Set (Var "CH"))) ")" ) ")" ))))); theorem :: OSALG_1:18 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "CH")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Set "(" (Set "(" ($#k3_osalg_1 :::"ConstOSSet"::: ) "(" (Set (Var "S")) "," (Set (Var "z")) ")" ")" ) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Var "S")))) "," (Set (Set "(" ($#k3_osalg_1 :::"ConstOSSet"::: ) "(" (Set (Var "S")) "," (Set (Var "z")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Var "S")))) "holds" (Bool (Set ($#k4_osalg_1 :::"ConstOSA"::: ) "(" (Set (Var "S")) "," (Set (Var "z")) "," (Set (Var "CH")) ")" ) "is" ($#v12_osalg_1 :::"order-sorted"::: ) )))) ; registrationlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); cluster ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v12_osalg_1 :::"order-sorted"::: ) for ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S"; end; registrationlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "z" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "CH" be ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Set "(" (Set "(" ($#k3_osalg_1 :::"ConstOSSet"::: ) "(" (Set (Const "S")) "," (Set (Const "z")) ")" ")" ) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set (Const "S")))) "," (Set (Set "(" ($#k3_osalg_1 :::"ConstOSSet"::: ) "(" (Set (Const "S")) "," (Set (Const "z")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set (Const "S")))); cluster (Set ($#k4_osalg_1 :::"ConstOSA"::: ) "(" "S" "," "z" "," "CH" ")" ) -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v12_osalg_1 :::"order-sorted"::: ) ; end; definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); mode OSAlgebra of "S" is ($#v12_osalg_1 :::"order-sorted"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S"; end; theorem :: OSALG_1:19 (Bool "for" (Set (Var "S")) "being" ($#v1_orders_3 :::"discrete"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "M")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool (Set (Var "M")) "is" ($#v12_osalg_1 :::"order-sorted"::: ) ))) ; registrationlet "S" be ($#v1_orders_3 :::"discrete"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); cluster -> ($#v12_osalg_1 :::"order-sorted"::: ) for ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" "S"; end; theorem :: OSALG_1:20 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "w1")) ($#r2_osalg_1 :::"<="::: ) (Set (Var "w2")))) "holds" (Bool (Set (Set "(" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "w1"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "w2"))))))) ; definitionlet "S0" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "M" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S0")); func :::"OSAlg"::: "M" -> ($#v3_msualg_1 :::"strict"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set ($#k1_osalg_1 :::"OSSign"::: ) "S0") means :: OSALG_1:def 19 (Bool "(" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "M")) & (Bool (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" "M")) ")" ); end; :: deftheorem defines :::"OSAlg"::: OSALG_1:def 19 : (Bool "for" (Set (Var "S0")) "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 "M")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S0")) (Bool "for" (Set (Var "b3")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set ($#k1_osalg_1 :::"OSSign"::: ) (Set (Var "S0"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_osalg_1 :::"OSAlg"::: ) (Set (Var "M")))) "iff" (Bool "(" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "M")))) & (Bool (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "M")))) ")" ) ")" )))); theorem :: OSALG_1:21 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "," (Set (Var "w3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "w1")) ($#r2_osalg_1 :::"<="::: ) (Set (Var "w2"))) & (Bool (Set (Var "w2")) ($#r2_osalg_1 :::"<="::: ) (Set (Var "w3")))) "holds" (Bool (Set (Var "w1")) ($#r2_osalg_1 :::"<="::: ) (Set (Var "w3"))))) ; definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "o1", "o2" be ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); pred "o1" :::"<="::: "o2" means :: OSALG_1:def 20 (Bool "(" (Bool "o1" ($#r1_osalg_1 :::"~="::: ) "o2") & (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) "o1") ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) "o2")) & (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) "o1") ($#r3_orders_2 :::"<="::: ) (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) "o2")) ")" ); reflexivity (Bool "for" (Set (Var "o1")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")) "holds" (Bool "(" (Bool (Set (Var "o1")) ($#r1_osalg_1 :::"~="::: ) (Set (Var "o1"))) & (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o1"))) ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o1")))) & (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o1"))) ($#r3_orders_2 :::"<="::: ) (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o1")))) ")" )) ; end; :: deftheorem defines :::"<="::: OSALG_1:def 20 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "o1")) ($#r6_osalg_1 :::"<="::: ) (Set (Var "o2"))) "iff" (Bool "(" (Bool (Set (Var "o1")) ($#r1_osalg_1 :::"~="::: ) (Set (Var "o2"))) & (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o1"))) ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o2")))) & (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o1"))) ($#r3_orders_2 :::"<="::: ) (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o2")))) ")" ) ")" ))); theorem :: OSALG_1:22 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "o1")) ($#r6_osalg_1 :::"<="::: ) (Set (Var "o2"))) & (Bool (Set (Var "o2")) ($#r6_osalg_1 :::"<="::: ) (Set (Var "o1")))) "holds" (Bool (Set (Var "o1")) ($#r1_hidden :::"="::: ) (Set (Var "o2"))))) ; theorem :: OSALG_1:23 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "," (Set (Var "o3")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "o1")) ($#r6_osalg_1 :::"<="::: ) (Set (Var "o2"))) & (Bool (Set (Var "o2")) ($#r6_osalg_1 :::"<="::: ) (Set (Var "o3")))) "holds" (Bool (Set (Var "o1")) ($#r6_osalg_1 :::"<="::: ) (Set (Var "o3"))))) ; theorem :: OSALG_1:24 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o1"))) ($#r3_orders_2 :::"<="::: ) (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o2"))))) "holds" (Bool (Set ($#k4_msualg_1 :::"Result"::: ) "(" (Set (Var "o1")) "," (Set (Var "A")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k4_msualg_1 :::"Result"::: ) "(" (Set (Var "o2")) "," (Set (Var "A")) ")" ))))) ; theorem :: OSALG_1:25 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o1"))) ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o2"))))) "holds" (Bool (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o1")) "," (Set (Var "A")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o2")) "," (Set (Var "A")) ")" ))))) ; theorem :: OSALG_1:26 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "o1")) ($#r6_osalg_1 :::"<="::: ) (Set (Var "o2")))) "holds" (Bool "(" (Bool (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o1")) "," (Set (Var "A")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o2")) "," (Set (Var "A")) ")" )) & (Bool (Set ($#k4_msualg_1 :::"Result"::: ) "(" (Set (Var "o1")) "," (Set (Var "A")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k4_msualg_1 :::"Result"::: ) "(" (Set (Var "o2")) "," (Set (Var "A")) ")" )) ")" )))) ; definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "A" be ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Const "S")); attr "A" is :::"monotone"::: means :: OSALG_1:def 21 (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" "S" "st" (Bool (Bool (Set (Var "o1")) ($#r6_osalg_1 :::"<="::: ) (Set (Var "o2")))) "holds" (Bool (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o2")) "," "A" ")" ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o1")) "," "A" ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o1")) "," "A" ")" ))); end; :: deftheorem defines :::"monotone"::: OSALG_1:def 21 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v13_osalg_1 :::"monotone"::: ) ) "iff" (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "o1")) ($#r6_osalg_1 :::"<="::: ) (Set (Var "o2")))) "holds" (Bool (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o2")) "," (Set (Var "A")) ")" ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o1")) "," (Set (Var "A")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o1")) "," (Set (Var "A")) ")" ))) ")" ))); theorem :: OSALG_1:27 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v13_osalg_1 :::"monotone"::: ) ) "iff" (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "o1")) ($#r6_osalg_1 :::"<="::: ) (Set (Var "o2")))) "holds" (Bool (Set ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o1")) "," (Set (Var "A")) ")" ) ($#r1_relset_1 :::"c="::: ) (Set ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o2")) "," (Set (Var "A")) ")" ))) ")" ))) ; theorem :: OSALG_1:28 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S")) "st" (Bool (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_orders_3 :::"discrete"::: ) ) "or" (Bool (Set (Var "S")) "is" ($#v6_osalg_1 :::"op-discrete"::: ) ) ")" )) "holds" (Bool (Set (Var "A")) "is" ($#v13_osalg_1 :::"monotone"::: ) ))) ; definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "z" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "z1" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "z")); func :::"TrivialOSA"::: "(" "S" "," "z" "," "z1" ")" -> ($#v3_msualg_1 :::"strict"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" "S" means :: OSALG_1:def 22 (Bool "(" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" it) ($#r8_pboole :::"="::: ) (Set ($#k3_osalg_1 :::"ConstOSSet"::: ) "(" "S" "," "z" ")" )) & (Bool "(" "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" "S" "holds" (Bool (Set ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," it ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," it ")" ")" ) ($#k8_funcop_1 :::"-->"::: ) "z1")) ")" ) ")" ); end; :: deftheorem defines :::"TrivialOSA"::: OSALG_1:def 22 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "z1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "z")) (Bool "for" (Set (Var "b4")) "being" ($#v3_msualg_1 :::"strict"::: ) ($#l3_msualg_1 :::"OSAlgebra":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k6_osalg_1 :::"TrivialOSA"::: ) "(" (Set (Var "S")) "," (Set (Var "z")) "," (Set (Var "z1")) ")" )) "iff" (Bool "(" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "b4"))) ($#r8_pboole :::"="::: ) (Set ($#k3_osalg_1 :::"ConstOSSet"::: ) "(" (Set (Var "S")) "," (Set (Var "z")) ")" )) & (Bool "(" "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set (Var "b4")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "b4")) ")" ")" ) ($#k8_funcop_1 :::"-->"::: ) (Set (Var "z1")))) ")" ) ")" ) ")" ))))); theorem :: OSALG_1:29 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "z1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "z")) "holds" (Bool "(" (Bool (Set ($#k6_osalg_1 :::"TrivialOSA"::: ) "(" (Set (Var "S")) "," (Set (Var "z")) "," (Set (Var "z1")) ")" ) "is" ($#v4_msualg_1 :::"non-empty"::: ) ) & (Bool (Set ($#k6_osalg_1 :::"TrivialOSA"::: ) "(" (Set (Var "S")) "," (Set (Var "z")) "," (Set (Var "z1")) ")" ) "is" ($#v13_osalg_1 :::"monotone"::: ) ) ")" )))) ; 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 "z" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "z1" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "z")); cluster (Set ($#k6_osalg_1 :::"TrivialOSA"::: ) "(" "S" "," "z" "," "z1" ")" ) -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v13_osalg_1 :::"monotone"::: ) ; end; definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); func :::"OperNames"::: "S" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S") equals :: OSALG_1:def 23 (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "the" ($#u1_osalg_1 :::"Overloading"::: ) "of" "S")); end; :: deftheorem defines :::"OperNames"::: OSALG_1:def 23 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) "holds" (Bool (Set ($#k7_osalg_1 :::"OperNames"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "the" ($#u1_osalg_1 :::"Overloading"::: ) "of" (Set (Var "S")))))); registrationlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); cluster -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_osalg_1 :::"OperNames"::: ) "S"); end; definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); mode OperName of "S" is ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_osalg_1 :::"OperNames"::: ) "S"); end; definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "op1" be ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); func :::"Name"::: "op1" -> ($#m2_subset_1 :::"OperName":::) "of" "S" equals :: OSALG_1:def 24 (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "the" ($#u1_osalg_1 :::"Overloading"::: ) "of" "S") "," "op1" ")" ); end; :: deftheorem defines :::"Name"::: OSALG_1:def 24 : (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "op1")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k8_osalg_1 :::"Name"::: ) (Set (Var "op1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "the" ($#u1_osalg_1 :::"Overloading"::: ) "of" (Set (Var "S"))) "," (Set (Var "op1")) ")" )))); theorem :: OSALG_1:30 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "op1")) "," (Set (Var "op2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "op1")) ($#r1_osalg_1 :::"~="::: ) (Set (Var "op2"))) "iff" (Bool (Set (Var "op2")) ($#r2_hidden :::"in"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "the" ($#u1_osalg_1 :::"Overloading"::: ) "of" (Set (Var "S"))) "," (Set (Var "op1")) ")" )) ")" ))) ; theorem :: OSALG_1:31 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "op1")) "," (Set (Var "op2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "op1")) ($#r1_osalg_1 :::"~="::: ) (Set (Var "op2"))) "iff" (Bool (Set ($#k8_osalg_1 :::"Name"::: ) (Set (Var "op1"))) ($#r1_hidden :::"="::: ) (Set ($#k8_osalg_1 :::"Name"::: ) (Set (Var "op2")))) ")" ))) ; theorem :: OSALG_1:32 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#m2_subset_1 :::"OperName":::) "of" (Set (Var "S"))) "iff" (Bool "ex" (Set (Var "op1")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k8_osalg_1 :::"Name"::: ) (Set (Var "op1"))))) ")" ))) ; definitionlet "S" be ($#l3_osalg_1 :::"OrderSortedSign":::); let "o" be ($#m2_subset_1 :::"OperName":::) "of" (Set (Const "S")); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "o" -> ($#m1_subset_1 :::"OperSymbol":::) "of" "S"; end; theorem :: OSALG_1:33 (Bool "for" (Set (Var "S")) "being" ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "on")) "being" ($#m2_subset_1 :::"OperName":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "op")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "op")) "is" ($#m1_osalg_1 :::"Element"::: ) "of" (Set (Var "on"))) "iff" (Bool (Set ($#k8_osalg_1 :::"Name"::: ) (Set (Var "op"))) ($#r1_hidden :::"="::: ) (Set (Var "on"))) ")" )))) ; theorem :: OSALG_1:34 (Bool "for" (Set (Var "SR")) "being" ($#v8_osalg_1 :::"monotone"::: ) ($#v10_osalg_1 :::"regular"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "op1")) "," (Set (Var "op2")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "SR")) (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "SR"))) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "op1")) ($#r1_osalg_1 :::"~="::: ) (Set (Var "op2"))) & (Bool (Set (Var "w")) ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "op1")))) & (Bool (Set (Var "w")) ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "op2"))))) "holds" (Bool (Set ($#k2_osalg_1 :::"LBound"::: ) "(" (Set (Var "op1")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_osalg_1 :::"LBound"::: ) "(" (Set (Var "op2")) "," (Set (Var "w")) ")" ))))) ; definitionlet "SR" be ($#v8_osalg_1 :::"monotone"::: ) ($#v10_osalg_1 :::"regular"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::); let "on" be ($#m2_subset_1 :::"OperName":::) "of" (Set (Const "SR")); let "w" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "SR"))) ($#k3_finseq_2 :::"*"::: ) ); assume (Bool "ex" (Set (Var "op")) "being" ($#m1_osalg_1 :::"Element"::: ) "of" (Set (Const "on")) "st" (Bool (Set (Const "w")) ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "op"))))) ; func :::"LBound"::: "(" "on" "," "w" ")" -> ($#m1_osalg_1 :::"Element"::: ) "of" "on" means :: OSALG_1:def 25 (Bool "for" (Set (Var "op")) "being" ($#m1_osalg_1 :::"Element"::: ) "of" "on" "st" (Bool (Bool "w" ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "op"))))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k2_osalg_1 :::"LBound"::: ) "(" (Set (Var "op")) "," "w" ")" ))); end; :: deftheorem defines :::"LBound"::: OSALG_1:def 25 : (Bool "for" (Set (Var "SR")) "being" ($#v8_osalg_1 :::"monotone"::: ) ($#v10_osalg_1 :::"regular"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "on")) "being" ($#m2_subset_1 :::"OperName":::) "of" (Set (Var "SR")) (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "SR"))) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool "ex" (Set (Var "op")) "being" ($#m1_osalg_1 :::"Element"::: ) "of" (Set (Var "on")) "st" (Bool (Set (Var "w")) ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "op")))))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_osalg_1 :::"Element"::: ) "of" (Set (Var "on")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k9_osalg_1 :::"LBound"::: ) "(" (Set (Var "on")) "," (Set (Var "w")) ")" )) "iff" (Bool "for" (Set (Var "op")) "being" ($#m1_osalg_1 :::"Element"::: ) "of" (Set (Var "on")) "st" (Bool (Bool (Set (Var "w")) ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "op"))))) "holds" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_osalg_1 :::"LBound"::: ) "(" (Set (Var "op")) "," (Set (Var "w")) ")" ))) ")" ))))); theorem :: OSALG_1:35 (Bool "for" (Set (Var "S")) "being" ($#v8_osalg_1 :::"monotone"::: ) ($#v10_osalg_1 :::"regular"::: ) ($#l3_osalg_1 :::"OrderSortedSign":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "w1")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "w1")) ($#r2_osalg_1 :::"<="::: ) (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o"))))) "holds" (Bool (Set ($#k2_osalg_1 :::"LBound"::: ) "(" (Set (Var "o")) "," (Set (Var "w1")) ")" ) ($#r6_osalg_1 :::"<="::: ) (Set (Var "o")))))) ;