| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/groups/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 355 kB |
|
Quelle isomorphism_theorems.prfSprache: Lisp |
|||||||||||||||
|
(isomorphism_theorems (G_TCC1 0 (G_TCC1-1 nil 3530909168 ("" (rewrite "T1_is_group") nil nil) ((T1_is_group formula-decl nil isomorphism_theorems nil)) nil)) (GP_TCC1 0 (GP_TCC1-1 nil 3530909168 ("" (rewrite "T2_is_group") nil nil) ((T2_is_group formula-decl nil isomorphism_theorems nil)) nil)) (quotient_subgroup_TCC1 0 (quotient_subgroup_TCC1-1 nil 3524781199 ("" (skosimp*) (("" (lemma "normal_subgroup_tran[T1, *, one1]") (("1" (inst -1 "G!1" "M!1" "N!1") (("1" (assert) (("1" (typepred "M!1") (("1" (expand "normal_subgroup?") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite "G_TCC1") nil nil)) nil)) nil) ((one1 formal-const-decl "T1" isomorphism_theorems nil) (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems nil) (T1 formal-type-decl nil isomorphism_theorems nil) (normal_subgroup_tran formula-decl nil groups_scaf nil) (fullset const-decl "set" sets nil) (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) (NOT const-decl "[bool -> bool]" booleans 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/") (G_TCC1 assuming-tcc nil isomorphism_theorems nil)) nil)) (quotient_subgroup_TCC2 0 (quotient_subgroup_TCC2-1 nil 3524781199 ("" (skosimp*) (("" (prop) (("1" (skosimp) (("1" (inst 1 "a!1") (("1" (hide -) (("1" (typepred "a!1" "M!1") (("1" (expand* "normal_subgroup?" "subgroup?") (("1" (flatten) (("1" (expand* "subset?" "member") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (inst 1 "lc_gen(M!1, N!1, x!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((T1 formal-type-decl nil isomorphism_theorems 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]" isomorphism_theorems nil) (one1 formal-const-decl "T1" isomorphism_theorems 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/") (a!1 skolem-const-decl "(M!1)" isomorphism_theorems nil) (M!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)" isomorphism_theorems nil) (G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems nil) (NOT const-decl "[bool -> bool]" booleans nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (subgroup? const-decl "bool" group_def "algebra/") (N!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)" isomorphism_theorems nil) (subgroup type-eq-decl nil group "algebra/") (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "set[T]" cosets "algebra/") (left_cosets type-eq-decl nil cosets "algebra/") (AND const-decl "[bool, bool -> bool]" booleans nil) (lc_gen const-decl "{a: T | G(a) AND lc = a * H}" cosets "algebra/")) nil)) (quotient_subgroup_TCC3 0 (quotient_subgroup_TCC3-1 nil 3524781199 ("" (skosimp*) (("" (inst 1 "one1") (("1" (rewrite "left_coset_one[T1,*,one1]") nil nil) ("2" (typepred "G!1") (("2" (expand* "group?" "monoid?" "monad?" "member") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil) ((G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems nil) (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one1 formal-const-decl "T1" isomorphism_theorems nil) (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems 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 isomorphism_theorems 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)) (quotient_subgroup_TCC4 0 (quotient_subgroup_TCC4-1 nil 3524781199 ("" (skosimp*) (("" (inst 1 "N!1") (("" (inst 1 "one1") (("1" (rewrite "left_coset_one[T1,*,one1]") nil nil) ("2" (typepred "G!1") (("2" (expand* "group?" "monoid?" "monad?" "member") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) ((T1 formal-type-decl nil isomorphism_theorems 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]" isomorphism_theorems nil) (one1 formal-const-decl "T1" isomorphism_theorems nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "set[T]" cosets "algebra/") (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/") (normal_subgroup type-eq-decl nil normal_subgroups "algebra/") (left_cosets type-eq-decl nil cosets "algebra/") (N!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)" isomorphism_theorems nil) (G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems nil) (NOT const-decl "[bool -> bool]" booleans nil) (monad? const-decl "bool" monad_def "algebra/") (member const-decl "bool" sets nil) (monoid? const-decl "bool" monoid_def "algebra/") (left_coset_one formula-decl nil cosets "algebra/")) nil)) (quotient_subgroup 0 (quotient_subgroup-1 nil 3524784283 ("" (skosimp*) (("" (expand "subgroup?") (("" (prop) (("1" (hide -1) (("1" (expand* "subset?" "member") (("1" (skosimp*) (("1" (expand "/") (("1" (expand "restrict") (("1" (expand "left_cosets") (("1" (skosimp) (("1" (inst?) (("1" (hide -1) (("1" (typepred "a!1" "M!1") (("1" (expand* "normal_subgroup?" "subgroup?" "subset?" "member") (("1" (flatten) (("1" (hide (-2 -4)) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (expand "group?") (("2" (prop) (("1" (expand "monoid?") (("1" (prop) (("1" (expand "monad?") (("1" (prop) (("1" (expand "star_closed?") (("1" (skosimp*) (("1" (expand "member") (("1" (expand "/") (("1" (expand "restrict") (("1" (expand "left_cosets") (("1" (typepred "x!1" "y!1") (("1" (hide (-2 -4)) (("1" (skosimp*) (("1" (inst 1 "a!1 * a!2") (("1" (replaces -1) (("1" (replaces -1) (("1" (lemma "mult_lem[T1, *, one1]") (("1" (inst?) (("1" (hide 2) (("1" (typepred "a!2" "M!1") (("1" (expand* "normal_subgroup?" "subgroup?" "subset?" "member") (("1" (flatten) (("1" (hide (-2 -4)) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "a!1" "M!1") (("2" (expand* "normal_subgroup?" "subgroup?" "subset?" "member") (("2" (flatten) (("2" (hide (-2 -4)) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 -2)) (("2" (rewrite "product_in[T1, *, one1]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand* "member" "/" "left_cosets") (("2" (expand "restrict") (("2" (typepred "M!1") (("2" (expand* "group?" "monoid?" "monad?" "member") (("2" (flatten) (("2" (hide-all-but (-2 1)) (("2" (inst 1 "one1") (("2" (rewrite "left_coset_one") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "identity?") (("3" (skosimp*) (("3" (expand "restrict") (("3" (lemma "N_is_identity[T1, *, one1]") (("3" (inst?) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (typepred "x!1") (("2" (skosimp*) (("2" (inst?) (("2" (hide -) (("2" (typepred "a!1" "M!1") (("2" (expand* "normal_subgroup?" "subgroup?" "subset?" "member") (("2" (flatten) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "associative?") (("2" (expand "restrict") (("2" (skosimp*) (("2" (typepred "z!1") (("2" (typepred "y!1") (("2" (typepred "x!1") (("2" (skosimp*) (("2" (replace -1) (("2" (hide -1) (("2" (replace -2) (("2" (hide -2) (("2" (replace -3) (("2" (hide -3) (("2" (rewrite "mult_lem[T1, *, one1]") (("1" (rewrite "mult_lem[T1, *, one1]") (("1" (rewrite "mult_lem[T1, *, one1]") (("1" (rewrite "mult_lem[T1, *, one1]") (("1" (rewrite "assoc[T1, *, one1]") nil nil) ("2" (hide-all-but 1) (("2" (typepred "a!2" "a!3" "G!1" "M!1") (("2" (expand "normal_subgroup?") (("2" (flatten) (("2" (expand "subgroup?") (("2" (expand "subset?") (("2" (hide (-4 -6)) (("2" (copy -4) (("2" (inst -1 "a!2") (("2" (inst -5 "a!3") (("2" (expand "member") (("2" (expand* "group?" "monoid?" "monad?") (("2" (flatten) (("2" (hide-all-but (-1 -4 -9 1)) (("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) ("3" (hide-all-but 1) (("3" (typepred "a!1" "M!1") (("3" (expand* "normal_subgroup?" "subgroup?" "subset?" "member") (("3" (flatten) (("3" (hide (-2 -4)) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "a!3" "M!1") (("2" (expand* "normal_subgroup?" "subgroup?" "subset?" "member") (("2" (flatten) (("2" (hide (-2 -4)) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (typepred "a!2" "M!1") (("3" (expand* "normal_subgroup?" "subgroup?" "subset?" "member") (("3" (flatten) (("3" (hide (-2 -4)) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "a!3" "M!1") (("2" (expand* "normal_subgroup?" "subgroup?" "subset?" "member") (("2" (flatten) (("2" (hide (-2 -4)) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (typepred "a!1" "a!2" "G!1" "M!1") (("3" (expand "normal_subgroup?") (("3" (flatten) (("3" (expand "subgroup?") (("3" (expand "subset?") (("3" (hide (-4 -6)) (("3" (copy -4) (("3" (inst -1 "a!1") (("3" (inst -5 "a!2") (("3" (expand "member") (("3" (expand* "group?" "monoid?" "monad?") (("3" (flatten) (("3" (hide-all-but (-1 -4 -9 1)) (("3" (expand "star_closed?") (("3" (inst?) (("3" (expand "member") (("3" (propax) 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" (typepred "a!2" "M!1") (("2" (expand* "normal_subgroup?" "subgroup?" "subset?" "member") (("2" (flatten) (("2" (hide (-2 -4)) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (typepred "a!1" "M!1") (("3" (expand* "normal_subgroup?" "subgroup?" "subset?" "member") (("3" (flatten) (("3" (hide (-2 -4)) (("3" (inst?) (("3" (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) ("2" (expand "inv_exists?") (("2" (skosimp*) (("2" (typepred "x!1") (("2" (skosimp*) (("2" (inst 1 "*[T1, *, one1](inv[T1, *, one1](a!1), N!1)") (("1" (replace -1) (("1" (hide -1) (("1" (rewrite "mult_lem[T1, *, one1]") (("1" (rewrite "mult_lem[T1, *, one1]") (("1" (rewrite "inv_right[T1, *, one1]") (("1" (rewrite "inv_left[T1, *, one1]") (("1" (rewrite "left_coset_one") nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "a!1" "M!1") (("2" (expand* "normal_subgroup?" "subgroup?" "subset?" "member") (("2" (flatten) (("2" (hide (-2 -4)) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (typepred "a!1" "M!1") (("3" (expand* "normal_subgroup?" "subgroup?" "subset?" "member") (("3" (flatten) (("3" (hide (-2 -4)) (("3" (inst?) (("3" (assert) (("3" (rewrite "inv_in[T1, *, one1]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "a!1" "M!1") (("2" (expand* "normal_subgroup?" "subgroup?" "subset?" "member") (("2" (flatten) (("2" (hide (-2 -4)) (("2" (inst?) (("2" (assert) (("2" (rewrite "inv_in[T1, *, one1]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (typepred "a!1" "M!1") (("3" (expand* "normal_subgroup?" "subgroup?" "subset?" "member") (("3" (flatten) (("3" (hide (-2 -4)) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (prop) (("1" (expand "*") (("1" (inst + "inv[T1, *, one1](a!1)") (("1" (rewrite "inv_in[T1, *, one1]") nil nil)) nil)) nil) ("2" (expand "/") (("2" (hide -2) (("2" (expand "restrict") (("2" (expand "left_cosets") (("2" (inst 1 "inv[T1, *, one1](a!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)) nil) ((subgroup? const-decl "bool" group_def "algebra/") (a!1 skolem-const-decl "(M!1)" isomorphism_theorems nil) (a!2 skolem-const-decl "(M!1)" isomorphism_theorems nil) (mult_lem formula-decl nil factor_groups "algebra/") (product_in formula-decl nil group "algebra/") (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "set[T]" cosets "algebra/") (left_cosets type-eq-decl nil cosets "algebra/") (mult const-decl "left_cosets(G, H)" factor_groups "algebra/") (star_closed? const-decl "bool" groupoid_def "algebra/") (left_coset_one formula-decl nil cosets "algebra/") (N_is_identity formula-decl nil factor_groups "algebra/") (a!1 skolem-const-decl "(M!1)" isomorphism_theorems nil) (N!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)" isomorphism_theorems nil) (x!1 skolem-const-decl "(M!1 / N!1)" isomorphism_theorems nil) (identity? const-decl "bool" operator_defs nil) (monad? const-decl "bool" monad_def "algebra/") (a!1 skolem-const-decl "(M!1)" isomorphism_theorems nil) (a!3 skolem-const-decl "(M!1)" isomorphism_theorems nil) (a!2 skolem-const-decl "(M!1)" isomorphism_theorems nil) (assoc formula-decl nil group "algebra/") (associative? const-decl "bool" operator_defs nil) (monoid? const-decl "bool" monoid_def "algebra/") (inv_in formula-decl nil group "algebra/") (inv_right formula-decl nil group "algebra/") (inv_left formula-decl nil group "algebra/") (AND const-decl "[bool, bool -> bool]" booleans nil) (inv const-decl "{y | x * y = one AND y * x = one}" group "algebra/") (a!1 skolem-const-decl "(M!1)" isomorphism_theorems nil) (inv_exists? const-decl "bool" group_def "algebra/") (restrict const-decl "R" restrict nil) (NOT const-decl "[bool -> bool]" booleans nil) (G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems nil) (M!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)" isomorphism_theorems nil) (a!1 skolem-const-decl "(M!1)" isomorphism_theorems 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" isomorphism_theorems nil) (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems 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 isomorphism_theorems nil) (left_cosets const-decl "setofsets[T]" right_left_cosets nil) (/ const-decl "group[left_cosets(G, N), mult(G, N), N]" right_left_cosets nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil)) shostak)) (second_isomorphism_th_aux_TCC1 0 (second_isomorphism_th_aux_TCC1-1 nil 3524841142 ("" (skosimp*) (("" (replaces -1) (("" (lemma "HK_subgroup[T1, *, one1]") (("" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) (("1" (lemma "HK_subgroup_permute[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (expand "subgroup?") (("1" (propax) nil nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((N!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)" isomorphism_theorems nil) (normal_subgroup type-eq-decl nil normal_subgroups "algebra/") (G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems nil) (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (subgroup? const-decl "bool" group_def "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) (subgroup type-eq-decl nil group "algebra/") (HK_subgroup_permute formula-decl nil products_subgroups nil) (NOT const-decl "[bool -> bool]" booleans nil) (HK_subgroup formula-decl nil products_subgroups nil) (T1 formal-type-decl nil isomorphism_theorems nil) (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems nil) (one1 formal-const-decl "T1" isomorphism_theorems nil)) nil)) (second_isomorphism_th_aux_TCC2 0 (second_isomorphism_th_aux_TCC2-1 nil 3524841142 ("" (skosimp*) (("" (replaces -2) (("" (replaces -1) (("" (lemma "HK_subgroup[T1, *, one1]") (("" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) (("1" (lemma "HK_subgroup_permute[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (lemma "H_K_are_subgroups[T1, *, one1]") (("1" (inst?) (("1" (prop) (("1" (hide -2) (("1" (lemma "normal_subgroup_tran[T1, *, one1]") (("1" (inst -1 "G!1" "prod[T1, *, one1](N!1, H!1)" "N!1") (("1" (assert) nil nil)) nil) ("2" (rewrite "G_TCC1") nil nil)) nil)) nil) ("2" (expand "subgroup?") (("2" (assert) nil nil)) nil)) nil) ("2" (typepred "N!1") (("2" (expand "normal_subgroup?" -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((N!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)" isomorphism_theorems nil) (normal_subgroup type-eq-decl nil normal_subgroups "algebra/") (G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems nil) (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (subgroup? const-decl "bool" group_def "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) (subgroup type-eq-decl nil group "algebra/") (HK_subgroup_permute formula-decl nil products_subgroups nil) (H_K_are_subgroups formula-decl nil products_subgroups nil) (NOT const-decl "[bool -> bool]" booleans nil) (normal_subgroup_tran formula-decl nil groups_scaf nil) (fullset const-decl "set" sets nil) (prod const-decl "set[T]" products_subgroups nil) (G_TCC1 assuming-tcc nil isomorphism_theorems nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (HK_subgroup formula-decl nil products_subgroups nil) (T1 formal-type-decl nil isomorphism_theorems nil) (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems nil) (one1 formal-const-decl "T1" isomorphism_theorems nil)) nil)) (second_isomorphism_th_aux_TCC3 0 (second_isomorphism_th_aux_TCC3-1 nil 3524841142 ("" (skosimp*) (("" (inst 1 "one1") (("1" (rewrite "left_coset_one") nil nil) ("2" (replaces -1) (("2" (lemma "HK_subgroup[T1, *, one1]") (("2" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) (("1" (lemma "HK_subgroup_permute[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (expand* "subgroup?" "group?" "monoid?" "monad?" "member") nil nil)) nil)) nil) ("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((one1 formal-const-decl "T1" isomorphism_theorems nil) (NH!1 skolem-const-decl "set[T1]" isomorphism_theorems 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 isomorphism_theorems nil) (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems 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/") (left_coset_one formula-decl nil cosets "algebra/") (HK_subgroup formula-decl nil products_subgroups nil) (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) (HK_subgroup_permute formula-decl nil products_subgroups nil) (subgroup type-eq-decl nil group "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems nil) (N!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)" isomorphism_theorems nil)) nil)) (second_isomorphism_th_aux_TCC4 0 (second_isomorphism_th_aux_TCC4-1 nil 3524841142 ("" (skosimp*) (("" (rewrite "left_cosets_group[T1, *, one1]") (("1" (hide 2) (("1" (replaces -1) (("1" (lemma "HK_subgroup[T1, *, one1]") (("1" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) (("1" (lemma "HK_subgroup_permute[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (lemma "H_K_are_subgroups[T1, *, one1]") (("1" (inst?) (("1" (prop) (("1" (hide -2) (("1" (lemma "normal_subgroup_tran[T1, *, one1]") (("1" (inst -1 "G!1" "prod[T1, *, one1](N!1, H!1)" "N!1") (("1" (assert) nil nil)) nil) ("2" (rewrite "G_TCC1") nil nil)) nil)) nil) ("2" (expand "subgroup?") (("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (replaces -1) (("2" (lemma "HK_subgroup[T1, *, one1]") (("2" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) (("1" (lemma "HK_subgroup_permute[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (expand* "subgroup?" "group?" "monoid?" "monad?" "member" -1) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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 isomorphism_theorems nil) (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems nil) (one1 formal-const-decl "T1" isomorphism_theorems nil) (N!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)" isomorphism_theorems nil) (G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems nil) (subgroup? const-decl "bool" group_def "algebra/") (subgroup type-eq-decl nil group "algebra/") (HK_subgroup_permute formula-decl nil products_subgroups nil) (H_K_are_subgroups formula-decl nil products_subgroups nil) (NOT const-decl "[bool -> bool]" booleans nil) (normal_subgroup_tran formula-decl nil groups_scaf nil) (fullset const-decl "set" sets nil) (prod const-decl "set[T]" products_subgroups nil) (G_TCC1 assuming-tcc nil isomorphism_theorems nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (HK_subgroup formula-decl nil products_subgroups nil)) nil)) (second_isomorphism_th_aux 0 (second_isomorphism_th_aux-1 nil 3524852278 ("" (skosimp*) (("" (expand "homomorphism?") (("" (inst 1 "(LAMBDA (x: (H!1)): *[T1, *, one1](x, N!1))") (("1" (prop) (("1" (skosimp*) (("1" (rewrite "mult_lem[T1, *, one1]") (("1" (hide 2) (("1" (typepred "b!1") (("1" (expand "prod") (("1" (inst 1 "one1" "b!1") (("1" (rewrite "one_left[T1, *, one1]") nil nil) ("2" (typepred "N!1") (("2" (expand* "group?" "monoid?" "monad?" "member") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "a!1") (("2" (expand "prod") (("2" (inst 1 "one1" "a!1") (("1" (rewrite "one_left[T1, *, one1]") nil nil) ("2" (typepred "N!1") (("2" (expand* "group?" "monoid?" "monad?" "member") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "surjective?") (("2" (skosimp*) (("2" (typepred "y!1") (("2" (skosimp) (("2" (typepred "a!1") (("2" (hide -3) (("2" (expand "prod" -1) (("2" (skosimp) (("2" (typepred "k!1") (("2" (typepred "h!1") (("2" (replaces -4) (("2" (lemma "normal_left_is_right[T1, *, one1]") (("2" (inst -1 "G!1" "N!1") (("2" (assert) (("2" (flatten) (("2" (inst -2 "a!1") (("1" (replaces -2) (("1" (replaces -4) (("1" (inst 1 "k!1") (("1" (lemma "normal_left_is_right[T1, *, one1]") (("1" (inst -1 "G!1" "N!1") (("1" (assert) (("1" (inst -1 "k!1") (("1" (replaces -1) (("1" (hide-all-but 1) (("1" (lemma "rc_is_eq[T1, *, one1]") (("1" (inst -1 "G!1" "N!1" "one1" "h!1") (("1" (assert) (("1" (prop) (("1" (rewrite "right_coset_one") (("1" (lemma "right_coset_assoc[T1, *, one1]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (inst 1 "inv[T1, *, one1](h!1)") (("1" (rewrite "inv_left[T1, *, one1]") nil nil) ("2" (hide 2) (("2" (typepred "h!1") (("2" (rewrite "inv_in") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "H!1") (("2" (hide-all-but (-2 -5 1)) (("2" (expand "subgroup?") (("2" (expand* "subset?" "member") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replaces -4) (("2" (hide (- 2)) (("2" (typepred "h!1" "k!1" "N!1" "H!1") (("2" (expand* "normal_subgroup?" "subgroup?" "subset?" "member") (("2" (flatten) (("2" (hide (-3 -5 -6)) (("2" (inst -3 "h!1") (("2" (inst -4 "k!1") (("2" (assert) (("2" (rewrite "product_in[T1, *, one1]") 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) ("3" (decompose-equality 1) (("1" (iff) (("1" (prop) (("1" (expand* "kernel" "intersection") (("1" (expand "member") (("1" (prop) (("1" (lemma "lc_eq[T1, *, one1]") (("1" (inst -1 "G!1" "N!1" "x!1" "one1") (("1" (assert) (("1" (rewrite "left_coset_one") (("1" (assert) (("1" (prop) (("1" (skosimp) (("1" (rewrite "one_left[T1, *, one1]") (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand* "intersection" "kernel") (("2" (expand "member") (("2" (flatten) (("2" (assert) (("2" (lemma "lc_is_eq[T1, *, one1]") (("2" (inst -1 "G!1" "N!1" "x!1" "one1") (("2" (prop) (("1" (rewrite "left_coset_one") nil nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (inst 1 "x!1") (("3" (rewrite "one_left[T1, *, one1]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "left_cosets_group[T1, *, one1]") (("1" (hide 2) (("1" (lemma "HK_subgroup[T1, *, one1]") (("1" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) (("1" (lemma "HK_subgroup_permute[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (lemma "normal_subgroup_tran[T1, *, one1]") (("1" (inst -1 "G!1" "prod[T1, *, one1](N!1, H!1)" "N!1") (("1" (assert) (("1" (expand "subgroup?" -1) (("1" (flatten) (("1" (hide -1) (("1" (lemma "H_K_are_subgroups[T1, *, one1]") (("1" (inst?) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "T1_is_group") nil nil)) nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "HK_subgroup[T1, *, one1]") (("2" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) (("1" (lemma "HK_subgroup_permute[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (expand "subgroup?") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (rewrite "T1_is_group") nil nil) ("4" (inst 1 "one1") (("1" (rewrite "left_coset_one") nil nil) ("2" (lemma "HK_subgroup[T1, *, one1]") (("2" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) (("1" (lemma "HK_subgroup_permute[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (expand "subgroup?") (("1" (flatten) (("1" (hide -1) (("1" (expand* "group?" "monoid?" "monad?" "member") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (expand "homomorphism?") (("5" (skosimp*) (("5" (rewrite "mult_lem[T1, *, one1]") (("1" (hide 2) (("1" (typepred "b!1") (("1" (lemma "HK_subgroup[T1, *, one1]") (("1" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) (("1" (expand "subgroup?") (("1" (flatten) (("1" (lemma "H_K_are_subgroups[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (lemma "HK_subgroup_permute[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (hide-all-but (-1 -5 1)) (("1" (expand* "subgroup?" "subset?" "member") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "a!1") (("2" (lemma "HK_subgroup[T1, *, one1]") (("2" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) (("1" (expand "subgroup?") (("1" (flatten) (("1" (hide -1) (("1" (lemma "H_K_are_subgroups[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (hide -2) (("1" (lemma "HK_subgroup_permute[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (expand* "subgroup?" "subset?" "member") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (skosimp*) (("6" (prop) (("1" (inst 1 "x!1") (("1" (typepred "x!1") (("1" (lemma "HK_subgroup[T1, *, one1]") (("1" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) (("1" (expand "subgroup?") (("1" (flatten) (("1" (hide -1) (("1" (lemma "H_K_are_subgroups[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (hide -2) (("1" (lemma "HK_subgroup_permute[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (expand* "subgroup?" "subset?" "member") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "/") (("2" (expand "restrict") (("2" (expand "left_cosets") (("2" (inst 1 "x!1") (("2" (lemma "HK_subgroup[T1, *, one1]") (("2" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) (("1" (expand "subgroup?") (("1" (flatten) (("1" (hide -1) (("1" (lemma "H_K_are_subgroups[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (hide -2) (("1" (lemma "HK_subgroup_permute[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (expand* "subgroup?" "subset?" "member") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (prop) (("1" (inst 1 "x!1") (("1" (lemma "HK_subgroup[T1, *, one1]") (("1" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) (("1" (expand "subgroup?") (("1" (flatten) (("1" (hide -1) (("1" (lemma "H_K_are_subgroups[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (hide -2) (("1" (lemma "HK_subgroup_permute[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (expand* "subgroup?" "subset?" "member") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "/") (("2" (expand "restrict") (("2" (expand "left_cosets") (("2" (inst 1 "x!1") (("2" (lemma "HK_subgroup[T1, *, one1]") (("2" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) (("1" (expand "subgroup?") (("1" (flatten) (("1" (hide -1) (("1" (lemma "H_K_are_subgroups[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (hide -2) (("1" (lemma "HK_subgroup_permute[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (expand* "subgroup?" "subset?" "member") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((homomorphism? const-decl "bool" homomorphisms "algebra/") (x!1 skolem-const-decl "(H!1)" isomorphism_theorems nil) (mult_lem formula-decl nil factor_groups "algebra/") (NOT const-decl "[bool -> bool]" booleans nil) (one_left formula-decl nil group "algebra/") (monoid? const-decl "bool" monoid_def "algebra/") (member const-decl "bool" sets nil) (monad? const-decl "bool" monad_def "algebra/") (normal_left_is_right formula-decl nil normal_subgroups "algebra/") (a!1 skolem-const-decl "(prod[T1, *, one1](N!1, H!1))" isomorphism_theorems nil) (subset? const-decl "bool" sets nil) (rc_is_eq formula-decl nil cosets "algebra/") (inv const-decl "{y | x * y = one AND y * x = one}" group "algebra/") (h!1 skolem-const-decl "(N!1)" isomorphism_theorems nil) (inv_left formula-decl nil group "algebra/") (inv_in formula-decl nil group "algebra/") (right_coset_one formula-decl nil cosets "algebra/") (right_coset_assoc formula-decl nil cosets "algebra/") (k!1 skolem-const-decl "(H!1)" isomorphism_theorems nil) (product_in formula-decl nil group "algebra/") (surjective? const-decl "bool" functions nil) (left_cosets const-decl "setofsets[T]" right_left_cosets nil) (restrict const-decl "R" restrict nil) (x!1 skolem-const-decl "(H!1)" isomorphism_theorems nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (left_cosets_group formula-decl nil factor_groups "algebra/") (HK_subgroup formula-decl nil products_subgroups nil) (T1_is_group formula-decl nil isomorphism_theorems nil) (H_K_are_subgroups formula-decl nil products_subgroups nil) (normal_subgroup_tran formula-decl nil groups_scaf nil) (HK_subgroup_permute formula-decl nil products_subgroups nil) (lc_is_eq formula-decl nil cosets "algebra/") (left_coset_one formula-decl nil cosets "algebra/") (lc_eq formula-decl nil cosets "algebra/") (homomorphism type-eq-decl nil homomorphisms "algebra/") (kernel const-decl "subgroup[T1, *, one1](G)" homomorphisms "algebra/") (intersection const-decl "set" sets nil) (fullset const-decl "set" sets nil) (T1 formal-type-decl nil isomorphism_theorems 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]" isomorphism_theorems nil) (one1 formal-const-decl "T1" isomorphism_theorems nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems nil) (subgroup type-eq-decl nil group "algebra/") (H!1 skolem-const-decl "subgroup[T1, *, one1](G!1)" isomorphism_theorems nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (prod const-decl "set[T]" products_subgroups nil) (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/") (normal_subgroup type-eq-decl nil normal_subgroups "algebra/") (N!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)" isomorphism_theorems nil) (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "set[T]" cosets "algebra/") (left_cosets type-eq-decl nil cosets "algebra/") (mult const-decl "left_cosets(G, H)" factor_groups "algebra/") (/ const-decl "group[left_cosets(G, N), mult(G, N), N]" right_left_cosets nil)) shostak)) (second_isomorphism_th_TCC1 0 (second_isomorphism_th_TCC1-1 nil 3524769565 ("" (skosimp*) (("" (replaces -1) (("" (lemma "subgroup_intersection[T1, *, one1]") (("1" (inst -1 "G!1" "N!1" "H!1") (("1" (assert) (("1" (expand "subgroup?") (("1" (hide (-1 2)) (("1" (typepred "N!1") (("1" (expand "normal_subgroup?") (("1" (flatten) (("1" (hide -3) (("1" (expand "subgroup?") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "G_TCC1") nil nil)) nil)) nil)) nil) ((G_TCC1 assuming-tcc nil isomorphism_theorems nil) (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/") (subgroup? const-decl "bool" group_def "algebra/") (subgroup type-eq-decl nil group "algebra/") (NOT const-decl "[bool -> bool]" booleans nil) (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/") (fullset const-decl "set" sets nil) (subgroup_intersection formula-decl nil groups_scaf nil) (T1 formal-type-decl nil isomorphism_theorems nil) (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems nil) (one1 formal-const-decl "T1" isomorphism_theorems nil)) nil)) (second_isomorphism_th_TCC2 0 (second_isomorphism_th_TCC2-1 nil 3524769565 ("" (skosimp*) (("" (replaces -3) (("" (lemma "HK_subgroup[T1, *, one1]") (("" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) (("1" (lemma "HK_subgroup_permute[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (expand "subgroup?") (("1" (propax) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((one1 formal-const-decl "T1" isomorphism_theorems nil) (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems nil) (T1 formal-type-decl nil isomorphism_theorems nil) (HK_subgroup formula-decl nil products_subgroups nil) (NOT const-decl "[bool -> bool]" booleans nil) (HK_subgroup_permute formula-decl nil products_subgroups nil) (subgroup type-eq-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/") (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]" isomorphism_theorems nil) (normal_subgroup type-eq-decl nil normal_subgroups "algebra/") (N!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)" isomorphism_theorems nil)) nil)) (second_isomorphism_th_TCC3 0 (second_isomorphism_th_TCC3-1 nil 3524769565 ("" (skosimp*) (("" (replaces -3) (("" (hide -1) (("" (lemma "HK_subgroup[T1, *, one1]") (("" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) (("1" (lemma "HK_subgroup_permute[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (expand "subgroup?" -1) (("1" (flatten) (("1" (lemma "H_K_are_subgroups[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (prop) (("1" (hide -2) (("1" (lemma "normal_subgroup_tran[T1, *, one1]") (("1" (inst -1 "G!1" "prod[T1, *, one1](N!1, H!1)" "N!1") (("1" (assert) nil nil)) nil) ("2" (rewrite "G_TCC1") nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((N!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)" isomorphism_theorems nil) (normal_subgroup type-eq-decl nil normal_subgroups "algebra/") (G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems nil) (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (subgroup? const-decl "bool" group_def "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) (subgroup type-eq-decl nil group "algebra/") (HK_subgroup_permute formula-decl nil products_subgroups nil) (H_K_are_subgroups formula-decl nil products_subgroups nil) (NOT const-decl "[bool -> bool]" booleans nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (G_TCC1 assuming-tcc nil isomorphism_theorems nil) (prod const-decl "set[T]" products_subgroups nil) (fullset const-decl "set" sets nil) (normal_subgroup_tran formula-decl nil groups_scaf nil) (HK_subgroup formula-decl nil products_subgroups nil) (T1 formal-type-decl nil isomorphism_theorems nil) (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems nil) (one1 formal-const-decl "T1" isomorphism_theorems nil)) nil)) (second_isomorphism_th_TCC4 0 (second_isomorphism_th_TCC4-1 nil 3524769565 ("" (skosimp*) (("" (inst 1 "one1") (("1" (rewrite "left_coset_one") nil nil) ("2" (hide-all-but 1) (("2" (typepred "H!1") (("2" (expand* "group?" "monoid?" "monad?" "member") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((H!1 skolem-const-decl "subgroup[T1, *, one1](G!1)" isomorphism_theorems nil) (subgroup type-eq-decl nil group "algebra/") (G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems nil) (subgroup? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one1 formal-const-decl "T1" isomorphism_theorems nil) (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems 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 isomorphism_theorems nil) (normal_subgroup type-eq-decl nil normal_subgroups "algebra/") (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/") (intersection const-decl "set" sets nil) (left_coset_one formula-decl nil cosets "algebra/") (NOT const-decl "[bool -> bool]" booleans nil) (monad? const-decl "bool" monad_def "algebra/") (member const-decl "bool" sets nil) (monoid? const-decl "bool" monoid_def "algebra/")) nil)) (second_isomorphism_th_TCC5 0 (second_isomorphism_th_TCC5-1 nil 3524769565 ("" (skosimp*) (("" (inst 1 "one1") (("1" (rewrite "left_coset_one") nil nil) ("2" (lemma "HK_subgroup[T1, *, one1]") (("2" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) (("1" (expand "subgroup?") (("1" (flatten) (("1" (lemma "HK_subgroup_permute[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (expand* "group?" "monoid?" "monad?" "member") nil nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((one1 formal-const-decl "T1" isomorphism_theorems nil) (NH!1 skolem-const-decl "set[T1]" isomorphism_theorems 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 isomorphism_theorems nil) (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems 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/") (left_coset_one formula-decl nil cosets "algebra/") (N!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)" isomorphism_theorems nil) (G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems nil) (subgroup? const-decl "bool" group_def "algebra/") (subgroup type-eq-decl nil group "algebra/") (HK_subgroup_permute formula-decl nil products_subgroups nil) (NOT const-decl "[bool -> bool]" booleans nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (member const-decl "bool" sets nil) (monad? const-decl "bool" monad_def "algebra/") (monoid? const-decl "bool" monoid_def "algebra/") (HK_subgroup formula-decl nil products_subgroups nil)) nil)) (second_isomorphism_th_TCC6 0 (second_isomorphism_th_TCC6-1 nil 3524769565 ("" (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/") (subgroup? const-decl "bool" group_def "algebra/") (subgroup type-eq-decl nil group "algebra/") (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/") (normal_subgroup type-eq-decl nil normal_subgroups "algebra/") (intersection const-decl "set" sets nil) (T1 formal-type-decl nil isomorphism_theorems nil) (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems nil) (one1 formal-const-decl "T1" isomorphism_theorems nil)) nil)) (second_isomorphism_th_TCC7 0 (second_isomorphism_th_TCC7-1 nil 3524769565 ("" (skosimp*) (("" (rewrite "left_cosets_group[T1, *, one1]") (("1" (hide (-1 2)) (("1" (replaces -2) (("1" (lemma "HK_subgroup[T1, *, one1]") (("1" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) (("1" (lemma "HK_subgroup_permute[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (lemma "H_K_are_subgroups[T1, *, one1]") (("1" (inst?) (("1" (expand "subgroup?" -2) (("1" (flatten) (("1" (assert) (("1" (flatten) (("1" (hide -2) (("1" (lemma "normal_subgroup_tran[T1, *, one1]") (("1" (inst -1 "G!1" "prod[T1, *, one1](N!1, H!1)" "N!1") (("1" (assert) nil nil)) nil) ("2" (rewrite "G_TCC1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (replaces -2) (("2" (lemma "HK_subgroup[T1, *, one1]") (("2" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) (("1" (lemma "HK_subgroup_permute[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (expand "subgroup?") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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 isomorphism_theorems nil) (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems nil) (one1 formal-const-decl "T1" isomorphism_theorems nil) (HK_subgroup formula-decl nil products_subgroups nil) (normal_subgroup_tran formula-decl nil groups_scaf nil) (fullset const-decl "set" sets nil) (prod const-decl "set[T]" products_subgroups nil) (G_TCC1 assuming-tcc nil isomorphism_theorems nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (NOT const-decl "[bool -> bool]" booleans nil) (H_K_are_subgroups formula-decl nil products_subgroups nil) (HK_subgroup_permute formula-decl nil products_subgroups nil) (subgroup type-eq-decl nil group "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems nil) (N!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)" isomorphism_theorems nil)) nil)) (second_isomorphism_th 0 (second_isomorphism_th-1 nil 3524840934 ("" (skosimp*) (("" (skoletin* 1) (("1" (lemma "second_isomorphism_th_aux") (("1" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) (("1" (skosimp) (("1" (lemma "first_isomorphism_th[T1, *, one1, left_cosets[T1, *, one1](prod[T1, *, one1](N!1, H!1), (("1" (inst -1 "H!1" "prod[T1, *, one1](N!1, H!1) / N!1" "varphi!1") (("1" (assert) (("1" (replace -4 -1) (("1" (case-replace "extend [left_cosets[T1, *, one1](prod[T1, *, one1](N!1, H!1), N!1), (prod[T1, *, one1](N!1, H!1) / N!1), bool, FALSE] (image(varphi!1, restrict[T1, (H!1), bool](H!1))) = prod[T1, *, one1](N!1, H!1) / N!1") (("1" (prop) (("1" (hide (-1 -2 -4)) (("1" (lemma "kernel_normal[T1, *, one1, left_cosets[T1, *, one1](prod[T1, *, one1](N!1, H!1), N!1), mu (("1" (inst -1 "H!1" "prod[T1, *, one1](N!1, H!1) / N!1" "varphi!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (replaces -6) (("2" (hide-all-but (-2 1)) (("2" (expand "isomorphic?") (("2" (skosimp) (("2" (inst 1 "phi!1") (("2" (expand "isomorphism?") (("2" (prop) (("2" (hide -1) (("2" (expand "homomorphism?") (("2" (skosimp*) (("2" (inst -1 "a!1" "b!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 -4 2)) (("2" (decompose-equality 1) (("2" (expand "extend") (("2" (lift-if) (("2" (prop) (("2" (expand "image") (("2" (expand "surjective?") (("2" (inst -3 "x!1") (("2" (skosimp) (("2" (inst 1 "x!2") (("1" (assert) nil nil) ("2" (expand "restrict") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "left_cosets_group[T1, *, one1]") (("1" (hide-all-but 1) (("1" (lemma "HK_subgroup[T1, *, one1]") (("1" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) (("1" (lemma "HK_subgroup_permute[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (lemma "H_K_are_subgroups[T1, *, one1]") (("1" (inst?) (("1" (prop) (("1" (hide -2) (("1" (lemma "normal_subgroup_tran[T1, *, one1]") (("1" (inst -1 "G!1" "prod[T1, *, one1](N!1, H!1)" "N!1") (("1" (assert) nil nil)) nil) ("2" (rewrite "G_TCC1") nil nil)) nil)) nil) ("2" (expand "subgroup?") (("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "HK_subgroup[T1, *, one1]") (("2" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) (("1" (lemma "HK_subgroup_permute[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (lemma "H_K_are_subgroups[T1, *, one1]") (("1" (inst?) (("1" (prop) (("1" (hide -2) (("1" (expand "subgroup?") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "subgroup?") (("2" (propax) nil nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (rewrite "G_TCC1") nil nil)) nil) ("4" (hide-all-but 1) (("4" (inst 1 "one1") (("1" (rewrite "left_coset_one[T1,*,one1]") nil nil) ("2" (lemma "HK_subgroup[T1, *, one1]") (("2" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) (("1" (lemma "HK_subgroup_permute[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (expand* "subgroup?" "group?" "monoid?" "monad?" "member") nil nil)) nil)) nil) ("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (rewrite "left_cosets_group[T1, *, one1]") (("1" (replaces -1) (("1" (replaces -2) (("1" (hide (-1 2)) (("1" (lemma "HK_subgroup[T1, *, one1]") (("1" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) (("1" (lemma "HK_subgroup_permute[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (lemma "H_K_are_subgroups[T1, *, one1]") (("1" (inst?) (("1" (prop) (("1" (hide -2) (("1" (lemma "normal_subgroup_tran[T1, *, one1]") (("1" (inst -1 "G!1" "prod[T1, *, one1](N!1, H!1)" "N!1") (("1" (assert) nil nil)) nil) ("2" (rewrite "G_TCC1") nil nil)) nil)) nil) ("2" (expand "subgroup?") (("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (replaces -2) (("2" (hide (-1 2)) (("2" (lemma "HK_subgroup[T1, *, one1]") (("2" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) (("1" (lemma "HK_subgroup_permute[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (expand "subgroup?") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (rewrite "left_cosets_group[T1, *, one1]") nil nil)) nil) ("4" (skosimp) (("4" (hide -2) (("4" (inst 1 "one1") (("1" (rewrite "left_coset_one[T1,*,one1]") nil nil) ("2" (replaces -1) (("2" (replaces -1) (("2" (lemma "HK_subgroup[T1, *, one1]") (("2" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) (("1" (lemma "HK_subgroup_permute[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (expand* "subgroup?" "group?" "monoid?" "monad?" "member") nil nil)) nil)) nil) ("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (skosimp) (("5" (hide -2) (("5" (inst 1 "one1") (("1" (rewrite "left_coset_one[T1,*,one1]") nil nil) ("2" (replaces -1) (("2" (replaces -1) (("2" (typepred "H!1") (("2" (expand* "subgroup?" "group?" "monoid?" "monad?" "member") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (skosimp) (("6" (replaces -1) (("6" (replaces -2) (("6" (hide -1) (("6" (lemma "HK_subgroup[T1, *, one1]") (("6" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) (("1" (lemma "HK_subgroup_permute[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (lemma "H_K_are_subgroups[T1, *, one1]") (("1" (inst?) (("1" (prop) (("1" (hide -2) (("1" (lemma "normal_subgroup_tran[T1, *, one1]") (("1" (inst -1 "G!1" "prod[T1, *, one1](N!1, H!1)" "N!1") (("1" (assert) nil nil)) nil) ("2" (rewrite "G_TCC1") nil nil)) nil)) nil) ("2" (expand "subgroup?") (("2" (assert) nil nil)) nil)) nil) ("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("7" (skosimp) (("7" (replaces -1) (("7" (replaces -2) (("7" (hide -1) (("7" (lemma "HK_subgroup[T1, *, one1]") (("7" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) (("1" (lemma "HK_subgroup_permute[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (expand* "subgroup?" "group?" "monoid?" "monad?" "member") nil nil)) nil)) nil) ("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("8" (skosimp) (("8" (hide (-1 -3)) (("8" (expand "normal_subgroup?") (("8" (flatten) (("8" (hide -2) (("8" (expand "subgroup?") (("8" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("9" (skosimp) (("9" (hide (-1 -2)) (("9" (lemma "subgroup_intersection[T1, *, one1]") (("1" (inst -1 "G!1" "N!1" "H!1") (("1" (assert) (("1" (typepred "N!1") (("1" (expand "normal_subgroup?") (("1" (flatten) (("1" (assert) (("1" (hide (-1 -2 -3)) (("1" (expand "subgroup?") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "G_TCC1") 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 isomorphism_theorems nil) (set type-eq-decl nil sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems nil) (one1 formal-const-decl "T1" isomorphism_theorems nil) (prod const-decl "set[T]" products_subgroups 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/") (subgroup? const-decl "bool" group_def "algebra/") (subgroup type-eq-decl nil group "algebra/") (intersection const-decl "set" sets nil) (* const-decl "set[T]" cosets "algebra/") (left_cosets type-eq-decl nil cosets "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) (member const-decl "bool" sets nil) (monad? const-decl "bool" monad_def "algebra/") (monoid? const-decl "bool" monoid_def "algebra/") (left_coset_one formula-decl nil cosets "algebra/") (HK_subgroup_permute formula-decl nil products_subgroups nil) (H_K_are_subgroups formula-decl nil products_subgroups nil) (NOT const-decl "[bool -> bool]" booleans nil) (normal_subgroup_tran formula-decl nil groups_scaf nil) (G_TCC1 assuming-tcc nil isomorphism_theorems nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (HK_subgroup formula-decl nil products_subgroups nil) (left_cosets_group formula-decl nil factor_groups "algebra/") (homomorphism type-eq-decl nil homomorphisms "algebra/") (homomorphism? const-decl "bool" homomorphisms "algebra/") (surjective? const-decl "bool" functions nil) (x!2 skolem-const-decl "(H!1)" isomorphism_theorems nil) (x!1 skolem-const-decl "left_cosets[T1, *, one1](prod[T1, *, one1](N!1, H!1), N!1)" isomorphism_theorems nil) (H!1 skolem-const-decl "subgroup[T1, *, one1](G!1)" isomorphism_theorems nil) (N!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)" isomorphism_theorems nil) (G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems nil) (kernel_normal formula-decl nil homomorphism_lemmas nil) (isomorphism? const-decl "bool" homomorphisms "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) (first_isomorphism_th formula-decl nil homomorphism_lemmas nil) (second_isomorphism_th_aux formula-decl nil isomorphism_theorems nil)) shostak)) (third_isomorphism_th_aux_TCC1 0 (third_isomorphism_th_aux_TCC1-1 nil 3524797530 ("" (skosimp*) (("" (inst 1 "one1") (("1" (rewrite "left_coset_one") nil nil) ("2" (hide-all-but 1) (("2" (typepred "G!1") (("2" (expand* "group?" "monoid?" "monad?" "member") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems nil) (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one1 formal-const-decl "T1" isomorphism_theorems nil) (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems 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 isomorphism_theorems 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/") (NOT const-decl "[bool -> bool]" booleans nil) (monad? const-decl "bool" monad_def "algebra/") (member const-decl "bool" sets nil) (monoid? const-decl "bool" monoid_def "algebra/")) nil)) (third_isomorphism_th_aux_TCC2 0 (third_isomorphism_th_aux_TCC2-1 nil 3524797530 ("" (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 isomorphism_theorems nil) (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems nil) (one1 formal-const-decl "T1" isomorphism_theorems nil)) nil)) (third_isomorphism_th_aux_TCC3 0 (third_isomorphism_th_aux_TCC3-1 nil 3524797530 ("" (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 isomorphism_theorems nil) (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems nil) (one1 formal-const-decl "T1" isomorphism_theorems nil)) nil)) (third_isomorphism_th_aux 0 (third_isomorphism_th_aux-1 nil 3524915806 ("" (skosimp*) (("" (inst 1 "(LAMBDA (A: left_cosets(G!1,N!1)): *[T1, *, one1](lc_gen(G!1,N!1,A), M!1))") (("1" (prop) (("1" (expand "homomorphism?") (("1" (skosimp*) (("1" (expand "restrict") (("1" (typepred "a!1" "b!1") (("1" (hide (-2 -4)) (("1" (skosimp*) (("1" (replace -1 1) (("1" (replace -2 1) (("1" (lemma "lc_gen_normal[T1, *, one1]") (("1" (copy -1) (("1" (inst -1 "G!1" "N!1" "a!2") (("1" (inst -2 "G!1" "N!1" "a!3") (("1" (assert) (("1" (skosimp*) (("1" (replaces -1) (("1" (replaces -1) (("1" (rewrite "mult_lem[T1, *, one1]") (("1" (lemma "lc_gen_normal[T1, *, one1]") (("1" (inst -1 "G!1" "N!1" "a!2 * a!3") (("1" (assert) (("1" (prop) (("1" (skosimp) (("1" (replaces -1) (("1" (typepred "h!1" "h!2" "h!3") (("1" (expand "subgroup?") (("1" (expand* "subset?" "member") (("1" (copy -6) (("1" (copy -7) (("1" (inst -1 "h!1") (("1" (inst -2 "h!2") (("1" (inst -8 "h!3") (("1" (assert) (("1" (hide (-3 -4 -5 -6 -7)) (("1" (lemma "normal_left_is_right[T1, *, one1]") (("1" (copy -1) (("1" (copy -1) (("1" (inst -1 "G!1" "M!1") (("1" (assert) (("1" (inst -2 "G!1" "M!1") (("1" (assert) (("1" (inst -3 "G!1" "M!1") (("1" (assert) (("1" (typepred "M!1") (("1" (hide -1) (("1" (expand "normal_subgroup?") (("1" (flatten) (("1" (hide (-1 -2 -3 -5 -7)) (("1" (inst -1 "h!3 * (a!2 * a!3)") (("1" (inst -2 "h!1 * a!2") (("1" (inst -3 "h!2 * a!3") (("1" (replaces -1) (("1" (replaces -1) (("1" (replaces -1) (("1" (lemma "right_coset_assoc[T1, *, one1]") (("1" (copy -1) (("1" (copy -1) (("1" (inst -1 "M!1" "h!3" "a!2 * a!3") (("1" (inst -2 "M!1" "h!1" "a!2") (("1" (inst -3 "M!1" "h!2" "a!3") (("1" (lemma "rc_is_eq[T1, *, one1]") (("1" (inst -1 "G!1" "M!1" "h!1" "one1") (("1" (reveal -8) (("1" (assert) (("1" (prop) (("1" (lemma "rc_is_eq[T1, *, one1]") (("1" (inst -1 "G!1" "M!1" "h!2" "one1") (("1" (assert) (("1" (prop) (("1" (lemma "rc_is_eq[T1, *, one1]") (("1" (inst -1 "G!1" "M!1" "h!3" "one1") (("1" (assert) (("1" (prop) (("1" (rewrite "right_coset_one") (("1" (replaces -1) (("1" (replaces -1) (("1" (replaces -1) (("1" (replace -2 1 rl) (("1" (replace -3 1 rl) (("1" (replace -4 1 rl) (("1" (lemma "normal_left_is_right[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (copy -1) (("1" (copy -1) (("1" (inst -1 "a!2 * a!3") (("1" (inst -2 "a!2") (("1" (inst -3 "a!3") (("1" (replace -1 1 rl) (("1" (replace -2 1 rl) (("1" (replace -3 1 rl) (("1" (rewrite "mult_lem[T1, *, one1]") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "a!2" "a!3" "G!1") (("2" (expand* "group?" "monoid?" "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) ("2" (hide-all-but 1) (("2" (inst 1 "h!3") (("2" (rewrite "one_right[T1, *, one1]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (inst 1 "h!2") (("2" (rewrite "one_right[T1, *, one1]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (inst 1 "h!1") (("2" (rewrite "one_right[T1, *, one1]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 -2 -3 -5 2)) (("2" (typepred "a!3") (("2" (reveal -7) (("2" (expand "subgroup?") (("2" (expand* "subgroup?" "subset?" "member") (("2" (inst -1 "h!2") (("2" (assert) (("2" (typepred "G!1") (("2" (expand* "group?" "monoid?" "monad?") (("2" (flatten) (("2" (hide (-2 -3 -4 -5)) (("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) ("2" (hide (-1 -2 -4 -5 2)) (("2" (typepred "a!2") (("2" (reveal -6) (("2" (expand "subgroup?") (("2" (expand* "subgroup?" "subset?" "member") (("2" (inst -1 "h!1") (("2" (assert) (("2" (typepred "G!1") (("2" (expand* "group?" "monoid?" "monad?") (("2" (flatten) (("2" (hide (-2 -3 -4 -5)) (("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) ("2" (hide (-1 -2 -3 -4 2)) (("2" (typepred "a!2" "a!3") (("2" (reveal -5) (("2" (expand "subgroup?") (("2" (expand* "subgroup?" "subset?" "member") (("2" (inst -1 "h!3") (("2" (assert) (("2" (typepred "G!1") (("2" (expand* "group?" "monoid?" "monad?") (("2" (flatten) (("2" (hide (-2 -3 -4 -5)) (("2" (expand "star_closed?") (("2" (copy -1) (("2" (inst -1 "a!2" "a!3") (("2" (expand "member") (("2" (inst -2 "h!3" "a!2 * a!3") 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" (typepred "a!2" "a!3") (("2" (typepred "G!1") (("2" (expand* "group?" "monoid?" "monad?") (("2" (flatten) (("2" (hide (-2 -3 -4 -5)) (("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) ("2" (expand "surjective?") (("2" (skosimp*) (("2" (typepred "y!1") (("2" (skosimp) (("2" (typepred "a!1") (("2" (expand "restrict") (("2" (inst 1 "*[T1, *, one1](a!1, N!1)") (("1" (replaces -2) (("1" (lemma "lc_gen_normal[T1, *, one1]") (("1" (inst?) (("1" (assert) (("1" (skosimp) (("1" (replaces -1) (("1" (lemma "normal_left_is_right[T1, *, one1]") (("1" (inst -1 "G!1" "M!1") (("1" (assert) (("1" (typepred "M!1") (("1" (hide -1) (("1" (expand "normal_subgroup?" -1) (("1" (flatten) (("1" (hide -2) (("1" (inst -3 "h!1 * a!1") (("1" (replaces -3) (("1" (lemma "right_coset_assoc[T1,*,one1]") (("1" (inst -1 "M!1" "h!1" "a!1") (("1" (replace -1 1 rl) (("1" (hide (-1 -2 -4 -5)) (("1" (lemma "rc_is_eq[T1,*,one1]") (("1" (inst -1 "G!1" "M!1" "h!1" "one1") (("1" (assert) (("1" (prop) (("1" (rewrite "right_coset_one") (("1" (replaces -1) (("1" (lemma "normal_left_is_right[T1,*,one1]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (inst 1 "h!1") (("1" (rewrite "one_right[T1,*,one1]") nil nil) ("2" (typepred "h!1") (("2" (hide -2) (("2" (expand* "subgroup?" "subset?" "member") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (typepred "h!1") (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (flatten) (("2" (hide (-1 -3)) (("2" (expand* "subgroup?" "subset?" "member") (("2" (inst -1 "h!1") (("2" (assert) (("2" (typepred "G!1") (("2" (expand* "group?" "monoid?" "monad?") (("2" (flatten) (("2" (hide (-2 -3 -4 -5)) (("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) ("2" (prop) (("1" (inst 1 "a!1") nil nil) ("2" (hide (-2 -3 -4)) (("2" (expand "/") (("2" (expand "restrict") (("2" (expand "left_cosets") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "restrict") (("3" (expand "kernel") (("3" (decompose-equality 1) (("1" (iff) (("1" (prop) (("1" (lemma "lc_eq[T1, *, one1]") (("1" (inst -1 "G!1" "M!1" "lc_gen(G!1, N!1, x!1)" "one1") (("1" (rewrite "left_coset_one") (("1" (prop) (("1" (skosimp) (("1" (expand "/") (("1" (expand "restrict") (("1" (expand "left_cosets") (("1" (hide (-3 -4)) (("1" (skosimp) (("1" (rewrite "one_left[T1, *, one1]") (("1" (inst 1 "h!1") (("1" (replace -1 1 rl) (("1" (hide -1) (("1" (replaces -1) (("1" (lemma "lc_gen_def[T1, *, one1]") (("1" (inst?) (("1" (typepred "a!1") (("1" (prop) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("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) (("2" (typepred "M!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "/") (("2" (expand "restrict") (("2" (expand "left_cosets") (("2" (skosimp) (("2" (inst?) (("2" (typepred "a!1") (("2" (hide (-2 -3)) (("2" (typepred "M!1") (("2" (hide -1) (("2" (expand "normal_subgroup?") (("2" (flatten) (("2" (hide -2) (("2" (expand "subgroup?") (("2" (expand* "subset?" "member") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "/") (("3" (expand "restrict") (("3" (expand "left_cosets") (("3" (skosimp) (("3" (replaces -1) (("3" (lemma "lc_gen_normal[T1, *, one1]") (("3" (inst -1 "G!1" "N!1" "a!1") (("3" (prop) (("1" (skosimp) (("1" (replaces -1) (("1" (typepred "h!1" "a!1") (("1" (lemma "lc_is_eq[T1,*,one1]") (("1" (inst -1 "G!1" "M!1" "h!1 * a!1" "one1") (("1" (prop) (("1" (rewrite "left_coset_one") nil nil) ("2" (typepred "M!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil) ("3" (inst 1 "h!1 * a!1") (("1" (rewrite "one_left[T1,*,one1]") nil nil) ("2" (hide 2) (("2" (expand "subgroup?") (("2" (expand* "subset?" "member") (("2" (inst -3 "h!1") (("2" (assert) (("2" (rewrite "product_in[T1,*,one1]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "N!1") (("2" (propax) nil nil)) nil)) nil) ("3" (typepred "a!1" "M!1") (("3" (hide (-2 -4 2)) (("3" (expand "normal_subgroup?") (("3" (expand "subgroup?") (("3" (expand* "subset?" "member") (("3" (flatten) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst 1 "one1") (("1" (rewrite "left_coset_one") nil nil) ("2" (hide (-1 -2)) (("2" (typepred "G!1") (("2" (expand* "group?" "monoid?" "monad?" "subset?" "member") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (inst 1 "lc_gen[T1, *, one1](G!1, N!1, a!1)") (("3" (typepred "N!1") (("3" (expand "normal_subgroup?") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (typepred "N!1") (("4" (expand "normal_subgroup?") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (prop) (("1" (inst 1 "lc_gen[T1, *, one1](G!1, N!1, x1!1)") (("1" (typepred "N!1") (("1" (expand "normal_subgroup?") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "/") (("2" (expand "restrict") (("2" (expand "left_cosets") (("2" (inst 1 "lc_gen[T1, *, one1](G!1, N!1, x1!1)") (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (prop) (("1" (inst 1 "lc_gen[T1, *, one1](G!1, N!1, A!1)") (("1" (typepred "N!1") (("1" (expand "normal_subgroup?") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "/") (("2" (expand "restrict") (("2" (expand "left_cosets") (("2" (inst 1 "lc_gen[T1, *, one1](G!1, N!1, A!1)") (("2" (typepred "N!1") (("2" (expand "normal_subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (typepred "N!1") (("4" (expand "normal_subgroup?") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((subgroup? const-decl "bool" group_def "algebra/") (left_cosets type-eq-decl nil cosets "algebra/") (N!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)" isomorphism_theorems 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) (G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems nil) (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one1 formal-const-decl "T1" isomorphism_theorems nil) (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems 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 isomorphism_theorems 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/") (M!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)" isomorphism_theorems nil) (lc_gen const-decl "{a: T | G(a) AND lc = a * H}" cosets "algebra/") (subgroup type-eq-decl nil group "algebra/") (AND const-decl "[bool, bool -> bool]" booleans nil) (restrict const-decl "R" restrict nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (lc_gen_def formula-decl nil cosets "algebra/") (one_left formula-decl nil group "algebra/") (left_coset_one formula-decl nil cosets "algebra/") (lc_eq formula-decl nil cosets "algebra/") (a!1 skolem-const-decl "(M!1)" isomorphism_theorems nil) (lc_is_eq formula-decl nil cosets "algebra/") (product_in formula-decl nil group "algebra/") (a!1 skolem-const-decl "(M!1)" isomorphism_theorems nil) (h!1 skolem-const-decl "(N!1)" isomorphism_theorems nil) (kernel const-decl "subgroup[T1, *, one1](G)" homomorphisms "algebra/") (surjective? const-decl "bool" functions nil) (a!1 skolem-const-decl "(G!1)" isomorphism_theorems nil) (h!1 skolem-const-decl "(N!1)" isomorphism_theorems nil) (left_cosets const-decl "setofsets[T]" right_left_cosets nil) (homomorphism? const-decl "bool" homomorphisms "algebra/") (lc_gen_normal formula-decl nil normal_subgroups "algebra/") (mult_lem formula-decl nil factor_groups "algebra/") (h!1 skolem-const-decl "(N!1)" isomorphism_theorems nil) (one_right formula-decl nil group "algebra/") (right_coset_one formula-decl nil cosets "algebra/") (star_closed? const-decl "bool" groupoid_def "algebra/") (monad? const-decl "bool" monad_def "algebra/") (monoid? const-decl "bool" monoid_def "algebra/") (rc_is_eq formula-decl nil cosets "algebra/") (right_coset_assoc formula-decl nil cosets "algebra/") (h!2 skolem-const-decl "(N!1)" isomorphism_theorems nil) (a!3 skolem-const-decl "(G!1)" isomorphism_theorems nil) (a!2 skolem-const-decl "(G!1)" isomorphism_theorems nil) (h!3 skolem-const-decl "(N!1)" isomorphism_theorems nil) (normal_left_is_right formula-decl nil normal_subgroups "algebra/") (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil)) shostak)) (third_isomorphism_th_TCC1 0 (third_isomorphism_th_TCC1-1 nil 3524769565 ("" (skosimp*) (("" (prop) (("1" (skosimp) (("1" (prop) (("1" (skosimp) (("1" (inst 1 "a!1") (("1" (hide -) (("1" (typepred "a!1" "M!1") (("1" (expand* "normal_subgroup?" "subgroup?") (("1" (flatten) (("1" (expand* "subset?" "member") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (inst 1 "lc_gen(M!1, N!1, x!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "quotient_subgroup") (("2" (inst?) (("2" (assert) (("2" (expand "subgroup?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T1 formal-type-decl nil isomorphism_theorems 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]" isomorphism_theorems nil) (one1 formal-const-decl "T1" isomorphism_theorems 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/") (a!1 skolem-const-decl "(M!1)" isomorphism_theorems nil) (M!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)" isomorphism_theorems nil) (G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems nil) (NOT const-decl "[bool -> bool]" booleans nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (subgroup? const-decl "bool" group_def "algebra/") (N!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)" isomorphism_theorems nil) (subgroup type-eq-decl nil group "algebra/") (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "set[T]" cosets "algebra/") (left_cosets type-eq-decl nil cosets "algebra/") (AND const-decl "[bool, bool -> bool]" booleans nil) (lc_gen const-decl "{a: T | G(a) AND lc = a * H}" cosets "algebra/") (quotient_subgroup formula-decl nil isomorphism_theorems nil)) nil)) (third_isomorphism_th_TCC2 0 (third_isomorphism_th_TCC2-1 nil 3524769565 ("" (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 isomorphism_theorems nil) (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems nil) (one1 formal-const-decl "T1" isomorphism_theorems nil)) nil)) (third_isomorphism_th_TCC3 0 (third_isomorphism_th_TCC3-1 nil 3524769565 ("" (skosimp*) (("" (prop) (("1" (skosimp) (("1" (prop) (("1" (hide (-2 -3 -4)) (("1" (skosimp) (("1" (inst 1 "a!1") (("1" (hide -) (("1" (typepred "a!1" "M!1") (("1" (expand* "normal_subgroup?" "subgroup?") (("1" (flatten) (("1" (expand* "subset?" "member") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 -3)) (("2" (inst 1 "lc_gen(M!1, N!1, x!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (inst 1 "N!1") (("1" (decompose-equality 1) (("1" (iff) (("1" (prop) (("1" (expand "*" 1) (("1" (inst 1 "x!1") (("1" (lemma "N_is_identity[T1, *, one1]") (("1" (inst -1 "G!1" "N!1" "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil) ("2" (skosimp) (("2" (prop) (("1" (hide -1) (("1" (expand "*" -1) (("1" (skosimp) (("1" (typepred "h!1") (("1" (skosimp) (("1" (lemma "N_is_identity[T1, *, one1]") (("1" (inst -1 "G!1" "N!1" "h!1") (("1" (flatten) (("1" (replaces -1) (("1" (replaces -2) (("1" (replaces -3) (("1" (inst 1 "a!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (skosimp) (("2" (inst 1 "a!1") (("2" (typepred "a!1" "M!1") (("2" (expand* "normal_subgroup?" "subgroup?" "subset?" "member") (("2" (flatten) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (rewrite "left_cosets_group[T1, *, one1]") nil nil)) nil) ("2" (prop) (("1" (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) ("2" (expand "/") (("2" (expand "restrict") (("2" (expand "left_cosets") (("2" (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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((subgroup? const-decl "bool" group_def "algebra/") (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems nil) (M!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)" isomorphism_theorems nil) (a!1 skolem-const-decl "(M!1)" isomorphism_theorems 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" isomorphism_theorems nil) (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems 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 isomorphism_theorems nil) (N!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)" isomorphism_theorems nil) (subgroup type-eq-decl nil group "algebra/") (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "set[T]" cosets "algebra/") (left_cosets type-eq-decl nil cosets "algebra/") (AND const-decl "[bool, bool -> bool]" booleans nil) (lc_gen const-decl "{a: T | G(a) AND lc = a * H}" cosets "algebra/") (/ 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_group formula-decl nil factor_groups "algebra/") (a!1 skolem-const-decl "(M!1)" isomorphism_theorems nil) (left_cosets const-decl "setofsets[T]" right_left_cosets nil) (restrict const-decl "R" restrict nil) (N_is_identity formula-decl nil factor_groups "algebra/") (x!1 skolem-const-decl "left_cosets[T1, *, one1](M!1, N!1)" isomorphism_theorems nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (fullset const-decl "set" sets nil) (left_coset_one formula-decl nil cosets "algebra/") (monoid? const-decl "bool" monoid_def "algebra/") (monad? const-decl "bool" monad_def "algebra/")) nil)) (third_isomorphism_th_TCC4 0 (third_isomorphism_th_TCC4-1 nil 3524769565 ("" (skosimp*) (("" (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)) nil) ((G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems nil) (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one1 formal-const-decl "T1" isomorphism_theorems nil) (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems 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 isomorphism_theorems 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)) (third_isomorphism_th_TCC5 0 (third_isomorphism_th_TCC5-1 nil 3524769565 ("" (skosimp*) (("" (lemma "left_cosets_group[left_cosets[T1, *, one1](G!1, N!1), mult[T1, *, one1](G!1, N!1), N!1] (("1" (inst -1 "G!1 / N!1" "M!1 / N!1") nil nil) ("2" (hide 2) (("2" (inst 1 "N!1") (("2" (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)) nil)) nil) ("3" (hide 2) (("3" (rewrite "left_cosets_group[T1, *, one1]") nil nil)) nil) ("4" (hide 2) (("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)) nil)) nil)) nil) ((mult const-decl "left_cosets(G, H)" factor_groups "algebra/") (left_cosets type-eq-decl nil cosets "algebra/") (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) (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one1 formal-const-decl "T1" isomorphism_theorems nil) (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems 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 isomorphism_theorems nil) (left_cosets_group formula-decl nil factor_groups "algebra/") (fullset const-decl "set" sets nil) (TRUE const-decl "bool" booleans nil) (G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems nil) (N!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)" isomorphism_theorems nil) (M!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)" isomorphism_theorems nil) (/ const-decl "group[left_cosets(G, N), mult(G, N), N]" right_left_cosets nil) (NOT const-decl "[bool -> bool]" booleans nil) (monad? const-decl "bool" monad_def "algebra/") (member const-decl "bool" sets nil) (monoid? const-decl "bool" monoid_def "algebra/") (left_coset_one formula-decl nil cosets "algebra/")) nil)) (third_isomorphism_th_TCC6 0 (third_isomorphism_th_TCC6-1 nil 3524769565 ("" (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 isomorphism_theorems nil) (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems nil) (one1 formal-const-decl "T1" isomorphism_theorems nil)) nil)) (third_isomorphism_th 0 (third_isomorphism_th-1 nil 3524796117 ("" (skosimp*) (("" (lemma "third_isomorphism_th_aux") (("" (inst?) (("" (assert) (("" (skosimp) (("" (lemma "first_isomorphism_th[left_cosets[T1, *, one1](G!1, N!1), mult(G!1, N!1), N!1, left_cos (("1" (inst -1 "G!1 / N!1" "G!1 / M!1" "psi!1") (("1" (replace -4 -1) (("1" (assert) (("1" (case-replace "extend [left_cosets[T1, *, one1](G!1, M!1), (G!1 / M!1), bool, FALSE] (image(psi!1, restrict [left_cosets[T1, *, one1](G!1, N!1), (G!1 / N!1), bool] (G!1 / N!1))) = G!1 / M!1" :hide? T) (("1" (assert) (("1" (hide (-1 -2 -3)) (("1" (lemma "kernel_normal[left_cosets[T1, *, one1](G!1, N!1), mult[T1, *, one1](G!1, N!1), N!1, left_cosets[T1, *, one1](G!1, M!1), mult[T1, *, one1](G!1, M!1), M!1]") (("1" (inst -1 "/[T1, *, one1](G!1, N!1)" "/[T1, *, one1](G!1, M!1)" "psi!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 -4 2)) (("2" (decompose-equality 1) (("2" (expand "extend") (("2" (lift-if) (("2" (prop) (("2" (expand "image") (("2" (expand "surjective?") (("2" (inst -3 "x!1") (("2" (skosimp) (("2" (inst 1 "x!2") (("1" (assert) nil nil) ("2" (expand "restrict") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "left_cosets_group[T1, *, one1]") nil nil)) nil) ("3" (hide-all-but 1) (("3" (rewrite "left_cosets_group[T1, *, one1]") nil nil)) nil) ("4" (hide-all-but 1) (("4" (inst 1 "one1") (("1" (rewrite "left_coset_one[T1,*,one1]") nil nil) ("2" (typepred "G!1") (("2" (expand* "group?" "monoid?" "monad?" "member") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil) ("5" (hide-all-but 1) (("5" (inst 1 "one1") (("1" (rewrite "left_coset_one[T1,*,one1]") nil nil) ("2" (typepred "G!1") (("2" (expand* "group?" "monoid?" "monad?" "member") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((third_isomorphism_th_aux formula-decl nil isomorphism_theorems nil) (mult const-decl "left_cosets(G, H)" factor_groups "algebra/") (left_cosets type-eq-decl nil cosets "algebra/") (* const-decl "set[T]" cosets "algebra/") (= const-decl "[T, T -> boolean]" equalities nil) (first_isomorphism_th formula-decl nil homomorphism_lemmas nil) (fullset const-decl "set" sets nil) (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) (kernel_normal formula-decl nil homomorphism_lemmas nil) (G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems nil) (M!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)" isomorphism_theorems nil) (x!1 skolem-const-decl "left_cosets[T1, *, one1](G!1, M!1)" isomorphism_theorems nil) (N!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)" isomorphism_theorems nil) (x!2 skolem-const-decl "(G!1 / N!1)" isomorphism_theorems nil) (surjective? const-decl "bool" functions nil) (homomorphism type-eq-decl nil homomorphisms "algebra/") (homomorphism? const-decl "bool" homomorphisms "algebra/") (/ const-decl "group[left_cosets(G, N), mult(G, N), N]" right_left_cosets nil) (left_cosets_group formula-decl nil factor_groups "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) (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" isomorphism_theorems nil) (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems 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 isomorphism_theorems nil)) shostak)) (correspondence_theorem 0 (correspondence_theorem-1 nil 3530907884 ("" (skosimp*) (("" (inst 1 "LAMBDA (N: subgroup_contain(G!1, kernel(G!1, GP!1)(f!1))): image(f!1, N)") (("1" (prop) (("1" (expand "bijective?") (("1" (prop) (("1" (expand "injective?") (("1" (skosimp*) (("1" (typepred "x1!1" "x2!1") (("1" (hide (-1 -4)) (("1" (lemma "homo_inv_image_image_cor[T1,*,one1,T2,o,one2]") (("1" (assert) (("1" (expand "subgroup?" -1) (("1" (inst-cp -1 "G!1" "GP!1" "f!1" "x2!1") (("1" (inst -1 "G!1" "GP!1" "f!1" "x1!1") (("1" (assert) (("1" (decompose-equality -1) (("1" (decompose-equality -2) (("1" (decompose-equality -7) (("1" (decompose-equality 1) (("1" (iff) (("1" (prop) (("1" (inst -3 "x!1") (("1" (inst -4 "x!1") (("1" (iff) (("1" (prop) (("1" (hide-all-but (-4 1)) (("1" (expand "restrict") (("1" (propax) nil nil)) nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (expand "restrict") (("2" (propax) nil nil)) nil)) nil) ("3" (hide (-2 1 3)) (("3" (expand "inverse_image") (("3" (expand "member") (("3" (inst?) (("3" (expand "extend") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (-1 1)) (("4" (expand "restrict") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -4 1)) (("2" (expand* "subgroup?" "subset?" "member") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst -3 "x!1") (("1" (inst -4 "x!1") (("1" (iff) (("1" (prop) (("1" (hide-all-but (-2 1)) (("1" (expand "restrict") (("1" (propax) nil nil)) nil)) nil) ("2" (hide (-2 1 3)) (("2" (expand "inverse_image") (("2" (expand "member") (("2" (inst?) (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-3 1)) (("3" (expand "restrict") (("3" (propax) nil nil)) nil)) nil) ("4" (hide-all-but (-1 3)) (("4" (expand "restrict") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -6 1)) (("2" (expand* "subgroup?" "subset?" "member") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "T2_is_group") nil nil) ("3" (rewrite "T1_is_group") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "surjective?") (("2" (skosimp*) (("2" (inst 1 "inverse_image(f!1, y!1)") (("1" (decompose-equality 1) (("1" (iff) (("1" (prop) (("1" (expand "extend") (("1" (prop) (("1" (expand "image") (("1" (skosimp) (("1" (typepred "x!2") (("1" (expand "restrict") (("1" (expand "inverse_image") (("1" (expand "member") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "image") (("1" (inst?) (("1" (skosimp) (("1" (inst 1 "x!2") (("1" (assert) nil nil) ("2" (expand "restrict") (("2" (expand "inverse_image") (("2" (expand "member") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2) (("2" (typepred "y!1") (("2" (hide -1) (("2" (expand* "subgroup?" "subset?" "member") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (lemma "homo_inv_image[T1,*,one1,T2,o,one2]") (("1" (inst?) (("1" (assert) (("1" (prop) (("1" (lemma "subgroup_is_group[T1, *, one1]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "kernel_in_inv_image[T1,*,one1,T2,o,one2]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "T2_is_group") nil nil)) nil) ("3" (hide 2) (("3" (rewrite "T1_is_group") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (prop) (("1" (lemma "homo_image[T1,*,one1,T2,o,one2]") (("1" (inst?) nil nil) ("2" (hide-all-but 1) (("2" (rewrite "T2_is_group") nil nil)) nil) ("3" (hide-all-but 1) (("3" (rewrite "T1_is_group") nil nil)) nil)) nil) ("2" (lemma "homo_inv_image[T1,*,one1,T2,o,one2]") (("1" (inst -1 "G!1" "GP!1" "f!1" "image(f!1, restrict[T1, (G!1), boolean](N!1))") (("1" (lemma "homo_inv_image_image_cor[T1, *, one1,T2, o, one2]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (prop) (("2" (hide (-2 2)) (("2" (lemma "subgroup_is_group[T2, o, one2]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "T2_is_group") nil nil)) nil) ("3" (hide-all-but 1) (("3" (rewrite "T1_is_group") nil nil)) nil)) nil) ("3" (lemma "homo_image_normal[T1,*,one1,T2,o,one2]") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "T2_is_group") nil nil)) nil) ("3" (hide-all-but 1) (("3" (rewrite "T1_is_group") nil nil)) nil)) nil) ("4" (lemma "homo_inv_image_normal[T1,*,one1,T2,o,one2]") (("1" (inst -1 "G!1" "GP!1" "f!1" "image(f!1, restrict[T1, (G!1), boolean](N!1))") (("1" (lemma "homo_inv_image_image_cor[T1, *, one1,T2, o, one2]") (("1" (inst?) (("1" (assert) (("1" (prop) (("1" (hide (-2 -4 -5)) (("1" (expand "normal_subgroup?") (("1" (flatten) (("1" (skosimp) (("1" (hide -2) (("1" (expand* "subset?" "member") (("1" (skosimp) (("1" (decompose-equality -1) (("1" (inst -1 "x!1") (("1" (iff) (("1" (prop) (("1" (hide-all-but (-2 1)) (("1" (expand "restrict") (("1" (propax) nil nil)) nil)) nil) ("2" (hide (1 3)) (("2" (expand "inverse_image") (("2" (expand "member") (("2" (expand "image") (("2" (inst -1 "a!1") (("2" (inst -1 "x!1") (("2" (prop) (("1" (expand "extend") (("1" (prop) nil nil)) nil) ("2" (hide 2) (("2" (expand "*") (("2" (skosimp) (("2" (typepred "h!1") (("2" (skosimp) (("2" (replaces -1) (("2" (inst 1 "inv[T1, *, one1](a!1) * h!2") (("2" (inst 1 "h!2") (("2" (expand "extend") (("2" (prop) (("1" (inst?) (("1" (assert) (("1" (expand "restrict") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (typepred "h!2" "N!1") (("2" (hide (-2 -4)) (("2" (expand* "subgroup?" "subset?" "member") (("2" (inst?) (("2" (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)) nil)) nil) ("2" (hide (-1 2)) (("2" (expand "*") (("2" (skosimp) (("2" (typepred "h!1") (("2" (skosimp) (("2" (replaces -1) (("2" (replaces -1) (("2" (rewrite "product_in[T1, *, one1]") (("2" (hide 2) (("2" (rewrite "product_in[T1, *, one1]") (("1" (hide 2) (("1" (rewrite "inv_in") nil nil)) nil) ("2" (hide 2) (("2" (typepred "h!2" "N!1") (("2" (hide (-2 -4)) (("2" (expand* "subgroup?" "subset?" "member") (("2" (inst?) (("2" (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)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "N!1") (("2" (hide (-1 -2)) (("2" (expand "subgroup?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "T2_is_group") nil nil)) nil) ("3" (hide-all-but 1) (("3" (rewrite "T1_is_group") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "homo_image[T1,*,one1,T2,o,one2]") (("1" (inst?) (("1" (assert) (("1" (hide -2) (("1" (lemma "subgroup_is_group[T2, o, one2]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "T2_is_group") nil nil)) nil) ("3" (hide 2) (("3" (rewrite "T1_is_group") nil nil)) nil)) nil)) nil) ("3" (rewrite "T1_is_group") nil nil)) nil)) nil) ((fullset const-decl "set" sets nil) (group? const-decl "bool" group_def "algebra/") (one1 formal-const-decl "T1" isomorphism_theorems nil) (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems 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 isomorphism_theorems nil) (restrict const-decl "R" restrict nil) (image const-decl "set[R]" function_image nil) (extend const-decl "R" extend nil) (FALSE const-decl "bool" booleans nil) (subgroup_contain type-eq-decl nil groups_scaf nil) (f!1 skolem-const-decl "homomorphism[T1, *, one1, T2, o, one2](G!1, GP!1)" isomorphism_theorems nil) (GP!1 skolem-const-decl "group[T2, o, one2]" isomorphism_theorems nil) (kernel const-decl "subgroup[T1, *, one1](G)" homomorphisms "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" isomorphism_theorems nil) (O formal-const-decl "[T2, T2 -> T2]" isomorphism_theorems nil) (T2 formal-type-decl nil isomorphism_theorems nil) (subset? const-decl "bool" sets nil) (G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems nil) (subgroup? const-decl "bool" group_def "algebra/") (AND const-decl "[bool, bool -> bool]" booleans nil) (group nonempty-type-eq-decl nil group "algebra/") (homo_inv_image_normal formula-decl nil homomorphism_lemmas nil) (x!1 skolem-const-decl "T1" isomorphism_theorems nil) (a!1 skolem-const-decl "(G!1)" isomorphism_theorems nil) (h!2 skolem-const-decl "(N!1)" isomorphism_theorems nil) (inv const-decl "{y | x * y = one AND y * x = one}" group "algebra/") (* const-decl "set[T]" cosets "algebra/") (* const-decl "set[T]" cosets "algebra/") (product_in formula-decl nil group "algebra/") (inv_in formula-decl nil group "algebra/") (homo_image_normal formula-decl nil homomorphism_lemmas nil) (normal_subgroup type-eq-decl nil normal_subgroups "algebra/") (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/") (N!1 skolem-const-decl "subgroup_contain[T1, *, one1](G!1, kernel(G!1, GP!1)(f!1))" isomorphism_theorems nil) (homo_image formula-decl nil homomorphism_lemmas nil) (bijective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (y!1 skolem-const-decl "subgroup[T2, o, one2](GP!1)" isomorphism_theorems nil) (x!2 skolem-const-decl "(G!1)" isomorphism_theorems nil) (x!1 skolem-const-decl "T2" isomorphism_theorems nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (homo_inv_image formula-decl nil homomorphism_lemmas nil) (kernel_in_inv_image formula-decl nil homomorphism_lemmas nil) (subgroup_is_group formula-decl nil group "algebra/") (injective? const-decl "bool" functions nil) (NOT const-decl "[bool -> bool]" booleans nil) (homo_inv_image_image_cor formula-decl nil homomorphism_lemmas nil) (inverse_image const-decl "set[D]" function_image nil) (= const-decl "[T, T -> boolean]" equalities nil) (x!1 skolem-const-decl "T1" isomorphism_theorems nil) (member const-decl "bool" sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (T2_is_group formula-decl nil isomorphism_theorems nil) (T1_is_group formula-decl nil isomorphism_theorems nil)) shostak)))
¤ Dauer der Verarbeitung: 0.429 Sekunden (vorverarbeitet am 2026-04-27) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26