Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: continuous_linear.prf Sprache: Lisp

Original von: PVS^©

(continuous_linear
(linear_cont_TCC1 0
  (linear_cont_TCC1-1 nil 3430729650
   ("" (skosimp*)
    (("" (lemma "connected_domain")
      (("" (inst?) (("" (inst - "y!1") (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((connected_domain formula-decl nil continuous_linear nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (T formal-subtype-decl nil continuous_linear nil)
    (T_pred const-decl "[real -> boolean]" continuous_linear 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))
   nil))
(linear_cont_TCC2 0
  (linear_cont_TCC2-1 nil 3430729650
   ("" (lemma "not_one_element") (("" (propax) nil nil)) nil)
   ((not_one_element formula-decl nil continuous_linear nil)) nil))
(linear_cont 0
  (linear_cont-3 nil 3258280425
   ("" (skosimp*)
    (("" (expand "linear?")
      (("" (skosimp*)
        (("" (replace -1 * lr)
          (("" (hide -1)
            (("" (expand "continuous?")
              (("" (skosimp*)
                (("" (lemma "identity_continuous[T]")
                  (("" (inst -1 "x0!1")
                    (("" (lemma "scal_continuous[T]")
                      (("" (inst -1 "I[T]" "m!1" "x0!1")
                        (("" (assert)
                          (("" (hide -2)
                            (("" (lemma "sum_continuous[T]")
                              ((""
                                (inst
                                 -1
                                 "m!1 * I[T]"
                                 "const_fun(k!1)"
                                 "x0!1")
                                ((""
                                  (assert)
                                  ((""
                                    (split -1)
                                    (("1"
                                      (expand "*")
                                      (("1"
                                        (expand "const_fun")
                                        (("1"
                                          (expand "+ ")
                                          (("1"
                                            (expand "I")
                                            (("1" (propax) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (rewrite "const_continuous[T]")
                                      nil
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (linear? const-decl "bool" linear_functions nil)
    (continuous? const-decl "bool" continuous_functions nil)
    (T formal-subtype-decl nil continuous_linear nil)
    (T_pred const-decl "[real -> boolean]" continuous_linear 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)
    (identity_continuous formula-decl nil continuous_functions nil)
    (scal_continuous formula-decl nil continuous_functions nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (id_fun_continuous name-judgement "continuous_fun"
     continuous_functions nil)
    (sum_continuous formula-decl nil continuous_functions nil)
    (const_fun_continuous application-judgement "continuous_fun"
     continuous_functions nil)
    (scal_fun_continuous application-judgement "continuous_fun"
     continuous_functions nil)
    (const_continuous formula-decl nil continuous_functions nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (const_fun const-decl "[T -> real]" real_fun_ops "reals/")
    (bool nonempty-type-eq-decl nil booleans nil)
    (bijective? const-decl "bool" functions nil)
    (I const-decl "(bijective?[T, T])" identity nil))
   nil)
  (linear_cont-2 nil 3257796697
   ("" (skosimp*)
    (("" (replace -1)
      (("" (hide -1)
        (("" (expand "continuous?")
          (("" (skosimp*)
            (("" (lemma "identity_continuous[T]")
              (("" (inst -1 "x0!1")
                (("" (lemma "scal_continuous[T]")
                  (("" (inst -1 "I[T]" "m!1" "x0!1")
                    (("" (assert)
                      (("" (hide -2)
                        (("" (lemma "sum_continuous[T]")
                          ((""
                            (inst -1 "m!1 * I[T]" "const_fun(c!1)"
                             "x0!1")
                            (("" (assert)
                              ((""
                                (split -1)
                                (("1"
                                  (expand "*")
                                  (("1"
                                    (expand "const_fun")
                                    (("1"
                                      (expand "+ ")
                                      (("1"
                                        (expand "I")
                                        (("1" (propax) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (rewrite "const_continuous[T]")
                                  nil
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((identity_continuous formula-decl nil continuous_functions nil)
    (scal_continuous formula-decl nil continuous_functions nil)
    (sum_continuous formula-decl nil continuous_functions nil)
    (const_continuous formula-decl nil continuous_functions nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (const_fun const-decl "[T -> real]" real_fun_ops "reals/"))
   nil)
  (linear_cont-1 nil 3257796139
   ("" (skosimp*)
    (("" (replace -1)
      (("" (hide -1)
        (("" (expand "continuous?")
          (("" (skosimp*)
            (("" (lemma "identity_continuous[T]")
              (("" (inst -1 "x0!1")
                (("" (lemma "scal_continuous[T]")
                  (("" (inst -1 "I[T]" "m!1" "x0!1")
                    (("" (assert)
                      (("" (hide -2)
                        (("" (lemma "sum_continuous[T]")
                          ((""
                            (inst -1 "m!1 * I[T]" "const_fun(b!1)"
                             "x0!1")
                            (("" (assert)
                              ((""
                                (split -1)
                                (("1"
                                  (expand "*")
                                  (("1"
                                    (expand "const_fun")
                                    (("1"
                                      (expand "+ ")
                                      (("1"
                                        (expand "I")
                                        (("1" (propax) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (rewrite "const_continuous[T]")
                                  nil
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((identity_continuous formula-decl nil continuous_functions nil)
    (scal_continuous formula-decl nil continuous_functions nil)
    (sum_continuous formula-decl nil continuous_functions nil)
    (const_continuous formula-decl nil continuous_functions nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (const_fun const-decl "[T -> real]" real_fun_ops "reals/"))
   shostak))
(cont_in_linear 0
  (cont_in_linear-1 nil 3258990857
   ("" (skosimp*)
    (("" (expand "continuous_in?")
      (("" (skosimp*)
        (("" (rewrite continuity_def)
          (("" (expand "convergence")
            (("" (expand "convergence")
              (("" (expand "fullset")
                (("" (expand "linear_on?")
                  (("" (skosimp*)
                    (("" (prop)
                      (("1" (expand "adh")
                        (("1" (skosimp*)
                          (("1" (inst + "min(x!1+e!1/2,(x!1+b!1)/2)")
                            (("1" (hide -1) (("1" (grind) nil nil))
                              nil)
                             ("2" (expand "min")
                              (("2"
                                (ground)
                                (("1"
                                  (lemma "connected_domain")
                                  (("1"
                                    (inst?)
                                    (("1"
                                      (inst -1 "a!1" "b!1")
                                      (("1" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (lemma "connected_domain")
                                  (("2"
                                    (inst?)
                                    (("2"
                                      (inst -1 "a!1" "b!1")
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (skosimp*)
                        (("2" (case-replace "m!1 = 0")
                          (("1"
                            (inst +
                             "min(epsilon!1,min(abs(x!1-a!1),abs(b!1-x!1)))")
                            (("1" (skosimp*)
                              (("1"
                                (inst-cp -3 "x!1")
                                (("1"
                                  (inst - "x!2")
                                  (("1"
                                    (assert)
                                    (("1"
                                      (split -3)
                                      (("1"
                                        (replace -1)
                                        (("1"
                                          (hide -1)
                                          (("1"
                                            (replace -3)
                                            (("1" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (expand "abs")
                                        (("2"
                                          (assert)
                                          (("2"
                                            (hide -1 -3 2)
                                            (("2"
                                              (case
                                               "abs(x!2 - x!1) < abs(x!1 - a!1)")
                                              (("1"
                                                (hide -2)
                                                (("1" (grind) nil nil))
                                                nil)
                                               ("2"
                                                (expand "min")
                                                (("2"
                                                  (lift-if)
                                                  (("2"
                                                    (ground)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("3"
                                        (case
                                         "abs(x!2 - x!1) < abs(b!1 - x!1)")
                                        (("1"
                                          (hide -3)
                                          (("1" (grind) nil nil))
                                          nil)
                                         ("2"
                                          (hide 3)
                                          (("2" (grind) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (grind) nil nil))
                            nil)
                           ("2"
                            (inst +
                             "min(epsilon!1/abs(m!1),min(abs(x!1-a!1),abs(b!1-x!1)))")
                            (("1" (skosimp*)
                              (("1"
                                (inst-cp - "x!1")
                                (("1"
                                  (inst - "x!2")
                                  (("1"
                                    (assert)
                                    (("1"
                                      (split -2)
                                      (("1"
                                        (replace -1)
                                        (("1"
                                          (hide -1)
                                          (("1"
                                            (replace -2)
                                            (("1"
                                              (hide -2)
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (case-replace
                                                   "m!1 * x!2 - m!1 * x!1 = m!1 * (x!2 - x!1)")
                                                  (("1"
                                                    (rewrite
                                                     "abs_mult")
                                                    (("1"
                                                      (case
                                                       "abs(x!2 - x!1) < epsilon!1 / abs(m!1)")
                                                      (("1"
                                                        (hide -3)
                                                        (("1"
                                                          (cross-mult
                                                           -1)
                                                          (("1"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (hide-all-but
                                                         (-2 1))
                                                        (("2"
                                                          (grind)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (ground)
                                        (("2"
                                          (case
                                           "abs(x!2 - x!1) <
                                     abs(x!1 - a!1)")
                                          (("1"
                                            (hide -2 3)
                                            (("1" (grind) nil nil))
                                            nil)
                                           ("2"
                                            (hide 4)
                                            (("2" (grind) nil nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("3"
                                        (case
                                         "abs(x!2 - x!1) < abs(b!1 - x!1)")
                                        (("1"
                                          (hide -1 3)
                                          (("1" (grind) nil nil))
                                          nil)
                                         ("2"
                                          (hide 4)
                                          (("2" (grind) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (case "epsilon!1 / abs(m!1) > 0")
                              (("1"
                                (name-replace
                                 "EOM"
                                 "epsilon!1 / abs(m!1)")
                                (("1" (grind) nil nil))
                                nil)
                               ("2"
                                (hide 2)
                                (("2"
                                  (cross-mult 1)
                                  (("2" (grind) nil nil))
                                  nil))
                                nil)
                               ("3"
                                (hide 2)
                                (("3" (grind) nil nil))
                                nil))
                              nil)
                             ("3" (hide -1)
                              (("3"
                                (lemma "abs_eq_0")
                                (("3"
                                  (inst?)
                                  (("3" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((continuous_in? const-decl "bool" continuous_linear nil)
    (continuity_def formula-decl nil continuous_functions 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)
    (T_pred const-decl "[real -> boolean]" continuous_linear nil)
    (T formal-subtype-decl nil continuous_linear nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (convergence const-decl "bool" convergence_functions nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (linear_on? const-decl "bool" linear_functions nil)
    (connected_domain formula-decl nil continuous_linear nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (e!1 skolem-const-decl "posreal" continuous_linear nil)
    (x!1 skolem-const-decl "T" continuous_linear nil)
    (b!1 skolem-const-decl "T" continuous_linear nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (adh const-decl "setof[real]" convergence_functions nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (abs_0 formula-decl nil abs_lems "reals/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (< const-decl "bool" reals nil)
    (epsilon!1 skolem-const-decl "posreal" continuous_linear nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (a!1 skolem-const-decl "T" continuous_linear nil)
    (nonneg_real_min application-judgement
     "{z: nonneg_real | z <= x AND z <= y}" real_defs nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (abs_eq_0 formula-decl nil abs_lems "reals/")
    (EOM skolem-const-decl "nzreal" continuous_linear nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (div_mult_pos_gt1 formula-decl nil extra_real_props nil)
    (abs_nat formula-decl nil abs_lems "reals/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (div_mult_pos_lt2 formula-decl nil real_props nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (abs_mult formula-decl nil real_props nil)
    (m!1 skolem-const-decl "real" continuous_linear nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (fullset const-decl "set" sets nil)
    (convergence const-decl "bool" lim_of_functions nil))
   nil))
(unary_minus_dist 0
  (unary_minus_dist-1 nil 3258987029
   ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((real_minus_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
(piecewise 0
  (piecewise-3 nil 3258287121
   ("" (skosimp*)
    (("" (assert)
      (("" (rewrite continuity_def)
        (("" (expand "convergence")
          (("" (expand "fullset")
            (("" (expand "linear_on?")
              (("" (skosimp*)
                (("" (expand "convergence")
                  (("" (prop)
                    (("1" (expand "adh")
                      (("1" (skosimp*)
                        (("1" (inst + "b!1")
                          (("1" (expand "abs") (("1" (assert) nil nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (skosimp*)
                      (("2" (case "m!1 = 0 AND m!2 = 0")
                        (("1" (flatten)
                          (("1" (replace -1)
                            (("1" (replace -2)
                              (("1"
                                (assert)
                                (("1"
                                  (inst
                                   +
                                   "min(abs(b!1-a!1),abs(c!1-b!1))")
                                  (("1"
                                    (skosimp*)
                                    (("1"
                                      (lift-if)
                                      (("1"
                                        (ground)
                                        (("1"
                                          (hide -9)
                                          (("1"
                                            (inst-cp - "x!1")
                                            (("1"
                                              (inst - "b!1")
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (replace -8)
                                                  (("1"
                                                    (split -9)
                                                    (("1"
                                                      (replace -1)
                                                      (("1"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (expand "abs")
                                                      (("2"
                                                        (assert)
                                                        (("2"
                                                          (hide 2)
                                                          (("2"
                                                            (grind)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (hide -7)
                                          (("2"
                                            (inst-cp - "x!1")
                                            (("2"
                                              (inst - "b!1")
                                              (("2"
                                                (assert)
                                                (("2"
                                                  (replace -4 * rl)
                                                  (("2"
                                                    (replace -7)
                                                    (("2"
                                                      (split -8)
                                                      (("1"
                                                        (replace -1)
                                                        (("1"
                                                          (expand
                                                           "abs")
                                                          (("1"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (hide 3)
                                                        (("2"
                                                          (grind)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2" (grind) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2"
                          (name "Mabc"
                                "min(abs(b!1-a!1),abs(c!1-b!1))")
                          (("2" (case-replace "m!1 = 0")
                            (("1" (assert)
                              (("1"
                                (hide -1)
                                (("1"
                                  (inst
                                   +
                                   "min(epsilon!1/abs(m!2), Mabc)")
                                  (("1"
                                    (skosimp*)
                                    (("1"
                                      (lift-if)
                                      (("1"
                                        (case "x!1 <= b!1")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (replace -2 * rl)
                                            (("1"
                                              (hide -2)
                                              (("1"
                                                (hide -7)
                                                (("1"
                                                  (inst-cp - "x!1")
                                                  (("1"
                                                    (inst - "b!1")
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (replace -6)
                                                        (("1"
                                                          (split -7)
                                                          (("1"
                                                            (replace
                                                             -1)
                                                            (("1"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (expand
                                                             "abs")
                                                            (("2"
                                                              (assert)
                                                              (("2"
                                                                (grind)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (assert)
                                          (("2"
                                            (hide -6)
                                            (("2"
                                              (hide -2)
                                              (("2"
                                                (replace -2)
                                                (("2"
                                                  (inst-cp - "x!1")
                                                  (("2"
                                                    (inst - "b!1")
                                                    (("2"
                                                      (assert)
                                                      (("2"
                                                        (replace -5)
                                                        (("2"
                                                          (split -6)
                                                          (("1"
                                                            (replace
                                                             -1)
                                                            (("1"
                                                              (assert)
                                                              (("1"
                                                                (case-replace
                                                                 "m!2 * x!1 - m!2 * b!1 = m!2 * (x!1 - b!1)")
                                                                (("1"
                                                                  (rewrite
                                                                   "abs_mult")
                                                                  (("1"
                                                                    (div-by
                                                                     3
                                                                     "abs(m!2)")
                                                                    (("1"
                                                                      (grind
                                                                       :exclude
                                                                       "abs")
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (hide 4)
                                                            (("2"
                                                              (grind)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (case "epsilon!1 / abs(m!2) > 0")
                                    (("1" (grind) nil nil)
                                     ("2"
                                      (case "abs(m!2) = 0")
                                      (("1"
                                        (expand "abs" -1)
                                        (("1"
                                          (assert)
                                          (("1"
                                            (lift-if)
                                            (("1" (ground) nil nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (mult-by 2 "abs(m!2)")
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil)
                                     ("3"
                                      (expand "abs" 1)
                                      (("3"
                                        (assert)
                                        (("3"
                                          (ground)
                                          (("1"
                                            (lift-if)
                                            (("1" (ground) nil nil))
                                            nil)
                                           ("2"
                                            (lift-if)
                                            (("2" (ground) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("3"
                                    (expand "abs" 1)
                                    (("3"
                                      (lift-if)
                                      (("3" (ground) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (assert)
                              (("2"
                                (case-replace "m!2 = 0")
                                (("1"
                                  (hide -1)
                                  (("1"
                                    (inst
                                     +
                                     "min(epsilon!1/abs(m!1), Mabc)")
                                    (("1"
                                      (skosimp*)
                                      (("1"
                                        (assert)
                                        (("1"
                                          (lift-if)
                                          (("1"
                                            (case "x!1 <= b!1")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (replace -2 * rl)
                                                (("1"
                                                  (hide -2)
                                                  (("1"
                                                    (hide -7)
                                                    (("1"
                                                      (inst-cp - "x!1")
                                                      (("1"
                                                        (inst - "b!1")
                                                        (("1"
                                                          (replace -1)
                                                          (("1"
                                                            (split -6)
                                                            (("1"
                                                              (replace
                                                               -1)
                                                              (("1"
                                                                (split
                                                                 -7)
                                                                (("1"
                                                                  (replace
                                                                   -1)
                                                                  (("1"
                                                                    (assert)
                                                                    (("1"
                                                                      (case-replace
                                                                       "m!1 * x!1 - m!1 * b!1 = m!1 * (x!1 - b!1)")
                                                                      (("1"
                                                                        (hide
                                                                         -1)
                                                                        (("1"
                                                                          (rewrite
                                                                           "abs_mult")
                                                                          (("1"
                                                                            (div-by
                                                                             2
                                                                             "abs(m!1)")
                                                                            (("1"
                                                                              (grind
                                                                               :exclude
                                                                               "abs")
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (assert)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (hide
                                                                   3)
                                                                  (("2"
                                                                    (grind)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (assert)
                                                              nil
                                                              nil)
                                                             ("3"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (assert)
                                              (("2"
                                                (replace -1 * rl)
                                                (("2"
                                                  (hide -1)
                                                  (("2"
                                                    (hide -5)
                                                    (("2"
                                                      (replace -2)
                                                      (("2"
                                                        (inst-cp
                                                         -
                                                         "x!1")
                                                        (("2"
                                                          (inst
                                                           -
                                                           "b!1")
                                                          (("2"
                                                            (assert)
                                                            (("2"
                                                              (replace
                                                               -5)
                                                              (("2"
                                                                (split
                                                                 -6)
                                                                (("1"
                                                                  (replace
                                                                   -1)
                                                                  (("1"
                                                                    (expand
                                                                     "abs")
                                                                    (("1"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (hide
                                                                   4)
                                                                  (("2"
                                                                    (grind)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (case "epsilon!1 / abs(m!1) > 0")
                                      (("1" (grind) nil nil)
                                       ("2"
                                        (hide 2)
                                        (("2"
                                          (case "abs(m!1) = 0")
                                          (("1"
                                            (expand "abs")
                                            (("1"
                                              (lift-if)
                                              (("1" (ground) nil nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (cross-mult 2)
                                            (("2" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("3" (assert) nil nil))
                                      nil)
                                     ("3"
                                      (expand "abs" 1)
                                      (("3"
                                        (assert)
                                        (("3"
                                          (flatten)
                                          (("3"
                                            (expand "abs")
                                            (("3"
                                              (lift-if)
                                              (("3" (ground) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (assert)
                                  (("2"
                                    (case-replace
                                     "abs(m!1) > 0 AND abs(m!2) > 0")
                                    (("1"
                                      (flatten)
                                      (("1"
                                        (name
                                         "MEPS"
                                         "min(epsilon!1/abs(m!1),epsilon!1/abs(m!2))")
                                        (("1"
                                          (inst + "min(MEPS,Mabc)")
                                          (("1"
                                            (skosimp*)
                                            (("1"
                                              (lift-if)
                                              (("1"
                                                (case "x!1 <= b!1")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (hide -11)
                                                    (("1"
                                                      (inst-cp - "x!1")
                                                      (("1"
                                                        (inst - "b!1")
                                                        (("1"
                                                          (assert)
                                                          (("1"
                                                            (replace
                                                             -10)
                                                            (("1"
                                                              (split
                                                               -11)
                                                              (("1"
                                                                (replace
                                                                 -1)
                                                                (("1"
                                                                  (case-replace
                                                                   "m!1 * x!1 - m!1 * b!1 = m!1 * (x!1 - b!1)")
                                                                  (("1"
                                                                    (rewrite
                                                                     "abs_mult")
                                                                    (("1"
                                                                      (div-by
                                                                       3
                                                                       "abs(m!1)")
                                                                      (("1"
                                                                        (case-replace
                                                                         "abs((x!1 - b!1)) < MEPS")
                                                                        (("1"
                                                                          (replace
                                                                           -5
                                                                           *
                                                                           rl)
                                                                          (("1"
                                                                            (hide-all-but
                                                                             (-1
                                                                              1
                                                                              2
                                                                              3))
                                                                            (("1"
                                                                              (expand
                                                                               "min")
                                                                              (("1"
                                                                                (lift-if)
                                                                                (("1"
                                                                                  (ground)
                                                                                  nil
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil)
                                                                         ("2"
                                                                          (hide
                                                                           4)
                                                                          (("2"
                                                                            (hide
                                                                             -7)
                                                                            (("2"
                                                                              (grind
                                                                               :exclude
                                                                               "abs")
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (assert)
                                                                (("2"
                                                                  (assert)
                                                                  (("2"
                                                                    (hide
                                                                     4)
                                                                    (("2"
                                                                      (hide
                                                                       -2)
                                                                      (("2"
                                                                        (hide
                                                                         -2
                                                                         -3)
                                                                        (("2"
                                                                          (replace
                                                                           -2
                                                                           *
                                                                           rl)
                                                                          (("2"
                                                                            (hide
                                                                             -2)
                                                                            (("2"
                                                                              (grind)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (assert)
                                                  (("2"
                                                    (hide -9)
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.41 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.