Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: vect3_fun_ops.prf Sprache: Lisp

Original von: PVS^©

(system_solvers
(rows_fun_TCC1 0
  (rows_fun_TCC1-1 nil 3621776159
   ("" (skeep)
    ((""
      (case "RelF6(j) = 0 OR RelF6(j) = 1 OR RelF6(j) = 2 or RelF6(j) = 3 OR RelF6(j) = 4 or RelF6(j) = 5")
      (("1" (split)
        (("1" (replace -1) (("1" (eval-formula 1) nil nil)) nil)
         ("2" (replace -1) (("2" (eval-formula 1) nil nil)) nil)
         ("3" (replace -1) (("3" (eval-formula 1) nil nil)) nil)
         ("4" (replace -1) (("4" (eval-formula 1) nil nil)) nil)
         ("5" (replace -1) (("5" (eval-formula 1) nil nil)) nil)
         ("6" (replace -1) (("6" (eval-formula 1) nil nil)) nil))
        nil)
       ("2" (ground) nil nil))
      nil))
    nil)
   ((upto nonempty-type-eq-decl nil naturalnumbers nil)
    (subrange type-eq-decl nil integers nil)
    (<= const-decl "bool" reals nil)
    (AND 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number nonempty-type-decl nil numbers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil))
   nil))
(entry_fun_TCC1 0
  (entry_fun_TCC1-1 nil 3621776159 ("" (subtype-tcc) nil nil) nil nil))
(entry_fun_TCC2 0
  (entry_fun_TCC2-1 nil 3621776159 ("" (subtype-tcc) nil nil)
   ((listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (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)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (length def-decl "nat" list_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (listn type-eq-decl nil listn "structures/")
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
(entry_fun_TCC3 0
  (entry_fun_TCC3-1 nil 3621776159 ("" (subtype-tcc) nil nil)
   ((listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (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)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (length def-decl "nat" list_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (listn type-eq-decl nil listn "structures/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/"))
   nil))
(entry_is 0
  (entry_is-1 nil 3621776387
   ("" (skeep)
    (("" (expand "entry_fun")
      (("" (lemma "tensor_entry")
        (("" (inst -1 "A63" "1+k" " base_n_to_nat(6, RelF6, k)" "i")
          (("1" (ground)
            (("1" (case "rows(A63) = 6 AND columns(A63) = 3")
              (("1" (flatten)
                (("1" (replace -1)
                  (("1" (replace -2)
                    (("1" (replace -3)
                      (("1" (rewrite "product_eq")
                        (("1" (hide 2)
                          (("1" (skeep)
                            (("1" (expand "entry_pick")
                              (("1"
                                (lemma "base_n_base_n_to_nat")
                                (("1"
                                  (inst -1 "6" "RelF6" "k")
                                  (("1"
                                    (ground)
                                    (("1"
                                      (inst -1 "n")
                                      (("1"
                                        (replace -1)
                                        (("1"
                                          (expand "rows_fun")
                                          (("1"
                                            (expand "base_list")
                                            (("1"
                                              (typepred
                                               "array2list[below(3)](1+k)(base_n(3, i))")
                                              (("1"
                                                (inst -3 "n")
                                                (("1"
                                                  (replace -3 :dir rl)
                                                  (("1"
                                                    (ground)
                                                    (("1"
                                                      (expand "entry")
                                                      (("1"
                                                        (expand
                                                         "access")
                                                        (("1"
                                                          (propax)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (inst 1 "0")
                                                nil
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (skeep)
                                      (("2" (ground) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (skeep)
                          (("2" (hide 2) (("2" (ground) nil nil)) nil))
                          nil)
                         ("3" (skeep)
                          (("3" (hide 2) (("3" (ground) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (eval-formula 1) nil nil))
              nil))
            nil)
           ("2" (case-replace "columns(A63) = 3")
            (("1" (ground) nil nil) ("2" (eval-formula 1) nil nil))
            nil)
           ("3" (lemma "base_n_to_nat_lt")
            (("3" (inst -1 "RelF6" "k" "6")
              (("3" (split -1)
                (("1" (case-replace "rows(A63) = 6")
                  (("1" (ground) nil nil)
                   ("2" (eval-formula 1) nil nil))
                  nil)
                 ("2" (skeep) (("2" (ground) nil nil)) nil))
                nil))
              nil))
            nil)
           ("4" (ground) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((entry_fun const-decl "real" system_solvers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (nat_exp application-judgement "nat" exponentiation nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (A63 const-decl
         "{M: PosFullMatrix | rows(M) = 6 AND columns(M) = 3}"
         tarski_query_matrix nil)
    (PosFullMatrix type-eq-decl nil matrices "matrices/")
    (columns def-decl "{c: nat |
         (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND
          (null?(M) AND c = 0 OR
            (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}"
             matrices "matrices/")
    (<= const-decl "bool" reals nil)
    (FullMatrix type-eq-decl nil matrices "matrices/")
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (below type-eq-decl nil naturalnumbers nil)
    (length def-decl "nat" list_props nil)
    (< const-decl "bool" reals nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (rows const-decl "nat" matrices "matrices/")
    (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)
    (Matrix type-eq-decl nil matrices "matrices/")
    (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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (k skolem-const-decl "nat" system_solvers nil)
    (RelF6 skolem-const-decl "[nat -> subrange(0, 5)]" system_solvers
     nil)
    (subrange type-eq-decl nil integers nil)
    (base_n_to_nat const-decl "nat" base_repr "reals/")
    (i skolem-const-decl "below(3 ^ (1 + k))" system_solvers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (NOT const-decl "[bool -> bool]" booleans nil)
    (array2list const-decl
     "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}"
     array2list "structures/")
    (entry const-decl "real" matrices "matrices/")
    (access const-decl "real" matrices "matrices/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (base_n_base_n_to_nat formula-decl nil base_repr "reals/")
    (product_eq formula-decl nil product "reals/")
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (upto nonempty-type-eq-decl nil naturalnumbers nil)
    (Vector type-eq-decl nil matrices "matrices/")
    (row const-decl "Vector" matrices "matrices/")
    (rows_fun const-decl
     "{V: Vector | V = row(A63)(RelF6(j)) AND length(V) = 3}"
     system_solvers nil)
    (listn type-eq-decl nil listn "structures/")
    (base_list const-decl "listn[below(n)](digits)" base_repr "reals/")
    (entry_pick const-decl "real" tensor_product "matrices/")
    (base_n def-decl "nat" base_repr "reals/")
    (T_high type-eq-decl nil product "reals/")
    (T_low type-eq-decl nil product "reals/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (posint_exp application-judgement "posint" exponentiation nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (base_n_to_nat_lt formula-decl nil base_repr "reals/")
    (tensor_entry formula-decl nil tensor_product "matrices/"))
   shostak))
(TQlist_fun_TCC1 0
  (TQlist_fun_TCC1-1 nil 3621782555
   ("" (skeep) (("" (inst 1 "0") nil nil)) nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/"))
   nil))
(TQlist_fun_TCC2 0
  (TQlist_fun_TCC2-1 nil 3621782555 ("" (subtype-tcc) nil nil)
   ((listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (/= const-decl "boolean" notequal nil)
    (<= const-decl "bool" reals nil)
    (upto nonempty-type-eq-decl nil naturalnumbers 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)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (length def-decl "nat" list_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (listn type-eq-decl nil listn "structures/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (x1!1 skolem-const-decl "nat" system_solvers nil)
    (k!1 skolem-const-decl "nat" system_solvers nil))
   nil))
(TQlist_lem_TCC1 0
  (TQlist_lem_TCC1-1 nil 3621782865
   ("" (skeep)
    (("" (skeep)
      (("" (lemma "base_n_lt_n")
        (("" (inst?) (("" (ground) nil nil)) nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (> const-decl "bool" reals nil) (< const-decl "bool" reals nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (below type-eq-decl nil naturalnumbers nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (base_n_lt_n formula-decl nil base_repr "reals/"))
   nil))
(TQlist_lem 0
  (TQlist_lem-1 nil 3621782966
   ("" (expand "TQlist_fun")
    (("" (skeep)
      (("" (typepred (j))
        (("" (expand "base_list")
          (("" (lemma "array2list_inv[below(3)]")
            (("" (inst -1 "base_n(3, j)" "0" "1+k" "_")
              ((""
                (case-replace "list2array[below(3)]
                 (0)(array2list[below(3)](1 + k)(base_n(3, j)))=base_n(3, j)")
                (("" (hide 2)
                  (("" (decompose-equality 1)
                    (("" (case "x!1<1+k")
                      (("1" (inst?) nil nil)
                       ("2" (lemma "list2array_sound[below(3)]")
                        (("2" (hide -2)
                          (("2" (expand "length")
                            (("2"
                              (inst -1
                               "array2list[below(3)](1 + k)(base_n(3, j))"
                               "0" "x!1")
                              (("2"
                                (typepred
                                 "array2list[below(3)](1 + k)(base_n(3, j))")
                                (("2"
                                  (expand "length" -2)
                                  (("2"
                                    (replace -2)
                                    (("2"
                                      (lift-if -4)
                                      (("2"
                                        (ground)
                                        (("2"
                                          (replace -1)
                                          (("2"
                                            (lemma "base_n_0")
                                            (("2"
                                              (inst?)
                                              (("2"
                                                (flip-ineq 1)
                                                (("2"
                                                  (swap-rel -1)
                                                  (("2"
                                                    (lemma
                                                     "both_sides_expt_gt1_le")
                                                    (("2"
                                                      (inst
                                                       -1
                                                       "3"
                                                       "1+k"
                                                       "x!1")
                                                      (("2"
                                                        (ground)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((base_list const-decl "listn[below(n)](digits)" base_repr "reals/")
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (base_n def-decl "nat" base_repr "reals/")
    (> const-decl "bool" reals nil)
    (x!1 skolem-const-decl "nat" system_solvers nil)
    (k skolem-const-decl "nat" system_solvers nil)
    (<= const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (both_sides_expt_gt1_le formula-decl nil exponentiation nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (base_n_0 formula-decl nil base_repr "reals/")
    (list2array_sound formula-decl nil array2list "structures/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posint_exp application-judgement "posint" exponentiation nil)
    (array2list const-decl
     "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}"
     array2list "structures/")
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (listn type-eq-decl nil listn "structures/")
    (length def-decl "nat" list_props nil)
    (list2array def-decl "T" array2list "structures/")
    (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 "[T, T -> boolean]" equalities nil)
    (array2list_inv formula-decl nil array2list "structures/")
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (< const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (below type-eq-decl nil naturalnumbers nil)
    (TQlist_fun const-decl "real" system_solvers nil))
   shostak))
(sturm_tarski_faster_TCC1 0
  (sturm_tarski_faster_TCC1-1 nil 3621782555 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (/= const-decl "boolean" notequal nil)
    (<= const-decl "bool" reals nil)
    (upto nonempty-type-eq-decl nil naturalnumbers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/"))
   nil))
(sturm_tarski_faster_TCC2 0
  (sturm_tarski_faster_TCC2-1 nil 3621782555 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (/= const-decl "boolean" notequal nil)
    (<= const-decl "bool" reals nil)
    (upto nonempty-type-eq-decl nil naturalnumbers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (posnat_expt application-judgement "posnat" exponentiation nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (^ const-decl "real" exponentiation nil))
   nil))
(sturm_tarski_faster_TCC3 0
  (sturm_tarski_faster_TCC3-1 nil 3621782555 ("" (subtype-tcc) nil nil)
   ((array2list const-decl
     "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}"
     array2list "structures/")
    (base_list const-decl "listn[below(n)](digits)" base_repr
     "reals/"))
   nil))
(sturm_tarski_faster_TCC4 0
  (sturm_tarski_faster_TCC4-1 nil 3621782555
   ("" (skeep)
    ((""
      (case-replace
       "dot_tail_sum2plus(k + 1, EntFun, TQlist_fun(k, a, m, p, n), 0, 0,
                        base_list(3, 0, k + 1)) = sturm_tarski_solver_slow_basic(k,a,m,p,n,RelF6)")
      (("1" (ground) nil nil)
       ("2" (hide 3)
        (("2" (lemma "dot_tail_sum_lem")
          (("2" (inst?)
            (("2" (replace -1)
              (("2" (simplify)
                (("2" (expand "sturm_tarski_solver_slow_basic")
                  (("2"
                    (typepred
                     "super_dot(row(A63_tensor_power_mat_row(1 + k)(RelF6))(0),
                 col(TQ_vect3k(k, a, m, p, n))(0))")
                    (("2" (replace -1)
                      (("2" (hide (-1 -2))
                        (("2" (rewrite "dot_eq_sigma")
                          (("2"
                            (typepred
                             "A63_tensor_power_mat_row(1 + k)(RelF6)")
                            (("2" (rewrite "length_row")
                              (("1"
                                (rewrite "length_col")
                                (("1"
                                  (replace -6)
                                  (("1"
                                    (typepred
                                     "TQ_vect3k(k, a, m, p, n)")
                                    (("1"
                                      (replace -5)
                                      (("1"
                                        (hide-all-but (-13 1 2))
                                        (("1"
                                          (ground)
                                          (("1"
                                            (rewrite "sigma_eq")
                                            (("1"
                                              (hide 2)
                                              (("1"
                                                (skeep)
                                                (("1"
                                                  (replace -1)
                                                  (("1"
                                                    (rewrite
                                                     "entry_is")
                                                    (("1"
                                                      (rewrite
                                                       "TQlist_lem")
                                                      (("1"
                                                        (rewrite
                                                         "access_col")
                                                        (("1"
                                                          (rewrite
                                                           "access_row")
                                                          (("1"
                                                            (lemma
                                                             "A63_tensor_power_mat_row_def")
                                                            (("1"
                                                              (inst
                                                               -1
                                                               "RelF6"
                                                               "k")
                                                              (("1"
                                                                (ground)
                                                                (("1"
                                                                  (replace
                                                                   -1)
                                                                  (("1"
                                                                    (expand
                                                                     "vect2matrix")
                                                                    (("1"
                                                                      (lemma
                                                                       "entry_form_matrix")
                                                                      (("1"
                                                                        (inst?)
                                                                        (("1"
                                                                          (ground)
                                                                          (("1"
                                                                            (replace
                                                                             -1)
                                                                            (("1"
                                                                              (rewrite
                                                                               "access_row")
                                                                              (("1"
                                                                                (hide
                                                                                 -1)
                                                                                (("1"
                                                                                  (expand
                                                                                   "TQ_vect3k")
                                                                                  (("1"
                                                                                    (lemma
                                                                                     "entry_form_matrix")
                                                                                    (("1"
                                                                                      (inst
                                                                                       -1
                                                                                       "LAMBDA (i_1: nat, j_1: nat):
                            IF i_1 >= 3 ^ (1 + k) OR j_1 >= 1 THEN 0
                            ELSE TQ_fam(k, a, m, p, n, base_n(3, i_1))
                            ENDIF"
                                                                                       "_"
                                                                                       "_"
                                                                                       "_"
                                                                                       "_")
                                                                                      (("1"
                                                                                        (inst?)
                                                                                        (("1"
                                                                                          (replace
                                                                                           -1)
                                                                                          (("1"
                                                                                            (ground)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil)
                                                                                       ("2"
                                                                                        (hide
                                                                                         2)
                                                                                        (("2"
                                                                                          (skeep)
                                                                                          (("2"
                                                                                            (skeep)
                                                                                            (("2"
                                                                                              (lemma
                                                                                               "base_n_lt_n")
                                                                                              (("2"
                                                                                                (inst?)
                                                                                                (("2"
                                                                                                  (ground)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (expand "rows")
                                (("2" (ground) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("3" (ground) nil nil) ("4" (ground) nil nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (posint_exp application-judgement "posint" exponentiation nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (> const-decl "bool" reals nil) (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)
    (below type-eq-decl nil naturalnumbers nil)
    (length def-decl "nat" list_props nil)
    (upto nonempty-type-eq-decl nil naturalnumbers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (listn type-eq-decl nil listn "structures/")
    (base_list const-decl "listn[below(n)](digits)" base_repr "reals/")
    (<= const-decl "bool" reals nil)
    (dot_tail_sum2plus def-decl "real" query_coeff "matrices/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (TQlist_fun const-decl "real" system_solvers nil)
    (subrange type-eq-decl nil integers nil)
    (NSol_all const-decl "nat" poly_families nil)
    (sturm_tarski_solver_slow_basic const-decl "{r: real |
         r = NSol_all(k, a, m, p, n, RelF6) AND
          rational_pred(r) AND integer_pred(r)}" poly_systems nil)
    (dot_tail_sum_lem formula-decl nil query_coeff "matrices/")
    (dot_eq_sigma formula-decl nil matrices "matrices/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (int_min application-judgement "{k: int | k <= i AND k <= j}"
     real_defs nil)
    (length_row formula-decl nil matrices "matrices/")
    (min_id formula-decl nil min_max "reals/")
    (TQlist_lem formula-decl nil system_solvers nil)
    (access_row formula-decl nil matrices "matrices/")
    (entry_form_matrix formula-decl nil matrices "matrices/")
    (form_matrix_square application-judgement "FullMatrix" matrices
     "matrices/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (k skolem-const-decl "nat" system_solvers nil)
    (base_n def-decl "nat" base_repr "reals/")
    (TQ_fam const-decl "int" poly_families nil)
    (base_n_lt_n formula-decl nil base_repr "reals/")
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (tensor_power_alt def-decl "PosFullMatrix" tensor_product
     "matrices/")
    (A63 const-decl
         "{M: PosFullMatrix | rows(M) = 6 AND columns(M) = 3}"
         tarski_query_matrix nil)
    (base_n_to_nat const-decl "nat" base_repr "reals/")
    (vect2matrix const-decl
     "{PFM | rows(PFM) = 1 AND columns(PFM) = length(v)}" matrices
     "matrices/")
    (A63_tensor_power_mat_row_def formula-decl nil poly_systems nil)
    (access_col formula-decl nil matrices "matrices/")
    (entry_is formula-decl nil system_solvers nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sigma_eq formula-decl nil sigma "reals/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (access const-decl "real" matrices "matrices/")
    (T_high type-eq-decl nil sigma "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T_low type-eq-decl nil sigma "reals/")
    (length_col formula-decl nil matrices "matrices/")
    (TQ_vect3k const-decl
     "{v: PosFullMatrix | rows(v) = 3 ^ (k + 1) AND columns(v) = 1}"
     tarski_query_matrix nil)
    (col def-decl "VectorN(rows(M))" matrices "matrices/")
    (VectorN type-eq-decl nil matrices "matrices/")
    (A63_tensor_power_mat_row def-decl
     "{M: PosFullMatrix | rows(M) = 1 AND columns(M) = 3 ^ m}"
     poly_systems nil)
    (PosFullMatrix type-eq-decl nil matrices "matrices/")
    (columns def-decl "{c: nat |
         (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND
          (null?(M) AND c = 0 OR
            (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}"
             matrices "matrices/")
    (rows const-decl "nat" matrices "matrices/")
    (FullMatrix type-eq-decl nil matrices "matrices/")
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (row const-decl "Vector" matrices "matrices/")
    (Matrix type-eq-decl nil matrices "matrices/")
    (super_dot def-decl "{rr: real | rr = dot(v1, v2)}" matrices
     "matrices/")
    (dot def-decl "real" matrices "matrices/")
    (Vector type-eq-decl nil matrices "matrices/")
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
(Test1_TCC1 0
  (Test1_TCC1-1 nil 3621776159 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (A63 const-decl
         "{M: PosFullMatrix | rows(M) = 6 AND columns(M) = 3}"
         tarski_query_matrix nil)
    (entry const-decl "real" matrices "matrices/")
    (T1 const-decl "real" system_solvers nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil))
   nil))
(Test1_TCC2 0
  (Test1_TCC2-1 nil 3621776159 ("" (termination-tcc) nil nil)
   ((A63 const-decl
         "{M: PosFullMatrix | rows(M) = 6 AND columns(M) = 3}"
         tarski_query_matrix nil)
    (row const-decl "Vector" matrices "matrices/")
    (length def-decl "nat" list_props nil)
    (access const-decl "real" matrices "matrices/")
    (entry const-decl "real" matrices "matrices/")
    (T1 const-decl "real" system_solvers nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil))
   nil))
(Test2recurse_TCC1 0
  (Test2recurse_TCC1-1 nil 3621776159 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (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)
    (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)
    (Matrix type-eq-decl nil matrices "matrices/")
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt 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)
    (< const-decl "bool" reals nil)
    (length def-decl "nat" list_props nil)
    (below type-eq-decl nil naturalnumbers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (below type-eq-decl nil nat_types nil)
    (nth def-decl "T" list_props nil)
    (FullMatrix type-eq-decl nil matrices "matrices/")
    (> const-decl "bool" reals nil)
    (rows const-decl "nat" matrices "matrices/")
    (<= const-decl "bool" reals nil)
    (columns def-decl "{c: nat |
         (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND
          (null?(M) AND c = 0 OR
            (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}"
             matrices "matrices/")
    (PosFullMatrix type-eq-decl nil matrices "matrices/")
    (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)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (entry const-decl "real" matrices "matrices/")
    (T2 const-decl "real" system_solvers nil))
   nil))
(Test2recurse_TCC2 0
  (Test2recurse_TCC2-1 nil 3621776159 ("" (termination-tcc) nil nil)
   ((row const-decl "Vector" matrices "matrices/")
    (length def-decl "nat" list_props nil)
    (access const-decl "real" matrices "matrices/")
    (entry const-decl "real" matrices "matrices/")
    (T2 const-decl "real" system_solvers nil))
   nil)))

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.