|
(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)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.169 Sekunden
(vorverarbeitet)
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
