|
(gcd (gcd_TCC1 0
(gcd_TCC1-1 nil 3319536974
("" (skosimp*)
(("" (rewrite "gcd_noem")
(("" (assert) (("" (rewrite "gcd_prep") nil nil)) nil)) nil))
nil)
((gcd_noem formula-decl nil divides_lems 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)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(/= const-decl "boolean" notequal nil)
(gcd_prep formula-decl nil divides_lems nil))
nil))
(gcd_divides_TCC1 0
(gcd_divides_TCC1-1 nil 3319536974 ("" (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)
(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 "boolean" notequal nil))
nil))
(gcd_divides 0
(gcd_divides-1 nil 3319536974
("" (skosimp*)
(("" (expand "gcd")
((""
(typepred
"max({k: posnat | divides(k, i!1) AND divides(k, j!1)})")
(("1" (assert) (("1" (prop) nil nil)) nil)
("2" (rewrite "gcd_noem")
(("2" (rewrite "gcd_prep") (("2" (ground) nil nil)) nil))
nil))
nil))
nil))
nil)
((gcd const-decl "{k: posnat | divides(k, i) AND divides(k, j)}"
gcd nil)
(gcd_noem formula-decl nil divides_lems nil)
(gcd_prep formula-decl nil divides_lems nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(/= const-decl "boolean" notequal nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(> 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)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(max const-decl
"{a: posnat | S(a) AND (FORALL x: S(x) IMPLIES x <= a)}"
max_bounded_posnat nil)
(divides const-decl "bool" divides nil))
nil))
(gcd_is_max 0
(gcd_is_max-1 nil 3319536974
("" (skosimp*)
(("" (expand "gcd")
((""
(typepred
"max({k: posnat | divides(k, i!1) AND divides(k, j!1)})")
(("1" (inst?)
(("1" (assert) (("1" (ground) nil nil)) nil)
("2" (assert) nil nil))
nil)
("2" (rewrite "gcd_noem")
(("2" (assert)
(("2" (rewrite "gcd_prep") (("2" (prop) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((gcd const-decl "{k: posnat | divides(k, i) AND divides(k, j)}"
gcd nil)
(gcd_noem formula-decl nil divides_lems nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(gcd_prep formula-decl nil divides_lems nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(/= const-decl "boolean" notequal nil)
(nzint nonempty-type-eq-decl nil integers nil)
(kk!1 skolem-const-decl "nzint" gcd nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(> 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)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(max const-decl
"{a: posnat | S(a) AND (FORALL x: S(x) IMPLIES x <= a)}"
max_bounded_posnat nil)
(divides const-decl "bool" divides nil))
nil))
(gcd_def 0
(gcd_def-1 nil 3319536974
("" (skosimp*)
(("" (split +)
(("1" (flatten)
(("1" (assert)
(("1" (skosimp*)
(("1" (lemma "gcd_is_max")
(("1" (inst?)
(("1" (inst -1 "mm!1") (("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (expand "gcd")
(("2" (lemma "max_def")
(("2" (inst?)
(("1" (assert)
(("1" (hide 2)
(("1" (expand "maximum?")
(("1" (propax) nil nil)) nil))
nil))
nil)
("2" (rewrite "gcd_noem")
(("2" (rewrite "gcd_prep") (("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((gcd_is_max formula-decl nil gcd nil)
(/= const-decl "boolean" notequal nil)
(nzint nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans 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)
(real_le_is_total_order name-judgement "(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)
(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)
(gcd const-decl "{k: posnat | divides(k, i) AND divides(k, j)}"
gcd nil)
(<= const-decl "bool" reals nil)
(j!1 skolem-const-decl "int" gcd nil)
(i!1 skolem-const-decl "int" gcd nil)
(divides const-decl "bool" divides nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(maximum? const-decl "bool" max_bounded_posnat nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(gcd_prep formula-decl nil divides_lems nil)
(gcd_noem formula-decl nil divides_lems nil)
(max_def formula-decl nil max_bounded_posnat nil))
nil))
(gcd_0_pos 0
(gcd_0_pos-1 nil 3319536974
("" (skosimp*)
(("" (expand "gcd")
(("" (lemma "max_def")
(("" (inst?)
(("1" (flatten)
(("1" (assert)
(("1" (hide -1 2)
(("1" (expand "maximum?")
(("1" (split)
(("1" (expand "divides")
(("1" (inst + "0") (("1" (assert) nil nil))
nil))
nil)
("2" (expand "divides")
(("2" (inst + "1") (("2" (assert) nil nil))
nil))
nil)
("3" (skosimp*)
(("3" (expand "divides")
(("3" (skosimp*)
(("3"
(typepred "mm!1")
(("3"
(typepred "x!1")
(("3"
(lemma "pos_times_gt")
(("3"
(hide -4)
(("3"
(inst?)
(("3"
(assert)
(("3"
(replace -4)
(("3"
(lemma
"both_sides_times_pos_le1")
(("3"
(inst
-1
"x!1"
"1"
"x!3")
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (prop)
(("1" (rewrite "gcd_noem") nil nil)
("2" (rewrite "gcd_prep") nil nil))
nil))
nil))
nil))
nil))
nil)
((gcd const-decl "{k: posnat | divides(k, i) AND divides(k, j)}"
gcd nil)
(<= const-decl "bool" reals nil)
(mm!1 skolem-const-decl "posnat" gcd nil)
(divides const-decl "bool" divides nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(number nonempty-type-decl nil numbers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(maximum? const-decl "bool" max_bounded_posnat nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(both_sides_times_pos_le1 formula-decl nil real_props nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(pos_times_gt formula-decl nil real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(int_times_even_is_even application-judgement "even_int"
integers nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(/= const-decl "boolean" notequal nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(gcd_prep formula-decl nil divides_lems nil)
(gcd_noem formula-decl nil divides_lems nil)
(max_def formula-decl nil max_bounded_posnat nil))
nil))
(gcd_abs_TCC1 0
(gcd_abs_TCC1-1 nil 3319536974 ("" (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)
(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)
(int_abs_is_nonneg application-judgement
"{j: nonneg_int | j >= i}" real_defs nil)
(/= const-decl "boolean" notequal nil))
nil))
(gcd_abs 0
(gcd_abs-1 nil 3319536974
("" (skosimp*)
(("" (expand "gcd")
((""
(case "{k: posnat | divides(k, i!1) AND divides(k, j!1)}
= {k: posnat | divides(k, abs(i!1)) AND divides(k, abs(j!1))}")
(("1" (assert) nil nil)
("2" (hide 2)
(("2" (apply-extensionality 1 :hide? t)
(("2" (iff)
(("2" (split +)
(("1" (flatten)
(("1" (expand "divides")
(("1" (skosimp*)
(("1" (prop)
(("1"
(inst +
"IF i!1 < 0 THEN -x!2 ELSE x!2 ENDIF")
(("1" (grind) nil nil)) nil)
("2"
(inst +
"IF i!1 < 0 THEN -x!2 ELSE x!2 ENDIF")
(("2" (grind) nil nil)) nil)
("3"
(inst +
"IF j!1 < 0 THEN -x!3 ELSE x!3 ENDIF")
(("3" (grind) nil nil)) nil)
("4"
(inst +
"IF j!1 < 0 THEN -x!3 ELSE x!3 ENDIF")
(("4" (grind) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (expand "divides")
(("2" (skosimp*)
(("2" (prop)
(("1"
(inst +
"IF i!1 < 0 THEN -x!2 ELSE x!2 ENDIF")
(("1"
(hide -2)
(("1" (grind) nil nil))
nil))
nil)
("2" (hide -2)
(("2"
(inst
+
"IF i!1 < 0 THEN -x!2 ELSE x!2 ENDIF")
(("2" (grind) nil nil))
nil))
nil)
("3" (hide -1)
(("3"
(inst
+
"IF j!1 < 0 THEN -x!3 ELSE x!3 ENDIF")
(("3" (grind) nil nil))
nil))
nil)
("4" (hide -1)
(("4"
(inst
+
"IF j!1 < 0 THEN -x!3 ELSE x!3 ENDIF")
(("4" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((gcd const-decl "{k: posnat | divides(k, i) AND divides(k, j)}"
gcd nil)
(minus_int_is_int application-judgement "int" integers nil)
(< const-decl "bool" reals nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(mult_divides2 application-judgement "(divides(m))" divides
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_abs_is_nonneg application-judgement
"{j: nonneg_int | j >= i}" real_defs 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)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(divides const-decl "bool" divides nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil))
nil))
(gcd_0_neg 0
(gcd_0_neg-1 nil 3319536974
("" (skosimp*)
(("" (rewrite "gcd_abs")
(("" (expand "abs")
(("" (rewrite "gcd_0_pos") (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((minus_nzint_is_nzint application-judgement "nzint" integers
nil)
(gcd_abs formula-decl nil gcd 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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(bool nonempty-type-eq-decl nil booleans 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)
(nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
real_defs nil)
(int_abs_is_nonneg application-judgement
"{j: nonneg_int | j >= i}" real_defs nil)
(abs_nat_rew formula-decl nil abs_rews nil)
(abs_neg_rew formula-decl nil abs_rews nil)
(gcd_0_pos formula-decl nil gcd nil))
nil))
(gcd_sym 0
(gcd_sym-1 nil 3319536974
("" (skosimp*)
(("" (expand "gcd")
((""
(case-replace
"{k: posnat | divides(k, i!1) AND divides(k, j!1)}
= {k: posnat | divides(k, j!1) AND divides(k, i!1)}")
(("" (hide 2)
(("" (apply-extensionality 1 :hide? t)
(("" (iff) (("" (ground) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((gcd const-decl "{k: posnat | divides(k, i) AND divides(k, j)}"
gcd nil)
(divides const-decl "bool" divides nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(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))
(gcd_lt_nat_TCC1 0
(gcd_lt_nat_TCC1-1 nil 3319536974 ("" (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)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(/= const-decl "boolean" notequal nil))
nil))
(gcd_lt_nat 0
(gcd_lt_nat-1 nil 3319536974
("" (skosimp*)
(("" (typepred "gcd(n!1, m!1)")
(("" (expand "divides")
(("" (skosimp*)
(("" (name-replace "NN" "gcd(n!1,m!1)")
(("" (case-replace "x!1 = 0")
(("1" (assert) nil nil)
("2" (lemma "pos_times_ge")
(("2" (inst?)
(("2" (assert)
(("2" (lemma "both_sides_times_pos_le1")
(("2" (inst -1 "NN" "1" "x!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nat nonempty-type-eq-decl nil naturalnumbers nil)
(gcd const-decl "{k: posnat | divides(k, i) AND divides(k, j)}"
gcd nil)
(divides const-decl "bool" divides nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(/= const-decl "boolean" notequal nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans 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)
(int nonempty-type-eq-decl nil integers 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(int_times_even_is_even application-judgement "even_int"
integers nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(both_sides_times_pos_le1 formula-decl nil real_props nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(pos_times_ge formula-decl nil real_props nil))
nil))
(gcd_lt_TCC1 0
(gcd_lt_TCC1-1 nil 3319536974 ("" (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)
(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 "boolean" notequal nil))
nil))
(gcd_lt 0
(gcd_lt-1 nil 3319536974
("" (skosimp*)
(("" (lemma "gcd_lt_nat")
(("" (inst-cp -1 "abs(j!1)" "abs(i!1)")
(("" (inst -1 "abs(i!1)" "abs(j!1)")
(("" (split -1)
(("1" (split -2)
(("1" (rewrite "gcd_sym" -2)
(("1" (rewrite "gcd_abs" +)
(("1"
(name-replace "GCD" "gcd(abs(i!1), abs(j!1))")
(("1" (grind) nil nil)
("2" (hide -1 4) (("2" (grind) nil nil)) nil))
nil))
nil))
nil)
("2" (hide -1 4) (("2" (grind) nil nil)) nil))
nil)
("2" (hide -1 4) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((gcd_lt_nat formula-decl nil gcd nil)
(gcd_abs formula-decl nil gcd 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)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(gcd const-decl "{k: posnat | divides(k, i) AND divides(k, j)}"
gcd nil)
(divides const-decl "bool" divides nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nat_min application-judgement "{k: nat | k <= i AND k <= j}"
real_defs nil)
(gcd_sym formula-decl nil gcd nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_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)
(int_abs_is_nonneg application-judgement
"{j: nonneg_int | j >= i}" real_defs nil))
nil))
(gcd_0 0
(gcd_0-1 nil 3319536974
("" (skosimp*)
(("" (typepred "ii!1")
(("" (flatten)
(("" (rewrite "gcd_abs")
(("" (rewrite "gcd_0_pos") nil nil)) nil))
nil))
nil))
nil)
((nzint nonempty-type-eq-decl nil integers 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)
(/= const-decl "boolean" notequal 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)
(gcd_abs formula-decl nil gcd nil)
(int_abs_is_nonneg application-judgement
"{j: nonneg_int | j >= i}" real_defs nil)
(abs_nat_rew formula-decl nil abs_rews nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types 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)
(gcd_0_pos formula-decl nil gcd nil))
nil))
(gcd_mod_TCC1 0
(gcd_mod_TCC1-1 nil 3407857358 ("" (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)
(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 "boolean" notequal nil)
(mod const-decl "{k | abs(k) < abs(j)}" mod nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil))
nil))
(gcd_mod_TCC2 0
(gcd_mod_TCC2-1 nil 3407857358 ("" (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)
(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 "boolean" notequal nil))
nil))
(gcd_mod 0
(gcd_mod-1 nil 3319536974
("" (skosimp*)
(("" (expand "gcd")
((""
(case "{k: posnat | divides(k, mod(j!1, i!1)) AND divides(k, i!1)}
= {k: posnat | divides(k, i!1) AND divides(k, j!1)}")
(("1" (assert) nil nil)
("2" (hide 3)
(("2" (apply-extensionality 1 :hide? t)
(("2" (rewrite "divides_mod")
(("2" (rewrite "divides_mod")
(("2" (rewrite "divides_mod")
(("2" (case-replace "mod(i!1, x!1) = 0")
(("1" (assert)
(("1" (iff 1)
(("1" (lemma "mod_0_divides")
(("1"
(inst?)
(("1"
(assert)
(("1"
(expand "divides")
(("1"
(skosimp*)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(prop)
(("1"
(assert)
(("1"
(hide -2)
(("1"
(expand "mod" -1 2)
(("1"
(name
"T1"
"floor(j!1 / (x!1 * x!2)) * x!2 ")
(("1"
(case-replace
"floor(j!1 / (x!1 * x!2)) * x!1 * x!2 = floor(j!1 / (x!1 * x!2)) * x!2 * x!1")
(("1"
(hide -1)
(("1"
(replace -1)
(("1"
(lemma
"mod_sum")
(("1"
(inst
-1
"j!1"
"x!1"
"-T1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma "mod_0_divides")
(("2"
(inst?)
(("2"
(assert)
(("2"
(expand "divides")
(("2"
(skosimp*)
(("2"
(replace -1)
(("2"
(hide -1)
(("2"
(expand
"mod"
1
2)
(("2"
(name-replace
"T1"
"div(x!1 * x!3, x!1 * x!2)")
(("2"
(hide
-1
-2)
(("2"
(case-replace
"x!1 * x!3 - T1 * x!1 * x!2 = x!1*(x!3 - T1*x!2)")
(("1"
(name-replace
"T2"
"(x!3 - T1 * x!2)")
(("1"
(grind)
nil
nil))
nil)
("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)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (assert) nil nil))
nil))
nil))
nil)
((gcd const-decl "{k: posnat | divides(k, i) AND divides(k, j)}"
gcd nil)
(divides_mod formula-decl nil divides_lems nil)
(nil application-judgement "below(m)" mod nil)
(mod_0_divides formula-decl nil mod_lems nil)
(div const-decl "integer" div nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(minus_int_is_int application-judgement "int" integers nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(mod_sum formula-decl nil mod nil)
(divides const-decl "bool" divides nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields
nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(<= const-decl "bool" reals nil)
(integer nonempty-type-from-decl nil integers nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals
nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(nzint nonempty-type-eq-decl nil integers nil)
(i!1 skolem-const-decl "int" gcd 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)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(divides const-decl "bool" divides nil)
(/= const-decl "boolean" notequal nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil)
(mod const-decl "{k | abs(k) < abs(j)}" mod nil))
nil))
(gcd_mod_div 0
(gcd_mod_div-1 nil 3319536974
("" (skosimp*)
(("" (rewrite "gcd_mod" :dir rl)
(("" (lemma "gcd_divides")
(("" (inst?)
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
nil))
nil))
nil)
((gcd_mod formula-decl nil gcd 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 "boolean" notequal nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(< const-decl "bool" reals nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil)
(mod const-decl "{k | abs(k) < abs(j)}" mod nil)
(gcd_divides formula-decl nil gcd nil))
nil))
(gcd_factors_nat_TCC1 0
(gcd_factors_nat_TCC1-1 nil 3319536974 ("" (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)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(/= const-decl "boolean" notequal nil))
nil))
(gcd_factors_nat 0
(gcd_factors_nat-1 nil 3319536974
("" (induct "m" 1 "NAT_induction")
(("1" (skosimp*)
(("1" (case-replace "j!1 = 0")
(("1" (assert)
(("1" (rewrite "gcd_sym")
(("1" (rewrite "gcd_0_pos")
(("1" (inst + "1" "1") (("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (lemma "mod_pos")
(("2" (inst - "n!1" "j!1")
(("1" (flatten)
(("1" (inst - "mod(n!1,j!1)")
(("1" (assert)
(("1" (inst - "j!1")
(("1" (assert)
(("1" (skosimp*)
(("1" (rewrite "gcd_sym" +)
(("1"
(rewrite "gcd_mod" + :dir rl)
(("1"
(rewrite "gcd_sym" +)
(("1"
(replace -3)
(("1"
(hide -3)
(("1"
(expand "mod")
(("1"
(inst
+
"jp!1"
"ip!1 - div(n!1,j!1)*jp!1")
(("1"
(assert)
(("1"
(expand "div")
(("1"
(expand "abs")
(("1"
(expand "sgn")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (skosimp*) (("2" (assert) nil nil)) nil))
nil)
((mod_pos formula-decl nil mod 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)
(div const-decl "integer" div nil)
(integer nonempty-type-from-decl nil integers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals
nil)
(div_nat formula-decl nil div nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(gcd_mod formula-decl nil gcd nil)
(n!1 skolem-const-decl "nat" gcd nil)
(mod const-decl "{k | abs(k) < abs(j)}" mod nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(j!1 skolem-const-decl "nat" gcd nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(gcd_0_pos formula-decl nil gcd nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(gcd_sym formula-decl nil gcd nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(NAT_induction formula-decl nil naturalnumbers nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(gcd const-decl "{k: posnat | divides(k, i) AND divides(k, j)}"
gcd nil)
(divides const-decl "bool" divides nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(pred type-eq-decl nil defined_types 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)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(= const-decl "[T, T -> boolean]" equalities nil))
nil))
(gcd_factors 0
(gcd_factors-1 nil 3319536974
("" (skosimp*)
(("" (rewrite "gcd_abs")
(("" (lemma "gcd_factors_nat")
(("" (inst?)
(("" (split -1)
(("1" (skosimp*)
(("1" (replace -1)
(("1" (hide -1)
(("1"
(inst + "IF i!1 < 0 THEN -ip!1 ELSE ip!1 ENDIF"
"IF j!1 < 0 THEN -jp!1 ELSE jp!1 ENDIF")
(("1" (grind) nil nil)) nil))
nil))
nil))
nil)
("2" (hide 2) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((gcd_abs formula-decl nil gcd 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)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_abs_is_nonneg application-judgement
"{j: nonneg_int | j >= i}" real_defs nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil)
(/= const-decl "boolean" notequal 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)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(< const-decl "bool" reals nil)
(minus_int_is_int application-judgement "int" integers nil)
(gcd_factors_nat formula-decl nil gcd nil))
nil))
(divides_gcd 0
(divides_gcd-1 nil 3319536974
("" (skosimp*)
(("" (expand "divides")
(("" (skosimp*)
(("" (lemma "gcd_factors")
(("" (inst?)
(("" (assert)
(("" (replace -2)
(("" (assert)
(("" (skosimp*)
(("" (replace -1)
(("" (hide -1)
(("" (hide -1)
((""
(replace -1)
((""
(hide -1)
((""
(inst
1
"ip!1 * x!1 + jp!1 * x!2 ")
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((divides const-decl "bool" divides nil)
(gcd_factors formula-decl nil gcd nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(mult_divides1 application-judgement "(divides(n))" divides
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)
(int_plus_int_is_int application-judgement "int" integers 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))
(gcd_same_TCC1 0
(gcd_same_TCC1-1 nil 3453735305 ("" (subtype-tcc) nil nil) nil
nil))
(gcd_same 0
(gcd_same-1 nil 3453735363
("" (skosimp)
(("" (expand "gcd")
(("" (rewrite "max_def")
(("1" (expand "maximum?")
(("1" (rewrite "divides_reflexive")
(("1" (skosimp)
(("1" (forward-chain "divisor_smaller")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (hide 2 -1)
(("2" (prop)
(("1" (rewrite "nonempty_exists")
(("1" (inst + "1")
(("1" (rewrite "one_divides") nil nil)) nil))
nil)
("2" (inst + "p!1")
(("2" (skolem-typepred)
(("2" (forward-chain "divisor_smaller")
(("2" (assert) nil nil)) nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.108 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.
|
