:: FINSOP_1 semantic presentation begin definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); let "g" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); assume (Bool "(" (Bool (Set (Const "g")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) "or" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Const "F"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) ")" ) ; func "g" :::""**""::: "F" -> ($#m1_subset_1 :::"Element"::: ) "of" "D" means :: FINSOP_1:def 1 (Bool it ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) "g")) if (Bool "(" (Bool "g" "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) "F") ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) otherwise (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," "D" "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) "F"))) "holds" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set "g" ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" "F" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )) ")" ) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "F" ")" ))) ")" )); end; :: deftheorem defines :::""**""::: FINSOP_1:def 1 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool "(" (Bool (Set (Var "g")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) "or" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) ")" )) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "g")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "F")))) "iff" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "g")))) ")" ) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "g")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) "or" "not" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "F")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "D")) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )) ")" ) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")) ")" ))) ")" )) ")" ) ")" ")" ))))); theorem :: FINSOP_1:1 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "D")) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )) ")" ) & (Bool (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")) ")" ))) ")" ))))) ; theorem :: FINSOP_1:2 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "D")) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )) ")" ) & (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")) ")" ))) ")" ))) "holds" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "F")))))))) ; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Const "A")); let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "A")); :: original: :::"+*"::: redefine func "F" :::"+*"::: "p" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," "A"; end; notationlet "f" be ($#m1_hidden :::"FinSequence":::); synonym :::"findom"::: "f" for :::"dom"::: "f"; end; definitionlet "f" be ($#m1_hidden :::"FinSequence":::); :: original: :::"findom"::: redefine func :::"findom"::: "f" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set ($#k5_numbers :::"NAT"::: ) )); end; theorem :: FINSOP_1:3 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool "(" (Bool (Set (Var "g")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) "or" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) ")" ) & (Bool (Set (Var "g")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "g")) "is" ($#v1_binop_1 :::"commutative"::: ) )) "holds" (Bool (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k7_setwiseo :::"$$"::: ) "(" (Set "(" ($#k3_finsop_1 :::"findom"::: ) (Set (Var "F")) ")" ) "," (Set "(" (Set "(" (Set ($#k5_numbers :::"NAT"::: ) ) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "g")) ")" ) ")" ) ($#k2_finsop_1 :::"+*"::: ) (Set (Var "F")) ")" ) ")" ))))) ; theorem :: FINSOP_1:4 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool "(" (Bool (Set (Var "g")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) "or" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) ")" )) "holds" (Bool (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set (Var "F")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d")) ($#k12_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "F")) ")" ) "," (Set (Var "d")) ")" )))))) ; theorem :: FINSOP_1:5 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "g")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool "(" (Bool (Set (Var "g")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) "or" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) ")" ) ")" )) "holds" (Bool (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set (Var "F")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "F")) ")" ) "," (Set "(" (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "G")) ")" ) ")" ))))) ; theorem :: FINSOP_1:6 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "g")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool "(" (Bool (Set (Var "g")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) "or" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) ")" )) "holds" (Bool (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set "(" (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "F")) ")" ) ")" )))))) ; theorem :: FINSOP_1:7 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")) ")" ) "st" (Bool (Bool (Set (Var "g")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "g")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool "(" (Bool (Set (Var "g")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) "or" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) ")" ) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_relat_1 :::"*"::: ) (Set (Var "P"))))) "holds" (Bool (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "G")))))))) ; theorem :: FINSOP_1:8 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool "(" (Bool (Set (Var "g")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) "or" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) ")" ) & (Bool (Set (Var "g")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "g")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "G")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "G"))))))) ; theorem :: FINSOP_1:9 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "g")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "g")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool "(" (Bool (Set (Var "g")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) "or" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) ")" ) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) "," (Set "(" (Set (Var "H")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) ")" )) ")" )) "holds" (Bool (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "G")) ")" ) "," (Set "(" (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "H")) ")" ) ")" ))))) ; theorem :: FINSOP_1:10 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "g")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) )) "holds" (Bool (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set (Var "D")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "g")))))) ; theorem :: FINSOP_1:11 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "d")))))) ; theorem :: FINSOP_1:12 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "d1")) "," (Set (Var "d2")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ))))) ; theorem :: FINSOP_1:13 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "g")) "is" ($#v1_binop_1 :::"commutative"::: ) )) "holds" (Bool (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "d1")) "," (Set (Var "d2")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "d2")) "," (Set (Var "d1")) ($#k2_finseq_4 :::"*>"::: ) )))))) ; theorem :: FINSOP_1:14 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "," (Set (Var "d3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "d1")) "," (Set (Var "d2")) "," (Set (Var "d3")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "g")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ")" ) "," (Set (Var "d3")) ")" ))))) ; theorem :: FINSOP_1:15 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "," (Set (Var "d3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "g")) "is" ($#v1_binop_1 :::"commutative"::: ) )) "holds" (Bool (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "d1")) "," (Set (Var "d2")) "," (Set (Var "d3")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "d2")) "," (Set (Var "d1")) "," (Set (Var "d3")) ($#k3_finseq_4 :::"*>"::: ) )))))) ; theorem :: FINSOP_1:16 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Num 1) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "d")))))) ; theorem :: FINSOP_1:17 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Num 2) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set (Var "d")) ")" ))))) ; theorem :: FINSOP_1:18 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "k")) "," (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "g")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool "(" (Bool (Set (Var "g")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) "or" (Bool "(" (Bool (Set (Var "k")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "l")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) "holds" (Bool (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Set (Var "l")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set (Var "k")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d")) ")" ) ")" ) "," (Set "(" (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set (Var "l")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d")) ")" ) ")" ) ")" )))))) ; theorem :: FINSOP_1:19 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "k")) "," (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "g")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool "(" (Bool (Set (Var "g")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) "or" (Bool "(" (Bool (Set (Var "k")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "l")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) "holds" (Bool (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set "(" (Set (Var "k")) ($#k4_nat_1 :::"*"::: ) (Set (Var "l")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set (Var "l")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set "(" (Set (Var "k")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d")) ")" ) ")" ) ")" ))))))) ; theorem :: FINSOP_1:20 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Num 1)))))) ; theorem :: FINSOP_1:21 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Num 2))) "holds" (Bool (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Num 2) ")" ) ")" ))))) ;