| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/algebra/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 117 kB |
|
Quelle group.prfSprache: Lisp |
|||||||||||||||
|
(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) ("2" (case-replace "i!1=-1") (("1" (grind) (("1" (rewrite "right_identity") (("1" (rewrite "inv_right") nil nil)) nil)) nil) ("2" (assert) (("2" (expand "power" 3 1) (("2" (propax) 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) (right_identity formula-decl nil monad 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (associative formula-decl nil semigroup 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) (>= 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) (inv_right formula-decl nil group nil) (left_identity formula-decl nil monad nil) (power def-decl "T" monoid_def 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_mult 0 (expt_mult-1 nil 3292926712 ("" (skolem!) (("" (case "FORALL (a:T,i:int,n:nat): a^i*a^n = a^(i+n) & a^n*a^i=a^(i+n)") (("1" (case "j!1 < 0") (("1" (case "i!1 < 0") (("1" (inst - "inv(a!1)" "-i!1" "-j!1") (("1" (flatten) (("1" (lemma "expt_neg" ("a" "inv(a!1)")) (("1" (inst-cp - "i!1+j!1") (("1" (inst-cp - "i!1") (("1" (inst - "j!1") (("1" (assert) (("1" (rewrite "inv_inv") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (inst - "a!1" "j!1" "i!1") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (inst - "a!1" "i!1" "j!1") (("1" (flatten) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skolem 1 ("a" "i" "_")) (("2" (induct "n") (("1" (grind) (("1" (rewrite "right_identity") nil nil) ("2" (rewrite "right_identity") nil nil)) nil) ("2" (grind) (("1" (rewrite "left_identity") nil nil) ("2" (rewrite "left_identity") nil nil)) nil) ("3" (skosimp*) (("3" (lemma "expt_def1" ("a" "a")) (("3" (inst-cp - "j!2") (("3" (inst - "i+j!2") (("3" (replace -1) (("3" (replace -2) (("3" (lemma "cancel_right" ("z" "a" "x" "a ^ i * a ^ j!2" "y" "a ^ (i + j!2)")) (("3" (lemma "expt_def2" ("a" "a" "i" "i")) (("3" (lemma "cancel_right" ("z" "a" "x" "a ^ j!2 * a ^ i" "y" "a ^ (i + j!2)")) (("3" (lemma "expt_def1" ("a" "a" "i" "i")) (("3" (rewrite "associative") (("3" (rewrite "associative") (("3" (rewrite "associative") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (^ 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) (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) (T formal-nonempty-type-decl nil group 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) (inv_inv formula-decl nil group nil) (expt_neg formula-decl nil group nil) (one formal-const-decl "T" group nil) (inv const-decl "{y | x * y = one AND y * x = one}" group nil) (j!1 skolem-const-decl "int" group nil) (- const-decl "[numfield -> numfield]" number_fields nil) (minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (i!1 skolem-const-decl "int" group nil) (< const-decl "bool" reals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (cancel_right formula-decl nil group nil) (associative formula-decl nil semigroup nil) (expt_def2 formula-decl nil group nil) (int_minus_int_is_int application-judgement "int" integers nil) (expt_def1 formula-decl nil group nil) (left_identity formula-decl nil monad nil) (power def-decl "T" monoid_def nil) (right_identity formula-decl nil monad nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil)) shostak)) (expt_div 0 (expt_div-1 nil 3407072208 ("" (skosimp*) (("" (lemma "expt_mult") (("" (inst - "a!1" "i!1" "-j!1") (("" (rewrite "expt_neg") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((expt_mult formula-decl nil group nil) (expt_neg formula-decl nil group nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil 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) (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) (T formal-nonempty-type-decl nil group nil) (minus_int_is_int application-judgement "int" integers nil)) shostak)) (expt_expt 0 (expt_expt-1 nil 3292929475 ("" (skolem!) (("" (case "FORALL (a:T,n:nat): (a ^ i!1) ^ n = a ^ (i!1 * n)") (("1" (case "j!1<0") (("1" (inst - "inv(a!1)" "-j!1") (("1" (rewrite "inv_expt" -2 :dir rl) (("1" (rewrite "expt_neg" -2 :dir rl) (("1" (lemma "expt_neg" ("a" "a!1" "i" "i!1*-j!1")) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (inst - "a!1" "j!1") (("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (skolem!) (("1" (rewrite "expt_0") (("1" (rewrite "expt_0") nil nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "expt_def1" ("a" "a!2^i!1" "i" "j!2")) (("2" (inst - "a!2") (("2" (lemma "expt_mult" ("a" "a!2" "i" "i!1*j!2" "j" "i!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (^ const-decl "T" group nil) (= const-decl "[T, T -> boolean]" equalities 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) (T formal-nonempty-type-decl nil group nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield -> numfield]" number_fields nil) (j!1 skolem-const-decl "int" group 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) (expt_neg formula-decl nil group nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (inv_expt formula-decl nil group nil) (< const-decl "bool" reals nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (expt_0 formula-decl nil group nil) (expt_def1 formula-decl nil group nil) (expt_mult formula-decl nil group nil) (int_plus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) shostak)) (expt_commutes 0 (expt_commutes-1 nil 3292930125 ("" (skolem!) (("" (rewrite "expt_mult") (("" (rewrite "expt_mult") nil nil)) nil)) nil) ((expt_mult 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) (int_plus_int_is_int application-judgement "int" integers nil)) shostak)) (expt_inv_right 0 (expt_inv_right-1 nil 3292930181 ("" (skolem!) (("" (rewrite "inv_expt" :dir rl) (("" (assert) nil nil)) nil)) nil) ((inv_expt 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) (inv_right formula-decl nil group nil)) shostak)) (expt_inv_left 0 (expt_inv_left-1 nil 3292930210 ("" (skolem!) (("" (rewrite "inv_expt" :dir rl) (("" (assert) nil nil)) nil)) nil) ((inv_expt 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) (inv_left formula-decl nil group nil)) shostak)) (expt_member 0 (expt_member-1 nil 3293202255 ("" (skosimp*) (("" (expand "^") (("" (case "i!1<0") (("1" (assert) (("1" (typepred "G!1") (("1" (expand "group?") (("1" (expand "inv_exists?") (("1" (flatten) (("1" (inst - "a!1") (("1" (skosimp*) (("1" (typepred "y!1") (("1" (lemma "unique_inv" ("x" "a!1" "y" "y!1")) (("1" (assert) (("1" (replace -1 * rl) (("1" (lemma "power_member" ("M" "G!1" "a" "y!1" "n" "-i!1")) (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "power_member" ("M" "G!1" "a" "a!1" "n" "i!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((^ const-decl "T" group 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) (member const-decl "bool" sets nil) (unique_inv formula-decl nil group nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (monoid nonempty-type-eq-decl nil monoid nil) (monoid? const-decl "bool" monoid_def nil) (power_member formula-decl nil monoid nil) (inv_exists? const-decl "bool" group_def 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) (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)) shostak)) (generated_by_TCC1 0 (generated_by_TCC1-1 nil 3293203363 ("" (skosimp*) (("" (expand "group?") (("" (split) (("1" (expand "monoid?") (("1" (split) (("1" (expand "monad?") (("1" (expand "groupoid?") (("1" (expand "star_closed?") (("1" (expand "identity?") (("1" (expand "member") (("1" (split) (("1" (skosimp*) (("1" (typepred "x!1") (("1" (typepred "y!1") (("1" (skosimp*) (("1" (inst + "i!2+i!1") (("1" (rewrite "expt_mult" :dir rl) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "0") (("2" (rewrite "expt_0") nil nil)) nil) ("3" (skosimp) (("3" (expand "restrict") (("3" (rewrite "left_identity") (("3" (rewrite "right_identity") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "fullset_is_group") (("2" (expand "group?") (("2" (expand "monoid?") (("2" (flatten) (("2" (expand "restrict") (("2" (expand "associative?") (("2" (skosimp*) (("2" (typepred "x!1") (("2" (typepred "y!1") (("2" (typepred "z!1") (("2" (skosimp*) (("2" (inst - "x!1" "y!1" "z!1") (("1" (expand "fullset") (("1" (propax) nil nil)) nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil) ("3" (expand "fullset") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "inv_exists?") (("2" (skosimp*) (("2" (typepred "x!1") (("2" (skolem!) (("2" (inst + "a!1^(-i!1)") (("1" (replace -1) (("1" (lemma "expt_mult" ("a" "a!1" "i" "i!1" "j" "-i!1")) (("1" (lemma "expt_mult" ("a" "a!1" "i" "-i!1" "j" "i!1")) (("1" (assert) (("1" (rewrite "expt_0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "-i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((group? const-decl "bool" group_def nil) (inv_exists? const-decl "bool" group_def nil) (minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield -> numfield]" number_fields nil) (i!1 skolem-const-decl "int" group nil) (monoid? const-decl "bool" monoid_def nil) (associative? const-decl "bool" operator_defs nil) (fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil) (a!1 skolem-const-decl "T" group nil) (x!1 skolem-const-decl "({t: T | EXISTS (i: int): t = a!1 ^ i})" group nil) (y!1 skolem-const-decl "({t: T | EXISTS (i: int): t = a!1 ^ i})" group nil) (z!1 skolem-const-decl "({t: T | EXISTS (i: int): t = a!1 ^ i})" group nil) (fullset_is_group formula-decl nil group nil) (monad? const-decl "bool" monad_def nil) (identity? const-decl "bool" operator_defs nil) (^ const-decl "T" group nil) (= const-decl "[T, T -> boolean]" equalities nil) (T formal-nonempty-type-decl nil group 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) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (expt_mult formula-decl nil group nil) (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) (expt_0 formula-decl nil group nil) (restrict const-decl "R" restrict nil) (right_identity formula-decl nil monad nil) (one formal-const-decl "T" group nil) (* formal-const-decl "[T, T -> T]" group nil) (left_identity formula-decl nil monad nil) (member const-decl "bool" sets nil) (star_closed? const-decl "bool" groupoid_def nil)) shostak)) (generated_by_lem 0 (generated_by_lem-1 nil 3396976913 ("" (skosimp*) (("" (expand "generated_by") (("" (inst?) nil nil)) nil)) nil) ((generated_by const-decl "group" 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)) shostak)) (generated_is_subgroup 0 (generated_is_subgroup-1 nil 3293271210 ("" (skosimp*) (("" (typepred "generated_by(a!1)") (("" (expand "subgroup?") (("" (expand "subset?") (("" (skosimp*) (("" (assert) (("" (expand "generated_by" -3) (("" (expand "member") (("" (skosimp) (("" (lemma "expt_member" ("G" "G!1" "a" "a!1" "i" "i!1")) (("" (expand "member") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((generated_by const-decl "group" group 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) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (expt_member formula-decl nil group 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) (subgroup? const-decl "bool" group_def nil)) shostak)) (generated_by_is_finite 0 (generated_by_is_finite-2 nil 3407003916 ("" (skosimp*) (("" (assert) (("" (rewrite "finite_group_surj") (("" (hide 2) (("" (expand "generated_by") (("" (inst + "k!1" "(LAMBDA (n: below[k!1]): a!1^n)") (("1" (expand "surjective?") (("1" (skosimp*) (("1" (typepred "y!1") (("1" (replace -2) (("1" (assert) (("1" (skosimp*) (("1" (replace -1) (("1" (lemma "euclid_int") (("1" (inst - "k!1" "i!1") (("1" (skosimp*) (("1" (replace -1) (("1" (typepred "r!1") (("1" (inst + "r!1") (("1" (lemma "expt_mult") (("1" (inst - "a!1" "k!1*q!1" "r!1") (("1" (assert) (("1" (replace -1 + rl) (("1" (lemma "expt_expt") (("1" (inst?) (("1" (replace -1 + rl) (("1" (replace -7) (("1" (assert) (("1" (rewrite "one_expt") (("1" (rewrite "left_identity") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (replace -1) (("2" (assert) (("2" (inst + "n!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((a!1 skolem-const-decl "T" group nil) (^ const-decl "T" group nil) (S!1 skolem-const-decl "set[T]" group nil) (below type-eq-decl nil nat_types nil) (k!1 skolem-const-decl "posnat" group 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (euclid_int formula-decl nil euclidean_division nil) (mod nonempty-type-eq-decl nil euclidean_division nil) (expt_mult formula-decl nil group nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (expt_expt formula-decl nil group nil) (left_identity formula-decl nil monad nil) (one_expt formula-decl nil group nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (NOT const-decl "[bool -> bool]" booleans nil) (surjective? const-decl "bool" functions nil) (generated_by const-decl "group" 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) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (finite_group_surj formula-decl nil group_def nil)) nil) (generated_by_is_finite-1 nil 3407003019 ("" (skosimp*) (("" (assert) (("" (rewrite "finite_group_surj") (("" (hide 2) (("" (expand "generated_by") (("" (inst + "k!1" "(LAMBDA (n: below[k!1]): group[T,*,one].^(a!1,n))") (("1" (expand "surjective?") (("1" (skosimp*) (("1" (typepred "y!1") (("1" (replace -2) (("1" (assert) (("1" (skosimp*) (("1" (replace -1) (("1" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (center_TCC1 0 (center_TCC1-1 nil 3460720344 ("" (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) (group? const-decl "bool" group_def nil) (group nonempty-type-eq-decl nil group 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) (G!1 skolem-const-decl "group" group nil) (extend const-decl "R" extend nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil)) nil)) (center_def 0 (center_def-1 nil 3460720393 ("" (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) (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) (group? const-decl "bool" group_def nil) (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) (center const-decl "{s: set[T] | subset?(s, G)}" group nil) (extend const-decl "R" extend nil)) shostak)) (center_subgroup 0 (center_subgroup-1 nil 3460720417 ("" (skosimp*) (("" (lemma "subgroup_def") (("" (inst?) (("" (assert) (("" (hide 2) (("" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "one") (("1" (grind) (("1" (lemma "one_member") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "center") (("2" (expand "extend") (("2" (expand "star_closed?") (("2" (expand "member") (("2" (skosimp*) (("2" (prop) (("1" (skosimp*) (("1" (typepred "x!2") (("1" (typepred "G!1") (("1" (expand "group?") (("1" (expand "monoid?") (("1" (flatten) (("1" (expand "restrict") (("1" (expand "associative?") (("1" (typepred "x!1") (("1" (inst-cp - "x!1" "y!1" "x!2") (("1" (inst-cp - "x!2" "x!1" "y!1") (("1" (assert) (("1" (replace -5 + rl) (("1" (inst - "x!2") (("1" (replace - +) (("1" (inst-cp - "x!1" "x!2" "y!1") (("1" (replace -5) (("1" (typepred "y!1") (("1" (assert) (("1" (inst - "x!2") (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (typepred "x!1") (("2" (typepred "y!1") (("2" (hide -1 -3) (("2" (typepred "G!1") (("2" (expand "group?") (("2" (expand "monoid?") (("2" (expand "monad?") (("2" (flatten) (("2" (expand "star_closed?") (("2" (assert) (("2" (inst - "x!1" "y!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "inv_closed?") (("3" (skosimp*) (("3" (assert) (("3" (expand "center") (("3" (expand "extend") (("3" (ground) (("1" (skolem 1 "q") (("1" (typepred "q") (("1" (lemma "inv_star") (("1" (inst?) (("1" (rewrite "inv_inv") (("1" (typepred "x!1") (("1" (lemma "center_def") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (inst - "inv(q)") (("1" (assert) (("1" (replace -2 - rl) (("1" (case "inv(inv(q * inv(x!1))) = inv(inv(q) * x!1)") (("1" (rewrite "inv_inv") (("1" (rewrite "inv_star") nil nil)) nil) ("2" (replace -4) (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-4 1)) (("2" (lemma "inv_member") (("2" (inst?) (("2" (assert) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "inv_member") (("2" (inst?) (("2" (inst?) (("2" (assert) (("2" (typepred "x!1") (("2" (lemma "center_def") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((subgroup_def formula-decl nil group nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (empty? const-decl "bool" sets nil) (one_member formula-decl nil monad nil) (monad? const-decl "bool" monad_def nil) (monad nonempty-type-eq-decl nil monad nil) (right_identity formula-decl nil monad nil) (left_identity formula-decl nil monad nil) (extend const-decl "R" extend nil) (member const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (associative? const-decl "bool" operator_defs nil) (FALSE const-decl "bool" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (restrict const-decl "R" restrict nil) (monoid? const-decl "bool" monoid_def nil) (star_closed? const-decl "bool" groupoid_def nil) (inv const-decl "{y | x * y = one AND y * x = one}" group nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (inv_member formula-decl nil group nil) (q skolem-const-decl "(G!1)" group nil) (G!1 skolem-const-decl "group" group nil) (center_def formula-decl nil group nil) (inv_inv formula-decl nil group nil) (inv_star formula-decl nil group nil) (inv_closed? const-decl "bool" group nil) (center const-decl "{s: set[T] | subset?(s, G)}" group nil) (subset? 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)) nil)) (one_left 0 (one_left-1 nil 3406039608 ("" (skosimp*) (("" (rewrite "left_identity") nil nil)) nil) ((left_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)) shostak)) (one_right 0 (one_right-1 nil 3406039617 ("" (skosimp*) (("" (rewrite "right_identity") nil nil)) 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)) shostak)) (assoc 0 (assoc-1 nil 3406289999 ("" (skosimp*) (("" (rewrite "associative") nil nil)) nil) ((associative formula-decl nil semigroup nil) (T formal-nonempty-type-decl nil group nil) (* formal-const-decl "[T, T -> T]" group nil)) shostak)))
¤ Dauer der Verarbeitung: 0.65 Sekunden (vorverarbeitet am 2026-04-25) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26