:: GRNILP_1 semantic presentation begin theorem :: GRNILP_1:1 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ))))) ; theorem :: GRNILP_1:2 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) ($#k2_group_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) ($#k2_group_5 :::".]"::: ) ) ($#k2_group_3 :::"|^"::: ) (Set (Var "b")))))) ; theorem :: GRNILP_1:3 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) ($#k2_group_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_group_5 :::"[."::: ) (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) "," (Set (Var "b")) ($#k2_group_5 :::".]"::: ) ) ($#k2_group_3 :::"|^"::: ) (Set (Var "a")))))) ; theorem :: GRNILP_1:4 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) ($#k2_group_5 :::".]"::: ) ) ($#k2_group_3 :::"|^"::: ) (Set (Var "b")) ")" ) ($#k2_group_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_group_5 :::"[."::: ) (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) "," (Set (Var "a")) ($#k2_group_5 :::".]"::: ) ) ($#k2_group_3 :::"|^"::: ) (Set (Var "b")))))) ; theorem :: GRNILP_1:5 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set ($#k3_group_5 :::"[."::: ) (Set (Var "a")) "," (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) "," (Set (Var "c")) ($#k3_group_5 :::".]"::: ) ) ($#k2_group_3 :::"|^"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k2_group_5 :::"[."::: ) (Set "(" (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) ($#k2_group_5 :::".]"::: ) ) ($#k2_group_3 :::"|^"::: ) (Set (Var "b")) ")" ) "," (Set "(" (Set (Var "c")) ($#k2_group_3 :::"|^"::: ) (Set (Var "b")) ")" ) ($#k2_group_5 :::".]"::: ) )))) ; theorem :: GRNILP_1:6 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set ($#k2_group_5 :::"[."::: ) (Set (Var "a")) "," (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) ($#k2_group_5 :::".]"::: ) ) ($#k2_group_3 :::"|^"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k2_group_5 :::"[."::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k2_group_5 :::".]"::: ) )))) ; theorem :: GRNILP_1:7 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set ($#k3_group_5 :::"[."::: ) (Set (Var "a")) "," (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) "," (Set (Var "c")) ($#k3_group_5 :::".]"::: ) ) ($#k2_group_3 :::"|^"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k3_group_5 :::"[."::: ) (Set (Var "b")) "," (Set (Var "a")) "," (Set "(" (Set (Var "c")) ($#k2_group_3 :::"|^"::: ) (Set (Var "b")) ")" ) ($#k3_group_5 :::".]"::: ) )))) ; theorem :: GRNILP_1:8 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set ($#k3_group_5 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" (Set (Var "c")) ($#k2_group_3 :::"|^"::: ) (Set (Var "a")) ")" ) ($#k3_group_5 :::".]"::: ) ) ($#k6_algstr_0 :::"*"::: ) (Set ($#k3_group_5 :::"[."::: ) (Set (Var "c")) "," (Set (Var "a")) "," (Set "(" (Set (Var "b")) ($#k2_group_3 :::"|^"::: ) (Set (Var "c")) ")" ) ($#k3_group_5 :::".]"::: ) ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set ($#k3_group_5 :::"[."::: ) (Set (Var "b")) "," (Set (Var "c")) "," (Set "(" (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "b")) ")" ) ($#k3_group_5 :::".]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))))) ; theorem :: GRNILP_1:9 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k8_group_5 :::"[."::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_group_5 :::".]"::: ) ) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set ($#k8_group_5 :::"[."::: ) (Set (Var "B")) "," (Set (Var "A")) ($#k8_group_5 :::".]"::: ) )))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "A", "B" be ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); :: original: :::"[."::: redefine func :::"[.":::"A" "," "B":::".]"::: -> ($#m1_group_2 :::"Subgroup"::: ) "of" "G"; commutativity (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")) "holds" (Bool (Set ($#k8_group_5 :::"[."::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_group_5 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k8_group_5 :::"[."::: ) (Set (Var "B")) "," (Set (Var "A")) ($#k8_group_5 :::".]"::: ) ))) ; end; theorem :: GRNILP_1:10 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "B")) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "A")))) "holds" (Bool (Set ($#k5_group_5 :::"commutators"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "A")))))) ; theorem :: GRNILP_1:11 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "B")) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "A")))) "holds" (Bool (Set ($#k1_grnilp_1 :::"[."::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k1_grnilp_1 :::".]"::: ) ) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "A"))))) ; theorem :: GRNILP_1:12 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "B")) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "A")))) "holds" (Bool (Set ($#k1_grnilp_1 :::"[."::: ) (Set (Var "B")) "," (Set (Var "A")) ($#k1_grnilp_1 :::".]"::: ) ) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "A"))))) ; theorem :: GRNILP_1:13 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "," (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k1_grnilp_1 :::"[."::: ) (Set (Var "H1")) "," (Set "(" ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")) ")" ) ($#k1_grnilp_1 :::".]"::: ) ) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "H2")))) "holds" (Bool (Set ($#k1_grnilp_1 :::"[."::: ) (Set "(" (Set (Var "H1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H")) ")" ) "," (Set (Var "H")) ($#k1_grnilp_1 :::".]"::: ) ) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Set (Var "H2")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H")))))) ; theorem :: GRNILP_1:14 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k1_grnilp_1 :::"[."::: ) (Set (Var "H1")) "," (Set (Var "H2")) ($#k1_grnilp_1 :::".]"::: ) ) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set ($#k1_grnilp_1 :::"[."::: ) (Set (Var "H1")) "," (Set "(" ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")) ")" ) ($#k1_grnilp_1 :::".]"::: ) )))) ; theorem :: GRNILP_1:15 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G"))) "iff" (Bool (Set ($#k1_grnilp_1 :::"[."::: ) (Set (Var "A")) "," (Set "(" ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")) ")" ) ($#k1_grnilp_1 :::".]"::: ) ) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "A"))) ")" ))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); func :::"the_normal_subgroups_of"::: "G" -> ($#m1_hidden :::"set"::: ) means :: GRNILP_1:def 1 (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" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G") ")" )); end; :: deftheorem defines :::"the_normal_subgroups_of"::: GRNILP_1:def 1 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_grnilp_1 :::"the_normal_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 "b2"))) "iff" (Bool (Set (Var "x")) "is" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G"))) ")" )) ")" ))); registrationlet "G" be ($#l3_algstr_0 :::"Group":::); cluster (Set ($#k2_grnilp_1 :::"the_normal_subgroups_of"::: ) "G") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: GRNILP_1:16 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_grnilp_1 :::"the_normal_subgroups_of"::: ) (Set (Var "G"))) (Bool "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) "is" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")))))) ; theorem :: GRNILP_1:17 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k2_grnilp_1 :::"the_normal_subgroups_of"::: ) (Set (Var "G"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_group_3 :::"Subgroups"::: ) (Set (Var "G"))))) ; theorem :: GRNILP_1:18 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_grnilp_1 :::"the_normal_subgroups_of"::: ) (Set (Var "G"))) "holds" (Bool (Set (Var "F")) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_group_3 :::"Subgroups"::: ) (Set (Var "G")))))) ; definitionlet "IT" be ($#l3_algstr_0 :::"Group":::); attr "IT" is :::"nilpotent"::: means :: GRNILP_1:def 2 (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_grnilp_1 :::"the_normal_subgroups_of"::: ) "IT") "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k7_group_2 :::"(Omega)."::: ) "IT")) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) "IT")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "IT" "st" (Bool (Bool (Set (Var "G1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "G2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool "(" (Bool (Set (Var "G2")) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "G1"))) & (Bool (Set (Set (Var "G1")) ($#k5_group_6 :::"./."::: ) (Set "(" "(" (Set (Var "G1")) "," (Set (Var "G2")) ")" ($#k1_group_6 :::"`*`"::: ) ")" )) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set ($#k10_group_5 :::"center"::: ) (Set "(" "IT" ($#k5_group_6 :::"./."::: ) (Set (Var "G2")) ")" ))) ")" )) ")" ) ")" )); end; :: deftheorem defines :::"nilpotent"::: GRNILP_1:def 2 : (Bool "for" (Set (Var "IT")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_grnilp_1 :::"nilpotent"::: ) ) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_grnilp_1 :::"the_normal_subgroups_of"::: ) (Set (Var "IT"))) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "IT")))) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "IT")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "G1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "G2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool "(" (Bool (Set (Var "G2")) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "G1"))) & (Bool (Set (Set (Var "G1")) ($#k5_group_6 :::"./."::: ) (Set "(" "(" (Set (Var "G1")) "," (Set (Var "G2")) ")" ($#k1_group_6 :::"`*`"::: ) ")" )) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set ($#k10_group_5 :::"center"::: ) (Set "(" (Set (Var "IT")) ($#k5_group_6 :::"./."::: ) (Set (Var "G2")) ")" ))) ")" )) ")" ) ")" )) ")" )); 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"::: ) ($#v1_grnilp_1 :::"nilpotent"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; end; theorem :: GRNILP_1:19 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "G1")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N")) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "G1"))) & (Bool (Set (Set (Var "G1")) ($#k5_group_6 :::"./."::: ) (Set "(" "(" (Set (Var "G1")) "," (Set (Var "N")) ")" ($#k1_group_6 :::"`*`"::: ) ")" )) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set ($#k10_group_5 :::"center"::: ) (Set "(" (Set (Var "G")) ($#k5_group_6 :::"./."::: ) (Set (Var "N")) ")" )))) "holds" (Bool (Set ($#k1_grnilp_1 :::"[."::: ) (Set (Var "G1")) "," (Set "(" ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")) ")" ) ($#k1_grnilp_1 :::".]"::: ) ) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "N")))))) ; theorem :: GRNILP_1:20 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "G1")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N")) "is" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "G1"))) & (Bool (Set ($#k1_grnilp_1 :::"[."::: ) (Set (Var "G1")) "," (Set "(" ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")) ")" ) ($#k1_grnilp_1 :::".]"::: ) ) "is" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "N")))) "holds" (Bool (Set (Set (Var "G1")) ($#k5_group_6 :::"./."::: ) (Set "(" "(" (Set (Var "G1")) "," (Set (Var "N")) ")" ($#k1_group_6 :::"`*`"::: ) ")" )) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set ($#k10_group_5 :::"center"::: ) (Set "(" (Set (Var "G")) ($#k5_group_6 :::"./."::: ) (Set (Var "N")) ")" )))))) ; theorem :: GRNILP_1:21 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v1_grnilp_1 :::"nilpotent"::: ) ) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_grnilp_1 :::"the_normal_subgroups_of"::: ) (Set (Var "G"))) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "G2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool "(" (Bool (Set (Var "G2")) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "G1"))) & (Bool (Set ($#k1_grnilp_1 :::"[."::: ) (Set (Var "G1")) "," (Set "(" ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")) ")" ) ($#k1_grnilp_1 :::".]"::: ) ) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "G2"))) ")" )) ")" ) ")" )) ")" )) ; theorem :: GRNILP_1:22 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "," (Set (Var "G1")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "G2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "H")) (Bool "for" (Set (Var "H2")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "H")) "st" (Bool (Bool (Set (Var "G2")) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "G1"))) & (Bool (Set (Set (Var "G1")) ($#k5_group_6 :::"./."::: ) (Set "(" "(" (Set (Var "G1")) "," (Set (Var "G2")) ")" ($#k1_group_6 :::"`*`"::: ) ")" )) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set ($#k10_group_5 :::"center"::: ) (Set "(" (Set (Var "G")) ($#k5_group_6 :::"./."::: ) (Set (Var "G2")) ")" ))) & (Bool (Set (Var "H1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H")))) & (Bool (Set (Var "H2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k3_group_6 :::"/\"::: ) (Set (Var "H"))))) "holds" (Bool (Set (Set (Var "H1")) ($#k5_group_6 :::"./."::: ) (Set "(" "(" (Set (Var "H1")) "," (Set (Var "H2")) ")" ($#k1_group_6 :::"`*`"::: ) ")" )) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set ($#k10_group_5 :::"center"::: ) (Set "(" (Set (Var "H")) ($#k5_group_6 :::"./."::: ) (Set (Var "H2")) ")" )))))))) ; registrationlet "G" be ($#v1_grnilp_1 :::"nilpotent"::: ) ($#l3_algstr_0 :::"Group":::); cluster -> ($#v1_grnilp_1 :::"nilpotent"::: ) for ($#m1_group_2 :::"Subgroup"::: ) "of" "G"; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) -> ($#v1_grnilp_1 :::"nilpotent"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v1_gr_cy_1 :::"cyclic"::: ) -> ($#v1_grnilp_1 :::"nilpotent"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; end; theorem :: GRNILP_1:23 (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) (Bool "for" (Set (Var "A")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "b")) ")" ) ")" ) ($#k13_group_2 :::"*"::: ) (Set "(" (Set (Var "h")) ($#k2_grsolv_1 :::".:"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k13_group_2 :::"*"::: ) (Set (Var "A")) ")" ))) & (Bool (Set (Set "(" (Set "(" (Set (Var "h")) ($#k2_grsolv_1 :::".:"::: ) (Set (Var "A")) ")" ) ($#k14_group_2 :::"*"::: ) (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) ")" ) ($#k5_group_2 :::"*"::: ) (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set "(" (Set (Var "A")) ($#k14_group_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k5_group_2 :::"*"::: ) (Set (Var "b")) ")" ))) ")" ))))) ; theorem :: GRNILP_1:24 (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) (Bool "for" (Set (Var "A")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set ($#k10_group_6 :::"Image"::: ) (Set (Var "h"))) (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k10_group_6 :::"Image"::: ) (Set (Var "h")) ")" ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "b")))) & (Bool (Set (Var "H1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k2_grsolv_1 :::".:"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set "(" (Set (Var "a1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b1")) ")" ) ($#k13_group_2 :::"*"::: ) (Set (Var "H1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "b")) ")" ) ")" ) ($#k13_group_2 :::"*"::: ) (Set "(" (Set (Var "h")) ($#k2_grsolv_1 :::".:"::: ) (Set (Var "A")) ")" ))))))))) ; theorem :: GRNILP_1:25 (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) (Bool "for" (Set (Var "G1")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "G2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "H1")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_6 :::"Subgroup"::: ) "of" (Set ($#k10_group_6 :::"Image"::: ) (Set (Var "h"))) (Bool "for" (Set (Var "H2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_6 :::"Subgroup"::: ) "of" (Set ($#k10_group_6 :::"Image"::: ) (Set (Var "h"))) "st" (Bool (Bool (Set (Var "G2")) "is" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "G1"))) & (Bool (Set (Set (Var "G1")) ($#k5_group_6 :::"./."::: ) (Set "(" "(" (Set (Var "G1")) "," (Set (Var "G2")) ")" ($#k1_group_6 :::"`*`"::: ) ")" )) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set ($#k10_group_5 :::"center"::: ) (Set "(" (Set (Var "G")) ($#k5_group_6 :::"./."::: ) (Set (Var "G2")) ")" ))) & (Bool (Set (Var "H1")) ($#r1_group_2 :::"="::: ) (Set (Set (Var "h")) ($#k2_grsolv_1 :::".:"::: ) (Set (Var "G1")))) & (Bool (Set (Var "H2")) ($#r1_group_2 :::"="::: ) (Set (Set (Var "h")) ($#k2_grsolv_1 :::".:"::: ) (Set (Var "G2"))))) "holds" (Bool (Set (Set (Var "H1")) ($#k5_group_6 :::"./."::: ) (Set "(" "(" (Set (Var "H1")) "," (Set (Var "H2")) ")" ($#k1_group_6 :::"`*`"::: ) ")" )) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set ($#k10_group_5 :::"center"::: ) (Set "(" (Set "(" ($#k10_group_6 :::"Image"::: ) (Set (Var "h")) ")" ) ($#k5_group_6 :::"./."::: ) (Set (Var "H2")) ")" ))))))))) ; theorem :: GRNILP_1:26 (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) (Bool "for" (Set (Var "A")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "h")) ($#k2_grsolv_1 :::".:"::: ) (Set (Var "A"))) "is" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_6 :::"Subgroup"::: ) "of" (Set ($#k10_group_6 :::"Image"::: ) (Set (Var "h"))))))) ; registrationlet "G" be ($#v15_algstr_0 :::"strict"::: ) ($#v1_grnilp_1 :::"nilpotent"::: ) ($#l3_algstr_0 :::"Group":::); let "H" be ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::); let "h" be ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Const "G")) "," (Set (Const "H")); cluster (Set ($#k10_group_6 :::"Image"::: ) "h") -> ($#v1_grnilp_1 :::"nilpotent"::: ) ; end; registrationlet "G" be ($#v15_algstr_0 :::"strict"::: ) ($#v1_grnilp_1 :::"nilpotent"::: ) ($#l3_algstr_0 :::"Group":::); let "N" be ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); cluster (Set "G" ($#k5_group_6 :::"./."::: ) "N") -> ($#v1_grnilp_1 :::"nilpotent"::: ) ; end; theorem :: GRNILP_1:27 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "st" (Bool (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_grnilp_1 :::"the_normal_subgroups_of"::: ) (Set (Var "G"))) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool "for" (Set (Var "G1")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set ($#k1_grnilp_1 :::"[."::: ) (Set (Var "G1")) "," (Set "(" ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")) ")" ) ($#k1_grnilp_1 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )))) ")" ) ")" ))) "holds" (Bool (Set (Var "G")) "is" ($#v1_grnilp_1 :::"nilpotent"::: ) )) ; theorem :: GRNILP_1:28 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "st" (Bool (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_grnilp_1 :::"the_normal_subgroups_of"::: ) (Set (Var "G"))) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "G2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool "(" (Bool (Set (Var "G2")) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "G1"))) & (Bool (Set (Set (Var "G")) ($#k5_group_6 :::"./."::: ) (Set (Var "G2"))) "is" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::)) ")" )) ")" ) ")" ))) "holds" (Bool (Set (Var "G")) "is" ($#v1_grnilp_1 :::"nilpotent"::: ) )) ; theorem :: GRNILP_1:29 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "st" (Bool (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_grnilp_1 :::"the_normal_subgroups_of"::: ) (Set (Var "G"))) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "G2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool "(" (Bool (Set (Var "G2")) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set (Var "G1"))) & (Bool (Set (Set (Var "G")) ($#k5_group_6 :::"./."::: ) (Set (Var "G2"))) "is" ($#v1_gr_cy_1 :::"cyclic"::: ) ($#l3_algstr_0 :::"Group":::)) ")" )) ")" ) ")" ))) "holds" (Bool (Set (Var "G")) "is" ($#v1_grnilp_1 :::"nilpotent"::: ) )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v1_grnilp_1 :::"nilpotent"::: ) -> ($#v1_grsolv_1 :::"solvable"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; end;