|
(normal_subgroups
(IMP_cosets_TCC1 0
(IMP_cosets_TCC1-1 nil 3406034865
("" (lemma "fullset_is_group") (("" (propax) nil nil)) nil)
((fullset_is_group formula-decl nil normal_subgroups nil)) nil))
(normal_prep 0
(normal_prep-2 nil 3406302414
("" (skosimp*)
(("" (typepred "G!1")
(("" (case "N!1 = a!1 * (inv(a!1) * N!1 * a!1) * inv(a!1)")
(("1"
(case "subset?(a!1 * (inv(a!1) * N!1 * a!1) * inv(a!1),a!1 * N!1 * inv(a!1))")
(("1"
(case "a!1 * N!1 * inv(a!1) = inv(inv(a!1)) * N!1 * inv(a!1)")
(("1" (inst -5 "inv(a!1)")
(("1" (assert)
(("1" (replace -3 -2 rl)
(("1" (hide -1 -3 -4 -6)
(("1" (lemma "subset_antisymmetric[T]")
(("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (rewrite "inv_in") nil nil))
nil)
("2" (hide 2) (("2" (rewrite "inv_inv") nil nil)) nil))
nil)
("2" (hide 2)
(("2" (inst?)
(("2" (name "ANA" "inv(a!1) * N!1 * a!1")
(("2" (replace -1)
(("2" (lemma "subset_left_coset")
(("2" (inst - "N!1" "ANA" "a!1")
(("2" (assert)
(("2" (lemma "subset_right_coset")
(("2" (inst - "a!1*N!1" "a!1*ANA" "inv(a!1)")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2"
(case "a!1 * (inv(a!1) * N!1 * a!1) * inv(a!1) = (a!1 * inv(a!1)) * N!1 * (a!1 * inv(a!1))")
(("1" (assert)
(("1" (rewrite "inv_right")
(("1" (rewrite "left_coset_one")
(("1" (rewrite "right_coset_one")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (hide -2 -3)
(("2" (assert)
(("2" (lemma "right_coset_assoc")
(("2" (inst - "inv(a!1)*N!1" "a!1" "inv(a!1)")
(("2"
(case-replace
"inv(a!1) * N!1 * a!1 * inv(a!1) = (inv(a!1) * N!1 * a!1) * inv(a!1)")
(("2" (replace -2)
(("2" (hide -1)
(("2" (expand "group?")
(("2"
(flatten)
(("2"
(expand "monoid?")
(("2"
(flatten)
(("2"
(expand "associative?")
(("2"
(expand "restrict")
(("2"
(lemma "right_coset_assoc")
(("2"
(inst
-
"(inv(a!1)*N!1)"
"a!1"
"inv(a!1)")
(("2"
(hide -1)
(("2"
(lemma
"lr_coset_assoc")
(("2"
(inst?)
(("2"
(replace -1)
(("2"
(hide -1)
(("2"
(lemma
"left_coset_assoc")
(("2"
(inst?)
(("2"
(replace
-1)
(("2"
(rewrite
"inv_right")
(("2"
(rewrite
"left_coset_one")
(("2"
(lemma
"right_coset_assoc")
(("2"
(inst?)
(("2"
(replace
-1)
(("2"
(rewrite
"inv_right")
(("2"
(rewrite
"left_coset_one")
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)
((group nonempty-type-eq-decl nil group nil)
(group? const-decl "bool" group_def nil)
(one formal-const-decl "T" normal_subgroups nil)
(* formal-const-decl "[T, T -> T]" normal_subgroups nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil normal_subgroups nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(monoid? const-decl "bool" monoid_def nil)
(associative? const-decl "bool" operator_defs nil)
(left_coset_assoc formula-decl nil cosets nil)
(lr_coset_assoc formula-decl nil cosets nil)
(restrict const-decl "R" restrict nil)
(right_coset_assoc formula-decl nil cosets nil)
(inv_right formula-decl nil group nil)
(right_coset_one formula-decl nil cosets nil)
(left_coset_one formula-decl nil cosets nil)
(subset? const-decl "bool" sets nil)
(G!1 skolem-const-decl "group[T, *, one]" normal_subgroups nil)
(a!1 skolem-const-decl "(G!1)" normal_subgroups nil)
(subset_antisymmetric formula-decl nil sets_lemmas nil)
(inv_inv formula-decl nil group nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(inv_in formula-decl nil group nil)
(subset_right_coset formula-decl nil cosets nil)
(subset_left_coset formula-decl nil cosets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(* const-decl "set[T]" cosets nil)
(* const-decl "set[T]" cosets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group nil))
nil)
(normal_prep-1 nil 3405953922
("" (skosimp*)
(("" (typepred "G!1")
(("" (case "N!1 = a!1 * (inv(a!1) * N!1 * a!1) * inv(a!1)")
(("1"
(case "subset?(a!1 * (inv(a!1) * N!1 * a!1) * inv(a!1),a!1 * N!1 * inv(a!1))")
(("1"
(case "a!1 * N!1 * inv(a!1) = inv(inv(a!1)) * N!1 * inv(a!1)")
(("1" (inst -5 "inv(a!1)")
(("1" (assert)
(("1" (replace -3 -2 rl)
(("1" (hide -1 -3 -4 -6)
(("1" (lemma "subset_antisymmetric[T]")
(("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (rewrite "inv_in") nil nil))
nil)
("2" (hide 2) (("2" (rewrite "inv_inv") nil nil)) nil))
nil)
("2" (hide 2)
(("2" (inst?)
(("2" (name "ANA" "inv(a!1) * N!1 * a!1")
(("2" (replace -1)
(("2" (lemma "left_coset_subset")
(("2" (inst - "N!1" "ANA" "a!1")
(("2" (assert)
(("2" (lemma "right_coset_subset")
(("2" (inst - "a!1*N!1" "a!1*ANA" "inv(a!1)")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2"
(case "a!1 * (inv(a!1) * N!1 * a!1) * inv(a!1) = (a!1 * inv(a!1)) * N!1 * (a!1 * inv(a!1))")
(("1" (assert)
(("1" (rewrite "inv_right")
(("1" (rewrite "left_coset_one")
(("1" (rewrite "right_coset_one")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (hide -2 -3)
(("2" (assert)
(("2" (lemma "right_coset_assoc")
(("2" (inst - "inv(a!1)*N!1" "a!1" "inv(a!1)")
(("2"
(case-replace
"inv(a!1) * N!1 * a!1 * inv(a!1) = (inv(a!1) * N!1 * a!1) * inv(a!1)")
(("2" (replace -2)
(("2" (hide -1)
(("2" (expand "group?")
(("2"
(flatten)
(("2"
(expand "monoid?")
(("2"
(flatten)
(("2"
(expand "associative?")
(("2"
(expand "restrict")
(("2"
(lemma "right_coset_assoc")
(("2"
(inst
-
"(inv(a!1)*N!1)"
"a!1"
"inv(a!1)")
(("2"
(hide -1)
(("2"
(lemma
"lr_coset_assoc")
(("2"
(inst?)
(("2"
(replace -1)
(("2"
(hide -1)
(("2"
(lemma
"left_coset_assoc")
(("2"
(inst?)
(("2"
(replace
-1)
(("2"
(rewrite
"inv_right")
(("2"
(rewrite
"left_coset_one")
(("2"
(lemma
"right_coset_assoc")
(("2"
(inst?)
(("2"
(replace
-1)
(("2"
(rewrite
"inv_right")
(("2"
(rewrite
"left_coset_one")
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)
((group nonempty-type-eq-decl nil group nil)
(group? const-decl "bool" group_def nil)
(monoid? const-decl "bool" monoid_def nil)
(left_coset_assoc formula-decl nil cosets nil)
(lr_coset_assoc formula-decl nil cosets nil)
(right_coset_assoc formula-decl nil cosets nil)
(left_coset_one formula-decl nil cosets nil)
(right_coset_one formula-decl nil cosets nil)
(inv_right formula-decl nil group nil)
(inv_inv formula-decl nil group nil)
(inv_in formula-decl nil group nil)
(right_coset_subset formula-decl nil cosets nil)
(left_coset_subset formula-decl nil cosets nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group nil))
nil))
(normal_left_is_right 0
(normal_left_is_right-3 nil 3405953953
("" (skosimp*)
(("" (prop)
(("1" (expand "normal_subgroup?") (("1" (flatten) nil nil)) nil)
("2" (expand "normal_subgroup?")
(("2" (flatten)
(("2" (lemma "normal_prep")
(("2" (inst - "G!1" "N!1")
(("2" (assert)
(("2" (replace -3)
(("2" (skosimp*)
(("2" (inst?)
(("2" (case "a!1 * N!1 * inv(a!1)*a!1 = N!1*a!1")
(("1" (hide -2)
(("1" (expand "subgroup?")
(("1" (lemma "right_coset_assoc")
(("1"
(inst?)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(rewrite "inv_left")
(("1"
(rewrite "right_coset_one")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "normal_subgroup?")
(("3" (assert)
(("3" (skosimp*)
(("3" (inst?)
(("1" (replace -2)
(("1" (lemma "right_coset_assoc")
(("1" (inst?)
(("1" (replace -1)
(("1" (rewrite "inv_left")
(("1" (rewrite "right_coset_one")
(("1" (hide -1 -2 -3) (("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (typepred "a!1")
(("2" (rewrite "inv_in") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((normal_subgroup? const-decl "boolean" normal_subgroups nil)
(T formal-nonempty-type-decl nil normal_subgroups 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 "[T, T -> T]" normal_subgroups nil)
(one formal-const-decl "T" normal_subgroups nil)
(group? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil)
(right_coset_assoc formula-decl nil cosets nil)
(inv_left formula-decl nil group nil)
(right_coset_one formula-decl nil cosets nil)
(subgroup? const-decl "bool" group_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(* const-decl "set[T]" cosets nil)
(* const-decl "set[T]" cosets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(normal_prep formula-decl nil normal_subgroups nil)
(a!1 skolem-const-decl "(G!1)" normal_subgroups nil)
(G!1 skolem-const-decl "group[T, *, one]" normal_subgroups nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(inv_in formula-decl nil group nil))
nil)
(normal_left_is_right-2 nil 3405952612
("" (skosimp*)
(("" (prop)
(("1" (expand "normal_subgroup?") (("1" (flatten) nil nil)) nil)
("2" (expand "normal_subgroup?")
(("2" (flatten)
(("2" (lemma "prep")
(("2" (inst - "G!1" "N!1")
(("2" (assert)
(("2" (replace -3)
(("2" (skosimp*)
(("2" (inst?)
(("2" (case "a!1 * N!1 * inv(a!1)*a!1 = N!1*a!1")
(("1" (hide -2)
(("1" (expand "subgroup?")
(("1" (lemma "right_coset_assoc")
(("1"
(inst?)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(rewrite "inv_left")
(("1"
(rewrite "right_coset_one")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "normal_subgroup?")
(("3" (assert)
(("3" (skosimp*)
(("3" (inst?)
(("1" (replace -2)
(("1" (lemma "right_coset_assoc")
(("1" (inst?)
(("1" (replace -1)
(("1" (rewrite "inv_left")
(("1" (rewrite "right_coset_one")
(("1" (hide -1 -2 -3) (("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (typepred "a!1")
(("2" (rewrite "inv_in") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((group? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil)
(inv_left formula-decl nil group nil)
(subgroup? const-decl "bool" group_def nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(inv_in formula-decl nil group nil))
nil)
(normal_left_is_right-1 nil 3397296944
("" (skosimp*)
(("" (prop)
(("1" (expand "normal?") (("1" (flatten) nil nil)) nil)
("2" (expand "normal?")
(("2" (flatten)
(("2" (lemma "prep")
(("2" (inst - "G!1" "N!1")
(("2" (assert)
(("2" (replace -3)
(("2" (skosimp*)
(("2" (inst?)
(("2" (case "a!1 * N!1 * inv(a!1)*a!1 = N!1*a!1")
(("1" (hide -2)
(("1" (expand "subgroup?")
(("1" (lemma "right_coset_assoc")
(("1"
(inst?)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(rewrite "inv_left")
(("1"
(rewrite "right_coset_one")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "normal?")
(("3" (assert)
(("3" (skosimp*)
(("3" (inst?)
(("1" (replace -2)
(("1" (lemma "right_coset_assoc")
(("1" (inst?)
(("1" (replace -1)
(("1" (rewrite "inv_left")
(("1" (rewrite "right_coset_one")
(("1" (hide -1 -2 -3) (("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (typepred "a!1")
(("2" (rewrite "inv_in") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((group? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil)
(inv_left formula-decl nil group nil)
(subgroup? const-decl "bool" group_def nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(inv_in formula-decl nil group nil))
shostak))
(normal_subgroup_is_subgroup 0
(normal_subgroup_is_subgroup-1 nil 3405954274
("" (skosimp*)
(("" (typepred "x!1")
(("" (expand "normal_subgroup?") (("" (flatten) nil nil)) nil))
nil))
nil)
((normal_subgroup type-eq-decl nil normal_subgroups nil)
(normal_subgroup? const-decl "boolean" normal_subgroups nil)
(group nonempty-type-eq-decl nil group nil)
(group? const-decl "bool" group_def nil)
(one formal-const-decl "T" normal_subgroups nil)
(* formal-const-decl "[T, T -> T]" normal_subgroups nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil normal_subgroups nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(nsg_prop 0
(nsg_prop-1 nil 3406563746
("" (skosimp*)
(("" (typepred "H!1")
(("" (expand "normal_subgroup?")
(("" (flatten)
(("" (inst - "inv(a!1)")
(("1" (expand "subset?")
(("1" (assert)
(("1" (inst - "a!1 * h!1 * inv(a!1)")
(("1" (assert)
(("1" (hide 2)
(("1" (expand "*")
(("1" (inst + "a!1*h!1")
(("1" (inst + "h!1") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2) (("2" (rewrite "inv_in") nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((normal_subgroup type-eq-decl nil normal_subgroups nil)
(normal_subgroup? const-decl "boolean" normal_subgroups nil)
(group nonempty-type-eq-decl nil group nil)
(group? const-decl "bool" group_def nil)
(one formal-const-decl "T" normal_subgroups nil)
(* formal-const-decl "[T, T -> T]" normal_subgroups nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil normal_subgroups 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 nil)
(subset? const-decl "bool" sets nil)
(H!1 skolem-const-decl "normal_subgroup(G!1)" normal_subgroups nil)
(h!1 skolem-const-decl "T" normal_subgroups nil)
(* const-decl "set[T]" cosets nil)
(* const-decl "set[T]" cosets nil)
(member const-decl "bool" sets nil)
(inv_inv formula-decl nil group nil)
(G!1 skolem-const-decl "group[T, *, one]" normal_subgroups nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(a!1 skolem-const-decl "T" normal_subgroups nil))
nil))
(nsg_prop2 0
(nsg_prop2-1 nil 3406563783
("" (skosimp*)
(("" (typepred "H!1")
(("" (expand "normal_subgroup?")
(("" (flatten)
(("" (inst - "a!1")
(("" (expand "subset?")
(("" (assert)
(("" (inst - "inv(a!1)*h!1*a!1")
(("" (assert)
(("" (hide 2)
(("" (expand "*")
(("" (inst + "inv(a!1)*h!1")
(("" (inst + "h!1") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((normal_subgroup type-eq-decl nil normal_subgroups nil)
(normal_subgroup? const-decl "boolean" normal_subgroups nil)
(group nonempty-type-eq-decl nil group nil)
(group? const-decl "bool" group_def nil)
(one formal-const-decl "T" normal_subgroups nil)
(* formal-const-decl "[T, T -> T]" normal_subgroups nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil normal_subgroups nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(subset? const-decl "bool" sets nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(H!1 skolem-const-decl "normal_subgroup(G!1)" normal_subgroups nil)
(h!1 skolem-const-decl "T" normal_subgroups nil)
(* const-decl "set[T]" cosets nil)
(* const-decl "set[T]" cosets nil)
(member const-decl "bool" sets nil)
(a!1 skolem-const-decl "T" normal_subgroups nil)
(G!1 skolem-const-decl "group[T, *, one]" normal_subgroups nil))
nil))
(lc_gen_normal_TCC1 0
(lc_gen_normal_TCC1-1 nil 3406564260 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(group? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(one formal-const-decl "T" normal_subgroups nil)
(* formal-const-decl "[T, T -> T]" normal_subgroups nil)
(T formal-nonempty-type-decl nil normal_subgroups nil)
(subgroup? const-decl "bool" group_def nil)
(* const-decl "set[T]" cosets nil)
(normal_subgroup? const-decl "boolean" normal_subgroups nil))
nil))
(lc_gen_normal_TCC2 0
(lc_gen_normal_TCC2-1 nil 3406564260
("" (skosimp*) (("" (inst + "a!1") nil nil)) nil)
((T formal-nonempty-type-decl nil normal_subgroups 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 "[T, T -> T]" normal_subgroups nil)
(one formal-const-decl "T" normal_subgroups nil)
(group? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil)
(a!1 skolem-const-decl "T" normal_subgroups nil)
(G!1 skolem-const-decl "group[T, *, one]" normal_subgroups nil))
nil))
(lc_gen_normal 0
(lc_gen_normal-1 nil 3406564267
("" (skosimp*)
(("" (lemma "lc_gen_def")
(("" (inst?)
(("" (assert)
(("" (expand "normal_subgroup?")
(("" (flatten)
(("" (assert)
(("" (name "aa" "lc_gen(G!1, H!1, a!1 * H!1)")
(("" (replace -1)
(("" (lemma "lc_eq")
(("" (inst - "G!1" "H!1" "aa" "a!1")
(("" (assert)
(("" (skosimp*)
(("" (replace -1)
((""
(inst + "a!1*h!1*inv(a!1)")
(("1"
(rewrite "associative")
(("1"
(rewrite "associative")
(("1"
(rewrite "associative")
(("1"
(rewrite "inv_left")
(("1"
(rewrite "one_right")
nil
nil))
nil))
nil))
nil))
nil)
("2"
(lemma "nsg_prop")
(("2"
(inst?)
(("2"
(inst - "G!1" "H!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((one formal-const-decl "T" normal_subgroups nil)
(* formal-const-decl "[T, T -> T]" normal_subgroups nil)
(T formal-nonempty-type-decl nil normal_subgroups nil)
(lc_gen_def formula-decl nil cosets nil)
(lc_gen const-decl "{a: T | G(a) AND lc = a * H}" cosets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(left_cosets type-eq-decl nil cosets nil)
(subgroup? const-decl "bool" group_def nil)
(* const-decl "set[T]" cosets nil)
(subgroup type-eq-decl nil group nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(lc_eq formula-decl nil cosets nil)
(nsg_prop formula-decl nil normal_subgroups nil)
(normal_subgroup type-eq-decl nil normal_subgroups nil)
(associative formula-decl nil semigroup nil)
(one_right formula-decl nil group nil)
(inv_left formula-decl nil group nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(h!1 skolem-const-decl "(H!1)" normal_subgroups nil)
(a!1 skolem-const-decl "T" normal_subgroups nil)
(H!1 skolem-const-decl "group[T, *, one]" normal_subgroups nil)
(normal_subgroup? const-decl "boolean" normal_subgroups nil)
(group nonempty-type-eq-decl nil group nil)
(group? const-decl "bool" group_def nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(abelian_normal 0
(abelian_normal-1 nil 3406306875
("" (skosimp*)
(("" (expand "normal_subgroup?")
(("" (assert)
(("" (skosimp*)
(("" (expand "subset?")
(("" (skosimp*)
(("" (assert)
(("" (expand "*")
(("" (skosimp*)
(("" (replace -3)
(("" (typepred "h!1")
(("" (skosimp*)
(("" (typepred "h!2")
(("" (replace -2)
((""
(hide -2)
((""
(hide -4)
((""
(expand "abelian_group?")
((""
(expand "commutative?")
((""
(expand "restrict")
((""
(inst -2 "h!2" "a!1")
(("1"
(rewrite "associative")
(("1"
(replace -2)
(("1"
(rewrite "assoc")
(("1"
(rewrite "inv_left")
(("1"
(rewrite
"one_left")
nil
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand "subgroup?")
(("2"
(expand "subset?")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((normal_subgroup? const-decl "boolean" normal_subgroups nil)
(* const-decl "set[T]" cosets nil)
(* const-decl "set[T]" cosets nil)
(commutative? const-decl "bool" operator_defs nil)
(G!1 skolem-const-decl "group[T, *, one]" normal_subgroups nil)
(H!1 skolem-const-decl "group[T, *, one]" normal_subgroups nil)
(h!2 skolem-const-decl "(H!1)" normal_subgroups nil)
(assoc formula-decl nil group nil)
(inv_left formula-decl nil group nil)
(one_left formula-decl nil group nil)
(associative formula-decl nil semigroup nil)
(subgroup? const-decl "bool" group_def nil)
(restrict const-decl "R" restrict nil)
(abelian_group? const-decl "bool" group_def nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-nonempty-type-decl nil normal_subgroups nil)
(set type-eq-decl nil sets nil)
(* formal-const-decl "[T, T -> T]" normal_subgroups nil)
(one formal-const-decl "T" normal_subgroups nil)
(group? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil))
shostak)))
¤ Dauer der Verarbeitung: 0.76 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
