| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/groups/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 193 kB |
|
Quellcode-Bibliothek homomorphism_lemmas.prfInteraktion undPortierbarkeitLisp |
|||||||||||||||
|
(homomorphism_lemmas (G_TCC1 0 (G_TCC1-1 nil 3530720894 ("" (rewrite "T1_is_group") nil nil) ((T1_is_group formula-decl nil homomorphism_lemmas nil)) nil)) (GP_TCC1 0 (GP_TCC1-1 nil 3528505895 ("" (rewrite "T2_is_group") nil nil) ((T2_is_group formula-decl nil homomorphism_lemmas nil)) nil)) (natural_homo_TCC1 0 (natural_homo_TCC1-1 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) ((G!1 skolem-const-decl "group[T1, *, one1]" homomorphism_lemmas nil) (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one1 formal-const-decl "T1" homomorphism_lemmas nil) (* formal-const-decl "[T1, T1 -> T1]" homomorphism_lemmas nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T1 formal-type-decl nil homomorphism_lemmas nil) (normal_subgroup type-eq-decl nil normal_subgroups "algebra/") (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/") (left_coset_one formula-decl nil cosets "algebra/") (monoid? const-decl "bool" monoid_def "algebra/") (member const-decl "bool" sets nil) (monad? const-decl "bool" monad_def "algebra/") (NOT const-decl "[bool -> bool]" booleans nil)) nil)) (natural_homo_TCC2 0 (natural_homo_TCC2-1 nil 3524789060 ("" (skosimp*) (("" (rewrite "left_cosets_group[T1, *, one1]") nil nil)) nil) ((left_cosets_group formula-decl nil factor_groups "algebra/") (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/") (normal_subgroup type-eq-decl nil normal_subgroups "algebra/") (T1 formal-type-decl nil homomorphism_lemmas nil) (* formal-const-decl "[T1, T1 -> T1]" homomorphism_lemmas nil) (one1 formal-const-decl "T1" homomorphism_lemmas nil)) nil)) (natural_homo 0 (natural_homo-1 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" (flatten) (("1" (hide-all-but (-1 -2 -8 1)) (("1" (expand "star_closed?") (("1" (inst?) (("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" (flatten) (("2" (hide-all-but (-1 -7 -8 1)) (("2" (expand* "star_closed?" "member") (("2" (lemma "inv_in[T1, *, one1]") (("2" (inst -1 "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" (flatten) (("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) ((/ const-decl "group[left_cosets(G, N), mult(G, N), N]" right_left_cosets nil) (mult const-decl "left_cosets(G, H)" factor_groups "algebra/") (left_cosets type-eq-decl nil cosets "algebra/") (K!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)" homomorphism_lemmas nil) (normal_subgroup type-eq-decl nil normal_subgroups "algebra/") (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/") (* const-decl "set[T]" cosets "algebra/") (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (G!1 skolem-const-decl "group[T1, *, one1]" homomorphism_lemmas nil) (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one1 formal-const-decl "T1" homomorphism_lemmas nil) (* formal-const-decl "[T1, T1 -> T1]" homomorphism_lemmas nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T1 formal-type-decl nil homomorphism_lemmas nil) (fullset const-decl "set" sets nil) (homomorphism type-eq-decl nil homomorphisms "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (subgroup type-eq-decl nil group "algebra/") (kernel const-decl "subgroup[T1, *, one1](G)" homomorphisms "algebra/") (one_right formula-decl nil group "algebra/") (inv const-decl "{y | x * y = one AND y * x = one}" group "algebra/") (x!1 skolem-const-decl "T1" homomorphism_lemmas nil) (x!2 skolem-const-decl "T1" homomorphism_lemmas nil) (inv_right formula-decl nil group "algebra/") (one_left formula-decl nil group "algebra/") (assoc formula-decl nil group "algebra/") (inv_in formula-decl nil group "algebra/") (star_closed? const-decl "bool" groupoid_def "algebra/") (monad? const-decl "bool" monad_def "algebra/") (monoid? const-decl "bool" monoid_def "algebra/") (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (left_cosets_group formula-decl nil factor_groups "algebra/") (T1_is_group formula-decl nil homomorphism_lemmas nil) (left_coset_one formula-decl nil cosets "algebra/") (restrict const-decl "R" restrict nil) (left_cosets const-decl "setofsets[T]" right_left_cosets nil) (surjective? const-decl "bool" functions nil) (NOT const-decl "[bool -> bool]" booleans nil) (homomorphism? const-decl "bool" homomorphisms "algebra/") (mult_lem formula-decl nil factor_groups "algebra/")) shostak)) (homo_inv_TCC1 0 (homo_inv_TCC1-1 nil 3524504949 ("" (skosimp*) (("" (typepred "x!1") (("" (rewrite "inv_in[T1, *, one1]") nil nil)) nil)) nil) ((group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one1 formal-const-decl "T1" homomorphism_lemmas nil) (* formal-const-decl "[T1, T1 -> T1]" homomorphism_lemmas nil) (set type-eq-decl nil sets nil) (T1 formal-type-decl nil homomorphism_lemmas nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (inv_in formula-decl nil group "algebra/")) nil)) (homo_inv 0 (homo_inv-1 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" (replaces -1) (("1" (lemma "unique_inv[T2, o, one2]") (("1" (inst?) (("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) ((one1 formal-const-decl "T1" homomorphism_lemmas nil) (* formal-const-decl "[T1, T1 -> T1]" homomorphism_lemmas nil) (T1 formal-type-decl nil homomorphism_lemmas nil) (inv_left formula-decl nil group "algebra/") (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (homomorphism type-eq-decl nil homomorphisms "algebra/") (homomorphism? const-decl "bool" homomorphisms "algebra/") (one2 formal-const-decl "T2" homomorphism_lemmas nil) (O formal-const-decl "[T2, T2 -> T2]" homomorphism_lemmas nil) (T2 formal-type-decl nil homomorphism_lemmas nil) (NOT const-decl "[bool -> bool]" booleans nil) (unique_inv formula-decl nil group "algebra/") (homo_one formula-decl nil homomorphisms "algebra/") (inv_in formula-decl nil group "algebra/") (x!1 skolem-const-decl "(G!1)" homomorphism_lemmas nil) (inv const-decl "{y | x * y = one AND y * x = one}" group "algebra/") (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (G!1 skolem-const-decl "group[T1, *, one1]" homomorphism_lemmas nil) (inv_right formula-decl nil group "algebra/")) shostak)) (kernel_normal 0 (kernel_normal-1 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" (inst -1 "inv[T1, *, one1](a) * h!2" "a") (("1" (replaces -1) (("1" (inst -1 "inv[T1, *, one1](a)" "h!2") (("1" (replaces -1) (("1" (replaces -2) (("1" (lemma "one_right[T2, o, one2]") (("1" (inst?) (("1" (replaces -1) (("1" (rewrite "homo_inv") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "a") (("2" (rewrite "inv_in[T1, *, one1]") nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "a") (("2" (lemma "inv_in[T1, *, one1]") (("2" (inst?) (("2" (typepred "G") (("2" (expand "group?") (("2" (flatten) (("2" (expand "monoid?") (("2" (flatten) (("2" (expand "monad?") (("2" (flatten) (("2" (expand "star_closed?") (("2" (hide-all-but (-1 -6 -7 1)) (("2" (inst?) (("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" (typepred "G") (("2" (expand "group?") (("2" (flatten) (("2" (expand "monoid?") (("2" (flatten) (("2" (expand "monad?") (("2" (flatten) (("2" (expand "star_closed?") (("2" (hide-all-but (-1 -6 -7 -8 1)) (("2" (copy -1) (("2" (inst -2 "inv[T1, *, one1](a)" "h!2") (("2" (expand "member") (("2" (inst -1 "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) ((IFF const-decl "[bool, bool -> bool]" booleans nil) (T1 formal-type-decl nil homomorphism_lemmas nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (* formal-const-decl "[T1, T1 -> T1]" homomorphism_lemmas nil) (one1 formal-const-decl "T1" homomorphism_lemmas nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (T2 formal-type-decl nil homomorphism_lemmas nil) (O formal-const-decl "[T2, T2 -> T2]" homomorphism_lemmas nil) (one2 formal-const-decl "T2" homomorphism_lemmas nil) (homomorphism? const-decl "bool" homomorphisms "algebra/") (homomorphism type-eq-decl nil homomorphisms "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (subgroup type-eq-decl nil group "algebra/") (kernel const-decl "subgroup[T1, *, one1](G)" homomorphisms "algebra/") (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/") (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (* const-decl "set[T]" cosets "algebra/") (NOT const-decl "[bool -> bool]" booleans nil) (* const-decl "set[T]" cosets "algebra/") (AND const-decl "[bool, bool -> bool]" booleans nil) (inv const-decl "{y | x * y = one AND y * x = one}" group "algebra/") (G skolem-const-decl "group[T1, *, one1]" homomorphism_lemmas nil) (a skolem-const-decl "(G)" homomorphism_lemmas nil) (GP skolem-const-decl "group[T2, o, one2]" homomorphism_lemmas nil) (phi skolem-const-decl "homomorphism[T1, *, one1, T2, o, one2](G, GP)" homomorphism_lemmas nil) (h!2 skolem-const-decl "(kernel(G, GP)(phi))" homomorphism_lemmas nil) (homo_inv formula-decl nil homomorphism_lemmas nil) (one_right formula-decl nil group "algebra/") (inv_in formula-decl nil group "algebra/") (monoid? const-decl "bool" monoid_def "algebra/") (monad? const-decl "bool" monad_def "algebra/") (star_closed? const-decl "bool" groupoid_def "algebra/") (h!2 skolem-const-decl "(kernel(G, GP)(phi))" homomorphism_lemmas nil) (K skolem-const-decl "subgroup[T1, *, one1](G)" homomorphism_lemmas nil)) shostak)) (homo_image 0 (homo_image-1 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" (flatten) (("1" (expand "monad?") (("1" (flatten) (("1" (hide-all-but (-2 1)) (("1" (expand "member") (("1" (assert) (("1" (expand "image") (("1" (inst 1 "one1") (("1" (rewrite "homo_one[T1, *, one1,T2, o, one2]") nil nil) ("2" (prop) (("1" (typepred "G!1") (("1" (expand "group?") (("1" (flatten) (("1" (expand "monoid?") (("1" (flatten) (("1" (expand "monad?") (("1" (flatten) (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "restrict") (("2" (typepred "H!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)) 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" (prop) (("1" (expand "image") (("1" (skosimp) (("1" (skosimp) (("1" (inst 1 "x!2 * x!3") (("1" (typepred "phi!1") (("1" (expand "homomorphism?") (("1" (inst -1 "x!2" "x!3") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (prop) (("1" (typepred "x!2") (("1" (typepred "x!3") (("1" (typepred "G!1") (("1" (expand "group?") (("1" (flatten) (("1" (expand "monoid?") (("1" (flatten) (("1" (expand "monad?") (("1" (flatten) (("1" (hide-all-but (-1 -6 -8 1)) (("1" (expand "star_closed?") (("1" (inst?) (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "restrict") (("2" (typepred "x!2") (("2" (typepred "x!3") (("2" (typepred "H!1") (("2" (expand "group?") (("2" (flatten) (("2" (expand "monoid?") (("2" (flatten) (("2" (expand "monad?") (("2" (flatten) (("2" (hide-all-but (-1 -8 -10 1)) (("2" (expand* "restrict" "star_closed?" "member") (("2" (inst?) 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" (flatten) (("2" (expand "monad?") (("2" (flatten) (("2" (typepred "x!1") (("2" (typepred "y!1") (("2" (expand* "extend" "star_closed?" "member" "image") (("2" (prop) (("2" (hide-all-but (-1 -3 -5 1)) (("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" (typepred "x!2") (("1" (inst 1 "inv[T1, *, one1](x!2)") (("1" (rewrite "homo_inv") (("1" (assert) nil nil)) nil) ("2" (prop) (("1" (hide-all-but (-1 1)) (("1" (rewrite "inv_in") nil nil)) nil) ("2" (expand "restrict") (("2" (hide-all-but (-2 1)) (("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) ((one2 formal-const-decl "T2" homomorphism_lemmas nil) (O formal-const-decl "[T2, T2 -> T2]" homomorphism_lemmas nil) (T2 formal-type-decl nil homomorphism_lemmas nil) (subgroup_def formula-decl nil group "algebra/") (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (homo_one formula-decl nil homomorphisms "algebra/") (H!1 skolem-const-decl "subgroup[T1, *, one1](G!1)" homomorphism_lemmas nil) (G!1 skolem-const-decl "group[T1, *, one1]" homomorphism_lemmas nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (monad? const-decl "bool" monad_def "algebra/") (monoid? const-decl "bool" monoid_def "algebra/") (member const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (x!1 skolem-const-decl "(extend[T2, (GP!1), bool, FALSE] (image(phi!1, restrict[T1, (G!1), boolean](H!1))))" homomorphism_lemmas nil) (y!1 skolem-const-decl "(extend[T2, (GP!1), bool, FALSE] (image(phi!1, restrict[T1, (G!1), boolean](H!1))))" homomorphism_lemmas nil) (phi!1 skolem-const-decl "homomorphism[T1, *, one1, T2, o, one2](G!1, GP!1)" homomorphism_lemmas nil) (GP!1 skolem-const-decl "group[T2, o, one2]" homomorphism_lemmas nil) (x!3 skolem-const-decl "(restrict[T1, (G!1), boolean](H!1))" homomorphism_lemmas nil) (x!2 skolem-const-decl "(restrict[T1, (G!1), boolean](H!1))" homomorphism_lemmas nil) (star_closed? const-decl "bool" groupoid_def "algebra/") (= const-decl "[T, T -> boolean]" equalities nil) (inv const-decl "{y | x * y = one AND y * x = one}" group "algebra/") (x!2 skolem-const-decl "(restrict[T1, (G!1), boolean](H!1))" homomorphism_lemmas nil) (homo_inv formula-decl nil homomorphism_lemmas nil) (inv_in formula-decl nil group "algebra/") (inv_closed? const-decl "bool" group "algebra/") (subgroup type-eq-decl nil group "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (restrict const-decl "R" restrict nil) (homomorphism type-eq-decl nil homomorphisms "algebra/") (homomorphism? const-decl "bool" homomorphisms "algebra/") (image const-decl "set[R]" function_image nil) (one1 formal-const-decl "T1" homomorphism_lemmas nil) (* formal-const-decl "[T1, T1 -> T1]" homomorphism_lemmas nil) (T1 formal-type-decl nil homomorphism_lemmas nil) (extend const-decl "R" extend nil) (FALSE const-decl "bool" booleans nil) (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (homo_image_normal_TCC1 0 (homo_image_normal_TCC1-1 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) ((homo_image formula-decl nil homomorphism_lemmas nil) (NOT const-decl "[bool -> bool]" booleans nil) (subgroup_is_group formula-decl nil group "algebra/") (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (image const-decl "set[R]" function_image nil) (restrict const-decl "R" restrict nil) (subgroup type-eq-decl nil group "algebra/") (homomorphism type-eq-decl nil homomorphisms "algebra/") (homomorphism? const-decl "bool" homomorphisms "algebra/") (one2 formal-const-decl "T2" homomorphism_lemmas nil) (O formal-const-decl "[T2, T2 -> T2]" homomorphism_lemmas nil) (T2 formal-type-decl nil homomorphism_lemmas nil) (T1 formal-type-decl nil homomorphism_lemmas nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (* formal-const-decl "[T1, T1 -> T1]" homomorphism_lemmas nil) (one1 formal-const-decl "T1" homomorphism_lemmas nil) (group? const-decl "bool" group_def "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/") (G!1 skolem-const-decl "group[T1, *, one1]" homomorphism_lemmas nil) (normal_subgroup type-eq-decl nil normal_subgroups "algebra/") (H!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)" homomorphism_lemmas nil)) nil)) (homo_image_normal 0 (homo_image_normal-1 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" (skosimp) (("1" (typepred "h!1") (("1" (skosimp) (("1" (replaces -1) (("1" (typepred "h!2") (("1" (expand "extend") (("1" (prop) (("1" (expand "image") (("1" (skosimp) (("1" (inst -6 "a!1") (("1" (skosimp) (("1" (inst 1 "inv[T1, *, one1](x!3) * x!2 * x!3") (("1" (hide-all-but (-2 -6 -7 1)) (("1" (typepred "phi!1") (("1" (expand "homomorphism?") (("1" (inst-cp -1 "inv[T1, *, one1](x!3) * x!2" "x!3") (("1" (inst -1 "inv[T1, *, one1](x!3)" "x!2") (("1" (replaces -1) (("1" (replaces -1) (("1" (lemma "homo_inv[T1, *, one1,T2, o, one2]") (("1" (inst?) (("1" (replaces -1) (("1" (replaces -2) (("1" (replace -1 1 rl) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "inv_in") nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "product_in[T1, *, one1]") (("2" (hide 2) (("2" (rewrite "inv_in") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (prop) (("1" (hide-all-but 1) (("1" (rewrite "product_in[T1, *, one1]") (("1" (hide 2) (("1" (rewrite "product_in[T1, *, one1]") (("1" (hide 2) (("1" (rewrite "inv_in") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "restrict") (("2" (hide-all-but (-5 1)) (("2" (typepred "x!2") (("2" (expand "restrict") (("2" (hide -1) (("2" (inst -2 "x!3") (("2" (inst -2 "inv[T1, *, one1](x!3) * x!2 * x!3") (("2" (assert) (("2" (hide 1) (("2" (expand "*") (("2" (inst 1 "inv[T1, *, one1](x!3) * x!2") (("2" (inst 1 "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" (skosimp) (("2" (typepred "h!1" "a!1") (("2" (skosimp) (("2" (replaces -1) (("2" (typepred "h!2") (("2" (expand "extend") (("2" (prop) (("2" (hide -2) (("2" (replaces -3) (("2" (rewrite "product_in[T2, o, one2]") (("2" (hide 2) (("2" (rewrite "product_in[T2, o, one2]") (("2" (hide 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) ((normal_subgroup type-eq-decl nil normal_subgroups "algebra/") (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one1 formal-const-decl "T1" homomorphism_lemmas nil) (* formal-const-decl "[T1, T1 -> T1]" homomorphism_lemmas nil) (set type-eq-decl nil sets nil) (T1 formal-type-decl nil homomorphism_lemmas nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (homo_image formula-decl nil homomorphism_lemmas nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (extend const-decl "R" extend nil) (surjective? const-decl "bool" functions nil) (product_in formula-decl nil group "algebra/") (homo_inv formula-decl nil homomorphism_lemmas nil) (inv_in formula-decl nil group "algebra/") (x!2 skolem-const-decl "(restrict[T1, (G!1), boolean](H!1))" homomorphism_lemmas nil) (x!3 skolem-const-decl "(G!1)" homomorphism_lemmas nil) (inv const-decl "{y | x * y = one AND y * x = one}" group "algebra/") (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (restrict const-decl "R" restrict nil) (image const-decl "set[R]" function_image nil) (FALSE const-decl "bool" booleans nil) (* const-decl "set[T]" cosets "algebra/") (* const-decl "set[T]" cosets "algebra/") (subgroup type-eq-decl nil group "algebra/") (homomorphism type-eq-decl nil homomorphisms "algebra/") (homomorphism? const-decl "bool" homomorphisms "algebra/") (one2 formal-const-decl "T2" homomorphism_lemmas nil) (O formal-const-decl "[T2, T2 -> T2]" homomorphism_lemmas nil) (T2 formal-type-decl nil homomorphism_lemmas nil) (subgroup? const-decl "bool" group_def "algebra/") (G!1 skolem-const-decl "group[T1, *, one1]" homomorphism_lemmas nil) (H!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)" homomorphism_lemmas nil)) shostak)) (homo_inv_image 0 (homo_inv_image-1 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" (flatten) (("1" (expand "monad?") (("1" (flatten) (("1" (hide-all-but (-2 1)) (("1" (expand* "inverse_image" "member") (("1" (assert) (("1" (typepred "K!1") (("1" (hide -2) (("1" (expand "group?") (("1" (flatten) (("1" (expand "monoid?") (("1" (flatten) (("1" (expand "monad?") (("1" (flatten) (("1" (hide-all-but (-2 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" (prop) (("1" (hide (-1 -2 -4)) (("1" (typepred "phi!1") (("1" (expand "homomorphism?") (("1" (inst -1 "x!1" "y!1") (("1" (replaces -1) (("1" (typepred "K!1") (("1" (hide -2) (("1" (expand "group?") (("1" (flatten) (("1" (expand "monoid?") (("1" (flatten) (("1" (expand "monad?") (("1" (flatten) (("1" (hide-all-but (-1 -6 -7 1)) (("1" (expand* "star_closed?" "member") (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-2 -4)) (("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) ((one1 formal-const-decl "T1" homomorphism_lemmas nil) (* formal-const-decl "[T1, T1 -> T1]" homomorphism_lemmas nil) (T1 formal-type-decl nil homomorphism_lemmas nil) (subgroup_def formula-decl nil group "algebra/") (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (homo_one formula-decl nil homomorphisms "algebra/") (monad? const-decl "bool" monad_def "algebra/") (monoid? const-decl "bool" monoid_def "algebra/") (member const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (x!1 skolem-const-decl "(extend[T1, (G!1), bool, FALSE](inverse_image(phi!1, K!1)))" homomorphism_lemmas nil) (y!1 skolem-const-decl "(extend[T1, (G!1), bool, FALSE](inverse_image(phi!1, K!1)))" homomorphism_lemmas nil) (phi!1 skolem-const-decl "homomorphism[T1, *, one1, T2, o, one2](G!1, GP!1)" homomorphism_lemmas nil) (G!1 skolem-const-decl "group[T1, *, one1]" homomorphism_lemmas nil) (K!1 skolem-const-decl "subgroup[T2, o, one2](GP!1)" homomorphism_lemmas nil) (GP!1 skolem-const-decl "group[T2, o, one2]" homomorphism_lemmas nil) (product_in formula-decl nil group "algebra/") (star_closed? const-decl "bool" groupoid_def "algebra/") (homo_inv formula-decl nil homomorphism_lemmas nil) (inv_in formula-decl nil group "algebra/") (inv_closed? const-decl "bool" group "algebra/") (subgroup type-eq-decl nil group "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (homomorphism type-eq-decl nil homomorphisms "algebra/") (homomorphism? const-decl "bool" homomorphisms "algebra/") (one2 formal-const-decl "T2" homomorphism_lemmas nil) (O formal-const-decl "[T2, T2 -> T2]" homomorphism_lemmas nil) (inverse_image const-decl "set[D]" function_image nil) (T2 formal-type-decl nil homomorphism_lemmas nil) (extend const-decl "R" extend nil) (FALSE const-decl "bool" booleans nil) (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (homo_inv_image_normal_TCC1 0 (homo_inv_image_normal_TCC1-1 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) ((homo_inv_image formula-decl nil homomorphism_lemmas nil) (NOT const-decl "[bool -> bool]" booleans nil) (subgroup_is_group formula-decl nil group "algebra/") (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (inverse_image const-decl "set[D]" function_image nil) (subgroup type-eq-decl nil group "algebra/") (homomorphism type-eq-decl nil homomorphisms "algebra/") (homomorphism? const-decl "bool" homomorphisms "algebra/") (one1 formal-const-decl "T1" homomorphism_lemmas nil) (* formal-const-decl "[T1, T1 -> T1]" homomorphism_lemmas nil) (T1 formal-type-decl nil homomorphism_lemmas nil) (T2 formal-type-decl nil homomorphism_lemmas nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (O formal-const-decl "[T2, T2 -> T2]" homomorphism_lemmas nil) (one2 formal-const-decl "T2" homomorphism_lemmas nil) (group? const-decl "bool" group_def "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/") (GP!1 skolem-const-decl "group[T2, o, one2]" homomorphism_lemmas nil) (normal_subgroup type-eq-decl nil normal_subgroups "algebra/") (K!1 skolem-const-decl "normal_subgroup[T2, o, one2](GP!1)" homomorphism_lemmas nil)) nil)) (homo_inv_image_normal 0 (homo_inv_image_normal-1 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" (skosimp) (("1" (typepred "h!1") (("1" (skosimp) (("1" (replaces -1) (("1" (typepred "h!2") (("1" (expand "extend") (("1" (prop) (("1" (inst -5 "phi!1(a!1)") (("1" (inst -5 "phi!1(x!1)") (("1" (assert) (("1" (hide 1) (("1" (expand "*") (("1" (inst 1 "inv[T2, o, one2](phi!1(a!1)) o phi!1(h!2)") (("1" (replaces -5) (("1" (hide-all-but 1) (("1" (typepred "phi!1") (("1" (expand "homomorphism?") (("1" (inst-cp -1 "inv[T1, *, one1](a!1) * h!2" "a!1") (("1" (inst -1 "inv[T1, *, one1](a!1)" "h!2") (("1" (replaces -1) (("1" (replaces -1) (("1" (lemma "homo_inv[T1, *, one1,T2, o, one2]") (("1" (inst?) (("1" (replaces -1) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "inv_in") nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "product_in[T1, *, one1]") (("2" (hide 2) (("2" (rewrite "inv_in") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst?) 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" (skosimp) (("2" (typepred "h!1" "a!1") (("2" (skosimp) (("2" (typepred "h!2") (("2" (expand "extend") (("2" (prop) (("2" (hide -2) (("2" (replaces -2) (("2" (replaces -3) (("2" (rewrite "product_in[T1, *, one1]") (("2" (hide 2) (("2" (rewrite "product_in[T1, *, one1]") (("2" (hide 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) ((normal_subgroup type-eq-decl nil normal_subgroups "algebra/") (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one2 formal-const-decl "T2" homomorphism_lemmas nil) (O formal-const-decl "[T2, T2 -> T2]" homomorphism_lemmas nil) (set type-eq-decl nil sets nil) (T2 formal-type-decl nil homomorphism_lemmas nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (homo_inv_image formula-decl nil homomorphism_lemmas nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (extend const-decl "R" extend nil) (inverse_image const-decl "set[D]" function_image nil) (* const-decl "set[T]" cosets "algebra/") (* const-decl "set[T]" cosets "algebra/") (FALSE const-decl "bool" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (inv const-decl "{y | x * y = one AND y * x = one}" group "algebra/") (inv_in formula-decl nil group "algebra/") (homo_inv formula-decl nil homomorphism_lemmas nil) (product_in formula-decl nil group "algebra/") (h!2 skolem-const-decl "(extend[T1, (G!1), bool, FALSE]({x: (G!1) | K!1(phi!1(x))}))" homomorphism_lemmas nil) (a!1 skolem-const-decl "(G!1)" homomorphism_lemmas nil) (phi!1 skolem-const-decl "homomorphism[T1, *, one1, T2, o, one2](G!1, GP!1)" homomorphism_lemmas nil) (G!1 skolem-const-decl "group[T1, *, one1]" homomorphism_lemmas nil) (subgroup type-eq-decl nil group "algebra/") (homomorphism type-eq-decl nil homomorphisms "algebra/") (homomorphism? const-decl "bool" homomorphisms "algebra/") (one1 formal-const-decl "T1" homomorphism_lemmas nil) (* formal-const-decl "[T1, T1 -> T1]" homomorphism_lemmas nil) (T1 formal-type-decl nil homomorphism_lemmas nil) (subgroup? const-decl "bool" group_def "algebra/") (GP!1 skolem-const-decl "group[T2, o, one2]" homomorphism_lemmas nil) (K!1 skolem-const-decl "normal_subgroup[T2, o, one2](GP!1)" homomorphism_lemmas nil)) shostak)) (kernel_in_inv_image 0 (kernel_in_inv_image-1 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") (("" (replaces -3) (("" (typepred "S!1") (("" (expand "group?") (("" (flatten) (("" (expand "monoid?") (("" (flatten) (("" (expand "monad?") (("" (flatten) (("" (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) ((IFF const-decl "[bool, bool -> bool]" booleans nil) (T1 formal-type-decl nil homomorphism_lemmas nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (* formal-const-decl "[T1, T1 -> T1]" homomorphism_lemmas nil) (one1 formal-const-decl "T1" homomorphism_lemmas nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (T2 formal-type-decl nil homomorphism_lemmas nil) (O formal-const-decl "[T2, T2 -> T2]" homomorphism_lemmas nil) (one2 formal-const-decl "T2" homomorphism_lemmas nil) (homomorphism? const-decl "bool" homomorphisms "algebra/") (homomorphism type-eq-decl nil homomorphisms "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (subgroup type-eq-decl nil group "algebra/") (kernel const-decl "subgroup[T1, *, one1](G)" homomorphisms "algebra/") (inverse_image const-decl "set[D]" function_image nil) (extend const-decl "R" extend nil) (FALSE const-decl "bool" booleans nil) (subset? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (monad? const-decl "bool" monad_def "algebra/") (monoid? const-decl "bool" monoid_def "algebra/") (member const-decl "bool" sets nil)) shostak)) (homo_inv_image_image 0 (homo_inv_image_image-1 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" (inst -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" (inst?) (("1" (replaces -2) (("1" (typepred "x!2") (("1" (hide -1) (("1" (expand "restrict") (("1" (inst 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" (hide -3) (("2" (replaces -3) (("2" (expand "kernel") (("2" (assert) (("2" (hide (-1 -2)) (("2" (rewrite "product_in[T1, *, one1]") (("2" (hide 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" (inst?) (("1" (replaces -1) (("1" (replaces -2) (("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" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((IFF const-decl "[bool, bool -> bool]" booleans nil) (T1 formal-type-decl nil homomorphism_lemmas nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (* formal-const-decl "[T1, T1 -> T1]" homomorphism_lemmas nil) (one1 formal-const-decl "T1" homomorphism_lemmas nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (T2 formal-type-decl nil homomorphism_lemmas nil) (O formal-const-decl "[T2, T2 -> T2]" homomorphism_lemmas nil) (one2 formal-const-decl "T2" homomorphism_lemmas nil) (homomorphism? const-decl "bool" homomorphisms "algebra/") (homomorphism type-eq-decl nil homomorphisms "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (subgroup type-eq-decl nil group "algebra/") (kernel const-decl "subgroup[T1, *, one1](G)" homomorphisms "algebra/") (prod const-decl "set[T]" products_subgroups nil) (restrict const-decl "R" restrict nil) (image const-decl "set[R]" function_image nil) (inverse_image const-decl "set[D]" function_image nil) (h!1 skolem-const-decl "(H!1)" homomorphism_lemmas nil) (one_right formula-decl nil group "algebra/") (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (cancel_left formula-decl nil group "algebra/") (inv_left formula-decl nil group "algebra/") (NOT const-decl "[bool -> bool]" booleans nil) (inv_in formula-decl nil group "algebra/") (product_in formula-decl nil group "algebra/") (assoc formula-decl nil group "algebra/") (one_left formula-decl nil group "algebra/") (inv_right formula-decl nil group "algebra/") (x!1 skolem-const-decl "(G!1)" homomorphism_lemmas nil) (K!1 skolem-const-decl "subgroup[T1, *, one1](G!1)" homomorphism_lemmas nil) (x!2 skolem-const-decl "(restrict[T1, (G!1), boolean](H!1))" homomorphism_lemmas nil) (H!1 skolem-const-decl "subgroup[T1, *, one1](G!1)" homomorphism_lemmas nil) (G!1 skolem-const-decl "group[T1, *, one1]" homomorphism_lemmas nil) (homo_inv formula-decl nil homomorphism_lemmas nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (inv const-decl "{y | x * y = one AND y * x = one}" group "algebra/")) shostak)) (homo_inv_image_image_cor 0 (homo_inv_image_image_cor-1 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" (inst 2 "one1" "x!1") (("1" (rewrite "one_left[T1,*,one1]") nil nil) ("2" (assert) nil nil) ("3" (typepred "H!1") (("3" (expand* "group?" "monoid?" "monad?") (("3" (flatten) (("3" (hide-all-but (-2 1)) (("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" (inst -2 "k!1") (("1" (assert) (("1" (replaces -1) (("1" (hide -2) (("1" (typepred "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" (typepred "G!1") (("2" (expand* "group?" "monoid?" "monad?") (("2" (flatten) (("2" (hide-all-but (-2 1)) (("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) ((IFF const-decl "[bool, bool -> bool]" booleans nil) (T1 formal-type-decl nil homomorphism_lemmas nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (* formal-const-decl "[T1, T1 -> T1]" homomorphism_lemmas nil) (one1 formal-const-decl "T1" homomorphism_lemmas nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (T2 formal-type-decl nil homomorphism_lemmas nil) (O formal-const-decl "[T2, T2 -> T2]" homomorphism_lemmas nil) (one2 formal-const-decl "T2" homomorphism_lemmas nil) (homomorphism? const-decl "bool" homomorphisms "algebra/") (homomorphism type-eq-decl nil homomorphisms "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (subgroup type-eq-decl nil group "algebra/") (kernel const-decl "subgroup[T1, *, one1](G)" homomorphisms "algebra/") (restrict const-decl "R" restrict nil) (image const-decl "set[R]" function_image nil) (inverse_image const-decl "set[D]" function_image nil) (product_in formula-decl nil group "algebra/") (homo_one formula-decl nil homomorphisms "algebra/") (one_right formula-decl nil group "algebra/") (x!1 skolem-const-decl "(G!1)" homomorphism_lemmas nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (prod const-decl "set[T]" products_subgroups nil) (H!1 skolem-const-decl "subgroup[T1, *, one1](G!1)" homomorphism_lemmas nil) (GP!1 skolem-const-decl "group[T2, o, one2]" homomorphism_lemmas nil) (phi!1 skolem-const-decl "homomorphism[T1, *, one1, T2, o, one2](G!1, GP!1)" homomorphism_lemmas nil) (one_left formula-decl nil group "algebra/") (monoid? const-decl "bool" monoid_def "algebra/") (monad? const-decl "bool" monad_def "algebra/") (NOT const-decl "[bool -> bool]" booleans nil) (x!1 skolem-const-decl "T1" homomorphism_lemmas nil) (G!1 skolem-const-decl "group[T1, *, one1]" homomorphism_lemmas nil) (homo_inv_image_image formula-decl nil homomorphism_lemmas nil)) shostak)) (first_isomorphism_th_TCC1 0 (first_isomorphism_th_TCC1-1 nil 3524797513 ("" (skosimp*) (("" (lemma "kernel_normal[T1, *, one1,T2, o, one2]") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((kernel_normal formula-decl nil homomorphism_lemmas nil) (homomorphism type-eq-decl nil homomorphisms "algebra/") (homomorphism? const-decl "bool" homomorphisms "algebra/") (one2 formal-const-decl "T2" homomorphism_lemmas nil) (O formal-const-decl "[T2, T2 -> T2]" homomorphism_lemmas nil) (T2 formal-type-decl nil homomorphism_lemmas nil) (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one1 formal-const-decl "T1" homomorphism_lemmas nil) (* formal-const-decl "[T1, T1 -> T1]" homomorphism_lemmas nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T1 formal-type-decl nil homomorphism_lemmas nil)) nil)) (first_isomorphism_th_TCC2 0 (first_isomorphism_th_TCC2-1 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) ((homo_image formula-decl nil homomorphism_lemmas nil) (group_is_subgroup formula-decl nil group "algebra/") (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (subgroup type-eq-decl nil group "algebra/") (homomorphism type-eq-decl nil homomorphisms "algebra/") (homomorphism? const-decl "bool" homomorphisms "algebra/") (one2 formal-const-decl "T2" homomorphism_lemmas nil) (O formal-const-decl "[T2, T2 -> T2]" homomorphism_lemmas nil) (T2 formal-type-decl nil homomorphism_lemmas nil) (T1 formal-type-decl nil homomorphism_lemmas nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (* formal-const-decl "[T1, T1 -> T1]" homomorphism_lemmas nil) (one1 formal-const-decl "T1" homomorphism_lemmas nil) (group? const-decl "bool" group_def "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (G!1 skolem-const-decl "group[T1, *, one1]" homomorphism_lemmas nil)) nil)) (first_isomorphism_th_TCC3 0 (first_isomorphism_th_TCC3-1 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) ((G!1 skolem-const-decl "group[T1, *, one1]" homomorphism_lemmas nil) (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one1 formal-const-decl "T1" homomorphism_lemmas nil) (* formal-const-decl "[T1, T1 -> T1]" homomorphism_lemmas nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T1 formal-type-decl nil homomorphism_lemmas nil) (subgroup type-eq-decl nil group "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (left_coset_one formula-decl nil cosets "algebra/") (monoid? const-decl "bool" monoid_def "algebra/") (monad? const-decl "bool" monad_def "algebra/") (member const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil)) nil)) (first_isomorphism_th_TCC4 0 (first_isomorphism_th_TCC4-1 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) ((one1 formal-const-decl "T1" homomorphism_lemmas nil) (* formal-const-decl "[T1, T1 -> T1]" homomorphism_lemmas nil) (T1 formal-type-decl nil homomorphism_lemmas nil) (left_cosets_group formula-decl nil factor_groups "algebra/") (homomorphism type-eq-decl nil homomorphisms "algebra/") (homomorphism? const-decl "bool" homomorphisms "algebra/") (one2 formal-const-decl "T2" homomorphism_lemmas nil) (O formal-const-decl "[T2, T2 -> T2]" homomorphism_lemmas nil) (T2 formal-type-decl nil homomorphism_lemmas nil) (kernel_normal formula-decl nil homomorphism_lemmas nil) (G!1 skolem-const-decl "group[T1, *, one1]" homomorphism_lemmas nil) (K!1 skolem-const-decl "subgroup[T1, *, one1](G!1)" homomorphism_lemmas nil) (subgroup type-eq-decl nil group "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (normal_subgroup type-eq-decl nil normal_subgroups "algebra/") (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (first_isomorphism_th 0 (first_isomorphism_th-1 nil 3524797650 ("" (skosimp*) (("" (skoletin* 1) (("1" (expand "isomorphic?") (("1" (inst 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" (inst -1 "G!1" "K" "lc_gen(G!1, K, x1!1)" "lc_gen(G!1, K, x2!1)") (("1" (assert) (("1" (inst 1 "inv[T1, *, one1](lc_gen(G!1, K, x2!1)) * lc_gen(G!1, K, x1!1)") (("1" (lemma "inv_right[T1, *, one1]") (("1" (inst?) (("1" (rewrite "assoc[T1, *, one1]") (("1" (replaces -1) (("1" (rewrite "one_left[T1,*,one1]") nil nil)) nil)) nil)) nil)) nil) ("2" (expand "K" 1) (("2" (expand "kernel" 1 1) (("2" (prop) (("1" (replace -2 1 rl) (("1" (hide (- 2)) (("1" (typepred "lc_gen[T1, *, one1](G!1, K, x2!1)") (("1" (typepred "lc_gen[T1, *, one1](G!1, K, x1!1)") (("1" (hide (-2 -4)) (("1" (lemma "inv_in[T1, *, one1]") (("1" (inst -1 "G!1" "lc_gen[T1, *, one1](G!1, K, x2!1)") (("1" (typepred "G!1") (("1" (expand "group?") (("1" (flatten) (("1" (expand "monoid?") (("1" (flatten) (("1" (expand "monad?") (("1" (flatten) (("1" (hide-all-but (-1 -6 -7 1)) (("1" (expand "star_closed?") (("1" (inst?) (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "phi!1") (("2" (expand "homomorphism?") (("2" (inst?) (("1" (rewrite "homo_inv") (("1" (replace -3 * rl) (("1" (replaces -2) (("1" (rewrite "inv_left[T2, o, one2]") nil nil)) nil)) nil)) nil) ("2" (hide (-1 2 3)) (("2" (replace -1 1 rl) (("2" (typepred "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" (skosimp) (("2" (inst 1 "*[T1, *, one1](x!1, K)") (("1" (expand "restrict") (("1" (typepred "lc_gen(G!1, K, *[T1, *, one1](x!1, K))") (("1" (lemma "lc_eq[T1, *, one1]") (("1" (inst -1 "G!1" "K" "x!1" "lc_gen(G!1, K, *[T1, *, one1](x!1, K))") (("1" (assert) (("1" (skosimp*) (("1" (typepred "h!1") (("1" (expand "K" -1) (("1" (expand "kernel" -1) (("1" (flatten) (("1" (replace -3 -7) (("1" (replace -7 1) (("1" (typepred "phi!1") (("1" (expand "homomorphism?") (("1" (inst?) (("1" (replaces -1) (("1" (replaces -2) (("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" (prop) (("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" (typepred "lc_gen(G!1, K, mult(G!1, K)(a!1, b!1))") (("2" (typepred "a!1") (("2" (typepred "b!1") (("2" (skosimp*) (("2" (name-replace "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" (lemma "lc_eq[T1, *, one1]") (("2" (inst -1 "G!1" "K" "a!3 * a!2" "J") (("2" (assert) (("2" (skosimp) (("2" (lemma "divby_r[T1,*,one1]") (("1" (inst?) (("1" (assert) (("1" (replace -1 1 rl) (("1" (typepred "lc_gen(G!1, K, a!1)") (("1" (replace -7 -2) (("1" (lemma "lc_eq[T1, *, one1]") (("1" (inst?) (("1" (inst -1 "G!1") (("1" (assert) (("1" (skosimp) (("1" (lemma "divby_r[T1,*,one1]") (("1" (inst?) (("1" (assert) (("1" (replace -9 1) (("1" (replace -1 1 rl) (("1" (typepred "lc_gen(G!1, K, b!1)") (("1" (replace -9 -2) (("1" (lemma "lc_eq[T1, *, one1]") (("1" (inst?) (("1" (inst -1 "G!1") (("1" (assert) (("1" (skosimp) (("1" (lemma "divby_r[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (replace -11 1) (("1" (replace -1 1 rl) (("1" (hide-all-but 1) (("1" (typepred "h!1") (("1" (typepred "h!2") (("1" (typepred "h!3") (("1" (expand* "K" "kernel") (("1" (flatten) (("1" (lemma "inv_in[T1, *, one1]") (("1" (copy -1) (("1" (copy -1) (("1" (inst -1 "G!1" "h!1") (("1" (inst -2 "G!1" "h!2") (("1" (inst -3 "G!1" "h!3") (("1" (lemma "homo_inv") (("1" (copy -1) (("1" (copy -1) (("1" (inst -1 "G!1" "GP!1" "phi!1" "h!1") (("1" (inst -2 "G!1" "GP!1" "phi!1" "h!2") (("1" (inst -3 "G!1" "GP!1" "phi!1" "h!3") (("1" (replace -12 -1) (("1" (replace -10 -2) (("1" (replace -8 -3) (("1" (rewrite "inv_one[T2,o,one2]") (("1" (typepred "phi!1") (("1" (expand "homomorphism?") (("1" (copy -1) (("1" (copy -1) (("1" (copy -1) (("1" (inst -1 "a!3 * a!2" "inv[T1, *, one1](h!1)") (("1" (inst -2 "a!3" "a!2") (("1" (inst -3 "a!3" "inv[T1, *, one1](h!2)") (("1" (inst -4 "a!2" "inv[T1, *, one1](h!3)") (("1" (replaces -1) (("1" (replaces -1) (("1" (replaces -1) (("1" (replaces -1) (("1" (replaces -1) (("1" (replaces -1) (("1" (replaces -1) (("1" (hide-all-but 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" (hide-all-but 1) (("2" (typepred "a!2" "a!3" "G!1") (("2" (expand "group?") (("2" (flatten) (("2" (expand "monoid?") (("2" (flatten) (("2" (expand "monad?") (("2" (flatten) (("2" (hide (-4 -5 -6 -7)) (("2" (expand "star_closed?") (("2" (inst?) (("2" (expand "member") (("2" (propax) 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" (hide-all-but 1) (("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) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (T1 formal-type-decl nil homomorphism_lemmas nil) (set type-eq-decl nil sets nil) (* formal-const-decl "[T1, T1 -> T1]" homomorphism_lemmas nil) (one1 formal-const-decl "T1" homomorphism_lemmas nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (subgroup type-eq-decl nil group "algebra/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (T2 formal-type-decl nil homomorphism_lemmas nil) (O formal-const-decl "[T2, T2 -> T2]" homomorphism_lemmas nil) (one2 formal-const-decl "T2" homomorphism_lemmas nil) (homomorphism? const-decl "bool" homomorphisms "algebra/") (homomorphism type-eq-decl nil homomorphisms "algebra/") (kernel const-decl "subgroup[T1, *, one1](G)" homomorphisms "algebra/") (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/") (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (image const-decl "set[R]" function_image nil) (restrict const-decl "R" restrict nil) (* const-decl "set[T]" cosets "algebra/") (left_cosets type-eq-decl nil cosets "algebra/") (normal_subgroup type-eq-decl nil normal_subgroups "algebra/") (mult const-decl "left_cosets(G, H)" factor_groups "algebra/") (fullset const-decl "set" sets nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (isomorphic? const-decl "bool" homomorphisms "algebra/") (/ const-decl "group[left_cosets(G, N), mult(G, N), N]" right_left_cosets nil) (G!1 skolem-const-decl "group[T1, *, one1]" homomorphism_lemmas nil) (K skolem-const-decl "subgroup[T1, *, one1](G!1)" homomorphism_lemmas nil) (GP!1 skolem-const-decl "group[T2, o, one2]" homomorphism_lemmas nil) (phi!1 skolem-const-decl "homomorphism[T1, *, one1, T2, o, one2](G!1, GP!1)" homomorphism_lemmas nil) (lc_gen const-decl "{a: T | G(a) AND lc = a * H}" cosets "algebra/") (lc_is_eq formula-decl nil cosets "algebra/") (inv_in formula-decl nil group "algebra/") (star_closed? const-decl "bool" groupoid_def "algebra/") (member const-decl "bool" sets nil) (monad? const-decl "bool" monad_def "algebra/") (monoid? const-decl "bool" monoid_def "algebra/") (NOT const-decl "[bool -> bool]" booleans nil) (homo_inv formula-decl nil homomorphism_lemmas nil) (inv_left formula-decl nil group "algebra/") (inv_right formula-decl nil group "algebra/") (assoc formula-decl nil group "algebra/") (one_left formula-decl nil group "algebra/") (x1!1 skolem-const-decl "(G!1 / K)" homomorphism_lemmas nil) (x2!1 skolem-const-decl "(G!1 / K)" homomorphism_lemmas nil) (inv const-decl "{y | x * y = one AND y * x = one}" group "algebra/") (injective? const-decl "bool" functions nil) (x!1 skolem-const-decl "(restrict[T1, (G!1), boolean](G!1))" homomorphism_lemmas nil) (one_right formula-decl nil group "algebra/") (lc_eq formula-decl nil cosets "algebra/") (left_cosets const-decl "setofsets[T]" right_left_cosets nil) (surjective? const-decl "bool" functions nil) (divby_r formula-decl nil groups_scaf nil) (h!3 skolem-const-decl "(K)" homomorphism_lemmas nil) (h!2 skolem-const-decl "(K)" homomorphism_lemmas nil) (a!2 skolem-const-decl "(G!1)" homomorphism_lemmas nil) (a!3 skolem-const-decl "(G!1)" homomorphism_lemmas nil) (h!1 skolem-const-decl "(K)" homomorphism_lemmas nil) (inv_one formula-decl nil group "algebra/") (T1_is_group formula-decl nil homomorphism_lemmas nil) (mult_lem formula-decl nil factor_groups "algebra/") (isomorphism? const-decl "bool" homomorphisms "algebra/") (x1!1 skolem-const-decl "(G!1 / K)" homomorphism_lemmas nil) (kernel_normal formula-decl nil homomorphism_lemmas nil) (A!1 skolem-const-decl "left_cosets[T1, *, one1](G!1, K)" homomorphism_lemmas nil)) shostak)))
¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.182Bemerkung: (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-27) ¤*Eine klare Vorstellung vom Zielzustand |
|
||||||||||||||
2026-05-26