products/Sources/formale Sprachen/PVS/Sturm image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: sturmsquarefree.prf   Sprache: Lisp

Original von: PVS©

(sturmsquarefree
 (sturm_sequence?_TCC1 0
  (sturm_sequence?_TCC1-1 nil 3583755671 ("" (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 "real" exponentiation nil)
    (polynomial const-decl "[real -> real]" polynomials "reals/")
    (rat_max application-judgement "{s: rat | s >= q AND s >= r}"
     real_defs nil)
    (int_max application-judgement "{k: int | i <= k AND j <= k}"
     real_defs nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (/= const-decl "boolean" notequal nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil))
 (sturm_sequence?_TCC2 0
  (sturm_sequence?_TCC2-1 nil 3583755671 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_times_real_is_real application-judgement "real" reals 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)
    (poly_deriv const-decl "real" polynomials "reals/")
    (^ const-decl "real" exponentiation nil)
    (polynomial const-decl "[real -> real]" polynomials "reals/")
    (/= const-decl "boolean" notequal nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (int_max application-judgement "{k: int | i <= k AND j <= k}"
     real_defs nil)
    (rat_max application-judgement "{s: rat | s >= q AND s >= r}"
     real_defs nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
 (sturm_sequence_degree_1 0
  (sturm_sequence_degree_1-1 nil 3588942625
   ("" (skeep)
    (("" (expand "sturm_sequence?")
      (("" (assert)
        (("" (split +)
          (("1" (skeep) (("1" (assertnil nil)) nil)
           ("2" (skeep)
            (("2" (case "i = 1")
              (("1" (replaces -1)
                (("1" (replace -5)
                  (("1" (expand "poly_deriv" -2)
                    (("1" (assertnil nil)) nil))
                  nil))
                nil)
               ("2" (assertnil nil))
              nil))
            nil)
           ("3" (skeep) (("3" (assertnil nil)) nil)
           ("4" (skeep)
            (("4" (assert)
              (("4" (replaces -1)
                (("4" (replace -2) (("4" (grind) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sturm_sequence? const-decl "bool" sturmsquarefree 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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (poly_deriv const-decl "real" polynomials "reals/")
    (sign_ext const-decl
     "{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}"
     sign "reals/")
    (polynomial const-decl "[real -> real]" polynomials "reals/")
    (sigma def-decl "real" sigma "reals/")
    (^ const-decl "real" exponentiation nil)
    (expt def-decl "real" exponentiation nil)
    (max_npreal_0 formula-decl nil min_max "reals/")
    (int_minus_int_is_int application-judgement "int" integers nil))
   shostak))
 (sturm_seq_repeated_root 0
  (sturm_seq_repeated_root-1 nil 3584191381
   ("" (skeep)
    ((""
      (case "FORALL (i:nat): i-1>=0 AND i+1<=m AND polynomial(p(i),n(i))(x)=0 IMPLIES (polynomial(p(i-1),n(i-1))(x)=0 IFF polynomial(p(i+1),n(i+1))(x)=0)")
      (("1" (skeep)
        (("1"
          (case "FORALL (j:nat): i-j>=0 IMPLIES FORALL (k:nat): k<=j IMPLIES polynomial(p(i-k), n(i-k))(x) = 0")
          (("1"
            (case "FORALL (j:nat): i+j<=m IMPLIES FORALL (k:nat): k<=j IMPLIES polynomial(p(i+k), n(i+k))(x) = 0")
            (("1" (skeep)
              (("1" (case "j>=i")
                (("1" (inst - "j-i")
                  (("1" (assert)
                    (("1" (inst - "j-i") (("1" (assertnil nil)) nil))
                    nil)
                   ("2" (assertnil nil))
                  nil)
                 ("2" (inst -2 "i-j")
                  (("1" (assert)
                    (("1" (inst -2 "i-j") (("1" (assertnil nil))
                      nil))
                    nil)
                   ("2" (assertnil nil))
                  nil))
                nil))
              nil)
             ("2" (hide (-1 2))
              (("2" (induct "j")
                (("1" (assert)
                  (("1" (skeep) (("1" (assertnil nil)) nil)) nil)
                 ("2" (assert)
                  (("2" (skosimp*)
                    (("2" (assert)
                      (("2" (case "k!1=0 OR k!1=1")
                        (("1" (ground) nil nil)
                         ("2" (flatten)
                          (("2" (inst-cp - "k!1-1")
                            (("2" (inst - "k!1-2")
                              (("1"
                                (assert)
                                (("1"
                                  (assert)
                                  (("1"
                                    (inst - "i-1+k!1")
                                    (("1" (assertnil nil))
                                    nil))
                                  nil))
                                nil)
                               ("2" (assertnil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide 2)
            (("2" (induct "j")
              (("1" (assert)
                (("1" (skosimp*) (("1" (assertnil nil)) nil)) nil)
               ("2" (skosimp*)
                (("2" (assert)
                  (("2" (case "k!1=0")
                    (("1" (assertnil nil)
                     ("2" (assert)
                      (("2" (inst-cp - "k!1-1")
                        (("2" (case "k!1=1")
                          (("1" (hide -2)
                            (("1" (assert)
                              (("1"
                                (inst - "i")
                                (("1" (assertnil nil))
                                nil))
                              nil))
                            nil)
                           ("2" (inst - "k!1-2")
                            (("1" (assert)
                              (("1"
                                (inst - "i-k!1+1")
                                (("1" (assertnil nil))
                                nil))
                              nil)
                             ("2" (assertnil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("3" (skosimp*) (("3" (assertnil nil)) nil)
               ("4" (assert)
                (("4" (skosimp*) (("4" (assertnil nil)) nil)) nil)
               ("5" (skosimp*) (("5" (assertnil nil)) nil)
               ("6" (skosimp*) (("6" (assertnil nil)) nil)
               ("7" (skosimp*) (("7" (assertnil nil)) nil))
              nil))
            nil)
           ("3" (skosimp*) (("3" (assertnil nil)) nil))
          nil))
        nil)
       ("2" (hide 2)
        (("2" (skeep)
          (("2" (assert)
            (("2" (expand "sturm_sequence?")
              (("2" (flatten)
                (("2" (inst - "x" "i")
                  (("2" (assert)
                    (("2" (expand "sign_ext" -7)
                      (("2" (lift-if)
                        (("2" (lift-if)
                          (("2" (lift-if)
                            (("2" (lift-if)
                              (("2"
                                (assert)
                                (("2" (ground) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((IFF const-decl "[bool, bool -> bool]" booleans nil)
    (polynomial const-decl "[real -> real]" polynomials "reals/")
    (sequence type-eq-decl nil sequences nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (<= const-decl "bool" reals nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (k!1 skolem-const-decl "nat" sturmsquarefree nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (pred type-eq-decl nil defined_types nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (m skolem-const-decl "nat" sturmsquarefree nil)
    (j skolem-const-decl "upto(m)" sturmsquarefree nil)
    (i skolem-const-decl "nat" sturmsquarefree nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (upto nonempty-type-eq-decl nil naturalnumbers nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (k!1 skolem-const-decl "nat" sturmsquarefree nil)
    (sturm_sequence? const-decl "bool" sturmsquarefree nil)
    (sign_ext const-decl
     "{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}"
     sign "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   shostak))
 (sturm_seq_last_nonzero 0
  (sturm_seq_last_nonzero-1 nil 3588410248
   ("" (skeep)
    (("" (skeep)
      ((""
        (case "NOT FORALL (xyzp:real): polynomial(p(m),n(m))(xyzp) = 0")
        (("1" (skeep)
          (("1" (expand "sturm_sequence?")
            (("1" (flatten)
              (("1" (inst -6 "xyz" "xyzp")
                (("1" (expand "sign_ext" -6)
                  (("1" (assert)
                    (("1" (assert)
                      (("1" (lift-if) (("1" (assertnil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (lemma "polynomial_eq_coeff")
          (("2" (inst - "p(m)" "LAMBDA (i:nat): 0" "n(m)")
            (("2" (assert)
              (("2" (flatten)
                (("2" (hide -2)
                  (("2" (split -)
                    (("1" (inst - "n(m)")
                      (("1" (expand "sturm_sequence?")
                        (("1" (flatten)
                          (("1" (inst -5 "m") (("1" (assertnil nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (decompose-equality 1)
                      (("2" (inst - "x!1")
                        (("2" (assert)
                          (("2" (replaces -1)
                            (("2" (expand "polynomial" +)
                              (("2"
                                (rewrite "sigma_restrict_eq_0")
                                (("2"
                                  (skosimp*)
                                  (("2"
                                    (assert)
                                    (("2"
                                      (lift-if)
                                      (("2" (assertnil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((polynomial_eq_coeff formula-decl nil polynomials "reals/")
    (T_low type-eq-decl nil sigma "reals/")
    (T_high type-eq-decl nil sigma "reals/")
    (^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (sigma_restrict_eq_0 formula-decl nil sigma "reals/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (upto nonempty-type-eq-decl nil naturalnumbers nil)
    (<= const-decl "bool" reals nil)
    (sign_ext const-decl
     "{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}"
     sign "reals/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sturm_sequence? const-decl "bool" sturmsquarefree 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 "[T, T -> boolean]" equalities 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)
    (sequence type-eq-decl nil sequences nil)
    (polynomial const-decl "[real -> real]" polynomials "reals/"))
   shostak))
 (sturm_seq_first_signs_eq 0
  (sturm_seq_first_signs_eq-1 nil 3587370024
   ("" (skeep)
    ((""
      (case "NOT (polynomial(p(0), n(0))(x) /= 0 AND
                                    polynomial(p(0), n(0))(y) /= 0)")
      (("1" (hide 2)
        (("1" (inst-cp - "x")
          (("1" (inst - "y") (("1" (ground) nil nil)) nil)) nil))
        nil)
       ("2" (flatten)
        (("2" (assert)
          (("2" (inst-cp - "b")
            (("2" (assert)
              (("2" (flatten)
                (("2"
                  (case "polynomial(poly_deriv(p(0)),max(n(0)-1,0))(b) = 0")
                  (("1" (expand "sturm_sequence?")
                    (("1" (flatten)
                      (("1" (inst -8 "b")
                        (("1" (assert)
                          (("1" (expand "sign_ext" -8)
                            (("1" (assert)
                              (("1"
                                (lift-if)
                                (("1" (assertnil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (lemma "poly_continuous")
                    (("2"
                      (inst - "poly_deriv(p(0))" "max(n(0)-1,0)" "b"
                       "abs(polynomial(poly_deriv(p(0)),n(0)-1)(b))")
                      (("1" (skeep -)
                        (("1"
                          (case "EXISTS (deltiv:posreal): FORALL (x1:real): abs(b-x1))
                          (("1"
                            (case "sign_ext(polynomial(p(0), n(0))(x)) =
                                     -sign_ext(polynomial(poly_deriv(p(0)), max(n(0)-1,0))(b))
                                     AND
                                     sign_ext(polynomial(p(0), n(0))(y)) =
                                      sign_ext(polynomial(poly_deriv(p(0)), max(n(0)-1,0))(b))")
                            (("1" (hide (-2 -3))
                              (("1"
                                (flatten)
                                (("1"
                                  (expand "sturm_sequence?")
                                  (("1"
                                    (flatten)
                                    (("1"
                                      (inst -9 "b")
                                      (("1" (assertnil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (hide 6)
                              (("2"
                                (case
                                 "polynomial(poly_deriv(p(0)), max(n(0)-1,0))(b)>0")
                                (("1"
                                  (skeep -2)
                                  (("1"
                                    (case
                                     "FORALL (x1,x2:real): abs(x1-b))
                                    (("1"
                                      (inst-cp - "b-deltiv/2" "b")
                                      (("1"
                                        (inst-cp - "b" "b+deltiv/2")
                                        (("1"
                                          (label "hyplem" -1)
                                          (("1"
                                            (hide "hyplem")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (split +)
                                                (("1"
                                                  (expand "sign_ext")
                                                  (("1"
                                                    (lift-if)
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (split 1)
                                                        (("1"
                                                          (propax)
                                                          nil
                                                          nil)
                                                         ("2"
                                                          (assert)
                                                          (("2"
                                                            (hide -1)
                                                            (("2"
                                                              (split -)
                                                              (("1"
                                                                (replace
                                                                 -7)
                                                                (("1"
                                                                  (assert)
                                                                  (("1"
                                                                    (lemma
                                                                     "poly_intermediate_value_dec")
                                                                    (("1"
                                                                      (inst
                                                                       -
                                                                       "p(0)"
                                                                       "0"
                                                                       "n(0)"
                                                                       "x"
                                                                       "b-deltiv/2")
                                                                      (("1"
                                                                        (assert)
                                                                        (("1"
                                                                          (split
                                                                           -)
                                                                          (("1"
                                                                            (skeep
                                                                             -1)
                                                                            (("1"
                                                                              (inst
                                                                               -
                                                                               "cc")
                                                                              (("1"
                                                                                (inst
                                                                                 -
                                                                                 "cc")
                                                                                (("1"
                                                                                  (inst
                                                                                   -
                                                                                   "cc")
                                                                                  (("1"
                                                                                    (assert)
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (inst
                                                                             -
                                                                             "b-deltiv/2")
                                                                            (("2"
                                                                              (split
                                                                               -)
                                                                              (("1"
                                                                                (flatten)
                                                                                (("1"
                                                                                  (assert)
                                                                                  nil
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (hide-all-but
                                                                                 1)
                                                                                (("2"
                                                                                  (grind)
                                                                                  nil
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (hide-all-but
                                                                 1)
                                                                (("2"
                                                                  (grind)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (expand "sign_ext")
                                                  (("2"
                                                    (lift-if)
                                                    (("2"
                                                      (assert)
                                                      (("2"
                                                        (split 1)
                                                        (("1"
                                                          (assert)
                                                          (("1"
                                                            (hide -3)
                                                            (("1"
                                                              (split -)
                                                              (("1"
                                                                (replace
                                                                 -8)
                                                                (("1"
                                                                  (assert)
                                                                  (("1"
                                                                    (lemma
                                                                     "poly_intermediate_value_dec")
                                                                    (("1"
                                                                      (inst
                                                                       -
                                                                       "p(0)"
                                                                       "0"
                                                                       "n(0)"
                                                                       "b+deltiv/2"
                                                                       "y")
                                                                      (("1"
                                                                        (assert)
                                                                        (("1"
                                                                          (split
                                                                           -)
                                                                          (("1"
                                                                            (skeep
                                                                             -1)
                                                                            (("1"
                                                                              (inst
                                                                               -
                                                                               "cc")
                                                                              (("1"
                                                                                (inst
                                                                                 -
                                                                                 "cc")
                                                                                (("1"
                                                                                  (inst
                                                                                   -
                                                                                   "cc")
                                                                                  (("1"
                                                                                    (assert)
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (inst
                                                                             -
                                                                             "b+deltiv/2")
                                                                            (("2"
                                                                              (split
                                                                               -)
                                                                              (("1"
                                                                                (flatten)
                                                                                (("1"
                                                                                  (assert)
                                                                                  nil
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (hide-all-but
                                                                                 1)
                                                                                (("2"
                                                                                  (grind)
                                                                                  nil
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (hide-all-but
                                                                 1)
                                                                (("2"
                                                                  (grind)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (propax)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (skeep)
                                      (("2"
                                        (lemma
                                         "poly_strictly_increasing")
                                        (("2"
                                          (inst
                                           -
                                           "p(0)"
                                           "n(0)"
                                           "x1"
                                           "x2")
                                          (("2"
                                            (assert)
                                            (("2"
                                              (case "n(0)=0")
                                              (("1"
                                                (replaces -1)
                                                (("1"
                                                  (expand "polynomial")
                                                  (("1"
                                                    (expand "sigma")
                                                    (("1"
                                                      (expand "sigma")
                                                      (("1"
                                                        (propax)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (assert)
                                                (("2"
                                                  (skeep)
                                                  (("2"
                                                    (expand "max")
                                                    (("2"
                                                      (assert)
                                                      (("2"
                                                        (inst - "c")
                                                        (("2"
                                                          (assert)
                                                          (("2"
                                                            (split -)
                                                            (("1"
                                                              (inst
                                                               -
                                                               "c")
                                                              (("1"
                                                                (flatten)
                                                                (("1"
                                                                  (assert)
                                                                  (("1"
                                                                    (expand
                                                                     "abs")
                                                                    (("1"
                                                                      (lift-if)
                                                                      (("1"
                                                                        (ground)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (expand
                                                               "abs"
                                                               (-1
                                                                -2
                                                                -3
                                                                -4
                                                                -5
                                                                1))
                                                              (("2"
                                                                (lift-if)
                                                                (("2"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (case
                                   "polynomial(poly_deriv(p(0)), max(n(0)-1,0))(b)<0")
                                  (("1"
                                    (hide 1)
                                    (("1"
                                      (skeep -2)
                                      (("1"
                                        (case
                                         "FORALL (x1,x2:real): abs(x1-b) polynomial(p(0),n(0))(x2)")
                                        (("1"
                                          (inst-cp - "b-deltiv/2" "b")
                                          (("1"
                                            (inst-cp
                                             -
                                             "b"
                                             "b+deltiv/2")
                                            (("1"
                                              (label "hyplem" -1)
                                              (("1"
                                                (hide "hyplem")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (split +)
                                                    (("1"
                                                      (expand
                                                       "sign_ext")
                                                      (("1"
                                                        (lift-if)
                                                        (("1"
                                                          (assert)
                                                          (("1"
                                                            (split 1)
                                                            (("1"
                                                              (replace
                                                               -9)
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (lemma
                                                                   "poly_intermediate_value_inc")
                                                                  (("1"
                                                                    (inst
                                                                     -
                                                                     "p(0)"
                                                                     "0"
                                                                     "n(0)"
                                                                     "x"
                                                                     "b-deltiv/2")
                                                                    (("1"
                                                                      (assert)
                                                                      (("1"
                                                                        (split
                                                                         -)
                                                                        (("1"
                                                                          (skeep
                                                                           -1)
                                                                          (("1"
                                                                            (inst
                                                                             -
                                                                             "cc")
                                                                            (("1"
                                                                              (inst
                                                                               -
                                                                               "cc")
                                                                              (("1"
                                                                                (inst
                                                                                 -
                                                                                 "cc")
                                                                                (("1"
                                                                                  (assert)
                                                                                  nil
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil)
                                                                         ("2"
                                                                          (inst
                                                                           -
                                                                           "b-deltiv/2")
                                                                          (("2"
                                                                            (split
                                                                             -3)
                                                                            (("1"
                                                                              (assert)
                                                                              (("1"
                                                                                (hide-all-but
                                                                                 2)
                                                                                (("1"
                                                                                  (grind)
                                                                                  nil
                                                                                  nil))
                                                                                nil))
                                                                              nil)
                                                                             ("2"
                                                                              (hide-all-but
                                                                               1)
                                                                              (("2"
                                                                                (grind)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil)
                                                                         ("3"
                                                                          (assert)
                                                                          (("3"
                                                                            (hide-all-but
                                                                             2)
                                                                            (("3"
                                                                              (grind)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (propax)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (expand
                                                       "sign_ext")
                                                      (("2"
                                                        (lift-if)
                                                        (("2"
                                                          (assert)
                                                          (("2"
                                                            (split 1)
                                                            (("1"
                                                              (propax)
                                                              nil
                                                              nil)
                                                             ("2"
                                                              (assert)
                                                              (("2"
                                                                (hide
                                                                 -2)
                                                                (("2"
                                                                  (split
                                                                   -)
                                                                  (("1"
                                                                    (replace
                                                                     -7)
                                                                    (("1"
                                                                      (assert)
                                                                      (("1"
                                                                        (lemma
                                                                         "poly_intermediate_value_inc")
                                                                        (("1"
                                                                          (inst
                                                                           -
                                                                           "p(0)"
                                                                           "0"
                                                                           "n(0)"
                                                                           "b+deltiv/2"
                                                                           "y")
                                                                          (("1"
                                                                            (assert)
                                                                            (("1"
                                                                              (split
                                                                               -)
                                                                              (("1"
                                                                                (skeep
                                                                                 -1)
                                                                                (("1"
                                                                                  (inst
                                                                                   -
                                                                                   "cc")
                                                                                  (("1"
                                                                                    (inst
                                                                                     -
                                                                                     "cc")
                                                                                    (("1"
                                                                                      (inst
                                                                                       -
                                                                                       "cc")
                                                                                      (("1"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (inst
                                                                                 -
                                                                                 "b+deltiv/2")
                                                                                (("2"
                                                                                  (split
                                                                                   -)
                                                                                  (("1"
                                                                                    (flatten)
                                                                                    (("1"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil)
                                                                                   ("2"
                                                                                    (hide-all-but
                                                                                     1)
                                                                                    (("2"
                                                                                      (grind)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (hide-all-but
                                                                     1)
                                                                    (("2"
                                                                      (grind)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (skeep)
                                          (("2"
                                            (lemma
                                             "poly_strictly_decreasing")
                                            (("2"
                                              (inst
                                               -
                                               "p(0)"
                                               "n(0)"
                                               "x1"
                                               "x2")
                                              (("2"
                                                (assert)
                                                (("2"
                                                  (case "n(0)=0")
                                                  (("1"
                                                    (replaces -1)
                                                    (("1"
                                                      (expand
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.67 Sekunden  (vorverarbeitet)  ¤





Download des
Quellennavigators
Download des
sprechenden Kalenders

Eigene Datei ansehen




Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff