|
(p_groups
(IMP_finite_groups_TCC1 0
(IMP_finite_groups_TCC1-1 nil 3530721851
("" (rewrite "fullset_is_group") nil nil)
((fullset_is_group formula-decl nil p_groups nil)) nil))
(p_group?_TCC1 0
(p_group?_TCC1-1 nil 3530273648 ("" (subtype-tcc) nil nil) nil nil))
(alt_is_action_TCC1 0
(alt_is_action_TCC1-1 nil 3530265242
("" (skosimp*)
(("" (typepred "x1!1`2" "x1!1`1" "H!1")
(("" (expand "subgroup?")
(("" (expand* "subset?" "member")
(("" (inst?)
(("" (assert)
(("" (hide -3)
(("" (expand "left_cosets")
(("" (skosimp)
(("" (expand "alt")
(("" (inst 1 "x1!1`1 * a!1")
(("1" (replaces -1)
(("1" (rewrite "left_coset_assoc") nil nil))
nil)
("2" (rewrite "product_in") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((left_cosets const-decl "setofsets[T]" right_left_cosets nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(subgroup 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)
(group nonempty-type-eq-decl nil group "algebra/")
(one formal-const-decl "T" p_groups nil)
(* formal-const-decl "[T, T -> T]" p_groups nil)
(T formal-type-decl nil p_groups 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)
(alt const-decl "set[T]" p_groups nil)
(product_in formula-decl nil group "algebra/")
(left_coset_assoc formula-decl nil cosets "algebra/")
(G!1 skolem-const-decl "group[T, *, one]" p_groups nil)
(H!1 skolem-const-decl "subgroup[T, *, one](G!1)" p_groups nil)
(K!1 skolem-const-decl "subgroup[T, *, one](G!1)" p_groups nil)
(x1!1 skolem-const-decl "[(H!1), (left_cosets(G!1, K!1))]" p_groups
nil)
(a!1 skolem-const-decl "(G!1)" p_groups nil))
nil))
(alt_is_action 0
(alt_is_action-1 nil 3530282276
("" (skosimp*)
(("" (expand "group_action?")
(("" (skosimp*)
(("" (prop)
(("1" (expand "alt")
(("1" (rewrite "left_coset_one") nil nil)) nil)
("2" (expand "alt")
(("2" (rewrite "left_coset_assoc") nil nil)) nil))
nil))
nil))
nil))
nil)
((group_action? const-decl "bool" group_action nil)
(left_coset_one formula-decl nil cosets "algebra/")
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(group nonempty-type-eq-decl nil group "algebra/")
(group? const-decl "bool" group_def "algebra/")
(subgroup? const-decl "bool" group_def "algebra/")
(subgroup type-eq-decl nil group "algebra/")
(setofsets type-eq-decl nil sets nil)
(left_cosets const-decl "setofsets[T]" right_left_cosets nil)
(T formal-type-decl nil p_groups nil)
(* formal-const-decl "[T, T -> T]" p_groups nil)
(one formal-const-decl "T" p_groups nil)
(alt const-decl "set[T]" p_groups nil)
(left_coset_assoc formula-decl nil cosets "algebra/"))
shostak))
(Fix_iff_subset 0
(Fix_iff_subset-1 nil 3530282442
("" (skosimp*)
(("" (expand* "subset?" "member" "Fix" "alt")
(("" (expand "extend")
(("" (prop)
(("1" (skosimp)
(("1" (inst -2 "x!1")
(("1" (rewrite "left_coset_assoc")
(("1" (lemma "lc_eq")
(("1" (inst -1 "G!1" "K!1" "x!1 * g!1" "g!1")
(("1" (assert)
(("1" (skosimp)
(("1" (hide (-2 -3 -4))
(("1" (expand "*" 1)
(("1" (inst 1 "g!1 * h!1")
(("1"
(replace -1 1 rl)
(("1"
(rewrite "assoc" :dir rl)
nil
nil))
nil)
("2" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (typepred "g!2")
(("2" (inst?)
(("2" (assert)
(("2" (expand "*" -3)
(("2" (skosimp)
(("2" (hide -1)
(("2" (rewrite "left_coset_assoc")
(("2" (lemma "lc_is_eq")
(("2"
(inst -1 "G!1" "K!1" "g!2 * g!1" "g!1")
(("2"
(assert)
(("2"
(inst 1 "inv(g!1) * h!1")
(("1"
(hide 2)
(("1"
(replaces -2)
(("1"
(rewrite "assoc")
(("1"
(rewrite "assoc" :dir rl)
nil
nil))
nil))
nil))
nil)
("2"
(hide (-1 -2 2))
(("2"
(typepred "h!1")
(("2"
(skosimp)
(("2"
(replaces -1)
(("2"
(typepred "h!2")
(("2"
(rewrite "assoc")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide -1)
(("3" (expand "left_cosets") (("3" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((member const-decl "bool" sets nil)
(alt const-decl "set[T]" p_groups nil)
(Fix const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil)
(subset? const-decl "bool" sets nil)
(x!1 skolem-const-decl "T" p_groups nil)
(H!1 skolem-const-decl "subgroup[T, *, one](G!1)" p_groups nil)
(subgroup type-eq-decl nil group "algebra/")
(G!1 skolem-const-decl "group[T, *, one]" p_groups 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" p_groups nil)
(* formal-const-decl "[T, T -> T]" p_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-type-decl nil p_groups nil)
(lc_eq formula-decl nil cosets "algebra/")
(K!1 skolem-const-decl "subgroup[T, *, one](G!1)" p_groups nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(g!1 skolem-const-decl "(G!1)" p_groups nil)
(h!1 skolem-const-decl "(K!1)" p_groups nil)
(inv_right 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/")
(* const-decl "set[T]" cosets "algebra/")
(* const-decl "set[T]" cosets "algebra/")
(left_coset_assoc formula-decl nil cosets "algebra/")
(NOT const-decl "[bool -> bool]" booleans nil)
(h!1 skolem-const-decl "({t: T | EXISTS (h: (K!1)): t = g!1 * h})"
p_groups nil)
(inv_left formula-decl nil group "algebra/")
(left_identity formula-decl nil monad "algebra/")
(lc_is_eq formula-decl nil cosets "algebra/")
(left_cosets const-decl "setofsets[T]" right_left_cosets nil)
(extend const-decl "R" extend nil))
shostak))
(Fix_iff_subset_cor_TCC1 0
(Fix_iff_subset_cor_TCC1-1 nil 3530267101
("" (skosimp*)
(("" (typepred "x1!1`2" "x1!1`1" "H!1")
(("" (expand "subgroup?")
(("" (expand* "subset?" "member")
(("" (inst?)
(("" (assert)
(("" (hide -3)
(("" (expand "left_cosets")
(("" (skosimp)
(("" (expand "alt")
(("" (inst 1 "x1!1`1 * a!1")
(("1" (replaces -1)
(("1" (rewrite "left_coset_assoc") nil nil))
nil)
("2" (rewrite "product_in") 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/")
(left_cosets const-decl "setofsets[T]" right_left_cosets nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(subgroup 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)
(group nonempty-type-eq-decl nil group "algebra/")
(one formal-const-decl "T" p_groups nil)
(* formal-const-decl "[T, T -> T]" p_groups nil)
(T formal-type-decl nil p_groups 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)
(alt const-decl "set[T]" p_groups nil)
(product_in formula-decl nil group "algebra/")
(left_coset_assoc formula-decl nil cosets "algebra/")
(G!1 skolem-const-decl "finite_group[T, *, one]" p_groups nil)
(H!1 skolem-const-decl "subgroup[T, *, one](G!1)" p_groups nil)
(x1!1 skolem-const-decl "[(H!1), (left_cosets(G!1, H!1))]" p_groups
nil)
(a!1 skolem-const-decl "(G!1)" p_groups nil))
nil))
(Fix_iff_subset_cor 0
(Fix_iff_subset_cor-1 nil 3530285250
("" (skosimp*)
(("" (lemma "Fix_iff_subset")
(("" (inst -1 "G!1" "H!1" "H!1" "g!1")
(("" (assert)
(("" (prop)
(("1" (hide (-1 -2))
(("1" (lemma "left_coset_correspondence_inv[T, *, one]")
(("1" (inst -1 "G!1" "H!1" "g!1")
(("1" (assert)
(("1" (typepred "H!1")
(("1" (hide -1)
(("1" (lemma "finite_subgroups")
(("1" (inst?)
(("1" (assert)
(("1"
(hide -2)
(("1"
(expand "finite_group?")
(("1"
(lemma "card_eq_bij[T, T]")
(("1"
(inst
-1
"H!1"
"g!1 * H!1 * inv(g!1)")
(("1"
(prop)
(("1"
(hide (-2 -4))
(("1"
(rewrite
"same_card_subset")
nil
nil))
nil))
nil)
("2"
(hide (-3 2))
(("2"
(lemma
"bijection_finite_set2[T,T]")
(("2"
(inst
-1
"H!1"
"g!1 * H!1 * inv(g!1)")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide (1 3))
(("2" (replace -1 1 rl)
(("2" (hide -1)
(("2" (rewrite "subset_reflexive") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Fix_iff_subset formula-decl nil p_groups nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(member const-decl "bool" sets nil)
(subset_reflexive formula-decl nil sets_lemmas nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(finite_subgroups formula-decl nil group "algebra/")
(is_finite const-decl "bool" finite_sets nil)
(G!1 skolem-const-decl "finite_group[T, *, one]" p_groups nil)
(H!1 skolem-const-decl "subgroup[T, *, one](G!1)" p_groups nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group
"algebra/")
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(g!1 skolem-const-decl "(G!1)" p_groups nil)
(* const-decl "set[T]" cosets "algebra/")
(* const-decl "set[T]" cosets "algebra/")
(finite_set type-eq-decl nil finite_sets nil)
(same_card_subset formula-decl nil finite_sets nil)
(bijection_finite_set2 formula-decl nil finite_sets_eq
"finite_sets/")
(card_eq_bij formula-decl nil finite_sets_card_eq "finite_sets/")
(left_coset_correspondence_inv formula-decl nil right_left_cosets
nil)
(subgroup type-eq-decl nil group "algebra/")
(subgroup? const-decl "bool" group_def "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" p_groups nil)
(* formal-const-decl "[T, T -> T]" p_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-type-decl nil p_groups nil))
shostak))
(subgroup_is_p_group_TCC1 0
(subgroup_is_p_group_TCC1-1 nil 3530352745
("" (skosimp*)
(("" (lemma "finite_subgroups")
(("" (inst -1 "H!1" "G!1") (("" (assert) nil nil)) nil)) nil))
nil)
((one formal-const-decl "T" p_groups nil)
(* formal-const-decl "[T, T -> T]" p_groups nil)
(T formal-type-decl nil p_groups nil)
(finite_subgroups formula-decl nil group "algebra/")
(subgroup type-eq-decl nil group "algebra/")
(finite_group nonempty-type-eq-decl nil group "algebra/")
(finite_group? const-decl "bool" group_def "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))
nil))
(subgroup_is_p_group 0
(subgroup_is_p_group-1 nil 3530352927
("" (skosimp*)
(("" (hide -1)
(("" (expand "p_group?")
(("" (skosimp)
(("" (inst -1 "a!1")
(("1" (skosimp)
(("1" (inst?)
(("1" (replace -1 1 rl)
(("1" (hide -1)
(("1" (expand "period") (("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (typepred "a!1" "H!1")
(("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)
((subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(period const-decl "posnat" finite_groups "algebra/")
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(T formal-type-decl nil p_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]" p_groups nil)
(one formal-const-decl "T" p_groups nil)
(finite_group? const-decl "bool" group_def "algebra/")
(finite_group nonempty-type-eq-decl nil group "algebra/")
(G!1 skolem-const-decl "finite_group[T, *, one]" p_groups 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/")
(H!1 skolem-const-decl "subgroup[T, *, one](G!1)" p_groups nil)
(a!1 skolem-const-decl "(H!1)" p_groups nil)
(p_group? const-decl "bool" p_groups nil))
shostak))
(p_group_iff_power_TCC1 0
(p_group_iff_power_TCC1-1 nil 3530273648 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)
(divides const-decl "bool" divides nil)
(prime? const-decl "bool" primes "ints/"))
nil))
(p_group_iff_power 0
(p_group_iff_power-1 nil 3530719670
("" (skosimp*)
(("" (prop)
(("1" (lemma "prime_factors")
(("1" (inst -1 "order(G!1)")
(("1" (skosimp)
(("1" (lemma "product_only_power")
(("1" (inst -1 "fs!1" "p!1")
(("1" (prop)
(("1" (skosimp)
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
("2" (hide 2)
(("2" (expand "ordered_list_of_primes?")
(("2" (flatten)
(("2" (hide -3)
(("2"
(expand* "only_power_p" "p_group?"
"list_of_primes?")
(("2" (skosimp)
(("2"
(lemma "divides_product")
(("2"
(inst -1 "fs!1" "j!1")
(("2"
(inst -3 "j!1")
(("2"
(replace -2 -1 rl)
(("2"
(hide -2)
(("2"
(lemma "cauchy")
(("2"
(inst?)
(("2"
(assert)
(("2"
(skosimp)
(("2"
(inst -4 "x!1")
(("2"
(skosimp)
(("2"
(replaces -1)
(("2"
(inst?)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (expand "p_group?")
(("2" (skosimp)
(("2" (lemma "Lagrange")
(("2" (inst -1 "G!1" "generated_by(a!1)")
(("1" (prop)
(("1" (replaces -2)
(("1" (lemma "divides_prime_power")
(("1" (inst?)
(("1" (assert)
(("1" (skosimp)
(("1" (hide -1)
(("1"
(lemma "period_is_generated_order")
(("1"
(inst?)
(("1"
(assert)
(("1"
(inst 1 "i!1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (rewrite "generated_is_subgroup") nil nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (expand "finite_group?")
(("2" (lemma "finite_generated_by")
(("2" (inst -1 "G!1" "a!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(T formal-type-decl nil p_groups nil)
(set type-eq-decl nil sets nil)
(* formal-const-decl "[T, T -> T]" p_groups nil)
(one formal-const-decl "T" p_groups nil)
(finite_monad? const-decl "bool" monad_def "algebra/")
(finite_monad nonempty-type-eq-decl nil monad "algebra/")
(order const-decl "posnat" monad "algebra/")
(finite_group? const-decl "bool" group_def "algebra/")
(finite_group nonempty-type-eq-decl nil group "algebra/")
(product_only_power formula-decl nil general_properties nil)
(posint_exp application-judgement "posint" exponentiation nil)
(ordered_list_of_primes? const-decl "bool" prime_factorization
"numbers/")
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(cauchy formula-decl nil cauchy nil)
(divides_product formula-decl nil general_properties nil)
(only_power_p const-decl "bool" general_properties nil)
(list_of_primes? const-decl "bool" prime_factorization "numbers/")
(p_group? const-decl "bool" p_groups nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(barray type-eq-decl nil fseqs "structures/")
(fseq type-eq-decl nil fseqs "structures/")
(prime_factors formula-decl nil prime_factorization "numbers/")
(Lagrange formula-decl nil lagrange "algebra/")
(finite_generated_by formula-decl nil finite_groups "algebra/")
(divides_prime_power formula-decl nil general_properties nil)
(member const-decl "bool" sets nil)
(period_is_generated_order formula-decl nil finite_groups
"algebra/")
(generated_is_subgroup formula-decl nil cyclic_group "algebra/")
(group? const-decl "bool" group_def "algebra/")
(group nonempty-type-eq-decl nil group "algebra/")
(generated_by const-decl "group" group "algebra/")
(G!1 skolem-const-decl "finite_group[T, *, one]" p_groups nil)
(a!1 skolem-const-decl "(G!1)" p_groups nil))
shostak))
(p_divides_index 0
(p_divides_index-1 nil 3530567198
("" (skosimp*)
(("" (typepred "G!1" "H!1")
(("" (hide -2)
(("" (lemma "finite_subgroups")
(("" (inst -1 "H!1" "G!1")
(("" (assert)
(("" (lemma "index_divides")
(("" (inst?)
(("" (assert)
(("" (lemma "p_group_iff_power")
(("" (inst?)
(("" (assert)
(("" (skosimp)
(("" (replaces -1)
((""
(lemma "divides_prime_power")
((""
(inst?)
(("1"
(assert)
(("1"
(skosimp)
(("1"
(hide (-1 -3 -8))
(("1"
(case-replace
"i!1 = 0"
:hide?
T)
(("1"
(rewrite "expt_x0")
(("1"
(lemma "Lagrange_index")
(("1"
(inst?)
(("1"
(assert)
(("1"
(replaces -2 -1)
(("1"
(rewrite
"identity_mult")
(("1"
(lemma
"orders_equal")
(("1"
(inst
-1
"G!1"
"H!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide (-2 -3 -4 2))
(("2"
(replaces -1)
(("2"
(rewrite
"divides_power")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide (-1 -5 -6 2 3))
(("2"
(lemma "index_gt1")
(("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)
((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/")
(finite_group nonempty-type-eq-decl nil group "algebra/")
(finite_group? const-decl "bool" group_def "algebra/")
(one formal-const-decl "T" p_groups nil)
(* formal-const-decl "[T, T -> T]" p_groups nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil p_groups nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(finite_subgroups formula-decl nil group "algebra/")
(p_group_iff_power formula-decl nil p_groups nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(index const-decl "nat" right_left_cosets nil)
(G!1 skolem-const-decl "finite_group[T, *, one]" p_groups nil)
(H!1 skolem-const-decl "subgroup[T, *, one](G!1)" p_groups nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Lagrange_index formula-decl nil lagrange_index nil)
(order const-decl "posnat" monad "algebra/")
(finite_monad nonempty-type-eq-decl nil monad "algebra/")
(finite_monad? const-decl "bool" monad_def "algebra/")
(numfield nonempty-type-eq-decl nil number_fields nil)
(identity_mult formula-decl nil number_fields nil)
(orders_equal formula-decl nil finite_groups "algebra/")
(expt_x0 formula-decl nil exponentiation nil)
(divides_power formula-decl nil general_properties nil)
(posint_exp application-judgement "posint" exponentiation nil)
(index_gt1 formula-decl nil right_left_cosets nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(divides_prime_power formula-decl nil general_properties nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers 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)
(index_divides formula-decl nil lagrange_index nil))
shostak))
(factor_cyclic_TCC1 0
(factor_cyclic_TCC1-1 nil 3530273648
("" (skosimp*)
(("" (lemma "center_subgroup")
(("" (inst?)
(("" (expand "normal_subgroup?")
(("" (assert)
(("" (expand "subgroup?")
(("" (assert)
(("" (skosimp)
(("" (expand* "subset?" "member")
(("" (skosimp)
(("" (hide -1)
(("" (expand "*")
(("" (skosimp)
(("" (typepred "h!1")
((""
(skosimp)
((""
(typepred "h!2")
((""
(expand "center")
((""
(expand "extend")
((""
(ground)
(("1"
(skosimp)
(("1"
(hide (-1 -2))
(("1"
(replaces -2)
(("1"
(replaces -2)
(("1"
(inst-cp -1 "a!1")
(("1"
(rewrite
"assoc"
:dir
rl)
(("1"
(replace -2 1 rl)
(("1"
(rewrite
"assoc")
(("1"
(inst
-1
"x!2")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -2)
(("2"
(replaces -2)
(("2"
(replaces -2)
(("2"
(rewrite "product_in")
(("2"
(rewrite
"product_in")
(("2"
(rewrite "inv_in")
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)
((one formal-const-decl "T" p_groups nil)
(* formal-const-decl "[T, T -> T]" p_groups nil)
(T formal-type-decl nil p_groups nil)
(center_subgroup formula-decl nil group "algebra/")
(normal_subgroup? const-decl "boolean" normal_subgroups "algebra/")
(subgroup? const-decl "bool" group_def "algebra/")
(* const-decl "set[T]" cosets "algebra/")
(* const-decl "set[T]" cosets "algebra/")
(NOT const-decl "[bool -> bool]" booleans nil)
(center const-decl "{s: set[T] | subset?(s, G)}" group "algebra/")
(= 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
"algebra/")
(extend const-decl "R" extend nil)
(inv_in formula-decl nil group "algebra/")
(product_in formula-decl nil group "algebra/")
(left_identity formula-decl nil monad "algebra/")
(inv_left formula-decl nil group "algebra/")
(assoc formula-decl nil group "algebra/")
(subset? const-decl "bool" sets nil)
(member 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))
nil))
(factor_cyclic_TCC2 0
(factor_cyclic_TCC2-1 nil 3530273648
("" (skosimp*)
(("" (inst 1 "one")
(("1" (rewrite "left_coset_one") nil nil)
("2" (rewrite "one_in") nil nil))
nil))
nil)
((G!1 skolem-const-decl "group[T, *, one]" p_groups nil)
(group nonempty-type-eq-decl nil group "algebra/")
(group? const-decl "bool" group_def "algebra/")
(one formal-const-decl "T" p_groups nil)
(* formal-const-decl "[T, T -> T]" p_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-type-decl nil p_groups nil)
(center const-decl "{s: set[T] | subset?(s, G)}" group "algebra/")
(subset? const-decl "bool" sets nil)
(left_coset_one formula-decl nil cosets "algebra/")
(monad nonempty-type-eq-decl nil monad "algebra/")
(monad? const-decl "bool" monad_def "algebra/")
(one_in formula-decl nil monad "algebra/"))
nil))
(factor_cyclic_TCC3 0
(factor_cyclic_TCC3-1 nil 3530721851
("" (skosimp*)
(("" (rewrite "left_cosets_group")
(("" (hide 2)
(("" (lemma "center_is_normal[T, *, one]")
(("1" (inst?)
(("1" (assert)
(("1" (expand "normal_subgroup?")
(("1" (flatten)
(("1" (hide -2)
(("1" (expand "subgroup?") (("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2) (("2" (rewrite "fullset_is_group") nil nil))
nil))
nil))
nil))
nil))
nil)
((AND const-decl "[bool, bool -> bool]" booleans nil)
(left_cosets_group formula-decl nil factor_groups "algebra/")
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(group? const-decl "bool" group_def "algebra/")
(group nonempty-type-eq-decl nil group "algebra/")
(normal_subgroup? const-decl "boolean" normal_subgroups "algebra/")
(normal_subgroup type-eq-decl nil normal_subgroups "algebra/")
(subset? const-decl "bool" sets nil)
(center const-decl "{s: set[T] | subset?(s, G)}" group "algebra/")
(T formal-type-decl nil p_groups nil)
(* formal-const-decl "[T, T -> T]" p_groups nil)
(one formal-const-decl "T" p_groups nil)
(center_is_normal formula-decl nil groups_scaf nil)
(fullset const-decl "set" sets nil)
(subgroup? const-decl "bool" group_def "algebra/")
(fullset_is_group formula-decl nil p_groups nil))
nil))
(factor_cyclic 0
(factor_cyclic-1 nil 3530384047
("" (skosimp*)
(("" (lemma "center_is_normal[T, *, one]")
(("1" (inst?)
(("1" (expand "cyclic?")
(("1" (skosimp)
(("1" (typepred "a!1")
(("1" (skosimp)
(("1" (decompose-equality -4)
(("1" (hide -3)
(("1" (expand "abelian_group?")
(("1" (expand* "commutative?" "restrict")
(("1" (skosimp)
(("1" (inst-cp -1 "x!1 * center(G!1)")
(("1" (iff)
(("1"
(prop)
(("1"
(hide -1)
(("1"
(inst -2 "y!1 * center(G!1)")
(("1"
(iff)
(("1"
(prop)
(("1"
(hide -1)
(("1"
(expand "generated_by")
(("1"
(skosimp*)
(("1"
(replaces -3)
(("1"
(lemma
"coset_power_int[T,*,one]")
(("1"
(inst-cp
-1
"G!1"
"i!1"
"a!2"
"center(G!1)")
(("1"
(inst
-1
"G!1"
"i!2"
"a!2"
"center(G!1)")
(("1"
(replaces -1)
(("1"
(replaces -1)
(("1"
(lemma
"lc_eq")
(("1"
(inst-cp
-1
"G!1"
"center(G!1)"
"y!1"
"a!2 ^ i!1")
(("1"
(inst
-1
"G!1"
"center(G!1)"
"x!1"
"a!2 ^ i!2")
(("1"
(expand
"normal_subgroup?")
(("1"
(flatten)
(("1"
(assert)
(("1"
(hide
(-3
-4
-5
-6))
(("1"
(skosimp*)
(("1"
(replaces
-1)
(("1"
(replaces
-1)
(("1"
(typepred
"h!1"
"h!2")
(("1"
(expand*
"center"
"extend")
(("1"
(prop)
(("1"
(hide
(-1
-3))
(("1"
(rewrite
"assoc")
(("1"
(rewrite
"assoc")
(("1"
(rewrite
"assoc"
:dir
rl)
(("1"
(inst
-2
"a!2 ^ i!1")
(("1"
(replace
-2
1
rl)
(("1"
(hide
-2)
(("1"
(rewrite
"assoc"
:dir
rl)
(("1"
(rewrite
"assoc"
:dir
rl)
(("1"
(inst-cp
-1
"h!1")
(("1"
(replaces
-2)
(("1"
(rewrite
"assoc"
:dir
rl)
(("1"
(rewrite
"assoc"
:dir
rl)
(("1"
(inst
-1
"a!2 ^ i!2")
(("1"
(replace
-1
1
rl)
(("1"
(hide
-1)
(("1"
(rewrite
"assoc"
:dir
rl)
(("1"
(rewrite
"assoc")
(("1"
(rewrite
"assoc")
(("1"
(rewrite
"assoc")
(("1"
(rewrite
"assoc")
(("1"
(rewrite
"assoc")
(("1"
(rewrite
"assoc")
(("1"
(rewrite
"expt_mult")
(("1"
(rewrite
"expt_mult")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
2)
(("2"
(lemma
"expt_member")
(("2"
(inst
-1
"G!1"
"a!2"
"i!2")
(("2"
(assert)
nil
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.81 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
