| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ints/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 160 kB |
|
SSL gcd.prfSprache: Lisp |
|||||||||||||||
|
(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)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((gcd const-decl "{k: posnat | divides(k, i) AND divides(k, j)}" gcd nil) (NOT const-decl "[bool -> bool]" booleans nil) (nonempty_exists formula-decl nil sets_lemmas nil) (one_divides formula-decl nil divides nil) (p!1 skolem-const-decl "posint" gcd nil) (maximum? const-decl "bool" max_bounded_posnat nil) (divisor_smaller formula-decl nil divides nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (divides_reflexive formula-decl nil divides nil) (posint nonempty-type-eq-decl nil integers nil) (divides const-decl "bool" divides nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals 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) (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) (max_def formula-decl nil max_bounded_posnat nil)) nil)) (gcd_minus 0 (gcd_minus-1 nil 3453735393 ("" (skosimp) (("" (expand "gcd") (("" (rewrite "congruence") (("1" (hide 3) (("1" (decompose-equality) (("1" (iff) (("1" (prop) (("1" (rewrite "divides_diff") nil nil) ("2" (lemma "divides_sum") (("2" (inst - "p!1" "q!1 - p!1" "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (prop) (("1" (rewrite "nonempty_exists") (("1" (inst + "1") (("1" (rewrite "one_divides") (("1" (rewrite "one_divides") nil nil)) nil)) nil)) nil) ("2" (inst + "p!1") (("2" (skolem-typepred) (("2" (use "divisor_smaller") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (prop) (("1" (rewrite "nonempty_exists") (("1" (inst + "1") (("1" (rewrite "one_divides") (("1" (rewrite "one_divides") nil nil)) nil)) nil)) nil) ("2" (inst + "p!1") (("2" (skolem-typepred) (("2" (use "divisor_smaller") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((gcd const-decl "{k: posnat | divides(k, i) AND divides(k, j)}" gcd nil) (divisor_smaller formula-decl nil divides nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (nonempty_exists formula-decl nil sets_lemmas nil) (one_divides formula-decl nil divides nil) (q!1 skolem-const-decl "posint" gcd nil) (p!1 skolem-const-decl "posint" gcd nil) (divides_sum formula-decl nil divides nil) (divides_diff formula-decl nil divides nil) (<= const-decl "bool" reals 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) (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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posint nonempty-type-eq-decl nil integers nil) (divides const-decl "bool" divides nil) (max const-decl "{a: posnat | S(a) AND (FORALL x: S(x) IMPLIES x <= a)}" max_bounded_posnat nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (congruence formula-decl nil functions nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (gcd_times_TCC1 0 (gcd_times_TCC1-1 nil 3453735305 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posint nonempty-type-eq-decl nil integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil)) nil)) (gcd_times 0 (gcd_times-2 nil 3453735638 ("" (measure-induct+ "p + q" (p q)) (("1" (skosimp) (("1" (case-replace "x!1 = x!2") (("1" (hide -2) (("1" (rewrite "gcd_same") (("1" (rewrite "gcd_same") nil nil)) nil)) nil) ("2" (case "x!1 < x!2") (("1" (rewrite "gcd_minus" +) (("1" (swap-rel 2) (("1" (rewrite "gcd_minus" +) (("1" (swap-rel 2) (("1" (inst?) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (cancel-by -1 "l!1") nil nil)) nil)) nil) ("2" (rewrite "gcd_sym") (("2" (rewrite "gcd_minus" +) (("1" (swap-rel 3) (("1" (rewrite "gcd_sym" +) (("1" (rewrite "gcd_minus" +) (("1" (swap-rel 3) (("1" (inst?) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (cancel-by -1 "l!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (hide 2) (("3" (skosimp) (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp) (("4" (assert) nil nil)) nil) ("5" (assert) (("5" (hide-all-but 1) (("5" (skosimp) (("5" (assert) nil nil)) nil)) nil)) nil) ("6" (hide-all-but 1) (("6" (skosimp) (("6" (assert) nil nil)) nil)) nil) ("7" (hide-all-but 1) (("7" (skosimp) (("7" (assert) nil nil)) nil)) nil) ("8" (assert) nil nil) ("9" (hide-all-but 1) (("9" (skosimp) (("9" (assert) nil nil)) nil)) nil) ("10" (assert) nil nil)) nil) ((posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (both_sides_times1_imp formula-decl nil extra_real_props nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (int_plus_int_is_int application-judgement "int" integers nil) (x!1 skolem-const-decl "posint" gcd nil) (x!2 skolem-const-decl "posint" gcd nil) (real_ge_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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (gcd_minus formula-decl nil gcd nil) (gcd_sym formula-decl nil gcd nil) (gcd_same formula-decl nil gcd 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 "boolean" notequal nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (posint 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) (measure_induction formula-decl nil measure_induction nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) nil) (gcd_times-1 nil 3453735428 (";;; Proof gcd_times-1 for formula gcd_fractions.gcd_times" (measure-induct+ "p + q" (p q)) (("1" (skosimp) (("1" (case-replace "x!1 = x!2") (("1" (hide -2) (("1" (rewrite "gcd_same") (("1" (rewrite "gcd_same") nil))))) ("2" (case "x!1 < x!2") (("1" (rewrite "gcd_minus" +) (("1" (swap-rel 2) (("1" (rewrite "gcd_minus" +) (("1" (swap-rel 2) (("1" (inst?) (("1" (assert) nil) ("2" (assert) nil))))))))) ("2" (flatten) (("2" (cancel-by -1 "k!1") nil))))) ("2" (rewrite "gcd_sym") (("2" (rewrite "gcd_minus" +) (("1" (swap-rel 3) (("1" (rewrite "gcd_sym" +) (("1" (rewrite "gcd_minus" +) (("1" (swap-rel 3) (("1" (inst?) (("1" (assert) nil) ("2" (assert) nil))))))))))) ("2" (flatten) (("2" (cancel-by -1 "k!1") nil))))))))))))) ("2" (assert) nil) ("3" (hide 2) (("3" (skosimp) (("3" (assert) nil))))) ("4" (skosimp) (("4" (assert) nil))) ("5" (assert) (("5" (hide-all-but 1) (("5" (skosimp) (("5" (assert) nil))))))) ("6" (hide-all-but 1) (("6" (skosimp) (("6" (assert) nil))))) ("7" (hide-all-but 1) (("7" (skosimp) (("7" (assert) nil))))) ("8" (assert) nil) ("9" (hide-all-but 1) (("9" (skosimp) (("9" (assert) nil))))) ("10" (assert) nil)) ";;; developed with shostak decision procedures") nil nil)) (rel_prime_lem 0 (rel_prime_lem-1 nil 3408109358 ("" (skosimp*) (("" (expand "rel_prime") (("" (split +) (("1" (flatten) (("1" (lemma "gcd_factors") (("1" (inst?) (("1" (replace -3) (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (skosimp*) (("2" (name "K" "gcd(i!1, j!1)") (("2" (replace -1) (("2" (case "divides(K, i!1) AND divides(K, j!1)") (("1" (flatten) (("1" (expand "divides") (("1" (skosimp*) (("1" (replace -1) (("1" (hide -1) (("1" (replace -1) (("1" (hide -1) (("1" (factor -2) (("1" (name "MM" "(m!1 * x!1 + n!1 * x!2)") (("1" (replace -1) (("1" (lemma "product_1") (("1" (inst - "K" "MM") (("1" (assert) (("1" (lemma "pos_times_le") (("1" (inst - "K" "MM") (("1" (assert) 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)) nil)) nil) ((mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (rel_prime const-decl "bool" gcd 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) (>= const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities 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) (pos_times_le formula-decl nil real_props 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) (product_1 formula-decl nil real_props 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) (gcd_factors formula-decl nil gcd nil)) shostak)) (rel_prime_div_prod 0 (rel_prime_div_prod-1 nil 3539695165 ("" (skeep) (("" (case "i = 0 OR j = 0") (("1" (case "i = 0") (("1" (assert) (("1" (hide -2) (("1" (replace -1) (("1" (expand "rel_prime" -) (("1" (rewrite "gcd_0") (("1" (case "k = 0") (("1" (replace -1) (("1" (expand "divides" +) (("1" (propax) nil nil)) nil)) nil) ("2" (expand "divides") (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace -1) (("2" (expand "rel_prime") (("2" (rewrite "gcd_sym") (("2" (rewrite "gcd_0") (("2" (expand "divides") (("2" (copy 2) (("2" (inst + "k") (("2" (inst + "-k") (("2" (expand "abs") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (hide -1) (("2" (rewrite "rel_prime_lem" -1) (("2" (skosimp*) (("2" (mult-by -1 "k") (("2" (assert) (("2" (replace -1 +) (("2" (assert) (("2" (expand "divides" -) (("2" (skosimp*) (("2" (replace -2) (("2" (expand "divides") (("2" (inst + "k*m!1+n!1*x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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 "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (gcd_sym formula-decl nil gcd 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) (/= const-decl "boolean" notequal nil) (gcd_0 formula-decl nil gcd 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) (even_times_int_is_even application-judgement "even_int" integers nil) (divides const-decl "bool" divides nil) (rel_prime const-decl "bool" gcd nil) (int_plus_int_is_int application-judgement "int" integers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (both_sides_times1_imp formula-decl nil extra_real_props nil) (rel_prime_lem formula-decl nil gcd nil)) shostak)) (rel_prime_sym 0 (rel_prime_sym-1 nil 3539711449 ("" (skeep) (("" (expand "rel_prime") (("" (rewrite "gcd_sym") nil nil)) nil)) nil) ((rel_prime const-decl "bool" gcd 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_sym formula-decl nil gcd nil)) nil)) (rel_prime_mult_right_TCC1 0 (rel_prime_mult_right_TCC1-1 nil 3539712193 ("" (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) (divides const-decl "bool" divides nil) (gcd const-decl "{k: posnat | divides(k, i) AND divides(k, j)}" gcd nil) (rel_prime const-decl "bool" gcd nil)) nil)) (rel_prime_mult_right_TCC2 0 (rel_prime_mult_right_TCC2-1 nil 3539712193 ("" (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) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (divides const-decl "bool" divides nil) (gcd const-decl "{k: posnat | divides(k, i) AND divides(k, j)}" gcd nil) (rel_prime const-decl "bool" gcd nil) (/= const-decl "boolean" notequal nil)) nil)) (rel_prime_mult_right 0 (rel_prime_mult_right-1 nil 3539712194 ("" (skeep) (("" (rewrite "rel_prime_lem") (("" (rewrite "rel_prime_lem") (("" (skosimp*) (("" (rewrite "rel_prime_lem") (("1" (mult-eq -3 -4) (("1" (assert) (("1" (inst + "n!1*n!2" "i*m!1*m!2+k*m!1*n!2+j*m!2*n!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "j = 0 OR k = 0") (("1" (ground) nil nil) ("2" (lemma "nzreal_times_nzreal_is_nzreal") (("2" (inst - "j" "k") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((rel_prime_lem 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) (nzreal_times_nzreal_is_nzreal judgement-tcc nil real_types nil) (nzreal nonempty-type-eq-decl nil reals nil) (k skolem-const-decl "int" gcd nil) (j skolem-const-decl "int" gcd nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (odd_times_odd_is_odd application-judgement "odd_int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil)) shostak)) (rel_prime_mult_left_TCC1 0 (rel_prime_mult_left_TCC1-1 nil 3539712538 ("" (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) (divides const-decl "bool" divides nil) (gcd const-decl "{k: posnat | divides(k, i) AND divides(k, j)}" gcd nil) (rel_prime const-decl "bool" gcd nil)) nil)) (rel_prime_mult_left_TCC2 0 (rel_prime_mult_left_TCC2-1 nil 3539712538 ("" (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) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (divides const-decl "bool" divides nil) (gcd const-decl "{k: posnat | divides(k, i) AND divides(k, j)}" gcd nil) (rel_prime const-decl "bool" gcd nil) (/= const-decl "boolean" notequal nil)) nil)) (rel_prime_mult_left 0 (rel_prime_mult_left-1 nil 3539712539 ("" (skeep) (("" (rewrite "rel_prime_sym" -3) (("" (rewrite "rel_prime_sym" -4) (("" (rewrite "rel_prime_sym" +) (("1" (lemma "rel_prime_mult_right") (("1" (inst - "j" "i" "k") (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (lemma "nzreal_times_nzreal_is_nzreal") (("2" (inst - "i" "k") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((rel_prime_sym 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 -> numfield]" number_fields nil) (rel_prime_mult_right formula-decl nil gcd nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (nzreal_times_nzreal_is_nzreal judgement-tcc nil real_types nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil)) shostak)) (compute_gcd_TCC1 0 (compute_gcd_TCC1-1 nil 3586790620 ("" (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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal nil) (int_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) (minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil)) (compute_gcd_TCC2 0 (compute_gcd_TCC2-1 nil 3586790620 ("" (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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal 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_plus_int_is_int application-judgement "int" integers nil) (minus_int_is_int application-judgement "int" integers nil)) nil)) (compute_gcd_TCC3 0 (compute_gcd_TCC3-1 nil 3586790620 ("" (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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal 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) (int_plus_int_is_int application-judgement "int" integers nil)) nil)) (compute_gcd_TCC4 0 (compute_gcd_TCC4-1 nil 3586790620 ("" (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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal 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_plus_int_is_int application-judgement "int" integers nil)) nil)) (compute_gcd_TCC5 0 (compute_gcd_TCC5-1 nil 3586790620 ("" (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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal 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_plus_int_is_int application-judgement "int" integers nil)) nil)) (compute_gcd_TCC6 0 (compute_gcd_TCC6-1 nil 3586790620 ("" (termination-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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities 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) (/= const-decl "boolean" notequal nil)) nil)) (compute_gcd_TCC7 0 (compute_gcd_TCC7-1 nil 3586790620 ("" (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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal 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) (minus_int_is_int application-judgement "int" integers nil)) nil)) (compute_gcd_TCC8 0 (compute_gcd_TCC8-1 nil 3586790620 ("" (skeep) (("" (typepred "v(-i,j)") (("1" (rewrite "gcd_abs" -) (("1" (rewrite "gcd_abs" +) nil nil)) nil) ("2" (assert) nil nil)) nil)) 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (numfield nonempty-type-eq-decl nil number_fields 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) (minus_int_is_int application-judgement "int" integers 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) (abs_neg_rew formula-decl nil abs_rews nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (gcd_abs formula-decl nil gcd nil)) nil)) (compute_gcd_TCC9 0 (compute_gcd_TCC9-1 nil 3586790620 ("" (termination-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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities 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) (/= const-decl "boolean" notequal nil)) nil)) (compute_gcd_TCC10 0 (compute_gcd_TCC10-1 nil 3586790620 ("" (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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (minus_int_is_int application-judgement "int" integers nil)) nil)) (compute_gcd_TCC11 0 (compute_gcd_TCC11-1 nil 3586790620 ("" (skeep) (("" (typepred "v(i,-j)") (("1" (rewrite "gcd_abs" -) (("1" (rewrite "gcd_abs" +) nil nil)) nil) ("2" (assert) nil nil)) nil)) 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (numfield nonempty-type-eq-decl nil number_fields 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) (minus_int_is_int application-judgement "int" integers 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) (abs_neg_rew formula-decl nil abs_rews nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (gcd_abs formula-decl nil gcd nil)) nil)) (compute_gcd_TCC12 0 (compute_gcd_TCC12-1 nil 3586790620 ("" (skeep) (("" (replace -1) (("" (assert) (("" (typepred "j") (("" (assert) (("" (rewrite "gcd_0_pos") nil nil)) nil)) nil)) nil)) nil)) nil) ((/= const-decl "boolean" notequal 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 "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (gcd_0_pos formula-decl nil gcd 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_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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (compute_gcd_TCC13 0 (compute_gcd_TCC13-1 nil 3586790620 ("" (skeep) (("" (assert) (("" (replace -1) (("" (rewrite "gcd_sym") (("" (rewrite "gcd_0_pos") nil nil)) nil)) nil)) nil)) 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) (gcd_sym 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) (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) (gcd_0_pos formula-decl nil gcd nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil)) nil)) (compute_gcd_TCC14 0 (compute_gcd_TCC14-1 nil 3586790620 ("" (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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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)) nil)) (compute_gcd_TCC15 0 (compute_gcd_TCC15-1 nil 3586790620 ("" (skosimp*) (("" (typepred "v!1(j!1,i!1)") (("1" (replace -2) (("1" (lemma "gcd_sym") (("1" (inst?) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (numfield nonempty-type-eq-decl nil number_fields 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) (gcd_sym formula-decl nil gcd nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (compute_gcd_TCC16 0 (compute_gcd_TCC16-2 nil 3591024730 ("" (skeep) (("" (skeep) (("" (typepred "rem") (("" (assert) (("" (replace -2) (("" (expand "mod") (("" (case "i = j*floor(i/j)") (("1" (name "a" "floor(i/j)") (("1" (replaces -1) (("1" (replaces -1) (("1" (hide -) (("1" (lemma "gcd_def") (("1" (inst - "j*a" "j" "j") (("1" (assert) (("1" (expand "divides") (("1" (ground) (("1" (inst + "a") nil nil) ("2" (inst + "1") (("2" (assert) nil nil)) nil) ("3" (skeep) (("3" (skosimp*) (("3" (typepred "mm") (("3" (case "x!2 <= 0") (("1" (mult-by -2 "-x!2") (("1" (assert) nil nil)) nil) ("2" (case "x!2 >=1") (("1" (mult-by -1 "mm") (("1" (assert) nil nil)) nil) ("2" (assert) 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)) 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (abs_nat_rew formula-decl nil abs_rews nil) (int_minus_int_is_int application-judgement "int" integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (gcd_def formula-decl nil gcd nil) (even_times_int_is_even application-judgement "even_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (x!2 skolem-const-decl "int" gcd nil) (posreal nonempty-type-eq-decl nil real_types nil) (both_sides_times_pos_gt1 formula-decl nil real_props nil) (minus_int_is_int application-judgement "int" integers nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (divides const-decl "bool" divides nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (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) (>= 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) (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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal nil)) nil) (compute_gcd_TCC16-1 nil 3586790620 ("" (skeep) (("" (skeep) (("" (replace -1) (("" (lemma "gcd_mod") (("" (inst - "j" "i") (("" (assert) (("" (replace -3 :dir rl) (("" (rewrite "gcd_0") (("" (lemma "gcd_sym") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((abs_nat_rew formula-decl nil abs_rews nil)) nil)) (compute_gcd_TCC17 0 (compute_gcd_TCC17-1 nil 3586790620 ("" (skeep) (("" (assert) (("" (skeep) (("" (case "NOT divides(j,i)") (("1" (expand "mod") (("1" (expand "divides") (("1" (inst + "floor(i/j)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "gcd_def") (("2" (inst - "i" "j" "j") (("2" (assert) (("2" (split) (("1" (expand "divides" 1) (("1" (inst + "1") (("1" (assert) nil nil)) nil)) nil) ("2" (skeep) (("2" (expand "divides" -2) (("2" (skeep -2) (("2" (case "NOT x>0") (("1" (mult-by 1 "mm") (("1" (assert) nil nil)) nil) ("2" (case "NOT x>=1") (("1" (assert) nil nil) ("2" (mult-by -1 "mm") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (compute_gcd_TCC18 0 (compute_gcd_TCC18-1 nil 3586790620 ("" (skeep) (("" (skeep) (("" (assert) (("" (case "rem > 0") (("1" (assert) (("1" (lift-if) (("1" (case "rem<i") (("1" (assert) (("1" (split +) (("1" (flatten) (("1" (assert) (("1" (typepred "mod(i,j)") (("1" (replace -5 :dir rl) (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (assert) (("2" (typepred "mod(i,j)") (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 8) (("2" (expand "mod" -1) (("2" (replaces -1) (("2" (typepred "floor(i/j)") (("2" (mult-by -1 "j") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((/= const-decl "boolean" notequal nil) (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (>= const-decl "bool" reals 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) (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) (NOT const-decl "[bool -> bool]" booleans nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (<= const-decl "bool" reals nil) (integer nonempty-type-from-decl nil integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_cancel2 formula-decl nil real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props 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)) nil)) (compute_gcd_TCC19 0 (compute_gcd_TCC19-2 nil 3591024818 ("" (skosimp*) (("" (typepred "v!1(j!1,rem!1)") (("1" (replaces -2) (("1" (replace -2) (("1" (assert) (("1" (rewrite "gcd_sym" +) (("1" (rewrite "gcd_mod") (("1" (rewrite "gcd_sym" +) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (nonneg_real nonempty-type-eq-decl nil real_types 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (numfield nonempty-type-eq-decl nil number_fields 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) (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (gcd_sym formula-decl nil gcd nil) (gcd_mod 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)) nil) (compute_gcd_TCC19-1 nil 3586790620 ("" (skeep) (("" (skeep) (("" (typepred "v(j,rem)") (("1" (replace -3) (("1" (replace -2) (("1" (copy 7) (("1" (hide 8) (("1" (hide -) (("1" (invoke (name "A1" "%1") (! 1 1)) (("1" (invoke (name "A2" "%1") (! 1 2)) (("1" (replace -1) (("1" (replace -2) (("1" (case "divides(A1,A2) AND divides(A2,A1)") (("1" (flatten) (("1" (expand "divides") (("1" (skosimp*) (("1" (copy -2) (("1" (replace -2 -1) (("1" (case "x!1 = 0") (("1" (assert) nil nil) ("2" (case "x!2 = 0") (("1" (assert) nil nil) ("2" (case "x!1 < 0") (("1" (mult-by -1 "A1") (("1" (assert) nil nil)) nil) ("2" (case "x!2 < 0") (("1" (mult-by -1 "A2") (("1" (assert) nil nil)) nil) ("2" (case "x!1 = 1 OR x!2 = 1") (("1" (ground) nil nil) ("2" (flatten) (("2" (case "x!1 > 1") (("1" (case "x!2 > 1") (("1" (mult-ineq -1 -2) (("1" (assert) (("1" (mult-by -1 "A1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split +) (("1" (postpone) nil nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil) nil nil)) (compute_gcd_TCC20 0 (compute_gcd_TCC20-1 nil 3586790953 ("" (skeep) (("" (skeep) (("" (typepred "v(j,rem)") (("1" (replace -2) (("1" (hide -2) (("1" (assert) (("1" (case "EXISTS (kk:int): i = kk*j + rem") (("1" (skeep -1) (("1" (lemma "gcd_def") (("1" (inst - "i" "j" "gcd(j,rem)") (("1" (assert) (("1" (split +) (("1" (typepred "gcd(j,rem)") (("1" (expand "divides") (("1" (skolem -2 "xj") (("1" (skolem -3 "xrem") (("1" (inst + "xj*kk + xrem") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "gcd_def") (("2" (inst - "j" "rem" "gcd(j,rem)") (("2" (assert) (("2" (skeep) (("2" (inst - "mm") (("2" (assert) (("2" (expand "divides") (("2" (skolem -1 "xi") (("2" (skolem -2 "xj") (("2" (inst + "xi - kk*xj") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "mod") (("2" (inst + "floor(i/j)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) nil nil)) nil)) nil)) nil) nil nil)) (rel_prime_inverse_TCC1 0 (rel_prime_inverse_TCC1-1 nil 3542976467 ("" (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) (real_ge_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) (/= const-decl "boolean" notequal nil)) nil)) (rel_prime_inverse_TCC2 0 (rel_prime_inverse_TCC2-1 nil 3542976467 ("" (subtype-tcc) nil nil) ((divides const-decl "bool" divides nil) (gcd const-decl "{k: posnat | divides(k, i) AND divides(k, j)}" gcd nil) (rel_prime const-decl "bool" gcd nil)) nil)) (rel_prime_inverse 0 (rel_prime_inverse-1 nil 3542976469 ("" (lemma "pigeonhole_principle_nat") (("" (skeep) (("" (inst - "m" "LAMBDA (k:below(m)): mod(n*k,m)") (("1" (flatten) (("1" (hide -1) (("1" (expand "bijective?") (("1" (ground) (("1" (expand "surjective?") (("1" (propax) nil nil)) nil) ("2" (hide (2 3)) (("2" (expand "injective?") (("2" (skeep) (("2" (case "NOT divides(m,n*x1-n*x2)") (("1" (expand "mod") (("1" (expand "divides") (("1" (inst + "floor(n*x1/m)-floor(n*x2/m)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -2) (("2" (lemma "rel_prime_div_prod") (("2" (inst - "m" "n" "x1-x2") (("2" (assert) (("2" (split -) (("1" (typepred "x1") (("1" (typepred "x2") (("1" (case "NOT abs(x1-x2)<m") (("1" (hide-all-but (-1 -2 1)) (("1" (grind) nil nil)) nil) ("2" (expand "divides" -4) (("2" (skosimp*) (("2" (replace -4) (("2" (rewrite "abs_mult") (("2" (case "x!1 = 0") (("1" (assert) nil nil) ("2" (case "abs(x!1)>=1") (("1" (mult-by -1 "m") (("1" (assert) nil nil)) nil) ("2" (hide -) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "rel_prime_sym") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (skeep) (("2" (assert) (("2" (typepred "mod(n*k,m)") (("2" (assert) (("2" (lemma "mod_pos") (("2" (inst?) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (mod_pos formula-decl nil mod nil) (bijective? const-decl "bool" functions nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (abs_nat_rew formula-decl nil abs_rews nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (abs_mult formula-decl nil 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) (minus_int_is_int application-judgement "int" integers nil) (rel_prime_sym formula-decl nil gcd nil) (rel_prime_div_prod formula-decl nil gcd nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals 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) (divides const-decl "bool" divides nil) (NOT const-decl "[bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (injective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (< const-decl "bool" reals nil) (m skolem-const-decl "nat" gcd nil) (below type-eq-decl nil naturalnumbers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (nonzero_integer nonempty-type-eq-decl nil integers 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) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (n skolem-const-decl "nat" gcd nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (pigeonhole_principle_nat formula-decl nil pigeonhole nil)) shostak)))
¤ 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.0.180Bemerkung: (vorverarbeitet am 2026-05-06) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26