:: MONOID_0 semantic presentation begin definitionlet "G" be ($#l1_struct_0 :::"1-sorted"::: ) ; mode BinOp of "G" is ($#m1_subset_1 :::"BinOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G"); end; definitionlet "IT" be ($#l1_struct_0 :::"1-sorted"::: ) ; attr "IT" is :::"constituted-Functions"::: means :: MONOID_0:def 1 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Var "a")) "is" ($#m1_hidden :::"Function":::))); attr "IT" is :::"constituted-FinSeqs"::: means :: MONOID_0:def 2 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Var "a")) "is" ($#m1_hidden :::"FinSequence":::))); end; :: deftheorem defines :::"constituted-Functions"::: MONOID_0:def 1 : (Bool "for" (Set (Var "IT")) "being" ($#l1_struct_0 :::"1-sorted"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_monoid_0 :::"constituted-Functions"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Var "a")) "is" ($#m1_hidden :::"Function":::))) ")" )); :: deftheorem defines :::"constituted-FinSeqs"::: MONOID_0:def 2 : (Bool "for" (Set (Var "IT")) "being" ($#l1_struct_0 :::"1-sorted"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_monoid_0 :::"constituted-FinSeqs"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Var "a")) "is" ($#m1_hidden :::"FinSequence":::))) ")" )); registration cluster ($#v1_monoid_0 :::"constituted-Functions"::: ) for ($#l1_struct_0 :::"1-sorted"::: ) ; cluster ($#v2_monoid_0 :::"constituted-FinSeqs"::: ) for ($#l1_struct_0 :::"1-sorted"::: ) ; end; registrationlet "X" be ($#v1_monoid_0 :::"constituted-Functions"::: ) ($#l1_struct_0 :::"1-sorted"::: ) ; cluster -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X"); end; registration cluster ($#v2_monoid_0 :::"constituted-FinSeqs"::: ) -> ($#v1_monoid_0 :::"constituted-Functions"::: ) for ($#l1_struct_0 :::"1-sorted"::: ) ; end; registrationlet "X" be ($#v2_monoid_0 :::"constituted-FinSeqs"::: ) ($#l1_struct_0 :::"1-sorted"::: ) ; cluster -> ($#v1_finseq_1 :::"FinSequence-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X"); end; definitionlet "D" be ($#m1_hidden :::"set"::: ) ; let "p", "q" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); :: original: :::"^"::: redefine func "p" :::"^"::: "q" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "D" ($#k3_finseq_2 :::"*"::: ) ); end; notationlet "g", "f" be ($#m1_hidden :::"Function":::); synonym "f" :::"(*)"::: "g" for "f" :::"*"::: "g"; end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "IT" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); attr "IT" is :::"left-invertible"::: means :: MONOID_0:def 3 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "D" (Bool "ex" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "D" "st" (Bool (Set "IT" ($#k5_binop_1 :::"."::: ) "(" (Set (Var "l")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "b"))))); attr "IT" is :::"right-invertible"::: means :: MONOID_0:def 4 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "D" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "D" "st" (Bool (Set "IT" ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "b"))))); attr "IT" is :::"invertible"::: means :: MONOID_0:def 5 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "D" (Bool "ex" (Set (Var "r")) "," (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "D" "st" (Bool "(" (Bool (Set "IT" ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set "IT" ($#k5_binop_1 :::"."::: ) "(" (Set (Var "l")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ))); attr "IT" is :::"left-cancelable"::: means :: MONOID_0:def 6 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "D" "st" (Bool (Bool (Set "IT" ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set "IT" ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c")))); attr "IT" is :::"right-cancelable"::: means :: MONOID_0:def 7 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "D" "st" (Bool (Bool (Set "IT" ($#k5_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set "IT" ($#k5_binop_1 :::"."::: ) "(" (Set (Var "c")) "," (Set (Var "a")) ")" ))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c")))); attr "IT" is :::"cancelable"::: means :: MONOID_0:def 8 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "D" "st" (Bool (Bool "(" (Bool (Set "IT" ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set "IT" ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" )) "or" (Bool (Set "IT" ($#k5_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set "IT" ($#k5_binop_1 :::"."::: ) "(" (Set (Var "c")) "," (Set (Var "a")) ")" )) ")" )) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c")))); attr "IT" is :::"uniquely-decomposable"::: means :: MONOID_0:def 9 (Bool "(" (Bool "IT" "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "D" "st" (Bool (Bool (Set "IT" ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) "IT"))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) "IT")) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"left-invertible"::: MONOID_0:def 3 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_monoid_0 :::"left-invertible"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "ex" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Set (Set (Var "IT")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "l")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ")" ))); :: deftheorem defines :::"right-invertible"::: MONOID_0:def 4 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_monoid_0 :::"right-invertible"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Set (Set (Var "IT")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ")" ))); :: deftheorem defines :::"invertible"::: MONOID_0:def 5 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_monoid_0 :::"invertible"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "ex" (Set (Var "r")) "," (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool "(" (Bool (Set (Set (Var "IT")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Set (Var "IT")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "l")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ))) ")" ))); :: deftheorem defines :::"left-cancelable"::: MONOID_0:def 6 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_monoid_0 :::"left-cancelable"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Set (Var "IT")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "IT")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c")))) ")" ))); :: deftheorem defines :::"right-cancelable"::: MONOID_0:def 7 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v7_monoid_0 :::"right-cancelable"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Set (Var "IT")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "IT")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "c")) "," (Set (Var "a")) ")" ))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c")))) ")" ))); :: deftheorem defines :::"cancelable"::: MONOID_0:def 8 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v8_monoid_0 :::"cancelable"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool "(" (Bool (Set (Set (Var "IT")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "IT")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" )) "or" (Bool (Set (Set (Var "IT")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "IT")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "c")) "," (Set (Var "a")) ")" )) ")" )) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c")))) ")" ))); :: deftheorem defines :::"uniquely-decomposable"::: MONOID_0:def 9 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v9_monoid_0 :::"uniquely-decomposable"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Set (Var "IT")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "IT"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "IT")))) ")" ) ")" ) ")" ) ")" ))); theorem :: MONOID_0:1 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_monoid_0 :::"invertible"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_monoid_0 :::"left-invertible"::: ) ) & (Bool (Set (Var "f")) "is" ($#v4_monoid_0 :::"right-invertible"::: ) ) ")" ) ")" ))) ; theorem :: MONOID_0:2 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v8_monoid_0 :::"cancelable"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v6_monoid_0 :::"left-cancelable"::: ) ) & (Bool (Set (Var "f")) "is" ($#v7_monoid_0 :::"right-cancelable"::: ) ) ")" ) ")" ))) ; theorem :: MONOID_0:3 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "x")) "," (Set (Var "x")) ")" ($#k13_funcop_1 :::".-->"::: ) (Set (Var "x")))) & (Bool (Set (Var "f")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "f")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "f")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "f")) "is" ($#v3_binop_1 :::"idempotent"::: ) ) & (Bool (Set (Var "f")) "is" ($#v5_monoid_0 :::"invertible"::: ) ) & (Bool (Set (Var "f")) "is" ($#v8_monoid_0 :::"cancelable"::: ) ) & (Bool (Set (Var "f")) "is" ($#v9_monoid_0 :::"uniquely-decomposable"::: ) ) ")" ))) ; begin definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; redefine attr "IT" is :::"unital"::: means :: MONOID_0:def 10 (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "IT") "is" ($#v1_setwiseo :::"having_a_unity"::: ) ); end; :: deftheorem defines :::"unital"::: MONOID_0:def 10 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_group_1 :::"unital"::: ) ) "iff" (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "IT"))) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) ")" )); definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; redefine attr "G" is :::"commutative"::: means :: MONOID_0:def 11 (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "G") "is" ($#v1_binop_1 :::"commutative"::: ) ); redefine attr "G" is :::"associative"::: means :: MONOID_0:def 12 (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "G") "is" ($#v2_binop_1 :::"associative"::: ) ); end; :: deftheorem defines :::"commutative"::: MONOID_0:def 11 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v5_group_1 :::"commutative"::: ) ) "iff" (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G"))) "is" ($#v1_binop_1 :::"commutative"::: ) ) ")" )); :: deftheorem defines :::"associative"::: MONOID_0:def 12 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_group_1 :::"associative"::: ) ) "iff" (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G"))) "is" ($#v2_binop_1 :::"associative"::: ) ) ")" )); definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; attr "IT" is :::"idempotent"::: means :: MONOID_0:def 13 (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "IT") "is" ($#v3_binop_1 :::"idempotent"::: ) ); attr "IT" is :::"left-invertible"::: means :: MONOID_0:def 14 (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "IT") "is" ($#v3_monoid_0 :::"left-invertible"::: ) ); attr "IT" is :::"right-invertible"::: means :: MONOID_0:def 15 (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "IT") "is" ($#v4_monoid_0 :::"right-invertible"::: ) ); attr "IT" is :::"invertible"::: means :: MONOID_0:def 16 (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "IT") "is" ($#v5_monoid_0 :::"invertible"::: ) ); attr "IT" is :::"left-cancelable"::: means :: MONOID_0:def 17 (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "IT") "is" ($#v6_monoid_0 :::"left-cancelable"::: ) ); attr "IT" is :::"right-cancelable"::: means :: MONOID_0:def 18 (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "IT") "is" ($#v7_monoid_0 :::"right-cancelable"::: ) ); attr "IT" is :::"cancelable"::: means :: MONOID_0:def 19 (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "IT") "is" ($#v8_monoid_0 :::"cancelable"::: ) ); attr "IT" is :::"uniquely-decomposable"::: means :: MONOID_0:def 20 (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "IT") "is" ($#v9_monoid_0 :::"uniquely-decomposable"::: ) ); end; :: deftheorem defines :::"idempotent"::: MONOID_0:def 13 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v10_monoid_0 :::"idempotent"::: ) ) "iff" (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "IT"))) "is" ($#v3_binop_1 :::"idempotent"::: ) ) ")" )); :: deftheorem defines :::"left-invertible"::: MONOID_0:def 14 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v11_monoid_0 :::"left-invertible"::: ) ) "iff" (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "IT"))) "is" ($#v3_monoid_0 :::"left-invertible"::: ) ) ")" )); :: deftheorem defines :::"right-invertible"::: MONOID_0:def 15 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v12_monoid_0 :::"right-invertible"::: ) ) "iff" (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "IT"))) "is" ($#v4_monoid_0 :::"right-invertible"::: ) ) ")" )); :: deftheorem defines :::"invertible"::: MONOID_0:def 16 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v13_monoid_0 :::"invertible"::: ) ) "iff" (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "IT"))) "is" ($#v5_monoid_0 :::"invertible"::: ) ) ")" )); :: deftheorem defines :::"left-cancelable"::: MONOID_0:def 17 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v14_monoid_0 :::"left-cancelable"::: ) ) "iff" (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "IT"))) "is" ($#v6_monoid_0 :::"left-cancelable"::: ) ) ")" )); :: deftheorem defines :::"right-cancelable"::: MONOID_0:def 18 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v15_monoid_0 :::"right-cancelable"::: ) ) "iff" (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "IT"))) "is" ($#v7_monoid_0 :::"right-cancelable"::: ) ) ")" )); :: deftheorem defines :::"cancelable"::: MONOID_0:def 19 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v16_monoid_0 :::"cancelable"::: ) ) "iff" (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "IT"))) "is" ($#v8_monoid_0 :::"cancelable"::: ) ) ")" )); :: deftheorem defines :::"uniquely-decomposable"::: MONOID_0:def 20 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v17_monoid_0 :::"uniquely-decomposable"::: ) ) "iff" (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "IT"))) "is" ($#v9_monoid_0 :::"uniquely-decomposable"::: ) ) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v1_monoid_0 :::"constituted-Functions"::: ) ($#v2_monoid_0 :::"constituted-FinSeqs"::: ) ($#v10_monoid_0 :::"idempotent"::: ) ($#v13_monoid_0 :::"invertible"::: ) ($#v16_monoid_0 :::"cancelable"::: ) ($#v17_monoid_0 :::"uniquely-decomposable"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; end; theorem :: MONOID_0:4 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "st" (Bool (Bool (Set (Var "G")) "is" ($#v1_group_1 :::"unital"::: ) )) "holds" (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G")))) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G"))))) ; theorem :: MONOID_0:5 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v1_group_1 :::"unital"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G"))) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G"))) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" )) ")" )) ; theorem :: MONOID_0:6 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v1_group_1 :::"unital"::: ) ) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ))) ")" )) ; theorem :: MONOID_0:7 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v10_monoid_0 :::"idempotent"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ")" )) ; theorem :: MONOID_0:8 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v11_monoid_0 :::"left-invertible"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "ex" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Set (Set (Var "l")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ")" )) ; theorem :: MONOID_0:9 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v12_monoid_0 :::"right-invertible"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ")" )) ; theorem :: MONOID_0:10 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v13_monoid_0 :::"invertible"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "ex" (Set (Var "r")) "," (Set (Var "l")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Set (Var "l")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ))) ")" )) ; theorem :: MONOID_0:11 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v14_monoid_0 :::"left-cancelable"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "c"))))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c")))) ")" )) ; theorem :: MONOID_0:12 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v15_monoid_0 :::"right-cancelable"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c")))) ")" )) ; theorem :: MONOID_0:13 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v16_monoid_0 :::"cancelable"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool "(" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "c")))) "or" (Bool (Set (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a")))) ")" )) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c")))) ")" )) ; theorem :: MONOID_0:14 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v17_monoid_0 :::"uniquely-decomposable"::: ) ) "iff" (Bool "(" (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G"))) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G")))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G"))))) ")" ) ")" ) ")" ) ")" )) ; theorem :: MONOID_0:15 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_group_1 :::"associative"::: ) )) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v13_monoid_0 :::"invertible"::: ) ) "iff" (Bool "(" (Bool (Set (Var "G")) "is" ($#v1_group_1 :::"unital"::: ) ) & (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G"))) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) ")" ) ")" )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_monoid_0 :::"invertible"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v13_monoid_0 :::"invertible"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_monoid_0 :::"invertible"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_monoid_0 :::"left-invertible"::: ) ($#v12_monoid_0 :::"right-invertible"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_monoid_0 :::"left-invertible"::: ) ($#v12_monoid_0 :::"right-invertible"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_monoid_0 :::"invertible"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_monoid_0 :::"cancelable"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v14_monoid_0 :::"left-cancelable"::: ) ($#v15_monoid_0 :::"right-cancelable"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v14_monoid_0 :::"left-cancelable"::: ) ($#v15_monoid_0 :::"right-cancelable"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_monoid_0 :::"cancelable"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v13_monoid_0 :::"invertible"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#v16_monoid_0 :::"cancelable"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; end; begin definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; redefine attr "IT" is :::"well-unital"::: means :: MONOID_0:def 21 (Bool (Set ($#k5_struct_0 :::"1."::: ) "IT") ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "IT")); end; :: deftheorem defines :::"well-unital"::: MONOID_0:def 21 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_vectsp_1 :::"well-unital"::: ) ) "iff" (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "IT"))) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "IT")))) ")" )); theorem :: MONOID_0:16 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v4_vectsp_1 :::"well-unital"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "M")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" )) ")" )) ; theorem :: MONOID_0:17 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) "st" (Bool (Bool (Set (Var "M")) "is" ($#v4_vectsp_1 :::"well-unital"::: ) )) "holds" (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "M")))))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v22_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v1_monoid_0 :::"constituted-Functions"::: ) ($#v2_monoid_0 :::"constituted-FinSeqs"::: ) ($#v10_monoid_0 :::"idempotent"::: ) ($#v13_monoid_0 :::"invertible"::: ) ($#v16_monoid_0 :::"cancelable"::: ) ($#v17_monoid_0 :::"uniquely-decomposable"::: ) for ($#l4_algstr_0 :::"multLoopStr"::: ) ; end; definitionmode Monoid is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; end; definitionlet "G" be ($#l3_algstr_0 :::"multMagma"::: ) ; mode :::"MonoidalExtension"::: "of" "G" -> ($#l4_algstr_0 :::"multLoopStr"::: ) means :: MONOID_0:def 22 (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" it) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "G") "#)" )); end; :: deftheorem defines :::"MonoidalExtension"::: MONOID_0:def 22 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "b2")) "being" ($#l4_algstr_0 :::"multLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_monoid_0 :::"MonoidalExtension"::: ) "of" (Set (Var "G"))) "iff" (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "b2"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G"))) "#)" )) ")" ))); registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#m1_monoid_0 :::"MonoidalExtension"::: ) "of" "G"; end; theorem :: MONOID_0:18 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_monoid_0 :::"MonoidalExtension"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))) & (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "M"))) ($#r1_funct_2 :::"="::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G")))) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "a9")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "a9"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "b9")))) "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a9")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b9"))))) ")" ) ")" ))) ; registrationlet "G" be ($#l3_algstr_0 :::"multMagma"::: ) ; cluster ($#v22_algstr_0 :::"strict"::: ) for ($#m1_monoid_0 :::"MonoidalExtension"::: ) "of" "G"; end; theorem :: MONOID_0:19 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_monoid_0 :::"MonoidalExtension"::: ) "of" (Set (Var "G")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "G")) "is" ($#v1_group_1 :::"unital"::: ) )) "implies" (Bool (Set (Var "M")) "is" ($#v1_group_1 :::"unital"::: ) ) ")" & "(" (Bool (Bool (Set (Var "G")) "is" ($#v5_group_1 :::"commutative"::: ) )) "implies" (Bool (Set (Var "M")) "is" ($#v5_group_1 :::"commutative"::: ) ) ")" & "(" (Bool (Bool (Set (Var "G")) "is" ($#v3_group_1 :::"associative"::: ) )) "implies" (Bool (Set (Var "M")) "is" ($#v3_group_1 :::"associative"::: ) ) ")" & "(" (Bool (Bool (Set (Var "G")) "is" ($#v13_monoid_0 :::"invertible"::: ) )) "implies" (Bool (Set (Var "M")) "is" ($#v13_monoid_0 :::"invertible"::: ) ) ")" & "(" (Bool (Bool (Set (Var "G")) "is" ($#v17_monoid_0 :::"uniquely-decomposable"::: ) )) "implies" (Bool (Set (Var "M")) "is" ($#v17_monoid_0 :::"uniquely-decomposable"::: ) ) ")" & "(" (Bool (Bool (Set (Var "G")) "is" ($#v16_monoid_0 :::"cancelable"::: ) )) "implies" (Bool (Set (Var "M")) "is" ($#v16_monoid_0 :::"cancelable"::: ) ) ")" ")" ))) ; registrationlet "G" be ($#v1_monoid_0 :::"constituted-Functions"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster -> ($#v1_monoid_0 :::"constituted-Functions"::: ) for ($#m1_monoid_0 :::"MonoidalExtension"::: ) "of" "G"; end; registrationlet "G" be ($#v2_monoid_0 :::"constituted-FinSeqs"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster -> ($#v2_monoid_0 :::"constituted-FinSeqs"::: ) for ($#m1_monoid_0 :::"MonoidalExtension"::: ) "of" "G"; end; registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster -> ($#v1_group_1 :::"unital"::: ) for ($#m1_monoid_0 :::"MonoidalExtension"::: ) "of" "G"; end; registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster -> ($#v3_group_1 :::"associative"::: ) for ($#m1_monoid_0 :::"MonoidalExtension"::: ) "of" "G"; end; registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster -> ($#v5_group_1 :::"commutative"::: ) for ($#m1_monoid_0 :::"MonoidalExtension"::: ) "of" "G"; end; registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_monoid_0 :::"invertible"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster -> ($#v13_monoid_0 :::"invertible"::: ) for ($#m1_monoid_0 :::"MonoidalExtension"::: ) "of" "G"; end; registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_monoid_0 :::"cancelable"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster -> ($#v16_monoid_0 :::"cancelable"::: ) for ($#m1_monoid_0 :::"MonoidalExtension"::: ) "of" "G"; end; registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v17_monoid_0 :::"uniquely-decomposable"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster -> ($#v17_monoid_0 :::"uniquely-decomposable"::: ) for ($#m1_monoid_0 :::"MonoidalExtension"::: ) "of" "G"; end; registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v22_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) for ($#m1_monoid_0 :::"MonoidalExtension"::: ) "of" "G"; end; theorem :: MONOID_0:20 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#v22_algstr_0 :::"strict"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#m1_monoid_0 :::"MonoidalExtension"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Var "M1")) ($#r1_hidden :::"="::: ) (Set (Var "M2"))))) ; begin definitionlet "G" be ($#l3_algstr_0 :::"multMagma"::: ) ; mode :::"SubStr"::: "of" "G" -> ($#l3_algstr_0 :::"multMagma"::: ) means :: MONOID_0:def 23 (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" it) ($#r1_tarski :::"c="::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "G")); end; :: deftheorem defines :::"SubStr"::: MONOID_0:def 23 : (Bool "for" (Set (Var "G")) "," (Set (Var "b2")) "being" ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set (Var "G"))) "iff" (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "b2"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G")))) ")" )); registrationlet "G" be ($#l3_algstr_0 :::"multMagma"::: ) ; cluster ($#v15_algstr_0 :::"strict"::: ) for ($#m2_monoid_0 :::"SubStr"::: ) "of" "G"; end; registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) for ($#m2_monoid_0 :::"SubStr"::: ) "of" "G"; end; registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v10_monoid_0 :::"idempotent"::: ) ($#v13_monoid_0 :::"invertible"::: ) ($#v16_monoid_0 :::"cancelable"::: ) ($#v17_monoid_0 :::"uniquely-decomposable"::: ) for ($#m2_monoid_0 :::"SubStr"::: ) "of" "G"; end; definitionlet "G" be ($#l3_algstr_0 :::"multMagma"::: ) ; mode :::"MonoidalSubStr"::: "of" "G" -> ($#l4_algstr_0 :::"multLoopStr"::: ) means :: MONOID_0:def 24 (Bool "(" (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" it) ($#r1_tarski :::"c="::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "G")) & (Bool "(" "for" (Set (Var "M")) "being" ($#l4_algstr_0 :::"multLoopStr"::: ) "st" (Bool (Bool "G" ($#r1_hidden :::"="::: ) (Set (Var "M")))) "holds" (Bool (Set ($#k5_struct_0 :::"1."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "M")))) ")" ) ")" ); end; :: deftheorem defines :::"MonoidalSubStr"::: MONOID_0:def 24 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "b2")) "being" ($#l4_algstr_0 :::"multLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m3_monoid_0 :::"MonoidalSubStr"::: ) "of" (Set (Var "G"))) "iff" (Bool "(" (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "b2"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G")))) & (Bool "(" "for" (Set (Var "M")) "being" ($#l4_algstr_0 :::"multLoopStr"::: ) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Var "M")))) "holds" (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "M")))) ")" ) ")" ) ")" ))); registrationlet "G" be ($#l3_algstr_0 :::"multMagma"::: ) ; cluster ($#v22_algstr_0 :::"strict"::: ) for ($#m3_monoid_0 :::"MonoidalSubStr"::: ) "of" "G"; end; registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v22_algstr_0 :::"strict"::: ) for ($#m3_monoid_0 :::"MonoidalSubStr"::: ) "of" "G"; end; definitionlet "M" be ($#l4_algstr_0 :::"multLoopStr"::: ) ; redefine mode :::"MonoidalSubStr"::: "of" "M" means :: MONOID_0:def 25 (Bool "(" (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" it) ($#r1_tarski :::"c="::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "M")) & (Bool (Set ($#k5_struct_0 :::"1."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "M")) ")" ); end; :: deftheorem defines :::"MonoidalSubStr"::: MONOID_0:def 25 : (Bool "for" (Set (Var "M")) "," (Set (Var "b2")) "being" ($#l4_algstr_0 :::"multLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m3_monoid_0 :::"MonoidalSubStr"::: ) "of" (Set (Var "M"))) "iff" (Bool "(" (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "b2"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "M")))) & (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "M")))) ")" ) ")" )); registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v22_algstr_0 :::"strict"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v10_monoid_0 :::"idempotent"::: ) ($#v13_monoid_0 :::"invertible"::: ) ($#v16_monoid_0 :::"cancelable"::: ) ($#v17_monoid_0 :::"uniquely-decomposable"::: ) for ($#m3_monoid_0 :::"MonoidalSubStr"::: ) "of" "G"; end; theorem :: MONOID_0:21 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "M")) "being" ($#m3_monoid_0 :::"MonoidalSubStr"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Var "M")) "is" ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set (Var "G"))))) ; definitionlet "G" be ($#l3_algstr_0 :::"multMagma"::: ) ; let "M" be ($#m1_monoid_0 :::"MonoidalExtension"::: ) "of" (Set (Const "G")); :: original: :::"SubStr"::: redefine mode :::"SubStr"::: "of" "M" -> ($#m2_monoid_0 :::"SubStr"::: ) "of" "G"; end; definitionlet "G1" be ($#l3_algstr_0 :::"multMagma"::: ) ; let "G2" be ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set (Const "G1")); :: original: :::"SubStr"::: redefine mode :::"SubStr"::: "of" "G2" -> ($#m2_monoid_0 :::"SubStr"::: ) "of" "G1"; end; definitionlet "G1" be ($#l3_algstr_0 :::"multMagma"::: ) ; let "G2" be ($#m3_monoid_0 :::"MonoidalSubStr"::: ) "of" (Set (Const "G1")); :: original: :::"SubStr"::: redefine mode :::"SubStr"::: "of" "G2" -> ($#m2_monoid_0 :::"SubStr"::: ) "of" "G1"; end; definitionlet "G" be ($#l3_algstr_0 :::"multMagma"::: ) ; let "M" be ($#m3_monoid_0 :::"MonoidalSubStr"::: ) "of" (Set (Const "G")); :: original: :::"MonoidalSubStr"::: redefine mode :::"MonoidalSubStr"::: "of" "M" -> ($#m3_monoid_0 :::"MonoidalSubStr"::: ) "of" "G"; end; theorem :: MONOID_0:22 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set (Var "G"))) & (Bool (Set (Var "M")) "is" ($#m3_monoid_0 :::"MonoidalSubStr"::: ) "of" (Set (Var "M"))) ")" ))) ; theorem :: MONOID_0:23 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m3_monoid_0 :::"MonoidalSubStr"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))) ")" )))) ; theorem :: MONOID_0:24 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set (Var "G")) "holds" (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G"))) ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))))))) ; theorem :: MONOID_0:25 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) (Bool "for" (Set (Var "a9")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "a9"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "b9")))) "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a9")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b9")))))))) ; theorem :: MONOID_0:26 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2"))))) "holds" (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "H1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "H2"))) "#)" )))) ; theorem :: MONOID_0:27 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m3_monoid_0 :::"MonoidalSubStr"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2"))))) "holds" (Bool (Set ($#g4_algstr_0 :::"multLoopStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "H1"))) "," (Set "the" ($#u3_struct_0 :::"OneF"::: ) "of" (Set (Var "H1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g4_algstr_0 :::"multLoopStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "H2"))) "," (Set "the" ($#u3_struct_0 :::"OneF"::: ) "of" (Set (Var "H2"))) "#)" )))) ; theorem :: MONOID_0:28 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2"))))) "holds" (Bool (Set (Var "H1")) "is" ($#m5_monoid_0 :::"SubStr"::: ) "of" (Set (Var "H2"))))) ; theorem :: MONOID_0:29 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m3_monoid_0 :::"MonoidalSubStr"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2"))))) "holds" (Bool (Set (Var "H1")) "is" ($#m7_monoid_0 :::"MonoidalSubStr"::: ) "of" (Set (Var "H2"))))) ; theorem :: MONOID_0:30 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v1_group_1 :::"unital"::: ) ) & (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G")))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))))) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v1_group_1 :::"unital"::: ) ) & (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G")))) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "H"))))) ")" ))) ; theorem :: MONOID_0:31 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m3_monoid_0 :::"MonoidalSubStr"::: ) "of" (Set (Var "M")) "holds" (Bool (Set (Var "N")) "is" ($#v4_vectsp_1 :::"well-unital"::: ) ))) ; theorem :: MONOID_0:32 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v5_group_1 :::"commutative"::: ) )) "holds" (Bool (Set (Var "H")) "is" ($#v5_group_1 :::"commutative"::: ) ))) ; theorem :: MONOID_0:33 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_group_1 :::"associative"::: ) )) "holds" (Bool (Set (Var "H")) "is" ($#v3_group_1 :::"associative"::: ) ))) ; theorem :: MONOID_0:34 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v10_monoid_0 :::"idempotent"::: ) )) "holds" (Bool (Set (Var "H")) "is" ($#v10_monoid_0 :::"idempotent"::: ) ))) ; theorem :: MONOID_0:35 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v16_monoid_0 :::"cancelable"::: ) )) "holds" (Bool (Set (Var "H")) "is" ($#v16_monoid_0 :::"cancelable"::: ) ))) ; theorem :: MONOID_0:36 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G")))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H")))) & (Bool (Set (Var "G")) "is" ($#v17_monoid_0 :::"uniquely-decomposable"::: ) )) "holds" (Bool (Set (Var "H")) "is" ($#v17_monoid_0 :::"uniquely-decomposable"::: ) ))) ; theorem :: MONOID_0:37 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v17_monoid_0 :::"uniquely-decomposable"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m3_monoid_0 :::"MonoidalSubStr"::: ) "of" (Set (Var "M")) "holds" (Bool (Set (Var "N")) "is" ($#v17_monoid_0 :::"uniquely-decomposable"::: ) ))) ; registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_monoid_0 :::"constituted-Functions"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_monoid_0 :::"constituted-Functions"::: ) for ($#m2_monoid_0 :::"SubStr"::: ) "of" "G"; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_monoid_0 :::"constituted-Functions"::: ) for ($#m3_monoid_0 :::"MonoidalSubStr"::: ) "of" "G"; end; registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_monoid_0 :::"constituted-FinSeqs"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_monoid_0 :::"constituted-FinSeqs"::: ) for ($#m2_monoid_0 :::"SubStr"::: ) "of" "G"; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_monoid_0 :::"constituted-FinSeqs"::: ) for ($#m3_monoid_0 :::"MonoidalSubStr"::: ) "of" "G"; end; registrationlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) for ($#m3_monoid_0 :::"MonoidalSubStr"::: ) "of" "M"; end; registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) for ($#m2_monoid_0 :::"SubStr"::: ) "of" "G"; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) for ($#m3_monoid_0 :::"MonoidalSubStr"::: ) "of" "G"; end; registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) for ($#m2_monoid_0 :::"SubStr"::: ) "of" "G"; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) for ($#m3_monoid_0 :::"MonoidalSubStr"::: ) "of" "G"; end; registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_monoid_0 :::"idempotent"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_monoid_0 :::"idempotent"::: ) for ($#m2_monoid_0 :::"SubStr"::: ) "of" "G"; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_monoid_0 :::"idempotent"::: ) for ($#m3_monoid_0 :::"MonoidalSubStr"::: ) "of" "G"; end; registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_monoid_0 :::"cancelable"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_monoid_0 :::"cancelable"::: ) for ($#m2_monoid_0 :::"SubStr"::: ) "of" "G"; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_monoid_0 :::"cancelable"::: ) for ($#m3_monoid_0 :::"MonoidalSubStr"::: ) "of" "G"; end; registrationlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v17_monoid_0 :::"uniquely-decomposable"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v17_monoid_0 :::"uniquely-decomposable"::: ) for ($#m3_monoid_0 :::"MonoidalSubStr"::: ) "of" "M"; end; scheme :: MONOID_0:sch 1 SubStrEx2{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set F1 "(" ")" ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H")))) "iff" (Bool P1[(Set (Var "x"))]) ")" ))) provided (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "x"))]) & (Bool P1[(Set (Var "y"))])) "holds" (Bool P1[(Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")))])) and (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" ) "st" (Bool P1[(Set (Var "x"))])) proof end; scheme :: MONOID_0:sch 2 MonoidalSubStrEx2{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v22_algstr_0 :::"strict"::: ) ($#m3_monoid_0 :::"MonoidalSubStr"::: ) "of" (Set F1 "(" ")" ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M")))) "iff" (Bool P1[(Set (Var "x"))]) ")" ))) provided (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "x"))]) & (Bool P1[(Set (Var "y"))])) "holds" (Bool P1[(Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")))])) and (Bool P1[(Set ($#k5_struct_0 :::"1."::: ) (Set F1 "(" ")" ))]) proof end; notationlet "G" be ($#l3_algstr_0 :::"multMagma"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); synonym "a" :::"[*]"::: "b" for "a" :::"*"::: "b"; end; begin definitionfunc :::""::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) equals :: MONOID_0:def 26 (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k33_binop_2 :::"addreal"::: ) ) "#)" ); end; :: deftheorem defines :::""::: MONOID_0:def 26 : (Bool (Set ($#k2_monoid_0 :::""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k33_binop_2 :::"addreal"::: ) ) "#)" )); registration cluster (Set ($#k2_monoid_0 :::""::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v13_monoid_0 :::"invertible"::: ) ($#v16_monoid_0 :::"cancelable"::: ) ; end; theorem :: MONOID_0:38 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k2_monoid_0 :::""::: ) )) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Real":::)) ")" )) ; theorem :: MONOID_0:39 (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set ($#k2_monoid_0 :::""::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k9_binop_2 :::"+"::: ) (Set (Var "y"))))))) ; theorem :: MONOID_0:40 (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set ($#k2_monoid_0 :::""::: ) ) "holds" (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "N")))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v13_monoid_0 :::"invertible"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#v2_group_1 :::"Group-like"::: ) ($#v16_monoid_0 :::"cancelable"::: ) for ($#m2_monoid_0 :::"SubStr"::: ) "of" "G"; end; definition:: original: :::"INT.Group"::: redefine func :::"INT.Group"::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set ($#k2_monoid_0 :::""::: ) ); end; theorem :: MONOID_0:41 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set ($#k2_monoid_0 :::""::: ) ) "holds" (Bool "(" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k3_monoid_0 :::"INT.Group"::: ) )) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k4_numbers :::"INT"::: ) )) ")" )) ; theorem :: MONOID_0:42 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_monoid_0 :::"INT.Group"::: ) )) "iff" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"Integer":::)) ")" )) ; definitionfunc :::""::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v17_monoid_0 :::"uniquely-decomposable"::: ) ($#m5_monoid_0 :::"SubStr"::: ) "of" (Set ($#k3_monoid_0 :::"INT.Group"::: ) ) means :: MONOID_0:def 27 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )); end; :: deftheorem defines :::""::: MONOID_0:def 27 : (Bool "for" (Set (Var "b1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v17_monoid_0 :::"uniquely-decomposable"::: ) ($#m5_monoid_0 :::"SubStr"::: ) "of" (Set ($#k3_monoid_0 :::"INT.Group"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k4_monoid_0 :::""::: ) )) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ")" )); definitionfunc :::""::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v22_algstr_0 :::"strict"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#m1_monoid_0 :::"MonoidalExtension"::: ) "of" (Set ($#k4_monoid_0 :::""::: ) ) means :: MONOID_0:def 28 (Bool verum); end; :: deftheorem defines :::""::: MONOID_0:def 28 : (Bool "for" (Set (Var "b1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v22_algstr_0 :::"strict"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#m1_monoid_0 :::"MonoidalExtension"::: ) "of" (Set ($#k4_monoid_0 :::""::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k5_monoid_0 :::""::: ) )) "iff" (Bool verum) ")" )); definitionredefine func :::"addnat"::: equals :: MONOID_0:def 29 (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set ($#k4_monoid_0 :::""::: ) )); end; :: deftheorem defines :::"addnat"::: MONOID_0:def 29 : (Bool (Set ($#k47_binop_2 :::"addnat"::: ) ) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set ($#k4_monoid_0 :::""::: ) ))); theorem :: MONOID_0:43 (Bool (Set ($#k4_monoid_0 :::""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k47_binop_2 :::"addnat"::: ) ) "#)" )) ; theorem :: MONOID_0:44 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k5_monoid_0 :::""::: ) )) "iff" (Bool (Set (Var "x")) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )) ")" )) ; theorem :: MONOID_0:45 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k5_monoid_0 :::""::: ) ) "st" (Bool (Bool (Set (Var "n1")) ($#r1_hidden :::"="::: ) (Set (Var "m1"))) & (Bool (Set (Var "n2")) ($#r1_hidden :::"="::: ) (Set (Var "m2")))) "holds" (Bool (Set (Set (Var "m1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n1")) ($#k23_binop_2 :::"+"::: ) (Set (Var "n2")))))) ; theorem :: MONOID_0:46 (Bool (Set ($#k5_monoid_0 :::""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g4_algstr_0 :::"multLoopStr"::: ) "(#" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k47_binop_2 :::"addnat"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "#)" )) ; theorem :: MONOID_0:47 (Bool "(" (Bool (Set ($#k47_binop_2 :::"addnat"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k33_binop_2 :::"addreal"::: ) ) ($#k1_realset1 :::"||"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) & (Bool (Set ($#k47_binop_2 :::"addnat"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k44_binop_2 :::"addint"::: ) ) ($#k1_realset1 :::"||"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) ")" ) ; theorem :: MONOID_0:48 (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set ($#k47_binop_2 :::"addnat"::: ) )) & (Bool (Set ($#k47_binop_2 :::"addnat"::: ) ) "is" ($#v9_monoid_0 :::"uniquely-decomposable"::: ) ) ")" ) ; definitionfunc :::""::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) equals :: MONOID_0:def 30 (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k35_binop_2 :::"multreal"::: ) ) "#)" ); end; :: deftheorem defines :::""::: MONOID_0:def 30 : (Bool (Set ($#k6_monoid_0 :::""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k35_binop_2 :::"multreal"::: ) ) "#)" )); theorem :: MONOID_0:49 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k6_monoid_0 :::""::: ) )) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Real":::)) ")" )) ; theorem :: MONOID_0:50 (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set ($#k6_monoid_0 :::""::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k11_binop_2 :::"*"::: ) (Set (Var "y"))))))) ; theorem :: MONOID_0:51 (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set ($#k6_monoid_0 :::""::: ) ) "holds" (Bool "(" (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "N")))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "N")))) ($#r1_hidden :::"="::: ) (Num 1)) ")" )) ; definitionfunc :::""::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v17_monoid_0 :::"uniquely-decomposable"::: ) ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set ($#k6_monoid_0 :::""::: ) ) means :: MONOID_0:def 31 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )); end; :: deftheorem defines :::""::: MONOID_0:def 31 : (Bool "for" (Set (Var "b1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v17_monoid_0 :::"uniquely-decomposable"::: ) ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set ($#k6_monoid_0 :::""::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k7_monoid_0 :::""::: ) )) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ")" )); definitionfunc :::""::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v22_algstr_0 :::"strict"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#m1_monoid_0 :::"MonoidalExtension"::: ) "of" (Set ($#k7_monoid_0 :::""::: ) ) means :: MONOID_0:def 32 (Bool verum); end; :: deftheorem defines :::""::: MONOID_0:def 32 : (Bool "for" (Set (Var "b1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v22_algstr_0 :::"strict"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#m1_monoid_0 :::"MonoidalExtension"::: ) "of" (Set ($#k7_monoid_0 :::""::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k8_monoid_0 :::""::: ) )) "iff" (Bool verum) ")" )); definitionredefine func :::"multnat"::: equals :: MONOID_0:def 33 (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set ($#k7_monoid_0 :::""::: ) )); end; :: deftheorem defines :::"multnat"::: MONOID_0:def 33 : (Bool (Set ($#k48_binop_2 :::"multnat"::: ) ) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set ($#k7_monoid_0 :::""::: ) ))); theorem :: MONOID_0:52 (Bool (Set ($#k7_monoid_0 :::""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k48_binop_2 :::"multnat"::: ) ) "#)" )) ; theorem :: MONOID_0:53 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k7_monoid_0 :::""::: ) ) "st" (Bool (Bool (Set (Var "n1")) ($#r1_hidden :::"="::: ) (Set (Var "m1"))) & (Bool (Set (Var "n2")) ($#r1_hidden :::"="::: ) (Set (Var "m2")))) "holds" (Bool (Set (Set (Var "m1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n1")) ($#k24_binop_2 :::"*"::: ) (Set (Var "n2")))))) ; theorem :: MONOID_0:54 (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set ($#k7_monoid_0 :::""::: ) ))) ($#r1_hidden :::"="::: ) (Num 1)) ; theorem :: MONOID_0:55 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k8_monoid_0 :::""::: ) ) "st" (Bool (Bool (Set (Var "n1")) ($#r1_hidden :::"="::: ) (Set (Var "m1"))) & (Bool (Set (Var "n2")) ($#r1_hidden :::"="::: ) (Set (Var "m2")))) "holds" (Bool (Set (Set (Var "m1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n1")) ($#k24_binop_2 :::"*"::: ) (Set (Var "n2")))))) ; theorem :: MONOID_0:56 (Bool (Set ($#k8_monoid_0 :::""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g4_algstr_0 :::"multLoopStr"::: ) "(#" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k48_binop_2 :::"multnat"::: ) ) "," (Num 1) "#)" )) ; theorem :: MONOID_0:57 (Bool (Set ($#k48_binop_2 :::"multnat"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k35_binop_2 :::"multreal"::: ) ) ($#k1_realset1 :::"||"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) ; theorem :: MONOID_0:58 (Bool "(" (Bool (Num 1) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set ($#k48_binop_2 :::"multnat"::: ) )) & (Bool (Set ($#k48_binop_2 :::"multnat"::: ) ) "is" ($#v9_monoid_0 :::"uniquely-decomposable"::: ) ) ")" ) ; begin definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func "D" :::"*+^"::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v2_monoid_0 :::"constituted-FinSeqs"::: ) ($#v16_monoid_0 :::"cancelable"::: ) ($#v17_monoid_0 :::"uniquely-decomposable"::: ) ($#l3_algstr_0 :::"multMagma"::: ) means :: MONOID_0:def 34 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "D" ($#k3_finseq_2 :::"*"::: ) )) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" it "holds" (Bool (Set (Set (Var "p")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")))) ")" ) ")" ); end; :: deftheorem defines :::"*+^"::: MONOID_0:def 34 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v2_monoid_0 :::"constituted-FinSeqs"::: ) ($#v16_monoid_0 :::"cancelable"::: ) ($#v17_monoid_0 :::"uniquely-decomposable"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "D")) ($#k9_monoid_0 :::"*+^"::: ) )) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) )) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "b2")) "holds" (Bool (Set (Set (Var "p")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")))) ")" ) ")" ) ")" ))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func "D" :::"*+^+<0>"::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v22_algstr_0 :::"strict"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#m1_monoid_0 :::"MonoidalExtension"::: ) "of" (Set "D" ($#k9_monoid_0 :::"*+^"::: ) ) means :: MONOID_0:def 35 (Bool verum); func "D" :::"-concatenation"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" "D" ($#k3_finseq_2 :::"*"::: ) ")" ) equals :: MONOID_0:def 36 (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set "(" "D" ($#k9_monoid_0 :::"*+^"::: ) ")" )); end; :: deftheorem defines :::"*+^+<0>"::: MONOID_0:def 35 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v22_algstr_0 :::"strict"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#m1_monoid_0 :::"MonoidalExtension"::: ) "of" (Set (Set (Var "D")) ($#k9_monoid_0 :::"*+^"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "D")) ($#k10_monoid_0 :::"*+^+<0>"::: ) )) "iff" (Bool verum) ")" ))); :: deftheorem defines :::"-concatenation"::: MONOID_0:def 36 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "D")) ($#k11_monoid_0 :::"-concatenation"::: ) ) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set "(" (Set (Var "D")) ($#k9_monoid_0 :::"*+^"::: ) ")" )))); theorem :: MONOID_0:59 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "D")) ($#k9_monoid_0 :::"*+^"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "(" (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set "(" (Set (Var "D")) ($#k11_monoid_0 :::"-concatenation"::: ) ")" ) "#)" ))) ; theorem :: MONOID_0:60 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set "(" (Set (Var "D")) ($#k9_monoid_0 :::"*+^"::: ) ")" ))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: MONOID_0:61 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "D")) ($#k10_monoid_0 :::"*+^+<0>"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) )) & (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set "(" (Set (Var "D")) ($#k10_monoid_0 :::"*+^+<0>"::: ) ")" )) ($#r1_funct_2 :::"="::: ) (Set (Set (Var "D")) ($#k11_monoid_0 :::"-concatenation"::: ) )) & (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set "(" (Set (Var "D")) ($#k10_monoid_0 :::"*+^+<0>"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: MONOID_0:62 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "D")) ($#k10_monoid_0 :::"*+^+<0>"::: ) ")" ) "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "b")))))) ; theorem :: MONOID_0:63 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set (Set (Var "D")) ($#k9_monoid_0 :::"*+^"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds" (Bool (Set (Set (Var "p")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))))))) ; theorem :: MONOID_0:64 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set (Set (Var "D")) ($#k9_monoid_0 :::"*+^"::: ) ) "holds" (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "F")))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: MONOID_0:65 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set (Set (Var "D")) ($#k9_monoid_0 :::"*+^"::: ) ) "st" (Bool (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")))) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_group_1 :::"unital"::: ) ) & (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "F")))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ; theorem :: MONOID_0:66 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "A")) ($#k9_monoid_0 :::"*+^"::: ) ) "is" ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set (Set (Var "B")) ($#k9_monoid_0 :::"*+^"::: ) ))) ; theorem :: MONOID_0:67 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set (Var "D")) ($#k11_monoid_0 :::"-concatenation"::: ) ) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "(" (Set (Var "D")) ($#k11_monoid_0 :::"-concatenation"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "D")) ($#k11_monoid_0 :::"-concatenation"::: ) ) "is" ($#v2_binop_1 :::"associative"::: ) ) ")" )) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"GPFuncs"::: "X" -> ($#v15_algstr_0 :::"strict"::: ) ($#v1_monoid_0 :::"constituted-Functions"::: ) ($#l3_algstr_0 :::"multMagma"::: ) means :: MONOID_0:def 37 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" "X" "," "X" ")" )) & (Bool "(" "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" it "holds" (Bool (Set (Set (Var "f")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k3_relat_1 :::"(*)"::: ) (Set (Var "f")))) ")" ) ")" ); end; :: deftheorem defines :::"GPFuncs"::: MONOID_0:def 37 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_monoid_0 :::"constituted-Functions"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k12_monoid_0 :::"GPFuncs"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" )) & (Bool "(" "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "b2")) "holds" (Bool (Set (Set (Var "f")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k3_relat_1 :::"(*)"::: ) (Set (Var "f")))) ")" ) ")" ) ")" ))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k12_monoid_0 :::"GPFuncs"::: ) "X") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v1_monoid_0 :::"constituted-Functions"::: ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"MPFuncs"::: "X" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v22_algstr_0 :::"strict"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#m1_monoid_0 :::"MonoidalExtension"::: ) "of" (Set ($#k12_monoid_0 :::"GPFuncs"::: ) "X") means :: MONOID_0:def 38 (Bool verum); func "X" :::"-composition"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" "X" "," "X" ")" ")" ) equals :: MONOID_0:def 39 (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set "(" ($#k12_monoid_0 :::"GPFuncs"::: ) "X" ")" )); end; :: deftheorem defines :::"MPFuncs"::: MONOID_0:def 38 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v22_algstr_0 :::"strict"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#m1_monoid_0 :::"MonoidalExtension"::: ) "of" (Set ($#k12_monoid_0 :::"GPFuncs"::: ) (Set (Var "X"))) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k13_monoid_0 :::"MPFuncs"::: ) (Set (Var "X")))) "iff" (Bool verum) ")" ))); :: deftheorem defines :::"-composition"::: MONOID_0:def 39 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "X")) ($#k14_monoid_0 :::"-composition"::: ) ) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set "(" ($#k12_monoid_0 :::"GPFuncs"::: ) (Set (Var "X")) ")" )))); theorem :: MONOID_0:68 (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k12_monoid_0 :::"GPFuncs"::: ) (Set (Var "X")) ")" )) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "X"))) ")" )) ; theorem :: MONOID_0:69 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set "(" ($#k12_monoid_0 :::"GPFuncs"::: ) (Set (Var "X")) ")" ))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X"))))) ; theorem :: MONOID_0:70 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set ($#k12_monoid_0 :::"GPFuncs"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds" (Bool (Set (Set (Var "f")) ($#k6_algstr_0 :::"[*]"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k3_relat_1 :::"(*)"::: ) (Set (Var "f"))))))) ; theorem :: MONOID_0:71 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set ($#k12_monoid_0 :::"GPFuncs"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X"))) "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")))) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_group_1 :::"unital"::: ) ) & (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "F")))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X")))) ")" ))) ; theorem :: MONOID_0:72 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k12_monoid_0 :::"GPFuncs"::: ) (Set (Var "Y"))) "is" ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set ($#k12_monoid_0 :::"GPFuncs"::: ) (Set (Var "X"))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"GFuncs"::: "X" -> ($#v15_algstr_0 :::"strict"::: ) ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set ($#k12_monoid_0 :::"GPFuncs"::: ) "X") means :: MONOID_0:def 40 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" "X" "," "X" ")" )); end; :: deftheorem defines :::"GFuncs"::: MONOID_0:def 40 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set ($#k12_monoid_0 :::"GPFuncs"::: ) (Set (Var "X"))) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k15_monoid_0 :::"GFuncs"::: ) (Set (Var "X")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" )) ")" ))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k15_monoid_0 :::"GFuncs"::: ) "X") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"MFuncs"::: "X" -> ($#v22_algstr_0 :::"strict"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#m1_monoid_0 :::"MonoidalExtension"::: ) "of" (Set ($#k15_monoid_0 :::"GFuncs"::: ) "X") means :: MONOID_0:def 41 (Bool verum); end; :: deftheorem defines :::"MFuncs"::: MONOID_0:def 41 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v22_algstr_0 :::"strict"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#m1_monoid_0 :::"MonoidalExtension"::: ) "of" (Set ($#k15_monoid_0 :::"GFuncs"::: ) (Set (Var "X"))) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k16_monoid_0 :::"MFuncs"::: ) (Set (Var "X")))) "iff" (Bool verum) ")" ))); theorem :: MONOID_0:73 (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k15_monoid_0 :::"GFuncs"::: ) (Set (Var "X")) ")" )) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X"))) ")" )) ; theorem :: MONOID_0:74 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set "(" ($#k15_monoid_0 :::"GFuncs"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k14_monoid_0 :::"-composition"::: ) ")" ) ($#k1_realset1 :::"||"::: ) (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" )))) ; theorem :: MONOID_0:75 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set "(" ($#k15_monoid_0 :::"GFuncs"::: ) (Set (Var "X")) ")" ))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X"))))) ; theorem :: MONOID_0:76 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k16_monoid_0 :::"MFuncs"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" )) & (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set "(" ($#k16_monoid_0 :::"MFuncs"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k14_monoid_0 :::"-composition"::: ) ")" ) ($#k1_realset1 :::"||"::: ) (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ))) & (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set "(" ($#k16_monoid_0 :::"MFuncs"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X")))) ")" )) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"GPerms"::: "X" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ($#m5_monoid_0 :::"SubStr"::: ) "of" (Set ($#k15_monoid_0 :::"GFuncs"::: ) "X") means :: MONOID_0:def 42 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k15_monoid_0 :::"GFuncs"::: ) "X" ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it)) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Permutation":::) "of" "X") ")" )); end; :: deftheorem defines :::"GPerms"::: MONOID_0:def 42 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ($#m5_monoid_0 :::"SubStr"::: ) "of" (Set ($#k15_monoid_0 :::"GFuncs"::: ) (Set (Var "X"))) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k17_monoid_0 :::"GPerms"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k15_monoid_0 :::"GFuncs"::: ) (Set (Var "X")) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2")))) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "X"))) ")" )) ")" ))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k17_monoid_0 :::"GPerms"::: ) "X") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v13_monoid_0 :::"invertible"::: ) ; end; theorem :: MONOID_0:77 (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k17_monoid_0 :::"GPerms"::: ) (Set (Var "X")) ")" )) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "X"))) ")" )) ; theorem :: MONOID_0:78 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set "(" ($#k17_monoid_0 :::"GPerms"::: ) (Set (Var "X")) ")" ))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X")))) & (Bool (Set ($#k1_group_1 :::"1_"::: ) (Set "(" ($#k17_monoid_0 :::"GPerms"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X")))) ")" )) ; theorem :: MONOID_0:79 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k17_monoid_0 :::"GPerms"::: ) (Set (Var "X")) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k2_group_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_funct_1 :::"""::: ) )))) ; theorem :: MONOID_0:80 (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "is" ($#v4_funct_1 :::"functional"::: ) )) "holds" (Bool (Set (Var "S")) "is" ($#v1_monoid_0 :::"constituted-Functions"::: ) )) ; theorem :: MONOID_0:81 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" )) "holds" (Bool "ex" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ($#m2_monoid_0 :::"SubStr"::: ) "of" (Set (Var "G")) "st" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Var "D")))))) ; theorem :: MONOID_0:82 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" ) & (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "G"))) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool "ex" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v22_algstr_0 :::"strict"::: ) ($#m3_monoid_0 :::"MonoidalSubStr"::: ) "of" (Set (Var "G")) "st" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Var "D")))))) ;