:: ALGSTR_0 semantic presentation begin definitionattr "c1" is :::"strict"::: ; struct :::"addMagma"::: -> ($#l1_struct_0 :::"1-sorted"::: ) ; aggr :::"addMagma":::(# :::"carrier":::, :::"addF"::: #) -> ($#l1_algstr_0 :::"addMagma"::: ) ; sel :::"addF"::: "c1" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "o" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); cluster (Set ($#g1_algstr_0 :::"addMagma"::: ) "(#" "D" "," "o" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; registrationlet "T" be ($#v1_zfmisc_1 :::"trivial"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "T")); cluster (Set ($#g1_algstr_0 :::"addMagma"::: ) "(#" "T" "," "f" "#)" ) -> ($#v7_struct_0 :::"trivial"::: ) ; end; registrationlet "N" be ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) ; let "b" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "N")); cluster (Set ($#g1_algstr_0 :::"addMagma"::: ) "(#" "N" "," "b" "#)" ) -> ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ; end; definitionlet "M" be ($#l1_algstr_0 :::"addMagma"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "M")); func "x" :::"+"::: "y" -> ($#m1_subset_1 :::"Element":::) "of" "M" equals :: ALGSTR_0:def 1 (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" "M") ($#k5_binop_1 :::"."::: ) "(" "x" "," "y" ")" ); end; :: deftheorem defines :::"+"::: ALGSTR_0:def 1 : (Bool "for" (Set (Var "M")) "being" ($#l1_algstr_0 :::"addMagma"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "M"))) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))); definitionfunc :::"Trivial-addMagma"::: -> ($#l1_algstr_0 :::"addMagma"::: ) equals :: ALGSTR_0:def 2 (Set ($#g1_algstr_0 :::"addMagma"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "#)" ); end; :: deftheorem defines :::"Trivial-addMagma"::: ALGSTR_0:def 2 : (Bool (Set ($#k2_algstr_0 :::"Trivial-addMagma"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_algstr_0 :::"addMagma"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "#)" )); registration cluster (Set ($#k2_algstr_0 :::"Trivial-addMagma"::: ) ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v1_algstr_0 :::"strict"::: ) ; end; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v1_algstr_0 :::"strict"::: ) for ($#l1_algstr_0 :::"addMagma"::: ) ; end; definitionlet "M" be ($#l1_algstr_0 :::"addMagma"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "M")); attr "x" is :::"left_add-cancelable"::: means :: ALGSTR_0:def 3 (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "st" (Bool (Bool (Set "x" ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set "x" ($#k1_algstr_0 :::"+"::: ) (Set (Var "z"))))) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "z")))); attr "x" is :::"right_add-cancelable"::: means :: ALGSTR_0:def 4 (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "st" (Bool (Bool (Set (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) "x") ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k1_algstr_0 :::"+"::: ) "x"))) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "z")))); end; :: deftheorem defines :::"left_add-cancelable"::: ALGSTR_0:def 3 : (Bool "for" (Set (Var "M")) "being" ($#l1_algstr_0 :::"addMagma"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v2_algstr_0 :::"left_add-cancelable"::: ) ) "iff" (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z"))))) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "z")))) ")" ))); :: deftheorem defines :::"right_add-cancelable"::: ALGSTR_0:def 4 : (Bool "for" (Set (Var "M")) "being" ($#l1_algstr_0 :::"addMagma"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v3_algstr_0 :::"right_add-cancelable"::: ) ) "iff" (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "x"))))) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "z")))) ")" ))); definitionlet "M" be ($#l1_algstr_0 :::"addMagma"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "M")); attr "x" is :::"add-cancelable"::: means :: ALGSTR_0:def 5 (Bool "(" (Bool "x" "is" ($#v3_algstr_0 :::"right_add-cancelable"::: ) ) & (Bool "x" "is" ($#v2_algstr_0 :::"left_add-cancelable"::: ) ) ")" ); end; :: deftheorem defines :::"add-cancelable"::: ALGSTR_0:def 5 : (Bool "for" (Set (Var "M")) "being" ($#l1_algstr_0 :::"addMagma"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v4_algstr_0 :::"add-cancelable"::: ) ) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#v3_algstr_0 :::"right_add-cancelable"::: ) ) & (Bool (Set (Var "x")) "is" ($#v2_algstr_0 :::"left_add-cancelable"::: ) ) ")" ) ")" ))); registrationlet "M" be ($#l1_algstr_0 :::"addMagma"::: ) ; cluster ($#v2_algstr_0 :::"left_add-cancelable"::: ) ($#v3_algstr_0 :::"right_add-cancelable"::: ) -> ($#v4_algstr_0 :::"add-cancelable"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M"); cluster ($#v4_algstr_0 :::"add-cancelable"::: ) -> ($#v2_algstr_0 :::"left_add-cancelable"::: ) ($#v3_algstr_0 :::"right_add-cancelable"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M"); end; definitionlet "M" be ($#l1_algstr_0 :::"addMagma"::: ) ; attr "M" is :::"left_add-cancelable"::: means :: ALGSTR_0:def 6 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "holds" (Bool (Set (Var "x")) "is" ($#v2_algstr_0 :::"left_add-cancelable"::: ) )); attr "M" is :::"right_add-cancelable"::: means :: ALGSTR_0:def 7 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "holds" (Bool (Set (Var "x")) "is" ($#v3_algstr_0 :::"right_add-cancelable"::: ) )); end; :: deftheorem defines :::"left_add-cancelable"::: ALGSTR_0:def 6 : (Bool "for" (Set (Var "M")) "being" ($#l1_algstr_0 :::"addMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v5_algstr_0 :::"left_add-cancelable"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool (Set (Var "x")) "is" ($#v2_algstr_0 :::"left_add-cancelable"::: ) )) ")" )); :: deftheorem defines :::"right_add-cancelable"::: ALGSTR_0:def 7 : (Bool "for" (Set (Var "M")) "being" ($#l1_algstr_0 :::"addMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v6_algstr_0 :::"right_add-cancelable"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool (Set (Var "x")) "is" ($#v3_algstr_0 :::"right_add-cancelable"::: ) )) ")" )); definitionlet "M" be ($#l1_algstr_0 :::"addMagma"::: ) ; attr "M" is :::"add-cancelable"::: means :: ALGSTR_0:def 8 (Bool "(" (Bool "M" "is" ($#v6_algstr_0 :::"right_add-cancelable"::: ) ) & (Bool "M" "is" ($#v5_algstr_0 :::"left_add-cancelable"::: ) ) ")" ); end; :: deftheorem defines :::"add-cancelable"::: ALGSTR_0:def 8 : (Bool "for" (Set (Var "M")) "being" ($#l1_algstr_0 :::"addMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v7_algstr_0 :::"add-cancelable"::: ) ) "iff" (Bool "(" (Bool (Set (Var "M")) "is" ($#v6_algstr_0 :::"right_add-cancelable"::: ) ) & (Bool (Set (Var "M")) "is" ($#v5_algstr_0 :::"left_add-cancelable"::: ) ) ")" ) ")" )); registration cluster ($#v5_algstr_0 :::"left_add-cancelable"::: ) ($#v6_algstr_0 :::"right_add-cancelable"::: ) -> ($#v7_algstr_0 :::"add-cancelable"::: ) for ($#l1_algstr_0 :::"addMagma"::: ) ; cluster ($#v7_algstr_0 :::"add-cancelable"::: ) -> ($#v5_algstr_0 :::"left_add-cancelable"::: ) ($#v6_algstr_0 :::"right_add-cancelable"::: ) for ($#l1_algstr_0 :::"addMagma"::: ) ; end; registration cluster (Set ($#k2_algstr_0 :::"Trivial-addMagma"::: ) ) -> ($#v7_algstr_0 :::"add-cancelable"::: ) ; end; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v1_algstr_0 :::"strict"::: ) ($#v7_algstr_0 :::"add-cancelable"::: ) for ($#l1_algstr_0 :::"addMagma"::: ) ; end; registrationlet "M" be ($#v5_algstr_0 :::"left_add-cancelable"::: ) ($#l1_algstr_0 :::"addMagma"::: ) ; cluster -> ($#v2_algstr_0 :::"left_add-cancelable"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M"); end; registrationlet "M" be ($#v6_algstr_0 :::"right_add-cancelable"::: ) ($#l1_algstr_0 :::"addMagma"::: ) ; cluster -> ($#v3_algstr_0 :::"right_add-cancelable"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M"); end; definitionattr "c1" is :::"strict"::: ; struct :::"addLoopStr"::: -> ($#l2_struct_0 :::"ZeroStr"::: ) "," ($#l1_algstr_0 :::"addMagma"::: ) ; aggr :::"addLoopStr":::(# :::"carrier":::, :::"addF":::, :::"ZeroF"::: #) -> ($#l2_algstr_0 :::"addLoopStr"::: ) ; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "o" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); let "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); cluster (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" "D" "," "o" "," "d" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; registrationlet "T" be ($#v1_zfmisc_1 :::"trivial"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "T")); let "t" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "T")); cluster (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" "T" "," "f" "," "t" "#)" ) -> ($#v7_struct_0 :::"trivial"::: ) ; end; registrationlet "N" be ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) ; let "b" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "N")); let "m" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "N")); cluster (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" "N" "," "b" "," "m" "#)" ) -> ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ; end; definitionfunc :::"Trivial-addLoopStr"::: -> ($#l2_algstr_0 :::"addLoopStr"::: ) equals :: ALGSTR_0:def 9 (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k5_funct_5 :::"op0"::: ) ) "#)" ); end; :: deftheorem defines :::"Trivial-addLoopStr"::: ALGSTR_0:def 9 : (Bool (Set ($#k3_algstr_0 :::"Trivial-addLoopStr"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k5_funct_5 :::"op0"::: ) ) "#)" )); registration cluster (Set ($#k3_algstr_0 :::"Trivial-addLoopStr"::: ) ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v8_algstr_0 :::"strict"::: ) ; end; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v8_algstr_0 :::"strict"::: ) for ($#l2_algstr_0 :::"addLoopStr"::: ) ; end; definitionlet "M" be ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "M")); attr "x" is :::"left_complementable"::: means :: ALGSTR_0:def 10 (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "st" (Bool (Set (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) "x") ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "M"))); attr "x" is :::"right_complementable"::: means :: ALGSTR_0:def 11 (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "st" (Bool (Set "x" ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "M"))); end; :: deftheorem defines :::"left_complementable"::: ALGSTR_0:def 10 : (Bool "for" (Set (Var "M")) "being" ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v9_algstr_0 :::"left_complementable"::: ) ) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Set (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "M"))))) ")" ))); :: deftheorem defines :::"right_complementable"::: ALGSTR_0:def 11 : (Bool "for" (Set (Var "M")) "being" ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v10_algstr_0 :::"right_complementable"::: ) ) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "M"))))) ")" ))); definitionlet "M" be ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "M")); attr "x" is :::"complementable"::: means :: ALGSTR_0:def 12 (Bool "(" (Bool "x" "is" ($#v10_algstr_0 :::"right_complementable"::: ) ) & (Bool "x" "is" ($#v9_algstr_0 :::"left_complementable"::: ) ) ")" ); end; :: deftheorem defines :::"complementable"::: ALGSTR_0:def 12 : (Bool "for" (Set (Var "M")) "being" ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v11_algstr_0 :::"complementable"::: ) ) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#v10_algstr_0 :::"right_complementable"::: ) ) & (Bool (Set (Var "x")) "is" ($#v9_algstr_0 :::"left_complementable"::: ) ) ")" ) ")" ))); registrationlet "M" be ($#l2_algstr_0 :::"addLoopStr"::: ) ; cluster ($#v9_algstr_0 :::"left_complementable"::: ) ($#v10_algstr_0 :::"right_complementable"::: ) -> ($#v11_algstr_0 :::"complementable"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M"); cluster ($#v11_algstr_0 :::"complementable"::: ) -> ($#v9_algstr_0 :::"left_complementable"::: ) ($#v10_algstr_0 :::"right_complementable"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M"); end; definitionlet "M" be ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "M")); assume (Bool "(" (Bool (Set (Const "x")) "is" ($#v9_algstr_0 :::"left_complementable"::: ) ) & (Bool (Set (Const "x")) "is" ($#v3_algstr_0 :::"right_add-cancelable"::: ) ) ")" ) ; func :::"-"::: "x" -> ($#m1_subset_1 :::"Element":::) "of" "M" means :: ALGSTR_0:def 13 (Bool (Set it ($#k1_algstr_0 :::"+"::: ) "x") ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "M")); end; :: deftheorem defines :::"-"::: ALGSTR_0:def 13 : (Bool "for" (Set (Var "M")) "being" ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v9_algstr_0 :::"left_complementable"::: ) ) & (Bool (Set (Var "x")) "is" ($#v3_algstr_0 :::"right_add-cancelable"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")))) "iff" (Bool (Set (Set (Var "b3")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "M")))) ")" )))); definitionlet "V" be ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "v", "w" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "V")); func "v" :::"-"::: "w" -> ($#m1_subset_1 :::"Element":::) "of" "V" equals :: ALGSTR_0:def 14 (Set "v" ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) "w" ")" )); end; :: deftheorem defines :::"-"::: ALGSTR_0:def 14 : (Bool "for" (Set (Var "V")) "being" ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "w")) ")" ))))); registration cluster (Set ($#k3_algstr_0 :::"Trivial-addLoopStr"::: ) ) -> ($#v7_algstr_0 :::"add-cancelable"::: ) ; end; definitionlet "M" be ($#l2_algstr_0 :::"addLoopStr"::: ) ; attr "M" is :::"left_complementable"::: means :: ALGSTR_0:def 15 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "holds" (Bool (Set (Var "x")) "is" ($#v9_algstr_0 :::"left_complementable"::: ) )); attr "M" is :::"right_complementable"::: means :: ALGSTR_0:def 16 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "holds" (Bool (Set (Var "x")) "is" ($#v10_algstr_0 :::"right_complementable"::: ) )); end; :: deftheorem defines :::"left_complementable"::: ALGSTR_0:def 15 : (Bool "for" (Set (Var "M")) "being" ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v12_algstr_0 :::"left_complementable"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool (Set (Var "x")) "is" ($#v9_algstr_0 :::"left_complementable"::: ) )) ")" )); :: deftheorem defines :::"right_complementable"::: ALGSTR_0:def 16 : (Bool "for" (Set (Var "M")) "being" ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v13_algstr_0 :::"right_complementable"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool (Set (Var "x")) "is" ($#v10_algstr_0 :::"right_complementable"::: ) )) ")" )); definitionlet "M" be ($#l2_algstr_0 :::"addLoopStr"::: ) ; attr "M" is :::"complementable"::: means :: ALGSTR_0:def 17 (Bool "(" (Bool "M" "is" ($#v13_algstr_0 :::"right_complementable"::: ) ) & (Bool "M" "is" ($#v12_algstr_0 :::"left_complementable"::: ) ) ")" ); end; :: deftheorem defines :::"complementable"::: ALGSTR_0:def 17 : (Bool "for" (Set (Var "M")) "being" ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v14_algstr_0 :::"complementable"::: ) ) "iff" (Bool "(" (Bool (Set (Var "M")) "is" ($#v13_algstr_0 :::"right_complementable"::: ) ) & (Bool (Set (Var "M")) "is" ($#v12_algstr_0 :::"left_complementable"::: ) ) ")" ) ")" )); registration cluster ($#v12_algstr_0 :::"left_complementable"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) -> ($#v14_algstr_0 :::"complementable"::: ) for ($#l2_algstr_0 :::"addLoopStr"::: ) ; cluster ($#v14_algstr_0 :::"complementable"::: ) -> ($#v12_algstr_0 :::"left_complementable"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) for ($#l2_algstr_0 :::"addLoopStr"::: ) ; end; registration cluster (Set ($#k3_algstr_0 :::"Trivial-addLoopStr"::: ) ) -> ($#v14_algstr_0 :::"complementable"::: ) ; end; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v7_algstr_0 :::"add-cancelable"::: ) ($#v8_algstr_0 :::"strict"::: ) ($#v14_algstr_0 :::"complementable"::: ) for ($#l2_algstr_0 :::"addLoopStr"::: ) ; end; registrationlet "M" be ($#v12_algstr_0 :::"left_complementable"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; cluster -> ($#v9_algstr_0 :::"left_complementable"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M"); end; registrationlet "M" be ($#v13_algstr_0 :::"right_complementable"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; cluster -> ($#v10_algstr_0 :::"right_complementable"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M"); end; begin definitionattr "c1" is :::"strict"::: ; struct :::"multMagma"::: -> ($#l1_struct_0 :::"1-sorted"::: ) ; aggr :::"multMagma":::(# :::"carrier":::, :::"multF"::: #) -> ($#l3_algstr_0 :::"multMagma"::: ) ; sel :::"multF"::: "c1" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "o" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); cluster (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" "D" "," "o" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; registrationlet "T" be ($#v1_zfmisc_1 :::"trivial"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "T")); cluster (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" "T" "," "f" "#)" ) -> ($#v7_struct_0 :::"trivial"::: ) ; end; registrationlet "N" be ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) ; let "b" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "N")); cluster (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" "N" "," "b" "#)" ) -> ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ; end; definitionlet "M" be ($#l3_algstr_0 :::"multMagma"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "M")); func "x" :::"*"::: "y" -> ($#m1_subset_1 :::"Element":::) "of" "M" equals :: ALGSTR_0:def 18 (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "M") ($#k5_binop_1 :::"."::: ) "(" "x" "," "y" ")" ); end; :: deftheorem defines :::"*"::: ALGSTR_0:def 18 : (Bool "for" (Set (Var "M")) "being" ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "M"))) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))); definitionfunc :::"Trivial-multMagma"::: -> ($#l3_algstr_0 :::"multMagma"::: ) equals :: ALGSTR_0:def 19 (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "#)" ); end; :: deftheorem defines :::"Trivial-multMagma"::: ALGSTR_0:def 19 : (Bool (Set ($#k7_algstr_0 :::"Trivial-multMagma"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "#)" )); registration cluster (Set ($#k7_algstr_0 :::"Trivial-multMagma"::: ) ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v15_algstr_0 :::"strict"::: ) ; end; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v15_algstr_0 :::"strict"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; end; definitionlet "M" be ($#l3_algstr_0 :::"multMagma"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "M")); attr "x" is :::"left_mult-cancelable"::: means :: ALGSTR_0:def 20 (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "st" (Bool (Bool (Set "x" ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set "x" ($#k6_algstr_0 :::"*"::: ) (Set (Var "z"))))) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "z")))); attr "x" is :::"right_mult-cancelable"::: means :: ALGSTR_0:def 21 (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "st" (Bool (Bool (Set (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) "x") ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k6_algstr_0 :::"*"::: ) "x"))) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "z")))); end; :: deftheorem defines :::"left_mult-cancelable"::: ALGSTR_0:def 20 : (Bool "for" (Set (Var "M")) "being" ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v16_algstr_0 :::"left_mult-cancelable"::: ) ) "iff" (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z"))))) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "z")))) ")" ))); :: deftheorem defines :::"right_mult-cancelable"::: ALGSTR_0:def 21 : (Bool "for" (Set (Var "M")) "being" ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v17_algstr_0 :::"right_mult-cancelable"::: ) ) "iff" (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))))) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "z")))) ")" ))); definitionlet "M" be ($#l3_algstr_0 :::"multMagma"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "M")); attr "x" is :::"mult-cancelable"::: means :: ALGSTR_0:def 22 (Bool "(" (Bool "x" "is" ($#v17_algstr_0 :::"right_mult-cancelable"::: ) ) & (Bool "x" "is" ($#v16_algstr_0 :::"left_mult-cancelable"::: ) ) ")" ); end; :: deftheorem defines :::"mult-cancelable"::: ALGSTR_0:def 22 : (Bool "for" (Set (Var "M")) "being" ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v18_algstr_0 :::"mult-cancelable"::: ) ) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#v17_algstr_0 :::"right_mult-cancelable"::: ) ) & (Bool (Set (Var "x")) "is" ($#v16_algstr_0 :::"left_mult-cancelable"::: ) ) ")" ) ")" ))); registrationlet "M" be ($#l3_algstr_0 :::"multMagma"::: ) ; cluster ($#v16_algstr_0 :::"left_mult-cancelable"::: ) ($#v17_algstr_0 :::"right_mult-cancelable"::: ) -> ($#v18_algstr_0 :::"mult-cancelable"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M"); cluster ($#v18_algstr_0 :::"mult-cancelable"::: ) -> ($#v16_algstr_0 :::"left_mult-cancelable"::: ) ($#v17_algstr_0 :::"right_mult-cancelable"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M"); end; definitionlet "M" be ($#l3_algstr_0 :::"multMagma"::: ) ; attr "M" is :::"left_mult-cancelable"::: means :: ALGSTR_0:def 23 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "holds" (Bool (Set (Var "x")) "is" ($#v16_algstr_0 :::"left_mult-cancelable"::: ) )); attr "M" is :::"right_mult-cancelable"::: means :: ALGSTR_0:def 24 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "holds" (Bool (Set (Var "x")) "is" ($#v17_algstr_0 :::"right_mult-cancelable"::: ) )); end; :: deftheorem defines :::"left_mult-cancelable"::: ALGSTR_0:def 23 : (Bool "for" (Set (Var "M")) "being" ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v19_algstr_0 :::"left_mult-cancelable"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool (Set (Var "x")) "is" ($#v16_algstr_0 :::"left_mult-cancelable"::: ) )) ")" )); :: deftheorem defines :::"right_mult-cancelable"::: ALGSTR_0:def 24 : (Bool "for" (Set (Var "M")) "being" ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v20_algstr_0 :::"right_mult-cancelable"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool (Set (Var "x")) "is" ($#v17_algstr_0 :::"right_mult-cancelable"::: ) )) ")" )); definitionlet "M" be ($#l3_algstr_0 :::"multMagma"::: ) ; attr "M" is :::"mult-cancelable"::: means :: ALGSTR_0:def 25 (Bool "(" (Bool "M" "is" ($#v19_algstr_0 :::"left_mult-cancelable"::: ) ) & (Bool "M" "is" ($#v20_algstr_0 :::"right_mult-cancelable"::: ) ) ")" ); end; :: deftheorem defines :::"mult-cancelable"::: ALGSTR_0:def 25 : (Bool "for" (Set (Var "M")) "being" ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v21_algstr_0 :::"mult-cancelable"::: ) ) "iff" (Bool "(" (Bool (Set (Var "M")) "is" ($#v19_algstr_0 :::"left_mult-cancelable"::: ) ) & (Bool (Set (Var "M")) "is" ($#v20_algstr_0 :::"right_mult-cancelable"::: ) ) ")" ) ")" )); registration cluster ($#v19_algstr_0 :::"left_mult-cancelable"::: ) ($#v20_algstr_0 :::"right_mult-cancelable"::: ) -> ($#v21_algstr_0 :::"mult-cancelable"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; cluster ($#v21_algstr_0 :::"mult-cancelable"::: ) -> ($#v19_algstr_0 :::"left_mult-cancelable"::: ) ($#v20_algstr_0 :::"right_mult-cancelable"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; end; registration cluster (Set ($#k7_algstr_0 :::"Trivial-multMagma"::: ) ) -> ($#v21_algstr_0 :::"mult-cancelable"::: ) ; end; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v15_algstr_0 :::"strict"::: ) ($#v21_algstr_0 :::"mult-cancelable"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; end; registrationlet "M" be ($#v19_algstr_0 :::"left_mult-cancelable"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster -> ($#v16_algstr_0 :::"left_mult-cancelable"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M"); end; registrationlet "M" be ($#v20_algstr_0 :::"right_mult-cancelable"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster -> ($#v17_algstr_0 :::"right_mult-cancelable"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M"); end; definitionattr "c1" is :::"strict"::: ; struct :::"multLoopStr"::: -> ($#l3_struct_0 :::"OneStr"::: ) "," ($#l3_algstr_0 :::"multMagma"::: ) ; aggr :::"multLoopStr":::(# :::"carrier":::, :::"multF":::, :::"OneF"::: #) -> ($#l4_algstr_0 :::"multLoopStr"::: ) ; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "o" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); let "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); cluster (Set ($#g4_algstr_0 :::"multLoopStr"::: ) "(#" "D" "," "o" "," "d" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; registrationlet "T" be ($#v1_zfmisc_1 :::"trivial"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "T")); let "t" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "T")); cluster (Set ($#g4_algstr_0 :::"multLoopStr"::: ) "(#" "T" "," "f" "," "t" "#)" ) -> ($#v7_struct_0 :::"trivial"::: ) ; end; registrationlet "N" be ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) ; let "b" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "N")); let "m" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "N")); cluster (Set ($#g4_algstr_0 :::"multLoopStr"::: ) "(#" "N" "," "b" "," "m" "#)" ) -> ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ; end; definitionfunc :::"Trivial-multLoopStr"::: -> ($#l4_algstr_0 :::"multLoopStr"::: ) equals :: ALGSTR_0:def 26 (Set ($#g4_algstr_0 :::"multLoopStr"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k5_funct_5 :::"op0"::: ) ) "#)" ); end; :: deftheorem defines :::"Trivial-multLoopStr"::: ALGSTR_0:def 26 : (Bool (Set ($#k8_algstr_0 :::"Trivial-multLoopStr"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g4_algstr_0 :::"multLoopStr"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k5_funct_5 :::"op0"::: ) ) "#)" )); registration cluster (Set ($#k8_algstr_0 :::"Trivial-multLoopStr"::: ) ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v22_algstr_0 :::"strict"::: ) ; end; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v22_algstr_0 :::"strict"::: ) for ($#l4_algstr_0 :::"multLoopStr"::: ) ; end; registration cluster (Set ($#k8_algstr_0 :::"Trivial-multLoopStr"::: ) ) -> ($#v21_algstr_0 :::"mult-cancelable"::: ) ; end; definitionlet "M" be ($#l4_algstr_0 :::"multLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "M")); attr "x" is :::"left_invertible"::: means :: ALGSTR_0:def 27 (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "st" (Bool (Set (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) "x") ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "M"))); attr "x" is :::"right_invertible"::: means :: ALGSTR_0:def 28 (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "st" (Bool (Set "x" ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "M"))); end; :: deftheorem defines :::"left_invertible"::: ALGSTR_0:def 27 : (Bool "for" (Set (Var "M")) "being" ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v23_algstr_0 :::"left_invertible"::: ) ) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Set (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "M"))))) ")" ))); :: deftheorem defines :::"right_invertible"::: ALGSTR_0:def 28 : (Bool "for" (Set (Var "M")) "being" ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v24_algstr_0 :::"right_invertible"::: ) ) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "M"))))) ")" ))); definitionlet "M" be ($#l4_algstr_0 :::"multLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "M")); attr "x" is :::"invertible"::: means :: ALGSTR_0:def 29 (Bool "(" (Bool "x" "is" ($#v24_algstr_0 :::"right_invertible"::: ) ) & (Bool "x" "is" ($#v23_algstr_0 :::"left_invertible"::: ) ) ")" ); end; :: deftheorem defines :::"invertible"::: ALGSTR_0:def 29 : (Bool "for" (Set (Var "M")) "being" ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v25_algstr_0 :::"invertible"::: ) ) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#v24_algstr_0 :::"right_invertible"::: ) ) & (Bool (Set (Var "x")) "is" ($#v23_algstr_0 :::"left_invertible"::: ) ) ")" ) ")" ))); registrationlet "M" be ($#l4_algstr_0 :::"multLoopStr"::: ) ; cluster ($#v23_algstr_0 :::"left_invertible"::: ) ($#v24_algstr_0 :::"right_invertible"::: ) -> ($#v25_algstr_0 :::"invertible"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M"); cluster ($#v25_algstr_0 :::"invertible"::: ) -> ($#v23_algstr_0 :::"left_invertible"::: ) ($#v24_algstr_0 :::"right_invertible"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M"); end; definitionlet "M" be ($#l4_algstr_0 :::"multLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "M")); assume (Bool "(" (Bool (Set (Const "x")) "is" ($#v23_algstr_0 :::"left_invertible"::: ) ) & (Bool (Set (Const "x")) "is" ($#v17_algstr_0 :::"right_mult-cancelable"::: ) ) ")" ) ; func :::"/"::: "x" -> ($#m1_subset_1 :::"Element":::) "of" "M" means :: ALGSTR_0:def 30 (Bool (Set it ($#k6_algstr_0 :::"*"::: ) "x") ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "M")); end; :: deftheorem defines :::"/"::: ALGSTR_0:def 30 : (Bool "for" (Set (Var "M")) "being" ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v23_algstr_0 :::"left_invertible"::: ) ) & (Bool (Set (Var "x")) "is" ($#v17_algstr_0 :::"right_mult-cancelable"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k9_algstr_0 :::"/"::: ) (Set (Var "x")))) "iff" (Bool (Set (Set (Var "b3")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "M")))) ")" )))); definitionlet "M" be ($#l4_algstr_0 :::"multLoopStr"::: ) ; attr "M" is :::"left_invertible"::: means :: ALGSTR_0:def 31 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "holds" (Bool (Set (Var "x")) "is" ($#v23_algstr_0 :::"left_invertible"::: ) )); attr "M" is :::"right_invertible"::: means :: ALGSTR_0:def 32 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "holds" (Bool (Set (Var "x")) "is" ($#v24_algstr_0 :::"right_invertible"::: ) )); end; :: deftheorem defines :::"left_invertible"::: ALGSTR_0:def 31 : (Bool "for" (Set (Var "M")) "being" ($#l4_algstr_0 :::"multLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v26_algstr_0 :::"left_invertible"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool (Set (Var "x")) "is" ($#v23_algstr_0 :::"left_invertible"::: ) )) ")" )); :: deftheorem defines :::"right_invertible"::: ALGSTR_0:def 32 : (Bool "for" (Set (Var "M")) "being" ($#l4_algstr_0 :::"multLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v27_algstr_0 :::"right_invertible"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool (Set (Var "x")) "is" ($#v24_algstr_0 :::"right_invertible"::: ) )) ")" )); definitionlet "M" be ($#l4_algstr_0 :::"multLoopStr"::: ) ; attr "M" is :::"invertible"::: means :: ALGSTR_0:def 33 (Bool "(" (Bool "M" "is" ($#v27_algstr_0 :::"right_invertible"::: ) ) & (Bool "M" "is" ($#v26_algstr_0 :::"left_invertible"::: ) ) ")" ); end; :: deftheorem defines :::"invertible"::: ALGSTR_0:def 33 : (Bool "for" (Set (Var "M")) "being" ($#l4_algstr_0 :::"multLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v28_algstr_0 :::"invertible"::: ) ) "iff" (Bool "(" (Bool (Set (Var "M")) "is" ($#v27_algstr_0 :::"right_invertible"::: ) ) & (Bool (Set (Var "M")) "is" ($#v26_algstr_0 :::"left_invertible"::: ) ) ")" ) ")" )); registration cluster ($#v26_algstr_0 :::"left_invertible"::: ) ($#v27_algstr_0 :::"right_invertible"::: ) -> ($#v28_algstr_0 :::"invertible"::: ) for ($#l4_algstr_0 :::"multLoopStr"::: ) ; cluster ($#v28_algstr_0 :::"invertible"::: ) -> ($#v26_algstr_0 :::"left_invertible"::: ) ($#v27_algstr_0 :::"right_invertible"::: ) for ($#l4_algstr_0 :::"multLoopStr"::: ) ; end; registration cluster (Set ($#k8_algstr_0 :::"Trivial-multLoopStr"::: ) ) -> ($#v28_algstr_0 :::"invertible"::: ) ; end; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v21_algstr_0 :::"mult-cancelable"::: ) ($#v22_algstr_0 :::"strict"::: ) ($#v28_algstr_0 :::"invertible"::: ) for ($#l4_algstr_0 :::"multLoopStr"::: ) ; end; registrationlet "M" be ($#v26_algstr_0 :::"left_invertible"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; cluster -> ($#v23_algstr_0 :::"left_invertible"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M"); end; registrationlet "M" be ($#v27_algstr_0 :::"right_invertible"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; cluster -> ($#v24_algstr_0 :::"right_invertible"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M"); end; begin definitionattr "c1" is :::"strict"::: ; struct :::"multLoopStr_0"::: -> ($#l4_algstr_0 :::"multLoopStr"::: ) "," ($#l4_struct_0 :::"ZeroOneStr"::: ) ; aggr :::"multLoopStr_0":::(# :::"carrier":::, :::"multF":::, :::"ZeroF":::, :::"OneF"::: #) -> ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "o" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); let "d", "e" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); cluster (Set ($#g5_algstr_0 :::"multLoopStr_0"::: ) "(#" "D" "," "o" "," "d" "," "e" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; registrationlet "T" be ($#v1_zfmisc_1 :::"trivial"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "T")); let "s", "t" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "T")); cluster (Set ($#g5_algstr_0 :::"multLoopStr_0"::: ) "(#" "T" "," "f" "," "s" "," "t" "#)" ) -> ($#v7_struct_0 :::"trivial"::: ) ; end; registrationlet "N" be ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) ; let "b" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "N")); let "m", "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "N")); cluster (Set ($#g5_algstr_0 :::"multLoopStr_0"::: ) "(#" "N" "," "b" "," "m" "," "n" "#)" ) -> ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ; end; definitionfunc :::"Trivial-multLoopStr_0"::: -> ($#l5_algstr_0 :::"multLoopStr_0"::: ) equals :: ALGSTR_0:def 34 (Set ($#g5_algstr_0 :::"multLoopStr_0"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k5_funct_5 :::"op0"::: ) ) "," (Set ($#k5_funct_5 :::"op0"::: ) ) "#)" ); end; :: deftheorem defines :::"Trivial-multLoopStr_0"::: ALGSTR_0:def 34 : (Bool (Set ($#k10_algstr_0 :::"Trivial-multLoopStr_0"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g5_algstr_0 :::"multLoopStr_0"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k5_funct_5 :::"op0"::: ) ) "," (Set ($#k5_funct_5 :::"op0"::: ) ) "#)" )); registration cluster (Set ($#k10_algstr_0 :::"Trivial-multLoopStr_0"::: ) ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v29_algstr_0 :::"strict"::: ) ; end; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v29_algstr_0 :::"strict"::: ) for ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; end; definitionlet "M" be ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "M")); func "x" :::"""::: -> ($#m1_subset_1 :::"Element":::) "of" "M" means :: ALGSTR_0:def 35 (Bool (Set it ($#k6_algstr_0 :::"*"::: ) "x") ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "M")) if (Bool "(" (Bool "x" "is" ($#v23_algstr_0 :::"left_invertible"::: ) ) & (Bool "x" "is" ($#v17_algstr_0 :::"right_mult-cancelable"::: ) ) ")" ) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "M")); end; :: deftheorem defines :::"""::: ALGSTR_0:def 35 : (Bool "for" (Set (Var "M")) "being" ($#l5_algstr_0 :::"multLoopStr_0"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) "is" ($#v23_algstr_0 :::"left_invertible"::: ) ) & (Bool (Set (Var "x")) "is" ($#v17_algstr_0 :::"right_mult-cancelable"::: ) )) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k11_algstr_0 :::"""::: ) )) "iff" (Bool (Set (Set (Var "b3")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "M")))) ")" ) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "x")) "is" ($#v23_algstr_0 :::"left_invertible"::: ) ) "or" "not" (Bool (Set (Var "x")) "is" ($#v17_algstr_0 :::"right_mult-cancelable"::: ) ) ")" )) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k11_algstr_0 :::"""::: ) )) "iff" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "M")))) ")" ) ")" ")" ))); definitionlet "M" be ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; attr "M" is :::"almost_left_cancelable"::: means :: ALGSTR_0:def 36 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) "M"))) "holds" (Bool (Set (Var "x")) "is" ($#v16_algstr_0 :::"left_mult-cancelable"::: ) )); attr "M" is :::"almost_right_cancelable"::: means :: ALGSTR_0:def 37 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) "M"))) "holds" (Bool (Set (Var "x")) "is" ($#v17_algstr_0 :::"right_mult-cancelable"::: ) )); end; :: deftheorem defines :::"almost_left_cancelable"::: ALGSTR_0:def 36 : (Bool "for" (Set (Var "M")) "being" ($#l5_algstr_0 :::"multLoopStr_0"::: ) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v30_algstr_0 :::"almost_left_cancelable"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "M"))))) "holds" (Bool (Set (Var "x")) "is" ($#v16_algstr_0 :::"left_mult-cancelable"::: ) )) ")" )); :: deftheorem defines :::"almost_right_cancelable"::: ALGSTR_0:def 37 : (Bool "for" (Set (Var "M")) "being" ($#l5_algstr_0 :::"multLoopStr_0"::: ) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v31_algstr_0 :::"almost_right_cancelable"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "M"))))) "holds" (Bool (Set (Var "x")) "is" ($#v17_algstr_0 :::"right_mult-cancelable"::: ) )) ")" )); definitionlet "M" be ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; attr "M" is :::"almost_cancelable"::: means :: ALGSTR_0:def 38 (Bool "(" (Bool "M" "is" ($#v30_algstr_0 :::"almost_left_cancelable"::: ) ) & (Bool "M" "is" ($#v31_algstr_0 :::"almost_right_cancelable"::: ) ) ")" ); end; :: deftheorem defines :::"almost_cancelable"::: ALGSTR_0:def 38 : (Bool "for" (Set (Var "M")) "being" ($#l5_algstr_0 :::"multLoopStr_0"::: ) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v32_algstr_0 :::"almost_cancelable"::: ) ) "iff" (Bool "(" (Bool (Set (Var "M")) "is" ($#v30_algstr_0 :::"almost_left_cancelable"::: ) ) & (Bool (Set (Var "M")) "is" ($#v31_algstr_0 :::"almost_right_cancelable"::: ) ) ")" ) ")" )); registration cluster ($#v30_algstr_0 :::"almost_left_cancelable"::: ) ($#v31_algstr_0 :::"almost_right_cancelable"::: ) -> ($#v32_algstr_0 :::"almost_cancelable"::: ) for ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; cluster ($#v32_algstr_0 :::"almost_cancelable"::: ) -> ($#v30_algstr_0 :::"almost_left_cancelable"::: ) ($#v31_algstr_0 :::"almost_right_cancelable"::: ) for ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; end; registration cluster (Set ($#k10_algstr_0 :::"Trivial-multLoopStr_0"::: ) ) -> ($#v32_algstr_0 :::"almost_cancelable"::: ) ; end; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v29_algstr_0 :::"strict"::: ) ($#v32_algstr_0 :::"almost_cancelable"::: ) for ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; end; definitionlet "M" be ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; attr "M" is :::"almost_left_invertible"::: means :: ALGSTR_0:def 39 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) "M"))) "holds" (Bool (Set (Var "x")) "is" ($#v23_algstr_0 :::"left_invertible"::: ) )); attr "M" is :::"almost_right_invertible"::: means :: ALGSTR_0:def 40 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "M" "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) "M"))) "holds" (Bool (Set (Var "x")) "is" ($#v24_algstr_0 :::"right_invertible"::: ) )); end; :: deftheorem defines :::"almost_left_invertible"::: ALGSTR_0:def 39 : (Bool "for" (Set (Var "M")) "being" ($#l5_algstr_0 :::"multLoopStr_0"::: ) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v33_algstr_0 :::"almost_left_invertible"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "M"))))) "holds" (Bool (Set (Var "x")) "is" ($#v23_algstr_0 :::"left_invertible"::: ) )) ")" )); :: deftheorem defines :::"almost_right_invertible"::: ALGSTR_0:def 40 : (Bool "for" (Set (Var "M")) "being" ($#l5_algstr_0 :::"multLoopStr_0"::: ) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v34_algstr_0 :::"almost_right_invertible"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "M"))))) "holds" (Bool (Set (Var "x")) "is" ($#v24_algstr_0 :::"right_invertible"::: ) )) ")" )); definitionlet "M" be ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; attr "M" is :::"almost_invertible"::: means :: ALGSTR_0:def 41 (Bool "(" (Bool "M" "is" ($#v34_algstr_0 :::"almost_right_invertible"::: ) ) & (Bool "M" "is" ($#v33_algstr_0 :::"almost_left_invertible"::: ) ) ")" ); end; :: deftheorem defines :::"almost_invertible"::: ALGSTR_0:def 41 : (Bool "for" (Set (Var "M")) "being" ($#l5_algstr_0 :::"multLoopStr_0"::: ) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v35_algstr_0 :::"almost_invertible"::: ) ) "iff" (Bool "(" (Bool (Set (Var "M")) "is" ($#v34_algstr_0 :::"almost_right_invertible"::: ) ) & (Bool (Set (Var "M")) "is" ($#v33_algstr_0 :::"almost_left_invertible"::: ) ) ")" ) ")" )); registration cluster ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v34_algstr_0 :::"almost_right_invertible"::: ) -> ($#v35_algstr_0 :::"almost_invertible"::: ) for ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; cluster ($#v35_algstr_0 :::"almost_invertible"::: ) -> ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v34_algstr_0 :::"almost_right_invertible"::: ) for ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; end; registration cluster (Set ($#k10_algstr_0 :::"Trivial-multLoopStr_0"::: ) ) -> ($#v35_algstr_0 :::"almost_invertible"::: ) ; end; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v29_algstr_0 :::"strict"::: ) ($#v32_algstr_0 :::"almost_cancelable"::: ) ($#v35_algstr_0 :::"almost_invertible"::: ) for ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; end; begin definitionattr "c1" is :::"strict"::: ; struct :::"doubleLoopStr"::: -> ($#l2_algstr_0 :::"addLoopStr"::: ) "," ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; aggr :::"doubleLoopStr":::(# :::"carrier":::, :::"addF":::, :::"multF":::, :::"OneF":::, :::"ZeroF"::: #) -> ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "o", "o1" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); let "d", "e" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); cluster (Set ($#g6_algstr_0 :::"doubleLoopStr"::: ) "(#" "D" "," "o" "," "o1" "," "d" "," "e" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; registrationlet "T" be ($#v1_zfmisc_1 :::"trivial"::: ) ($#m1_hidden :::"set"::: ) ; let "f", "f1" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "T")); let "s", "t" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "T")); cluster (Set ($#g6_algstr_0 :::"doubleLoopStr"::: ) "(#" "T" "," "f" "," "f1" "," "s" "," "t" "#)" ) -> ($#v7_struct_0 :::"trivial"::: ) ; end; registrationlet "N" be ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) ; let "b", "b1" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "N")); let "m", "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "N")); cluster (Set ($#g6_algstr_0 :::"doubleLoopStr"::: ) "(#" "N" "," "b" "," "b1" "," "m" "," "n" "#)" ) -> ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ; end; definitionfunc :::"Trivial-doubleLoopStr"::: -> ($#l6_algstr_0 :::"doubleLoopStr"::: ) equals :: ALGSTR_0:def 42 (Set ($#g6_algstr_0 :::"doubleLoopStr"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k5_funct_5 :::"op0"::: ) ) "," (Set ($#k5_funct_5 :::"op0"::: ) ) "#)" ); end; :: deftheorem defines :::"Trivial-doubleLoopStr"::: ALGSTR_0:def 42 : (Bool (Set ($#k12_algstr_0 :::"Trivial-doubleLoopStr"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g6_algstr_0 :::"doubleLoopStr"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k5_funct_5 :::"op0"::: ) ) "," (Set ($#k5_funct_5 :::"op0"::: ) ) "#)" )); registration cluster (Set ($#k12_algstr_0 :::"Trivial-doubleLoopStr"::: ) ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v36_algstr_0 :::"strict"::: ) ; end; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v36_algstr_0 :::"strict"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end;