Quelle gcd_coeff.prf Sprache: 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"
--> --------------------

--> maximum size reached

--> --------------------

quality100%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.