:: ALGSTR_1 semantic presentation begin theorem :: ALGSTR_1:1 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "c")) ")" ))) ")" ) & (Bool (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "holds" (Bool (Set (Set (Var "b")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))))) ; theorem :: ALGSTR_1:2 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "c")) ")" ))) ")" )) "holds" (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "L")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "L")) ")" ))))) ; theorem :: ALGSTR_1:3 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "c")) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))))) ; definitionlet "x" be ($#m1_hidden :::"set"::: ) ; func :::"Extract"::: "x" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) equals :: ALGSTR_1:def 1 "x"; end; :: deftheorem defines :::"Extract"::: ALGSTR_1:def 1 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_algstr_1 :::"Extract"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))); theorem :: ALGSTR_1:4 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_algstr_0 :::"Trivial-addLoopStr"::: ) ) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ; theorem :: ALGSTR_1:5 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_algstr_0 :::"Trivial-addLoopStr"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k3_algstr_0 :::"Trivial-addLoopStr"::: ) )))) ; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; attr "IT" is :::"left_zeroed"::: means :: ALGSTR_1:def 2 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) "IT" ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))); end; :: deftheorem defines :::"left_zeroed"::: ALGSTR_1:def 2 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_algstr_1 :::"left_zeroed"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "IT")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ")" )); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; attr "L" is :::"add-left-invertible"::: means :: ALGSTR_1:def 3 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))))); attr "L" is :::"add-right-invertible"::: means :: ALGSTR_1:def 4 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))))); end; :: deftheorem defines :::"add-left-invertible"::: ALGSTR_1:def 3 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v2_algstr_1 :::"add-left-invertible"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ")" )); :: deftheorem defines :::"add-right-invertible"::: ALGSTR_1:def 4 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v3_algstr_1 :::"add-right-invertible"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ")" )); definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; attr "IT" is :::"Loop-like"::: means :: ALGSTR_1:def 5 (Bool "(" (Bool "IT" "is" ($#v5_algstr_0 :::"left_add-cancelable"::: ) ) & (Bool "IT" "is" ($#v6_algstr_0 :::"right_add-cancelable"::: ) ) & (Bool "IT" "is" ($#v2_algstr_1 :::"add-left-invertible"::: ) ) & (Bool "IT" "is" ($#v3_algstr_1 :::"add-right-invertible"::: ) ) ")" ); end; :: deftheorem defines :::"Loop-like"::: ALGSTR_1:def 5 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_algstr_1 :::"Loop-like"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_algstr_0 :::"left_add-cancelable"::: ) ) & (Bool (Set (Var "IT")) "is" ($#v6_algstr_0 :::"right_add-cancelable"::: ) ) & (Bool (Set (Var "IT")) "is" ($#v2_algstr_1 :::"add-left-invertible"::: ) ) & (Bool (Set (Var "IT")) "is" ($#v3_algstr_1 :::"add-right-invertible"::: ) ) ")" ) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_algstr_1 :::"Loop-like"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_algstr_0 :::"left_add-cancelable"::: ) ($#v6_algstr_0 :::"right_add-cancelable"::: ) ($#v2_algstr_1 :::"add-left-invertible"::: ) ($#v3_algstr_1 :::"add-right-invertible"::: ) for ($#l2_algstr_0 :::"addLoopStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_algstr_0 :::"left_add-cancelable"::: ) ($#v6_algstr_0 :::"right_add-cancelable"::: ) ($#v2_algstr_1 :::"add-left-invertible"::: ) ($#v3_algstr_1 :::"add-right-invertible"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_algstr_1 :::"Loop-like"::: ) for ($#l2_algstr_0 :::"addLoopStr"::: ) ; end; theorem :: ALGSTR_1:6 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v4_algstr_1 :::"Loop-like"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "a"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ) ")" ) ")" )) ; registration cluster (Set ($#k3_algstr_0 :::"Trivial-addLoopStr"::: ) ) -> ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v4_algstr_1 :::"Loop-like"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_algstr_0 :::"strict"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v4_algstr_1 :::"Loop-like"::: ) for ($#l2_algstr_0 :::"addLoopStr"::: ) ; end; definitionmode Loop is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v4_algstr_1 :::"Loop-like"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_algstr_0 :::"left_add-cancelable"::: ) ($#v6_algstr_0 :::"right_add-cancelable"::: ) ($#v7_algstr_0 :::"add-cancelable"::: ) ($#v8_algstr_0 :::"strict"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v2_algstr_1 :::"add-left-invertible"::: ) ($#v3_algstr_1 :::"add-right-invertible"::: ) ($#v4_algstr_1 :::"Loop-like"::: ) for ($#l2_algstr_0 :::"addLoopStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_algstr_1 :::"Loop-like"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_algstr_1 :::"add-left-invertible"::: ) for ($#l2_algstr_0 :::"addLoopStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v4_algstr_1 :::"Loop-like"::: ) for ($#l2_algstr_0 :::"addLoopStr"::: ) ; end; theorem :: ALGSTR_1:7 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#l2_algstr_0 :::"AddGroup":::)) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "c")) ")" ))) ")" ) ")" ) ")" )) ; registration cluster (Set ($#k3_algstr_0 :::"Trivial-addLoopStr"::: ) ) -> ($#v2_rlvect_1 :::"Abelian"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_algstr_0 :::"left_add-cancelable"::: ) ($#v6_algstr_0 :::"right_add-cancelable"::: ) ($#v7_algstr_0 :::"add-cancelable"::: ) ($#v8_algstr_0 :::"strict"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v2_algstr_1 :::"add-left-invertible"::: ) ($#v3_algstr_1 :::"add-right-invertible"::: ) ($#v4_algstr_1 :::"Loop-like"::: ) for ($#l2_algstr_0 :::"addLoopStr"::: ) ; end; theorem :: ALGSTR_1:8 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v2_rlvect_1 :::"Abelian"::: ) ($#l2_algstr_0 :::"AddGroup":::)) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "c")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "a")))) ")" ) ")" ) ")" )) ; registration cluster (Set ($#k8_algstr_0 :::"Trivial-multLoopStr"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; theorem :: ALGSTR_1:9 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k8_algstr_0 :::"Trivial-multLoopStr"::: ) ) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ; theorem :: ALGSTR_1:10 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k8_algstr_0 :::"Trivial-multLoopStr"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set ($#k8_algstr_0 :::"Trivial-multLoopStr"::: ) )))) ; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; attr "IT" is :::"invertible"::: means :: ALGSTR_1:def 6 (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ")" ) ")" ); end; :: deftheorem defines :::"invertible"::: ALGSTR_1:def 6 : (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" ($#v5_algstr_1 :::"invertible"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ")" ) ")" ) ")" )); notationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; synonym :::"cancelable"::: "L" for :::"mult-cancelable"::: ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v21_algstr_0 :::"cancelable"::: ) ($#v22_algstr_0 :::"strict"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_algstr_1 :::"invertible"::: ) for ($#l4_algstr_0 :::"multLoopStr"::: ) ; end; definitionmode multLoop is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v21_algstr_0 :::"cancelable"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_algstr_1 :::"invertible"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; end; registration cluster (Set ($#k8_algstr_0 :::"Trivial-multLoopStr"::: ) ) -> ($#v21_algstr_0 :::"cancelable"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_algstr_1 :::"invertible"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v19_algstr_0 :::"left_mult-cancelable"::: ) ($#v20_algstr_0 :::"right_mult-cancelable"::: ) ($#v21_algstr_0 :::"cancelable"::: ) ($#v22_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#v5_algstr_1 :::"invertible"::: ) for ($#l4_algstr_0 :::"multLoopStr"::: ) ; end; definitionmode multGroup is ($#v3_group_1 :::"associative"::: ) ($#l4_algstr_0 :::"multLoop":::); end; theorem :: ALGSTR_1:11 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#l4_algstr_0 :::"multGroup":::)) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "L"))))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "c")) ")" ))) ")" ) ")" ) ")" )) ; registration cluster (Set ($#k8_algstr_0 :::"Trivial-multLoopStr"::: ) ) -> ($#v3_group_1 :::"associative"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v19_algstr_0 :::"left_mult-cancelable"::: ) ($#v20_algstr_0 :::"right_mult-cancelable"::: ) ($#v21_algstr_0 :::"cancelable"::: ) ($#v22_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#v5_algstr_1 :::"invertible"::: ) for ($#l4_algstr_0 :::"multLoopStr"::: ) ; end; theorem :: ALGSTR_1:12 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v5_group_1 :::"commutative"::: ) ($#l4_algstr_0 :::"multGroup":::)) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "L"))))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "c")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a")))) ")" ) ")" ) ")" )) ; notationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v21_algstr_0 :::"cancelable"::: ) ($#v5_algstr_1 :::"invertible"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); synonym "x" :::"""::: for :::"/"::: "x"; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v21_algstr_0 :::"cancelable"::: ) ($#v5_algstr_1 :::"invertible"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; cluster -> ($#v23_algstr_0 :::"left_invertible"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"); end; theorem :: ALGSTR_1:13 (Bool "for" (Set (Var "G")) "being" ($#l4_algstr_0 :::"multGroup":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "a")) ($#k9_algstr_0 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k9_algstr_0 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "G")))) ")" ))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v21_algstr_0 :::"cancelable"::: ) ($#v5_algstr_1 :::"invertible"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func "a" :::"/"::: "b" -> ($#m1_subset_1 :::"Element":::) "of" "L" equals :: ALGSTR_1:def 7 (Set "a" ($#k6_algstr_0 :::"*"::: ) (Set "(" "b" ($#k9_algstr_0 :::"""::: ) ")" )); end; :: deftheorem defines :::"/"::: ALGSTR_1:def 7 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v21_algstr_0 :::"cancelable"::: ) ($#v5_algstr_1 :::"invertible"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k2_algstr_1 :::"/"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k9_algstr_0 :::"""::: ) ")" ))))); definitionfunc :::"multEX_0"::: -> ($#v29_algstr_0 :::"strict"::: ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) equals :: ALGSTR_1:def 8 (Set ($#g5_algstr_0 :::"multLoopStr_0"::: ) "(#" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k35_binop_2 :::"multreal"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "#)" ); end; :: deftheorem defines :::"multEX_0"::: ALGSTR_1:def 8 : (Bool (Set ($#k3_algstr_1 :::"multEX_0"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g5_algstr_0 :::"multLoopStr_0"::: ) "(#" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k35_binop_2 :::"multreal"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "#)" )); registration cluster (Set ($#k3_algstr_1 :::"multEX_0"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v29_algstr_0 :::"strict"::: ) ; end; registration cluster (Set ($#k3_algstr_1 :::"multEX_0"::: ) ) -> ($#v29_algstr_0 :::"strict"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ; end; theorem :: ALGSTR_1:14 (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k11_binop_2 :::"*"::: ) (Set (Var "y")))))) ; theorem :: ALGSTR_1:15 (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k11_binop_2 :::"*"::: ) (Set (Var "q")))))) ; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; attr "IT" is :::"almost_invertible"::: means :: ALGSTR_1:def 9 (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) "IT"))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) "IT"))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ")" ) ")" ); end; :: deftheorem defines :::"almost_invertible"::: ALGSTR_1:def 9 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_algstr_1 :::"almost_invertible"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "IT"))))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "IT"))))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ")" ) ")" ) ")" )); definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; attr "IT" is :::"multLoop_0-like"::: means :: ALGSTR_1:def 10 (Bool "(" (Bool "IT" "is" ($#v6_algstr_1 :::"almost_invertible"::: ) ) & (Bool "IT" "is" ($#v32_algstr_0 :::"almost_cancelable"::: ) ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) "IT" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "IT")) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) "IT" ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "IT")) ")" ) ")" ); end; :: deftheorem defines :::"multLoop_0-like"::: ALGSTR_1:def 10 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v7_algstr_1 :::"multLoop_0-like"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_algstr_1 :::"almost_invertible"::: ) ) & (Bool (Set (Var "IT")) "is" ($#v32_algstr_0 :::"almost_cancelable"::: ) ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "IT")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "IT")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "IT")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "IT")))) ")" ) ")" ) ")" )); theorem :: ALGSTR_1:16 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v7_algstr_1 :::"multLoop_0-like"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) & (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "L")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) ")" ) ")" ) ")" )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_algstr_1 :::"multLoop_0-like"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v32_algstr_0 :::"almost_cancelable"::: ) ($#v6_algstr_1 :::"almost_invertible"::: ) for ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v29_algstr_0 :::"strict"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v7_algstr_1 :::"multLoop_0-like"::: ) for ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; end; definitionmode multLoop_0 is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v7_algstr_1 :::"multLoop_0-like"::: ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; end; registration cluster (Set ($#k3_algstr_1 :::"multEX_0"::: ) ) -> ($#v29_algstr_0 :::"strict"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v7_algstr_1 :::"multLoop_0-like"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v29_algstr_0 :::"strict"::: ) ($#v30_algstr_0 :::"almost_left_cancelable"::: ) ($#v31_algstr_0 :::"almost_right_cancelable"::: ) ($#v32_algstr_0 :::"almost_cancelable"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#v6_algstr_1 :::"almost_invertible"::: ) ($#v7_algstr_1 :::"multLoop_0-like"::: ) for ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; end; definitionmode multGroup_0 is ($#v3_group_1 :::"associative"::: ) ($#l5_algstr_0 :::"multLoop_0":::); end; registration cluster (Set ($#k3_algstr_1 :::"multEX_0"::: ) ) -> ($#v29_algstr_0 :::"strict"::: ) ($#v3_group_1 :::"associative"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v29_algstr_0 :::"strict"::: ) ($#v30_algstr_0 :::"almost_left_cancelable"::: ) ($#v31_algstr_0 :::"almost_right_cancelable"::: ) ($#v32_algstr_0 :::"almost_cancelable"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#v6_algstr_1 :::"almost_invertible"::: ) ($#v7_algstr_1 :::"multLoop_0-like"::: ) for ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; end; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v32_algstr_0 :::"almost_cancelable"::: ) ($#v6_algstr_1 :::"almost_invertible"::: ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); assume (Bool (Set (Const "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Const "L")))) ; redefine func "x" :::"""::: means :: ALGSTR_1:def 11 (Bool (Set it ($#k6_algstr_0 :::"*"::: ) "x") ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "L")); end; :: deftheorem defines :::"""::: ALGSTR_1:def 11 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v32_algstr_0 :::"almost_cancelable"::: ) ($#v6_algstr_1 :::"almost_invertible"::: ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "holds" (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 "L")))) ")" )))); theorem :: ALGSTR_1:17 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v32_algstr_0 :::"almost_cancelable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v6_algstr_1 :::"almost_invertible"::: ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "G"))))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "a")) ($#k11_algstr_0 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k11_algstr_0 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "G")))) ")" ))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v32_algstr_0 :::"almost_cancelable"::: ) ($#v6_algstr_1 :::"almost_invertible"::: ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func "a" :::"/"::: "b" -> ($#m1_subset_1 :::"Element":::) "of" "L" equals :: ALGSTR_1:def 12 (Set "a" ($#k6_algstr_0 :::"*"::: ) (Set "(" "b" ($#k11_algstr_0 :::"""::: ) ")" )); end; :: deftheorem defines :::"/"::: ALGSTR_1:def 12 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v32_algstr_0 :::"almost_cancelable"::: ) ($#v6_algstr_1 :::"almost_invertible"::: ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k4_algstr_1 :::"/"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k11_algstr_0 :::"""::: ) ")" ))))); registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) for ($#l2_algstr_0 :::"addLoopStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_struct_0 :::"trivial"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; end;