|
(homomorphism_lemmas
(G_TCC1 0
(G_TCC1-1 nil 3530720894 ("" (rewrite "T1_is_group") nil nil)
((T1_is_group formula-decl nil homomorphism_lemmas nil)) nil))
(GP_TCC1 0
(GP_TCC1-1 nil 3528505895 ("" (rewrite "T2_is_group") nil nil)
((T2_is_group formula-decl nil homomorphism_lemmas nil)) nil))
(natural_homo_TCC1 0
(natural_homo_TCC1-1 nil 3524654775
("" (skosimp)
(("" (inst 1 "one1")
(("1" (rewrite "left_coset_one[T1, *, one1]") nil nil)
("2" (typepred "G!1")
(("2" (expand* "group?" "monoid?" "monad?" "subset?" "member")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil)
((G!1 skolem-const-decl "group[T1, *, one1]" homomorphism_lemmas
nil)
(group nonempty-type-eq-decl nil group "algebra/")
(group? const-decl "bool" group_def "algebra/")
(one1 formal-const-decl "T1" homomorphism_lemmas nil)
(* formal-const-decl "[T1, T1 -> T1]" homomorphism_lemmas nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T1 formal-type-decl nil homomorphism_lemmas nil)
(normal_subgroup type-eq-decl nil normal_subgroups "algebra/")
(normal_subgroup? const-decl "boolean" normal_subgroups "algebra/")
(left_coset_one formula-decl nil cosets "algebra/")
(monoid? const-decl "bool" monoid_def "algebra/")
(member const-decl "bool" sets nil)
(monad? const-decl "bool" monad_def "algebra/")
(NOT const-decl "[bool -> bool]" booleans nil))
nil))
(natural_homo_TCC2 0
(natural_homo_TCC2-1 nil 3524789060
("" (skosimp*)
(("" (rewrite "left_cosets_group[T1, *, one1]") nil nil)) nil)
((left_cosets_group formula-decl nil factor_groups "algebra/")
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(group? const-decl "bool" group_def "algebra/")
(group nonempty-type-eq-decl nil group "algebra/")
(normal_subgroup? const-decl "boolean" normal_subgroups "algebra/")
(normal_subgroup type-eq-decl nil normal_subgroups "algebra/")
(T1 formal-type-decl nil homomorphism_lemmas nil)
(* formal-const-decl "[T1, T1 -> T1]" homomorphism_lemmas nil)
(one1 formal-const-decl "T1" homomorphism_lemmas nil))
nil))
(natural_homo 0
(natural_homo-1 nil 3524654777
("" (skosimp*)
(("" (inst 1 "(LAMBDA (x:(G!1)): *[T1, *, one1](x, K!1))")
(("1" (prop)
(("1" (expand "homomorphism?")
(("1" (skosimp*)
(("1" (rewrite "mult_lem[T1, *, one1]") nil nil)) nil))
nil)
("2" (expand "surjective?")
(("2" (skosimp*)
(("2" (typepred "y!1")
(("2" (skosimp*)
(("2" (inst 1 "a!1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("3" (decompose-equality 1)
(("1" (expand "kernel")
(("1" (iff)
(("1" (prop)
(("1" (typepred "K!1")
(("1" (expand "normal_subgroup?")
(("1" (flatten)
(("1" (expand "subgroup?")
(("1" (expand* "subset?" "member")
(("1" (inst -2 "x!1")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (decompose-equality 1)
(("2" (expand "*")
(("2" (iff)
(("2" (prop)
(("1" (skosimp)
(("1" (replaces -1)
(("1" (typepred "h!1" "K!1")
(("1"
(expand* "group?" "monoid?" "monad?")
(("1"
(flatten)
(("1"
(hide-all-but (-1 -2 -8 1))
(("1"
(expand "star_closed?")
(("1"
(inst?)
(("1"
(expand "member")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst 1 "inv[T1, *, one1](x!1) * x!2")
(("1" (rewrite "assoc[T1, *, one1]")
(("1" (rewrite "inv_right[T1, *, one1]")
(("1"
(rewrite "one_left[T1, *, one1]")
nil
nil))
nil))
nil)
("2" (typepred "K!1")
(("2" (expand* "group?" "monoid?" "monad?")
(("2"
(flatten)
(("2"
(hide-all-but (-1 -7 -8 1))
(("2"
(expand* "star_closed?" "member")
(("2"
(lemma "inv_in[T1, *, one1]")
(("2"
(inst -1 "K!1" "x!1")
(("2" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "*")
(("3" (decompose-equality -2)
(("3" (inst?)
(("3" (iff)
(("3" (prop)
(("3" (inst 2 "one1")
(("1" (rewrite "one_right[T1, *, one1]")
nil nil)
("2" (typepred "K!1")
(("2"
(expand* "group?" "monoid?" "monad?")
(("2"
(flatten)
(("2"
(expand "member")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "left_cosets_group[T1, *, one1]") nil nil)
("3" (rewrite "T1_is_group") nil nil)
("4" (inst 1 "one1")
(("1" (rewrite "left_coset_one[T1, *, one1]") nil nil)
("2" (typepred "G!1")
(("2" (expand* "group?" "monoid?" "monad?" "member")
(("2" (assert) nil nil)) nil))
nil))
nil)
("5" (expand "homomorphism?")
(("5" (skosimp*)
(("5" (rewrite "mult_lem[T1, *, one1]") nil nil)) nil))
nil)
("6" (skosimp*)
(("6" (prop)
(("1" (inst 1 "x!1") nil nil) ("2" (grind) nil nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (prop)
(("1" (inst 1 "x!1") nil nil) ("2" (grind) nil nil)) nil))
nil))
nil))
nil)
((/ const-decl "group[left_cosets(G, N), mult(G, N), N]"
right_left_cosets nil)
(mult const-decl "left_cosets(G, H)" factor_groups "algebra/")
(left_cosets type-eq-decl nil cosets "algebra/")
(K!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)"
homomorphism_lemmas nil)
(normal_subgroup type-eq-decl nil normal_subgroups "algebra/")
(normal_subgroup? const-decl "boolean" normal_subgroups "algebra/")
(* const-decl "set[T]" cosets "algebra/")
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(G!1 skolem-const-decl "group[T1, *, one1]" homomorphism_lemmas
nil)
(group nonempty-type-eq-decl nil group "algebra/")
(group? const-decl "bool" group_def "algebra/")
(one1 formal-const-decl "T1" homomorphism_lemmas nil)
(* formal-const-decl "[T1, T1 -> T1]" homomorphism_lemmas nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T1 formal-type-decl nil homomorphism_lemmas nil)
(fullset const-decl "set" sets nil)
(homomorphism type-eq-decl nil homomorphisms "algebra/")
(subgroup? const-decl "bool" group_def "algebra/")
(subgroup type-eq-decl nil group "algebra/")
(kernel const-decl "subgroup[T1, *, one1](G)" homomorphisms
"algebra/")
(one_right formula-decl nil group "algebra/")
(inv const-decl "{y | x * y = one AND y * x = one}" group
"algebra/")
(x!1 skolem-const-decl "T1" homomorphism_lemmas nil)
(x!2 skolem-const-decl "T1" homomorphism_lemmas nil)
(inv_right formula-decl nil group "algebra/")
(one_left formula-decl nil group "algebra/")
(assoc formula-decl nil group "algebra/")
(inv_in formula-decl nil group "algebra/")
(star_closed? const-decl "bool" groupoid_def "algebra/")
(monad? const-decl "bool" monad_def "algebra/")
(monoid? const-decl "bool" monoid_def "algebra/")
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(left_cosets_group formula-decl nil factor_groups "algebra/")
(T1_is_group formula-decl nil homomorphism_lemmas nil)
(left_coset_one formula-decl nil cosets "algebra/")
(restrict const-decl "R" restrict nil)
(left_cosets const-decl "setofsets[T]" right_left_cosets nil)
(surjective? const-decl "bool" functions nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(homomorphism? const-decl "bool" homomorphisms "algebra/")
(mult_lem formula-decl nil factor_groups "algebra/"))
shostak))
(homo_inv_TCC1 0
(homo_inv_TCC1-1 nil 3524504949
("" (skosimp*)
(("" (typepred "x!1")
(("" (rewrite "inv_in[T1, *, one1]") nil nil)) nil))
nil)
((group nonempty-type-eq-decl nil group "algebra/")
(group? const-decl "bool" group_def "algebra/")
(one1 formal-const-decl "T1" homomorphism_lemmas nil)
(* formal-const-decl "[T1, T1 -> T1]" homomorphism_lemmas nil)
(set type-eq-decl nil sets nil)
(T1 formal-type-decl nil homomorphism_lemmas nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(inv_in formula-decl nil group "algebra/"))
nil))
(homo_inv 0
(homo_inv-1 nil 3524504972
("" (skosimp*)
(("" (lemma "inv_left[T1, *, one1]")
(("" (lemma "inv_right[T1, *, one1]")
(("" (inst?)
(("" (inst?)
(("" (typepred "phi!1")
(("" (expand "homomorphism?")
(("" (copy -1)
(("" (inst -1 "x!1" "inv[T1, *, one1](x!1)")
(("1" (inst -2 "inv[T1, *, one1](x!1)" "x!1")
(("1" (replaces -3)
(("1" (replaces -3)
(("1" (lemma "homo_one[T1,*,one1,T2,o,one2]")
(("1" (inst -1 "G!1" "GP!1" "phi!1")
(("1"
(replaces -1)
(("1"
(lemma "unique_inv[T2, o, one2]")
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "inv_in[T1, *, one1]") nil nil))
nil)
("2" (rewrite "inv_in[T1, *, one1]") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((one1 formal-const-decl "T1" homomorphism_lemmas nil)
(* formal-const-decl "[T1, T1 -> T1]" homomorphism_lemmas nil)
(T1 formal-type-decl nil homomorphism_lemmas nil)
(inv_left formula-decl nil group "algebra/")
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(group? const-decl "bool" group_def "algebra/")
(group nonempty-type-eq-decl nil group "algebra/")
(homomorphism type-eq-decl nil homomorphisms "algebra/")
(homomorphism? const-decl "bool" homomorphisms "algebra/")
(one2 formal-const-decl "T2" homomorphism_lemmas nil)
(O formal-const-decl "[T2, T2 -> T2]" homomorphism_lemmas nil)
(T2 formal-type-decl nil homomorphism_lemmas nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(unique_inv formula-decl nil group "algebra/")
(homo_one formula-decl nil homomorphisms "algebra/")
(inv_in formula-decl nil group "algebra/")
(x!1 skolem-const-decl "(G!1)" homomorphism_lemmas nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group
"algebra/")
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(G!1 skolem-const-decl "group[T1, *, one1]" homomorphism_lemmas
nil)
(inv_right formula-decl nil group "algebra/"))
shostak))
(kernel_normal 0
(kernel_normal-1 nil 3524504993
("" (skeep)
(("" (skoletin* 1)
(("" (expand "normal_subgroup?")
(("" (assert)
(("" (skeep)
(("" (expand "subset?")
(("" (skeep)
(("" (expand "member")
(("" (expand "K" 1)
(("" (grind)
(("1" (typepred "phi")
(("1" (expand "homomorphism?")
(("1" (copy -1)
(("1"
(inst -1 "inv[T1, *, one1](a) * h!2" "a")
(("1"
(replaces -1)
(("1"
(inst -1 "inv[T1, *, one1](a)" "h!2")
(("1"
(replaces -1)
(("1"
(replaces -2)
(("1"
(lemma
"one_right[T2, o, one2]")
(("1"
(inst?)
(("1"
(replaces -1)
(("1"
(rewrite "homo_inv")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(typepred "a")
(("2"
(rewrite "inv_in[T1, *, one1]")
nil
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(typepred "a")
(("2"
(lemma "inv_in[T1, *, one1]")
(("2"
(inst?)
(("2"
(typepred "G")
(("2"
(expand "group?")
(("2"
(flatten)
(("2"
(expand "monoid?")
(("2"
(flatten)
(("2"
(expand "monad?")
(("2"
(flatten)
(("2"
(expand
"star_closed?")
(("2"
(hide-all-but
(-1 -6 -7 1))
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-1 1))
(("2" (typepred "a")
(("2" (lemma "inv_in[T1, *, one1]")
(("2" (inst?)
(("2"
(typepred "G")
(("2"
(expand "group?")
(("2"
(flatten)
(("2"
(expand "monoid?")
(("2"
(flatten)
(("2"
(expand "monad?")
(("2"
(flatten)
(("2"
(expand "star_closed?")
(("2"
(hide-all-but
(-1 -6 -7 -8 1))
(("2"
(copy -1)
(("2"
(inst
-2
"inv[T1, *, one1](a)"
"h!2")
(("2"
(expand "member")
(("2"
(inst
-1
"inv[T1, *, one1](a) * h!2"
"a")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((IFF const-decl "[bool, bool -> bool]" booleans nil)
(T1 formal-type-decl nil homomorphism_lemmas nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(* formal-const-decl "[T1, T1 -> T1]" homomorphism_lemmas nil)
(one1 formal-const-decl "T1" homomorphism_lemmas nil)
(group? const-decl "bool" group_def "algebra/")
(group nonempty-type-eq-decl nil group "algebra/")
(T2 formal-type-decl nil homomorphism_lemmas nil)
(O formal-const-decl "[T2, T2 -> T2]" homomorphism_lemmas nil)
(one2 formal-const-decl "T2" homomorphism_lemmas nil)
(homomorphism? const-decl "bool" homomorphisms "algebra/")
(homomorphism type-eq-decl nil homomorphisms "algebra/")
(subgroup? const-decl "bool" group_def "algebra/")
(subgroup type-eq-decl nil group "algebra/")
(kernel const-decl "subgroup[T1, *, one1](G)" homomorphisms
"algebra/")
(normal_subgroup? const-decl "boolean" normal_subgroups "algebra/")
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(* const-decl "set[T]" cosets "algebra/")
(NOT const-decl "[bool -> bool]" booleans nil)
(* const-decl "set[T]" cosets "algebra/")
(AND const-decl "[bool, bool -> bool]" booleans nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group
"algebra/")
(G skolem-const-decl "group[T1, *, one1]" homomorphism_lemmas nil)
(a skolem-const-decl "(G)" homomorphism_lemmas nil)
(GP skolem-const-decl "group[T2, o, one2]" homomorphism_lemmas nil)
(phi skolem-const-decl
"homomorphism[T1, *, one1, T2, o, one2](G, GP)"
homomorphism_lemmas nil)
(h!2 skolem-const-decl "(kernel(G, GP)(phi))" homomorphism_lemmas
nil)
(homo_inv formula-decl nil homomorphism_lemmas nil)
(one_right formula-decl nil group "algebra/")
(inv_in formula-decl nil group "algebra/")
(monoid? const-decl "bool" monoid_def "algebra/")
(monad? const-decl "bool" monad_def "algebra/")
(star_closed? const-decl "bool" groupoid_def "algebra/")
(h!2 skolem-const-decl "(kernel(G, GP)(phi))" homomorphism_lemmas
nil)
(K skolem-const-decl "subgroup[T1, *, one1](G)" homomorphism_lemmas
nil))
shostak))
(homo_image 0
(homo_image-1 nil 3524526933
("" (skosimp*)
(("" (lemma "subgroup_def[T2, o, one2]")
(("" (inst?)
(("" (assert)
(("" (hide 2)
(("" (prop)
(("1" (expand "nonempty?")
(("1" (expand "empty?")
(("1" (expand "member")
(("1" (expand "extend")
(("1" (inst -1 "one2")
(("1" (typepred "GP!1")
(("1" (expand "group?")
(("1" (flatten)
(("1"
(expand "monoid?")
(("1"
(flatten)
(("1"
(expand "monad?")
(("1"
(flatten)
(("1"
(hide-all-but (-2 1))
(("1"
(expand "member")
(("1"
(assert)
(("1"
(expand "image")
(("1"
(inst 1 "one1")
(("1"
(rewrite
"homo_one[T1, *, one1,T2, o, one2]")
nil
nil)
("2"
(prop)
(("1"
(typepred "G!1")
(("1"
(expand "group?")
(("1"
(flatten)
(("1"
(expand
"monoid?")
(("1"
(flatten)
(("1"
(expand
"monad?")
(("1"
(flatten)
(("1"
(expand
"member")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "restrict")
(("2"
(typepred "H!1")
(("2"
(expand
"group?")
(("2"
(flatten)
(("2"
(expand
"monoid?")
(("2"
(flatten)
(("2"
(expand
"monad?")
(("2"
(flatten)
(("2"
(expand
"member")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "subset?")
(("2" (skosimp*)
(("2" (expand "member")
(("2" (expand "extend") (("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("3" (expand "star_closed?")
(("3" (skosimp*)
(("3" (expand "member")
(("3" (expand "extend")
(("3" (prop)
(("1" (typepred "x!1")
(("1" (typepred "y!1")
(("1" (expand "extend")
(("1"
(prop)
(("1"
(expand "image")
(("1"
(skosimp)
(("1"
(skosimp)
(("1"
(inst 1 "x!2 * x!3")
(("1"
(typepred "phi!1")
(("1"
(expand "homomorphism?")
(("1"
(inst -1 "x!2" "x!3")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(prop)
(("1"
(typepred "x!2")
(("1"
(typepred "x!3")
(("1"
(typepred "G!1")
(("1"
(expand "group?")
(("1"
(flatten)
(("1"
(expand
"monoid?")
(("1"
(flatten)
(("1"
(expand
"monad?")
(("1"
(flatten)
(("1"
(hide-all-but
(-1
-6
-8
1))
(("1"
(expand
"star_closed?")
(("1"
(inst?)
(("1"
(expand
"member")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "restrict")
(("2"
(typepred "x!2")
(("2"
(typepred "x!3")
(("2"
(typepred "H!1")
(("2"
(expand "group?")
(("2"
(flatten)
(("2"
(expand
"monoid?")
(("2"
(flatten)
(("2"
(expand
"monad?")
(("2"
(flatten)
(("2"
(hide-all-but
(-1
-8
-10
1))
(("2"
(expand*
"restrict"
"star_closed?"
"member")
(("2"
(inst?)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "GP!1")
(("2" (expand "group?")
(("2" (flatten)
(("2"
(expand "monoid?")
(("2"
(flatten)
(("2"
(expand "monad?")
(("2"
(flatten)
(("2"
(typepred "x!1")
(("2"
(typepred "y!1")
(("2"
(expand*
"extend"
"star_closed?"
"member"
"image")
(("2"
(prop)
(("2"
(hide-all-but
(-1 -3 -5 1))
(("2" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (expand "inv_closed?")
(("4" (skosimp*)
(("4" (expand* "member" "extend" "image" "restrict")
(("4" (prop)
(("1" (typepred "x!1")
(("1" (expand* "extend" "image" "restrict")
(("1" (prop)
(("1" (skosimp)
(("1"
(typepred "x!2")
(("1"
(inst 1 "inv[T1, *, one1](x!2)")
(("1"
(rewrite "homo_inv")
(("1" (assert) nil nil))
nil)
("2"
(prop)
(("1"
(hide-all-but (-1 1))
(("1"
(rewrite "inv_in")
nil
nil))
nil)
("2"
(expand "restrict")
(("2"
(hide-all-but (-2 1))
(("2"
(rewrite "inv_in")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "x!1")
(("2" (expand "extend")
(("2" (prop)
(("2" (rewrite "inv_in") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((one2 formal-const-decl "T2" homomorphism_lemmas nil)
(O formal-const-decl "[T2, T2 -> T2]" homomorphism_lemmas nil)
(T2 formal-type-decl nil homomorphism_lemmas nil)
(subgroup_def formula-decl nil group "algebra/")
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(empty? const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(homo_one formula-decl nil homomorphisms "algebra/")
(H!1 skolem-const-decl "subgroup[T1, *, one1](G!1)"
homomorphism_lemmas nil)
(G!1 skolem-const-decl "group[T1, *, one1]" homomorphism_lemmas
nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(monad? const-decl "bool" monad_def "algebra/")
(monoid? const-decl "bool" monoid_def "algebra/")
(member const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(x!1 skolem-const-decl "(extend[T2, (GP!1), bool, FALSE]
(image(phi!1, restrict[T1, (G!1), boolean](H!1))))"
homomorphism_lemmas nil)
(y!1 skolem-const-decl "(extend[T2, (GP!1), bool, FALSE]
(image(phi!1, restrict[T1, (G!1), boolean](H!1))))"
homomorphism_lemmas nil)
(phi!1 skolem-const-decl
"homomorphism[T1, *, one1, T2, o, one2](G!1, GP!1)"
homomorphism_lemmas nil)
(GP!1 skolem-const-decl "group[T2, o, one2]" homomorphism_lemmas
nil)
(x!3 skolem-const-decl "(restrict[T1, (G!1), boolean](H!1))"
homomorphism_lemmas nil)
(x!2 skolem-const-decl "(restrict[T1, (G!1), boolean](H!1))"
homomorphism_lemmas nil)
(star_closed? const-decl "bool" groupoid_def "algebra/")
(= const-decl "[T, T -> boolean]" equalities nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group
"algebra/")
(x!2 skolem-const-decl "(restrict[T1, (G!1), boolean](H!1))"
homomorphism_lemmas nil)
(homo_inv formula-decl nil homomorphism_lemmas nil)
(inv_in formula-decl nil group "algebra/")
(inv_closed? const-decl "bool" group "algebra/")
(subgroup type-eq-decl nil group "algebra/")
(subgroup? const-decl "bool" group_def "algebra/")
(restrict const-decl "R" restrict nil)
(homomorphism type-eq-decl nil homomorphisms "algebra/")
(homomorphism? const-decl "bool" homomorphisms "algebra/")
(image const-decl "set[R]" function_image nil)
(one1 formal-const-decl "T1" homomorphism_lemmas nil)
(* formal-const-decl "[T1, T1 -> T1]" homomorphism_lemmas nil)
(T1 formal-type-decl nil homomorphism_lemmas nil)
(extend const-decl "R" extend nil)
(FALSE const-decl "bool" booleans nil)
(group nonempty-type-eq-decl nil group "algebra/")
(group? const-decl "bool" group_def "algebra/")
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(homo_image_normal_TCC1 0
(homo_image_normal_TCC1-1 nil 3530914988
("" (skosimp*)
(("" (lemma "homo_image")
(("" (inst?)
(("1" (lemma "subgroup_is_group[T2, o, one2]")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
("2" (hide 2)
(("2" (typepred "H!1")
(("2" (expand "normal_subgroup?") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((homo_image formula-decl nil homomorphism_lemmas nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(subgroup_is_group formula-decl nil group "algebra/")
(FALSE const-decl "bool" booleans nil)
(extend const-decl "R" extend nil)
(image const-decl "set[R]" function_image nil)
(restrict const-decl "R" restrict nil)
(subgroup type-eq-decl nil group "algebra/")
(homomorphism type-eq-decl nil homomorphisms "algebra/")
(homomorphism? const-decl "bool" homomorphisms "algebra/")
(one2 formal-const-decl "T2" homomorphism_lemmas nil)
(O formal-const-decl "[T2, T2 -> T2]" homomorphism_lemmas nil)
(T2 formal-type-decl nil homomorphism_lemmas nil)
(T1 formal-type-decl nil homomorphism_lemmas nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(* formal-const-decl "[T1, T1 -> T1]" homomorphism_lemmas nil)
(one1 formal-const-decl "T1" homomorphism_lemmas nil)
(group? const-decl "bool" group_def "algebra/")
(subgroup? const-decl "bool" group_def "algebra/")
(group nonempty-type-eq-decl nil group "algebra/")
(normal_subgroup? const-decl "boolean" normal_subgroups "algebra/")
(G!1 skolem-const-decl "group[T1, *, one1]" homomorphism_lemmas
nil)
(normal_subgroup type-eq-decl nil normal_subgroups "algebra/")
(H!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)"
homomorphism_lemmas nil))
nil))
(homo_image_normal 0
(homo_image_normal-1 nil 3530915201
("" (skosimp*)
(("" (typepred "H!1")
(("" (hide -1)
(("" (expand "normal_subgroup?")
(("" (flatten)
(("" (lemma "homo_image")
(("" (inst?)
(("" (assert)
(("" (hide -1)
(("" (expand* "subset?" "member")
(("" (skosimp*)
(("" (expand "extend" 1)
(("" (prop)
(("1" (expand "surjective?")
(("1"
(expand "*" -5)
(("1"
(skosimp)
(("1"
(typepred "h!1")
(("1"
(skosimp)
(("1"
(replaces -1)
(("1"
(typepred "h!2")
(("1"
(expand "extend")
(("1"
(prop)
(("1"
(expand "image")
(("1"
(skosimp)
(("1"
(inst -6 "a!1")
(("1"
(skosimp)
(("1"
(inst
1
"inv[T1, *, one1](x!3) * x!2 * x!3")
(("1"
(hide-all-but
(-2
-6
-7
1))
(("1"
(typepred
"phi!1")
(("1"
(expand
"homomorphism?")
(("1"
(inst-cp
-1
"inv[T1, *, one1](x!3) * x!2"
"x!3")
(("1"
(inst
-1
"inv[T1, *, one1](x!3)"
"x!2")
(("1"
(replaces
-1)
(("1"
(replaces
-1)
(("1"
(lemma
"homo_inv[T1, *, one1,T2, o, one2]")
(("1"
(inst?)
(("1"
(replaces
-1)
(("1"
(replaces
-2)
(("1"
(replace
-1
1
rl)
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(rewrite
"inv_in")
nil
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(rewrite
"product_in[T1, *, one1]")
(("2"
(hide
2)
(("2"
(rewrite
"inv_in")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(prop)
(("1"
(hide-all-but
1)
(("1"
(rewrite
"product_in[T1, *, one1]")
(("1"
(hide
2)
(("1"
(rewrite
"product_in[T1, *, one1]")
(("1"
(hide
2)
(("1"
(rewrite
"inv_in")
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"restrict")
(("2"
(hide-all-but
(-5 1))
(("2"
(typepred
"x!2")
(("2"
(expand
"restrict")
(("2"
(hide
-1)
(("2"
(inst
-2
"x!3")
(("2"
(inst
-2
"inv[T1, *, one1](x!3) * x!2 * x!3")
(("2"
(assert)
(("2"
(hide
1)
(("2"
(expand
"*")
(("2"
(inst
1
"inv[T1, *, one1](x!3) * x!2")
(("2"
(inst
1
"x!2")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.135 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
