Quelle homomorphism_lemmas.prf
Sprache: Lisp
(homomorphism_lemmasnil 3530720894 ("" (rewrite "T1_is_group" ) nil nil )nil homomorphism_lemmas nil )) nil ))nil 3528505895 ("" (rewrite "T2_is_group" ) nil nil )nil homomorphism_lemmas nil )) nil ))nil 3524654775"" (skosimp)"" (inst 1 "one1" )"1" (rewrite "left_coset_one[T1, *, one1]" ) nil nil )"2" (typepred "G!1" )"2" (expand * "group?" "monoid?" "monad?" "subset?" "member" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil )"group[T1, *, one1]" homomorphism_lemmasnil )nil group "algebra/" )"bool" group_def "algebra/" )"T1" homomorphism_lemmas nil )"[T1, T1 -> T1]" homomorphism_lemmas nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil homomorphism_lemmas nil )nil normal_subgroups "algebra/" )"boolean" normal_subgroups "algebra/" )nil cosets "algebra/" )"bool" monoid_def "algebra/" )"bool" sets nil )"bool" monad_def "algebra/" )NOT const-decl "[bool -> bool]" booleans nil ))nil ))nil 3524789060"" (skosimp*)"" (rewrite "left_cosets_group[T1, *, one1]" ) nil nil )) nil )nil factor_groups "algebra/" )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" group_def "algebra/" )nil group "algebra/" )"boolean" normal_subgroups "algebra/" )nil normal_subgroups "algebra/" )nil homomorphism_lemmas nil )"[T1, T1 -> T1]" homomorphism_lemmas nil )"T1" homomorphism_lemmas nil ))nil ))nil 3524654777"" (skosimp*)"" (inst 1 "(LAMBDA (x:(G!1)): *[T1, *, one1](x, K!1))" )"1" (prop)"1" (expand "homomorphism?" )"1" (skosimp*)"1" (rewrite "mult_lem[T1, *, one1]" ) nil nil )) nil ))nil )"2" (expand "surjective?" )"2" (skosimp*)"2" (typepred "y!1" )"2" (skosimp*)"2" (inst 1 "a!1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (decompose-equality 1)"1" (expand "kernel" )"1" (iff)"1" (prop)"1" (typepred "K!1" )"1" (expand "normal_subgroup?" )"1" (flatten)"1" (expand "subgroup?" )"1" (expand * "subset?" "member" )"1" (inst -2 "x!1" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (decompose-equality 1)"2" (expand "*" )"2" (iff)"2" (prop)"1" (skosimp)"1" (replaces -1)"1" (typepred "h!1" "K!1" )"1" expand * "group?" "monoid?" "monad?" )"1" "1" "1" expand "star_closed?" )"1" "1" expand "member" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst 1 "inv[T1, *, one1](x!1) * x!2" )"1" (rewrite "assoc[T1, *, one1]" )"1" (rewrite "inv_right[T1, *, one1]" )"1" rewrite "one_left[T1, *, one1]" )nil nil ))nil ))nil )"2" (typepred "K!1" )"2" (expand * "group?" "monoid?" "monad?" )"2" "2" "2" expand * "star_closed?" "member" )"2" "inv_in[T1, *, one1]" )"2" "K!1" "x!1" )"2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (expand "*" )"3" (decompose-equality -2)"3" (inst?)"3" (iff)"3" (prop)"3" (inst 2 "one1" )"1" (rewrite "one_right[T1, *, one1]" )nil nil )"2" (typepred "K!1" )"2" expand * "group?" "monoid?" "monad?" )"2" "2" expand "member" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "left_cosets_group[T1, *, one1]" ) nil nil )"3" (rewrite "T1_is_group" ) nil nil )"4" (inst 1 "one1" )"1" (rewrite "left_coset_one[T1, *, one1]" ) nil nil )"2" (typepred "G!1" )"2" (expand * "group?" "monoid?" "monad?" "member" )"2" (assert ) nil nil )) nil ))nil ))nil )"5" (expand "homomorphism?" )"5" (skosimp*)"5" (rewrite "mult_lem[T1, *, one1]" ) nil nil )) nil ))nil )"6" (skosimp*)"6" (prop)"1" (inst 1 "x!1" ) nil nil ) ("2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (prop)"1" (inst 1 "x!1" ) nil nil ) ("2" (grind) nil nil )) nil ))nil ))nil ))nil )"group[left_cosets(G, N), mult(G, N), N]" nil )"left_cosets(G, H)" factor_groups "algebra/" )nil cosets "algebra/" )"normal_subgroup[T1, *, one1](G!1)" nil )nil normal_subgroups "algebra/" )"boolean" normal_subgroups "algebra/" )"set[T]" cosets "algebra/" )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )"group[T1, *, one1]" homomorphism_lemmasnil )nil group "algebra/" )"bool" group_def "algebra/" )"T1" homomorphism_lemmas nil )"[T1, T1 -> T1]" homomorphism_lemmas nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil homomorphism_lemmas nil )"set" sets nil )nil homomorphisms "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"subgroup[T1, *, one1](G)" homomorphisms"algebra/" )nil group "algebra/" )"{y | x * y = one AND y * x = one}" group"algebra/" )"T1" homomorphism_lemmas nil )"T1" homomorphism_lemmas nil )nil group "algebra/" )nil group "algebra/" )nil group "algebra/" )nil group "algebra/" )"bool" groupoid_def "algebra/" )"bool" monad_def "algebra/" )"bool" monoid_def "algebra/" )"bool" sets nil )"bool" sets nil )nil factor_groups "algebra/" )nil homomorphism_lemmas nil )nil cosets "algebra/" )"R" restrict nil )"setofsets[T]" right_left_cosets nil )"bool" functions nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" homomorphisms "algebra/" )nil factor_groups "algebra/" ))nil 3524504949"" (skosimp*)"" (typepred "x!1" )"" (rewrite "inv_in[T1, *, one1]" ) nil nil )) nil ))nil )nil group "algebra/" )"bool" group_def "algebra/" )"T1" homomorphism_lemmas nil )"[T1, T1 -> T1]" homomorphism_lemmas nil )set type-eq-decl nil sets nil )nil homomorphism_lemmas nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil group "algebra/" ))nil ))nil 3524504972"" (skosimp*)"" (lemma "inv_left[T1, *, one1]" )"" (lemma "inv_right[T1, *, one1]" )"" (inst?)"" (inst?)"" (typepred "phi!1" )"" (expand "homomorphism?" )"" (copy -1)"" (inst -1 "x!1" "inv[T1, *, one1](x!1)" )"1" (inst -2 "inv[T1, *, one1](x!1)" "x!1" )"1" (replaces -3)"1" (replaces -3)"1" (lemma "homo_one[T1,*,one1,T2,o,one2]" )"1" (inst -1 "G!1" "GP!1" "phi!1" )"1" "1" "unique_inv[T2, o, one2]" )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "inv_in[T1, *, one1]" ) nil nil ))nil )"2" (rewrite "inv_in[T1, *, one1]" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"T1" homomorphism_lemmas nil )"[T1, T1 -> T1]" homomorphism_lemmas nil )nil homomorphism_lemmas nil )nil group "algebra/" )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" group_def "algebra/" )nil group "algebra/" )nil homomorphisms "algebra/" )"bool" homomorphisms "algebra/" )"T2" homomorphism_lemmas nil )"[T2, T2 -> T2]" homomorphism_lemmas nil )nil homomorphism_lemmas nil )NOT const-decl "[bool -> bool]" booleans nil )nil group "algebra/" )nil homomorphisms "algebra/" )nil group "algebra/" )"(G!1)" homomorphism_lemmas nil )"{y | x * y = one AND y * x = one}" group"algebra/" )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )"group[T1, *, one1]" homomorphism_lemmasnil )nil group "algebra/" ))nil 3524504993"" (skeep)"" (skoletin* 1)"" (expand "normal_subgroup?" )"" (assert )"" (skeep)"" (expand "subset?" )"" (skeep)"" (expand "member" )"" (expand "K" 1)"" (grind)"1" (typepred "phi" )"1" (expand "homomorphism?" )"1" (copy -1)"1" "inv[T1, *, one1](a) * h!2" "a" )"1" "1" "inv[T1, *, one1](a)" "h!2" )"1" "1" "1" "one_right[T2, o, one2]" )"1" "1" "1" rewrite "homo_inv" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "a" )"2" rewrite "inv_in[T1, *, one1]" )nil nil ))nil ))nil ))nil ))nil )"2" "2" "a" )"2" "inv_in[T1, *, one1]" )"2" "2" "G" )"2" expand "group?" )"2" "2" expand "monoid?" )"2" "2" expand "monad?" )"2" "2" expand "star_closed?" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" (typepred "a" )"2" (lemma "inv_in[T1, *, one1]" )"2" (inst?)"2" "G" )"2" expand "group?" )"2" "2" expand "monoid?" )"2" "2" expand "monad?" )"2" "2" expand "star_closed?" )"2" "2" "2" "inv[T1, *, one1](a)" "h!2" )"2" expand "member" )"2" "inv[T1, *, one1](a) * h!2" "a" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[bool, bool -> bool]" booleans nil )nil homomorphism_lemmas nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"[T, T -> boolean]" equalities nil )"[T1, T1 -> T1]" homomorphism_lemmas nil )"T1" homomorphism_lemmas nil )"bool" group_def "algebra/" )nil group "algebra/" )nil homomorphism_lemmas nil )"[T2, T2 -> T2]" homomorphism_lemmas nil )"T2" homomorphism_lemmas nil )"bool" homomorphisms "algebra/" )nil homomorphisms "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"subgroup[T1, *, one1](G)" homomorphisms"algebra/" )"boolean" normal_subgroups "algebra/" )"bool" sets nil )"bool" sets nil )"set[T]" cosets "algebra/" )NOT const-decl "[bool -> bool]" booleans nil )"set[T]" cosets "algebra/" )AND const-decl "[bool, bool -> bool]" booleans nil )"{y | x * y = one AND y * x = one}" group"algebra/" )"group[T1, *, one1]" homomorphism_lemmas nil )"(G)" homomorphism_lemmas nil )"group[T2, o, one2]" homomorphism_lemmas nil )"homomorphism[T1, *, one1, T2, o, one2](G, GP)" nil )"(kernel(G, GP)(phi))" homomorphism_lemmasnil )nil homomorphism_lemmas nil )nil group "algebra/" )nil group "algebra/" )"bool" monoid_def "algebra/" )"bool" monad_def "algebra/" )"bool" groupoid_def "algebra/" )"(kernel(G, GP)(phi))" homomorphism_lemmasnil )"subgroup[T1, *, one1](G)" homomorphism_lemmasnil ))nil 3524526933"" (skosimp*)"" (lemma "subgroup_def[T2, o, one2]" )"" (inst?)"" (assert )"" (hide 2)"" (prop)"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (expand "member" )"1" (expand "extend" )"1" (inst -1 "one2" )"1" (typepred "GP!1" )"1" (expand "group?" )"1" (flatten)"1" expand "monoid?" )"1" "1" expand "monad?" )"1" "1" "1" expand "member" )"1" assert )"1" expand "image" )"1" "one1" )"1" rewrite "homo_one[T1, *, one1,T2, o, one2]" )nil nil )"2" "1" "G!1" )"1" expand "group?" )"1" "1" expand "monoid?" )"1" "1" expand "monad?" )"1" "1" expand "member" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "restrict" )"2" "H!1" )"2" expand "group?" )"2" "2" expand "monoid?" )"2" "2" expand "monad?" )"2" "2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "subset?" )"2" (skosimp*)"2" (expand "member" )"2" (expand "extend" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (expand "star_closed?" )"3" (skosimp*)"3" (expand "member" )"3" (expand "extend" )"3" (prop)"1" (typepred "x!1" )"1" (typepred "y!1" )"1" (expand "extend" )"1" "1" expand "image" )"1" "1" "1" "x!2 * x!3" )"1" "phi!1" )"1" expand "homomorphism?" )"1" "x!2" "x!3" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" "1" "x!2" )"1" "x!3" )"1" "G!1" )"1" expand "group?" )"1" "1" expand "monoid?" )"1" "1" expand "monad?" )"1" "1" "1" expand "star_closed?" )"1" "1" expand "member" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "restrict" )"2" "x!2" )"2" "x!3" )"2" "H!1" )"2" expand "group?" )"2" "2" expand "monoid?" )"2" "2" expand "monad?" )"2" "2" "2" expand *"restrict" "star_closed?" "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "GP!1" )"2" (expand "group?" )"2" (flatten)"2" expand "monoid?" )"2" "2" expand "monad?" )"2" "2" "x!1" )"2" "y!1" )"2" expand *"extend" "star_closed?" "member" "image" )"2" "2" "2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (expand "inv_closed?" )"4" (skosimp*)"4" (expand * "member" "extend" "image" "restrict" )"4" (prop)"1" (typepred "x!1" )"1" (expand * "extend" "image" "restrict" )"1" (prop)"1" (skosimp)"1" "x!2" )"1" "inv[T1, *, one1](x!2)" )"1" rewrite "homo_inv" )"1" (assert ) nil nil ))nil )"2" "1" "1" rewrite "inv_in" )nil nil ))nil )"2" expand "restrict" )"2" "2" rewrite "inv_in" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "x!1" )"2" (expand "extend" )"2" (prop)"2" (rewrite "inv_in" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"T2" homomorphism_lemmas nil )"[T2, T2 -> T2]" homomorphism_lemmas nil )nil homomorphism_lemmas nil )nil group "algebra/" )"(partial_order?[set[T]])" nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )nil homomorphisms "algebra/" )"subgroup[T1, *, one1](G!1)" nil )"group[T1, *, one1]" homomorphism_lemmasnil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" monad_def "algebra/" )"bool" monoid_def "algebra/" )"bool" sets nil )"bool" sets nil )"bool" sets nil )"(extend[T2, (GP!1), bool, FALSE] " nil )"(extend[T2, (GP!1), bool, FALSE] " nil )"homomorphism[T1, *, one1, T2, o, one2](G!1, GP!1)" nil )"group[T2, o, one2]" homomorphism_lemmasnil )"(restrict[T1, (G!1), boolean](H!1))" nil )"(restrict[T1, (G!1), boolean](H!1))" nil )"bool" groupoid_def "algebra/" )"[T, T -> boolean]" equalities nil )"{y | x * y = one AND y * x = one}" group"algebra/" )"(restrict[T1, (G!1), boolean](H!1))" nil )nil homomorphism_lemmas nil )nil group "algebra/" )"bool" group "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )"R" restrict nil )nil homomorphisms "algebra/" )"bool" homomorphisms "algebra/" )"set[R]" function_image nil )"T1" homomorphism_lemmas nil )"[T1, T1 -> T1]" homomorphism_lemmas nil )nil homomorphism_lemmas nil )"R" extend nil )"bool" booleans nil )nil group "algebra/" )"bool" group_def "algebra/" )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil ))nil 3530914988"" (skosimp*)"" (lemma "homo_image" )"" (inst?)"1" (lemma "subgroup_is_group[T2, o, one2]" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil )"2" (hide 2)"2" (typepred "H!1" )"2" (expand "normal_subgroup?" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil homomorphism_lemmas nil )NOT const-decl "[bool -> bool]" booleans nil )nil group "algebra/" )"bool" booleans nil )"R" extend nil )"set[R]" function_image nil )"R" restrict nil )nil group "algebra/" )nil homomorphisms "algebra/" )"bool" homomorphisms "algebra/" )"T2" homomorphism_lemmas nil )"[T2, T2 -> T2]" homomorphism_lemmas nil )nil homomorphism_lemmas nil )nil homomorphism_lemmas nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"[T1, T1 -> T1]" homomorphism_lemmas nil )"T1" homomorphism_lemmas nil )"bool" group_def "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"boolean" normal_subgroups "algebra/" )"group[T1, *, one1]" homomorphism_lemmasnil )nil normal_subgroups "algebra/" )"normal_subgroup[T1, *, one1](G!1)" nil ))nil ))nil 3530915201"" (skosimp*)"" (typepred "H!1" )"" (hide -1)"" (expand "normal_subgroup?" )"" (flatten)"" (lemma "homo_image" )"" (inst?)"" (assert )"" (hide -1)"" (expand * "subset?" "member" )"" (skosimp*)"" (expand "extend" 1)"" (prop)"1" (expand "surjective?" )"1" expand "*" -5)"1" "1" "h!1" )"1" "1" "1" "h!2" )"1" expand "extend" )"1" "1" expand "image" )"1" "1" "a!1" )"1" "1" "inv[T1, *, one1](x!3) * x!2 * x!3" )"1" "1" "phi!1" )"1" expand "homomorphism?" )"1" "inv[T1, *, one1](x!3) * x!2" "x!3" )"1" "inv[T1, *, one1](x!3)" "x!2" )"1" "1" "1" "homo_inv[T1, *, one1,T2, o, one2]" )"1" "1" "1" "1" replace "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "inv_in" )nil nil ))nil ))nil )"2" "2" rewrite "product_in[T1, *, one1]" )"2" "2" rewrite "inv_in" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" "1" rewrite "product_in[T1, *, one1]" )"1" "1" rewrite "product_in[T1, *, one1]" )"1" "1" rewrite "inv_in" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "restrict" )"2" "2" "x!2" )"2" expand "restrict" )"2" "2" "x!3" )"2" "inv[T1, *, one1](x!3) * x!2 * x!3" )"2" assert )"2" "2" expand "*" )"2" "inv[T1, *, one1](x!3) * x!2" )"2" "x!2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 -2 -3))"2" expand "*" )"2" "2" "h!1" "a!1" )"2" "2" "2" "h!2" )"2" expand "extend" )"2" "2" "2" "2" rewrite "product_in[T2, o, one2]" )"2" "2" rewrite "product_in[T2, o, one2]" )"2" "2" rewrite "inv_in" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil normal_subgroups "algebra/" )"boolean" normal_subgroups "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )"T1" homomorphism_lemmas nil )"[T1, T1 -> T1]" homomorphism_lemmas nil )set type-eq-decl nil sets nil )nil homomorphism_lemmas nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil homomorphism_lemmas nil )"bool" sets nil )"bool" sets nil )"R" extend nil )"bool" functions nil )nil group "algebra/" )nil homomorphism_lemmas nil )nil group "algebra/" )"(restrict[T1, (G!1), boolean](H!1))" nil )"(G!1)" homomorphism_lemmas nil )"{y | x * y = one AND y * x = one}" group"algebra/" )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"R" restrict nil )"set[R]" function_image nil )"bool" booleans nil )"set[T]" cosets "algebra/" )"set[T]" cosets "algebra/" )nil group "algebra/" )nil homomorphisms "algebra/" )"bool" homomorphisms "algebra/" )"T2" homomorphism_lemmas nil )"[T2, T2 -> T2]" homomorphism_lemmas nil )nil homomorphism_lemmas nil )"bool" group_def "algebra/" )"group[T1, *, one1]" homomorphism_lemmasnil )"normal_subgroup[T1, *, one1](G!1)" nil ))nil 3530878347"" (skosimp*)"" (lemma "subgroup_def[T1, *, one1]" )"" (inst?)"" (assert )"" (hide 2)"" (prop)"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (expand "member" )"1" (expand "extend" )"1" (inst -1 "one1" )"1" (typepred "G!1" )"1" (expand "group?" )"1" (flatten)"1" expand "monoid?" )"1" "1" expand "monad?" )"1" "1" "1" expand *"inverse_image" "member" )"1" assert )"1" "K!1" )"1" "1" expand "group?" )"1" "1" expand "monoid?" )"1" "1" expand "monad?" )"1" "1" "1" expand "member" )"1" rewrite "homo_one[T1, *, one1,T2, o, one2]" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "subset?" )"2" (skosimp*)"2" (expand "member" )"2" (expand "extend" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (expand "star_closed?" )"3" (skosimp*)"3" (expand "member" )"3" (expand "extend" )"3" (typepred "x!1" )"3" (typepred "y!1" )"3" (expand "extend" )"3" (expand "inverse_image" )"3" expand "member" )"3" "1" "1" "phi!1" )"1" expand "homomorphism?" )"1" "x!1" "y!1" )"1" "1" "K!1" )"1" "1" expand "group?" )"1" "1" expand "monoid?" )"1" "1" expand "monad?" )"1" "1" "1" expand *"star_closed?" "member" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "product_in[T1, *, one1]" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (expand "inv_closed?" )"4" (skosimp*)"4" (expand * "extend" "inverse_image" "member" )"4" (typepred "x!1" )"4" (expand * "extend" "inverse_image" "member" )"4" (prop)"1" (hide (-1 -2))"1" (rewrite "homo_inv" )"1" rewrite "inv_in[T2, o, one2]" )nil nil ))nil ))nil )"2" (hide -2)"2" (rewrite "inv_in[T1, *, one1]" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"T1" homomorphism_lemmas nil )"[T1, T1 -> T1]" homomorphism_lemmas nil )nil homomorphism_lemmas nil )nil group "algebra/" )"(partial_order?[set[T]])" nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )nil homomorphisms "algebra/" )"bool" monad_def "algebra/" )"bool" monoid_def "algebra/" )"bool" sets nil )"bool" sets nil )"bool" sets nil )"(extend[T1, (G!1), bool, FALSE](inverse_image(phi!1, K!1)))" nil )"(extend[T1, (G!1), bool, FALSE](inverse_image(phi!1, K!1)))" nil )"homomorphism[T1, *, one1, T2, o, one2](G!1, GP!1)" nil )"group[T1, *, one1]" homomorphism_lemmasnil )"subgroup[T2, o, one2](GP!1)" nil )"group[T2, o, one2]" homomorphism_lemmasnil )nil group "algebra/" )"bool" groupoid_def "algebra/" )nil homomorphism_lemmas nil )nil group "algebra/" )"bool" group "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )nil homomorphisms "algebra/" )"bool" homomorphisms "algebra/" )"T2" homomorphism_lemmas nil )"[T2, T2 -> T2]" homomorphism_lemmas nil )"set[D]" function_image nil )nil homomorphism_lemmas nil )"R" extend nil )"bool" booleans nil )nil group "algebra/" )"bool" group_def "algebra/" )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil ))nil 3530920596"" (skosimp*)"" (lemma "homo_inv_image" )"" (inst?)"1" (lemma "subgroup_is_group[T1, *, one1]" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil )"2" (hide 2)"2" (typepred "K!1" )"2" (expand "normal_subgroup?" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil homomorphism_lemmas nil )NOT const-decl "[bool -> bool]" booleans nil )nil group "algebra/" )"bool" booleans nil )"R" extend nil )"set[D]" function_image nil )nil group "algebra/" )nil homomorphisms "algebra/" )"bool" homomorphisms "algebra/" )"T1" homomorphism_lemmas nil )"[T1, T1 -> T1]" homomorphism_lemmas nil )nil homomorphism_lemmas nil )nil homomorphism_lemmas nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"[T2, T2 -> T2]" homomorphism_lemmas nil )"T2" homomorphism_lemmas nil )"bool" group_def "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"boolean" normal_subgroups "algebra/" )"group[T2, o, one2]" homomorphism_lemmasnil )nil normal_subgroups "algebra/" )"normal_subgroup[T2, o, one2](GP!1)" nil ))nil ))nil 3530920597"" (skosimp*)"" (typepred "K!1" )"" (hide -1)"" (expand "normal_subgroup?" )"" (flatten)"" (lemma "homo_inv_image" )"" (inst?)"" (assert )"" (hide -1)"" (expand * "subset?" "member" )"" (skosimp*)"" (expand "extend" 1)"" (prop)"1" (expand "inverse_image" )"1" expand "member" )"1" expand "*" -4)"1" "1" "h!1" )"1" "1" "1" "h!2" )"1" expand "extend" )"1" "1" "phi!1(a!1)" )"1" "phi!1(x!1)" )"1" assert )"1" "1" expand "*" )"1" "inv[T2, o, one2](phi!1(a!1)) o phi!1(h!2)" )"1" "1" "1" "phi!1" )"1" expand "homomorphism?" )"1" "inv[T1, *, one1](a!1) * h!2" "a!1" )"1" "inv[T1, *, one1](a!1)" "h!2" )"1" "1" "1" "homo_inv[T1, *, one1,T2, o, one2]" )"1" "1" nil nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "inv_in" )nil nil ))nil ))nil )"2" "2" rewrite "product_in[T1, *, one1]" )"2" "2" rewrite "inv_in" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 -2))"2" expand "*" )"2" "2" "h!1" "a!1" )"2" "2" "h!2" )"2" expand "extend" )"2" "2" "2" "2" "2" rewrite "product_in[T1, *, one1]" )"2" "2" rewrite "product_in[T1, *, one1]" )"2" "2" rewrite "inv_in" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil normal_subgroups "algebra/" )"boolean" normal_subgroups "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )"T2" homomorphism_lemmas nil )"[T2, T2 -> T2]" homomorphism_lemmas nil )set type-eq-decl nil sets nil )nil homomorphism_lemmas nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil homomorphism_lemmas nil )"bool" sets nil )"bool" sets nil )"R" extend nil )"set[D]" function_image nil )"set[T]" cosets "algebra/" )"set[T]" cosets "algebra/" )"bool" booleans nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )"{y | x * y = one AND y * x = one}" group"algebra/" )nil group "algebra/" )nil homomorphism_lemmas nil )nil group "algebra/" )"(extend[T1, (G!1), bool, FALSE]({x: (G!1) | K!1(phi!1(x))}))" nil )"(G!1)" homomorphism_lemmas nil )"homomorphism[T1, *, one1, T2, o, one2](G!1, GP!1)" nil )"group[T1, *, one1]" homomorphism_lemmasnil )nil group "algebra/" )nil homomorphisms "algebra/" )"bool" homomorphisms "algebra/" )"T1" homomorphism_lemmas nil )"[T1, T1 -> T1]" homomorphism_lemmas nil )nil homomorphism_lemmas nil )"bool" group_def "algebra/" )"group[T2, o, one2]" homomorphism_lemmasnil )"normal_subgroup[T2, o, one2](GP!1)" nil ))nil 3530890201"" (skosimp*)"" (skoletin* 1 "!1" )"" (expand * "subset?" "member" )"" (skosimp)"" (expand "extend" )"" (typepred "K!1" )"" (expand "subgroup?" )"" (expand "subset?" )"" (inst?)"" (assert )"" (expand "inverse_image" )"" (expand "member" )"" (replaces -4)"" (expand "kernel" )"" "" "S!1" )"" expand "group?" )"" "" expand "monoid?" )"" "" expand "monad?" )"" "" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[bool, bool -> bool]" booleans nil )nil homomorphism_lemmas nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"[T, T -> boolean]" equalities nil )"[T1, T1 -> T1]" homomorphism_lemmas nil )"T1" homomorphism_lemmas nil )"bool" group_def "algebra/" )nil group "algebra/" )nil homomorphism_lemmas nil )"[T2, T2 -> T2]" homomorphism_lemmas nil )"T2" homomorphism_lemmas nil )"bool" homomorphisms "algebra/" )nil homomorphisms "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"subgroup[T1, *, one1](G)" homomorphisms"algebra/" )"set[D]" function_image nil )"R" extend nil )"bool" booleans nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" monad_def "algebra/" )"bool" monoid_def "algebra/" )"bool" sets nil ))nil 3530891648"" (skosimp*)"" (skoletin* 1 "!1" )"" (decompose-equality 1)"" (iff)"" (prop)"1" expand * "inverse_image" "image" "prod" "member" "restrict" )"1" (skosimp)"1" (lemma "cancel_left[T2,o,one2]" )"1" "phi!1(x!1)" "phi!1(x!2)" "inv[T2, o, one2](phi!1(x!2))" )"1" (prop)"1" (hide -2)"1" (rewrite "inv_left" )"1" (rewrite "homo_inv" :dir rl)"1" (typepred "phi!1" )"1" expand "homomorphism?" )"1" "1" "1" "x!2" )"1" "1" expand "restrict" )"1" "x!2" "inv[T1, *, one1](x!2) * x!1" )"1" rewrite "assoc[T1, *, one1]" )"1" rewrite "inv_right[T1, *, one1]" )"1" rewrite "one_left[T1, *, one1]" )nil nil ))nil ))nil )"2" "2" "2" expand "kernel" )"2" assert )"2" "2" rewrite "product_in[T1, *, one1]" )"2" "2" rewrite "inv_in[T1, *, one1]" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (rewrite "T2_is_group" ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" expand * "inverse_image" "image" "prod" "member" "restrict" )"2" (skosimp)"2" (inst 1 "h!1" )"1" (replaces -1)"1" (typepred "k!1" )"1" (replaces -2)"1" (expand "kernel" )"1" (flatten)"1" (typepred "phi!1" )"1" expand "homomorphism?" )"1" "1" "1" "1" rewrite "one_right[T2, o, one2]" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "h!1" )"2" (expand "restrict" )"2" (typepred "H!1" )"2" (hide (-1 -4 -5))"2" (expand "subgroup?" )"2" (expand "subset?" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[bool, bool -> bool]" booleans nil )nil homomorphism_lemmas nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"[T, T -> boolean]" equalities nil )"[T1, T1 -> T1]" homomorphism_lemmas nil )"T1" homomorphism_lemmas nil )"bool" group_def "algebra/" )nil group "algebra/" )nil homomorphism_lemmas nil )"[T2, T2 -> T2]" homomorphism_lemmas nil )"T2" homomorphism_lemmas nil )"bool" homomorphisms "algebra/" )nil homomorphisms "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"subgroup[T1, *, one1](G)" homomorphisms"algebra/" )"set[T]" products_subgroups nil )"R" restrict nil )"set[R]" function_image nil )"set[D]" function_image nil )"(H!1)" homomorphism_lemmas nil )nil group "algebra/" )"bool" sets nil )"bool" sets nil )nil group "algebra/" )nil group "algebra/" )NOT const-decl "[bool -> bool]" booleans nil )nil group "algebra/" )nil group "algebra/" )nil group "algebra/" )nil group "algebra/" )nil group "algebra/" )"(G!1)" homomorphism_lemmas nil )"subgroup[T1, *, one1](G!1)" nil )"(restrict[T1, (G!1), boolean](H!1))" nil )"subgroup[T1, *, one1](G!1)" nil )"group[T1, *, one1]" homomorphism_lemmasnil )nil homomorphism_lemmas nil )AND const-decl "[bool, bool -> bool]" booleans nil )"{y | x * y = one AND y * x = one}" group"algebra/" ))nil 3530893730"" (skosimp*)"" (skoletin* 1 "!1" )"" (lemma "homo_inv_image_image" )"" (inst?)"" (assert )"" (replaces -1)"" (prop)"1" (expand * "subgroup?" "subset?" "member" )"1" (skosimp)"1" (decompose-equality -1)"1" (inst?)"1" (iff)"1" (prop)"1" (expand "restrict" )"1" (propax) nil nil )) nil )"2" (expand "restrict" )"2" expand "prod" )"2" "one1" "x!1" )"1" rewrite "one_left[T1,*,one1]" )nil nil )"2" (assert ) nil nil )"3" "H!1" )"3" expand *"group?" "monoid?" "monad?" )"3" "3" "3" expand "member" )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replaces -2)"2" (expand "kernel" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (decompose-equality 1)"2" (iff)"2" (prop)"1" (expand "restrict" )"1" (expand "prod" )"1" (skosimp)"1" expand * "subgroup?" "subset?" "member" )"1" "k!1" )"1" assert )"1" "1" "1" "h!1" )"1" rewrite "product_in[T1, *, one1]" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "restrict" )"2" (expand "prod" )"2" (inst 1 "x!1" "one1" )"1" (rewrite "one_right[T1,*,one1]" ) nil nil )"2" (hide-all-but 1)"2" expand "kernel" )"2" "G!1" )"2" expand *"group?" "monoid?" "monad?" )"2" "2" "2" expand "member" )"2" assert )"2" rewrite "homo_one[T1, *, one1,T2, o, one2]" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[bool, bool -> bool]" booleans nil )nil homomorphism_lemmas nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"[T, T -> boolean]" equalities nil )"[T1, T1 -> T1]" homomorphism_lemmas nil )"T1" homomorphism_lemmas nil )"bool" group_def "algebra/" )nil group "algebra/" )nil homomorphism_lemmas nil )"[T2, T2 -> T2]" homomorphism_lemmas nil )"T2" homomorphism_lemmas nil )"bool" homomorphisms "algebra/" )nil homomorphisms "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"subgroup[T1, *, one1](G)" homomorphisms"algebra/" )"R" restrict nil )"set[R]" function_image nil )"set[D]" function_image nil )nil group "algebra/" )nil homomorphisms "algebra/" )nil group "algebra/" )"(G!1)" homomorphism_lemmas nil )"bool" sets nil )"bool" sets nil )"set[T]" products_subgroups nil )"subgroup[T1, *, one1](G!1)" nil )"group[T2, o, one2]" homomorphism_lemmasnil )"homomorphism[T1, *, one1, T2, o, one2](G!1, GP!1)" nil )nil group "algebra/" )"bool" monoid_def "algebra/" )"bool" monad_def "algebra/" )NOT const-decl "[bool -> bool]" booleans nil )"T1" homomorphism_lemmas nil )"group[T1, *, one1]" homomorphism_lemmasnil )nil homomorphism_lemmas nil ))nil 3524797513"" (skosimp*)"" (lemma "kernel_normal[T1, *, one1,T2, o, one2]" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil )nil homomorphism_lemmas nil )nil homomorphisms "algebra/" )"bool" homomorphisms "algebra/" )"T2" homomorphism_lemmas nil )"[T2, T2 -> T2]" homomorphism_lemmas nil )nil homomorphism_lemmas nil )nil group "algebra/" )"bool" group_def "algebra/" )"T1" homomorphism_lemmas nil )"[T1, T1 -> T1]" homomorphism_lemmas nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil homomorphism_lemmas nil ))nil ))nil 3524797513"" (skosimp*)"" (lemma "homo_image[T1, *, one1,T2, o, one2]" )"" (inst?)"1" (expand "subgroup?" ) (("1" (assert ) nil nil )) nil )"2" (hide (-1 2))"2" (rewrite "group_is_subgroup[T1, *, one1]" ) nil nil ))nil ))nil ))nil ))nil )nil homomorphism_lemmas nil )nil group "algebra/" )"(partial_order?[set[T]])" nil )nil group "algebra/" )nil homomorphisms "algebra/" )"bool" homomorphisms "algebra/" )"T2" homomorphism_lemmas nil )"[T2, T2 -> T2]" homomorphism_lemmas nil )nil homomorphism_lemmas nil )nil homomorphism_lemmas nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"[T1, T1 -> T1]" homomorphism_lemmas nil )"T1" homomorphism_lemmas nil )"bool" group_def "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"group[T1, *, one1]" homomorphism_lemmasnil ))nil ))nil 3524797513"" (skosimp*)"" (inst 1 "one1" )"1" (rewrite "left_coset_one" ) nil nil )"2" (typepred "G!1" )"2" (expand "group?" )"2" (flatten)"2" (expand "monoid?" )"2" (flatten)"2" (expand "monad?" )"2" (flatten)"2" (expand "member" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"group[T1, *, one1]" homomorphism_lemmasnil )nil group "algebra/" )"bool" group_def "algebra/" )"T1" homomorphism_lemmas nil )"[T1, T1 -> T1]" homomorphism_lemmas nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil homomorphism_lemmas nil )nil group "algebra/" )"bool" group_def "algebra/" )nil cosets "algebra/" )"bool" monoid_def "algebra/" )"bool" monad_def "algebra/" )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil ))nil ))nil 3530924567"" (skosimp*)"" (lemma "left_cosets_group[T1, *, one1]" )"" (inst?)"" (hide 2)"" (lemma "kernel_normal" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"T1" homomorphism_lemmas nil )"[T1, T1 -> T1]" homomorphism_lemmas nil )nil homomorphism_lemmas nil )nil factor_groups "algebra/" )nil homomorphisms "algebra/" )"bool" homomorphisms "algebra/" )"T2" homomorphism_lemmas nil )"[T2, T2 -> T2]" homomorphism_lemmas nil )nil homomorphism_lemmas nil )nil homomorphism_lemmas nil )"group[T1, *, one1]" homomorphism_lemmasnil )"subgroup[T1, *, one1](G!1)" nil )nil group "algebra/" )"bool" group_def "algebra/" )nil normal_subgroups "algebra/" )"boolean" normal_subgroups "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil ))nil ))nil 3524797650"" (skosimp*)"" (skoletin* 1)"1" (expand "isomorphic?" )"1" "(LAMBDA (A: left_cosets(G!1,K)): phi!1(lc_gen(G!1,K,A)))" )"1" (expand "isomorphism?" )"1" (prop)"1" (expand "bijective?" )"1" (prop)"1" (expand "injective?" )"1" (skosimp*)"1" (expand "restrict" )"1" (lemma "lc_is_eq[T1, *, one1]" )"1" "G!1" "K" "lc_gen(G!1, K, x1!1)" "lc_gen(G!1, K, x2!1)" )"1" (assert )"1" "inv[T1, *, one1](lc_gen(G!1, K, x2!1)) * lc_gen(G!1, K, x1!1)" )"1" "inv_right[T1, *, one1]" )"1" "1" rewrite "assoc[T1, *, one1]" )"1" "1" rewrite "one_left[T1,*,one1]" )nil nil ))nil ))nil ))nil ))nil )"2" expand "K" 1)"2" expand "kernel" 1 1)"2" "1" replace -2 1 rl)"1" "1" "lc_gen[T1, *, one1](G!1, K, x2!1)" )"1" "lc_gen[T1, *, one1](G!1, K, x1!1)" )"1" "1" "inv_in[T1, *, one1]" )"1" "G!1" "lc_gen[T1, *, one1](G!1, K, x2!1)" )"1" "G!1" )"1" expand "group?" )"1" "1" expand "monoid?" )"1" "1" expand "monad?" )"1" "1" "1" expand "star_closed?" )"1" "1" expand "member" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "phi!1" )"2" expand "homomorphism?" )"2" "1" rewrite "homo_inv" )"1" replace -3 * rl)"1" "1" rewrite "inv_left[T2, o, one2]" )nil nil ))nil ))nil ))nil )"2" "2" replace -1 1 rl)"2" "lc_gen[T1, *, one1](G!1, K, x2!1)" )"2" rewrite "inv_in[T1, *, one1]" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "surjective?" )"2" (skosimp*)"2" (typepred "y!1" )"2" (expand "extend" -1)"2" (prop)"2" (expand "image" )"2" "2" "*[T1, *, one1](x!1, K)" )"1" expand "restrict" )"1" "lc_gen(G!1, K, *[T1, *, one1](x!1, K))" )"1" "lc_eq[T1, *, one1]" )"1" "G!1" "K" "x!1" "lc_gen(G!1, K, *[T1, *, one1](x!1, K))" )"1" assert )"1" "1" "h!1" )"1" expand "K" -1)"1" expand "kernel" "1" "1" replace -3 -7)"1" replace "1" "phi!1" )"1" expand "homomorphism?" )"1" "1" "1" "1" rewrite "one_right[T2, o, one2]" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" (inst 1 "x!1" ) nil nil )"2" expand "/" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "homomorphism?" )"2" (skosimp*)"2" (expand "restrict" )"2" "lc_gen(G!1, K, mult(G!1, K)(a!1, b!1))" )"2" (typepred "a!1" )"2" (typepred "b!1" )"2" (skosimp*)"2" "J" "lc_gen(G!1, K, mult(G!1, K)(a!1, b!1))" )"2" replace -1 -6)"2" replace -3 -6)"2" rewrite "mult_lem[T1, *, one1]" )"2" "lc_eq[T1, *, one1]" )"2" "G!1" "K" "a!3 * a!2" "J" )"2" assert )"2" "2" "divby_r[T1,*,one1]" )"1" "1" assert )"1" replace -1 1 rl)"1" "lc_gen(G!1, K, a!1)" )"1" replace -7 -2)"1" "lc_eq[T1, *, one1]" )"1" "1" "G!1" )"1" assert )"1" "1" "divby_r[T1,*,one1]" )"1" "1" assert )"1" replace "1" replace "1" "lc_gen(G!1, K, b!1)" )"1" replace "1" "lc_eq[T1, *, one1]" )"1" "1" "G!1" )"1" assert )"1" "1" "divby_r[T1, *, one1]" )"1" "1" assert )"1" replace "1" replace "1" "1" "h!1" )"1" "h!2" )"1" "h!3" )"1" expand *"K" "kernel" )"1" "1" "inv_in[T1, *, one1]" )"1" "1" "1" "G!1" "h!1" )"1" "G!1" "h!2" )"1" "G!1" "h!3" )"1" "homo_inv" )"1" "1" "1" "G!1" "GP!1" "phi!1" "h!1" )"1" "G!1" "GP!1" "phi!1" "h!2" )"1" "G!1" "GP!1" "phi!1" "h!3" )"1" replace "1" replace "1" replace "1" rewrite "inv_one[T2,o,one2]" )"1" "phi!1" )"1" expand "homomorphism?" )"1" "1" "1" "1" "a!3 * a!2" "inv[T1, *, one1](h!1)" )"1" "a!3" "a!2" )"1" "a!3" "inv[T1, *, one1](h!2)" )"1" "a!2" "inv[T1, *, one1](h!3)" )"1" "1" "1" "1" "1" "1" "1" "1" "1" rewrite "one_right[T2,o,one2]" )"1" rewrite "one_right[T2,o,one2]" )"1" rewrite "one_right[T2,o,one2]" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "a!2" "a!3" "G!1" )"2" expand "group?" )"2" "2" expand "monoid?" )"2" "2" expand "monad?" )"2" "2" "2" expand "star_closed?" )"2" "2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "T1_is_group" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "extend" )"2" (expand "image" )"2" (inst 1 "lc_gen[T1, *, one1](G!1, K, x1!1)" )"2" (expand "restrict" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (lemma "kernel_normal" )"3" (inst?) (("3" (assert ) nil nil )) nil )) nil )"4" (skosimp*)"4" (expand "extend" )"4" (expand "image" )"4" (inst 1 "lc_gen[T1, *, one1](G!1, K, A!1)" )"4" (expand "restrict" ) (("4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*) (("2" (rewrite "T2_is_group" ) nil nil )) nil )"3" (skosimp*)"3" (rewrite "left_cosets_group[T1, *, one1]" )"3" (hide 2)"3" (lemma "kernel_normal" )"3" (inst?) (("3" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"4" (skosimp*)"4" (lemma "first_isomorphism_th_TCC3" )"4" (inst?) (("4" (assert ) nil nil )) nil )) nil ))nil )"5" (skosimp*)"5" (lemma "homo_image" )"5" (inst?)"1" (expand "subgroup?" ) (("1" (assert ) nil nil )) nil )"2" (hide 2)"2" (rewrite "group_is_subgroup[T1, *, one1]" ) nil nil ))nil ))nil ))nil ))nil )"6" (skosimp*)"6" (lemma "kernel_normal" )"6" (inst?) (("6" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil booleans nil )nil booleans nil )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil homomorphism_lemmas nil )set type-eq-decl nil sets nil )"[T1, T1 -> T1]" homomorphism_lemmas nil )"T1" homomorphism_lemmas nil )"bool" group_def "algebra/" )nil group "algebra/" )"bool" group_def "algebra/" )nil group "algebra/" )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil homomorphism_lemmas nil )"[T2, T2 -> T2]" homomorphism_lemmas nil )"T2" homomorphism_lemmas nil )"bool" homomorphisms "algebra/" )nil homomorphisms "algebra/" )"subgroup[T1, *, one1](G)" homomorphisms"algebra/" )"boolean" normal_subgroups "algebra/" )"bool" booleans nil )"R" extend nil )"set[R]" function_image nil )"R" restrict nil )"set[T]" cosets "algebra/" )nil cosets "algebra/" )nil normal_subgroups "algebra/" )"left_cosets(G, H)" factor_groups "algebra/" )"set" sets nil )"[bool, bool -> bool]" booleans nil )"bool" homomorphisms "algebra/" )"group[left_cosets(G, N), mult(G, N), N]" nil )"group[T1, *, one1]" homomorphism_lemmasnil )"subgroup[T1, *, one1](G!1)" nil )"group[T2, o, one2]" homomorphism_lemmasnil )"homomorphism[T1, *, one1, T2, o, one2](G!1, GP!1)" nil )"{a: T | G(a) AND lc = a * H}" cosets"algebra/" )nil cosets "algebra/" )nil group "algebra/" )"bool" groupoid_def "algebra/" )"bool" sets nil )"bool" monad_def "algebra/" )"bool" monoid_def "algebra/" )NOT const-decl "[bool -> bool]" booleans nil )nil homomorphism_lemmas nil )nil group "algebra/" )nil group "algebra/" )nil group "algebra/" )nil group "algebra/" )"(G!1 / K)" homomorphism_lemmas nil )"(G!1 / K)" homomorphism_lemmas nil )"{y | x * y = one AND y * x = one}" group"algebra/" )"bool" functions nil )"(restrict[T1, (G!1), boolean](G!1))" nil )nil group "algebra/" )nil cosets "algebra/" )"setofsets[T]" right_left_cosets nil )"bool" functions nil )nil groups_scaf nil )"(K)" homomorphism_lemmas nil )"(K)" homomorphism_lemmas nil )"(G!1)" homomorphism_lemmas nil )"(G!1)" homomorphism_lemmas nil )"(K)" homomorphism_lemmas nil )nil group "algebra/" )nil homomorphism_lemmas nil )nil factor_groups "algebra/" )"bool" homomorphisms "algebra/" )"(G!1 / K)" homomorphism_lemmas nil )nil homomorphism_lemmas nil )"left_cosets[T1, *, one1](G!1, K)" nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.129 Sekunden
(vorverarbeitet am 2026-04-27)
¤ *© Formatika GbR, Deutschland
2026-05-26
