|
(group
(IMP_monoid_TCC1 0
(IMP_monoid_TCC1-1 nil 3292762238
("" (lemma "fullset_is_group")
(("" (expand "group?") (("" (flatten) nil nil)) nil)) nil)
((group? const-decl "bool" group_def nil)
(fullset_is_group formula-decl nil group nil))
nil))
(group_TCC1 0
(group_TCC1-1 nil 3292762313
("" (lemma "fullset_is_group") (("" (propax) nil nil)) nil)
((fullset_is_group formula-decl nil group nil)) shostak))
(group_is_monoid 0
(group_is_monoid-1 nil 3292762890
("" (skolem!)
(("" (typepred "x!1")
(("" (expand "group?") (("" (flatten) nil nil)) nil)) nil))
nil)
((group nonempty-type-eq-decl nil group nil)
(group? const-decl "bool" group_def nil)
(one formal-const-decl "T" group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil group nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(finite_group_TCC1 0
(finite_group_TCC1-1 nil 3407081197
("" (inst + "singleton[T](one)")
(("" (grind)
(("1" (rewrite "left_identity") nil nil)
("2" (rewrite "associative") nil nil)
("3" (rewrite "left_identity") nil nil)
("4" (rewrite "left_identity") nil nil)
("5" (rewrite "left_identity") nil nil))
nil))
nil)
((group? const-decl "bool" group_def nil)
(inv_exists? const-decl "bool" group_def nil)
(monoid? const-decl "bool" monoid_def nil)
(associative? const-decl "bool" operator_defs nil)
(monad? const-decl "bool" monad_def nil)
(identity? const-decl "bool" operator_defs nil)
(left_identity formula-decl nil monad nil)
(restrict const-decl "R" restrict nil)
(right_identity formula-decl nil monad nil)
(star_closed? const-decl "bool" groupoid_def nil)
(member const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(singleton const-decl "(singleton?)" sets nil)
(singleton? const-decl "bool" sets nil)
(finite_group? const-decl "bool" group_def nil)
(one formal-const-decl "T" group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-nonempty-type-decl nil group nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set" finite_sets nil))
nil))
(finite_group_is_group 0
(finite_group_is_group-1 nil 3407081197 ("" (judgement-tcc) nil nil)
((finite_group nonempty-type-eq-decl nil group nil)
(finite_group? const-decl "bool" group_def nil)
(set type-eq-decl nil sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(is_finite const-decl "bool" finite_sets nil)
(injective? const-decl "bool" functions nil)
(member const-decl "bool" sets nil)
(star_closed? const-decl "bool" groupoid_def nil)
(one formal-const-decl "T" group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(T formal-nonempty-type-decl nil group nil)
(right_identity formula-decl nil monad nil)
(restrict const-decl "R" restrict nil)
(left_identity formula-decl nil monad nil)
(identity? const-decl "bool" operator_defs nil)
(monad? const-decl "bool" monad_def nil)
(associative? const-decl "bool" operator_defs nil)
(monoid? const-decl "bool" monoid_def nil)
(inv_exists? const-decl "bool" group_def nil)
(group? const-decl "bool" group_def nil))
nil))
(finite_group_is_finite_monoid 0
(finite_group_is_finite_monoid-1 nil 3407081197
("" (judgement-tcc) nil nil)
((finite_group nonempty-type-eq-decl nil group nil)
(finite_group? const-decl "bool" group_def nil)
(set type-eq-decl nil sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(group? const-decl "bool" group_def nil)
(inv_exists? const-decl "bool" group_def nil)
(member const-decl "bool" sets nil)
(star_closed? const-decl "bool" groupoid_def nil)
(one formal-const-decl "T" group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(T formal-nonempty-type-decl nil group nil)
(right_identity formula-decl nil monad nil)
(restrict const-decl "R" restrict nil)
(left_identity formula-decl nil monad nil)
(identity? const-decl "bool" operator_defs nil)
(monad? const-decl "bool" monad_def nil)
(associative? const-decl "bool" operator_defs nil)
(monoid? const-decl "bool" monoid_def nil)
(injective? const-decl "bool" functions nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_monoid? const-decl "bool" monoid_def nil))
nil))
(finite_subgroups 0
(finite_subgroups-1 nil 3407081210
("" (skosimp)
(("" (typepred "H!1")
(("" (expand "finite_group?")
(("" (expand "subgroup?")
(("" (flatten)
(("" (assert)
(("" (lemma "finite_subset" ("s" "S!1" "A" "H!1"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((finite_group nonempty-type-eq-decl nil group nil)
(finite_group? const-decl "bool" group_def nil)
(one formal-const-decl "T" group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil group nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(subgroup? const-decl "bool" group_def nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(finite_subset formula-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil))
nil))
(one_is_group 0
(one_is_group-1 nil 3426244215
("" (assert)
(("" (expand "group?")
(("" (assert)
(("" (expand "singleton")
(("" (expand "inv_exists?")
(("" (skosimp*)
(("" (typepred "x!1")
(("" (replace -1)
(("" (inst + "one") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((group? const-decl "bool" group_def nil)
(singleton const-decl "(singleton?)" sets nil)
(right_identity formula-decl nil monad nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(inv_exists? const-decl "bool" group_def nil)
(one formal-const-decl "T" group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(T formal-nonempty-type-decl nil group nil)
(one_is_monoid formula-decl nil monoid nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set" finite_sets nil))
shostak))
(one_finite_group 0
(one_finite_group-1 nil 3426244072
("" (expand "finite_group?") (("" (assert) nil nil)) nil)
((one_is_group formula-decl nil group nil)
(finite_group? const-decl "bool" group_def nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set" finite_sets nil))
shostak))
(one_group_TCC1 0
(one_group_TCC1-1 nil 3407147541
("" (expand "finite_group?")
(("" (expand "group?")
(("" (prop)
(("1" (grind) nil nil)
("2" (expand "inv_exists?")
(("2" (skosimp*)
(("2" (inst + "one")
(("1" (typepred "x!1")
(("1" (rewrite "left_identity")
(("1" (rewrite "right_identity")
(("1" (grind) nil nil)) nil))
nil))
nil)
("2" (expand "singleton") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((group? const-decl "bool" group_def nil)
(inv_exists? const-decl "bool" group_def nil)
(monoid? const-decl "bool" monoid_def nil)
(associative? const-decl "bool" operator_defs nil)
(monad? const-decl "bool" monad_def nil)
(identity? const-decl "bool" operator_defs nil)
(left_identity formula-decl nil monad nil)
(restrict const-decl "R" restrict nil)
(right_identity formula-decl nil monad nil)
(T formal-nonempty-type-decl nil group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(one formal-const-decl "T" group nil)
(star_closed? const-decl "bool" groupoid_def nil)
(member const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(singleton? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(finite_group? const-decl "bool" group_def nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set" finite_sets nil))
nil))
(group_card_gt_0_TCC1 0
(group_card_gt_0_TCC1-1 nil 3407148284 ("" (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-nonempty-type-decl nil group nil)
(set type-eq-decl nil sets nil)
(* formal-const-decl "[T, T -> T]" group nil)
(one formal-const-decl "T" group nil)
(finite_group? const-decl "bool" group_def nil)
(finite_group nonempty-type-eq-decl nil group nil)
(member const-decl "bool" sets nil)
(star_closed? const-decl "bool" groupoid_def nil)
(right_identity formula-decl nil monad nil)
(restrict const-decl "R" restrict nil)
(left_identity formula-decl nil monad nil)
(identity? const-decl "bool" operator_defs nil)
(monad? const-decl "bool" monad_def nil)
(associative? const-decl "bool" operator_defs nil)
(monoid? const-decl "bool" monoid_def nil)
(inv_exists? const-decl "bool" group_def nil)
(group? const-decl "bool" group_def nil)
(injective? const-decl "bool" functions nil)
(is_finite const-decl "bool" finite_sets nil))
nil))
(group_card_gt_0 0
(group_card_gt_0-1 nil 3407148289
("" (skosimp*)
(("" (lemma "one_in")
(("" (inst?)
(("" (lemma "nonempty_card[T]")
(("" (inst?)
(("" (assert)
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((one formal-const-decl "T" group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(T formal-nonempty-type-decl nil group nil)
(one_in formula-decl nil monad nil)
(nonempty_card formula-decl nil finite_sets nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(finite_group nonempty-type-eq-decl nil group nil)
(finite_group? const-decl "bool" group_def nil)
(monad nonempty-type-eq-decl nil monad nil)
(monad? const-decl "bool" monad_def nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(inv_exists 0
(inv_exists-1 nil 3292850790
("" (skosimp*)
(("" (lemma "fullset_is_group")
(("" (expand "group?")
(("" (expand "inv_exists?")
(("" (flatten)
(("" (inst - "x!1")
(("1" (skolem!) (("1" (inst + "y!1") nil nil)) nil)
("2" (expand "fullset") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((fullset_is_group formula-decl nil group nil)
(inv_exists? const-decl "bool" group_def nil)
(x!1 skolem-const-decl "T" group nil)
(fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-nonempty-type-decl nil group nil)
(group? const-decl "bool" group_def nil))
shostak))
(inv_TCC1 0
(inv_TCC1-2 nil 3406566424
(""
(inst +
"(lambda (x:T): choose({y: T | x * y = one AND y * x = one}))")
(("" (lemma "fullset_is_group")
(("" (expand "group?")
(("" (flatten)
(("" (expand "inv_exists?")
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (expand "member")
(("" (skosimp*)
(("" (inst -2 "x!1")
(("1" (skolem!) (("1" (inst - "y!1") nil nil))
nil)
("2" (expand "fullset") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((fullset_is_group formula-decl nil group nil)
(member const-decl "bool" sets nil)
(fullset const-decl "set" sets nil)
(x!1 skolem-const-decl "T" group nil)
(empty? const-decl "bool" sets nil)
(inv_exists? const-decl "bool" group_def nil)
(group? const-decl "bool" group_def nil)
(choose const-decl "(p)" sets nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(one formal-const-decl "T" group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(= 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)
(T formal-nonempty-type-decl nil group nil))
nil)
(inv_TCC1-1 nil 3406566388 ("" (existence-tcc) nil nil) nil nil))
(inv_left 0
(inv_left-1 nil 3292762906
("" (skosimp*)
(("" (typepred "inv(x!1)") (("" (propax) nil nil)) nil)) nil)
((inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(one formal-const-decl "T" group nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(* formal-const-decl "[T, T -> T]" group nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(T formal-nonempty-type-decl nil group nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(inv_right 0
(inv_right-1 nil 3292762947
("" (skosimp*)
(("" (typepred "inv(x!1)") (("" (propax) nil nil)) nil)) nil)
((inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(one formal-const-decl "T" group nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(* formal-const-decl "[T, T -> T]" group nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(T formal-nonempty-type-decl nil group nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(cancel_right 0
(cancel_right-1 nil 3292842800
("" (lemma "fullset_is_group")
(("" (expand "group?")
(("" (expand "inv_exists?")
(("" (skosimp*)
(("" (inst -2 "z!1")
(("1" (skosimp*)
(("1" (expand "monoid?")
(("1" (flatten)
(("1" (expand "associative?")
(("1" (inst-cp - "x!1" "z!1" "y!2")
(("1" (inst - "y!1" "z!1" "y!2")
(("1" (hide -1)
(("1" (grind)
(("1" (rewrite "right_identity")
(("1"
(rewrite "right_identity")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (expand "fullset")
(("2" (propax) nil nil)) nil)
("3" (expand "fullset")
(("3" (propax) nil nil)) nil))
nil)
("2" (expand "fullset") (("2" (propax) nil nil))
nil)
("3" (expand "fullset") (("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "fullset") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((group? const-decl "bool" group_def nil)
(x!1 skolem-const-decl "T" group nil)
(restrict const-decl "R" restrict nil)
(one formal-const-decl "T" group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(right_identity formula-decl nil monad nil)
(y!1 skolem-const-decl "T" group nil)
(associative? const-decl "bool" operator_defs nil)
(monoid? const-decl "bool" monoid_def nil)
(T formal-nonempty-type-decl nil group nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil)
(z!1 skolem-const-decl "T" group nil)
(inv_exists? const-decl "bool" group_def nil)
(fullset_is_group formula-decl nil group nil))
shostak))
(cancel_left 0
(cancel_left-1 nil 3292843123
("" (skosimp)
(("" (prop)
(("1" (lemma "inv_exists" ("x" "z!1"))
(("1" (skolem -1 ("z1"))
(("1" (flatten)
(("1" (lemma "associative" ("x" "z1" "y" "z!1" "z" "x!1"))
(("1"
(lemma "associative" ("x" "z1" "y" "z!1" "z" "y!1"))
(("1" (replace -4)
(("1" (rewrite "left_identity")
(("1" (rewrite "left_identity")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
((* formal-const-decl "[T, T -> T]" group nil)
(associative formula-decl nil semigroup nil)
(one formal-const-decl "T" group nil)
(left_identity formula-decl nil monad nil)
(inv_exists formula-decl nil group nil)
(T formal-nonempty-type-decl nil group nil))
shostak))
(inv_inv 0
(inv_inv-1 nil 3292762959
("" (skosimp)
((""
(lemma "cancel_right"
("x" "inv(inv(x!1))" "y" "x!1" "z" "inv(x!1)"))
(("" (rewrite "inv_right")
(("" (rewrite "inv_left") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(one formal-const-decl "T" group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(= 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)
(T formal-nonempty-type-decl nil group nil)
(cancel_right formula-decl nil group nil)
(inv_left formula-decl nil group nil)
(inv_right formula-decl nil group nil))
shostak))
(cancel_right_inv 0
(cancel_right_inv-1 nil 3293635913
("" (skosimp)
((""
(lemma "cancel_right"
("x" "x!1*inv(z!1)" "y" "y!1*inv(z!1)" "z" "z!1"))
(("" (rewrite "associative" -1)
(("" (rewrite "associative" -1)
(("" (rewrite "inv_left")
(("" (rewrite "right_identity")
(("" (rewrite "right_identity")
(("" (flatten) (("" (prop) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(one formal-const-decl "T" group nil)
(= 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)
(* formal-const-decl "[T, T -> T]" group nil)
(T formal-nonempty-type-decl nil group nil)
(cancel_right formula-decl nil group nil)
(right_identity formula-decl nil monad nil)
(inv_left formula-decl nil group nil)
(associative formula-decl nil semigroup nil))
shostak))
(cancel_left_inv 0
(cancel_left_inv-1 nil 3293636093
("" (skosimp*)
((""
(lemma "cancel_left"
("z" "inv(z!1)" "x" "z!1 * inv(x!1)" "y" "z!1 * inv(y!1)"))
(("" (rewrite "associative" -1 :dir rl)
(("" (rewrite "associative" -1 :dir rl)
(("" (rewrite "inv_left")
(("" (replace -1 1 rl)
(("" (hide -1)
(("" (prop)
(("1"
(lemma "cancel_right_inv"
("z" "inv(x!1)" "x" "inv(x!1)" "y" "inv(y!1)"))
(("1" (rewrite "inv_inv" -1)
(("1" (rewrite "inv_left" -1)
(("1" (flatten)
(("1" (assert)
(("1"
(lemma "cancel_left"
("z"
"y!1"
"x"
"one"
"y"
"inv(y!1) * x!1"))
(("1"
(rewrite "associative" -1 :dir rl)
(("1"
(rewrite "inv_right")
(("1"
(rewrite "right_identity")
(("1"
(rewrite "left_identity")
(("1"
(rewrite "left_identity")
(("1"
(rewrite "left_identity")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(one formal-const-decl "T" group nil)
(= 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)
(* formal-const-decl "[T, T -> T]" group nil)
(T formal-nonempty-type-decl nil group nil)
(cancel_left formula-decl nil group nil)
(inv_inv formula-decl nil group nil)
(inv_right formula-decl nil group nil)
(right_identity formula-decl nil monad nil)
(left_identity formula-decl nil monad nil)
(cancel_right_inv formula-decl nil group nil)
(inv_left formula-decl nil group nil)
(associative formula-decl nil semigroup nil))
shostak))
(inv_one 0
(inv_one-1 nil 3292764489
("" (lemma "cancel_right" ("x" "inv(one)" "y" "one" "z" "one"))
(("" (rewrite "inv_left")
(("" (assert) (("" (rewrite "left_identity") nil nil)) nil))
nil))
nil)
((inv_left formula-decl nil group nil)
(right_identity formula-decl nil monad nil)
(cancel_right formula-decl nil group nil)
(T formal-nonempty-type-decl nil group nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(* formal-const-decl "[T, T -> T]" group nil)
(one formal-const-decl "T" group nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group nil))
shostak))
(inv_star 0
(inv_star-1 nil 3292872970
("" (skosimp*)
((""
(lemma "cancel_right"
("x" "inv(x!1 * y!1)" "y" "inv(y!1) * inv(x!1)" "z" "x!1*y!1"))
(("" (rewrite "inv_left")
(("" (lemma "associative")
(("" (inst-cp - "inv(y!1)" "inv(x!1)" "x!1 * y!1")
(("" (inst - "inv(x!1)" "x!1" "y!1")
(("" (rewrite "inv_left")
(("" (assert)
(("" (rewrite "left_identity")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(one formal-const-decl "T" group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(= 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)
(T formal-nonempty-type-decl nil group nil)
(cancel_right formula-decl nil group nil)
(associative formula-decl nil semigroup nil)
(left_identity formula-decl nil monad nil)
(inv_left formula-decl nil group nil))
shostak))
(unique_inv 0
(unique_inv-1 nil 3292764765
("" (skolem!)
(("" (prop)
(("1"
(lemma "cancel_right" ("z" "inv(x!1)" "x" "y!1*x!1" "y" "one"))
(("1" (rewrite "associative")
(("1" (assert)
(("1" (rewrite "inv_right")
(("1" (rewrite "left_identity")
(("1" (rewrite "right_identity") nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (replace -1) (("2" (rewrite "inv_right") nil nil)) nil)
("3" (replace -1) (("3" (rewrite "inv_left") nil nil)) nil))
nil))
nil)
((associative formula-decl nil semigroup nil)
(inv_right formula-decl nil group nil)
(right_identity formula-decl nil monad nil)
(left_identity formula-decl nil monad nil)
(cancel_right formula-decl nil group nil)
(T formal-nonempty-type-decl nil group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(one formal-const-decl "T" group nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(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 nil)
(inv_left formula-decl nil group nil))
shostak))
(inv_member 0
(inv_member-1 nil 3293283133
("" (skosimp*)
(("" (typepred "G!1")
(("" (expand "group?")
(("" (flatten)
(("" (expand "inv_exists?")
(("" (assert)
(("" (prop)
(("1" (inst - "inv(x!1)")
(("1" (skolem!)
(("1" (typepred "y!1")
(("1"
(lemma "unique_inv" ("x" "inv(x!1)" "y" "y!1"))
(("1" (replace -5 -1)
(("1" (simplify -1)
(("1" (rewrite "inv_inv")
(("1"
(assert)
(("1"
(expand "member")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "member") (("2" (propax) nil nil))
nil))
nil)
("2" (inst - "x!1")
(("1" (skolem!)
(("1" (typepred "y!1")
(("1" (lemma "unique_inv" ("x" "x!1" "y" "y!1"))
(("1" (replace -5 -1)
(("1" (simplify -1)
(("1" (assert)
(("1"
(expand "member")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "member") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((group nonempty-type-eq-decl nil group nil)
(group? const-decl "bool" group_def nil)
(one formal-const-decl "T" group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil group 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)
(x!1 skolem-const-decl "T" group nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(G!1 skolem-const-decl "group" group nil)
(inv_inv formula-decl nil group nil)
(unique_inv formula-decl nil group nil)
(inv_exists? const-decl "bool" group_def nil))
shostak))
(inv_in 0
(inv_in-1 nil 3397482079
("" (skosimp*)
(("" (lemma "inv_member")
(("" (inst?)
(("" (inst?)
(("" (assert)
(("" (prop)
(("1" (assert)
(("1" (expand "member") (("1" (propax) nil nil)) nil))
nil)
("2" (expand "member") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((inv_member formula-decl nil group nil)
(member const-decl "bool" sets nil)
(group nonempty-type-eq-decl nil group nil)
(group? const-decl "bool" group_def nil)
(one formal-const-decl "T" group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-nonempty-type-decl nil group nil))
shostak))
(divby 0
(divby-1 nil 3406394234
("" (skosimp*)
(("" (prop)
(("1" (replace -1)
(("1" (rewrite "associative" :dir rl)
(("1" (rewrite "inv_left")
(("1" (rewrite "left_identity") nil nil)) nil))
nil))
nil)
("2" (replace - + rl)
(("2" (hide -1)
(("2" (rewrite "associative" :dir rl)
(("2" (rewrite "inv_right")
(("2" (rewrite "left_identity") nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((associative formula-decl nil semigroup nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(one formal-const-decl "T" group nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(T formal-nonempty-type-decl nil group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(left_identity formula-decl nil monad nil)
(inv_left formula-decl nil group nil)
(inv_right formula-decl nil group nil))
shostak))
(product_in 0
(product_in-1 nil 3460720535
("" (skeep)
(("" (typepred "G")
(("" (expand "group?")
(("" (flatten)
(("" (expand "monoid?")
(("" (flatten)
(("" (expand "monad?")
(("" (flatten)
(("" (expand "star_closed?")
(("" (assert) (("" (inst?) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((group nonempty-type-eq-decl nil group nil)
(group? const-decl "bool" group_def nil)
(one formal-const-decl "T" group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil group 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)
(star_closed? const-decl "bool" groupoid_def nil)
(monad? const-decl "bool" monad_def nil)
(monoid? const-decl "bool" monoid_def nil))
nil))
(one_is_subgroup 0
(one_is_subgroup-1 nil 3293048889
("" (skosimp)
(("" (expand "subgroup?")
(("" (lemma "one_member" ("M" "G!1"))
(("" (expand "member")
(("" (grind)
(("1" (rewrite "left_identity") nil nil)
("2" (rewrite "associative") nil nil)
("3" (rewrite "left_identity") nil nil)
("4" (rewrite "left_identity") nil nil)
("5" (rewrite "left_identity") nil nil))
nil))
nil))
nil))
nil))
nil)
((subgroup? const-decl "bool" group_def nil)
(member const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(subset? const-decl "bool" sets nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set" finite_sets nil)
(inv_exists? const-decl "bool" group_def nil)
(monoid? const-decl "bool" monoid_def nil)
(associative? const-decl "bool" operator_defs nil)
(identity? const-decl "bool" operator_defs nil)
(left_identity formula-decl nil monad nil)
(restrict const-decl "R" restrict nil)
(right_identity formula-decl nil monad nil)
(star_closed? const-decl "bool" groupoid_def nil)
(singleton const-decl "(singleton?)" sets nil)
(one_group const-decl "finite_group" group nil)
(singleton? const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(one_member formula-decl nil monad nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(monad? const-decl "bool" monad_def nil)
(monad nonempty-type-eq-decl nil monad nil)
(group? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil)
(T formal-nonempty-type-decl nil group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(one formal-const-decl "T" group nil))
shostak))
(group_is_subgroup 0
(group_is_subgroup-1 nil 3293049089
("" (skosimp*)
(("" (expand "subgroup?")
(("" (expand "subset?") (("" (grind) nil nil)) nil)) nil))
nil)
((subgroup? const-decl "bool" group_def nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil))
shostak))
(subgroup_is_group 0
(subgroup_is_group-1 nil 3293216084
("" (skosimp*)
(("" (expand "subgroup?") (("" (flatten) nil nil)) nil)) nil)
((subgroup? const-decl "bool" group_def nil)) shostak))
(subgroup_def 0
(subgroup_def-1 nil 3292939771
("" (skosimp)
(("" (typepred "G!1")
(("" (expand "subgroup?")
(("" (expand "group?")
(("" (expand "monoid?")
(("" (flatten)
(("" (assert)
(("" (prop)
(("1" (expand "nonempty?")
(("1" (expand "empty?")
(("1" (inst - "one")
(("1" (expand "monad?")
(("1" (flatten) nil nil)) nil))
nil))
nil))
nil)
("2" (expand "monad?")
(("2" (expand "groupoid?")
(("2" (flatten) nil nil)) nil))
nil)
("3" (expand "inv_closed?")
(("3" (skosimp)
(("3" (lemma "inv_member" ("x" "x!1" "G" "S!1"))
(("1" (expand "member")
(("1" (propax) nil nil)) nil)
("2" (expand "group?")
(("2" (expand "monoid?")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("4" (expand "monad?")
(("4" (expand "groupoid?")
(("4" (flatten)
(("4" (assert)
(("4" (expand "inv_closed?")
(("4" (expand "star_closed?")
(("4"
(expand "member")
(("4"
(expand "nonempty?")
(("4"
(expand "empty?")
(("4"
(skosimp)
(("4"
(expand "member")
(("4"
(inst - "x!1")
(("4"
(inst - "x!1" "inv(x!1)")
(("4"
(rewrite "inv_right")
(("4"
(assert)
(("4"
(expand "restrict")
(("4"
(expand
"identity?")
(("4"
(skosimp)
(("4"
(inst -7 "x!2")
(("4"
(expand
"subset?")
(("4"
(inst
-2
"x!2")
(("4"
(expand
"member")
(("4"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("5" (expand "inv_exists?")
(("5" (expand "inv_closed?")
(("5" (expand "member")
(("5" (expand "associative?")
(("5" (expand "restrict")
(("5" (skosimp*)
(("5"
(inst -6 "x!1" "y!1" "z!1")
(("1"
(expand "subset?")
(("1"
(expand "member")
(("1"
(inst -2 "z!1")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(expand "subset?")
(("2"
(expand "member")
(("2"
(inst -2 "y!1")
(("2" (assert) nil nil))
nil))
nil))
nil)
("3"
(expand "subset?")
(("3"
(inst -2 "x!1")
(("3"
(expand "member")
(("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("6" (expand "inv_exists?")
(("6" (skosimp*)
(("6" (inst - "x!1")
(("1" (typepred "x!1")
(("1" (expand "subset?")
(("1" (expand "member")
(("1"
(inst-cp -3 "x!1")
(("1"
(assert)
(("1"
(skosimp*)
(("1"
(expand "inv_closed?")
(("1"
(inst -6 "x!1")
(("1"
(expand "member")
(("1"
(lemma
"unique_inv"
("x" "x!1" "y" "y!1"))
(("1"
(assert)
(("1"
(replace -1 * rl)
(("1"
(inst + "y!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "x!1")
(("2" (expand "subset?")
(("2" (expand "member")
(("2"
(inst - "x!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((group nonempty-type-eq-decl nil group nil)
(group? const-decl "bool" group_def nil)
(one formal-const-decl "T" group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil group nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(empty? const-decl "bool" sets nil)
(monad? const-decl "bool" monad_def nil)
(nonempty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(inv_member formula-decl nil group nil)
(inv_closed? const-decl "bool" group nil)
(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 nil)
(identity? const-decl "bool" operator_defs nil)
(G!1 skolem-const-decl "group" group nil)
(x!2 skolem-const-decl "(S!1)" group nil)
(subset? const-decl "bool" sets nil)
(restrict const-decl "R" restrict nil)
(inv_right formula-decl nil group nil)
(x!1 skolem-const-decl "T" group nil)
(S!1 skolem-const-decl "set[T]" group nil)
(star_closed? const-decl "bool" groupoid_def nil)
(associative? const-decl "bool" operator_defs nil)
(z!1 skolem-const-decl "(S!1)" group nil)
(y!1 skolem-const-decl "(S!1)" group nil)
(x!1 skolem-const-decl "(S!1)" group nil)
(inv_exists? const-decl "bool" group_def nil)
(unique_inv formula-decl nil group nil)
(x!1 skolem-const-decl "(S!1)" group nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(monoid? const-decl "bool" monoid_def nil)
(subgroup? const-decl "bool" group_def nil))
shostak))
(inv_power 0
(inv_power-1 nil 3296998229
("" (induct "m")
(("1" (grind) (("1" (rewrite "inv_one") nil 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)
((inv_star formula-decl nil group nil)
(cancel_right formula-decl nil group nil)
(odd_plus_odd_is_even application-judgement "even_int" integers
nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(power_def formula-decl nil monoid nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(inv_one formula-decl nil group nil)
(nat_induction formula-decl nil naturalnumbers nil)
(power def-decl "T" monoid_def nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(one formal-const-decl "T" group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(T formal-nonempty-type-decl nil group 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))
shostak))
(power_inv_right 0
(power_inv_right-1 nil 3296998338
("" (skolem!)
(("" (rewrite "inv_power" :dir rl)
(("" (rewrite "inv_right") nil nil)) nil))
nil)
((inv_power formula-decl nil group nil)
(T formal-nonempty-type-decl nil group 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)
(power def-decl "T" monoid_def nil)
(one formal-const-decl "T" group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(inv_right formula-decl nil group nil))
shostak))
(power_inv_left 0
(power_inv_left-1 nil 3296998389
("" (skosimp)
(("" (rewrite "inv_power" :dir rl)
(("" (rewrite "inv_left") nil nil)) nil))
nil)
((inv_power formula-decl nil group nil)
(T formal-nonempty-type-decl nil group 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)
(power def-decl "T" monoid_def nil)
(one formal-const-decl "T" group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(inv_left formula-decl nil group nil))
shostak))
(caret_TCC1 0
(caret_TCC1-1 nil 3292925575 ("" (grind) nil nil)
((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)
(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)
(minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(caret_TCC2 0
(caret_TCC2-1 nil 3292925585 ("" (grind) nil nil)
((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)
(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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(expt_0 0
(expt_0-1 nil 3292926615 ("" (grind) nil nil)
((one formal-const-decl "T" group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(T formal-nonempty-type-decl nil group nil)
(power def-decl "T" monoid_def nil) (^ const-decl "T" group nil))
shostak))
(expt_1 0
(expt_1-1 nil 3292926621
("" (grind) (("" (rewrite "right_identity") nil nil)) nil)
((one formal-const-decl "T" group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(T formal-nonempty-type-decl nil group nil)
(power def-decl "T" monoid_def nil)
(right_identity formula-decl nil monad nil)
(^ const-decl "T" group nil))
shostak))
(expt_m1 0
(expt_m1-1 nil 3292939182
("" (grind) (("" (rewrite "right_identity") nil nil)) nil)
((one formal-const-decl "T" group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(T formal-nonempty-type-decl nil group nil)
(power def-decl "T" monoid_def nil)
(right_identity formula-decl nil monad nil)
(^ const-decl "T" group nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil))
shostak))
(one_expt 0
(one_expt-1 nil 3292926628
("" (expand "^")
(("" (skolem!)
(("" (case-replace "i!1<0")
(("1" (assert)
(("1" (rewrite "inv_one")
(("1" (rewrite "one_power") nil nil)) nil))
nil)
("2" (rewrite "one_power") (("2" (assert) nil nil)) nil))
nil))
nil))
nil)
((>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(inv_one formula-decl nil group nil)
(one formal-const-decl "T" group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(T formal-nonempty-type-decl nil group nil)
(one_power formula-decl nil monoid nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_int_is_int application-judgement "int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(< const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(^ const-decl "T" group nil))
shostak))
(expt_neg 0
(expt_neg-1 nil 3292927766
("" (expand "^")
(("" (skolem!)
(("" (lemma "trichotomy" ("x" "i!1"))
(("" (split -1)
(("1" (assert) nil nil)
("2" (rewrite -1)
(("2" (assert)
(("2" (rewrite "power_0")
(("2" (rewrite "power_0") nil nil)) nil))
nil))
nil)
("3" (assert) (("3" (rewrite "inv_inv") nil nil)) nil))
nil))
nil))
nil))
nil)
((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)
(minus_int_is_int application-judgement "int" integers nil)
(one formal-const-decl "T" group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(T formal-nonempty-type-decl nil group nil)
(power_0 formula-decl nil monoid nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(inv_inv formula-decl nil group nil)
(trichotomy formula-decl nil real_axioms 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)
(^ const-decl "T" group nil))
shostak))
(inv_expt 0
(inv_expt-1 nil 3292927863
("" (skolem!)
(("" (expand "^")
(("" (case-replace "i!1<0")
(("1" (rewrite "inv_power") nil nil)
("2" (assert) (("2" (rewrite "inv_power") nil nil)) nil))
nil))
nil))
nil)
((^ const-decl "T" group nil)
(real_lt_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)
(minus_int_is_int application-judgement "int" integers nil)
(inv_power formula-decl nil group nil)
(T formal-nonempty-type-decl nil group nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(* formal-const-decl "[T, T -> T]" group nil)
(one formal-const-decl "T" group nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields 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)
(< const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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))
(expt_def1 0
(expt_def1-1 nil 3292927937
("" (skolem!)
(("" (expand "^")
(("" (case "i!1<-1")
(("1" (assert)
(("1" (lemma "power_def" ("a" "inv(a!1)" "n" "-(1 + i!1)"))
(("1"
(lemma "cancel_right"
("z" "a!1" "x" "power(inv(a!1), -(1 + i!1) + 1)" "y"
"power(inv(a!1), -(1 + i!1)) * inv(a!1)"))
(("1" (rewrite "associative" -1)
(("1" (assert)
(("1" (rewrite "inv_left")
(("1" (rewrite "right_identity")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (case-replace "i!1=-1")
(("1" (grind)
(("1" (rewrite "right_identity")
(("1" (rewrite "inv_left") nil nil)) nil))
nil)
("2" (case-replace "i!1=0")
(("1" (grind)
(("1" (rewrite "right_identity")
(("1" (rewrite "left_identity") nil nil)) nil))
nil)
("2" (assert) (("2" (rewrite "power_def") nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((^ const-decl "T" group nil)
(odd_plus_odd_is_even application-judgement "even_int" integers
nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(left_identity formula-decl nil monad nil)
(odd_plus_even_is_odd application-judgement "odd_int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(minus_int_is_int application-judgement "int" integers nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(cancel_right formula-decl nil group nil)
(power def-decl "T" monoid_def nil)
(right_identity formula-decl nil monad nil)
(inv_left formula-decl nil group nil)
(associative formula-decl nil semigroup nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(power_def formula-decl nil monoid nil)
(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 nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(T formal-nonempty-type-decl nil group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(one formal-const-decl "T" group nil)
(minus_odd_is_odd application-judgement "odd_int" integers 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)
(bool nonempty-type-eq-decl nil booleans 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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil))
shostak))
(expt_def2 0
(expt_def2-1 nil 3292933650
("" (skosimp*)
(("" (expand "^")
(("" (case "i!1<-1")
(("1" (assert)
(("1" (expand "power" 1 2)
(("1" (rewrite "associative" :dir rl)
(("1" (assert)
(("1" (rewrite "inv_right")
(("1" (rewrite "left_identity")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.55 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.
|
