|
(zn
(floor_help 0
(floor_help-1 nil 3406628503
("" (skosimp*)
(("" (lemma "floor_small")
(("" (inst?)
(("" (ground) (("" (expand "abs") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((floor_small formula-decl nil floor_ceil nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
(nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(minus_odd_is_odd application-judgement "odd_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)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
real_defs nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(below type-eq-decl nil naturalnumbers nil)
(N formal-const-decl "posnat" zn 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)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer nonempty-type-from-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))
(Z_group 0
(Z_group-1 nil 3406632154
("" (expand "group?")
(("" (prop)
(("1" (grind) nil nil)
("2" (expand "inv_exists?")
(("2" (skosimp*)
(("2" (inst + "-x!1")
(("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil)
((fullset const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(star_closed? const-decl "bool" groupoid_def nil)
(restrict const-decl "R" restrict 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)
(int_plus_int_is_int application-judgement "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)
(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)
(set type-eq-decl nil sets nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(x!1 skolem-const-decl "(fullset[int])" zn nil)
(minus_int_is_int application-judgement "int" integers nil)
(inv_exists? const-decl "bool" group_def nil)
(group? const-decl "bool" group_def nil))
shostak))
(Z_TCC1 0
(Z_TCC1-1 nil 3406632132 ("" (rewrite "Z_group") nil nil)
((Z_group formula-decl nil zn nil)) nil))
(Z_prep_TCC1 0
(Z_prep_TCC1-1 nil 3406629634 ("" (subtype-tcc) nil nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(Z_prep_TCC2 0
(Z_prep_TCC2-1 nil 3406629634
("" (inst + "0") (("" (assert) nil nil)) nil)
((below type-eq-decl nil naturalnumbers nil)
(N formal-const-decl "posnat" zn 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)
(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)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(Z_prep 0
(Z_prep-1 nil 3406629642
("" (expand "group?")
(("" (prop)
(("1" (auto-rewrite-theory "group_rew") (("1" (grind) nil nil))
nil)
("2" (expand "inv_exists?")
(("2" (skosimp*)
(("2" (expand "++")
(("2" (case "x!1 = 0")
(("1" (inst + "0")
(("1" (assert)
(("1" (assert)
(("1" (replace -1)
(("1" (assert)
(("1" (lemma "mod_zero")
(("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "fullset") (("2" (propax) nil nil)) nil))
nil)
("2" (inst + "N-x!1")
(("1" (assert)
(("1" (assert) (("1" (rewrite "mod_eq_arg") nil nil))
nil))
nil)
("2" (assert)
(("2" (expand "fullset") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((int_minus_int_is_int application-judgement "int" integers nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers 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)
(restrict const-decl "R" restrict nil)
(floor_help formula-decl nil zn nil)
(star_closed? const-decl "bool" groupoid_def nil)
(member const-decl "bool" sets nil)
(fullset const-decl "set" sets nil)
(++ const-decl "below(N)" zn nil)
(mod const-decl "{k | abs(k) < abs(j)}" mod nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(set type-eq-decl nil sets nil)
(below type-eq-decl nil naturalnumbers nil)
(N formal-const-decl "posnat" zn nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(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)
(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)
(int_plus_int_is_int application-judgement "int" integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nil application-judgement "below(m)" mod nil)
(mod_zero formula-decl nil mod nil)
(/= const-decl "boolean" notequal nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(mod_eq_arg formula-decl nil mod nil)
(x!1 skolem-const-decl "(fullset[below(N)])" zn nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(inv_exists? const-decl "bool" group_def nil)
(group? const-decl "bool" group_def nil))
nil))
(Z__TCC1 0
(Z__TCC1-1 nil 3406628019 ("" (rewrite "Z_prep") nil nil)
((Z_prep formula-decl nil zn nil)) nil))
(nZ_plus_TCC1 0
(nZ_plus_TCC1-1 nil 3406633427
("" (skosimp*)
(("" (typepred "y!1")
(("" (typepred "x!1")
(("" (skosimp*)
(("" (replace -1)
(("" (hide -1)
(("" (replace -1)
(("" (hide -1)
(("" (inst + "k!1+k!2") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nZ_TYPE type-eq-decl nil zn nil)
(N formal-const-decl "posnat" zn 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)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil))
nil))
(nZ_prep_TCC1 0
(nZ_prep_TCC1-1 nil 3406630770 ("" (subtype-tcc) nil nil)
((number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil))
nil))
(nZ_prep_TCC2 0
(nZ_prep_TCC2-1 nil 3406630770
("" (inst + "0") (("" (inst?) (("" (assert) nil nil)) nil)) nil)
((nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(nZ_TYPE type-eq-decl nil zn nil)
(N formal-const-decl "posnat" zn 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)
(bool nonempty-type-eq-decl nil booleans nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities 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))
nil))
(nZ_prep 0
(nZ_prep-1 nil 3406630788
("" (expand "group?")
(("" (prop)
(("1" (grind) nil nil)
("2" (expand "inv_exists?")
(("2" (skosimp*)
(("2" (inst + "-x!1")
(("1" (grind) nil nil)
("2" (typepred "x!1")
(("2" (skosimp*)
(("2" (replace -1)
(("2" (prop)
(("1" (inst + "-k!1") (("1" (assert) nil nil)) nil)
("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nZ_plus const-decl "nZ_TYPE" zn nil)
(fullset const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(star_closed? const-decl "bool" groupoid_def nil)
(restrict const-decl "R" restrict 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)
(int_plus_int_is_int application-judgement "int" integers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(N formal-const-decl "posnat" zn nil)
(nZ_TYPE type-eq-decl nil zn nil) (set type-eq-decl nil sets nil)
(x!1 skolem-const-decl "(fullset[(nZ_TYPE)])" zn nil)
(minus_int_is_int application-judgement "int" integers nil)
(inv_exists? const-decl "bool" group_def nil)
(group? const-decl "bool" group_def nil))
shostak))
(nZ_TCC1 0
(nZ_TCC1-1 nil 3406632132
("" (skosimp*)
(("" (typepred "x1!1`1")
(("" (typepred "x1!1`2")
(("" (skosimp*)
(("" (inst + "k!1+k!2")
(("" (assert)
(("" (case-replace "x1!1 = (x1!1`1,x1!1`2)")
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nZ_TYPE type-eq-decl nil zn nil)
(N formal-const-decl "posnat" zn 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)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(int_plus_int_is_int application-judgement "int" integers nil))
nil))
(nZ_TCC2 0
(nZ_TCC2-1 nil 3406634220
("" (expand "group?")
(("" (prop)
(("1" (grind) nil nil)
("2" (expand "inv_exists?")
(("2" (skosimp*)
(("2" (inst + "-x!1")
(("1" (grind) nil nil)
("2" (prop)
(("1" (typepred "x!1")
(("1" (skosimp*)
(("1" (replace -1)
(("1" (hide -1)
(("1" (inst + "-k!1") (("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((fullset const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(star_closed? const-decl "bool" groupoid_def nil)
(restrict const-decl "R" restrict 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)
(int_plus_int_is_int application-judgement "int" integers nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(N formal-const-decl "posnat" zn nil)
(nZ_TYPE type-eq-decl nil zn nil) (set type-eq-decl nil sets nil)
(x!1 skolem-const-decl "(fullset[nZ_TYPE])" zn nil)
(minus_int_is_int application-judgement "int" integers nil)
(inv_exists? const-decl "bool" group_def nil)
(group? const-decl "bool" group_def nil))
nil))
(nZ_normal_TCC1 0
(nZ_normal_TCC1-1 nil 3406634590
("" (expand "group?")
(("" (prop)
(("1" (typepred "Z")
(("1" (expand "group?")
(("1" (flatten)
(("1" (hide -2)
(("1" (grind)
(("1" (typepred "Z")
(("1" (expand "group?")
(("1" (flatten)
(("1" (hide-all-but (-1 1))
(("1" (expand "monoid?")
(("1" (flatten)
(("1" (hide -2)
(("1"
(expand "monad?")
(("1"
(flatten)
(("1"
(expand "groupoid?")
(("1"
(expand "star_closed?")
(("1"
(expand "member")
(("1" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "Z")
(("2" (expand "group?")
(("2" (expand "monoid?")
(("2" (expand "monad?")
(("2" (expand "groupoid?")
(("2" (flatten)
(("2" (expand "inv_exists?")
(("2" (skosimp*)
(("2" (inst - "x!1")
(("1" (skosimp*)
(("1" (inst + "y!1")
(("1" (assert) nil nil)
("2" (typepred "y!1")
(("2"
(typepred "x!1")
(("2"
(skosimp*)
(("2"
(prop)
(("1"
(inst + "-k!1")
(("1" (assert) nil nil))
nil)
("2"
(expand "restrict")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (hide 2)
(("2" (typepred "x!1")
(("2"
(skosimp*)
(("2"
(expand "restrict")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((int_plus_int_is_int application-judgement "int" integers 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)
(star_closed? const-decl "bool" groupoid_def nil)
(member const-decl "bool" sets nil)
(fullset const-decl "set" sets 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)
(set type-eq-decl nil sets nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(restrict const-decl "R" restrict nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(group nonempty-type-eq-decl nil group nil)
(Z const-decl
"group[int, restrict[[numfield, numfield], [int, int], numfield](+), 0]"
zn nil)
(inv_exists? const-decl "bool" group_def nil)
(x!1 skolem-const-decl "(restrict[int, nZ_TYPE, boolean](Z))" zn
nil)
(nZ_TYPE type-eq-decl nil zn nil)
(N formal-const-decl "posnat" zn 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)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(y!1 skolem-const-decl "(Z)" zn nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(minus_int_is_int application-judgement "int" integers nil)
(group? const-decl "bool" group_def nil))
nil))
(nZ_normal 0
(nZ_normal-1 nil 3406634595
("" (expand "normal_subgroup?")
(("" (prop)
(("1" (expand "restrict")
(("1" (expand "subgroup?")
(("1" (expand "subset?")
(("1" (assert)
(("1" (skosimp*)
(("1" (typepred "x!1")
(("1" (skosimp*)
(("1" (replace -1)
(("1" (assert)
(("1" (expand "Z")
(("1" (expand "fullset")
(("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*) (("2" (grind) nil nil)) nil))
nil))
nil)
((subgroup? const-decl "bool" group_def nil)
(member const-decl "bool" sets nil)
(nZ_TYPE type-eq-decl nil zn nil)
(N formal-const-decl "posnat" zn 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)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(Z const-decl
"group[int, restrict[[numfield, numfield], [int, int], numfield](+), 0]"
zn nil)
(fullset const-decl "set" sets nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(subset? const-decl "bool" sets nil)
(restrict const-decl "R" restrict nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(* const-decl "set[T]" cosets nil)
(nZ const-decl "group
[nZ_TYPE,
restrict[[numfield, numfield], [nZ_TYPE, nZ_TYPE], numfield](+), 0]"
zn nil)
(normal_subgroup? const-decl "boolean" normal_subgroups nil))
shostak))
(Z_fact_test_TCC1 0
(Z_fact_test_TCC1-2 nil 3445765147
("" (auto-rewrite "fullset")
(("" (auto-rewrite "restrict")
(("" (auto-rewrite "extend")
(("" (auto-rewrite "nZ")
(("" (assert)
(("" (auto-rewrite "Z")
((""
(case " group?
[int, restrict[[numfield, numfield], [int, int], numfield](+), 0]
(extend[int, nZ_TYPE, bool, FALSE](fullset[nZ_TYPE]))")
(("1" (assert)
(("1" (expand "normal_subgroup?")
(("1" (expand "subgroup?")
(("1" (expand "subset?")
(("1" (assert)
(("1" (skosimp*)
(("1" (expand "extend")
(("1"
(assert)
(("1"
(ground)
(("1"
(expand "*")
(("1"
(skosimp*)
(("1"
(replace -2 * lr)
(("1"
(hide -2)
(("1"
(typepred "h!1")
(("1"
(skosimp*)
(("1"
(case-replace
"inv[int, restrict[[numfield, numfield], [int, int], numfield](+), 0]
(a!1) = -a!1")
(("1" (assert) nil nil)
("2"
(hide-all-but 1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "group?")
(("2" (expand "monoid?")
(("2" (expand "associative?")
(("2" (assert)
(("2" (prop)
(("1" (expand "monad?")
(("1"
(assert)
(("1"
(expand "groupoid?")
(("1"
(expand "star_closed?")
(("1"
(assert)
(("1"
(prop)
(("1"
(skosimp*)
(("1"
(assert)
(("1"
(expand "extend")
(("1"
(ground)
(("1"
(typepred "x!1")
(("1"
(typepred "y!1")
(("1"
(expand "extend")
(("1"
(ground)
(("1"
(skosimp*)
(("1"
(inst
+
"k!1+k!2")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "extend")
(("2"
(ground)
(("2"
(inst + "0")
(("2" (assert) nil nil))
nil))
nil))
nil)
("3"
(expand "identity?")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "inv_exists?")
(("2"
(skosimp*)
(("2"
(assert)
(("2"
(inst + "-x!1")
(("1" (assert) nil nil)
("2"
(assert)
(("2"
(expand "extend")
(("2"
(ground)
(("2"
(typepred "x!1")
(("2"
(expand "extend")
(("2"
(ground)
(("2"
(skosimp*)
(("2"
(inst + "-k!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((monoid? const-decl "bool" monoid_def nil)
(inv_exists? const-decl "bool" group_def nil)
(x!1 skolem-const-decl
"(extend[int, nZ_TYPE, bool, FALSE](fullset[nZ_TYPE]))" zn nil)
(monad? const-decl "bool" monad_def nil)
(star_closed? const-decl "bool" groupoid_def nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(identity? const-decl "bool" operator_defs nil)
(associative? const-decl "bool" operator_defs nil)
(Z const-decl
"group[int, restrict[[numfield, numfield], [int, int], numfield](+), 0]"
zn nil)
(subgroup? const-decl "bool" group_def nil)
(member const-decl "bool" sets nil)
(minus_int_is_int application-judgement "int" integers nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(TRUE const-decl "bool" booleans nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(* const-decl "set[T]" cosets nil)
(* const-decl "set[T]" cosets nil)
(subset? const-decl "bool" sets nil)
(normal_subgroup? const-decl "boolean" normal_subgroups nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(int_plus_int_is_int application-judgement "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)
(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)
(set type-eq-decl nil sets nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(restrict const-decl "R" restrict nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(group? const-decl "bool" group_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(N formal-const-decl "posnat" zn nil)
(nZ_TYPE type-eq-decl nil zn nil)
(FALSE const-decl "bool" booleans nil)
(extend const-decl "R" extend nil)
(fullset const-decl "set" sets nil)
(nZ const-decl "group
[nZ_TYPE,
restrict[[numfield, numfield], [nZ_TYPE, nZ_TYPE], numfield](+), 0]"
zn nil))
nil)
(Z_fact_test_TCC1-1 nil 3445765086 ("" (subtype-tcc) nil nil) nil
nil))
(Z_fact_test_TCC2 0
(Z_fact_test_TCC2-2 nil 3445765183
("" (expand "extend")
(("" (expand "*")
(("" (grind)
(("" (apply-extensionality 1 :hide? t)
(("" (lift-if)
(("" (ground)
(("1" (skosimp*)
(("1" (inst + "(k!1-1)*N")
(("1" (assert) nil nil)
("2" (ground)
(("2" (inst + "(k!1-1)") (("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (replace -1 * lr)
(("2" (hide -1)
(("2" (typepred "h!1")
(("2" (skosimp*)
(("2" (replace -2 * lr)
(("2" (hide -2)
(("2" (hide -1)
(("2"
(inst + "k!1+1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((* const-decl "set[T]" cosets nil)
(nZ_TYPE type-eq-decl nil zn nil)
(FALSE const-decl "bool" booleans nil)
(TRUE const-decl "bool" booleans nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(k!1 skolem-const-decl "int" zn nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, 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)
(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)
(set type-eq-decl nil sets nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(restrict const-decl "R" restrict nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(group? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(N formal-const-decl "posnat" zn nil)
(nZ const-decl "group
[nZ_TYPE,
restrict[[numfield, numfield], [nZ_TYPE, nZ_TYPE], numfield](+), 0]"
zn nil)
(fullset const-decl "set" sets nil)
(Z const-decl
"group[int, restrict[[numfield, numfield], [int, int], numfield](+), 0]"
zn nil)
(extend const-decl "R" extend nil))
nil)
(Z_fact_test_TCC2-1 nil 3445765086 ("" (subtype-tcc) nil nil) nil
nil))
(Z_fact_test 0
(Z_fact_test-1 nil 3445765676 ("" (assert) nil nil) nil shostak)))
¤ Dauer der Verarbeitung: 0.60 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.
|
