| products/sources/formale sprachen/PVS/Sturm/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: trig_basic.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(gcd_coeff
(gcd_coeff_TCC1 0 (gcd_coeff_TCC1-1 nil 3586799415 ("" (subtype-tcc) nil nil) ((listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (divides const-decl "bool" divides nil)) nil)) (gcd_coeff_TCC2 0 (gcd_coeff_TCC2-1 nil 3586799415 ("" (grind) nil nil) ((listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (gcd_coeff_TCC3 0 (gcd_coeff_TCC3-1 nil 3586799415 ("" (skeep) (("" (skeep) (("" (replace -1) (("" (case "ii = 0") (("1" (replaces -1) (("1" (assert) (("1" (expand "divides" 2) (("1" (inst + "sign(nth(ll,0))") (("1" (grind :exclude "nth") nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) 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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers 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) (/= const-decl "boolean" notequal nil) (nzint nonempty-type-eq-decl nil integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (Sign type-eq-decl nil sign "reals/") (sign const-decl "Sign" sign "reals/") (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_int_is_int application-judgement "int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (divides const-decl "bool" divides nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil)) nil)) (gcd_coeff_TCC4 0 (gcd_coeff_TCC4-1 nil 3586799415 ("" (grind) nil nil) ((listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (divides const-decl "bool" divides nil) (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (length def-decl "nat" list_props nil) (< const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil)) nil)) (gcd_coeff_TCC5 0 (gcd_coeff_TCC5-1 nil 3586799415 ("" (skeep) (("" (skeep) (("" (skeep) (("" (expand "nth" +) (("" (lift-if) (("" (ground) (("1" (expand "divides") (("1" (inst + "0") (("1" (assert) nil nil)) nil)) nil) ("2" (typepred "oldgcd") (("2" (inst?) (("2" (assert) (("2" (expand "length" -3) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nth def-decl "T" list_props 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) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (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) (divides const-decl "bool" divides nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (length def-decl "nat" list_props nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) (below type-eq-decl nil nat_types nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil)) nil)) (gcd_coeff_TCC6 0 (gcd_coeff_TCC6-1 nil 3587216897 ("" (skosimp*) (("" (expand "divides") (("" (inst + "nth[int](ll!1,ii!1)") (("" (assert) nil nil)) nil)) nil)) nil) ((divides const-decl "bool" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_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) (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (ii!1 skolem-const-decl "nat" gcd_coeff nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (length def-decl "nat" list_props nil) (ll!1 skolem-const-decl "list[int]" gcd_coeff nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff nil)) nil)) (gcd_coeff_TCC7 0 (gcd_coeff_TCC7-1 nil 3587224542 ("" (skeep) (("" (expand "length" 4 2) (("" (grind) nil nil)) nil)) nil) ((/= const-decl "boolean" notequal 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 "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) (divides const-decl "bool" divides nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (length def-decl "nat" list_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil)) nil)) (gcd_coeff_TCC8 0 (gcd_coeff_TCC8-1 nil 3587224542 ("" (skeep) (("" (skeep) (("" (skeep) (("" (typepred "compute_gcd(car[int](ll), oldgcd)") (("" (replaces -2) (("" (hide -1) (("" (typepred "gcd(car[int](ll), oldgcd)") (("" (expand "nth" +) (("" (lift-if) (("" (assert) (("" (split +) (("1" (propax) nil nil) ("2" (flatten) (("2" (typepred "oldgcd") (("2" (inst?) (("1" (assert) (("1" (split -) (("1" (expand "divides" (-1 -4 2)) (("1" (skosimp*) (("1" (inst + "x!1*x!2") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "length" -5) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) (length def-decl "nat" list_props nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (compute_gcd def-decl "{kj: posnat | kj = gcd(i, j)}" gcd "ints/") (gcd const-decl "{k: posnat | divides(k, i) AND divides(k, j)}" gcd "ints/") (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_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (int_minus_int_is_int application-judgement "int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (ii skolem-const-decl "nat" gcd_coeff nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil)) nil)) (gcd_coeff_TCC9 0 (gcd_coeff_TCC9-1 nil 3587224542 ("" (grind) nil nil) ((listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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)) nil)) (gcd_coeff_TCC10 0 (gcd_coeff_TCC10-1 nil 3594031418 ("" (skeep) (("" (expand "length" 3 2) (("" (lift-if) (("" (ground) (("" (grind) nil nil)) nil)) nil)) nil)) nil) ((length def-decl "nat" list_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil)) nil)) (gcd_coeff_nonzero 0 (gcd_coeff_nonzero-1 nil 3593259974 ("" (skeep) (("" (typepred "gcd_coeff(l)") (("" (skeep) (("" (assert) (("" (inst - "i") (("" (assert) (("" (replaces -2) (("" (expand "divides") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((gcd_coeff def-decl "{m: nat | FORALL (ii: nat): ii < length[int](ll) IMPLIES divides(m, nth[int](ll, ii))}" gcd_coeff nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (divides const-decl "bool" divides nil) (length def-decl "nat" list_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (< const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (below type-eq-decl nil naturalnumbers nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil)) shostak)) (gcd_coeff_zero 0 (gcd_coeff_zero-1 nil 3612883501 ("" (induct "l") (("1" (grind) nil nil) ("2" (skolem 1 ("ii" "ll")) (("2" (flatten) (("2" (assert) (("2" (split -1) (("1" (expand "gcd_coeff" +) (("1" (lift-if) (("1" (ground) (("1" (inst - "0") (("1" (assert) (("1" (replace -3) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (inst - "0") (("2" (assert) (("2" (expand "nth" -2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (inst - "i+1") (("2" (assert) (("2" (split -) (("1" (expand "nth" -1) (("1" (propax) nil nil)) nil) ("2" (expand "length" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_posint_is_posint application-judgement "posint" integers 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (abs_0_rew formula-decl nil abs_rews "ints/") (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (list_induction formula-decl nil list_adt 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) (gcd_coeff def-decl "{m: nat | FORALL (ii: nat): ii < length[int](ll) IMPLIES divides(m, nth[int](ll, ii))}" gcd_coeff nil) (divides const-decl "bool" divides nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (length def-decl "nat" list_props nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (list type-decl nil list_adt nil)) shostak)) (descalarize_list_TCC1 0 (descalarize_list_TCC1-1 nil 3586800317 ("" (subtype-tcc) nil nil) ((listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (below type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (< const-decl "bool" reals nil)) nil)) (descalarize_list_TCC2 0 (descalarize_list_TCC2-1 nil 3586800317 ("" (grind) nil nil) ((listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (nzint nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (divides const-decl "bool" divides nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (below type-eq-decl nil naturalnumbers nil)) nil)) (descalarize_list_TCC3 0 (descalarize_list_TCC3-1 nil 3586800317 ("" (skeep) (("" (typepred "k") (("" (skeep) (("" (inst - "ii+1") (("" (expand "length" -2 1) (("" (assert) (("" (expand "divides") (("" (skosimp*) (("" (inst + "x!1") (("" (expand "nth" -2) (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (divides const-decl "bool" divides nil) (length def-decl "nat" list_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (< const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals 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) (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil)) nil)) (descalarize_list_TCC4 0 (descalarize_list_TCC4-1 nil 3586800317 ("" (skeep) (("" (typepred "k") (("" (inst - "0") (("" (assert) (("" (split -) (("1" (expand "nth") (("1" (name "crr" "car(ll)") (("1" (replace -1) (("1" (hide -1) (("1" (expand "divides") (("1" (skosimp*) (("1" (case "crr/k = x!1") (("1" (assert) nil nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (divides const-decl "bool" divides nil) (length def-decl "nat" list_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (< const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_cancel3 formula-decl nil real_props nil) (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil)) nil)) (descalarize_list_TCC5 0 (descalarize_list_TCC5-1 nil 3593259903 ("" (skeep) (("" (skeep) (("" (typepred "k") (("" (assert) (("" (inst - "ii+1") (("" (assert) (("" (split -) (("1" (expand "nth" -1) (("1" (propax) nil nil)) nil) ("2" (expand "length" 1) (("2" (assert) 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_posint_is_posint application-judgement "posint" integers 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) (/= const-decl "boolean" notequal 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) (nzint nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (length def-decl "nat" list_props nil) (divides const-decl "bool" divides nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil)) nil)) (descalarize_list_TCC6 0 (descalarize_list_TCC6-1 nil 3593259903 ("" (termination-tcc) nil nil) ((listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (nzint nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (divides const-decl "bool" divides nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (descalarize_list_TCC7 0 (descalarize_list_TCC7-1 nil 3593259903 ("" (skeep) (("" (assert) (("" (split +) (("1" (expand "length" + 1) (("1" (typepred "v(cdr[int](ll),k)") (("1" (replace -2 +) (("1" (hide -) (("1" (expand "length" + 2) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (skeep) (("2" (typepred "k") (("2" (inst - "ii+1") (("2" (assert) (("2" (split -) (("1" (expand "nth" -) (("1" (propax) nil nil)) nil) ("2" (expand "length" + 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (skeep) (("2" (typepred "i") (("2" (typepred "v(cdr[int](ll),k)") (("1" (expand "nth" + 1) (("1" (case "i = 0") (("1" (assert) (("1" (expand "nth" +) (("1" (assert) (("1" (field) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst - "i-1") (("2" (replace -3) (("2" (assert) (("2" (expand "nth" + 2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (typepred "k") (("2" (hide 2) (("2" (inst - "ii+1") (("2" (split -) (("1" (expand "nth" -1) (("1" (propax) nil nil)) nil) ("2" (expand "length" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (length def-decl "nat" list_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_posint_is_posint application-judgement "posint" integers 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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (nzint nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (divides const-decl "bool" divides nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil)) nil)) (primitize_list_TCC1 0 (primitize_list_TCC1-1 nil 3586800317 ("" (subtype-tcc) nil nil) ((listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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 "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (/= const-decl "boolean" notequal nil) (divides const-decl "bool" divides nil)) nil)) (primitize_list_def_TCC1 0 (primitize_list_def_TCC1-1 nil 3593259479 ("" (subtype-tcc) nil nil) ((listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (divides const-decl "bool" divides nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil)) nil)) (primitize_list_def 0 (primitize_list_def-1 nil 3593259507 ("" (skeep) (("" (skeep) (("" (split +) (("1" (expand "primitize_list") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (skoletin 1) (("2" (assert) (("2" (lemma "gcd_coeff_nonzero") (("2" (inst?) (("2" (split -) (("1" (flatten) (("1" (assert) (("1" (skeep) (("1" (expand "primitize_list") (("1" (assert) (("1" (lift-if) (("1" (ground) (("1" (typepred "descalarize_list(l, gcd_coeff(l))") (("1" (inst - "k") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "i") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "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 "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (length def-decl "nat" list_props nil) (divides const-decl "bool" divides nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (> const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (gcd_coeff def-decl "{m: nat | FORALL (ii: nat): ii < length[int](ll) IMPLIES divides(m, nth[int](ll, ii))}" gcd_coeff nil) (below type-eq-decl nil naturalnumbers nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (gcd_coeff_nonzero formula-decl nil gcd_coeff nil) (NOT const-decl "[bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (nzint nonempty-type-eq-decl nil integers nil) (descalarize_list def-decl "{nl: list[int] | length[int](nl) = length[int](ll) AND (FORALL (i: below(length[int](ll))): nth[int](ll, i) = k * nth[int](nl, i))}" gcd_coeff nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (primitize_list const-decl "list[int]" gcd_coeff nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil)) shostak)) (primitize_zero_list 0 (primitize_zero_list-1 nil 3612884367 ("" (skeep) (("" (expand "primitize_list") (("" (lift-if) (("" (ground) (("1" (lemma "list_extensionality[int]") (("1" (inst - "l" "array2list[int](length[int](l))(LAMBDA (i: nat): 0)") (("1" (assert) (("1" (hide 2) (("1" (skosimp*) (("1" (typepred "array2list[int](length[int](l))(LAMBDA (i: nat): 0)") (("1" (inst -3 "n!1") (("1" (assert) (("1" (inst - "n!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "gcd_coeff_zero") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil) ("3" (lemma "gcd_coeff_zero") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((primitize_list const-decl "list[int]" gcd_coeff nil) (list type-decl nil list_adt nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (length def-decl "nat" list_props nil) (listn type-eq-decl nil listn "structures/") (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (list_extensionality formula-decl nil more_list_props "structures/") (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) (gcd_coeff_zero formula-decl nil gcd_coeff nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil)) shostak)) (primitize_list_length 0 (primitize_list_length-1 nil 3593770729 ("" (skeep) (("" (expand "primitize_list") (("" (lift-if) (("" (ground) nil nil)) nil)) nil)) nil) ((primitize_list const-decl "list[int]" gcd_coeff nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil)) shostak)) (nonzero_version_rec_TCC1 0 (nonzero_version_rec_TCC1-1 nil 3593340485 ("" (subtype-tcc) nil nil) ((listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_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_minus_int_is_int application-judgement "int" integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil)) nil)) (nonzero_version_rec_TCC2 0 (nonzero_version_rec_TCC2-1 nil 3593340485 ("" (skeep) (("" (assert) (("" (hide -2) (("" (hide-all-but (-1 1)) (("" (grind) nil nil)) nil)) nil)) nil)) 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) (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil)) nil)) (nonzero_version_rec_TCC3 0 (nonzero_version_rec_TCC3-1 nil 3593340485 ("" (grind) nil nil) ((listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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)) nil)) (nonzero_version_rec_TCC4 0 (nonzero_version_rec_TCC4-1 nil 3593340485 ("" (subtype-tcc) nil nil) ((listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff 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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil)) nil)) (nonzero_version_rec_TCC5 0 (nonzero_version_rec_TCC5-1 nil 3593340485 ("" (skeep) (("" (expand "length" 2 2) (("" (lift-if) (("" (ground) (("" (grind) nil nil)) nil)) nil)) nil)) nil) ((length def-decl "nat" list_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil)) nil)) (nonzero_version_rec_TCC6 0 (nonzero_version_rec_TCC6-1 nil 3593340485 ("" (skeep) (("" (assert) (("" (invoke (case "NOT %1") (! 2 1)) (("1" (hide 3) (("1" (typepred "v(cdr[int](ll))") (("1" (assert) (("1" (expand "length" 1 2) (("1" (lift-if) (("1" (ground) (("1" (hide-all-but (-1 3)) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (invoke (case "NOT %1") (! 2 1)) (("1" (hide 3) (("1" (skeep) (("1" (case "i = 0") (("1" (replace -1) (("1" (assert) (("1" (case " length[int](v(cdr[int](ll))) = length[int](ll)") (("1" (assert) (("1" (typepred "v(cdr[int](ll))") (("1" (expand "length" -5 2) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "nth" 2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lift-if) (("2" (split +) (("1" (flatten) (("1" (typepred "v(cdr[int](ll))") (("1" (hide (-1 -2 -4)) (("1" (inst - "i-1") (("1" (assert) (("1" (split -) (("1" (expand "nth" 1) (("1" (replace -1 1) (("1" (assert) (("1" (lift-if) (("1" (split 1) (("1" (propax) nil nil) ("2" (flatten) (("2" (assert) (("2" (expand "length" -2 1) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "length" -2 1) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (typepred "v(cdr[int](ll))") (("2" (hide (-1 -2 -4)) (("2" (inst - "i-1") (("2" (assert) (("2" (split -) (("1" (expand "nth" 2 1) (("1" (replace -1 +) (("1" (hide -1) (("1" (assert) (("1" (lift-if) (("1" (ground) (("1" --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.68 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
