| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/Sturm/ (Beweissystem der NASA Version 6.0.9©) Datei vom 7.10.2014 mit Größe 154 kB |
|
SSL gcd_coeff.prfSprache: Lisp |
|||||||||||||||
|
(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" (expand "length" 2 1) (("1" (lift-if) (("1" (ground) (("1" (hide-all-but (-1 4)) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "length" 2 4) (("2" (lift-if) (("2" (ground) (("2" (hide-all-but (-1 5)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "length" -1) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (flatten) (("2" (split -) (("1" (assert) (("1" (typepred "v(cdr[int](ll))") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (typepred "v(cdr[int](ll))") (("2" (hide (-1 -2 -3)) (("2" (split -) (("1" (propax) nil nil) ("2" (flatten) (("2" (skeep) (("2" (inst + "i-1") (("1" (assert) (("1" (flatten) (("1" (expand "nth" 2) (("1" (assert) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "i = 0") (("1" (replaces -1) (("1" (expand "nth" 3) (("1" (propax) nil nil)) nil)) nil) ("2" (assert) (("2" (typepred "i") (("2" (expand "length" -1) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 3) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (expand "length" 1 2) (("3" (lift-if) (("3" (ground) (("1" (hide-all-but (-1 3)) (("1" (grind) nil nil)) nil) ("2" (hide-all-but (-1 3)) (("2" (grind) nil nil)) nil) ("3" (hide-all-but (-3 2)) (("3" (grind) nil nil)) nil) ("4" (hide-all-but (-2 3)) (("4" (grind) nil nil)) nil) ("5" (hide-all-but (-3 2)) (("5" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (ll skolem-const-decl "list[int]" gcd_coeff nil) (i skolem-const-decl "below(length[int](ll))" gcd_coeff nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (/= const-decl "boolean" notequal nil) (below type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans 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) (IF const-decl "[boolean, T, T -> T]" if_def nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props 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) (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) (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) (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil)) nil)) (nonzero_version_rec_length_nonzero 0 (nonzero_version_rec_length_nonzero-1 nil 3593350425 ("" (induct "ll") (("1" (expand "nonzero_version_rec") (("1" (expand "length" 1 1) (("1" (expand "length" 1 1) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "length" 1 1) (("2" (propax) nil nil)) nil) ("3" (skeep) (("3" (name "ii" "cons1_var") (("3" (replaces -1) (("3" (name "L" "cons2_var") (("3" (replaces -1) (("3" (assert) (("3" (split +) (("1" (flatten) (("1" (expand "nonzero_version_rec" -1) (("1" (lift-if) (("1" (ground) (("1" (skosimp*) (("1" (inst + "i!1+1") (("1" (expand "nth" 2) (("1" (propax) nil nil)) nil) ("2" (expand "length" 1) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (inst + "0") (("1" (expand "nth" 3) (("1" (propax) nil nil)) nil) ("2" (expand "length" 1) (("2" (assert) nil nil)) nil)) nil) ("3" (inst 3 "0") (("1" (expand "nth" 3) (("1" (propax) nil nil)) nil) ("2" (expand "length" 1) (("2" (assert) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (inst + "i!1+1") (("1" (expand "nth" 2) (("1" (propax) nil nil)) nil) ("2" (expand "length" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "nonzero_version_rec" 1) (("2" (lift-if) (("2" (split +) (("1" (flatten) nil nil) ("2" (flatten) (("2" (assert) (("2" (skosimp*) (("2" (case "i!1 = 0") (("1" (replaces -1) (("1" (expand "nth" 3) (("1" (propax) nil nil)) nil)) nil) ("2" (assert) (("2" (case "L = null") (("1" (replace -1) (("1" (assert) (("1" (expand "nonzero_version_rec") (("1" (assert) (("1" (case "length[int](null)=0") (("1" (assert) (("1" (typepred "i!1") (("1" (expand "L") (("1" (expand "length" -1) (("1" (expand "length" -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "length" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "length[int](L) > 0") (("1" (assert) (("1" (inst + "i!1-1") (("1" (assert) (("1" (expand "nth" 5) (("1" (assert) nil nil)) nil)) nil) ("2" (typepred "i!1") (("2" (expand "length" -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (cons2_var skolem-const-decl "list[int]" gcd_coeff nil) (i!1 skolem-const-decl "below(length[int](cons2_var))" gcd_coeff nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (cons1_var skolem-const-decl "int" gcd_coeff nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (i!1 skolem-const-decl "below(length[int](cons2_var))" gcd_coeff nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (length_singleton formula-decl nil more_list_props "structures/") (length_null formula-decl nil more_list_props "structures/") (L skolem-const-decl "list[int]" gcd_coeff nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (i!1 skolem-const-decl "below(length[int](cons(cons1_var, cons2_var)))" gcd_coeff nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (nonzero_version_rec def-decl "{nl: list[int] | length[int](nl) <= length[int](ll) AND (FORALL (i: nat): i < length[int](ll) IMPLIES nth[int](ll, i) = (IF i < length[int](ll) - length[int](nl) THEN 0 ELSE nth[int](nl, i - length[int](ll) + length[int](nl)) ENDIF)) AND ((length[int](nl) > 0 OR (EXISTS (i: below(length[int](ll))): nth(ll, i) /= 0)) IMPLIES (length[int](nl) > 0 AND car[int](nl) /= 0))}" gcd_coeff nil) (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (/= const-decl "boolean" notequal nil) (below type-eq-decl nil naturalnumbers nil) (OR const-decl "[bool, bool -> bool]" booleans 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) (IF const-decl "[boolean, T, T -> T]" if_def nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (< const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals 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) (IFF 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)) (nonzero_version_rec_def_TCC1 0 (nonzero_version_rec_def_TCC1-1 nil 3593353172 ("" (skeep) (("" (grind) nil nil)) nil) ((length def-decl "nat" list_props nil) (/= const-decl "boolean" notequal nil) (nnint_plus_posint_is_posint application-judgement "posint" integers 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_def_TCC2 0 (nonzero_version_rec_def_TCC2-1 nil 3593353172 ("" (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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (IF const-decl "[boolean, T, T -> T]" if_def 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) (OR const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (car adt-accessor-decl "[(cons?) -> T]" list_adt 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) (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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (/= const-decl "boolean" notequal nil)) nil)) (nonzero_version_rec_def 0 (nonzero_version_rec_def-1 nil 3593353176 ("" (induct "ll") (("1" (assert) (("1" (flatten) nil nil)) nil) ("2" (skoletin 2) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) (("3" (hide +) (("3" (grind) nil nil)) nil)) nil)) nil) ("4" (skeep) (("4" (name "ii" "cons1_var") (("4" (replaces -1) (("4" (name "L" "cons2_var") (("4" (replaces -1) (("4" (assert) (("4" (case "ii/=0") (("1" (assert) (("1" (flatten) (("1" (expand "nonzero_version_rec" +) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (replaces -1) (("2" (expand "nonzero_version_rec" -2) (("2" (assert) (("2" (flatten) (("2" (expand "nonzero_version_rec" 2) (("2" (assert) (("2" (skeep) (("2" (case "i = 0") (("1" (replaces -1) (("1" (expand "nth" 2) (("1" (propax) nil nil)) nil)) nil) ("2" (inst - "i-1") (("1" (assert) (("1" (split -) (("1" (expand "nth" 3) (("1" (propax) nil nil)) nil) ("2" (expand "length" -2 1) (("2" (assert) nil nil)) 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) ("5" (hide 2) (("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp*) (("6" (grind) nil nil)) nil)) nil)) 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (i skolem-const-decl "nat" gcd_coeff nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (NOT const-decl "[bool -> bool]" booleans nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (IFF const-decl "[bool, bool -> bool]" booleans 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) (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) (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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (IF const-decl "[boolean, T, T -> T]" if_def 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) (OR const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (/= const-decl "boolean" notequal nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) (nonzero_version_rec def-decl "{nl: list[int] | length[int](nl) <= length[int](ll) AND (FORALL (i: nat): i < length[int](ll) IMPLIES nth[int](ll, i) = (IF i < length[int](ll) - length[int](nl) THEN 0 ELSE nth[int](nl, i - length[int](ll) + length[int](nl)) ENDIF)) AND ((length[int](nl) > 0 OR (EXISTS (i: below(length[int](ll))): nth(ll, i) /= 0)) IMPLIES (length[int](nl) > 0 AND car[int](nl) /= 0))}" gcd_coeff nil) (int_minus_int_is_int application-judgement "int" integers nil)) shostak)) (nonzero_version_def_TCC1 0 (nonzero_version_def_TCC1-1 nil 3586273286 ("" (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_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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" 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) (/= const-decl "boolean" notequal nil) (nonzero_version const-decl "list[int]" gcd_coeff nil)) nil)) (nonzero_version_def_TCC2 0 (nonzero_version_def_TCC2-1 nil 3593364928 ("" (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) (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) (int_minus_int_is_int application-judgement "int" integers nil) (/= const-decl "boolean" notequal nil) (nonzero_version const-decl "list[int]" gcd_coeff nil)) nil)) (nonzero_version_def 0 (nonzero_version_def-1 nil 3586273287 ("" (skeep) (("" (name "L" "nonzero_version(ll)") (("" (replace -1) (("" (assert) (("" (invoke (case "NOT %1") (! 1 1)) (("1" (hide 2) (("1" (replaces -1 :dir rl) (("1" (expand "nonzero_version") (("1" (rewrite "length_reverse") (("1" (typepred "nonzero_version_rec(reverse(ll))") (("1" (lemma "length_reverse[int]") (("1" (inst - "ll") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (invoke (case "NOT %1") (! 1 1)) (("1" (hide 2) (("1" (skeep) (("1" (lift-if) (("1" (ground) (("1" (replace -4 + :dir rl) (("1" (expand "nonzero_version" +) (("1" (lemma "reverse_def[int]") (("1" (inst?) (("1" (assert) (("1" (split -) (("1" (replace -1) (("1" (hide -1) (("1" (name "LP" "nonzero_version_rec(reverse(ll))") (("1" (replace -1) (("1" (typepred "LP") (("1" (hide (-1 -2 -4)) (("1" (inst - "length(ll)-1-i") (("1" (assert) (("1" (split -) (("1" (lemma "reverse_def[int]") (("1" (inst - "ll" "length(ll)-1-i") (("1" (assert) (("1" (replace -1 -2) (("1" (replace -2 +) (("1" (lift-if) (("1" (hide -2) (("1" (case "length(reverse(ll)) = length(ll)") (("1" (replace -1) (("1" (assert) (("1" (split +) (("1" (flatten) (("1" (assert) (("1" (both-sides "-" "length(ll)" -1) (("1" (assert) (("1" (neg-formula -1) (("1" (case "length(L) = length(LP)") (("1" (assert) nil nil) ("2" (expand "L" 1) (("2" (expand "LP" 1) (("2" (expand "nonzero_version") (("2" (rewrite "length_reverse") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "length_reverse") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "length_reverse") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "L" -1) (("2" (expand "nonzero_version" -1) (("2" (rewrite "length_reverse") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (copy 1) (("2" (expand "L" 1) (("2" (expand "nonzero_version" 1) (("2" (rewrite "length_reverse" 1) (("2" (typepred "nonzero_version_rec(reverse(ll))") (("2" (hide (-1 -2 -4)) (("2" (rewrite "length_reverse" -1) (("2" (inst - "length(ll)-1-i") (("2" (assert) (("2" (lemma "reverse_def[int]") (("2" (inst - "ll" "length(ll)-1-i") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace -1) (("2" (invoke (case "NOT %1") (! 1 1)) (("1" (hide (-1 2)) (("1" (flatten) (("1" (skeep) (("1" (typepred "i") (("1" (split +) (("1" (expand "L" +) (("1" (expand "nonzero_version" 1) (("1" (rewrite "length_reverse") (("1" (lemma "nonzero_version_rec_length_nonzero") (("1" (assert) (("1" (inst?) (("1" (replace -1) (("1" (hide -1) (("1" (invoke (case "NOT %1") (! 1 1)) (("1" (hide 2) (("1" (rewrite "length_reverse") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (inst + "length(ll)-1-i") (("1" (lemma "reverse_def[int]") (("1" (inst - "ll" "length(ll)-1-i") (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "length_reverse") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "L" 1) (("2" (expand "nonzero_version" 1) (("2" (rewrite "length_reverse") (("2" (lemma "reverse_def[int]") (("2" (inst - "nonzero_version_rec(reverse(ll))" "length(nonzero_version_rec(reverse(ll))) - 1") (("1" (assert) (("1" (replaces -1) (("1" (lemma "nonzero_version_rec_def") (("1" (inst - "reverse(ll)") (("1" (assert) (("1" (split -) (("1" (expand "nth" 1) (("1" (assert) (("1" (flatten) nil nil)) nil)) nil) ("2" (lemma "nonzero_version_rec_length_nonzero") (("2" (inst?) (("2" (assert) (("2" (rewrite "length_reverse" 1) (("2" (assert) (("2" (inst + "length(ll)-1-i") (("1" (assert) (("1" (flatten) (("1" (lemma "reverse_def[int]") (("1" (assert) (("1" (inst - "ll" "length(ll)-1-i") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (rewrite "length_reverse" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "nonzero_version_rec_length_nonzero") (("2" (inst?) (("2" (assert) (("2" (rewrite "length_reverse" 1) (("2" (assert) (("2" (inst + "length(ll)-1-i") (("1" (assert) (("1" (flatten) (("1" (lemma "reverse_def[int]") (("1" (inst - "ll" "length(ll)-1-i") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite "length_reverse" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (invoke (case "NOT %1") (! 1 1)) (("1" (hide 2) (("1" (expand "L" 1) (("1" (expand "nonzero_version" 1) (("1" (rewrite "length_reverse" 1) (("1" (lemma "nonzero_version_rec_length_nonzero") (("1" (inst - "reverse(ll)") (("1" (replace -1) (("1" (rewrite "length_reverse" 1) (("1" (split +) (("1" (flatten) (("1" (assert) (("1" (skeep) (("1" (assert) (("1" (split -) (("1" (skeep) (("1" (inst + "length(ll)-1-i!1") (("1" (assert) (("1" (lemma "reverse_def[int]") (("1" (inst - "ll" "i!1") (("1" (assert) (("1" (typepred "i!1") (("1" (rewrite "length_reverse" -1) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (typepred "i!1") (("2" (rewrite "length_reverse" -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (skeep -) (("2" (assert) (("2" (split -) (("1" (propax) nil nil) ("2" (assert) (("2" (inst + "length(ll)-1-i") (("1" (assert) (("1" (lemma "reverse_def[int]") (("1" (inst - "ll" "length(ll)-1-i") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (rewrite "length_reverse" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split +) (("1" (ground) nil nil) ("2" (ground) nil nil) ("3" (lemma "nonzero_version_rec_def") (("3" (expand "L" 1) (("3" (expand "nonzero_version" 1) (("3" (rewrite "length_reverse" 1) (("3" (inst - "reverse(ll)") (("3" (assert) (("3" (flatten) (("3" (assert) (("3" (flatten) (("3" (split +) (("1" (flatten) (("1" (rewrite "reverse_def") (("1" (expand "nth" -1) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (skeep) (("2" (inst - "length(ll)-1-i") (("1" (assert) (("1" (split -) (("1" (rewrite "reverse_def") nil nil) ("2" (rewrite "length_reverse" 1) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nonzero_version const-decl "list[int]" gcd_coeff 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) (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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil) (int_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_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nonzero_version_rec_def formula-decl nil gcd_coeff nil) (ll skolem-const-decl "list[int]" gcd_coeff nil) (i skolem-const-decl "below(length[int](ll))" gcd_coeff nil) (nonzero_version_rec_length_nonzero formula-decl nil gcd_coeff nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (i skolem-const-decl "below(length[int](ll))" gcd_coeff nil) (i!1 skolem-const-decl "below(length[int](reverse(ll)))" gcd_coeff nil) (i skolem-const-decl "nat" gcd_coeff nil) (reverse_def formula-decl nil more_list_props "structures/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (both_sides_minus_lt1 formula-decl nil real_props nil) (mult_neg formula-decl nil extra_tegies nil) (neg_neg formula-decl nil extra_tegies nil) (neg_one_times formula-decl nil extra_tegies nil) (minus_int_is_int application-judgement "int" integers nil) (both_sides_times_neg_lt1 formula-decl nil real_props nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (negreal nonempty-type-eq-decl nil real_types nil) (- const-decl "[numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (L skolem-const-decl "list[int]" gcd_coeff nil) (LP skolem-const-decl "{nl: list[int] | length[int](nl) <= length[int](reverse(ll)) AND (FORALL (i: nat): i < length[int](reverse(ll)) IMPLIES nth[int](reverse(ll), i) = (IF i < length[int](reverse(ll)) - length[int](nl) THEN 0 ELSE nth[int] (nl, i + length[int](nl) - length[int](reverse(ll))) ENDIF)) AND ((length[int](nl) > 0 OR (EXISTS (i: below(length[int](reverse(ll)))): nth(reverse(ll), i) /= 0)) IMPLIES (length[int](nl) > 0 AND car[int](nl) /= 0))}" gcd_coeff nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (reverse def-decl "list[T]" list_props nil) (nonzero_version_rec def-decl "{nl: list[int] | length[int](nl) <= length[int](ll) AND (FORALL (i: nat): i < length[int](ll) IMPLIES nth[int](ll, i) = (IF i < length[int](ll) - length[int](nl) THEN 0 ELSE nth[int](nl, i - length[int](ll) + length[int](nl)) ENDIF)) AND ((length[int](nl) > 0 OR (EXISTS (i: below(length[int](ll))): nth(ll, i) /= 0)) IMPLIES (length[int](nl) > 0 AND car[int](nl) /= 0))}" gcd_coeff nil) (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (/= const-decl "boolean" notequal nil) (below type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans 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) (IF const-decl "[boolean, T, T -> T]" if_def nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (length_reverse formula-decl nil list_props nil) (NOT const-decl "[bool -> bool]" booleans 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) (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil)) shostak)) (nonzero_version_length_nz_TCC1 0 (nonzero_version_length_nz_TCC1-1 nil 3612869101 ("" (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) (int_minus_int_is_int application-judgement "int" integers 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)) nil)) (nonzero_version_length_nz 0 (nonzero_version_length_nz-1 nil 3612869168 ("" (skeep) (("" (expand "nonzero_version") (("" (case "nonzero_version_rec(reverse(ll)) = reverse(ll)") (("1" (replaces -1) (("1" (rewrite "reverse_reverse") nil nil)) nil) ("2" (hide 3) (("2" (name "l3" "reverse(ll)") (("2" (replace -1) (("2" (case "nth(l3,0)=0") (("1" (lemma "reverse_def[int]") (("1" (inst?) (("1" (inst - "0") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (lemma "length_reverse[int]") (("2" (inst - "ll") (("2" (replace -2) (("2" (hide -2) (("2" (expand "nonzero_version_rec") (("2" (assert) (("2" (expand "nth" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (lemma "length_reverse[int]") (("3" (inst - "ll") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nonzero_version const-decl "list[int]" gcd_coeff nil) (length_reverse formula-decl nil list_props nil) (reverse_def formula-decl nil more_list_props "structures/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (reverse_reverse formula-decl nil list_props nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities 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) (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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (IF const-decl "[boolean, T, T -> T]" if_def 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) (OR const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (/= const-decl "boolean" notequal nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) (nonzero_version_rec def-decl "{nl: list[int] | length[int](nl) <= length[int](ll) AND (FORALL (i: nat): i < length[int](ll) IMPLIES nth[int](ll, i) = (IF i < length[int](ll) - length[int](nl) THEN 0 ELSE nth[int](nl, i - length[int](ll) + length[int](nl)) ENDIF)) AND ((length[int](nl) > 0 OR (EXISTS (i: below(length[int](ll))): nth(ll, i) /= 0)) IMPLIES (length[int](nl) > 0 AND car[int](nl) /= 0))}" gcd_coeff nil) (reverse def-decl "list[T]" list_props nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (listn_0 name-judgement "listn[real](0)" polynomial_division 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.146Bemerkung: (vorverarbeitet am 2026-04-30) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26