|
(groups_scaf
(IMP_finite_groups_TCC1 0
(IMP_finite_groups_TCC1-1 nil 3530393611
("" (rewrite "fullset_is_group") nil nil)
((fullset_is_group formula-decl nil groups_scaf nil)) nil))
(divby_r 0
(divby_r-1 nil 3528491658
("" (skosimp*)
(("" (prop)
(("1" (replace -1)
(("1" (lemma "assoc[T, *, one]")
(("1" (inst?)
(("1" (replace -1 1 rl)
(("1" (rewrite "inv_right[T, *, one]")
(("1" (rewrite "right_identity[T, *, one]") nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace - + rl)
(("2" (hide -1)
(("2" (lemma "assoc[T, *, one]")
(("2" (inst?)
(("2" (replace -1 1 rl)
(("2" (rewrite "inv_left[T, *, one]")
(("2" (rewrite "right_identity[T, *, one]") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((one formal-const-decl "T" groups_scaf nil)
(* formal-const-decl "[T, T -> T]" groups_scaf nil)
(T formal-type-decl nil groups_scaf nil)
(assoc formula-decl nil group "algebra/")
(right_identity formula-decl nil monad "algebra/")
(inv_right 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)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(inv_left formula-decl nil group "algebra/"))
shostak))
(subgroup_transitive 0
(subgroup_transitive-1 nil 3528492327
("" (skeep)
(("" (expand "subgroup?")
(("" (expand* "subset?" "member")
(("" (skosimp*)
(("" (inst?) (("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((subgroup? const-decl "bool" group_def "algebra/")
(T formal-type-decl nil groups_scaf nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil))
shostak))
(normal_subgroup_tran 0
(normal_subgroup_tran-1 nil 3528492356
("" (skeep)
(("" (expand "normal_subgroup?")
(("" (prop)
(("" (skosimp)
(("" (inst?)
(("" (expand "subgroup?" -1)
(("" (hide-all-but (-1 1))
(("" (expand* "subset?" "member")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((normal_subgroup? const-decl "boolean" normal_subgroups "algebra/")
(subgroup? const-decl "bool" group_def "algebra/")
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(G skolem-const-decl "group[T, *, one]" groups_scaf nil)
(H skolem-const-decl "group[T, *, one]" groups_scaf nil)
(a!1 skolem-const-decl "(H)" groups_scaf nil)
(group nonempty-type-eq-decl nil group "algebra/")
(group? const-decl "bool" group_def "algebra/")
(one formal-const-decl "T" groups_scaf nil)
(* formal-const-decl "[T, T -> T]" groups_scaf 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 groups_scaf nil))
shostak))
(subgroup_intersection 0
(subgroup_intersection-1 nil 3528492374
("" (skeep)
(("" (lemma "subgroup_def[T,*,one]")
(("" (inst - "G" "intersection(H, K)")
(("" (assert)
(("" (hide 2)
(("" (prop)
(("1" (expand "nonempty?")
(("1" (expand "empty?")
(("1" (expand "member")
(("1" (expand "intersection")
(("1" (expand "member")
(("1" (inst - "one")
(("1" (hide (-1 -2))
(("1" (rewrite "one_in")
(("1" (rewrite "one_in") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand* "subgroup?" "subset?" "member")
(("2" (skosimp*)
(("2" (inst?)
(("2" (inst?)
(("2" (expand "intersection")
(("2" (assert) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "star_closed?")
(("3" (expand "intersection")
(("3" (assert)
(("3" (skosimp*)
(("3" (typepred "x!1")
(("3" (typepred "y!1")
(("3" (expand "intersection")
(("3" (assert)
(("3"
(flatten)
(("3"
(rewrite "product_in")
(("3"
(rewrite "product_in")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (hide (-1 -2))
(("4" (expand "inv_closed?")
(("4" (expand "intersection")
(("4" (expand "member")
(("4" (skosimp*)
(("4" (typepred "x!1")
(("4" (expand "intersection")
(("4" (assert)
(("4"
(rewrite "inv_in")
(("4" (rewrite "inv_in") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((one formal-const-decl "T" groups_scaf nil)
(* formal-const-decl "[T, T -> T]" groups_scaf nil)
(T formal-type-decl nil groups_scaf 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/")
(member const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil)
(subgroup? const-decl "bool" group_def "algebra/")
(subset? const-decl "bool" sets nil)
(product_in formula-decl nil group "algebra/")
(NOT const-decl "[bool -> bool]" booleans nil)
(star_closed? const-decl "bool" groupoid_def "algebra/")
(inv_closed? const-decl "bool" group "algebra/")
(inv_in formula-decl nil group "algebra/")
(intersection const-decl "set" 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))
(conjugate_is_subgroup 0
(conjugate_is_subgroup-1 nil 3531316370
("" (skosimp*)
(("" (lemma "subgroup_def[T,*,one]")
(("" (inst?)
(("" (assert)
(("" (hide 2)
(("" (prop)
(("1" (expand* "nonempty?" "empty?" "member")
(("1" (inst -1 "one")
(("1" (expand "*")
(("1" (inst 1 "a!1")
(("1" (rewrite "inv_right") nil nil)
("2" (inst 1 "one")
(("1" (assert) nil nil)
("2" (rewrite "one_in") nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "H!1")
(("2" (hide -1)
(("2" (expand* "subgroup?" "subset?" "member")
(("2" (skosimp*)
(("2" (expand "*")
(("2" (skosimp)
(("2" (typepred "h!1")
(("2" (skosimp)
(("2"
(replaces -1)
(("2"
(replaces -2)
(("2"
(inst -1 "h!2")
(("2"
(assert)
(("2"
(rewrite "product_in")
(("1"
(hide 2)
(("1"
(rewrite "product_in")
nil
nil))
nil)
("2"
(hide 2)
(("2"
(rewrite "inv_in")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "star_closed?")
(("3" (skosimp*)
(("3" (expand "member")
(("3" (typepred "x!1" "y!1")
(("3" (expand "*")
(("3" (skosimp*)
(("3" (typepred "h!1" "h!2")
(("3" (skosimp*)
(("3"
(replaces -1)
(("3"
(replaces -1)
(("3"
(replaces -1)
(("3"
(replaces -1)
(("3"
(rewrite "assoc")
(("3"
(rewrite "assoc")
(("3"
(rewrite "assoc" :dir rl)
(("3"
(rewrite "assoc" :dir rl)
(("3"
(rewrite
"assoc"
:dir
rl)
(("3"
(inst
1
"a!1 * h!3 * h!4")
(("3"
(inst
1
"h!3 * h!4")
(("1"
(rewrite "assoc")
nil
nil)
("2"
(rewrite
"product_in")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (expand "inv_closed?")
(("4" (skosimp*)
(("4" (expand "member")
(("4" (typepred "x!1")
(("4" (expand "*")
(("4" (skosimp)
(("4" (typepred "h!1")
(("4" (skosimp)
(("4"
(replaces -1)
(("4"
(replaces -1)
(("4"
(rewrite "inv_star")
(("4"
(rewrite "inv_star")
(("4"
(rewrite "assoc")
(("4"
(inst 1 "a!1 * inv(h!2)")
(("4"
(inst 1 "inv(h!2)")
(("4"
(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)
((one formal-const-decl "T" groups_scaf nil)
(* formal-const-decl "[T, T -> T]" groups_scaf nil)
(T formal-type-decl nil groups_scaf nil)
(subgroup_def formula-decl nil group "algebra/")
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(G!1 skolem-const-decl "group[T, *, one]" groups_scaf nil)
(H!1 skolem-const-decl "subgroup[T, *, one](G!1)" groups_scaf nil)
(a!1 skolem-const-decl "(G!1)" groups_scaf nil)
(inv_right formula-decl nil group "algebra/")
(monad nonempty-type-eq-decl nil monad "algebra/")
(monad? const-decl "bool" monad_def "algebra/")
(one_in formula-decl nil monad "algebra/")
(right_identity formula-decl nil monad "algebra/")
(nonempty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(inv_in formula-decl nil group "algebra/")
(product_in formula-decl nil group "algebra/")
(subset? const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(h!3 skolem-const-decl "(H!1)" groups_scaf nil)
(h!4 skolem-const-decl "(H!1)" groups_scaf nil)
(inv_left formula-decl nil group "algebra/")
(assoc formula-decl nil group "algebra/")
(star_closed? const-decl "bool" groupoid_def "algebra/")
(h!2 skolem-const-decl "(H!1)" groups_scaf nil)
(inv_inv formula-decl nil group "algebra/")
(inv_star formula-decl nil group "algebra/")
(inv_closed? const-decl "bool" 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)
(subgroup type-eq-decl nil group "algebra/")
(subgroup? const-decl "bool" group_def "algebra/")
(* const-decl "set[T]" cosets "algebra/")
(* const-decl "set[T]" cosets "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))
(center_is_normal_TCC1 0
(center_is_normal_TCC1-1 nil 3530391030
("" (skosimp*)
(("" (lemma "center_subgroup")
(("" (inst?)
(("" (expand "subgroup?") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((one formal-const-decl "T" groups_scaf nil)
(* formal-const-decl "[T, T -> T]" groups_scaf nil)
(T formal-type-decl nil groups_scaf nil)
(center_subgroup formula-decl nil group "algebra/")
(subgroup? const-decl "bool" group_def "algebra/")
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas 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))
(center_is_normal 0
(center_is_normal-1 nil 3530391031
("" (skosimp)
(("" (expand "normal_subgroup?")
(("" (lemma "center_subgroup")
(("" (inst?)
(("" (assert)
(("" (skosimp*)
(("" (typepred "a!1")
(("" (expand "subset?")
(("" (skosimp*)
(("" (expand "member")
(("" (expand "*")
(("" (skosimp*)
(("" (typepred "h!1")
(("" (skosimp*)
((""
(typepred "h!2")
((""
(rewrite "center_def" +)
((""
(prop)
(("1"
(replace -5)
(("1"
(replace -2)
(("1"
(typepred "center(G!1)")
(("1"
(expand "subset?")
(("1"
(assert)
(("1"
(inst - "h!2")
(("1"
(assert)
(("1"
(hide -2 -3 -5 -6)
(("1"
(lemma
"inv_member")
(("1"
(inst?)
(("1"
(inst?)
(("1"
(assert)
(("1"
(lemma
"product_in")
(("1"
(inst?)
(("1"
(assert)
(("1"
(hide
2)
(("1"
(lemma
"product_in")
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace -5)
(("2"
(skosimp)
(("2"
(hide -5)
(("2"
(replace -2)
(("2"
(hide -2)
(("2"
(name
"w"
"inv[T, *, one](a!1)")
(("2"
(replace -1)
(("2"
(hide -4)
(("2"
(rewrite
"center_def")
(("2"
(flatten)
(("2"
(inst-cp
-3
"w")
(("1"
(replace
-4)
(("1"
(lemma
"assoc")
(("1"
(inst
-
"h!2"
"w"
"a!1")
(("1"
(replace
-1
+
rl)
(("1"
(replace
-2
+
rl)
(("1"
(rewrite
"inv_left")
(("1"
(assert)
(("1"
(inst?)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"inv_in")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((normal_subgroup? const-decl "boolean" normal_subgroups "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/")
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(center_def formula-decl nil group "algebra/")
(G!1 skolem-const-decl "group[T, *, one]" groups_scaf nil)
(a!1 skolem-const-decl "(G!1)" groups_scaf nil)
(w skolem-const-decl "{y | a!1 * y = one AND y * a!1 = one}"
groups_scaf nil)
(assoc formula-decl nil group "algebra/")
(inv_left formula-decl nil group "algebra/")
(right_identity formula-decl nil monad "algebra/")
(inv_in formula-decl nil group "algebra/")
(inv_member formula-decl nil group "algebra/")
(product_in formula-decl nil group "algebra/")
(inv const-decl "{y | x * y = one AND y * x = one}" group
"algebra/")
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(center const-decl "{s: set[T] | subset?(s, G)}" group "algebra/")
(* const-decl "set[T]" cosets "algebra/")
(* const-decl "set[T]" cosets "algebra/")
(NOT const-decl "[bool -> bool]" booleans nil)
(center_subgroup formula-decl nil group "algebra/")
(T formal-type-decl nil groups_scaf nil)
(* formal-const-decl "[T, T -> T]" groups_scaf nil)
(one formal-const-decl "T" groups_scaf nil))
shostak))
(abelian_eq_center 0
(abelian_eq_center-1 nil 3528508011
("" (skosimp*)
(("" (prop)
(("1" (decompose-equality 1)
(("1" (iff)
(("1" (prop)
(("1" (expand "abelian_group?")
(("1" (expand* "commutative?" "center")
(("1" (expand "extend")
(("1" (assert)
(("1" (skosimp*)
(("1" (inst -2 "x!2" "x!1")
(("1" (expand "restrict")
(("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -2)
(("2" (expand "center")
(("2" (expand "extend") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand* "abelian_group?" "commutative?")
(("2" (skosimp*)
(("2" (expand "restrict")
(("2" (decompose-equality -1)
(("2" (inst -1 "y!1")
(("2" (iff)
(("2" (typepred "y!1")
(("2" (prop)
(("2" (expand* "center" "extend")
(("2" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((abelian_group? const-decl "bool" group_def "algebra/")
(extend const-decl "R" extend nil)
(restrict const-decl "R" restrict nil)
(commutative? const-decl "bool" operator_defs nil)
(T formal-type-decl nil groups_scaf nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(center const-decl "{s: set[T] | subset?(s, G)}" group "algebra/")
(subset? const-decl "bool" sets nil)
(group nonempty-type-eq-decl nil group "algebra/")
(group? const-decl "bool" group_def "algebra/")
(one formal-const-decl "T" groups_scaf nil)
(* formal-const-decl "[T, T -> T]" groups_scaf nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(NOT const-decl "[bool -> bool]" booleans nil))
shostak))
(order_gt_1 0
(order_gt_1-1 nil 3528737004
("" (skosimp)
(("" (lemma "prime_gt_1")
(("" (inst -1 "p!1")
(("" (assert)
(("" (expand "divides")
(("" (skosimp)
(("" (hide -2)
(("" (lemma "eq1_gt")
(("" (inst?)
(("" (assert)
(("" (lemma "pos_times_lt")
(("" (inst?) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((prime_gt_1 formula-decl nil primes "ints/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(eq1_gt formula-decl nil real_props nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(pos_times_lt formula-decl nil real_props nil)
(divides const-decl "bool" divides nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
shostak))
(order_gt_p 0
(order_gt_p-1 nil 3530364210
("" (skosimp)
(("" (lemma "prime_gt_1")
(("" (inst -1 "p!1")
(("" (prop)
(("" (expand "divides")
(("" (skosimp)
(("" (hide -2)
(("" (lemma "eq1_gt")
(("" (inst?)
(("" (assert)
(("" (lemma "pos_times_lt")
(("" (inst?)
(("" (assert)
(("" (replaces -3)
((""
(hide 1)
((""
(expand ">=")
((""
(lemma "le_times_le_pos")
((""
(inst -1 "p!1" "1" "x!1" "p!1")
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((prime_gt_1 formula-decl nil primes "ints/")
(eq1_gt formula-decl nil real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(le_times_le_pos formula-decl nil real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(pos_times_lt formula-decl nil real_props nil)
(divides const-decl "bool" divides nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
shostak))
(exists_diff_one 0
(exists_diff_one-1 nil 3528736184
("" (skosimp)
(("" (expand "order")
(("" (lemma "card_2_has_2[T]")
(("" (inst?)
(("" (assert)
(("" (skosimp)
(("" (case "x!1 = one")
(("1" (inst 2 "y!1") (("1" (assert) nil nil)) nil)
("2" (inst 3 "x!1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((order const-decl "posnat" monad "algebra/")
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(* formal-const-decl "[T, T -> T]" groups_scaf nil)
(one formal-const-decl "T" groups_scaf nil)
(finite_group? const-decl "bool" group_def "algebra/")
(finite_group nonempty-type-eq-decl nil group "algebra/")
(x!1 skolem-const-decl "T" groups_scaf nil)
(G!1 skolem-const-decl "finite_group[T, *, one]" groups_scaf nil)
(y!1 skolem-const-decl "T" groups_scaf nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(card_2_has_2 formula-decl nil finite_sets nil)
(T formal-type-decl nil groups_scaf nil))
shostak))
(one_iff_divides 0
(one_iff_divides-1 nil 3528766494
("" (skosimp)
(("" (prop)
(("1" (name-replace "n!1" "period(G!1, a!1)" :hide? nil)
(("1" (lemma "euclid_int")
(("1" (inst -1 "n!1" "m!1")
(("1" (skosimp)
(("1" (case-replace "r!1 =0")
(("1" (assert)
(("1" (expand "divides")
(("1" (inst 1 "q!1") nil nil)) nil))
nil)
("2" (hide 2)
(("2" (replace -1 -3)
(("2" (lemma "expt_mult")
(("2" (inst?)
(("2" (lemma "expt_expt")
(("2" (inst?)
(("2" (replace -1 -2 rl)
(("2"
(replace -2 -5 rl)
(("2"
(hide (-1 -2))
(("2"
(lemma "a_hat_period")
(("2"
(inst?)
(("2"
(assert)
(("2"
(replace -3 -1)
(("2"
(replaces -1)
(("2"
(rewrite "one_expt")
(("2"
(rewrite "one_left")
(("2"
(hide -1)
(("2"
(typepred "r!1")
(("2"
(expand "period")
(("2"
(lemma
"min_def")
(("2"
(inst?)
(("1"
(assert)
(("1"
(expand
"minimum?")
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(expand
"nonempty?")
(("2"
(expand
"empty?")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "divides")
(("2" (skosimp)
(("2" (replaces -1)
(("2" (lemma "expt_expt")
(("2" (inst?)
(("2" (lemma "a_hat_period")
(("2" (inst?)
(("2" (assert)
(("2" (replaces -1)
(("2" (rewrite "one_expt")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((euclid_int formula-decl nil euclidean_division nil)
(expt_mult formula-decl nil group "algebra/")
(expt_expt formula-decl nil group "algebra/")
(one_expt formula-decl nil group "algebra/")
(nonempty? const-decl "bool" sets nil)
(G!1 skolem-const-decl "finite_group[T, *, one]" groups_scaf nil)
(a!1 skolem-const-decl "(G!1)" groups_scaf nil)
(minimum? const-decl "bool" min_posnat "ints/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(empty? const-decl "bool" sets nil)
(min_def formula-decl nil min_posnat "ints/")
(NOT const-decl "[bool -> bool]" booleans nil)
(one_left formula-decl nil group "algebra/")
(^ const-decl "T" group "algebra/")
(member const-decl "bool" sets nil)
(a_hat_period formula-decl nil finite_groups "algebra/")
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(divides const-decl "bool" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(mod nonempty-type-eq-decl nil euclidean_division nil)
(period const-decl "posnat" finite_groups "algebra/")
(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)
(finite_group? const-decl "bool" group_def "algebra/")
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(finite_group nonempty-type-eq-decl nil group "algebra/")
(one formal-const-decl "T" groups_scaf nil)
(* formal-const-decl "[T, T -> T]" groups_scaf nil)
(T formal-type-decl nil groups_scaf nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
shostak))
(order_power_TCC1 0
(order_power_TCC1-1 nil 3528766942
("" (skosimp)
(("" (lemma "expt_member")
(("" (inst -1 "G!1" "a!1" "k!1") (("" (assert) nil nil)) nil))
nil))
nil)
((one formal-const-decl "T" groups_scaf nil)
(* formal-const-decl "[T, T -> T]" groups_scaf nil)
(T formal-type-decl nil groups_scaf nil)
(expt_member formula-decl nil group "algebra/")
(member const-decl "bool" sets 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)
(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))
(order_power_TCC2 0
(order_power_TCC2-1 nil 3528766942 ("" (subtype-tcc) nil nil)
((^ const-decl "T" group "algebra/")
(one formal-const-decl "T" groups_scaf nil)
(* formal-const-decl "[T, T -> T]" groups_scaf nil)
(T formal-type-decl nil groups_scaf nil)
(period const-decl "posnat" finite_groups "algebra/"))
nil))
(order_power 0
(order_power-1 nil 3528767077
("" (skosimp)
(("" (skoletin 1)
(("1" (case "(a!1^k!1)^(n / gcd(k!1, n)) = one")
(("1" (lemma "one_iff_divides")
(("1" (inst -1 "(n / gcd(k!1, n))" "G!1" "a!1^k!1")
(("1" (assert)
(("1"
(name-replace "m!1" "period(G!1, a!1 ^ k!1)" :hide?
nil)
(("1" (case "a!1^(k!1*m!1) = one")
(("1" (lemma "one_iff_divides")
(("1" (inst -1 "k!1 * m!1" "G!1" "a!1")
(("1" (assert)
(("1" (hide (-2 -5))
(("1" (replace -4 -1 rl)
(("1"
(case "divides(n/gcd(k!1, n) , (k!1/gcd(k!1, n))*m!1 )")
(("1"
(lemma "gcd_div_by_gcd")
(("1"
(inst -1 "n" "k!1")
(("1"
(expand "div_by_gcd")
(("1"
(rewrite "gcd_sym")
(("1"
(lemma "divides_rel_primes")
(("1"
(inst?)
(("1"
(assert)
(("1"
(lemma
"mutual_divisors_nat")
(("1"
(inst
-1
"n / gcd(k!1, n)"
"m!1")
(("1" (assert) nil nil)
("2"
(hide-all-but 1)
(("2"
(rewrite "gcd_sym")
(("2"
(lemma
"div_by_gcd_prep")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(rewrite "gcd_sym")
(("2"
(lemma
"div_by_gcd_prep")
(("2"
(inst -1 "n" "k!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("3"
(hide-all-but 1)
(("3"
(lemma "div_by_gcd_prep")
(("3"
(inst -1 "k!1" "n")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but (-1 1))
(("2"
(expand "divides")
(("2"
(skosimp)
(("2"
(inst 1 "x!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("3"
(hide-all-but 1)
(("3"
(lemma "div_by_gcd_prep")
(("3"
(inst -1 "k!1" "n")
(("3"
(flatten)
(("3"
(rewrite "closed_times")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-1 1))
(("2" (rewrite "expt_expt" :dir rl)
(("2" (lemma "a_hat_period")
(("2" (inst?)
(("2" (assert)
(("2" (hide (-1 2))
(("2"
(lemma "expt_member")
(("2"
(inst -1 "G!1" "a!1" "k!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (rewrite "gcd_sym")
(("2" (lemma "div_by_gcd_prep")
(("2" (inst -1 "n" "k!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (rewrite "expt_expt")
(("2" (rewrite "times_div1")
(("2" (rewrite "commutative_mult")
(("2" (rewrite "times_div1" :dir rl)
(("2" (rewrite "expt_expt" :dir rl)
(("1" (lemma "a_hat_period")
(("1" (inst?)
(("1" (assert)
(("1" (replace -2 -1 rl)
(("1" (replaces -1)
(("1"
(rewrite "one_expt")
(("1"
(hide-all-but 1)
(("1"
(lemma "div_by_gcd_prep")
(("1"
(inst -1 "k!1" "n")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (lemma "div_by_gcd_prep")
(("2" (inst -1 "k!1" "n")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide-all-but 1)
(("3" (rewrite "gcd_sym")
(("3" (lemma "div_by_gcd_prep")
(("3" (inst -1 "n" "k!1") (("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (hide (-1 -2))
(("2" (lemma "expt_member")
(("2" (inst -1 "G!1" "a!1" "k!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(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)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(T formal-type-decl nil groups_scaf nil)
(* formal-const-decl "[T, T -> T]" groups_scaf nil)
(one formal-const-decl "T" groups_scaf nil)
(finite_group nonempty-type-eq-decl nil group "algebra/")
(set type-eq-decl nil sets nil)
(finite_group? const-decl "bool" group_def "algebra/")
(period const-decl "posnat" finite_groups "algebra/")
(^ const-decl "T" group "algebra/")
(/= const-decl "boolean" notequal nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(gcd const-decl "{k: posnat | divides(k, i) AND divides(k, j)}" gcd
"ints/")
(divides const-decl "bool" divides nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(times_div1 formula-decl nil real_props nil)
(one_expt formula-decl nil group "algebra/")
(commutative_mult formula-decl nil number_fields nil)
(one_iff_divides formula-decl nil groups_scaf nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(posint nonempty-type-eq-decl nil integers nil)
(gcd_sym formula-decl nil gcd "ints/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(mutual_divisors_nat formula-decl nil divides nil)
(div_by_gcd_prep formula-decl nil gcd_fractions "ints/")
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(divides_rel_primes formula-decl nil general_properties nil)
(div_by_gcd const-decl "posint" gcd_fractions "ints/")
(gcd_div_by_gcd formula-decl nil gcd_fractions "ints/")
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(closed_times formula-decl nil integers nil)
(expt_expt formula-decl nil group "algebra/")
(group nonempty-type-eq-decl nil group "algebra/")
(group? const-decl "bool" group_def "algebra/")
(expt_member formula-decl nil group "algebra/")
(member const-decl "bool" sets nil)
(a_hat_period formula-decl nil finite_groups "algebra/")
(k!1 skolem-const-decl "posnat" groups_scaf nil)
(n skolem-const-decl "posnat" groups_scaf nil))
shostak))
(coset_power_nat_TCC1 0
(coset_power_nat_TCC1-1 nil 3530393554
("" (skosimp*) (("" (inst?) nil nil)) nil)
((group nonempty-type-eq-decl nil group "algebra/")
(group? const-decl "bool" group_def "algebra/")
(one formal-const-decl "T" groups_scaf nil)
(* formal-const-decl "[T, T -> T]" groups_scaf 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 groups_scaf nil))
nil))
(coset_power_nat_TCC2 0
(coset_power_nat_TCC2-1 nil 3530393554
("" (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]" groups_scaf nil)
(group nonempty-type-eq-decl nil group "algebra/")
(group? const-decl "bool" group_def "algebra/")
(one formal-const-decl "T" groups_scaf nil)
(* formal-const-decl "[T, T -> T]" groups_scaf nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.190 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.
|
