|
(cyclic_monoid_def
(power_TCC1 0
(power_TCC1-1 nil 3292925562 3293621498 ("" (grind) nil nil)
proved-complete
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[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)
(>= const-decl "bool" 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil))
121 110 t shostak))
(power_TCC2 0
(power_TCC2-1 nil 3292925568 3293621498 ("" (grind) nil nil)
proved-complete nil 29 30 t shostak))
(power_0 0
(power_0-1 nil 3292925609 3293638300 ("" (grind) nil nil) proved
((power def-decl "T" groups nil)) 22 20 t shostak))
(power_1 0
(power_1-1 nil 3292925615 3293638300 ("" (grind) nil nil) proved
((power def-decl "T" groups nil)
(one formal-const-decl "T" groups nil)
(* formal-const-decl "[T, T -> T]" groups nil)
(T formal-nonempty-type-decl nil groups nil)
(right_identity formula-decl nil monoids nil))
42 30 t shostak))
(one_power 0
(one_power-1 nil 3292925621 3293638300
("" (induct "n")
(("1" (grind) nil nil)
("2" (skosimp*)
(("2" (expand "power" 1) (("2" (assert) nil nil)) nil)) nil))
nil)
proved
((* formal-const-decl "[T, T -> T]" groups nil)
(left_identity formula-decl nil monoids nil)
(nat_induction formula-decl nil naturalnumbers nil)
(one formal-const-decl "T" groups nil)
(power def-decl "T" groups nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(T formal-nonempty-type-decl nil groups nil)
(pred type-eq-decl nil defined_types 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))
60 50 t shostak))
(power_def 0
(power_def-1 nil 3292925779 3293638301
("" (induct "n")
(("1" (grind) nil nil)
("2" (skosimp*)
(("2" (inst - "a!1")
(("2" (expand "power" 1)
(("2"
(lemma "cancel_left"
("z" "a!1" "x" "power(a!1, j!1 + 1)" "y"
"power(a!1, j!1) * a!1"))
(("2" (rewrite "associative") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
proved
((associative formula-decl nil monoids nil)
(cancel_left formula-decl nil groups nil)
(one formal-const-decl "T" groups nil)
(right_identity formula-decl nil monoids nil)
(left_identity formula-decl nil monoids nil)
(nat_induction formula-decl nil naturalnumbers nil)
(* formal-const-decl "[T, T -> T]" groups nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(power def-decl "T" groups nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(T formal-nonempty-type-decl nil groups nil)
(pred type-eq-decl nil defined_types 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))
385 350 t shostak))
(power_mult 0
(power_mult-1 nil 3292925654 3293638301
("" (induct "m")
(("1" (skolem!)
(("1" (rewrite "power_0") (("1" (assert) nil nil)) nil)) nil)
("2" (skosimp*)
(("2" (inst - "a!1" "n!1+1")
(("2" (rewrite "power_def" -1)
(("2" (expand "power" 1 2)
(("2" (rewrite "associative" -1) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
proved
((power_def formula-decl nil groups nil)
(associative formula-decl nil monoids nil)
(one formal-const-decl "T" groups nil)
(right_identity formula-decl nil monoids nil)
(power_0 formula-decl nil groups nil)
(nat_induction formula-decl nil naturalnumbers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(power def-decl "T" groups nil)
(* formal-const-decl "[T, T -> T]" groups nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(T formal-nonempty-type-decl nil groups nil)
(pred type-eq-decl nil defined_types 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))
514 480 t shostak))
(power_power 0
(power_power-1 nil 3292926190 3293638302
("" (induct "m")
(("1" (skolem!)
(("1" (rewrite "power_0") (("1" (rewrite "power_0") nil nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "power" 1 1)
(("2" (inst - "a!1" "n!1")
(("2" (replace -1)
(("2" (rewrite "power_mult") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
proved
((power_mult formula-decl nil groups nil)
(power_0 formula-decl nil groups nil)
(nat_induction formula-decl nil naturalnumbers nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(power def-decl "T" groups nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(T formal-nonempty-type-decl nil groups nil)
(pred type-eq-decl nil defined_types 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))
601 570 t shostak))
(power_commutes 0
(power_commutes-1 nil 3292926297 3293638302
("" (skolem!)
(("" (rewrite "power_mult") (("" (rewrite "power_mult") nil nil))
nil))
nil)
proved
((power_mult formula-decl nil groups nil)
(T formal-nonempty-type-decl nil groups 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil))
229 220 t shostak))
(inv_power 0
(inv_power-1 nil 3292926316 3293638302
("" (induct "m")
(("1" (grind) nil nil)
("2" (skosimp*)
(("2" (expand "power" 1 1)
(("2" (rewrite "inv_star")
(("2" (rewrite "power_def")
(("2" (inst - "a!1")
(("2"
(lemma "cancel_right"
("z" "inv(a!1)" "x" "inv(power(a!1, j!1))" "y"
"power(inv(a!1), j!1)"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
proved
((inv_star formula-decl nil groups nil)
(cancel_right formula-decl nil groups nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(power_def formula-decl nil groups nil)
(inv_one formula-decl nil groups nil)
(nat_induction formula-decl nil naturalnumbers nil)
(power def-decl "T" groups nil)
(inv const-decl "{y | x * y = one AND y * x = one}" groups nil)
(one formal-const-decl "T" groups nil)
(* formal-const-decl "[T, T -> T]" groups nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(T formal-nonempty-type-decl nil groups nil)
(pred type-eq-decl nil defined_types 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))
412 410 t shostak))
(power_inv_right 0
(power_inv_right-1 nil 3292926510 3293638302
("" (skolem!)
(("" (rewrite "inv_power" :dir rl) (("" (assert) nil nil))
nil))
nil)
proved
((inv_power formula-decl nil groups nil)
(T formal-nonempty-type-decl nil groups 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(inv_right formula-decl nil groups nil))
46 50 t shostak))
(power_inv_left 0
(power_inv_left-1 nil 3292926554 3293638303
("" (skolem!)
(("" (rewrite "inv_power" :dir rl) (("" (assert) nil nil))
nil))
nil)
proved
((inv_power formula-decl nil groups nil)
(T formal-nonempty-type-decl nil groups 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(inv_left formula-decl nil groups nil))
39 40 t shostak))
(cyclic_group_is_abelian 0
(cyclic_group_is_abelian-1 nil 3293272131 3293621505
("" (skolem 1 ("G!1"))
(("" (typepred "G!1")
(("" (expand "cyclic_group?")
(("" (flatten)
(("" (expand "abelian_group?")
(("" (assert)
(("" (expand "cyclic?")
(("" (skolem!)
(("" (replace -1 -2)
(("" (expand "commutative_over?")
(("" (skosimp*)
(("" (replace -1)
(("" (assert)
(("" (expand "generated_by")
((""
(skosimp*)
((""
(lemma
"expt_mult"
("a" "a!1" "i" "i!1" "j" "i!2"))
((""
(lemma
"expt_mult"
("a" "a!1" "i" "i!2" "j" "i!1"))
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
proved-incomplete
((cyclic_group nonempty-type-eq-decl nil groups nil)
(cyclic_group? const-decl "bool" groups nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil groups nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(commutative_over? const-decl "bool" operator_defs_more nil)
(generated_by const-decl "group" groups 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)
(expt_mult formula-decl nil groups nil)
(member const-decl "bool" sets nil)
(cyclic? const-decl "bool" groups nil)
(abelian_group? const-decl "bool" groups_def nil))
290 250 t shostak)))
¤ Dauer der Verarbeitung: 0.16 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.
|
