|
(factor_groups
(IMP_normal_subgroups_TCC1 0
(IMP_normal_subgroups_TCC1-1 nil 3405954319
("" (lemma "fullset_is_group") (("" (propax) nil nil)) nil)
((fullset_is_group formula-decl nil factor_groups nil)) nil))
(p0 0
(p0-1 nil 3406303495
("" (skosimp*)
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (expand "member")
(("" (typepred "B!1")
(("" (typepred "A!1")
(("" (skosimp*)
(("" (replace -1)
(("" (hide -1)
(("" (replace -1)
(("" (hide -1)
(("" (inst - "(a!1*a!2)*H!1")
(("" (inst + "a!1" "a!2") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nonempty? const-decl "bool" sets nil)
(member const-decl "bool" sets 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 factor_groups nil)
(set type-eq-decl nil sets nil)
(* formal-const-decl "[T, T -> T]" factor_groups nil)
(one formal-const-decl "T" factor_groups nil)
(group? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(* const-decl "set[T]" cosets nil)
(normal_subgroup? const-decl "boolean" normal_subgroups nil)
(normal_subgroup type-eq-decl nil normal_subgroups nil)
(left_cosets type-eq-decl nil cosets nil)
(empty? const-decl "bool" sets nil))
shostak))
(prep 0
(prep-1 nil 3405949082
("" (skosimp*)
(("" (rewrite "left_coset_assoc" 1 :dir rl)
(("" (lemma "normal_left_is_right")
(("" (inst - "G!1" "H!1")
(("" (assert)
(("" (flatten)
(("" (inst - "b1!1")
(("" (replace -2)
(("" (rewrite "lr_coset_assoc" 1 :dir rl)
(("" (replace -3)
(("" (replace -4)
(("" (rewrite "lr_coset_assoc")
(("" (replace -4)
(("" (rewrite "left_coset_assoc") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((left_coset_assoc formula-decl nil cosets 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 nil)
(group nonempty-type-eq-decl nil group nil)
(normal_subgroup? const-decl "boolean" normal_subgroups nil)
(normal_subgroup type-eq-decl nil normal_subgroups nil)
(T formal-nonempty-type-decl nil factor_groups nil)
(* formal-const-decl "[T, T -> T]" factor_groups nil)
(one formal-const-decl "T" factor_groups nil)
(lr_coset_assoc formula-decl nil cosets nil)
(normal_left_is_right formula-decl nil normal_subgroups nil))
shostak))
(mult_prep 0
(mult_prep-1 nil 3405947871
("" (skosimp*)
(("" (lemma "is_singleton[set[T]]")
(("" (inst?)
(("" (assert)
(("" (hide 2)
(("" (prop)
(("1" (rewrite "p0") nil nil)
("2" (skosimp*)
(("2" (replace -3)
(("2" (hide -3)
(("2" (replace -5)
(("2" (hide -5)
(("2" (lemma "prep")
(("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-nonempty-type-decl nil factor_groups nil)
(is_singleton formula-decl nil sets nil)
(p0 formula-decl nil factor_groups nil)
(prep formula-decl nil factor_groups nil)
(left_cosets type-eq-decl nil cosets nil)
(normal_subgroup type-eq-decl nil normal_subgroups nil)
(normal_subgroup? const-decl "boolean" normal_subgroups nil)
(* const-decl "set[T]" cosets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(group nonempty-type-eq-decl nil group nil)
(group? const-decl "bool" group_def nil)
(one formal-const-decl "T" factor_groups nil)
(* formal-const-decl "[T, T -> T]" factor_groups nil))
shostak))
(mult_TCC1 0
(mult_TCC1-1 nil 3405871870
("" (skosimp*)
(("" (typepred "H!1")
(("" (assert)
(("" (expand "normal_subgroup?") (("" (propax) 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" factor_groups nil)
(* formal-const-decl "[T, T -> T]" factor_groups nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil factor_groups nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(mult_TCC2 0
(mult_TCC2-1 nil 3405954319
("" (skosimp*)
((""
(inst + "lc_gen[T, *, one](G!1, H!1, A!1) *
lc_gen[T, *, one](G!1, H!1, B!1)")
(("1" (rewrite "star_closed") nil nil)
("2" (assert)
(("2" (typepred "H!1")
(("2" (expand "normal_subgroup?") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
((T formal-nonempty-type-decl nil factor_groups 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]" factor_groups nil)
(one formal-const-decl "T" factor_groups nil)
(group? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil)
(subgroup type-eq-decl nil group nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(* const-decl "set[T]" cosets nil)
(subgroup? const-decl "bool" group_def nil)
(left_cosets type-eq-decl nil cosets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(lc_gen const-decl "{a: T | G(a) AND lc = a * H}" cosets nil)
(normal_subgroup? const-decl "boolean" normal_subgroups nil)
(normal_subgroup type-eq-decl nil normal_subgroups nil)
(H!1 skolem-const-decl "normal_subgroup[T, *, one](G!1)"
factor_groups nil)
(G!1 skolem-const-decl "group[T, *, one]" factor_groups nil)
(B!1 skolem-const-decl "left_cosets[T, *, one](G!1, H!1)"
factor_groups nil)
(A!1 skolem-const-decl "left_cosets[T, *, one](G!1, H!1)"
factor_groups nil)
(star_closed formula-decl nil groupoid nil)
(star_closed? const-decl "bool" groupoid_def nil)
(groupoid nonempty-type-eq-decl nil groupoid nil)
(NOT const-decl "[bool -> bool]" booleans nil))
nil))
(mult_lem_TCC1 0
(mult_lem_TCC1-1 nil 3405955207
("" (skosimp*) (("" (inst + "a!1") nil nil)) nil)
((T formal-nonempty-type-decl nil factor_groups 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]" factor_groups nil)
(one formal-const-decl "T" factor_groups nil)
(group? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil))
nil))
(mult_lem_TCC2 0
(mult_lem_TCC2-1 nil 3405955207
("" (skosimp*) (("" (inst + "b!1") nil nil)) nil)
((T formal-nonempty-type-decl nil factor_groups 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]" factor_groups nil)
(one formal-const-decl "T" factor_groups nil)
(group? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil))
nil))
(mult_lem 0
(mult_lem-3 nil 3406564417
("" (skosimp*)
(("" (expand "mult")
(("" (name "aa" "lc_gen(G!1, H!1, a!1 * H!1)")
(("" (replace -1)
(("" (name "bb" "lc_gen(G!1, H!1, b!1 * H!1)")
(("" (replace -1)
(("" (lemma "lc_is_eq")
(("" (inst - "G!1" "H!1" "aa*bb" "a!1*b!1")
(("" (typepred "H!1")
(("" (expand "normal_subgroup?")
(("" (flatten)
(("" (assert)
(("" (hide 2)
(("" (lemma "lc_gen_normal")
((""
(inst?)
((""
(assert)
((""
(skosimp*)
((""
(replace -1)
((""
(hide -1)
((""
(lemma "lc_gen_normal")
((""
(inst?)
((""
(assert)
((""
(skosimp*)
((""
(replace -1)
((""
(hide -1)
((""
(replace
-4
:dir
rl)
((""
(hide -4)
((""
(replace
-4
:dir
rl)
((""
(hide -4)
((""
(inst
+
"inv(b!1)*inv(a!1)*h!2*a!1*h!1*b!1")
(("1"
(rewrite
"assoc")
(("1"
(rewrite
"assoc")
(("1"
(rewrite
"assoc")
(("1"
(rewrite
"assoc")
(("1"
(rewrite
"assoc")
(("1"
(rewrite
"assoc")
(("1"
(case-replace
"(a!1 * b!1 * inv(b!1)) = a!1")
(("1"
(rewrite
"inv_right")
(("1"
(rewrite
"one_left")
nil
nil))
nil)
("2"
(assert)
(("2"
(hide
2)
(("2"
(rewrite
"associative")
(("2"
(rewrite
"inv_right")
(("2"
(assert)
(("2"
(rewrite
"one_right")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"nsg_prop2")
(("2"
(inst
-
"a!1"
"h!2"
"G!1"
"H!1")
(("2"
(assert)
(("2"
(name
"HH"
"inv(a!1) * h!2 * a!1")
(("2"
(case-replace
"inv[T, *, one](b!1) * inv[T, *, one](a!1) * h!2 * a!1 *
h!1
* b!1 = inv[T, *, one](b!1) * HH *
h!1
* b!1")
(("1"
(hide
-1)
(("1"
(lemma
"nsg_prop2")
(("1"
(inst
-
"b!1"
"HH*h!1"
"G!1"
"H!1")
(("1"
(assert)
(("1"
(split
-1)
(("1"
(assert)
(("1"
(rewrite
"assoc")
nil
nil))
nil)
("2"
(hide
2)
(("2"
(rewrite
"star_closed")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
2)
(("2"
(rewrite
"associative")
(("2"
(rewrite
"associative")
(("2"
(replace
-1)
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((mult const-decl "left_cosets(G, H)" factor_groups nil)
(lc_gen_normal formula-decl nil normal_subgroups nil)
(G!1 skolem-const-decl "group[T, *, one]" factor_groups nil)
(H!1 skolem-const-decl "normal_subgroup[T, *, one](G!1)"
factor_groups nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(b!1 skolem-const-decl "(G!1)" factor_groups nil)
(a!1 skolem-const-decl "(G!1)" factor_groups nil)
(h!2 skolem-const-decl "(H!1)" factor_groups nil)
(h!1 skolem-const-decl "(H!1)" factor_groups nil)
(right_identity formula-decl nil monad nil)
(associative formula-decl nil semigroup nil)
(inv_right formula-decl nil group nil)
(one_left formula-decl nil group nil)
(assoc formula-decl nil group nil)
(groupoid nonempty-type-eq-decl nil groupoid nil)
(star_closed? const-decl "bool" groupoid_def nil)
(star_closed formula-decl nil groupoid nil)
(nsg_prop2 formula-decl nil normal_subgroups nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(lc_is_eq formula-decl nil cosets nil)
(T formal-nonempty-type-decl nil factor_groups nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(* formal-const-decl "[T, T -> T]" factor_groups nil)
(one formal-const-decl "T" factor_groups nil)
(group nonempty-type-eq-decl nil group nil)
(subgroup type-eq-decl nil group nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(group? const-decl "bool" group_def nil)
(* const-decl "set[T]" cosets nil)
(subgroup? const-decl "bool" group_def nil)
(left_cosets type-eq-decl nil cosets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(lc_gen const-decl "{a: T | G(a) AND lc = a * H}" cosets nil)
(normal_subgroup? const-decl "boolean" normal_subgroups nil)
(normal_subgroup type-eq-decl nil normal_subgroups nil))
nil)
(mult_lem-2 nil 3406552141
("" (skosimp*)
(("" (expand "mult")
(("" (name "aa" "lc_gen(G!1, H!1, a!1 * H!1)")
(("" (replace -1)
(("" (name "bb" "lc_gen(G!1, H!1, b!1 * H!1)")
(("" (replace -1)
(("" (lemma "lc_is_eq")
(("" (inst - "G!1" "H!1" "aa*bb" "a!1*b!1")
(("" (typepred "H!1")
(("" (expand "normal_subgroup?")
(("" (flatten)
(("" (assert)
(("" (rewrite "star_closed")
(("" (rewrite "star_closed")
((""
(hide 2)
((""
(lemma "lc_gen_lem")
((""
(inst?)
((""
(assert)
((""
(skosimp*)
((""
(replace -1)
((""
(hide -1)
((""
(lemma "lc_gen_lem")
((""
(inst?)
((""
(assert)
((""
(skosimp*)
((""
(replace -1)
((""
(hide -1)
((""
(replace
-4
:dir
rl)
((""
(hide -4)
((""
(replace
-4
:dir
rl)
((""
(hide
-4)
((""
(inst
+
"inv(b!1)*inv(a!1)*h!2*a!1*h!1*b!1")
(("1"
(rewrite
"assoc")
(("1"
(rewrite
"assoc")
(("1"
(rewrite
"assoc")
(("1"
(rewrite
"assoc")
(("1"
(rewrite
"assoc")
(("1"
(rewrite
"assoc")
(("1"
(case-replace
"(a!1 * b!1 * inv(b!1)) = a!1")
(("1"
(rewrite
"inv_right")
(("1"
(rewrite
"one_left")
nil
nil))
nil)
("2"
(assert)
(("2"
(hide
2)
(("2"
(rewrite
"associative")
(("2"
(rewrite
"inv_right")
(("2"
(assert)
(("2"
(rewrite
"one_right")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"nsg_prop2")
(("2"
(inst
-
"a!1"
"h!2"
"G!1"
"H!1")
(("2"
(assert)
(("2"
(name
"HH"
"inv(a!1) * h!2 * a!1")
(("2"
(case-replace
"inv[T, *, one](b!1) * inv[T, *, one](a!1) * h!2 * a!1 *
h!1
* b!1 = inv[T, *, one](b!1) * HH *
h!1
* b!1")
(("1"
(hide
-1)
(("1"
(lemma
"nsg_prop2")
(("1"
(inst
-
"b!1"
"HH*h!1"
"G!1"
"H!1")
(("1"
(assert)
(("1"
(split
-1)
(("1"
(assert)
(("1"
(rewrite
"assoc")
nil
nil))
nil)
("2"
(hide
2)
(("2"
(rewrite
"star_closed")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
2)
(("2"
(rewrite
"associative")
(("2"
(rewrite
"associative")
(("2"
(replace
-1)
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((associative formula-decl nil semigroup nil)
(one_right formula-decl nil group nil)
(inv_right formula-decl nil group nil)
(one_left formula-decl nil group nil)
(assoc formula-decl nil group nil)
(groupoid nonempty-type-eq-decl nil groupoid nil)
(star_closed formula-decl nil groupoid nil)
(group nonempty-type-eq-decl nil group nil)
(subgroup type-eq-decl nil group nil)
(group? const-decl "bool" group_def nil)
(subgroup? const-decl "bool" group_def nil)
(left_cosets type-eq-decl nil cosets nil)
(lc_gen const-decl "{a: T | G(a) AND lc = a * H}" cosets nil)
(normal_subgroup? const-decl "boolean" normal_subgroups nil)
(normal_subgroup type-eq-decl nil normal_subgroups nil))
nil)
(mult_lem-1 nil 3405955211
("" (skosimp*)
(("" (expand "mult")
(("" (apply-extensionality 1 :hide? t)
(("" (iff 1)
(("" (name "A" "lc_gen(G!1, H!1, a!1 * H!1)")
(("" (replace -1)
(("" (name "B" "lc_gen(G!1, H!1, b!1 * H!1)")
(("" (replace -1)
(("" (rewrite "left_coset_assoc" :dir rl)
(("" (rewrite "left_coset_assoc" :dir rl)
(("" (expand "*" 1)
(("" (prop)
(("1" (skosimp*)
(("1" (replace -1)
(("1" (postpone) nil nil)) nil))
nil)
("2" (postpone) nil nil))
nil))
nil))
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)
(normal_subgroup? const-decl "boolean" normal_subgroups nil)
(normal_subgroup type-eq-decl nil normal_subgroups nil))
shostak))
(mult_in 0
(mult_in-1 nil 3405963548
("" (skosimp*)
(("" (typepred "B!1")
(("" (typepred "A!1")
(("" (skosimp*)
(("" (replace -1)
(("" (hide -1)
(("" (replace -1)
(("" (hide -1)
(("" (lemma "mult_lem")
(("" (inst?)
(("" (assert)
(("" (expand "restrict")
(("" (replace -1)
(("" (hide -1)
((""
(assert)
((""
(expand "*")
((""
(skosimp*)
((""
(typepred "a!2")
((""
(typepred "a!3")
((""
(typepred "h!1")
((""
(typepred "H!1")
((""
(expand
"normal_subgroup?")
((""
(flatten)
((""
(expand "subgroup?")
((""
(hide -3)
((""
(expand
"subset?")
((""
(assert)
((""
(inst
-
"h!1")
((""
(assert)
((""
(lemma
"star_closed")
((""
(inst?)
((""
(name-replace
"A23"
"a!2 * a!3")
((""
(hide
-2
-3
-4)
((""
(lemma
"star_closed")
((""
(inst
-
"G!1"
"A23"
"h!1")
((""
(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))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((left_cosets type-eq-decl nil cosets nil)
(normal_subgroup type-eq-decl nil normal_subgroups nil)
(normal_subgroup? const-decl "boolean" normal_subgroups nil)
(* const-decl "set[T]" cosets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(group nonempty-type-eq-decl nil group nil)
(group? const-decl "bool" group_def nil)
(one formal-const-decl "T" factor_groups nil)
(* formal-const-decl "[T, T -> T]" factor_groups nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil factor_groups nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(subgroup? const-decl "bool" group_def nil)
(subset? const-decl "bool" sets nil)
(star_closed formula-decl nil groupoid nil)
(A23 skolem-const-decl "T" factor_groups nil)
(G!1 skolem-const-decl "group[T, *, one]" factor_groups nil)
(star_closed? const-decl "bool" groupoid_def nil)
(groupoid nonempty-type-eq-decl nil groupoid nil)
(member const-decl "bool" sets nil)
(mult_lem formula-decl nil factor_groups nil))
shostak))
(mult_is_coset 0
(mult_is_coset-1 nil 3405963272
("" (skosimp*)
(("" (expand "restrict")
(("" (typepred "B!1")
(("" (typepred "A!1")
(("" (skosimp*)
(("" (replace -1)
(("" (hide -1)
(("" (replace -1)
(("" (hide -1)
(("" (inst + "a!1*a!2")
(("1" (lemma "mult_lem")
(("1" (inst?)
(("1" (expand "restrict")
(("1" (propax) nil nil)) nil))
nil))
nil)
("2" (typepred "a!1")
(("2" (typepred "a!2")
(("2" (assert)
(("2" (lemma "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)
((left_cosets type-eq-decl nil cosets nil)
(normal_subgroup type-eq-decl nil normal_subgroups nil)
(normal_subgroup? const-decl "boolean" normal_subgroups nil)
(* const-decl "set[T]" cosets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(group nonempty-type-eq-decl nil group nil)
(group? const-decl "bool" group_def nil)
(one formal-const-decl "T" factor_groups nil)
(* formal-const-decl "[T, T -> T]" factor_groups nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil factor_groups nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(groupoid nonempty-type-eq-decl nil groupoid nil)
(star_closed? const-decl "bool" groupoid_def nil)
(member const-decl "bool" sets nil)
(closed formula-decl nil groupoid nil)
(mult_lem formula-decl nil factor_groups nil)
(a!2 skolem-const-decl "(G!1)" factor_groups nil)
(a!1 skolem-const-decl "(G!1)" factor_groups nil)
(G!1 skolem-const-decl "group[T, *, one]" factor_groups nil))
shostak))
(N_is_identity_TCC1 0
(N_is_identity_TCC1-1 nil 3405964115
("" (skosimp*)
(("" (inst + "one")
(("1" (assert)
(("1" (apply-extensionality 1 :hide? t)
(("1" (expand "*")
(("1" (iff 1)
(("1" (prop)
(("1" (inst + "x!1")
(("1" (rewrite "left_identity") nil nil)) nil)
("2" (skosimp*)
(("2" (replace -1)
(("2" (rewrite "left_identity")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "one_in") nil nil))
nil))
nil)
((G!1 skolem-const-decl "group[T, *, one]" factor_groups nil)
(group nonempty-type-eq-decl nil group nil)
(group? const-decl "bool" group_def nil)
(one formal-const-decl "T" factor_groups nil)
(* formal-const-decl "[T, T -> T]" factor_groups nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-nonempty-type-decl nil factor_groups nil)
(* const-decl "set[T]" cosets nil)
(normal_subgroup type-eq-decl nil normal_subgroups nil)
(normal_subgroup? const-decl "boolean" normal_subgroups nil)
(x!1 skolem-const-decl "T" factor_groups nil)
(N!1 skolem-const-decl "normal_subgroup[T, *, one](G!1)"
factor_groups nil)
(left_identity formula-decl nil monad nil)
(monad nonempty-type-eq-decl nil monad nil)
(monad? const-decl "bool" monad_def nil)
(one_in formula-decl nil monad nil))
nil))
(N_is_identity 0
(N_is_identity-1 nil 3405964913
("" (skosimp*)
(("" (expand "restrict")
(("" (prop)
(("1" (apply-extensionality 1 :hide? t)
(("1" (typepred "N!1")
(("1"
(case-replace
"mult(G!1, N!1)(N!1, A!1)(x!1) = mult(G!1, N!1)(one*N!1, A!1)(x!1)")
(("1" (hide -1)
(("1" (typepred "A!1")
(("1" (skosimp*)
(("1" (replace -1)
(("1" (hide -1)
(("1" (lemma "mult_lem")
(("1" (inst?)
(("1" (replace -1)
(("1"
(hide -1)
(("1"
(expand "restrict")
(("1"
(rewrite "left_identity")
nil
nil))
nil))
nil))
nil)
("2" (rewrite "one_in") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (lemma "left_coset_one")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil)
("3" (hide 2)
(("3" (inst + "one") (("3" (rewrite "one_in") nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (apply-extensionality 1 :hide? t)
(("2"
(case-replace
"mult(G!1, N!1)(A!1,N!1)(x!1) = mult(G!1, N!1)(A!1,one*N!1)(x!1)")
(("1" (hide -1)
(("1" (typepred "A!1")
(("1" (skosimp*)
(("1" (replace -1)
(("1" (hide -1)
(("1" (lemma "mult_lem")
(("1" (inst?)
(("1" (replace -1)
(("1" (hide -1)
(("1"
(expand "restrict")
(("1"
(rewrite "right_identity")
nil
nil))
nil))
nil))
nil)
("2" (rewrite "one_in") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (lemma "left_coset_one")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil)
("3" (hide 2)
(("3" (inst + "one") (("3" (rewrite "one_in") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((NOT const-decl "[bool -> bool]" booleans nil)
(left_coset_one formula-decl nil cosets nil)
(G!1 skolem-const-decl "group[T, *, one]" factor_groups nil)
(left_identity formula-decl nil monad nil)
(one_in formula-decl nil monad nil)
(monad? const-decl "bool" monad_def nil)
(monad nonempty-type-eq-decl nil monad nil)
(mult_lem formula-decl nil factor_groups nil)
(* formal-const-decl "[T, T -> T]" factor_groups nil)
(one formal-const-decl "T" factor_groups nil)
(group nonempty-type-eq-decl nil group nil)
(group? const-decl "bool" group_def nil)
(normal_subgroup? const-decl "boolean" normal_subgroups nil)
(normal_subgroup type-eq-decl nil normal_subgroups nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(* const-decl "set[T]" cosets nil)
(left_cosets type-eq-decl nil cosets nil)
(mult const-decl "left_cosets(G, H)" factor_groups nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-nonempty-type-decl nil factor_groups nil)
(right_identity formula-decl nil monad nil))
shostak))
(left_cosets_group_TCC1 0
(left_cosets_group_TCC1-1 nil 3406297184
("" (skosimp*)
(("" (inst + "one")
(("1" (apply-extensionality 1 :hide? t)
(("1" (expand "*")
(("1" (iff 1)
(("1" (ground)
(("1" (inst?) (("1" (rewrite "one_left") nil nil)) nil)
("2" (skosimp*)
(("2" (replace -1)
(("2" (hide -1)
(("2" (rewrite "one_left") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "one_in") nil nil))
nil))
nil)
((G!1 skolem-const-decl "group[T, *, one]" factor_groups nil)
(group nonempty-type-eq-decl nil group nil)
(group? const-decl "bool" group_def nil)
(one formal-const-decl "T" factor_groups nil)
(* formal-const-decl "[T, T -> T]" factor_groups nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-nonempty-type-decl nil factor_groups nil)
(left_identity formula-decl nil monad nil)
(normal_subgroup? const-decl "boolean" normal_subgroups nil)
(normal_subgroup type-eq-decl nil normal_subgroups nil)
(* const-decl "set[T]" cosets nil)
(monad nonempty-type-eq-decl nil monad nil)
(monad? const-decl "bool" monad_def nil)
(one_in formula-decl nil monad nil))
nil))
(left_cosets_group_TCC2 0
(left_cosets_group_TCC2-1 nil 3406297184
("" (skosimp*)
(("" (inst + "N!1")
(("" (inst + "one")
(("1" (apply-extensionality 1 :hide? t)
(("1" (iff 1)
(("1" (ground)
(("1" (expand "*")
(("1" (inst?) (("1" (rewrite "one_left") nil nil))
nil))
nil)
("2" (expand "*")
(("2" (skosimp*)
(("2" (replace -1)
(("2" (hide -1)
(("2" (rewrite "one_left")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "fullset_is_group") (("2" (propax) nil nil))
nil))
nil)
("2" (rewrite "one_in") nil nil))
nil))
nil))
nil)
((T formal-nonempty-type-decl nil factor_groups 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]" factor_groups nil)
(one formal-const-decl "T" factor_groups nil)
(group? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(* const-decl "set[T]" cosets nil)
(normal_subgroup? const-decl "boolean" normal_subgroups nil)
(normal_subgroup type-eq-decl nil normal_subgroups nil)
(left_cosets type-eq-decl nil cosets nil)
(N!1 skolem-const-decl "normal_subgroup[T, *, one](G!1)"
factor_groups nil)
(G!1 skolem-const-decl "group[T, *, one]" factor_groups nil)
(monad nonempty-type-eq-decl nil monad nil)
(monad? const-decl "bool" monad_def nil)
(one_in formula-decl nil monad nil)
(one_left formula-decl nil group nil))
nil))
(left_cosets_group 0
(left_cosets_group-1 nil 3406303072
("" (skosimp*)
(("" (expand "group?")
(("" (prop)
(("1" (expand "monoid?")
(("1" (prop)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.46 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.
|
