:: GROUP_9 semantic presentation begin definitionlet "O", "E" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_subset_1 :::"Action":::) "of" (Set (Const "O")) "," (Set (Const "E")); let "IT" be ($#m1_hidden :::"set"::: ) ; pred "IT" :::"is_stable_under_the_action_of"::: "A" means :: GROUP_9:def 1 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "O" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" "E" "," "E" "st" (Bool (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) "O") & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set "A" ($#k1_funct_1 :::"."::: ) (Set (Var "o"))))) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) "IT") ($#r1_tarski :::"c="::: ) "IT"))); end; :: deftheorem defines :::"is_stable_under_the_action_of"::: GROUP_9:def 1 : (Bool "for" (Set (Var "O")) "," (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Action":::) "of" (Set (Var "O")) "," (Set (Var "E")) (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) ($#r1_group_9 :::"is_stable_under_the_action_of"::: ) (Set (Var "A"))) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "O")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "E")) "," (Set (Var "E")) "st" (Bool (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "O"))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "o"))))) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "IT"))) ($#r1_tarski :::"c="::: ) (Set (Var "IT"))))) ")" )))); definitionlet "O", "E" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_subset_1 :::"Action":::) "of" (Set (Const "O")) "," (Set (Const "E")); let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "E")); func :::"the_stable_subset_generated_by"::: "(" "X" "," "A" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "E" means :: GROUP_9:def 2 (Bool "(" (Bool "X" ($#r1_tarski :::"c="::: ) it) & (Bool it ($#r1_group_9 :::"is_stable_under_the_action_of"::: ) "A") & (Bool "(" "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" "E" "st" (Bool (Bool (Set (Var "Y")) ($#r1_group_9 :::"is_stable_under_the_action_of"::: ) "A") & (Bool "X" ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool it ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" ) ")" ); end; :: deftheorem defines :::"the_stable_subset_generated_by"::: GROUP_9:def 2 : (Bool "for" (Set (Var "O")) "," (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Action":::) "of" (Set (Var "O")) "," (Set (Var "E")) (Bool "for" (Set (Var "X")) "," (Set (Var "b5")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k1_group_9 :::"the_stable_subset_generated_by"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" )) "iff" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "b5"))) & (Bool (Set (Var "b5")) ($#r1_group_9 :::"is_stable_under_the_action_of"::: ) (Set (Var "A"))) & (Bool "(" "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_group_9 :::"is_stable_under_the_action_of"::: ) (Set (Var "A"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "b5")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" ) ")" ) ")" )))); definitionlet "O", "E" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_subset_1 :::"Action":::) "of" (Set (Const "O")) "," (Set (Const "E")); let "F" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "O")); func :::"Product"::: "(" "F" "," "A" ")" -> ($#m1_subset_1 :::"Function":::) "of" "E" "," "E" means :: GROUP_9:def 3 (Bool it ($#r2_funct_2 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) "E")) if (Bool (Set ($#k3_finseq_1 :::"len"::: ) "F") ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) otherwise (Bool "ex" (Set (Var "PF")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_funct_2 :::"Funcs"::: ) "(" "E" "," "E" ")" ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "PF")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "F" ")" ))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "PF"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "F")) & (Bool (Set (Set (Var "PF")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set "A" ($#k1_funct_1 :::"."::: ) (Set "(" "F" ($#k1_funct_1 :::"."::: ) (Num 1) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) "F"))) "holds" (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" "E" "," "E" "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "PF")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set "A" ($#k1_funct_1 :::"."::: ) (Set "(" "F" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) & (Bool (Set (Set (Var "PF")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set (Var "g")))) ")" )) ")" ) ")" )); end; :: deftheorem defines :::"Product"::: GROUP_9:def 3 : (Bool "for" (Set (Var "O")) "," (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Action":::) "of" (Set (Var "O")) "," (Set (Var "E")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "O")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "E")) "," (Set (Var "E")) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k2_group_9 :::"Product"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" )) "iff" (Bool (Set (Var "b5")) ($#r2_funct_2 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "E")))) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) "implies" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k2_group_9 :::"Product"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" )) "iff" (Bool "ex" (Set (Var "PF")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "E")) "," (Set (Var "E")) ")" ) "st" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "PF")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")) ")" ))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "PF"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "PF")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))))) "holds" (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "E")) "," (Set (Var "E")) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "PF")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) & (Bool (Set (Set (Var "PF")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set (Var "g")))) ")" )) ")" ) ")" )) ")" ) ")" ")" ))))); definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l3_algstr_0 :::"Group":::); let "IT" be ($#m1_subset_1 :::"Action":::) "of" (Set (Const "O")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "G"))); attr "IT" is :::"distributive"::: means :: GROUP_9:def 4 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "O" "st" (Bool (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) "O")) "holds" (Bool (Set "IT" ($#k1_funct_1 :::"."::: ) (Set (Var "o"))) "is" ($#m1_subset_1 :::"Homomorphism":::) "of" "G" "," "G")); end; :: deftheorem defines :::"distributive"::: GROUP_9:def 4 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Action":::) "of" (Set (Var "O")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_group_9 :::"distributive"::: ) ) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "O")) "st" (Bool (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "O")))) "holds" (Bool (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set (Var "o"))) "is" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "G")))) ")" )))); definitionlet "O" be ($#m1_hidden :::"set"::: ) ; attr "c2" is :::"strict"::: ; struct :::"HGrWOpStr"::: "over" "O" -> ($#l3_algstr_0 :::"multMagma"::: ) ; aggr :::"HGrWOpStr":::(# :::"carrier":::, :::"multF":::, :::"action"::: #) -> ($#l1_group_9 :::"HGrWOpStr"::: ) "over" "O"; sel :::"action"::: "c2" -> ($#m1_subset_1 :::"Action":::) "of" "O" "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c2"); end; registrationlet "O" be ($#m1_hidden :::"set"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#l1_group_9 :::"HGrWOpStr"::: ) "over" "O"; end; definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_group_9 :::"HGrWOpStr"::: ) "over" (Set (Const "O")); attr "IT" is :::"distributive"::: means :: GROUP_9:def 5 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Action":::) "of" "O" "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "a")) ($#r1_funct_2 :::"="::: ) (Set "the" ($#u1_group_9 :::"action"::: ) "of" "IT")) & (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT") "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "IT") "#)" ))) "holds" (Bool (Set (Var "a")) "is" ($#v1_group_9 :::"distributive"::: ) ))); end; :: deftheorem defines :::"distributive"::: GROUP_9:def 5 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_group_9 :::"HGrWOpStr"::: ) "over" (Set (Var "O")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_group_9 :::"distributive"::: ) ) "iff" (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Action":::) "of" (Set (Var "O")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "a")) ($#r1_funct_2 :::"="::: ) (Set "the" ($#u1_group_9 :::"action"::: ) "of" (Set (Var "IT")))) & (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IT"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "IT"))) "#)" ))) "holds" (Bool (Set (Var "a")) "is" ($#v1_group_9 :::"distributive"::: ) ))) ")" ))); registrationlet "O" be ($#m1_hidden :::"set"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v2_group_9 :::"strict"::: ) ($#v3_group_9 :::"distributive"::: ) for ($#l1_group_9 :::"HGrWOpStr"::: ) "over" "O"; end; definitionlet "O" be ($#m1_hidden :::"set"::: ) ; mode GroupWithOperators of "O" is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v3_group_9 :::"distributive"::: ) ($#l1_group_9 :::"HGrWOpStr"::: ) "over" "O"; end; definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); let "o" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "O")); func "G" :::"^"::: "o" -> ($#m1_subset_1 :::"Homomorphism":::) "of" "G" "," "G" equals :: GROUP_9:def 6 (Set (Set "the" ($#u1_group_9 :::"action"::: ) "of" "G") ($#k1_funct_1 :::"."::: ) "o") if (Bool "o" ($#r2_hidden :::"in"::: ) "O") otherwise (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G")); end; :: deftheorem defines :::"^"::: GROUP_9:def 6 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "O")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "O")))) "implies" (Bool (Set (Set (Var "G")) ($#k3_group_9 :::"^"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_group_9 :::"action"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set (Var "o")))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "O"))))) "implies" (Bool (Set (Set (Var "G")) ($#k3_group_9 :::"^"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))))) ")" ")" )))); definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); mode :::"StableSubgroup"::: "of" "G" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v3_group_9 :::"distributive"::: ) ($#l1_group_9 :::"HGrWOpStr"::: ) "over" "O" means :: GROUP_9:def 7 (Bool "(" (Bool it "is" ($#m1_group_2 :::"Subgroup"::: ) "of" "G") & (Bool "(" "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "O" "holds" (Bool (Set it ($#k3_group_9 :::"^"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "G" ($#k3_group_9 :::"^"::: ) (Set (Var "o")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it))) ")" ) ")" ); end; :: deftheorem defines :::"StableSubgroup"::: GROUP_9:def 7 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "b3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v3_group_9 :::"distributive"::: ) ($#l1_group_9 :::"HGrWOpStr"::: ) "over" (Set (Var "O")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G"))) "iff" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G"))) & (Bool "(" "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "O")) "holds" (Bool (Set (Set (Var "b3")) ($#k3_group_9 :::"^"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k3_group_9 :::"^"::: ) (Set (Var "o")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))))) ")" ) ")" ) ")" )))); registrationlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v2_group_9 :::"strict"::: ) ($#v3_group_9 :::"distributive"::: ) for ($#m1_group_9 :::"StableSubgroup"::: ) "of" "G"; end; definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); func :::"(1)."::: "G" -> ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" "G" means :: GROUP_9:def 8 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) "G" ")" ) ($#k1_tarski :::"}"::: ) )); end; :: deftheorem defines :::"(1)."::: GROUP_9:def 8 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "b3")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_group_9 :::"(1)."::: ) (Set (Var "G")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" ) ($#k1_tarski :::"}"::: ) )) ")" )))); definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); func :::"(Omega)."::: "G" -> ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" "G" equals :: GROUP_9:def 9 (Set ($#g1_group_9 :::"HGrWOpStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "G") "," (Set "the" ($#u1_group_9 :::"action"::: ) "of" "G") "#)" ); end; :: deftheorem defines :::"(Omega)."::: GROUP_9:def 9 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) "holds" (Bool (Set ($#k5_group_9 :::"(Omega)."::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#g1_group_9 :::"HGrWOpStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u1_group_9 :::"action"::: ) "of" (Set (Var "G"))) "#)" )))); definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); let "IT" be ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Const "G")); attr "IT" is :::"normal"::: means :: GROUP_9:def 10 (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G" "st" (Bool (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT") "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "IT") "#)" ))) "holds" (Bool (Set (Var "H")) "is" ($#v1_group_3 :::"normal"::: ) )); end; :: deftheorem defines :::"normal"::: GROUP_9:def 10 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "IT")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_group_9 :::"normal"::: ) ) "iff" (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IT"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "IT"))) "#)" ))) "holds" (Bool (Set (Var "H")) "is" ($#v1_group_3 :::"normal"::: ) )) ")" )))); registrationlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v2_group_9 :::"strict"::: ) ($#v3_group_9 :::"distributive"::: ) ($#v4_group_9 :::"normal"::: ) for ($#m1_group_9 :::"StableSubgroup"::: ) "of" "G"; end; registrationlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); let "H" be ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Const "G")); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v3_group_9 :::"distributive"::: ) ($#v4_group_9 :::"normal"::: ) for ($#m1_group_9 :::"StableSubgroup"::: ) "of" "H"; end; registrationlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); cluster (Set ($#k4_group_9 :::"(1)."::: ) "G") -> ($#v2_group_9 :::"strict"::: ) ($#v4_group_9 :::"normal"::: ) ; cluster (Set ($#k5_group_9 :::"(Omega)."::: ) "G") -> ($#v2_group_9 :::"strict"::: ) ($#v4_group_9 :::"normal"::: ) ; end; definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); func :::"the_stable_subgroups_of"::: "G" -> ($#m1_hidden :::"set"::: ) means :: GROUP_9:def 11 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) "is" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" "G") ")" )); end; :: deftheorem defines :::"the_stable_subgroups_of"::: GROUP_9:def 11 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_group_9 :::"the_stable_subgroups_of"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool (Set (Var "x")) "is" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G"))) ")" )) ")" )))); registrationlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); cluster (Set ($#k6_group_9 :::"the_stable_subgroups_of"::: ) "G") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "IT" be ($#l3_algstr_0 :::"Group":::); attr "IT" is :::"simple"::: means :: GROUP_9:def 12 (Bool "(" (Bool (Bool "not" "IT" "is" ($#v7_struct_0 :::"trivial"::: ) )) & (Bool "(" "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "IT" "holds" (Bool "(" "not" (Bool (Set (Var "H")) ($#r1_hidden :::"<>"::: ) (Set ($#k7_group_2 :::"(Omega)."::: ) "IT")) "or" "not" (Bool (Set (Var "H")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_group_2 :::"(1)."::: ) "IT")) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"simple"::: GROUP_9:def 12 : (Bool "for" (Set (Var "IT")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_group_9 :::"simple"::: ) ) "iff" (Bool "(" (Bool (Bool "not" (Set (Var "IT")) "is" ($#v7_struct_0 :::"trivial"::: ) )) & (Bool "(" "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "IT")) "holds" (Bool "(" "not" (Bool (Set (Var "H")) ($#r1_hidden :::"<>"::: ) (Set ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "IT")))) "or" "not" (Bool (Set (Var "H")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "IT")))) ")" ) ")" ) ")" ) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_9 :::"simple"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; end; definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "IT" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); attr "IT" is :::"simple"::: means :: GROUP_9:def 13 (Bool "(" (Bool (Bool "not" "IT" "is" ($#v7_struct_0 :::"trivial"::: ) )) & (Bool "(" "for" (Set (Var "H")) "being" ($#v2_group_9 :::"strict"::: ) ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" "IT" "holds" (Bool "(" "not" (Bool (Set (Var "H")) ($#r1_hidden :::"<>"::: ) (Set ($#k5_group_9 :::"(Omega)."::: ) "IT")) "or" "not" (Bool (Set (Var "H")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_group_9 :::"(1)."::: ) "IT")) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"simple"::: GROUP_9:def 13 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "IT")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_group_9 :::"simple"::: ) ) "iff" (Bool "(" (Bool (Bool "not" (Set (Var "IT")) "is" ($#v7_struct_0 :::"trivial"::: ) )) & (Bool "(" "for" (Set (Var "H")) "being" ($#v2_group_9 :::"strict"::: ) ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "IT")) "holds" (Bool "(" "not" (Bool (Set (Var "H")) ($#r1_hidden :::"<>"::: ) (Set ($#k5_group_9 :::"(Omega)."::: ) (Set (Var "IT")))) "or" "not" (Bool (Set (Var "H")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_group_9 :::"(1)."::: ) (Set (Var "IT")))) ")" ) ")" ) ")" ) ")" ))); registrationlet "O" be ($#m1_hidden :::"set"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v2_group_9 :::"strict"::: ) ($#v3_group_9 :::"distributive"::: ) ($#v6_group_9 :::"simple"::: ) for ($#l1_group_9 :::"HGrWOpStr"::: ) "over" "O"; end; definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); let "N" be ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Const "G")); func :::"Cosets"::: "N" -> ($#m1_hidden :::"set"::: ) means :: GROUP_9:def 14 (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G" "st" (Bool (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "N") "#)" ))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k15_group_2 :::"Cosets"::: ) (Set (Var "H"))))); end; :: deftheorem defines :::"Cosets"::: GROUP_9:def 14 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "N")) "being" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k7_group_9 :::"Cosets"::: ) (Set (Var "N")))) "iff" (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "N"))) "#)" ))) "holds" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k15_group_2 :::"Cosets"::: ) (Set (Var "H"))))) ")" ))))); definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); let "N" be ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Const "G")); func :::"CosOp"::: "N" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k7_group_9 :::"Cosets"::: ) "N" ")" ) means :: GROUP_9:def 15 (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G" "st" (Bool (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "N") "#)" ))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k4_group_6 :::"CosOp"::: ) (Set (Var "H"))))); end; :: deftheorem defines :::"CosOp"::: GROUP_9:def 15 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "N")) "being" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k7_group_9 :::"Cosets"::: ) (Set (Var "N")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k8_group_9 :::"CosOp"::: ) (Set (Var "N")))) "iff" (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "N"))) "#)" ))) "holds" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_group_6 :::"CosOp"::: ) (Set (Var "H"))))) ")" ))))); definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); let "N" be ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Const "G")); func :::"CosAc"::: "N" -> ($#m1_subset_1 :::"Action":::) "of" "O" "," (Set "(" ($#k7_group_9 :::"Cosets"::: ) "N" ")" ) means :: GROUP_9:def 16 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "O" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k4_tarski :::"]"::: ) ) where A, B "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_group_9 :::"Cosets"::: ) "N") : (Bool "ex" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" "G" "st" (Bool "(" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "(" "G" ($#k3_group_9 :::"^"::: ) (Set (Var "o")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "g")))) ")" )) "}" )) if (Bool (Bool "not" "O" "is" ($#v1_xboole_0 :::"empty"::: ) )) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k7_group_9 :::"Cosets"::: ) "N" ")" ) ")" ) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); end; :: deftheorem defines :::"CosAc"::: GROUP_9:def 16 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "N")) "being" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Action":::) "of" (Set (Var "O")) "," (Set "(" ($#k7_group_9 :::"Cosets"::: ) (Set (Var "N")) ")" ) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "O")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k9_group_9 :::"CosAc"::: ) (Set (Var "N")))) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "O")) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k4_tarski :::"]"::: ) ) where A, B "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_group_9 :::"Cosets"::: ) (Set (Var "N"))) : (Bool "ex" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k3_group_9 :::"^"::: ) (Set (Var "o")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "g")))) ")" )) "}" )) ")" ) ")" & "(" (Bool (Bool (Set (Var "O")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k9_group_9 :::"CosAc"::: ) (Set (Var "N")))) "iff" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k7_group_9 :::"Cosets"::: ) (Set (Var "N")) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" ) ")" ")" ))))); definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); let "N" be ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Const "G")); func "G" :::"./."::: "N" -> ($#l1_group_9 :::"HGrWOpStr"::: ) "over" "O" equals :: GROUP_9:def 17 (Set ($#g1_group_9 :::"HGrWOpStr"::: ) "(#" (Set "(" ($#k7_group_9 :::"Cosets"::: ) "N" ")" ) "," (Set "(" ($#k8_group_9 :::"CosOp"::: ) "N" ")" ) "," (Set "(" ($#k9_group_9 :::"CosAc"::: ) "N" ")" ) "#)" ); end; :: deftheorem defines :::"./."::: GROUP_9:def 17 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "N")) "being" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "G")) ($#k10_group_9 :::"./."::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set ($#g1_group_9 :::"HGrWOpStr"::: ) "(#" (Set "(" ($#k7_group_9 :::"Cosets"::: ) (Set (Var "N")) ")" ) "," (Set "(" ($#k8_group_9 :::"CosOp"::: ) (Set (Var "N")) ")" ) "," (Set "(" ($#k9_group_9 :::"CosAc"::: ) (Set (Var "N")) ")" ) "#)" ))))); registrationlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); let "N" be ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Const "G")); cluster (Set "G" ($#k10_group_9 :::"./."::: ) "N") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; cluster (Set "G" ($#k10_group_9 :::"./."::: ) "N") -> ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v3_group_9 :::"distributive"::: ) ; end; definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G", "H" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "G")) "," (Set (Const "H")); attr "f" is :::"homomorphic"::: means :: GROUP_9:def 18 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "O" (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" "G" "holds" (Bool (Set "f" ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" "G" ($#k3_group_9 :::"^"::: ) (Set (Var "o")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "H" ($#k3_group_9 :::"^"::: ) (Set (Var "o")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "g")) ")" ))))); end; :: deftheorem defines :::"homomorphic"::: GROUP_9:def 18 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v7_group_9 :::"homomorphic"::: ) ) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "O")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" (Set (Var "G")) ($#k3_group_9 :::"^"::: ) (Set (Var "o")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "H")) ($#k3_group_9 :::"^"::: ) (Set (Var "o")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "g")) ")" ))))) ")" )))); registrationlet "O" be ($#m1_hidden :::"set"::: ) ; let "G", "H" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "H") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_partfun1 :::"total"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v1_group_6 :::"multiplicative"::: ) ($#v7_group_9 :::"homomorphic"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "H") ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G", "H" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); mode Homomorphism of "G" "," "H" is ($#v1_group_6 :::"multiplicative"::: ) ($#v7_group_9 :::"homomorphic"::: ) ($#m1_subset_1 :::"Function":::) "of" "G" "," "H"; end; definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G", "H", "I" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); let "h" be ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Const "G")) "," (Set (Const "H")); let "h1" be ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Const "H")) "," (Set (Const "I")); :: original: :::"*"::: redefine func "h1" :::"*"::: "h" -> ($#m1_subset_1 :::"Homomorphism":::) "of" "G" "," "I"; end; definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G", "H" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); pred "G" "," "H" :::"are_isomorphic"::: means :: GROUP_9:def 19 (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" "G" "," "H" "st" (Bool (Set (Var "h")) "is" ($#v3_funct_2 :::"bijective"::: ) )); reflexivity (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")) (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "G")) "st" (Bool (Set (Var "h")) "is" ($#v3_funct_2 :::"bijective"::: ) ))) ; end; :: deftheorem defines :::"are_isomorphic"::: GROUP_9:def 19 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) "holds" (Bool "(" (Bool (Set (Var "G")) "," (Set (Var "H")) ($#r2_group_9 :::"are_isomorphic"::: ) ) "iff" (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "st" (Bool (Set (Var "h")) "is" ($#v3_funct_2 :::"bijective"::: ) )) ")" ))); definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G", "H" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); :: original: :::"are_isomorphic"::: redefine pred "G" "," "H" :::"are_isomorphic"::: ; symmetry (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")) "st" (Bool (Bool ((Set (Const "O")) "," (Set (Var "b1")) "," (Set (Var "b2"))))) "holds" (Bool ((Set (Const "O")) "," (Set (Var "b2")) "," (Set (Var "b1"))))) ; end; definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); let "N" be ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Const "G")); func :::"nat_hom"::: "N" -> ($#m1_subset_1 :::"Homomorphism":::) "of" "G" "," (Set "(" "G" ($#k10_group_9 :::"./."::: ) "N" ")" ) means :: GROUP_9:def 20 (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G" "st" (Bool (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "N") "#)" ))) "holds" (Bool it ($#r1_funct_2 :::"="::: ) (Set ($#k8_group_6 :::"nat_hom"::: ) (Set (Var "H"))))); end; :: deftheorem defines :::"nat_hom"::: GROUP_9:def 20 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "N")) "being" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set "(" (Set (Var "G")) ($#k10_group_9 :::"./."::: ) (Set (Var "N")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k12_group_9 :::"nat_hom"::: ) (Set (Var "N")))) "iff" (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "N"))) "#)" ))) "holds" (Bool (Set (Var "b4")) ($#r1_funct_2 :::"="::: ) (Set ($#k8_group_6 :::"nat_hom"::: ) (Set (Var "H"))))) ")" ))))); definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G", "H" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); let "g" be ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Const "G")) "," (Set (Const "H")); func :::"Ker"::: "g" -> ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" "G" means :: GROUP_9:def 21 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) "{" (Set (Var "a")) where a "is" ($#m1_subset_1 :::"Element":::) "of" "G" : (Bool (Set "g" ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) "H")) "}" ); end; :: deftheorem defines :::"Ker"::: GROUP_9:def 21 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) (Bool "for" (Set (Var "b5")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k13_group_9 :::"Ker"::: ) (Set (Var "g")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b5"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "a")) where a "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) : (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "H")))) "}" ) ")" ))))); registrationlet "O" be ($#m1_hidden :::"set"::: ) ; let "G", "H" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); let "g" be ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Const "G")) "," (Set (Const "H")); cluster (Set ($#k13_group_9 :::"Ker"::: ) "g") -> ($#v2_group_9 :::"strict"::: ) ($#v4_group_9 :::"normal"::: ) ; end; definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G", "H" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); let "g" be ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Const "G")) "," (Set (Const "H")); func :::"Image"::: "g" -> ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" "H" means :: GROUP_9:def 22 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "g" ($#k7_relset_1 :::".:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G"))); end; :: deftheorem defines :::"Image"::: GROUP_9:def 22 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) (Bool "for" (Set (Var "b5")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k14_group_9 :::"Image"::: ) (Set (Var "g")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k7_relset_1 :::".:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))))) ")" ))))); definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); let "H" be ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Const "G")); func :::"carr"::: "H" -> ($#m1_subset_1 :::"Subset":::) "of" "G" equals :: GROUP_9:def 23 (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "H"); end; :: deftheorem defines :::"carr"::: GROUP_9:def 23 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k15_group_9 :::"carr"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))))))); definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); let "H1", "H2" be ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Const "G")); func "H1" :::"*"::: "H2" -> ($#m1_subset_1 :::"Subset":::) "of" "G" equals :: GROUP_9:def 24 (Set (Set "(" ($#k15_group_9 :::"carr"::: ) "H1" ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" ($#k15_group_9 :::"carr"::: ) "H2" ")" )); end; :: deftheorem defines :::"*"::: GROUP_9:def 24 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "H1")) ($#k16_group_9 :::"*"::: ) (Set (Var "H2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_group_9 :::"carr"::: ) (Set (Var "H1")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" ($#k15_group_9 :::"carr"::: ) (Set (Var "H2")) ")" )))))); definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); let "H1", "H2" be ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Const "G")); func "H1" :::"/\"::: "H2" -> ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" "G" means :: GROUP_9:def 25 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_group_9 :::"carr"::: ) "H1" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_group_9 :::"carr"::: ) "H2" ")" ))); commutativity (Bool "for" (Set (Var "b1")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Const "G")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Const "G")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_group_9 :::"carr"::: ) (Set (Var "H1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_group_9 :::"carr"::: ) (Set (Var "H2")) ")" )))) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_group_9 :::"carr"::: ) (Set (Var "H2")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_group_9 :::"carr"::: ) (Set (Var "H1")) ")" ))))) ; end; :: deftheorem defines :::"/\"::: GROUP_9:def 25 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "b5")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k17_group_9 :::"/\"::: ) (Set (Var "H2")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_group_9 :::"carr"::: ) (Set (Var "H1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_group_9 :::"carr"::: ) (Set (Var "H2")) ")" ))) ")" ))))); definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")); func :::"the_stable_subgroup_of"::: "A" -> ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" "G" means :: GROUP_9:def 26 (Bool "(" (Bool "A" ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it)) & (Bool "(" "for" (Set (Var "H")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" "G" "st" (Bool (Bool "A" ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))))) "holds" (Bool it "is" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H"))) ")" ) ")" ); end; :: deftheorem defines :::"the_stable_subgroup_of"::: GROUP_9:def 26 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "b4")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k18_group_9 :::"the_stable_subgroup_of"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4")))) & (Bool "(" "for" (Set (Var "H")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))))) "holds" (Bool (Set (Var "b4")) "is" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H"))) ")" ) ")" ) ")" ))))); definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); let "H1", "H2" be ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Const "G")); func "H1" :::""\/""::: "H2" -> ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" "G" equals :: GROUP_9:def 27 (Set ($#k18_group_9 :::"the_stable_subgroup_of"::: ) (Set "(" (Set "(" ($#k15_group_9 :::"carr"::: ) "H1" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k15_group_9 :::"carr"::: ) "H2" ")" ) ")" )); end; :: deftheorem defines :::""\/""::: GROUP_9:def 27 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "H1")) ($#k19_group_9 :::""\/""::: ) (Set (Var "H2"))) ($#r1_hidden :::"="::: ) (Set ($#k18_group_9 :::"the_stable_subgroup_of"::: ) (Set "(" (Set "(" ($#k15_group_9 :::"carr"::: ) (Set (Var "H1")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k15_group_9 :::"carr"::: ) (Set (Var "H2")) ")" ) ")" )))))); begin theorem :: GROUP_9:1 (Bool "for" (Set (Var "O")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H1")))) "holds" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "G")))))) ; theorem :: GROUP_9:2 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "h1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H1")) "holds" (Bool (Set (Var "h1")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))))))) ; theorem :: GROUP_9:3 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "h1")) "," (Set (Var "h2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H1")) "st" (Bool (Bool (Set (Var "h1")) ($#r1_hidden :::"="::: ) (Set (Var "g1"))) & (Bool (Set (Var "h2")) ($#r1_hidden :::"="::: ) (Set (Var "g2")))) "holds" (Bool (Set (Set (Var "h1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g2"))))))))) ; theorem :: GROUP_9:4 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "H1"))))))) ; theorem :: GROUP_9:5 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "H1")))))) ; theorem :: GROUP_9:6 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "g1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "h1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H1")) "st" (Bool (Bool (Set (Var "h1")) ($#r1_hidden :::"="::: ) (Set (Var "g1")))) "holds" (Bool (Set (Set (Var "h1")) ($#k2_group_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "g1")) ($#k2_group_1 :::"""::: ) ))))))) ; theorem :: GROUP_9:7 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "g1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H1"))) & (Bool (Set (Var "g2")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H1")))) "holds" (Bool (Set (Set (Var "g1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g2"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "H1"))))))) ; theorem :: GROUP_9:8 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "g1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "g1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H1")))) "holds" (Bool (Set (Set (Var "g1")) ($#k2_group_1 :::"""::: ) ) ($#r1_struct_0 :::"in"::: ) (Set (Var "H1"))))))) ; theorem :: GROUP_9:9 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "g1")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "g2")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "g1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g2"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) & (Bool "(" "for" (Set (Var "g1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "g1")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "g1")) ($#k2_group_1 :::"""::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) & (Bool "(" "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "O")) (Bool "for" (Set (Var "g1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "g1")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k3_group_9 :::"^"::: ) (Set (Var "o")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "g1"))) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) ")" )) "holds" (Bool "ex" (Set (Var "H")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))))))) ; theorem :: GROUP_9:10 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) "holds" (Bool (Set (Var "G")) "is" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G"))))) ; theorem :: GROUP_9:11 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) "st" (Bool (Bool (Set (Var "G1")) "is" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G2"))) & (Bool (Set (Var "G2")) "is" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G3")))) "holds" (Bool (Set (Var "G1")) "is" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G3"))))) ; theorem :: GROUP_9:12 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2"))))) "holds" (Bool (Set (Var "H1")) "is" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H2")))))) ; theorem :: GROUP_9:13 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "g")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H1")))) "holds" (Bool (Set (Var "g")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H2"))) ")" )) "holds" (Bool (Set (Var "H1")) "is" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H2")))))) ; theorem :: GROUP_9:14 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2"))))) "holds" (Bool (Set (Var "H1")) ($#r1_hidden :::"="::: ) (Set (Var "H2")))))) ; theorem :: GROUP_9:15 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k4_group_9 :::"(1)."::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k4_group_9 :::"(1)."::: ) (Set (Var "H1"))))))) ; theorem :: GROUP_9:16 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k4_group_9 :::"(1)."::: ) (Set (Var "G"))) "is" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H1")))))) ; theorem :: GROUP_9:17 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set "(" ($#k15_group_9 :::"carr"::: ) (Set (Var "H1")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" ($#k15_group_9 :::"carr"::: ) (Set (Var "H2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_group_9 :::"carr"::: ) (Set (Var "H2")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" ($#k15_group_9 :::"carr"::: ) (Set (Var "H1")) ")" )))) "holds" (Bool "ex" (Set (Var "H")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_group_9 :::"carr"::: ) (Set (Var "H1")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" ($#k15_group_9 :::"carr"::: ) (Set (Var "H2")) ")" ))))))) ; theorem :: GROUP_9:18 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool "(" "for" (Set (Var "H")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k17_group_9 :::"/\"::: ) (Set (Var "H2"))))) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2"))))) ")" ) & (Bool "(" "for" (Set (Var "H")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2")))))) "holds" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k17_group_9 :::"/\"::: ) (Set (Var "H2")))) ")" ) ")" )))) ; theorem :: GROUP_9:19 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "H")) ($#k17_group_9 :::"/\"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Var "H")))))) ; theorem :: GROUP_9:20 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "," (Set (Var "H3")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "H1")) ($#k17_group_9 :::"/\"::: ) (Set (Var "H2")) ")" ) ($#k17_group_9 :::"/\"::: ) (Set (Var "H3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k17_group_9 :::"/\"::: ) (Set "(" (Set (Var "H2")) ($#k17_group_9 :::"/\"::: ) (Set (Var "H3")) ")" )))))) ; theorem :: GROUP_9:21 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_group_9 :::"(1)."::: ) (Set (Var "G")) ")" ) ($#k17_group_9 :::"/\"::: ) (Set (Var "H1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_group_9 :::"(1)."::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "H1")) ($#k17_group_9 :::"/\"::: ) (Set "(" ($#k4_group_9 :::"(1)."::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_group_9 :::"(1)."::: ) (Set (Var "G")))) ")" )))) ; theorem :: GROUP_9:22 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "N")) "being" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k7_group_9 :::"Cosets"::: ) (Set (Var "N")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))))))) ; theorem :: GROUP_9:23 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#v2_group_9 :::"strict"::: ) ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "ex" (Set (Var "N")) "being" ($#v2_group_9 :::"strict"::: ) ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_group_9 :::"carr"::: ) (Set (Var "N1")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" ($#k15_group_9 :::"carr"::: ) (Set (Var "N2")) ")" ))))))) ; theorem :: GROUP_9:24 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "g1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "g1")) ($#r1_struct_0 :::"in"::: ) (Set ($#k18_group_9 :::"the_stable_subgroup_of"::: ) (Set (Var "A")))) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))(Bool "ex" (Set (Var "I")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) )(Bool "ex" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set ($#k1_group_9 :::"the_stable_subset_generated_by"::: ) "(" (Set (Var "A")) "," (Set "the" ($#u1_group_9 :::"action"::: ) "of" (Set (Var "G"))) ")" )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "I")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "F")) ($#k4_group_4 :::"|^"::: ) (Set (Var "I")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "g1"))) ")" )))) ")" ))))) ; theorem :: GROUP_9:25 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k18_group_9 :::"the_stable_subgroup_of"::: ) (Set "(" ($#k15_group_9 :::"carr"::: ) (Set (Var "H")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "H")))))) ; theorem :: GROUP_9:26 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k18_group_9 :::"the_stable_subgroup_of"::: ) (Set (Var "A"))) "is" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set ($#k18_group_9 :::"the_stable_subgroup_of"::: ) (Set (Var "B"))))))) ; scheme :: GROUP_9:sch 1 MeetSbgWOpEx{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set F1 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "H")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set F2 "(" ")" ) : (Bool "ex" (Set (Var "K")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) & (Bool P1[(Set (Var "K"))]) ")" )) "}" ))) provided (Bool "ex" (Set (Var "H")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set F2 "(" ")" ) "st" (Bool P1[(Set (Var "H"))])) proof end; theorem :: GROUP_9:27 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k18_group_9 :::"the_stable_subgroup_of"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) : (Bool "ex" (Set (Var "H")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H")))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k15_group_9 :::"carr"::: ) (Set (Var "H")))) ")" )) "}" ))))) ; theorem :: GROUP_9:28 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#v2_group_9 :::"strict"::: ) ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "N1")) ($#k16_group_9 :::"*"::: ) (Set (Var "N2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N2")) ($#k16_group_9 :::"*"::: ) (Set (Var "N1"))))))) ; theorem :: GROUP_9:29 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "H1")) ($#k19_group_9 :::""\/""::: ) (Set (Var "H2"))) ($#r1_hidden :::"="::: ) (Set ($#k18_group_9 :::"the_stable_subgroup_of"::: ) (Set "(" (Set (Var "H1")) ($#k16_group_9 :::"*"::: ) (Set (Var "H2")) ")" )))))) ; theorem :: GROUP_9:30 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "H1")) ($#k16_group_9 :::"*"::: ) (Set (Var "H2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H2")) ($#k16_group_9 :::"*"::: ) (Set (Var "H1"))))) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "H1")) ($#k19_group_9 :::""\/""::: ) (Set (Var "H2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k16_group_9 :::"*"::: ) (Set (Var "H2"))))))) ; theorem :: GROUP_9:31 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#v2_group_9 :::"strict"::: ) ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "N1")) ($#k19_group_9 :::""\/""::: ) (Set (Var "N2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k16_group_9 :::"*"::: ) (Set (Var "N2"))))))) ; theorem :: GROUP_9:32 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#v2_group_9 :::"strict"::: ) ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "N1")) ($#k19_group_9 :::""\/""::: ) (Set (Var "N2"))) "is" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")))))) ; theorem :: GROUP_9:33 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_group_9 :::"(1)."::: ) (Set (Var "G")) ")" ) ($#k19_group_9 :::""\/""::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Var "H"))) & (Bool (Set (Set (Var "H")) ($#k19_group_9 :::""\/""::: ) (Set "(" ($#k4_group_9 :::"(1)."::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "H"))) ")" )))) ; theorem :: GROUP_9:34 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_group_9 :::"(Omega)."::: ) (Set (Var "G")) ")" ) ($#k19_group_9 :::""\/""::: ) (Set (Var "H1"))) ($#r1_hidden :::"="::: ) (Set ($#k5_group_9 :::"(Omega)."::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "H1")) ($#k19_group_9 :::""\/""::: ) (Set "(" ($#k5_group_9 :::"(Omega)."::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_group_9 :::"(Omega)."::: ) (Set (Var "G")))) ")" )))) ; theorem :: GROUP_9:35 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "H1")) "is" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Set (Var "H1")) ($#k19_group_9 :::""\/""::: ) (Set (Var "H2")))) & (Bool (Set (Var "H2")) "is" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Set (Var "H1")) ($#k19_group_9 :::""\/""::: ) (Set (Var "H2")))) ")" )))) ; theorem :: GROUP_9:36 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "H2")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "H1")) "is" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H2"))) "iff" (Bool (Set (Set (Var "H1")) ($#k19_group_9 :::""\/""::: ) (Set (Var "H2"))) ($#r1_hidden :::"="::: ) (Set (Var "H2"))) ")" ))))) ; theorem :: GROUP_9:37 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "H3")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "H1")) "is" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H3"))) & (Bool (Set (Var "H2")) "is" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H3")))) "holds" (Bool (Set (Set (Var "H1")) ($#k19_group_9 :::""\/""::: ) (Set (Var "H2"))) "is" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H3"))))))) ; theorem :: GROUP_9:38 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "H2")) "," (Set (Var "H3")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "H1")) "is" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H2")))) "holds" (Bool (Set (Set (Var "H1")) ($#k19_group_9 :::""\/""::: ) (Set (Var "H3"))) "is" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Set (Var "H2")) ($#k19_group_9 :::""\/""::: ) (Set (Var "H3")))))))) ; theorem :: GROUP_9:39 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H1")) (Bool "for" (Set (Var "X9")) "," (Set (Var "Y9")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "X9"))) & (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set (Var "Y9")))) "holds" (Bool (Set (Set (Var "X9")) ($#k17_group_9 :::"/\"::: ) (Set (Var "Y9"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k17_group_9 :::"/\"::: ) (Set (Var "Y"))))))))) ; theorem :: GROUP_9:40 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "N")) "being" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N")) "is" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H1")))) "holds" (Bool (Set (Var "N")) "is" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H1"))))))) ; theorem :: GROUP_9:41 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "N")) "being" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set (Var "H1")) ($#k17_group_9 :::"/\"::: ) (Set (Var "N"))) "is" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H1"))) & (Bool (Set (Set (Var "N")) ($#k17_group_9 :::"/\"::: ) (Set (Var "H1"))) "is" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H1"))) ")" ))))) ; theorem :: GROUP_9:42 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#v2_group_9 :::"strict"::: ) ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v7_struct_0 :::"trivial"::: ) )) "holds" (Bool (Set ($#k4_group_9 :::"(1)."::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Var "G"))))) ; theorem :: GROUP_9:43 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "N")) "being" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k1_group_1 :::"1_"::: ) (Set "(" (Set (Var "G")) ($#k10_group_9 :::"./."::: ) (Set (Var "N")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k15_group_9 :::"carr"::: ) (Set (Var "N"))))))) ; theorem :: GROUP_9:44 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#v2_group_9 :::"strict"::: ) ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "MN")) "being" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "N")) "st" (Bool (Bool (Set (Var "MN")) ($#r1_hidden :::"="::: ) (Set (Var "M"))) & (Bool (Set (Var "M")) "is" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "N")))) "holds" (Bool (Set (Set (Var "N")) ($#k10_group_9 :::"./."::: ) (Set (Var "MN"))) "is" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Set (Var "G")) ($#k10_group_9 :::"./."::: ) (Set (Var "M")))))))) ; theorem :: GROUP_9:45 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds" (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "H"))))))) ; theorem :: GROUP_9:46 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "g1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds" (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "g1")) ($#k2_group_1 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "g1")) ")" ) ($#k2_group_1 :::"""::: ) )))))) ; theorem :: GROUP_9:47 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "g1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds" (Bool "(" (Bool (Set (Var "g1")) ($#r1_struct_0 :::"in"::: ) (Set ($#k13_group_9 :::"Ker"::: ) (Set (Var "h")))) "iff" (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "g1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "H")))) ")" ))))) ; theorem :: GROUP_9:48 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "N")) "being" ($#v2_group_9 :::"strict"::: ) ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k13_group_9 :::"Ker"::: ) (Set "(" ($#k12_group_9 :::"nat_hom"::: ) (Set (Var "N")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "N")))))) ; theorem :: GROUP_9:49 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k14_group_9 :::"Image"::: ) (Set (Var "h")) ")" )))))) ; theorem :: GROUP_9:50 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "N")) "being" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k14_group_9 :::"Image"::: ) (Set "(" ($#k12_group_9 :::"nat_hom"::: ) (Set (Var "N")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k10_group_9 :::"./."::: ) (Set (Var "N"))))))) ; theorem :: GROUP_9:51 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H")) "being" ($#v2_group_9 :::"strict"::: ) ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds" (Bool "(" (Bool (Set (Var "h")) "is" ($#v2_funct_2 :::"onto"::: ) ) "iff" (Bool (Set ($#k14_group_9 :::"Image"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "H"))) ")" ))))) ; theorem :: GROUP_9:52 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H")) "being" ($#v2_group_9 :::"strict"::: ) ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "st" (Bool (Bool (Set (Var "h")) "is" ($#v2_funct_2 :::"onto"::: ) )) "holds" (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))))))))) ; theorem :: GROUP_9:53 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "N")) "being" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k12_group_9 :::"nat_hom"::: ) (Set (Var "N"))) "is" ($#v2_funct_2 :::"onto"::: ) )))) ; theorem :: GROUP_9:54 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) "holds" (Bool (Set ($#k12_group_9 :::"nat_hom"::: ) (Set "(" ($#k4_group_9 :::"(1)."::: ) (Set (Var "G")) ")" )) "is" ($#v3_funct_2 :::"bijective"::: ) ))) ; theorem :: GROUP_9:55 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "," (Set (Var "I")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) "st" (Bool (Bool (Set (Var "G")) "," (Set (Var "H")) ($#r3_group_9 :::"are_isomorphic"::: ) ) & (Bool (Set (Var "H")) "," (Set (Var "I")) ($#r3_group_9 :::"are_isomorphic"::: ) )) "holds" (Bool (Set (Var "G")) "," (Set (Var "I")) ($#r3_group_9 :::"are_isomorphic"::: ) ))) ; theorem :: GROUP_9:56 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#v2_group_9 :::"strict"::: ) ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) "holds" (Bool (Set (Var "G")) "," (Set (Set (Var "G")) ($#k10_group_9 :::"./."::: ) (Set "(" ($#k4_group_9 :::"(1)."::: ) (Set (Var "G")) ")" )) ($#r3_group_9 :::"are_isomorphic"::: ) ))) ; theorem :: GROUP_9:57 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#v2_group_9 :::"strict"::: ) ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) "holds" (Bool (Set (Set (Var "G")) ($#k10_group_9 :::"./."::: ) (Set "(" ($#k5_group_9 :::"(Omega)."::: ) (Set (Var "G")) ")" )) "is" ($#v7_struct_0 :::"trivial"::: ) ))) ; theorem :: GROUP_9:58 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#v2_group_9 :::"strict"::: ) ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) "st" (Bool (Bool (Set (Var "G")) "," (Set (Var "H")) ($#r3_group_9 :::"are_isomorphic"::: ) ) & (Bool (Set (Var "G")) "is" ($#v7_struct_0 :::"trivial"::: ) )) "holds" (Bool (Set (Var "H")) "is" ($#v7_struct_0 :::"trivial"::: ) ))) ; theorem :: GROUP_9:59 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "," (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds" (Bool (Set (Set (Var "G")) ($#k10_group_9 :::"./."::: ) (Set "(" ($#k13_group_9 :::"Ker"::: ) (Set (Var "h")) ")" )) "," (Set ($#k14_group_9 :::"Image"::: ) (Set (Var "h"))) ($#r3_group_9 :::"are_isomorphic"::: ) )))) ; theorem :: GROUP_9:60 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H")) "," (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "F1")) "is" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "F2")))) "holds" (Bool (Set (Set (Var "H")) ($#k17_group_9 :::"/\"::: ) (Set (Var "F1"))) "is" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Set (Var "H")) ($#k17_group_9 :::"/\"::: ) (Set (Var "F2"))))))) ; begin theorem :: GROUP_9:61 (Bool "for" (Set (Var "O")) "," (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Action":::) "of" (Set (Var "O")) "," (Set (Var "E")) "holds" (Bool (Set ($#k2_subset_1 :::"[#]"::: ) (Set (Var "E"))) ($#r1_group_9 :::"is_stable_under_the_action_of"::: ) (Set (Var "A"))))) ; theorem :: GROUP_9:62 (Bool "for" (Set (Var "O")) "," (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "O")) "," (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "E")) ")" ) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "is" ($#m1_subset_1 :::"Action":::) "of" (Set (Var "O")) "," (Set (Var "E")))) ; theorem :: GROUP_9:63 (Bool "for" (Set (Var "O")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "O")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Action":::) "of" (Set (Var "O")) "," (Set (Var "E")) "holds" (Bool (Set ($#k2_group_9 :::"Product"::: ) "(" (Set ($#k4_matrix_2 :::"<*"::: ) (Set (Var "o")) ($#k4_matrix_2 :::"*>"::: ) ) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_funct_2 :::"."::: ) (Set (Var "o")))))))) ; theorem :: GROUP_9:64 (Bool "for" (Set (Var "O")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "O")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Action":::) "of" (Set (Var "O")) "," (Set (Var "E")) "holds" (Bool (Set ($#k2_group_9 :::"Product"::: ) "(" (Set "(" (Set (Var "F1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "F2")) ")" ) "," (Set (Var "A")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k2_group_9 :::"Product"::: ) "(" (Set (Var "F1")) "," (Set (Var "A")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k2_group_9 :::"Product"::: ) "(" (Set (Var "F2")) "," (Set (Var "A")) ")" ")" ))))))) ; theorem :: GROUP_9:65 (Bool "for" (Set (Var "O")) "," (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Action":::) "of" (Set (Var "O")) "," (Set (Var "E")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "O")) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_group_9 :::"is_stable_under_the_action_of"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set "(" ($#k2_group_9 :::"Product"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "Y"))) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))))))) ; theorem :: GROUP_9:66 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Action":::) "of" (Set (Var "O")) "," (Set (Var "E")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "st" (Bool (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_group_9 :::"the_stable_subset_generated_by"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" )) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "O"))(Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Set "(" ($#k2_group_9 :::"Product"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ")" )))))) ; theorem :: GROUP_9:67 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "ex" (Set (Var "H")) "being" ($#v2_group_9 :::"strict"::: ) ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) "st" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "H"))) "#)" ))))) ; theorem :: GROUP_9:68 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "H1"))) "#)" ) "is" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")))))) ; theorem :: GROUP_9:69 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "N")) "being" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "N"))) "#)" ) "is" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")))))) ; theorem :: GROUP_9:70 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "O")) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "g1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "g1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H1")))) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k3_group_9 :::"^"::: ) (Set (Var "o")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "g1"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "H1")))))))) ; theorem :: GROUP_9:71 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "G9")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) (Bool "ex" (Set (Var "H9")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H")) "st" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H9"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G9")))))))))) ; theorem :: GROUP_9:72 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "holds" (Bool (Set ($#k18_group_9 :::"the_stable_subgroup_of"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k4_group_9 :::"(1)."::: ) (Set (Var "G"))))))) ; theorem :: GROUP_9:73 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_group_4 :::"gr"::: ) (Set (Var "C")) ")" )))) "holds" (Bool (Set ($#k18_group_9 :::"the_stable_subgroup_of"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k18_group_9 :::"the_stable_subgroup_of"::: ) (Set (Var "B"))))))) ; theorem :: GROUP_9:74 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "N")) "being" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "N9")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N9")) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "N"))) "#)" ))) "holds" (Bool "(" (Bool (Set (Set (Var "G")) ($#k5_group_6 :::"./."::: ) (Set (Var "N9"))) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "G")) ($#k10_group_9 :::"./."::: ) (Set (Var "N")) ")" )) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set "(" (Set (Var "G")) ($#k10_group_9 :::"./."::: ) (Set (Var "N")) ")" )) "#)" )) & (Bool (Set ($#k1_group_1 :::"1_"::: ) (Set "(" (Set (Var "G")) ($#k5_group_6 :::"./."::: ) (Set (Var "N9")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set "(" (Set (Var "G")) ($#k10_group_9 :::"./."::: ) (Set (Var "N")) ")" ))) ")" ))))) ; theorem :: GROUP_9:75 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2"))))) "holds" (Bool (Set ($#g1_group_9 :::"HGrWOpStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "H1"))) "," (Set "the" ($#u1_group_9 :::"action"::: ) "of" (Set (Var "H1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_group_9 :::"HGrWOpStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "H2"))) "," (Set "the" ($#u1_group_9 :::"action"::: ) "of" (Set (Var "H2"))) "#)" ))))) ; theorem :: GROUP_9:76 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "N1")) "being" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H1")) "st" (Bool (Bool (Set (Set (Var "H1")) ($#k10_group_9 :::"./."::: ) (Set (Var "N1"))) "is" ($#v7_struct_0 :::"trivial"::: ) )) "holds" (Bool (Set ($#g1_group_9 :::"HGrWOpStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "H1"))) "," (Set "the" ($#u1_group_9 :::"action"::: ) "of" (Set (Var "H1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_group_9 :::"HGrWOpStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N1"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "N1"))) "," (Set "the" ($#u1_group_9 :::"action"::: ) "of" (Set (Var "N1"))) "#)" )))))) ; theorem :: GROUP_9:77 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "N1")) "being" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H1")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N1"))))) "holds" (Bool (Set (Set (Var "H1")) ($#k10_group_9 :::"./."::: ) (Set (Var "N1"))) "is" ($#v7_struct_0 :::"trivial"::: ) ))))) ; theorem :: GROUP_9:78 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "H9")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "st" (Bool (Bool (Set (Var "N")) ($#r1_hidden :::"="::: ) (Set ($#k13_group_9 :::"Ker"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "G9")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G9"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H9"))))) & "(" (Bool (Bool (Set (Var "H9")) "is" ($#v4_group_9 :::"normal"::: ) )) "implies" (Bool "(" (Bool (Set (Var "N")) "is" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G9"))) & (Bool (Set (Var "G9")) "is" ($#v4_group_9 :::"normal"::: ) ) ")" ) ")" ")" ))))))) ; theorem :: GROUP_9:79 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "N")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "G9")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "st" (Bool (Bool (Set (Var "N")) ($#r1_hidden :::"="::: ) (Set ($#k13_group_9 :::"Ker"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "H9")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H")) "st" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H9"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G9"))))) & (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H9")))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "G9")) ($#k19_group_9 :::""\/""::: ) (Set (Var "N")) ")" ))) & "(" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_2 :::"onto"::: ) ) & (Bool (Set (Var "G9")) "is" ($#v4_group_9 :::"normal"::: ) )) "implies" (Bool (Set (Var "H9")) "is" ($#v4_group_9 :::"normal"::: ) ) ")" ")" ))))))) ; theorem :: GROUP_9:80 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#v2_group_9 :::"strict"::: ) ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "N")) "being" ($#v2_group_9 :::"strict"::: ) ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Set (Var "G")) ($#k10_group_9 :::"./."::: ) (Set (Var "N"))) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k12_group_9 :::"nat_hom"::: ) (Set (Var "N")) ")" ) ($#k8_relset_1 :::"""::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H")))))) "holds" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k5_group_9 :::"(Omega)."::: ) (Set "(" (Set (Var "G")) ($#k10_group_9 :::"./."::: ) (Set (Var "N")) ")" ))))))) ; theorem :: GROUP_9:81 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#v2_group_9 :::"strict"::: ) ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "N")) "being" ($#v2_group_9 :::"strict"::: ) ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Set (Var "G")) ($#k10_group_9 :::"./."::: ) (Set (Var "N"))) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k12_group_9 :::"nat_hom"::: ) (Set (Var "N")) ")" ) ($#k8_relset_1 :::"""::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H")))))) "holds" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k4_group_9 :::"(1)."::: ) (Set "(" (Set (Var "G")) ($#k10_group_9 :::"./."::: ) (Set (Var "N")) ")" ))))))) ; theorem :: GROUP_9:82 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#v2_group_9 :::"strict"::: ) ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) "st" (Bool (Bool (Set (Var "G")) "," (Set (Var "H")) ($#r3_group_9 :::"are_isomorphic"::: ) ) & (Bool (Set (Var "G")) "is" ($#v6_group_9 :::"simple"::: ) )) "holds" (Bool (Set (Var "H")) "is" ($#v6_group_9 :::"simple"::: ) ))) ; theorem :: GROUP_9:83 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "FG")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "FH")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))) (Bool "for" (Set (Var "I")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool (Bool (Set (Var "FG")) ($#r1_hidden :::"="::: ) (Set (Var "FH"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "FG"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "I"))))) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "FG")) ($#k4_group_4 :::"|^"::: ) (Set (Var "I")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "FH")) ($#k4_group_4 :::"|^"::: ) (Set (Var "I")) ")" ))))))))) ; theorem :: GROUP_9:84 (Bool "for" (Set (Var "O")) "," (Set (Var "E1")) "," (Set (Var "E2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"Action":::) "of" (Set (Var "O")) "," (Set (Var "E1")) (Bool "for" (Set (Var "A2")) "being" ($#m1_subset_1 :::"Action":::) "of" (Set (Var "O")) "," (Set (Var "E2")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "O")) "st" (Bool (Bool (Set (Var "E1")) ($#r1_tarski :::"c="::: ) (Set (Var "E2"))) & (Bool "(" "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "O")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "E1")) "," (Set (Var "E1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "E2")) "," (Set (Var "E2")) "st" (Bool (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k1_funct_1 :::"."::: ) (Set (Var "o")))) & (Bool (Set (Var "f2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A2")) ($#k1_funct_1 :::"."::: ) (Set (Var "o"))))) "holds" (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k2_partfun1 :::"|"::: ) (Set (Var "E1")))))) ")" )) "holds" (Bool (Set ($#k2_group_9 :::"Product"::: ) "(" (Set (Var "F")) "," (Set (Var "A1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_group_9 :::"Product"::: ) "(" (Set (Var "F")) "," (Set (Var "A2")) ")" ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "E1")))))))) ; theorem :: GROUP_9:85 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H1")) (Bool "for" (Set (Var "N19")) "," (Set (Var "N29")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N1")) ($#r1_hidden :::"="::: ) (Set (Var "N19"))) & (Bool (Set (Var "N2")) ($#r1_hidden :::"="::: ) (Set (Var "N29")))) "holds" (Bool (Set (Set (Var "N19")) ($#k16_group_9 :::"*"::: ) (Set (Var "N29"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k16_group_9 :::"*"::: ) (Set (Var "N2"))))))))) ; theorem :: GROUP_9:86 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H1")) (Bool "for" (Set (Var "N19")) "," (Set (Var "N29")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N1")) ($#r1_hidden :::"="::: ) (Set (Var "N19"))) & (Bool (Set (Var "N2")) ($#r1_hidden :::"="::: ) (Set (Var "N29")))) "holds" (Bool (Set (Set (Var "N19")) ($#k19_group_9 :::""\/""::: ) (Set (Var "N29"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k19_group_9 :::""\/""::: ) (Set (Var "N2"))))))))) ; theorem :: GROUP_9:87 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N1")) "is" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H1"))) & (Bool (Set (Var "N2")) "is" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H1")))) "holds" (Bool (Set (Set (Var "N1")) ($#k19_group_9 :::""\/""::: ) (Set (Var "N2"))) "is" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H1"))))))) ; theorem :: GROUP_9:88 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "," (Set (Var "I")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "H")) "," (Set (Var "I")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k13_group_9 :::"Ker"::: ) (Set "(" (Set (Var "g")) ($#k11_group_9 :::"*"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k13_group_9 :::"Ker"::: ) (Set (Var "g")) ")" )))))))) ; theorem :: GROUP_9:89 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "G9")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "H9")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "st" (Bool (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H9"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G9"))))) "or" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G9"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H9"))))) ")" )) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G9")))) "is" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G9")) "," (Set (Var "H9")))))))) ; theorem :: GROUP_9:90 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#v2_group_9 :::"strict"::: ) ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "N")) "," (Set (Var "L")) "," (Set (Var "G9")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "st" (Bool (Bool (Set (Var "N")) ($#r1_hidden :::"="::: ) (Set ($#k13_group_9 :::"Ker"::: ) (Set (Var "f")))) & (Bool (Set (Var "L")) "is" ($#v2_group_9 :::"strict"::: ) ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G9")))) "holds" (Bool "(" (Bool (Set (Set (Var "L")) ($#k19_group_9 :::""\/""::: ) (Set "(" (Set (Var "G9")) ($#k17_group_9 :::"/\"::: ) (Set (Var "N")) ")" )) "is" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G9"))) & (Bool (Set (Set (Var "L")) ($#k19_group_9 :::""\/""::: ) (Set (Var "N"))) "is" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Set (Var "G9")) ($#k19_group_9 :::""\/""::: ) (Set (Var "N")))) & (Bool "(" "for" (Set (Var "N1")) "being" ($#v2_group_9 :::"strict"::: ) ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Set (Var "G9")) ($#k19_group_9 :::""\/""::: ) (Set (Var "N"))) (Bool "for" (Set (Var "N2")) "being" ($#v2_group_9 :::"strict"::: ) ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G9")) "st" (Bool (Bool (Set (Var "N1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k19_group_9 :::""\/""::: ) (Set (Var "N")))) & (Bool (Set (Var "N2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k19_group_9 :::""\/""::: ) (Set "(" (Set (Var "G9")) ($#k17_group_9 :::"/\"::: ) (Set (Var "N")) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "G9")) ($#k19_group_9 :::""\/""::: ) (Set (Var "N")) ")" ) ($#k10_group_9 :::"./."::: ) (Set (Var "N1"))) "," (Set (Set (Var "G9")) ($#k10_group_9 :::"./."::: ) (Set (Var "N2"))) ($#r3_group_9 :::"are_isomorphic"::: ) )) ")" ) ")" ))))) ; begin theorem :: GROUP_9:91 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H")) "," (Set (Var "K")) "," (Set (Var "H9")) "," (Set (Var "K9")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "JH")) "being" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Set (Var "H9")) ($#k19_group_9 :::""\/""::: ) (Set "(" (Set (Var "H")) ($#k17_group_9 :::"/\"::: ) (Set (Var "K")) ")" )) (Bool "for" (Set (Var "HK")) "being" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Set (Var "H")) ($#k17_group_9 :::"/\"::: ) (Set (Var "K"))) "st" (Bool (Bool (Set (Var "H9")) "is" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H"))) & (Bool (Set (Var "K9")) "is" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "K"))) & (Bool (Set (Var "JH")) ($#r1_hidden :::"="::: ) (Set (Set (Var "H9")) ($#k19_group_9 :::""\/""::: ) (Set "(" (Set (Var "H")) ($#k17_group_9 :::"/\"::: ) (Set (Var "K9")) ")" ))) & (Bool (Set (Var "HK")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "H9")) ($#k17_group_9 :::"/\"::: ) (Set (Var "K")) ")" ) ($#k19_group_9 :::""\/""::: ) (Set "(" (Set (Var "K9")) ($#k17_group_9 :::"/\"::: ) (Set (Var "H")) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "H9")) ($#k19_group_9 :::""\/""::: ) (Set "(" (Set (Var "H")) ($#k17_group_9 :::"/\"::: ) (Set (Var "K")) ")" ) ")" ) ($#k10_group_9 :::"./."::: ) (Set (Var "JH"))) "," (Set (Set "(" (Set (Var "H")) ($#k17_group_9 :::"/\"::: ) (Set (Var "K")) ")" ) ($#k10_group_9 :::"./."::: ) (Set (Var "HK"))) ($#r3_group_9 :::"are_isomorphic"::: ) )))))) ; theorem :: GROUP_9:92 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H")) "," (Set (Var "K")) "," (Set (Var "H9")) "," (Set (Var "K9")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "H9")) "is" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H"))) & (Bool (Set (Var "K9")) "is" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set (Set (Var "H9")) ($#k19_group_9 :::""\/""::: ) (Set "(" (Set (Var "H")) ($#k17_group_9 :::"/\"::: ) (Set (Var "K9")) ")" )) "is" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Set (Var "H9")) ($#k19_group_9 :::""\/""::: ) (Set "(" (Set (Var "H")) ($#k17_group_9 :::"/\"::: ) (Set (Var "K")) ")" )))))) ; theorem :: GROUP_9:93 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H")) "," (Set (Var "K")) "," (Set (Var "H9")) "," (Set (Var "K9")) "being" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "JH")) "being" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Set (Var "H9")) ($#k19_group_9 :::""\/""::: ) (Set "(" (Set (Var "H")) ($#k17_group_9 :::"/\"::: ) (Set (Var "K")) ")" )) (Bool "for" (Set (Var "JK")) "being" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Set (Var "K9")) ($#k19_group_9 :::""\/""::: ) (Set "(" (Set (Var "K")) ($#k17_group_9 :::"/\"::: ) (Set (Var "H")) ")" )) "st" (Bool (Bool (Set (Var "JH")) ($#r1_hidden :::"="::: ) (Set (Set (Var "H9")) ($#k19_group_9 :::""\/""::: ) (Set "(" (Set (Var "H")) ($#k17_group_9 :::"/\"::: ) (Set (Var "K9")) ")" ))) & (Bool (Set (Var "JK")) ($#r1_hidden :::"="::: ) (Set (Set (Var "K9")) ($#k19_group_9 :::""\/""::: ) (Set "(" (Set (Var "K")) ($#k17_group_9 :::"/\"::: ) (Set (Var "H9")) ")" ))) & (Bool (Set (Var "H9")) "is" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H"))) & (Bool (Set (Var "K9")) "is" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set (Set "(" (Set (Var "H9")) ($#k19_group_9 :::""\/""::: ) (Set "(" (Set (Var "H")) ($#k17_group_9 :::"/\"::: ) (Set (Var "K")) ")" ) ")" ) ($#k10_group_9 :::"./."::: ) (Set (Var "JH"))) "," (Set (Set "(" (Set (Var "K9")) ($#k19_group_9 :::""\/""::: ) (Set "(" (Set (Var "K")) ($#k17_group_9 :::"/\"::: ) (Set (Var "H")) ")" ) ")" ) ($#k10_group_9 :::"./."::: ) (Set (Var "JK"))) ($#r3_group_9 :::"are_isomorphic"::: ) )))))) ; begin definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); let "IT" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k6_group_9 :::"the_stable_subgroups_of"::: ) (Set (Const "G"))); attr "IT" is :::"composition_series"::: means :: GROUP_9:def 28 (Bool "(" (Bool (Set "IT" ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k5_group_9 :::"(Omega)."::: ) "G")) & (Bool (Set "IT" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "IT" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_group_9 :::"(1)."::: ) "G")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "IT")) & (Bool (Set (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "IT"))) "holds" (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" "G" "st" (Bool (Bool (Set (Var "H1")) ($#r1_hidden :::"="::: ) (Set "IT" ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "H2")) ($#r1_hidden :::"="::: ) (Set "IT" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool (Set (Var "H2")) "is" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H1")))) ")" ) ")" ); end; :: deftheorem defines :::"composition_series"::: GROUP_9:def 28 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "IT")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k6_group_9 :::"the_stable_subgroups_of"::: ) (Set (Var "G"))) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v8_group_9 :::"composition_series"::: ) ) "iff" (Bool "(" (Bool (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k5_group_9 :::"(Omega)."::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "IT")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_group_9 :::"(1)."::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "IT")))) & (Bool (Set (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "IT"))))) "holds" (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "H1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "H2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool (Set (Var "H2")) "is" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H1")))) ")" ) ")" ) ")" )))); registrationlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k6_group_9 :::"the_stable_subgroups_of"::: ) "G") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v8_group_9 :::"composition_series"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k6_group_9 :::"the_stable_subgroups_of"::: ) "G"); end; definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); mode CompositionSeries of "G" is ($#v8_group_9 :::"composition_series"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k6_group_9 :::"the_stable_subgroups_of"::: ) "G"); end; definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); let "s1", "s2" be ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Const "G")); pred "s1" :::"is_finer_than"::: "s2" means :: GROUP_9:def 29 (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "s1")) & (Bool "s2" ($#r2_relset_1 :::"="::: ) (Set "s1" ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k14_finseq_1 :::"Sgm"::: ) (Set (Var "x")) ")" ))) ")" )); reflexivity (Bool "for" (Set (Var "s1")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Const "G")) (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "s1")))) & (Bool (Set (Var "s1")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "s1")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k14_finseq_1 :::"Sgm"::: ) (Set (Var "x")) ")" ))) ")" ))) ; end; :: deftheorem defines :::"is_finer_than"::: GROUP_9:def 29 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "s1")) ($#r4_group_9 :::"is_finer_than"::: ) (Set (Var "s2"))) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "s1")))) & (Bool (Set (Var "s2")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "s1")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k14_finseq_1 :::"Sgm"::: ) (Set (Var "x")) ")" ))) ")" )) ")" )))); definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); let "IT" be ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Const "G")); attr "IT" is :::"strictly_decreasing"::: means :: GROUP_9:def 30 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "IT")) & (Bool (Set (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "IT"))) "holds" (Bool "for" (Set (Var "H")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" "G" (Bool "for" (Set (Var "N")) "being" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H")) "st" (Bool (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set "IT" ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "N")) ($#r1_hidden :::"="::: ) (Set "IT" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool "not" (Bool (Set (Set (Var "H")) ($#k10_group_9 :::"./."::: ) (Set (Var "N"))) "is" ($#v7_struct_0 :::"trivial"::: ) ))))); end; :: deftheorem defines :::"strictly_decreasing"::: GROUP_9:def 30 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "IT")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v9_group_9 :::"strictly_decreasing"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "IT")))) & (Bool (Set (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "IT"))))) "holds" (Bool "for" (Set (Var "H")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H")) "st" (Bool (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "N")) ($#r1_hidden :::"="::: ) (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool "not" (Bool (Set (Set (Var "H")) ($#k10_group_9 :::"./."::: ) (Set (Var "N"))) "is" ($#v7_struct_0 :::"trivial"::: ) ))))) ")" )))); definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); let "IT" be ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Const "G")); attr "IT" is :::"jordan_holder"::: means :: GROUP_9:def 31 (Bool "(" (Bool "IT" "is" ($#v9_group_9 :::"strictly_decreasing"::: ) ) & (Bool "(" "for" (Set (Var "s")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" "G" "holds" (Bool "(" "not" (Bool (Set (Var "s")) ($#r1_hidden :::"<>"::: ) "IT") "or" "not" (Bool (Set (Var "s")) "is" ($#v9_group_9 :::"strictly_decreasing"::: ) ) "or" "not" (Bool (Set (Var "s")) ($#r4_group_9 :::"is_finer_than"::: ) "IT") ")" ) ")" ) ")" ); end; :: deftheorem defines :::"jordan_holder"::: GROUP_9:def 31 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "IT")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v10_group_9 :::"jordan_holder"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v9_group_9 :::"strictly_decreasing"::: ) ) & (Bool "(" "for" (Set (Var "s")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) "holds" (Bool "(" "not" (Bool (Set (Var "s")) ($#r1_hidden :::"<>"::: ) (Set (Var "IT"))) "or" "not" (Bool (Set (Var "s")) "is" ($#v9_group_9 :::"strictly_decreasing"::: ) ) "or" "not" (Bool (Set (Var "s")) ($#r4_group_9 :::"is_finer_than"::: ) (Set (Var "IT"))) ")" ) ")" ) ")" ) ")" )))); definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G1", "G2" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); let "s1" be ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Const "G1")); let "s2" be ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Const "G2")); pred "s1" :::"is_equivalent_with"::: "s2" means :: GROUP_9:def 32 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "s1") ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "s2")) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "s1"))) "holds" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "st" (Bool "for" (Set (Var "H1")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" "G1" (Bool "for" (Set (Var "H2")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" "G2" (Bool "for" (Set (Var "N1")) "being" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H1")) (Bool "for" (Set (Var "N2")) "being" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H2")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "H1")) ($#r1_hidden :::"="::: ) (Set "s1" ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "H2")) ($#r1_hidden :::"="::: ) (Set "s2" ($#k1_funct_1 :::"."::: ) (Set (Var "j")))) & (Bool (Set (Var "N1")) ($#r1_hidden :::"="::: ) (Set "s1" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Var "N2")) ($#r1_hidden :::"="::: ) (Set "s2" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "j")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool (Set (Set (Var "H1")) ($#k10_group_9 :::"./."::: ) (Set (Var "N1"))) "," (Set (Set (Var "H2")) ($#k10_group_9 :::"./."::: ) (Set (Var "N2"))) ($#r3_group_9 :::"are_isomorphic"::: ) ))))))) ")" ) ")" ); end; :: deftheorem defines :::"is_equivalent_with"::: GROUP_9:def 32 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "s1")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "s2")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G2")) "holds" (Bool "(" (Bool (Set (Var "s1")) ($#r5_group_9 :::"is_equivalent_with"::: ) (Set (Var "s2"))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s2")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s1"))))) "holds" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "st" (Bool "for" (Set (Var "H1")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "H2")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G2")) (Bool "for" (Set (Var "N1")) "being" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H1")) (Bool "for" (Set (Var "N2")) "being" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H2")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "H1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "H2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))) & (Bool (Set (Var "N1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Var "N2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "j")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool (Set (Set (Var "H1")) ($#k10_group_9 :::"./."::: ) (Set (Var "N1"))) "," (Set (Set (Var "H2")) ($#k10_group_9 :::"./."::: ) (Set (Var "N2"))) ($#r3_group_9 :::"are_isomorphic"::: ) ))))))) ")" ) ")" ) ")" ))))); definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); let "s" be ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Const "G")); func :::"the_series_of_quotients_of"::: "s" -> ($#m1_hidden :::"FinSequence":::) means :: GROUP_9:def 33 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "s") ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) it ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) it))) "holds" (Bool "for" (Set (Var "H")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" "G" (Bool "for" (Set (Var "N")) "being" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H")) "st" (Bool (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set "s" ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "N")) ($#r1_hidden :::"="::: ) (Set "s" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k10_group_9 :::"./."::: ) (Set (Var "N")))))) ")" ) ")" ) if (Bool (Set ($#k3_finseq_1 :::"len"::: ) "s") ($#r1_xxreal_0 :::">"::: ) (Num 1)) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); end; :: deftheorem defines :::"the_series_of_quotients_of"::: GROUP_9:def 33 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "s")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k20_group_9 :::"the_series_of_quotients_of"::: ) (Set (Var "s")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b4"))))) "holds" (Bool "for" (Set (Var "H")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H")) "st" (Bool (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "N")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k10_group_9 :::"./."::: ) (Set (Var "N")))))) ")" ) ")" ) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_xxreal_0 :::">"::: ) (Num 1)))) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k20_group_9 :::"the_series_of_quotients_of"::: ) (Set (Var "s")))) "iff" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ")" ))))); definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "f1", "f2" be ($#m1_hidden :::"FinSequence":::); let "p" be ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Const "f1")) ")" ); pred "f1" "," "f2" :::"are_equivalent_under"::: "p" "," "O" means :: GROUP_9:def 34 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "f1") ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "f2")) & (Bool "(" "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" "O" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "f1")) & (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set (Set "(" "p" ($#k2_funct_2 :::"""::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "H1")) ($#r1_hidden :::"="::: ) (Set "f1" ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "H2")) ($#r1_hidden :::"="::: ) (Set "f2" ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))) "holds" (Bool (Set (Var "H1")) "," (Set (Var "H2")) ($#r3_group_9 :::"are_isomorphic"::: ) )) ")" ) ")" ); end; :: deftheorem defines :::"are_equivalent_under"::: GROUP_9:def 34 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f1")) ")" ) "holds" (Bool "(" (Bool (Set (Var "f1")) "," (Set (Var "f2")) ($#r6_group_9 :::"are_equivalent_under"::: ) (Set (Var "p")) "," (Set (Var "O"))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f2")))) & (Bool "(" "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f1")))) & (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k2_funct_2 :::"""::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "H1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "H2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))) "holds" (Bool (Set (Var "H1")) "," (Set (Var "H2")) ($#r3_group_9 :::"are_isomorphic"::: ) )) ")" ) ")" ) ")" )))); theorem :: GROUP_9:94 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "s1")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "fs")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k6_group_9 :::"the_stable_subgroups_of"::: ) (Set (Var "G"))) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "s1")))) & (Bool (Set (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "s1")))) & (Bool (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Var "fs")) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "s1")) "," (Set (Var "i")) ")" ))) "holds" (Bool (Set (Var "fs")) "is" ($#v8_group_9 :::"composition_series"::: ) )))))) ; theorem :: GROUP_9:95 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "s1")) ($#r4_group_9 :::"is_finer_than"::: ) (Set (Var "s2")))) "holds" (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "s2")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")))))))) ; theorem :: GROUP_9:96 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "s2")) "," (Set (Var "s1")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s1")))) & (Bool (Set (Var "s2")) ($#r4_group_9 :::"is_finer_than"::: ) (Set (Var "s1")))) "holds" (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Var "s2")))))) ; theorem :: GROUP_9:97 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) "st" (Bool (Bool (Bool "not" (Set (Var "s1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "s2")) ($#r4_group_9 :::"is_finer_than"::: ) (Set (Var "s1")))) "holds" (Bool "not" (Bool (Set (Var "s2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))))) ; theorem :: GROUP_9:98 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "s1")) ($#r4_group_9 :::"is_finer_than"::: ) (Set (Var "s2"))) & (Bool (Set (Var "s1")) "is" ($#v10_group_9 :::"jordan_holder"::: ) ) & (Bool (Set (Var "s2")) "is" ($#v10_group_9 :::"jordan_holder"::: ) )) "holds" (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Var "s2")))))) ; theorem :: GROUP_9:99 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "s1")) "," (Set (Var "s19")) "," (Set (Var "s2")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "s1")))) & (Bool (Set (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "s1")))) & (Bool (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Var "s19")) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "s1")) "," (Set (Var "i")) ")" )) & (Bool (Set (Var "s2")) "is" ($#v10_group_9 :::"jordan_holder"::: ) ) & (Bool (Set (Var "s1")) ($#r4_group_9 :::"is_finer_than"::: ) (Set (Var "s2")))) "holds" (Bool (Set (Var "s19")) ($#r4_group_9 :::"is_finer_than"::: ) (Set (Var "s2"))))))) ; theorem :: GROUP_9:100 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s1"))) ($#r1_xxreal_0 :::">"::: ) (Num 1)) & (Bool (Set (Var "s2")) ($#r1_hidden :::"<>"::: ) (Set (Var "s1"))) & (Bool (Set (Var "s2")) "is" ($#v9_group_9 :::"strictly_decreasing"::: ) ) & (Bool (Set (Var "s2")) ($#r4_group_9 :::"is_finer_than"::: ) (Set (Var "s1")))) "holds" (Bool "ex" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "s1")))) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "s2")))) & (Bool (Set (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "s1")))) & (Bool (Set (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "s2")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "s2")))) & (Bool (Set (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "s2")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))) ")" ))))) ; theorem :: GROUP_9:101 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "s1")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "s1")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "s1")))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "H1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "H2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))) "holds" (Bool (Set (Var "H2")) "is" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H1")))))))) ; theorem :: GROUP_9:102 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s1")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k20_group_9 :::"the_series_of_quotients_of"::: ) (Set (Var "s1")) ")" )))) "holds" (Bool (Set (Var "y")) "is" ($#v2_group_9 :::"strict"::: ) ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O"))))))) ; theorem :: GROUP_9:103 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "s1")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k20_group_9 :::"the_series_of_quotients_of"::: ) (Set (Var "s1")) ")" ))) & (Bool "(" "for" (Set (Var "H")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) "st" (Bool (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k20_group_9 :::"the_series_of_quotients_of"::: ) (Set (Var "s1")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Var "H")) "is" ($#v7_struct_0 :::"trivial"::: ) ) ")" )) "holds" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "s1")))) & (Bool (Set (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "s1")))) & (Bool (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" ))))) ; theorem :: GROUP_9:104 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "s1")))) & (Bool (Set (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "s1")))) & (Bool (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "s1")) "," (Set (Var "i")) ")" ))) "holds" (Bool (Set ($#k20_group_9 :::"the_series_of_quotients_of"::: ) (Set (Var "s2"))) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_3 :::"Del"::: ) "(" (Set "(" ($#k20_group_9 :::"the_series_of_quotients_of"::: ) (Set (Var "s1")) ")" ) "," (Set (Var "i")) ")" )))))) ; theorem :: GROUP_9:105 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "s1")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "f1")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set ($#k20_group_9 :::"the_series_of_quotients_of"::: ) (Set (Var "s1")))) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f1")))) & (Bool "(" "for" (Set (Var "H")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) "st" (Bool (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Var "H")) "is" ($#v7_struct_0 :::"trivial"::: ) ) ")" )) "holds" (Bool "(" (Bool (Set ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "s1")) "," (Set (Var "i")) ")" ) "is" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G"))) & (Bool "(" "for" (Set (Var "s2")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "s1")) "," (Set (Var "i")) ")" ))) "holds" (Bool (Set ($#k20_group_9 :::"the_series_of_quotients_of"::: ) (Set (Var "s2"))) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "f1")) "," (Set (Var "i")) ")" )) ")" ) ")" )))))) ; theorem :: GROUP_9:106 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f1")))) & (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f1")) ")" ) "st" (Bool "(" (Bool (Set (Var "f1")) "," (Set (Var "f2")) ($#r6_group_9 :::"are_equivalent_under"::: ) (Set (Var "p")) "," (Set (Var "O"))) & (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k2_funct_2 :::"""::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ))) "holds" (Bool "ex" (Set (Var "p9")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "f1")) "," (Set (Var "i")) ")" ")" ) ")" ) "st" (Bool (Set ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "f1")) "," (Set (Var "i")) ")" ) "," (Set ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "f2")) "," (Set (Var "j")) ")" ) ($#r6_group_9 :::"are_equivalent_under"::: ) (Set (Var "p9")) "," (Set (Var "O"))))))) ; theorem :: GROUP_9:107 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "s1")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "s2")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "s1")) "is" ($#v1_xboole_0 :::"empty"::: ) ) & (Bool (Set (Var "s2")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "holds" (Bool (Set (Var "s1")) ($#r5_group_9 :::"is_equivalent_with"::: ) (Set (Var "s2"))))))) ; theorem :: GROUP_9:108 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "s1")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "s2")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Bool "not" (Set (Var "s1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "s2")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "s1")) ($#r5_group_9 :::"is_equivalent_with"::: ) (Set (Var "s2"))) "iff" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k20_group_9 :::"the_series_of_quotients_of"::: ) (Set (Var "s1")) ")" ) ")" ) "st" (Bool (Set ($#k20_group_9 :::"the_series_of_quotients_of"::: ) (Set (Var "s1"))) "," (Set ($#k20_group_9 :::"the_series_of_quotients_of"::: ) (Set (Var "s2"))) ($#r6_group_9 :::"are_equivalent_under"::: ) (Set (Var "p")) "," (Set (Var "O")))) ")" ))))) ; theorem :: GROUP_9:109 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "s1")) ($#r4_group_9 :::"is_finer_than"::: ) (Set (Var "s2"))) & (Bool (Set (Var "s2")) "is" ($#v10_group_9 :::"jordan_holder"::: ) ) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s1"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s2"))))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k20_group_9 :::"the_series_of_quotients_of"::: ) (Set (Var "s1")) ")" ))) & (Bool "(" "for" (Set (Var "H")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) "st" (Bool (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k20_group_9 :::"the_series_of_quotients_of"::: ) (Set (Var "s1")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Var "H")) "is" ($#v7_struct_0 :::"trivial"::: ) ) ")" ) ")" ))))) ; theorem :: GROUP_9:110 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "s1")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s1"))) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Var "s1")) "is" ($#v10_group_9 :::"jordan_holder"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k20_group_9 :::"the_series_of_quotients_of"::: ) (Set (Var "s1")) ")" )))) "holds" (Bool (Set (Set "(" ($#k20_group_9 :::"the_series_of_quotients_of"::: ) (Set (Var "s1")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#v2_group_9 :::"strict"::: ) ($#v6_group_9 :::"simple"::: ) ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")))) ")" )))) ; theorem :: GROUP_9:111 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "s1")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "s1")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)))) "holds" (Bool "(" (Bool (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G"))) & (Bool (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) "is" ($#v2_group_9 :::"strict"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G"))) ")" ))))) ; theorem :: GROUP_9:112 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "s1")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "s1")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool (Set (Var "H1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "H2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool (Set (Var "H2")) "is" ($#v4_group_9 :::"normal"::: ) ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "H1")))))))) ; theorem :: GROUP_9:113 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "s1")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) "holds" (Bool (Set (Var "s1")) ($#r5_group_9 :::"is_equivalent_with"::: ) (Set (Var "s1")))))) ; theorem :: GROUP_9:114 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) "st" (Bool (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s1"))) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) "or" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s2"))) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) ")" ) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s1"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s2"))))) "holds" (Bool (Set (Var "s2")) ($#r4_group_9 :::"is_finer_than"::: ) (Set (Var "s1")))))) ; theorem :: GROUP_9:115 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "s1")) ($#r5_group_9 :::"is_equivalent_with"::: ) (Set (Var "s2"))) & (Bool (Set (Var "s1")) "is" ($#v10_group_9 :::"jordan_holder"::: ) )) "holds" (Bool (Set (Var "s2")) "is" ($#v10_group_9 :::"jordan_holder"::: ) )))) ; begin definitionlet "O" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Const "O")); let "s1", "s2" be ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Const "G")); assume that (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Const "s1"))) ($#r1_xxreal_0 :::">"::: ) (Num 1)) and (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Const "s2"))) ($#r1_xxreal_0 :::">"::: ) (Num 1)) ; func :::"the_schreier_series_of"::: "(" "s1" "," "s2" ")" -> ($#m2_finseq_1 :::"CompositionSeries":::) "of" "G" means :: GROUP_9:def 35 (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "," (Set (Var "H3")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" "G" "holds" (Bool "(" "(" (Bool (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) "s2" ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) "s1" ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) "s2" ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool (Set (Var "H1")) ($#r1_hidden :::"="::: ) (Set "s1" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Var "H2")) ($#r1_hidden :::"="::: ) (Set "s1" ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "H3")) ($#r1_hidden :::"="::: ) (Set "s2" ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))) "implies" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k19_group_9 :::""\/""::: ) (Set "(" (Set (Var "H2")) ($#k17_group_9 :::"/\"::: ) (Set (Var "H3")) ")" ))) ")" & "(" (Bool (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) "s1" ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) "s2" ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)))) "implies" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_group_9 :::"(1)."::: ) "G")) ")" & (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) "s1" ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) "s2" ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1))) ")" ))); end; :: deftheorem defines :::"the_schreier_series_of"::: GROUP_9:def 35 : (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s1"))) ($#r1_xxreal_0 :::">"::: ) (Num 1)) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s2"))) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k21_group_9 :::"the_schreier_series_of"::: ) "(" (Set (Var "s1")) "," (Set (Var "s2")) ")" )) "iff" (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "," (Set (Var "H3")) "being" ($#m1_group_9 :::"StableSubgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "s2")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "s1")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "s2")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool (Set (Var "H1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Var "H2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "H3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))) "implies" (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k19_group_9 :::""\/""::: ) (Set "(" (Set (Var "H2")) ($#k17_group_9 :::"/\"::: ) (Set (Var "H3")) ")" ))) ")" & "(" (Bool (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "s1")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "s2")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)))) "implies" (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_group_9 :::"(1)."::: ) (Set (Var "G")))) ")" & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "s1")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "s2")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1))) ")" ))) ")" ))))); theorem :: GROUP_9:116 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s1"))) ($#r1_xxreal_0 :::">"::: ) (Num 1)) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s2"))) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool (Set ($#k21_group_9 :::"the_schreier_series_of"::: ) "(" (Set (Var "s1")) "," (Set (Var "s2")) ")" ) ($#r4_group_9 :::"is_finer_than"::: ) (Set (Var "s1")))))) ; theorem :: GROUP_9:117 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s1"))) ($#r1_xxreal_0 :::">"::: ) (Num 1)) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s2"))) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool (Set ($#k21_group_9 :::"the_schreier_series_of"::: ) "(" (Set (Var "s1")) "," (Set (Var "s2")) ")" ) ($#r5_group_9 :::"is_equivalent_with"::: ) (Set ($#k21_group_9 :::"the_schreier_series_of"::: ) "(" (Set (Var "s2")) "," (Set (Var "s1")) ")" ))))) ; theorem :: GROUP_9:118 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) (Bool "ex" (Set (Var "s19")) "," (Set (Var "s29")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "s19")) ($#r4_group_9 :::"is_finer_than"::: ) (Set (Var "s1"))) & (Bool (Set (Var "s29")) ($#r4_group_9 :::"is_finer_than"::: ) (Set (Var "s2"))) & (Bool (Set (Var "s19")) ($#r5_group_9 :::"is_equivalent_with"::: ) (Set (Var "s29"))) ")" ))))) ; begin theorem :: GROUP_9:119 (Bool "for" (Set (Var "O")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l1_group_9 :::"GroupWithOperators":::) "of" (Set (Var "O")) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m2_finseq_1 :::"CompositionSeries":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "s1")) "is" ($#v10_group_9 :::"jordan_holder"::: ) ) & (Bool (Set (Var "s2")) "is" ($#v10_group_9 :::"jordan_holder"::: ) )) "holds" (Bool (Set (Var "s1")) ($#r5_group_9 :::"is_equivalent_with"::: ) (Set (Var "s2")))))) ; begin theorem :: GROUP_9:120 (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "P")) ")" ) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R")))) "iff" (Bool (Set (Set (Var "P")) ($#k2_relat_1 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "P")) ($#k2_relat_1 :::"~"::: ) ")" ) ")" ))) ")" )) ; theorem :: GROUP_9:121 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "P")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "P")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "R")))))) ; theorem :: GROUP_9:122 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v5_valued_0 :::"increasing"::: ) ) & (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )))) "holds" (Bool (Set ($#k14_finseq_1 :::"Sgm"::: ) (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k14_finseq_1 :::"Sgm"::: ) (Set (Var "X")) ")" )))))) ; theorem :: GROUP_9:123 (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "y")) ($#r1_tarski :::"c="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Bool "not" (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "y"))))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set ($#k14_finseq_1 :::"Sgm"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k14_finseq_1 :::"Sgm"::: ) (Set "(" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "i")) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) ($#k2_funct_1 :::"""::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k14_finseq_1 :::"Sgm"::: ) (Set (Var "y")) ")" ))) & (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) ")" )))) ; theorem :: GROUP_9:124 (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 "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_3 :::"Del"::: ) "(" (Set "(" ($#k5_finseq_5 :::"Ins"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) "," (Set (Var "p")) ")" ")" ) "," (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )))))) ; theorem :: GROUP_9:125 (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "F1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "F2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))) (Bool "for" (Set (Var "I")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "st" (Bool (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F1"))))) "holds" (Bool (Set (Set (Var "F2")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "F1")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ))) ")" ) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "I")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "I"))))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "F1")) ($#k4_group_4 :::"|^"::: ) (Set (Var "I")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "F2")) ($#k4_group_4 :::"|^"::: ) (Set (Var "I")) ")" )))))))) ;