:: GCD_1 semantic presentation begin registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_vectsp_1 :::"left_unital"::: ) for ($#l4_algstr_0 :::"multLoopStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_vectsp_1 :::"distributive"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_vectsp_1 :::"distributive"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) -> for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; registration cluster (Set ($#k2_vectsp_1 :::"F_Real"::: ) ) -> ($#v1_vectsp_2 :::"domRing-like"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v36_algstr_0 :::"strict"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; theorem :: GCD_1:1 (Bool "for" (Set (Var "R")) "being" ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "c"))))) "implies" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" & "(" (Bool (Bool (Set (Set (Var "b")) ($#k8_group_1 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k8_group_1 :::"*"::: ) (Set (Var "a"))))) "implies" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" ")" ))) ; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); pred "x" :::"divides"::: "y" means :: GCD_1:def 1 (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "R" "st" (Bool "y" ($#r1_hidden :::"="::: ) (Set "x" ($#k6_algstr_0 :::"*"::: ) (Set (Var "z"))))); end; :: deftheorem defines :::"divides"::: GCD_1:def 1 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_gcd_1 :::"divides"::: ) (Set (Var "y"))) "iff" (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z"))))) ")" ))); definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); :: original: :::"divides"::: redefine pred "x" :::"divides"::: "y"; reflexivity (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")) "holds" (Bool ((Set (Const "R")) "," (Set (Var "b1")) "," (Set (Var "b1"))))) ; end; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); attr "x" is :::"unital"::: means :: GCD_1:def 2 (Bool "x" ($#r1_gcd_1 :::"divides"::: ) (Set ($#k5_struct_0 :::"1."::: ) "R")); end; :: deftheorem defines :::"unital"::: GCD_1:def 2 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v1_gcd_1 :::"unital"::: ) ) "iff" (Bool (Set (Var "x")) ($#r1_gcd_1 :::"divides"::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R")))) ")" ))); definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); pred "x" :::"is_associated_to"::: "y" means :: GCD_1:def 3 (Bool "(" (Bool "x" ($#r1_gcd_1 :::"divides"::: ) "y") & (Bool "y" ($#r1_gcd_1 :::"divides"::: ) "x") ")" ); symmetry (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")) "st" (Bool (Bool (Set (Var "x")) ($#r1_gcd_1 :::"divides"::: ) (Set (Var "y"))) & (Bool (Set (Var "y")) ($#r1_gcd_1 :::"divides"::: ) (Set (Var "x")))) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r1_gcd_1 :::"divides"::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_gcd_1 :::"divides"::: ) (Set (Var "y"))) ")" )) ; end; :: deftheorem defines :::"is_associated_to"::: GCD_1:def 3 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r3_gcd_1 :::"is_associated_to"::: ) (Set (Var "y"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_gcd_1 :::"divides"::: ) (Set (Var "y"))) & (Bool (Set (Var "y")) ($#r1_gcd_1 :::"divides"::: ) (Set (Var "x"))) ")" ) ")" ))); notationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); antonym "x" :::"is_not_associated_to"::: "y" for "x" :::"is_associated_to"::: "y"; end; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); :: original: :::"is_associated_to"::: redefine pred "x" :::"is_associated_to"::: "y"; reflexivity (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")) "holds" (Bool ((Set (Const "R")) "," (Set (Var "b1")) "," (Set (Var "b1"))))) ; end; definitionlet "R" be ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"Ring":::); let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); assume (Bool (Set (Const "y")) ($#r2_gcd_1 :::"divides"::: ) (Set (Const "x"))) ; assume (Bool (Set (Const "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Const "R")))) ; func "x" :::"/"::: "y" -> ($#m1_subset_1 :::"Element":::) "of" "R" means :: GCD_1:def 4 (Bool (Set it ($#k8_group_1 :::"*"::: ) "y") ($#r1_hidden :::"="::: ) "x"); end; :: deftheorem defines :::"/"::: GCD_1:def 4 : (Bool "for" (Set (Var "R")) "being" ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "y")) ($#r2_gcd_1 :::"divides"::: ) (Set (Var "x"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R"))))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_gcd_1 :::"/"::: ) (Set (Var "y")))) "iff" (Bool (Set (Set (Var "b4")) ($#k8_group_1 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )))); theorem :: GCD_1:2 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "a")) ($#r1_gcd_1 :::"divides"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_gcd_1 :::"divides"::: ) (Set (Var "c")))) "holds" (Bool (Set (Var "a")) ($#r1_gcd_1 :::"divides"::: ) (Set (Var "c"))))) ; theorem :: GCD_1:3 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "b")) ($#r1_gcd_1 :::"divides"::: ) (Set (Var "a"))) & (Bool (Set (Var "d")) ($#r1_gcd_1 :::"divides"::: ) (Set (Var "c")))) "holds" (Bool (Set (Set (Var "b")) ($#k8_group_1 :::"*"::: ) (Set (Var "d"))) ($#r1_gcd_1 :::"divides"::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "c")))))) ; theorem :: GCD_1:4 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "a")) ($#r3_gcd_1 :::"is_associated_to"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r3_gcd_1 :::"is_associated_to"::: ) (Set (Var "c")))) "holds" (Bool (Set (Var "a")) ($#r3_gcd_1 :::"is_associated_to"::: ) (Set (Var "c"))))) ; theorem :: GCD_1:5 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "a")) ($#r1_gcd_1 :::"divides"::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "c")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_gcd_1 :::"divides"::: ) (Set (Set (Var "c")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")))))) ; theorem :: GCD_1:6 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_gcd_1 :::"divides"::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")))) & "(" (Bool (Bool (Set (Var "R")) "is" ($#v5_group_1 :::"commutative"::: ) )) "implies" (Bool (Set (Var "b")) ($#r1_gcd_1 :::"divides"::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")))) ")" ")" ))) ; theorem :: GCD_1:7 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "a")) ($#r1_gcd_1 :::"divides"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "a")) ($#r1_gcd_1 :::"divides"::: ) (Set (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "c")))))) ; theorem :: GCD_1:8 (Bool "for" (Set (Var "R")) "being" ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "b")) ($#r2_gcd_1 :::"divides"::: ) (Set (Var "a"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R"))))) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k1_gcd_1 :::"/"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) "iff" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) ")" ))) ; theorem :: GCD_1:9 (Bool "for" (Set (Var "R")) "being" ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R"))))) "holds" (Bool (Set (Set (Var "a")) ($#k1_gcd_1 :::"/"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R")))))) ; theorem :: GCD_1:10 (Bool "for" (Set (Var "R")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool (Set (Set (Var "a")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: GCD_1:11 (Bool "for" (Set (Var "R")) "being" ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "c")) ($#r2_gcd_1 :::"divides"::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "b")))) & (Bool (Set (Var "c")) ($#r2_gcd_1 :::"divides"::: ) (Set (Var "a")))) "implies" (Bool (Set (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k1_gcd_1 :::"/"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_gcd_1 :::"/"::: ) (Set (Var "c")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "b")))) ")" & "(" (Bool (Bool (Set (Var "c")) ($#r2_gcd_1 :::"divides"::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "b")))) & (Bool (Set (Var "c")) ($#r2_gcd_1 :::"divides"::: ) (Set (Var "b")))) "implies" (Bool (Set (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k1_gcd_1 :::"/"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k1_gcd_1 :::"/"::: ) (Set (Var "c")) ")" ))) ")" ")" ))) ; theorem :: GCD_1:12 (Bool "for" (Set (Var "R")) "being" ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) & (Bool (Set (Var "c")) ($#r2_gcd_1 :::"divides"::: ) (Set (Var "a"))) & (Bool (Set (Var "c")) ($#r2_gcd_1 :::"divides"::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r2_gcd_1 :::"divides"::: ) (Set (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b"))))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_gcd_1 :::"/"::: ) (Set (Var "c")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_gcd_1 :::"/"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b")) ")" ) ($#k1_gcd_1 :::"/"::: ) (Set (Var "c")))))) ; theorem :: GCD_1:13 (Bool "for" (Set (Var "R")) "being" ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) & (Bool (Set (Var "c")) ($#r2_gcd_1 :::"divides"::: ) (Set (Var "a"))) & (Bool (Set (Var "c")) ($#r2_gcd_1 :::"divides"::: ) (Set (Var "b")))) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k1_gcd_1 :::"/"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_gcd_1 :::"/"::: ) (Set (Var "c")))) "iff" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ))) ; theorem :: GCD_1:14 (Bool "for" (Set (Var "R")) "being" ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) & (Bool (Set (Var "d")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) & (Bool (Set (Var "b")) ($#r2_gcd_1 :::"divides"::: ) (Set (Var "a"))) & (Bool (Set (Var "d")) ($#r2_gcd_1 :::"divides"::: ) (Set (Var "c")))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_gcd_1 :::"/"::: ) (Set (Var "b")) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "c")) ($#k1_gcd_1 :::"/"::: ) (Set (Var "d")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "c")) ")" ) ($#k1_gcd_1 :::"/"::: ) (Set "(" (Set (Var "b")) ($#k8_group_1 :::"*"::: ) (Set (Var "d")) ")" ))))) ; theorem :: GCD_1:15 (Bool "for" (Set (Var "R")) "being" ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) & (Bool (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "b"))) ($#r2_gcd_1 :::"divides"::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "c"))))) "holds" (Bool (Set (Var "b")) ($#r2_gcd_1 :::"divides"::: ) (Set (Var "c"))))) ; theorem :: GCD_1:16 (Bool "for" (Set (Var "R")) "being" ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "a")) ($#r4_gcd_1 :::"is_associated_to"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))))) ; theorem :: GCD_1:17 (Bool "for" (Set (Var "R")) "being" ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) & (Bool (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R")))))) ; theorem :: GCD_1:18 (Bool "for" (Set (Var "R")) "being" ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r4_gcd_1 :::"is_associated_to"::: ) (Set (Var "b"))) "iff" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "c")) "is" ($#v1_gcd_1 :::"unital"::: ) ) & (Bool (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" )) ")" ))) ; theorem :: GCD_1:19 (Bool "for" (Set (Var "R")) "being" ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) & (Bool (Set (Set (Var "c")) ($#k8_group_1 :::"*"::: ) (Set (Var "a"))) ($#r4_gcd_1 :::"is_associated_to"::: ) (Set (Set (Var "c")) ($#k8_group_1 :::"*"::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "a")) ($#r4_gcd_1 :::"is_associated_to"::: ) (Set (Var "b"))))) ; begin definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); func :::"Class"::: "a" -> ($#m1_subset_1 :::"Subset":::) "of" "R" means :: GCD_1:def 5 (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "R" "holds" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "b")) ($#r3_gcd_1 :::"is_associated_to"::: ) "a") ")" )); end; :: deftheorem defines :::"Class"::: GCD_1:def 5 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_gcd_1 :::"Class"::: ) (Set (Var "a")))) "iff" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool (Set (Var "b")) ($#r3_gcd_1 :::"is_associated_to"::: ) (Set (Var "a"))) ")" )) ")" )))); registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); cluster (Set ($#k2_gcd_1 :::"Class"::: ) "a") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: GCD_1:20 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set ($#k2_gcd_1 :::"Class"::: ) (Set (Var "a"))) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k2_gcd_1 :::"Class"::: ) (Set (Var "b"))))) "holds" (Bool (Set ($#k2_gcd_1 :::"Class"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k2_gcd_1 :::"Class"::: ) (Set (Var "b")))))) ; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; func :::"Classes"::: "R" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "R" means :: GCD_1:def 6 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "R" "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "R" "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_gcd_1 :::"Class"::: ) (Set (Var "a"))))) ")" )); end; :: deftheorem defines :::"Classes"::: GCD_1:def 6 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_gcd_1 :::"Classes"::: ) (Set (Var "R")))) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_gcd_1 :::"Class"::: ) (Set (Var "a"))))) ")" )) ")" ))); registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; cluster (Set ($#k3_gcd_1 :::"Classes"::: ) "R") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: GCD_1:21 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k3_gcd_1 :::"Classes"::: ) (Set (Var "R"))))) "holds" (Bool "not" (Bool (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) )))) ; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; mode :::"Am"::: "of" "R" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" "R" means :: GCD_1:def 7 (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "R" (Bool "ex" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" it "st" (Bool (Set (Var "z")) ($#r4_gcd_1 :::"is_associated_to"::: ) (Set (Var "a")))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" it "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "x")) ($#r3_gcd_1 :::"is_not_associated_to"::: ) (Set (Var "y"))) ")" ) ")" ); end; :: deftheorem defines :::"Am"::: GCD_1:def 7 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_gcd_1 :::"Am"::: ) "of" (Set (Var "R"))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "ex" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "b2")) "st" (Bool (Set (Var "z")) ($#r4_gcd_1 :::"is_associated_to"::: ) (Set (Var "a")))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "b2")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "x")) ($#r3_gcd_1 :::"is_not_associated_to"::: ) (Set (Var "y"))) ")" ) ")" ) ")" ))); definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; mode :::"AmpleSet"::: "of" "R" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" "R" means :: GCD_1:def 8 (Bool "(" (Bool it "is" ($#m1_gcd_1 :::"Am"::: ) "of" "R") & (Bool (Set ($#k5_struct_0 :::"1."::: ) "R") ($#r2_hidden :::"in"::: ) it) ")" ); end; :: deftheorem defines :::"AmpleSet"::: GCD_1:def 8 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R"))) "iff" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_gcd_1 :::"Am"::: ) "of" (Set (Var "R"))) & (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R"))) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) ")" ) ")" ))); theorem :: GCD_1:22 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R"))) ($#r2_hidden :::"in"::: ) (Set (Var "Amp"))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "ex" (Set (Var "z")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "Amp")) "st" (Bool (Set (Var "z")) ($#r4_gcd_1 :::"is_associated_to"::: ) (Set (Var "a")))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "Amp")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "x")) ($#r3_gcd_1 :::"is_not_associated_to"::: ) (Set (Var "y"))) ")" ) ")" ))) ; theorem :: GCD_1:23 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "Amp")) "st" (Bool (Bool (Set (Var "x")) ($#r4_gcd_1 :::"is_associated_to"::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))))) ; theorem :: GCD_1:24 (Bool "for" (Set (Var "R")) "being" ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R"))) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "Amp"))))) ; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; let "Amp" be ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Const "R")); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); func :::"NF"::: "(" "x" "," "Amp" ")" -> ($#m1_subset_1 :::"Element":::) "of" "R" means :: GCD_1:def 9 (Bool "(" (Bool it ($#r2_hidden :::"in"::: ) "Amp") & (Bool it ($#r4_gcd_1 :::"is_associated_to"::: ) "x") ")" ); end; :: deftheorem defines :::"NF"::: GCD_1:def 9 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "x")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_gcd_1 :::"NF"::: ) "(" (Set (Var "x")) "," (Set (Var "Amp")) ")" )) "iff" (Bool "(" (Bool (Set (Var "b4")) ($#r2_hidden :::"in"::: ) (Set (Var "Amp"))) & (Bool (Set (Var "b4")) ($#r4_gcd_1 :::"is_associated_to"::: ) (Set (Var "x"))) ")" ) ")" )))); theorem :: GCD_1:25 (Bool "for" (Set (Var "R")) "being" ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set ($#k4_gcd_1 :::"NF"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "R")) ")" ) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) & (Bool (Set ($#k4_gcd_1 :::"NF"::: ) "(" (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "R")) ")" ) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R")))) ")" ))) ; theorem :: GCD_1:26 (Bool "for" (Set (Var "R")) "being" ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "Amp"))) "iff" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k4_gcd_1 :::"NF"::: ) "(" (Set (Var "a")) "," (Set (Var "Amp")) ")" )) ")" )))) ; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; let "Amp" be ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Const "R")); attr "Amp" is :::"multiplicative"::: means :: GCD_1:def 10 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" "Amp" "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) "Amp")); end; :: deftheorem defines :::"multiplicative"::: GCD_1:def 10 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "Amp")) "is" ($#v2_gcd_1 :::"multiplicative"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "Amp")) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Var "Amp")))) ")" ))); theorem :: GCD_1:27 (Bool "for" (Set (Var "R")) "being" ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "Amp")) "is" ($#v2_gcd_1 :::"multiplicative"::: ) )) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "Amp")) "st" (Bool (Bool (Set (Var "y")) ($#r2_gcd_1 :::"divides"::: ) (Set (Var "x"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R"))))) "holds" (Bool (Set (Set (Var "x")) ($#k1_gcd_1 :::"/"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Var "Amp")))))) ; begin definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; attr "R" is :::"gcd-like"::: means :: GCD_1:def 11 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "R" (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "R" "st" (Bool "(" (Bool (Set (Var "z")) ($#r1_gcd_1 :::"divides"::: ) (Set (Var "x"))) & (Bool (Set (Var "z")) ($#r1_gcd_1 :::"divides"::: ) (Set (Var "y"))) & (Bool "(" "for" (Set (Var "zz")) "being" ($#m1_subset_1 :::"Element":::) "of" "R" "st" (Bool (Bool (Set (Var "zz")) ($#r1_gcd_1 :::"divides"::: ) (Set (Var "x"))) & (Bool (Set (Var "zz")) ($#r1_gcd_1 :::"divides"::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "zz")) ($#r1_gcd_1 :::"divides"::: ) (Set (Var "z"))) ")" ) ")" ))); end; :: deftheorem defines :::"gcd-like"::: GCD_1:def 11 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v3_gcd_1 :::"gcd-like"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "z")) ($#r1_gcd_1 :::"divides"::: ) (Set (Var "x"))) & (Bool (Set (Var "z")) ($#r1_gcd_1 :::"divides"::: ) (Set (Var "y"))) & (Bool "(" "for" (Set (Var "zz")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "zz")) ($#r1_gcd_1 :::"divides"::: ) (Set (Var "x"))) & (Bool (Set (Var "zz")) ($#r1_gcd_1 :::"divides"::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "zz")) ($#r1_gcd_1 :::"divides"::: ) (Set (Var "z"))) ")" ) ")" ))) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) bbbadV7_STRUCT_0() ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#v3_gcd_1 :::"gcd-like"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_gcd_1 :::"gcd-like"::: ) for ($#l4_algstr_0 :::"multLoopStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_gcd_1 :::"gcd-like"::: ) for ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_gcd_1 :::"gcd-like"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#v3_gcd_1 :::"gcd-like"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; definitionmode gcdDomain is ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#v3_gcd_1 :::"gcd-like"::: ) ($#l6_algstr_0 :::"Ring":::); end; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_gcd_1 :::"gcd-like"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; let "Amp" be ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Const "R")); let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); func :::"gcd"::: "(" "x" "," "y" "," "Amp" ")" -> ($#m1_subset_1 :::"Element":::) "of" "R" means :: GCD_1:def 12 (Bool "(" (Bool it ($#r2_hidden :::"in"::: ) "Amp") & (Bool it ($#r2_gcd_1 :::"divides"::: ) "x") & (Bool it ($#r2_gcd_1 :::"divides"::: ) "y") & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "R" "st" (Bool (Bool (Set (Var "z")) ($#r2_gcd_1 :::"divides"::: ) "x") & (Bool (Set (Var "z")) ($#r2_gcd_1 :::"divides"::: ) "y")) "holds" (Bool (Set (Var "z")) ($#r2_gcd_1 :::"divides"::: ) it) ")" ) ")" ); end; :: deftheorem defines :::"gcd"::: GCD_1:def 12 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_gcd_1 :::"gcd-like"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "b5")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "Amp")) ")" )) "iff" (Bool "(" (Bool (Set (Var "b5")) ($#r2_hidden :::"in"::: ) (Set (Var "Amp"))) & (Bool (Set (Var "b5")) ($#r2_gcd_1 :::"divides"::: ) (Set (Var "x"))) & (Bool (Set (Var "b5")) ($#r2_gcd_1 :::"divides"::: ) (Set (Var "y"))) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "z")) ($#r2_gcd_1 :::"divides"::: ) (Set (Var "x"))) & (Bool (Set (Var "z")) ($#r2_gcd_1 :::"divides"::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "z")) ($#r2_gcd_1 :::"divides"::: ) (Set (Var "b5"))) ")" ) ")" ) ")" )))); theorem :: GCD_1:28 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"gcdDomain":::) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "c")) ($#r2_gcd_1 :::"divides"::: ) (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "Amp")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r2_gcd_1 :::"divides"::: ) (Set (Var "a"))) & (Bool (Set (Var "c")) ($#r2_gcd_1 :::"divides"::: ) (Set (Var "b"))) ")" )))) ; theorem :: GCD_1:29 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"gcdDomain":::) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "Amp")) ")" ))))) ; theorem :: GCD_1:30 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"gcdDomain":::) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "R")) ")" ) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_gcd_1 :::"NF"::: ) "(" (Set (Var "a")) "," (Set (Var "Amp")) ")" )) & (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "R")) ")" ) "," (Set (Var "a")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_gcd_1 :::"NF"::: ) "(" (Set (Var "a")) "," (Set (Var "Amp")) ")" )) ")" )))) ; theorem :: GCD_1:31 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"gcdDomain":::) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) "holds" (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "R")) ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "R")) ")" ) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))))) ; theorem :: GCD_1:32 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"gcdDomain":::) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "R")) ")" ) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R")))) & (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "R")) ")" ) "," (Set (Var "a")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R")))) ")" )))) ; theorem :: GCD_1:33 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"gcdDomain":::) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) ")" ) ")" )))) ; theorem :: GCD_1:34 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"gcdDomain":::) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "b")) ($#r4_gcd_1 :::"is_associated_to"::: ) (Set (Var "c")))) "holds" (Bool "(" (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "Amp")) ")" ) ($#r4_gcd_1 :::"is_associated_to"::: ) (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "Amp")) ")" )) & (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "Amp")) ")" ) ($#r4_gcd_1 :::"is_associated_to"::: ) (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "Amp")) ")" )) ")" )))) ; theorem :: GCD_1:35 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"gcdDomain":::) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "Amp")) ")" ")" ) "," (Set (Var "c")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "Amp")) ")" ")" ) "," (Set (Var "Amp")) ")" ))))) ; theorem :: GCD_1:36 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"gcdDomain":::) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "c")) ")" ) "," (Set "(" (Set (Var "b")) ($#k8_group_1 :::"*"::: ) (Set (Var "c")) ")" ) "," (Set (Var "Amp")) ")" ) ($#r4_gcd_1 :::"is_associated_to"::: ) (Set (Set (Var "c")) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "Amp")) ")" ")" )))))) ; theorem :: GCD_1:37 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"gcdDomain":::) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R"))))) "holds" (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "b")) ($#k8_group_1 :::"*"::: ) (Set (Var "c")) ")" ) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "Amp")) ")" ))))) ; theorem :: GCD_1:38 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"gcdDomain":::) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "Amp")) ")" )) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R"))))) "holds" (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set "(" (Set (Var "a")) ($#k1_gcd_1 :::"/"::: ) (Set (Var "c")) ")" ) "," (Set "(" (Set (Var "b")) ($#k1_gcd_1 :::"/"::: ) (Set (Var "c")) ")" ) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R"))))))) ; theorem :: GCD_1:39 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"gcdDomain":::) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set "(" (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k8_group_1 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) "," (Set (Var "c")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "Amp")) ")" ))))) ; begin theorem :: GCD_1:40 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"gcdDomain":::) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R")))) & (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R")))) & (Bool (Set (Var "r2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R"))))) "holds" (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set "(" (Set "(" (Set (Var "r1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "s2")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r2")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "s1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "r2")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r2")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) ")" ) ")" ) ")" ) "," (Set "(" (Set (Var "r2")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "s2")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r2")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) ")" ) ")" ) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set "(" (Set "(" (Set (Var "r1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "s2")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r2")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "s1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "r2")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r2")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) ")" ) ")" ) ")" ) "," (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r2")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) "," (Set (Var "Amp")) ")" ))))) ; theorem :: GCD_1:41 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"gcdDomain":::) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R")))) & (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R")))) & (Bool (Set (Var "r2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) & (Bool (Set (Var "s2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R"))))) "holds" (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set "(" (Set "(" (Set (Var "r1")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "s1")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "s1")) "," (Set (Var "r2")) "," (Set (Var "Amp")) ")" ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "r2")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "s1")) "," (Set (Var "r2")) "," (Set (Var "Amp")) ")" ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "s2")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) ")" ) ")" ) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R"))))))) ; begin definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_gcd_1 :::"gcd-like"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; let "Amp" be ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Const "R")); let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); pred "x" "," "y" :::"are_canonical_wrt"::: "Amp" means :: GCD_1:def 13 (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" "x" "," "y" "," "Amp" ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "R")); end; :: deftheorem defines :::"are_canonical_wrt"::: GCD_1:def 13 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_gcd_1 :::"gcd-like"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r5_gcd_1 :::"are_canonical_wrt"::: ) (Set (Var "Amp"))) "iff" (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R")))) ")" )))); theorem :: GCD_1:42 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"gcdDomain":::) (Bool "for" (Set (Var "Amp")) "," (Set (Var "Amp9")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r5_gcd_1 :::"are_canonical_wrt"::: ) (Set (Var "Amp")))) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r5_gcd_1 :::"are_canonical_wrt"::: ) (Set (Var "Amp9")))))) ; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_gcd_1 :::"gcd-like"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); pred "x" "," "y" :::"are_co-prime"::: means :: GCD_1:def 14 (Bool "ex" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" "R" "st" (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" "x" "," "y" "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "R"))); end; :: deftheorem defines :::"are_co-prime"::: GCD_1:def 14 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_gcd_1 :::"gcd-like"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r6_gcd_1 :::"are_co-prime"::: ) ) "iff" (Bool "ex" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) "st" (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R"))))) ")" ))); definitionlet "R" be ($#l6_algstr_0 :::"gcdDomain":::); let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); :: original: :::"are_co-prime"::: redefine pred "x" "," "y" :::"are_co-prime"::: ; symmetry (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")) "st" (Bool (Bool ((Set (Const "R")) "," (Set (Var "b1")) "," (Set (Var "b2"))))) "holds" (Bool ((Set (Const "R")) "," (Set (Var "b2")) "," (Set (Var "b1"))))) ; end; theorem :: GCD_1:43 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"gcdDomain":::) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r7_gcd_1 :::"are_co-prime"::: ) )) "holds" (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R"))))))) ; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_gcd_1 :::"gcd-like"::: ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; let "Amp" be ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Const "R")); let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); pred "x" "," "y" :::"are_normalized_wrt"::: "Amp" means :: GCD_1:def 15 (Bool "(" (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" "x" "," "y" "," "Amp" ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "R")) & (Bool "y" ($#r2_hidden :::"in"::: ) "Amp") & (Bool "y" ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) "R")) ")" ); end; :: deftheorem defines :::"are_normalized_wrt"::: GCD_1:def 15 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_gcd_1 :::"gcd-like"::: ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r8_gcd_1 :::"are_normalized_wrt"::: ) (Set (Var "Amp"))) "iff" (Bool "(" (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Amp"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) ")" ) ")" )))); definitionlet "R" be ($#l6_algstr_0 :::"gcdDomain":::); let "Amp" be ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Const "R")); let "r1", "r2", "s1", "s2" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); assume that (Bool (Set (Const "r1")) "," (Set (Const "r2")) ($#r7_gcd_1 :::"are_co-prime"::: ) ) and (Bool (Set (Const "s1")) "," (Set (Const "s2")) ($#r7_gcd_1 :::"are_co-prime"::: ) ) and (Bool (Set (Const "r2")) ($#r1_hidden :::"="::: ) (Set ($#k4_gcd_1 :::"NF"::: ) "(" (Set (Const "r2")) "," (Set (Const "Amp")) ")" )) and (Bool (Set (Const "s2")) ($#r1_hidden :::"="::: ) (Set ($#k4_gcd_1 :::"NF"::: ) "(" (Set (Const "s2")) "," (Set (Const "Amp")) ")" )) ; func :::"add1"::: "(" "r1" "," "r2" "," "s1" "," "s2" "," "Amp" ")" -> ($#m1_subset_1 :::"Element":::) "of" "R" equals :: GCD_1:def 16 "s1" if (Bool "r1" ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "R")) "r1" if (Bool "s1" ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "R")) (Set (Set "(" "r1" ($#k8_group_1 :::"*"::: ) "s2" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" "r2" ($#k8_group_1 :::"*"::: ) "s1" ")" )) if (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" "r2" "," "s2" "," "Amp" ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "R")) (Set ($#k4_struct_0 :::"0."::: ) "R") if (Bool (Set (Set "(" "r1" ($#k8_group_1 :::"*"::: ) (Set "(" "s2" ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" "r2" "," "s2" "," "Amp" ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" "s1" ($#k8_group_1 :::"*"::: ) (Set "(" "r2" ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" "r2" "," "s2" "," "Amp" ")" ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "R")) otherwise (Set (Set "(" (Set "(" "r1" ($#k8_group_1 :::"*"::: ) (Set "(" "s2" ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" "r2" "," "s2" "," "Amp" ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" "s1" ($#k8_group_1 :::"*"::: ) (Set "(" "r2" ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" "r2" "," "s2" "," "Amp" ")" ")" ) ")" ) ")" ) ")" ) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set "(" (Set "(" "r1" ($#k8_group_1 :::"*"::: ) (Set "(" "s2" ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" "r2" "," "s2" "," "Amp" ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" "s1" ($#k8_group_1 :::"*"::: ) (Set "(" "r2" ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" "r2" "," "s2" "," "Amp" ")" ")" ) ")" ) ")" ) ")" ) "," (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" "r2" "," "s2" "," "Amp" ")" ")" ) "," "Amp" ")" ")" )); end; :: deftheorem defines :::"add1"::: GCD_1:def 16 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"gcdDomain":::) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "r1")) "," (Set (Var "r2")) ($#r7_gcd_1 :::"are_co-prime"::: ) ) & (Bool (Set (Var "s1")) "," (Set (Var "s2")) ($#r7_gcd_1 :::"are_co-prime"::: ) ) & (Bool (Set (Var "r2")) ($#r1_hidden :::"="::: ) (Set ($#k4_gcd_1 :::"NF"::: ) "(" (Set (Var "r2")) "," (Set (Var "Amp")) ")" )) & (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set ($#k4_gcd_1 :::"NF"::: ) "(" (Set (Var "s2")) "," (Set (Var "Amp")) ")" ))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "r1")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R"))))) "implies" (Bool (Set ($#k6_gcd_1 :::"add1"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "s1"))) ")" & "(" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R"))))) "implies" (Bool (Set ($#k6_gcd_1 :::"add1"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "r1"))) ")" & "(" (Bool (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r2")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R"))))) "implies" (Bool (Set ($#k6_gcd_1 :::"add1"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r1")) ($#k8_group_1 :::"*"::: ) (Set (Var "s2")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "r2")) ($#k8_group_1 :::"*"::: ) (Set (Var "s1")) ")" ))) ")" & "(" (Bool (Bool (Set (Set "(" (Set (Var "r1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "s2")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r2")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "s1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "r2")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r2")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R"))))) "implies" (Bool (Set ($#k6_gcd_1 :::"add1"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "r1")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R"))))) & (Bool (Bool "not" (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R"))))) & (Bool (Bool "not" (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r2")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R"))))) & (Bool (Bool "not" (Set (Set "(" (Set (Var "r1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "s2")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r2")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "s1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "r2")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r2")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))))) "implies" (Bool (Set ($#k6_gcd_1 :::"add1"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "r1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "s2")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r2")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "s1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "r2")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r2")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) ")" ) ")" ) ")" ) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set "(" (Set "(" (Set (Var "r1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "s2")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r2")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "s1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "r2")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r2")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) ")" ) ")" ) ")" ) "," (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r2")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) "," (Set (Var "Amp")) ")" ")" ))) ")" ")" )))); definitionlet "R" be ($#l6_algstr_0 :::"gcdDomain":::); let "Amp" be ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Const "R")); let "r1", "r2", "s1", "s2" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); assume that (Bool (Set (Const "r1")) "," (Set (Const "r2")) ($#r7_gcd_1 :::"are_co-prime"::: ) ) and (Bool (Set (Const "s1")) "," (Set (Const "s2")) ($#r7_gcd_1 :::"are_co-prime"::: ) ) and (Bool (Set (Const "r2")) ($#r1_hidden :::"="::: ) (Set ($#k4_gcd_1 :::"NF"::: ) "(" (Set (Const "r2")) "," (Set (Const "Amp")) ")" )) and (Bool (Set (Const "s2")) ($#r1_hidden :::"="::: ) (Set ($#k4_gcd_1 :::"NF"::: ) "(" (Set (Const "s2")) "," (Set (Const "Amp")) ")" )) ; func :::"add2"::: "(" "r1" "," "r2" "," "s1" "," "s2" "," "Amp" ")" -> ($#m1_subset_1 :::"Element":::) "of" "R" equals :: GCD_1:def 17 "s2" if (Bool "r1" ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "R")) "r2" if (Bool "s1" ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "R")) (Set "r2" ($#k8_group_1 :::"*"::: ) "s2") if (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" "r2" "," "s2" "," "Amp" ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "R")) (Set ($#k5_struct_0 :::"1."::: ) "R") if (Bool (Set (Set "(" "r1" ($#k8_group_1 :::"*"::: ) (Set "(" "s2" ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" "r2" "," "s2" "," "Amp" ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" "s1" ($#k8_group_1 :::"*"::: ) (Set "(" "r2" ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" "r2" "," "s2" "," "Amp" ")" ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "R")) otherwise (Set (Set "(" "r2" ($#k8_group_1 :::"*"::: ) (Set "(" "s2" ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" "r2" "," "s2" "," "Amp" ")" ")" ) ")" ) ")" ) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set "(" (Set "(" "r1" ($#k8_group_1 :::"*"::: ) (Set "(" "s2" ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" "r2" "," "s2" "," "Amp" ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" "s1" ($#k8_group_1 :::"*"::: ) (Set "(" "r2" ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" "r2" "," "s2" "," "Amp" ")" ")" ) ")" ) ")" ) ")" ) "," (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" "r2" "," "s2" "," "Amp" ")" ")" ) "," "Amp" ")" ")" )); end; :: deftheorem defines :::"add2"::: GCD_1:def 17 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"gcdDomain":::) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "r1")) "," (Set (Var "r2")) ($#r7_gcd_1 :::"are_co-prime"::: ) ) & (Bool (Set (Var "s1")) "," (Set (Var "s2")) ($#r7_gcd_1 :::"are_co-prime"::: ) ) & (Bool (Set (Var "r2")) ($#r1_hidden :::"="::: ) (Set ($#k4_gcd_1 :::"NF"::: ) "(" (Set (Var "r2")) "," (Set (Var "Amp")) ")" )) & (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set ($#k4_gcd_1 :::"NF"::: ) "(" (Set (Var "s2")) "," (Set (Var "Amp")) ")" ))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "r1")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R"))))) "implies" (Bool (Set ($#k7_gcd_1 :::"add2"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "s2"))) ")" & "(" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R"))))) "implies" (Bool (Set ($#k7_gcd_1 :::"add2"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "r2"))) ")" & "(" (Bool (Bool (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r2")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R"))))) "implies" (Bool (Set ($#k7_gcd_1 :::"add2"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r2")) ($#k8_group_1 :::"*"::: ) (Set (Var "s2")))) ")" & "(" (Bool (Bool (Set (Set "(" (Set (Var "r1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "s2")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r2")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "s1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "r2")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r2")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R"))))) "implies" (Bool (Set ($#k7_gcd_1 :::"add2"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R")))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "r1")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R"))))) & (Bool (Bool "not" (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R"))))) & (Bool (Bool "not" (Set ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r2")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R"))))) & (Bool (Bool "not" (Set (Set "(" (Set (Var "r1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "s2")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r2")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "s1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "r2")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r2")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))))) "implies" (Bool (Set ($#k7_gcd_1 :::"add2"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r2")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "s2")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r2")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) ")" ) ")" ) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set "(" (Set "(" (Set (Var "r1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "s2")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r2")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "s1")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "r2")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r2")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) ")" ) ")" ) ")" ) "," (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r2")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) "," (Set (Var "Amp")) ")" ")" ))) ")" ")" )))); theorem :: GCD_1:44 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"gcdDomain":::) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "Amp")) "is" ($#v2_gcd_1 :::"multiplicative"::: ) ) & (Bool (Set (Var "r1")) "," (Set (Var "r2")) ($#r8_gcd_1 :::"are_normalized_wrt"::: ) (Set (Var "Amp"))) & (Bool (Set (Var "s1")) "," (Set (Var "s2")) ($#r8_gcd_1 :::"are_normalized_wrt"::: ) (Set (Var "Amp")))) "holds" (Bool (Set ($#k6_gcd_1 :::"add1"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) "," (Set ($#k7_gcd_1 :::"add2"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) ($#r8_gcd_1 :::"are_normalized_wrt"::: ) (Set (Var "Amp")))))) ; theorem :: GCD_1:45 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"gcdDomain":::) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "r1")) "," (Set (Var "r2")) ($#r8_gcd_1 :::"are_normalized_wrt"::: ) (Set (Var "Amp"))) & (Bool (Set (Var "s1")) "," (Set (Var "s2")) ($#r8_gcd_1 :::"are_normalized_wrt"::: ) (Set (Var "Amp")))) "holds" (Bool (Set (Set "(" ($#k6_gcd_1 :::"add1"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "r2")) ($#k8_group_1 :::"*"::: ) (Set (Var "s2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_gcd_1 :::"add2"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "r1")) ($#k8_group_1 :::"*"::: ) (Set (Var "s2")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "s1")) ($#k8_group_1 :::"*"::: ) (Set (Var "r2")) ")" ) ")" )))))) ; definitionlet "R" be ($#l6_algstr_0 :::"gcdDomain":::); let "Amp" be ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Const "R")); let "r1", "r2", "s1", "s2" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); func :::"mult1"::: "(" "r1" "," "r2" "," "s1" "," "s2" "," "Amp" ")" -> ($#m1_subset_1 :::"Element":::) "of" "R" equals :: GCD_1:def 18 (Set ($#k4_struct_0 :::"0."::: ) "R") if (Bool "(" (Bool "r1" ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "R")) "or" (Bool "s1" ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "R")) ")" ) (Set "r1" ($#k8_group_1 :::"*"::: ) "s1") if (Bool "(" (Bool "r2" ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "R")) & (Bool "s2" ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "R")) ")" ) (Set (Set "(" "r1" ($#k8_group_1 :::"*"::: ) "s1" ")" ) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" "r1" "," "s2" "," "Amp" ")" ")" )) if (Bool "(" (Bool "s2" ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) "R")) & (Bool "r2" ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "R")) ")" ) (Set (Set "(" "r1" ($#k8_group_1 :::"*"::: ) "s1" ")" ) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" "s1" "," "r2" "," "Amp" ")" ")" )) if (Bool "(" (Bool "r2" ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) "R")) & (Bool "s2" ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "R")) ")" ) otherwise (Set (Set "(" "r1" ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" "r1" "," "s2" "," "Amp" ")" ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" "s1" ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" "s1" "," "r2" "," "Amp" ")" ")" ) ")" )); end; :: deftheorem defines :::"mult1"::: GCD_1:def 18 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"gcdDomain":::) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" "(" (Bool (Bool "(" (Bool (Set (Var "r1")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) "or" (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) ")" )) "implies" (Bool (Set ($#k8_gcd_1 :::"mult1"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) ")" & "(" (Bool (Bool (Set (Var "r2")) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R")))) & (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R"))))) "implies" (Bool (Set ($#k8_gcd_1 :::"mult1"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r1")) ($#k8_group_1 :::"*"::: ) (Set (Var "s1")))) ")" & "(" (Bool (Bool (Set (Var "s2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) & (Bool (Set (Var "r2")) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R"))))) "implies" (Bool (Set ($#k8_gcd_1 :::"mult1"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r1")) ($#k8_group_1 :::"*"::: ) (Set (Var "s1")) ")" ) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ))) ")" & "(" (Bool (Bool (Set (Var "r2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) & (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R"))))) "implies" (Bool (Set ($#k8_gcd_1 :::"mult1"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r1")) ($#k8_group_1 :::"*"::: ) (Set (Var "s1")) ")" ) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "s1")) "," (Set (Var "r2")) "," (Set (Var "Amp")) ")" ")" ))) ")" & (Bool "(" (Bool (Set (Var "r1")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) "or" (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) "or" (Bool "(" (Bool (Set (Var "r2")) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R")))) & (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R")))) ")" ) "or" (Bool "(" (Bool (Set (Var "s2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) & (Bool (Set (Var "r2")) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R")))) ")" ) "or" (Bool "(" (Bool (Set (Var "r2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) & (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R")))) ")" ) "or" (Bool (Set ($#k8_gcd_1 :::"mult1"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r1")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "s1")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "s1")) "," (Set (Var "r2")) "," (Set (Var "Amp")) ")" ")" ) ")" ))) ")" ) ")" )))); definitionlet "R" be ($#l6_algstr_0 :::"gcdDomain":::); let "Amp" be ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Const "R")); let "r1", "r2", "s1", "s2" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); assume that (Bool (Set (Const "r1")) "," (Set (Const "r2")) ($#r7_gcd_1 :::"are_co-prime"::: ) ) and (Bool (Set (Const "s1")) "," (Set (Const "s2")) ($#r7_gcd_1 :::"are_co-prime"::: ) ) and (Bool (Set (Const "r2")) ($#r1_hidden :::"="::: ) (Set ($#k4_gcd_1 :::"NF"::: ) "(" (Set (Const "r2")) "," (Set (Const "Amp")) ")" )) and (Bool (Set (Const "s2")) ($#r1_hidden :::"="::: ) (Set ($#k4_gcd_1 :::"NF"::: ) "(" (Set (Const "s2")) "," (Set (Const "Amp")) ")" )) ; func :::"mult2"::: "(" "r1" "," "r2" "," "s1" "," "s2" "," "Amp" ")" -> ($#m1_subset_1 :::"Element":::) "of" "R" equals :: GCD_1:def 19 (Set ($#k5_struct_0 :::"1."::: ) "R") if (Bool "(" (Bool "r1" ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "R")) "or" (Bool "s1" ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "R")) ")" ) (Set ($#k5_struct_0 :::"1."::: ) "R") if (Bool "(" (Bool "r2" ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "R")) & (Bool "s2" ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "R")) ")" ) (Set "s2" ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" "r1" "," "s2" "," "Amp" ")" ")" )) if (Bool "(" (Bool "s2" ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) "R")) & (Bool "r2" ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "R")) ")" ) (Set "r2" ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" "s1" "," "r2" "," "Amp" ")" ")" )) if (Bool "(" (Bool "r2" ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) "R")) & (Bool "s2" ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "R")) ")" ) otherwise (Set (Set "(" "r2" ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" "s1" "," "r2" "," "Amp" ")" ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" "s2" ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" "r1" "," "s2" "," "Amp" ")" ")" ) ")" )); end; :: deftheorem defines :::"mult2"::: GCD_1:def 19 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"gcdDomain":::) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "r1")) "," (Set (Var "r2")) ($#r7_gcd_1 :::"are_co-prime"::: ) ) & (Bool (Set (Var "s1")) "," (Set (Var "s2")) ($#r7_gcd_1 :::"are_co-prime"::: ) ) & (Bool (Set (Var "r2")) ($#r1_hidden :::"="::: ) (Set ($#k4_gcd_1 :::"NF"::: ) "(" (Set (Var "r2")) "," (Set (Var "Amp")) ")" )) & (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set ($#k4_gcd_1 :::"NF"::: ) "(" (Set (Var "s2")) "," (Set (Var "Amp")) ")" ))) "holds" (Bool "(" "(" (Bool (Bool "(" (Bool (Set (Var "r1")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) "or" (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) ")" )) "implies" (Bool (Set ($#k9_gcd_1 :::"mult2"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R")))) ")" & "(" (Bool (Bool (Set (Var "r2")) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R")))) & (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R"))))) "implies" (Bool (Set ($#k9_gcd_1 :::"mult2"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R")))) ")" & "(" (Bool (Bool (Set (Var "s2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) & (Bool (Set (Var "r2")) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R"))))) "implies" (Bool (Set ($#k9_gcd_1 :::"mult2"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ))) ")" & "(" (Bool (Bool (Set (Var "r2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) & (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R"))))) "implies" (Bool (Set ($#k9_gcd_1 :::"mult2"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r2")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "s1")) "," (Set (Var "r2")) "," (Set (Var "Amp")) ")" ")" ))) ")" & (Bool "(" (Bool (Set (Var "r1")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) "or" (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) "or" (Bool "(" (Bool (Set (Var "r2")) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R")))) & (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R")))) ")" ) "or" (Bool "(" (Bool (Set (Var "s2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) & (Bool (Set (Var "r2")) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R")))) ")" ) "or" (Bool "(" (Bool (Set (Var "r2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) & (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "R")))) ")" ) "or" (Bool (Set ($#k9_gcd_1 :::"mult2"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r2")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "s1")) "," (Set (Var "r2")) "," (Set (Var "Amp")) ")" ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "s2")) ($#k1_gcd_1 :::"/"::: ) (Set "(" ($#k5_gcd_1 :::"gcd"::: ) "(" (Set (Var "r1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) ")" ))) ")" ) ")" )))); theorem :: GCD_1:46 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"gcdDomain":::) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "Amp")) "is" ($#v2_gcd_1 :::"multiplicative"::: ) ) & (Bool (Set (Var "r1")) "," (Set (Var "r2")) ($#r8_gcd_1 :::"are_normalized_wrt"::: ) (Set (Var "Amp"))) & (Bool (Set (Var "s1")) "," (Set (Var "s2")) ($#r8_gcd_1 :::"are_normalized_wrt"::: ) (Set (Var "Amp")))) "holds" (Bool (Set ($#k8_gcd_1 :::"mult1"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) "," (Set ($#k9_gcd_1 :::"mult2"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ) ($#r8_gcd_1 :::"are_normalized_wrt"::: ) (Set (Var "Amp")))))) ; theorem :: GCD_1:47 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"gcdDomain":::) (Bool "for" (Set (Var "Amp")) "being" ($#m2_gcd_1 :::"AmpleSet"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "r1")) "," (Set (Var "r2")) ($#r8_gcd_1 :::"are_normalized_wrt"::: ) (Set (Var "Amp"))) & (Bool (Set (Var "s1")) "," (Set (Var "s2")) ($#r8_gcd_1 :::"are_normalized_wrt"::: ) (Set (Var "Amp")))) "holds" (Bool (Set (Set "(" ($#k8_gcd_1 :::"mult1"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "r2")) ($#k8_group_1 :::"*"::: ) (Set (Var "s2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_gcd_1 :::"mult2"::: ) "(" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "Amp")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "r1")) ($#k8_group_1 :::"*"::: ) (Set (Var "s1")) ")" )))))) ; theorem :: GCD_1:48 (Bool "for" (Set (Var "F")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ))) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ))) ")" ))) ; theorem :: GCD_1:49 (Bool "for" (Set (Var "F")) "being" ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v5_group_1 :::"commutative"::: ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F")))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k11_algstr_0 :::"""::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k11_algstr_0 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b")) ($#k8_group_1 :::"*"::: ) (Set (Var "a")) ")" ) ($#k11_algstr_0 :::"""::: ) )))) ;