|
(normalizer_centralizer
(IMP_normal_subgroups_TCC1 0
(IMP_normal_subgroups_TCC1-1 nil 3530611414
("" (rewrite "fullset_is_group") nil nil)
((fullset_is_group formula-decl nil normalizer_centralizer nil))
nil))
(normalizer_TCC1 0
(normalizer_TCC1-1 nil 3530280384 ("" (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)
(T formal-type-decl nil normalizer_centralizer nil)
(set type-eq-decl nil sets nil)
(* formal-const-decl "[T, T -> T]" normalizer_centralizer nil)
(one formal-const-decl "T" normalizer_centralizer nil)
(group? const-decl "bool" group_def "algebra/")
(group nonempty-type-eq-decl nil group "algebra/")
(subgroup? const-decl "bool" group_def "algebra/")
(subgroup type-eq-decl nil group "algebra/")
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(inv_exists? const-decl "bool" group_def "algebra/")
(monoid? const-decl "bool" monoid_def "algebra/")
(associative? const-decl "bool" operator_defs nil)
(monad? const-decl "bool" monad_def "algebra/")
(identity? const-decl "bool" operator_defs nil)
(left_identity formula-decl nil monad "algebra/")
(restrict const-decl "R" restrict nil)
(right_identity formula-decl nil monad "algebra/")
(one_member formula-decl nil monad "algebra/")
(star_closed? const-decl "bool" groupoid_def "algebra/")
(G!1 skolem-const-decl "group[T, *, one]" normalizer_centralizer
nil)
(extend const-decl "R" extend nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil))
nil))
(centralizer_TCC1 0
(centralizer_TCC1-1 nil 3530280384 ("" (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)
(T formal-type-decl nil normalizer_centralizer nil)
(set type-eq-decl nil sets nil)
(* formal-const-decl "[T, T -> T]" normalizer_centralizer nil)
(one formal-const-decl "T" normalizer_centralizer nil)
(group? const-decl "bool" group_def "algebra/")
(group nonempty-type-eq-decl nil group "algebra/")
(inv_exists? const-decl "bool" group_def "algebra/")
(monoid? const-decl "bool" monoid_def "algebra/")
(associative? const-decl "bool" operator_defs nil)
(monad? const-decl "bool" monad_def "algebra/")
(identity? const-decl "bool" operator_defs nil)
(left_identity formula-decl nil monad "algebra/")
(restrict const-decl "R" restrict nil)
(right_identity formula-decl nil monad "algebra/")
(one_member formula-decl nil monad "algebra/")
(star_closed? const-decl "bool" groupoid_def "algebra/")
(G!1 skolem-const-decl "group[T, *, one]" normalizer_centralizer
nil)
(extend const-decl "R" extend nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil))
nil))
(a_by_c_TCC1 0
(a_by_c_TCC1-1 nil 3530280384
("" (skosimp*)
(("" (typepred "h!1")
(("" (typepred "H!1")
(("" (hide -1)
(("" (expand "subgroup?")
(("" (expand* "subset?" "member")
(("" (inst -1 "h!1")
(("" (assert)
(("" (hide -2)
(("" (rewrite "product_in")
(("1" (rewrite "product_in") nil nil)
("2" (rewrite "inv_in") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((subgroup type-eq-decl nil group "algebra/")
(subgroup? const-decl "bool" group_def "algebra/")
(group nonempty-type-eq-decl nil group "algebra/")
(group? const-decl "bool" group_def "algebra/")
(one formal-const-decl "T" normalizer_centralizer nil)
(* formal-const-decl "[T, T -> T]" normalizer_centralizer nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil normalizer_centralizer nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(product_in formula-decl nil group "algebra/")
(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
"algebra/")
(inv_in formula-decl nil group "algebra/"))
nil))
(CL_TCC1 0
(CL_TCC1-1 nil 3530354396 ("" (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)
(T formal-type-decl nil normalizer_centralizer nil)
(set type-eq-decl nil sets nil)
(* formal-const-decl "[T, T -> T]" normalizer_centralizer nil)
(one formal-const-decl "T" normalizer_centralizer nil)
(group? const-decl "bool" group_def "algebra/")
(group nonempty-type-eq-decl nil group "algebra/")
(inv_exists? const-decl "bool" group_def "algebra/")
(monoid? const-decl "bool" monoid_def "algebra/")
(associative? const-decl "bool" operator_defs nil)
(monad? const-decl "bool" monad_def "algebra/")
(identity? const-decl "bool" operator_defs nil)
(left_identity formula-decl nil monad "algebra/")
(restrict const-decl "R" restrict nil)
(right_identity formula-decl nil monad "algebra/")
(one_member formula-decl nil monad "algebra/")
(star_closed? const-decl "bool" groupoid_def "algebra/")
(G!1 skolem-const-decl "group[T, *, one]" normalizer_centralizer
nil)
(extend const-decl "R" extend nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil))
nil))
(normalizer_is_subgroup 0
(normalizer_is_subgroup-1 nil 3530280992
("" (skosimp*)
(("" (lemma "subgroup_def")
(("" (inst -1 "G!1" "normalizer(G!1,H!1)")
(("" (assert)
(("" (hide 2)
(("" (prop)
(("1" (expand "nonempty?")
(("1" (expand "empty?")
(("1" (expand "member")
(("1" (inst - "one")
(("1" (expand "normalizer")
(("1" (expand "extend")
(("1" (ground)
(("1" (rewrite "left_coset_one")
(("1"
(rewrite "right_coset_one")
nil
nil))
nil)
("2" (rewrite "one_in") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "star_closed?")
(("2" (expand "member")
(("2" (skosimp*)
(("2" (typepred "x!1" "y!1")
(("2" (expand "normalizer")
(("2" (expand "extend")
(("2" (ground)
(("1" (rewrite "inv_star")
(("1"
(hide (-1 -2 -4 -6))
(("1"
(rewrite "right_coset_assoc" :dir rl)
(("1"
(rewrite
"left_coset_assoc"
:dir
rl)
(("1"
(rewrite "lr_coset_assoc")
(("1"
(replace -2 1)
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide (-2 -4 -5))
(("2" (rewrite "product_in") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "inv_closed?")
(("3" (skosimp*)
(("3" (expand "member")
(("3" (typepred "x!1")
(("3" (expand "normalizer")
(("3" (expand "extend")
(("3" (ground)
(("1" (replace -3 1 rl)
(("1"
(rewrite "lr_coset_assoc")
(("1"
(rewrite "lr_coset_assoc")
(("1"
(rewrite "lr_coset_assoc")
(("1"
(rewrite "right_coset_assoc")
(("1"
(rewrite "right_coset_one")
(("1"
(rewrite "left_coset_assoc")
(("1"
(rewrite "left_coset_one")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide (-2 -3))
(("2" (rewrite "inv_in") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((one formal-const-decl "T" normalizer_centralizer nil)
(* formal-const-decl "[T, T -> T]" normalizer_centralizer nil)
(T formal-type-decl nil normalizer_centralizer 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)
(extend const-decl "R" extend nil)
(monad nonempty-type-eq-decl nil monad "algebra/")
(monad? const-decl "bool" monad_def "algebra/")
(one_in formula-decl nil monad "algebra/")
(left_coset_one formula-decl nil cosets "algebra/")
(right_coset_one formula-decl nil cosets "algebra/")
(inv_one formula-decl nil group "algebra/")
(member const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(product_in formula-decl nil group "algebra/")
(inv_star formula-decl nil group "algebra/")
(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)
(* const-decl "set[T]" cosets "algebra/")
(right_coset_assoc formula-decl nil cosets "algebra/")
(lr_coset_assoc formula-decl nil cosets "algebra/")
(left_coset_assoc formula-decl nil cosets "algebra/")
(star_closed? const-decl "bool" groupoid_def "algebra/")
(inv_in formula-decl nil group "algebra/")
(* const-decl "set[T]" cosets "algebra/")
(inv_right formula-decl nil group "algebra/")
(inv_inv formula-decl nil group "algebra/")
(inv_closed? const-decl "bool" group "algebra/")
(normalizer const-decl "{S: set[T] | subset?(S, G)}"
normalizer_centralizer nil)
(subset? const-decl "bool" sets nil)
(subgroup type-eq-decl nil group "algebra/")
(subgroup? const-decl "bool" group_def "algebra/")
(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))
(subset_of_normalizer 0
(subset_of_normalizer-1 nil 3530281053
("" (skosimp*)
(("" (copy -1)
(("" (expand "subgroup?" -1)
(("" (expand* "subset?" "member")
(("" (skosimp)
(("" (inst?)
(("" (assert)
(("" (expand "normalizer")
(("" (expand "extend")
(("" (lemma "lc_is_eq")
(("" (inst -1 "G!1" "H!1" "inv(x!1)" "one")
(("" (assert)
(("" (prop)
(("1" (rewrite "left_coset_one")
(("1"
(replaces -1)
(("1"
(lemma "rc_is_eq")
(("1"
(inst -1 "G!1" "H!1" "x!1" "one")
(("1"
(assert)
(("1"
(prop)
(("1"
(rewrite "right_coset_one")
nil
nil)
("2"
(hide (-1 -2 2))
(("2" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide (-1 -2 2))
(("2"
(inst 1 "inv(x!1)")
(("2"
(lemma "inv_in")
(("2" (inst -1 "H!1" "x!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(T formal-type-decl nil normalizer_centralizer nil)
(normalizer const-decl "{S: set[T] | subset?(S, G)}"
normalizer_centralizer nil)
(lc_is_eq formula-decl nil cosets "algebra/")
(* formal-const-decl "[T, T -> T]" normalizer_centralizer nil)
(one formal-const-decl "T" normalizer_centralizer nil)
(left_identity formula-decl nil monad "algebra/")
(inv_in formula-decl nil group "algebra/")
(x!1 skolem-const-decl "T" normalizer_centralizer nil)
(H!1 skolem-const-decl "group[T, *, one]" normalizer_centralizer
nil)
(left_coset_one formula-decl nil cosets "algebra/")
(rc_is_eq formula-decl nil cosets "algebra/")
(right_identity formula-decl nil monad "algebra/")
(right_coset_one formula-decl nil cosets "algebra/")
(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)
(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)
(extend const-decl "R" extend nil)
(subgroup? const-decl "bool" group_def "algebra/"))
shostak))
(normal_in_normalizer_TCC1 0
(normal_in_normalizer_TCC1-1 nil 3530280384
("" (skosimp)
(("" (lemma "normalizer_is_subgroup")
(("" (inst?)
(("" (assert)
(("" (expand "subgroup?") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((normalizer_is_subgroup formula-decl nil normalizer_centralizer
nil)
(subgroup? const-decl "bool" group_def "algebra/")
(group nonempty-type-eq-decl nil group "algebra/")
(group? const-decl "bool" group_def "algebra/")
(one formal-const-decl "T" normalizer_centralizer nil)
(* formal-const-decl "[T, T -> T]" normalizer_centralizer 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-type-decl nil normalizer_centralizer nil))
nil))
(normal_in_normalizer 0
(normal_in_normalizer-1 nil 3530281087
("" (skosimp)
(("" (expand "normal_subgroup?")
(("" (prop)
(("1" (expand "subgroup?" 1)
(("1" (rewrite "subset_of_normalizer") nil nil)) nil)
("2" (skosimp)
(("2" (typepred "a!1")
(("2" (expand "normalizer")
(("2" (expand "extend")
(("2" (ground)
(("2" (decompose-equality -2)
(("2" (expand* "subset?" "member")
(("2" (skosimp)
(("2" (inst?)
(("2" (iff) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((normal_subgroup? const-decl "boolean" normal_subgroups "algebra/")
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(member const-decl "bool" sets nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group
"algebra/")
(AND const-decl "[bool, bool -> bool]" booleans nil)
(* const-decl "set[T]" cosets "algebra/")
(* const-decl "set[T]" cosets "algebra/")
(= const-decl "[T, T -> boolean]" equalities nil)
(extend const-decl "R" extend nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(subgroup type-eq-decl nil group "algebra/")
(subset? const-decl "bool" sets nil)
(normalizer const-decl "{S: set[T] | subset?(S, G)}"
normalizer_centralizer nil)
(subgroup? const-decl "bool" group_def "algebra/")
(group nonempty-type-eq-decl nil group "algebra/")
(group? const-decl "bool" group_def "algebra/")
(one formal-const-decl "T" normalizer_centralizer nil)
(* formal-const-decl "[T, T -> T]" normalizer_centralizer 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-type-decl nil normalizer_centralizer nil)
(subset_of_normalizer formula-decl nil normalizer_centralizer nil))
shostak))
(centralizer_is_subgroup 0
(centralizer_is_subgroup-1 nil 3530281149
("" (skosimp*)
(("" (lemma "subgroup_def")
(("" (inst?)
(("" (assert)
(("" (hide 2)
(("" (prop)
(("1" (expand "nonempty?")
(("1" (expand "empty?")
(("1" (expand "member")
(("1" (inst - "one")
(("1" (grind) (("1" (rewrite "one_in") nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "centralizer")
(("2" (expand "star_closed?")
(("2" (expand "member")
(("2" (skosimp*)
(("2" (typepred "x!1" "y!1")
(("2" (expand "extend")
(("2" (ground)
(("1" (hide (-1 -2 -4))
(("1"
(rewrite "assoc" :dir rl)
(("1"
(replaces -1)
(("1"
(rewrite "assoc")
(("1"
(replaces -1)
(("1"
(rewrite "assoc" :dir rl)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide (-2 -4))
(("2" (rewrite "product_in") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "inv_closed?")
(("3" (skosimp*)
(("3" (expand "member")
(("3" (expand "centralizer")
(("3" (typepred "x!1")
(("3" (expand "centralizer")
(("3" (expand "extend")
(("3" (ground)
(("1"
(lemma "divby")
(("1"
(inst -1 "a!1 * x!1" "x!1" "a!1")
(("1"
(assert)
(("1"
(replace -1 1 rl)
(("1"
(rewrite "assoc" :dir rl)
(("1"
(rewrite "assoc" :dir rl)
(("1"
(replace -4 1 rl)
(("1"
(rewrite "assoc")
(("1"
(rewrite "assoc")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "inv_in") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((one formal-const-decl "T" normalizer_centralizer nil)
(* formal-const-decl "[T, T -> T]" normalizer_centralizer nil)
(T formal-type-decl nil normalizer_centralizer 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)
(monad nonempty-type-eq-decl nil monad "algebra/")
(monad? const-decl "bool" monad_def "algebra/")
(one_in formula-decl nil monad "algebra/")
(left_identity formula-decl nil monad "algebra/")
(right_identity formula-decl nil monad "algebra/")
(extend const-decl "R" extend nil)
(member const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil)
(star_closed? const-decl "bool" groupoid_def "algebra/")
(product_in formula-decl nil group "algebra/")
(assoc formula-decl nil group "algebra/")
(= const-decl "[T, T -> boolean]" equalities nil)
(FALSE const-decl "bool" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(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/")
(divby formula-decl nil group "algebra/")
(inv_in formula-decl nil group "algebra/")
(inv_closed? const-decl "bool" group "algebra/")
(centralizer const-decl "{S: set[T] | subset?(S, G)}"
normalizer_centralizer nil)
(subset? const-decl "bool" sets 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))
(singleton_iff_center 0
(singleton_iff_center-1 nil 3530375215
("" (skosimp*)
(("" (prop)
(("1" (expand* "member" "center")
(("1" (expand "extend" 1)
(("1" (skosimp)
(("1" (case "EXISTS (z:(G!1)): x!1 /= z * x!1 * inv(z)")
(("1" (skosimp)
(("1" (decompose-equality -1)
(("1" (inst -1 "z!1 * x!1 * inv(z!1)")
(("1" (iff)
(("1" (prop)
(("1" (expand "CL")
(("1" (expand "extend")
(("1" (prop)
(("1"
(expand "singleton")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (expand "extend")
(("2" (prop)
(("1" (expand "singleton")
(("1"
(expand "CL")
(("1"
(expand "extend")
(("1"
(assert)
(("1" (inst 2 "z!1") nil nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2"
(typepred "z!1" "x!1")
(("2"
(lemma "inv_in")
(("2"
(inst?)
(("2"
(rewrite "product_in")
(("2"
(rewrite "product_in")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst 1 "x!2")
(("2" (prop)
(("2" (hide -2)
(("2" (lemma "cancel_right_inv")
(("2"
(inst -1 "x!1" "x!2 * x!1 * inv(x!2)"
"inv(x!2)")
(("2" (prop)
(("2" (rewrite "inv_inv")
(("2" (rewrite "associative")
(("2"
(rewrite "associative")
(("2"
(rewrite "associative")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand* "member" "center")
(("2" (expand "extend")
(("2" (decompose-equality 1)
(("2" (iff)
(("2" (prop)
(("1" (expand "singleton")
(("1" (expand "CL")
(("1" (expand "extend")
(("1" (assert)
(("1" (skosimp)
(("1" (inst -3 "g!1")
(("1" (replaces -3)
(("1" (rewrite "associative") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "CL")
(("2" (expand "extend") (("2" (assert) nil nil))
nil))
nil)
("3" (expand "CL")
(("3" (expand "extend")
(("3" (assert)
(("3" (expand "singleton")
(("3" (inst 1 "one")
(("1" (rewrite "inv_one")
(("1" (rewrite "one_left")
(("1" (rewrite "one_right") nil nil))
nil))
nil)
("2" (rewrite "one_in") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((extend const-decl "R" extend 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)
(/= const-decl "boolean" notequal nil)
(group nonempty-type-eq-decl nil group "algebra/")
(group? const-decl "bool" group_def "algebra/")
(one formal-const-decl "T" normalizer_centralizer nil)
(* formal-const-decl "[T, T -> T]" normalizer_centralizer 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-type-decl nil normalizer_centralizer nil)
(subset? const-decl "bool" sets nil)
(CL const-decl "{X: set[T] | subset?(X, G)}" normalizer_centralizer
nil)
(FALSE const-decl "bool" booleans nil)
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" finite_sets_inductions "finite_sets/")
(finite_extend application-judgement "finite_set[T]"
extend_set_props nil)
(nonempty_extend application-judgement "(nonempty?[T])"
extend_set_props nil)
(inv_in formula-decl nil group "algebra/")
(product_in formula-decl nil group "algebra/")
(NOT const-decl "[bool -> bool]" booleans nil)
(cancel_right_inv formula-decl nil group "algebra/")
(associative formula-decl nil semigroup "algebra/")
(inv_left formula-decl nil group "algebra/")
(right_identity formula-decl nil monad "algebra/")
(inv_inv formula-decl nil group "algebra/")
(member const-decl "bool" sets nil)
(center const-decl "{s: set[T] | subset?(s, G)}" group "algebra/")
(G!1 skolem-const-decl "group[T, *, one]" normalizer_centralizer
nil)
(one_left formula-decl nil group "algebra/")
(one_right formula-decl nil group "algebra/")
(inv_one formula-decl nil group "algebra/")
(one_in formula-decl nil monad "algebra/")
(monad? const-decl "bool" monad_def "algebra/")
(monad nonempty-type-eq-decl nil monad "algebra/")
(inv_right formula-decl nil group "algebra/")
(IF const-decl "[boolean, T, T -> T]" if_def nil))
shostak))
(a_by_c_is_action 0
(a_by_c_is_action-1 nil 3530281222
("" (skosimp*)
(("" (expand "group_action?")
(("" (skosimp*)
(("" (prop)
(("1" (expand "a_by_c")
(("1" (rewrite "inv_one")
(("1" (rewrite "one_left")
(("1" (rewrite "one_right") nil nil)) nil))
nil))
nil)
("2" (expand "a_by_c")
(("2" (rewrite "inv_star")
(("2" (rewrite "assoc")
(("2" (rewrite "assoc")
(("2" (rewrite "assoc") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((group_action? const-decl "bool" group_action nil)
(inv_one formula-decl nil group "algebra/")
(T formal-type-decl nil normalizer_centralizer nil)
(* formal-const-decl "[T, T -> T]" normalizer_centralizer nil)
(one formal-const-decl "T" normalizer_centralizer nil)
(one_right formula-decl nil group "algebra/")
(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)
(one_left formula-decl nil group "algebra/")
(a_by_c const-decl "(G)" normalizer_centralizer nil)
(inv_star formula-decl nil group "algebra/")
(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)
(assoc formula-decl nil group "algebra/"))
shostak))
(Fix_is_center_TCC1 0
(Fix_is_center_TCC1-1 nil 3530280384 ("" (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)
(T formal-type-decl nil normalizer_centralizer nil)
(set type-eq-decl nil sets nil)
(* formal-const-decl "[T, T -> T]" normalizer_centralizer nil)
(one formal-const-decl "T" normalizer_centralizer nil)
(group? const-decl "bool" group_def "algebra/")
(group nonempty-type-eq-decl nil group "algebra/")
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(subgroup? const-decl "bool" group_def "algebra/"))
nil))
(Fix_is_center 0
(Fix_is_center-1 nil 3530281422
("" (skosimp*)
(("" (decompose-equality 1)
(("" (iff)
(("" (prop)
(("1" (expand* "Fix" "center")
(("1" (expand "extend")
(("1" (prop)
(("1" (expand "a_by_c")
(("1" (skosimp)
(("1" (inst?)
(("1" (hide (-1 -2 -4))
(("1" (name-replace "x!3" "x!2 * x!1" :hide? T)
(("1" (replace -1 1 rl)
(("1" (rewrite "assoc" :dir rl) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand* "Fix" "center")
(("2" (expand "extend")
(("2" (prop)
(("2" (expand "a_by_c")
(("2" (skosimp)
(("2" (inst?)
(("2" (hide (-1 -2 -4))
(("2" (replaces -1)
(("2" (rewrite "assoc" :dir rl) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((* formal-const-decl "[T, T -> T]" normalizer_centralizer nil)
(one formal-const-decl "T" normalizer_centralizer nil)
(group? const-decl "bool" group_def "algebra/")
(group nonempty-type-eq-decl nil group "algebra/")
(F type-eq-decl nil group_action nil)
(subset? const-decl "bool" sets nil)
(Fix const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil)
(subgroup? const-decl "bool" group_def "algebra/")
(subgroup type-eq-decl nil group "algebra/")
(a_by_c const-decl "(G)" normalizer_centralizer nil)
(center const-decl "{s: set[T] | subset?(s, G)}" group "algebra/")
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil normalizer_centralizer nil)
(extend const-decl "R" extend nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(inv_left formula-decl nil group "algebra/")
(right_identity formula-decl nil monad "algebra/")
(inv const-decl "{y | x * y = one AND y * x = one}" group
"algebra/")
(AND const-decl "[bool, bool -> bool]" booleans nil)
(assoc formula-decl nil group "algebra/")
(inv_right formula-decl nil group "algebra/"))
shostak))
(stabilizer_is_centralizer 0
(stabilizer_is_centralizer-1 nil 3530281854
("" (skosimp*)
(("" (decompose-equality 1)
(("" (iff)
(("" (prop)
(("1" (expand* "stabilizer" "centralizer")
(("1" (expand "extend")
(("1" (prop)
(("1" (expand "a_by_c")
(("1" (hide (-1 -2))
(("1" (name-replace "x!3" "x!2 * x!1" :hide? T)
(("1" (replace -1 1 rl)
(("1" (rewrite "assoc" :dir rl) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand* "stabilizer" "centralizer")
(("2" (expand "extend")
(("2" (prop)
(("2" (expand "a_by_c")
(("2" (hide (-1 -2))
(("2" (replaces -1)
(("2" (rewrite "assoc" :dir rl) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((* formal-const-decl "[T, T -> T]" normalizer_centralizer nil)
(one formal-const-decl "T" normalizer_centralizer nil)
(group? const-decl "bool" group_def "algebra/")
(group nonempty-type-eq-decl nil group "algebra/")
(F type-eq-decl nil group_action nil)
(subset? const-decl "bool" sets nil)
(stabilizer const-decl "{S: set[T] | subset?(S, G)}" group_action
nil)
(subgroup? const-decl "bool" group_def "algebra/")
(subgroup type-eq-decl nil group "algebra/")
(a_by_c const-decl "(G)" normalizer_centralizer nil)
(centralizer const-decl "{S: set[T] | subset?(S, G)}"
normalizer_centralizer 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-type-decl nil normalizer_centralizer nil)
(extend const-decl "R" extend nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(inv_left formula-decl nil group "algebra/")
(right_identity formula-decl nil monad "algebra/")
(inv const-decl "{y | x * y = one AND y * x = one}" group
"algebra/")
(AND const-decl "[bool, bool -> bool]" booleans nil)
(assoc formula-decl nil group "algebra/")
(inv_right formula-decl nil group "algebra/"))
shostak))
(orbit_is_CL 0
(orbit_is_CL-1 nil 3530363031
("" (skosimp*)
(("" (decompose-equality 1)
(("" (iff) (("" (expand* "orbit" "CL" "a_by_c") nil nil)) nil))
nil))
nil)
((* formal-const-decl "[T, T -> T]" normalizer_centralizer nil)
(one formal-const-decl "T" normalizer_centralizer nil)
(group? const-decl "bool" group_def "algebra/")
(group nonempty-type-eq-decl nil group "algebra/")
(F type-eq-decl nil group_action nil)
(subset? const-decl "bool" sets nil)
(orbit const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil)
(subgroup? const-decl "bool" group_def "algebra/")
(subgroup type-eq-decl nil group "algebra/")
(a_by_c const-decl "(G)" normalizer_centralizer nil)
(CL const-decl "{X: set[T] | subset?(X, G)}" normalizer_centralizer
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-type-decl nil normalizer_centralizer nil))
shostak))
(orbits_is_CLs 0
(orbits_is_CLs-1 nil 3530363118
("" (skosimp*)
(("" (decompose-equality 1)
(("" (iff)
(("" (expand* "orbits" "orbit" "CLs" "CL" "a_by_c" "extend")
nil nil))
nil))
nil))
nil)
((bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(* formal-const-decl "[T, T -> T]" normalizer_centralizer nil)
(one formal-const-decl "T" normalizer_centralizer nil)
(group? const-decl "bool" group_def "algebra/")
(group nonempty-type-eq-decl nil group "algebra/")
(F type-eq-decl nil group_action nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(orbits const-decl "setofsets[T1]" group_action nil)
(subgroup? const-decl "bool" group_def "algebra/")
(subgroup type-eq-decl nil group "algebra/")
(a_by_c const-decl "(G)" normalizer_centralizer nil)
(CLs const-decl "setofsets[T]" normalizer_centralizer nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil normalizer_centralizer nil)
(orbit const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil)
(CL const-decl "{X: set[T] | subset?(X, G)}" normalizer_centralizer
nil))
shostak))
(orbits_nFix_is_CLs_nc 0
(orbits_nFix_is_CLs_nc-1 nil 3530363243
("" (skosimp)
(("" (decompose-equality 1)
(("" (iff)
(("" (expand* "orbits_nFix" "CLs_nc")
(("" (expand "extend")
(("" (lift-if)
(("" (lift-if)
(("" (lift-if)
(("" (lemma "Fix_is_center")
(("" (inst?)
(("" (prop)
(("1" (skosimp)
(("1" (inst?)
(("1" (rewrite "orbit_is_CL") nil nil)
("2" (hide (-2 -3 -4))
(("2"
(typepred "x!2")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (inst?)
(("1" (rewrite "orbit_is_CL") nil nil)
("2" (hide (-2 -3 -4))
(("2"
(typepred "x!2")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("3" (skosimp)
(("3" (hide (-1 -3))
(("3" (rewrite "orbits_is_CLs") nil nil))
nil))
nil)
("4" (skosimp)
(("4" (rewrite "orbits_is_CLs") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(* formal-const-decl "[T, T -> T]" normalizer_centralizer nil)
(one formal-const-decl "T" normalizer_centralizer nil)
(group? const-decl "bool" group_def "algebra/")
(group nonempty-type-eq-decl nil group "algebra/")
(F type-eq-decl nil group_action nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(orbits_nFix const-decl "setofsets[T1]" group_action nil)
(subgroup? const-decl "bool" group_def "algebra/")
(subgroup type-eq-decl nil group "algebra/")
(a_by_c const-decl "(G)" normalizer_centralizer nil)
(CLs_nc const-decl "setofsets[T]" normalizer_centralizer nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil normalizer_centralizer nil)
(orbits_is_CLs formula-decl nil normalizer_centralizer nil)
(x!2 skolem-const-decl "{x: (G!1) | NOT member(x, center(G!1))}"
normalizer_centralizer nil)
(orbit_is_CL formula-decl nil normalizer_centralizer nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(subset? const-decl "bool" sets nil)
(center const-decl "{s: set[T] | subset?(s, G)}" group "algebra/")
(G!1 skolem-const-decl "group[T, *, one]" normalizer_centralizer
nil)
(member const-decl "bool" sets nil)
(Fix const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil)
(x!2 skolem-const-decl
"{x: (G!1) | NOT member(x, Fix(G!1, G!1)(a_by_c(G!1, G!1)))}"
normalizer_centralizer nil)
(Fix_is_center formula-decl nil normalizer_centralizer nil)
(extend const-decl "R" extend nil))
shostak))
(CLs_eq_index_TCC1 0
(CLs_eq_index_TCC1-1 nil 3530354396
("" (skosimp)
(("" (lemma "centralizer_is_subgroup")
(("" (inst?)
(("" (assert)
(("" (lemma "subgroup_is_group")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((centralizer_is_subgroup formula-decl nil normalizer_centralizer
nil)
(subset? const-decl "bool" sets nil)
(centralizer const-decl "{S: set[T] | subset?(S, G)}"
normalizer_centralizer nil)
(subgroup_is_group formula-decl nil group "algebra/")
(finite_group nonempty-type-eq-decl nil group "algebra/")
(finite_group? const-decl "bool" group_def "algebra/")
(group nonempty-type-eq-decl nil group "algebra/")
(group? const-decl "bool" group_def "algebra/")
(one formal-const-decl "T" normalizer_centralizer nil)
(* formal-const-decl "[T, T -> T]" normalizer_centralizer 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-type-decl nil normalizer_centralizer nil))
nil))
(CLs_eq_index_TCC2 0
(CLs_eq_index_TCC2-1 nil 3530354396
("" (skosimp)
(("" (lemma "orbit_is_CL")
(("" (inst?)
(("" (replace -1 1 rl)
(("" (hide -1)
(("" (typepred "G!1")
(("" (expand "finite_group?")
(("" (flatten)
(("" (hide -1)
(("" (rewrite "orbit_is_finite")
(("" (hide (-1 2))
(("" (rewrite "a_by_c_is_action")
(("" (hide 2)
(("" (rewrite "group_is_subgroup") nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((orbit_is_CL formula-decl nil normalizer_centralizer nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(orbit_is_finite formula-decl nil group_action nil)
(F type-eq-decl nil group_action nil)
(subgroup? const-decl "bool" group_def "algebra/")
(subgroup type-eq-decl nil group "algebra/")
(a_by_c const-decl "(G)" normalizer_centralizer nil)
(a_by_c_is_action formula-decl nil normalizer_centralizer nil)
(group_is_subgroup formula-decl nil group "algebra/")
(finite_group nonempty-type-eq-decl nil group "algebra/")
(finite_group? const-decl "bool" group_def "algebra/")
(group nonempty-type-eq-decl nil group "algebra/")
(group? const-decl "bool" group_def "algebra/")
(one formal-const-decl "T" normalizer_centralizer nil)
(* formal-const-decl "[T, T -> T]" normalizer_centralizer 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-type-decl nil normalizer_centralizer nil))
nil))
(CLs_eq_index 0
(CLs_eq_index-1 nil 3530357482
("" (skosimp*)
(("" (typepred "G!1")
(("" (expand "finite_group?")
(("" (flatten)
(("" (hide -1)
(("" (lemma "orbits_eq_index")
(("" (inst -1 "G!1" "G!1" "x!1" "a_by_c(G!1,G!1)")
(("1" (assert)
(("1" (prop)
(("1" (rewrite "stabilizer_is_centralizer")
(("1" (rewrite "orbit_is_CL") nil nil)) nil)
("2" (hide (-1 2))
(("2" (rewrite "a_by_c_is_action")
(("2" (hide 2)
(("2" (rewrite "group_is_subgroup") nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide (-1 2))
(("2" (rewrite "group_is_subgroup") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((finite_group nonempty-type-eq-decl nil group "algebra/")
(finite_group? const-decl "bool" group_def "algebra/")
(one formal-const-decl "T" normalizer_centralizer nil)
(* formal-const-decl "[T, T -> T]" normalizer_centralizer nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil normalizer_centralizer nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(orbits_eq_index formula-decl nil group_action nil)
(group_is_subgroup formula-decl nil group "algebra/")
(a_by_c_is_action formula-decl nil normalizer_centralizer nil)
(stabilizer_is_centralizer formula-decl nil normalizer_centralizer
nil)
(orbit_is_CL formula-decl nil normalizer_centralizer nil)
(a_by_c const-decl "(G)" normalizer_centralizer nil)
(subgroup type-eq-decl nil group "algebra/")
(group nonempty-type-eq-decl nil group "algebra/")
(F type-eq-decl nil group_action nil)
(group? const-decl "bool" group_def "algebra/")
(subgroup? const-decl "bool" group_def "algebra/")
(G!1 skolem-const-decl "finite_group[T, *, one]"
normalizer_centralizer nil))
shostak))
(class_equation_2_TCC1 0
(class_equation_2_TCC1-1 nil 3530354396
("" (skosimp)
(("" (lemma "center_subgroup")
(("" (inst?)
(("" (expand "subgroup?")
(("" (typepred "G!1")
(("" (expand "finite_group?")
(("" (flatten)
(("" (hide (-1 -4))
(("" (lemma "finite_subset[T]")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((one formal-const-decl "T" normalizer_centralizer nil)
(* formal-const-decl "[T, T -> T]" normalizer_centralizer nil)
(T formal-type-decl nil normalizer_centralizer nil)
(center_subgroup formula-decl nil group "algebra/")
(subgroup? const-decl "bool" group_def "algebra/")
(is_finite const-decl "bool" finite_sets nil)
(G!1 skolem-const-decl "finite_group[T, *, one]"
normalizer_centralizer nil)
(finite_set type-eq-decl nil finite_sets nil)
(subset? const-decl "bool" sets nil)
(center const-decl "{s: set[T] | subset?(s, G)}" group "algebra/")
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(finite_subset formula-decl nil finite_sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(finite_group nonempty-type-eq-decl nil group "algebra/")
(finite_group? const-decl "bool" group_def "algebra/")
(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))
nil))
(class_equation_2_TCC2 0
(class_equation_2_TCC2-1 nil 3530354396
("" (skosimp)
(("" (case "empty?(CLs_nc(G!1))")
(("1"
(case-replace
"restrict[setof[T], finite_set[T], boolean](CLs_nc(G!1)) = emptyset"
:hide? T)
(("1" (rewrite "convergent_empty") nil nil)
("2" (hide 2)
(("2" (decompose-equality 1)
(("2" (expand "restrict")
(("2" (expand* "emptyset" "empty?" "member")
(("2" (inst -2 "x!1") nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (lemma "card_partition_TCC2")
(("2" (inst?)
(("1" (assert)
(("1" (hide 3)
(("1" (expand "nonempty?")
(("1" (hide 2)
(("1" (skosimp)
(("1" (typepred "A!1")
(("1" (expand "CLs_nc")
(("1" (expand "extend")
(("1" (prop)
(("1" (hide -2)
(("1"
(expand "CLs")
(("1"
(skosimp)
(("1"
(replaces -1)
(("1"
(lemma "orbit_is_CL")
(("1"
(inst?)
(("1"
(replace -1 -2 rl)
(("1"
(hide -1)
(("1"
(lemma "orbit_nonempty")
(("1"
(inst?)
(("1"
(prop)
(("1"
(expand
"nonempty?")
(("1"
(rewrite
"empty_card")
nil
nil))
nil)
("2"
(hide -1)
(("2"
(rewrite
"a_by_c_is_action")
(("2"
(hide 2)
(("2"
(rewrite
"group_is_subgroup")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide (2 3))
(("2" (lemma "orbits_nFix_is_CLs_nc")
(("2" (inst?)
(("2" (replace -1 1 rl)
(("2" (hide -1)
(("2" (typepred "G!1")
(("2" (expand "finite_group?")
(("2" (flatten)
(("2" (hide -1)
(("2" (lemma "orbits_nFix_partition")
(("2"
(inst?)
(("2"
(assert)
(("2"
(hide (-1 2))
(("2"
(rewrite "a_by_c_is_action")
(("2"
(hide 2)
(("2"
(rewrite "group_is_subgroup")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((finite_group nonempty-type-eq-decl nil group "algebra/")
(finite_group? const-decl "bool" group_def "algebra/")
(CLs_nc const-decl "setofsets[T]" normalizer_centralizer nil)
(setofsets type-eq-decl nil sets nil)
(group nonempty-type-eq-decl nil group "algebra/")
(group? const-decl "bool" group_def "algebra/")
(one formal-const-decl "T" normalizer_centralizer nil)
(* formal-const-decl "[T, T -> T]" normalizer_centralizer nil)
(empty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil normalizer_centralizer nil)
(member const-decl "bool" sets nil)
(card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
(Card const-decl "nat" finite_sets nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(convergent_empty formula-decl nil convergence_set "sigma_set/")
(emptyset const-decl "set" sets nil)
(restrict const-decl "R" restrict nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_emptyset name-judgement "finite_set[finite_set[T1]]"
normalizer_centralizer nil)
(finite_emptyset name-judgement "finite_set[T]"
finite_sets_inductions "finite_sets/")
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(G!1 skolem-const-decl "finite_group[T, *, one]"
normalizer_centralizer nil)
(finite_partition? const-decl "bool" lagrange_scaf "algebra/")
(finite_partition type-eq-decl nil lagrange_scaf "algebra/")
(NOT const-decl "[bool -> bool]" booleans nil)
(extend const-decl "R" extend nil)
(orbit_is_CL formula-decl nil normalizer_centralizer nil)
(orbit_nonempty formula-decl nil group_action nil)
(orbit const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil)
(subset? const-decl "bool" sets nil)
(empty_card formula-decl nil finite_sets nil)
(a_by_c_is_action formula-decl nil normalizer_centralizer nil)
(group_is_subgroup formula-decl nil group "algebra/")
(F type-eq-decl nil group_action nil)
(subgroup? const-decl "bool" group_def "algebra/")
(subgroup type-eq-decl nil group "algebra/")
(a_by_c const-decl "(G)" normalizer_centralizer nil)
(CLs const-decl "setofsets[T]" normalizer_centralizer nil)
(nonempty? const-decl "bool" sets nil)
(orbits_nFix_is_CLs_nc formula-decl nil normalizer_centralizer nil)
(orbits_nFix_partition formula-decl nil group_action nil)
(card_partition_TCC2 subtype-tcc nil class_equation_scaf nil))
nil))
(class_equation_2 0
(class_equation_2-1 nil 3530354496
("" (skosimp*)
(("" (typepred "G!1")
(("" (expand "finite_group?")
(("" (flatten)
(("" (hide -1)
(("" (lemma "class_equation")
(("" (inst -1 "G!1" "G!1" "a_by_c(G!1,G!1)")
(("1" (assert)
(("1" (prop)
(("1" (rewrite "Fix_is_center")
(("1" (rewrite "orbits_nFix_is_CLs_nc")
(("1" (expand "order") (("1" (propax) nil nil))
nil))
nil))
nil)
("2" (hide (-1 2))
(("2" (expand* "nonempty?" "empty?" "member")
(("2" (inst -1 "one")
(("2" (rewrite "one_in") nil nil)) nil))
nil))
nil)
("3" (hide 2)
(("3" (lemma "a_by_c_is_action")
(("3" (inst -1 "G!1" "G!1")
(("3" (assert)
(("3" (hide (-1 2))
(("3"
(rewrite "group_is_subgroup")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide (-1 2))
(("2" (rewrite "group_is_subgroup") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((finite_group nonempty-type-eq-decl nil group "algebra/")
(finite_group? const-decl "bool" group_def "algebra/")
(one formal-const-decl "T" normalizer_centralizer nil)
(* formal-const-decl "[T, T -> T]" normalizer_centralizer nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil normalizer_centralizer nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(class_equation formula-decl nil group_action nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(group_is_subgroup formula-decl nil group "algebra/")
(a_by_c_is_action formula-decl nil normalizer_centralizer nil)
(one_in formula-decl nil monad "algebra/")
(monad? const-decl "bool" monad_def "algebra/")
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.95 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.
|
