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

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: vs_bands.prf   Sprache: Lisp

Original von: PVS©
(vs_bands
 (vs_bands_vertical_dir_exclusive 0
  (vs_bands_vertical_dir_exclusive-1 nil 3477244353
   ("" (skeep)
    (("" (split +)
      (("1" (flatten)
        (("1" (split -)
          (("1" (flatten)
            (("1" (replace -1)
              (("1" (hide -1)
                (("1" (replace -1)
                  (("1" (hide -1)
                    (("1" (expand "abs")
                      (("1" (lift-if)
                        (("1" (split -2)
                          (("1" (flatten)
                            (("1" (neg-formula -2)
                              (("1"
                                (replace -1)
                                (("1"
                                  (case "vsp - viz < 0")
                                  (("1"
                                    (case "sz + B*(vsp-viz) > -H")
                                    (("1"
                                      (copy 2)
                                      (("1"
                                        (expand "conflict_vertical?")
                                        (("1"
                                          (inst + "B")
                                          (("1"
                                            (case
                                             "sz + B*(vsp-viz) >= H")
                                            (("1"
                                              (name
                                               "newt"
                                               "-sz/(vsp-viz)")
                                              (("1"
                                                (case
                                                 "B <= newt and newt <= T")
                                                (("1"
                                                  (flatten)
                                                  (("1"
                                                    (inst + "newt")
                                                    (("1"
                                                      (case
                                                       "sz + newt*(vsp-viz) = 0")
                                                      (("1"
                                                        (assert)
                                                        nil)
                                                       ("2"
                                                        (replace
                                                         -3
                                                         :dir
                                                         rl)
                                                        (("2"
                                                          (name
                                                           "const3"
                                                           "vsp-viz")
                                                          (("2"
                                                            (replace
                                                             -1)
                                                            (("2"
                                                              (both-sides
                                                               "-"
                                                               "sz"
                                                               1)
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (cross-mult
                                                                   1)
                                                                  nil)))
                                                               ("2"
                                                                (assert)
                                                                nil)))))))))))
                                                     ("2"
                                                      (assert)
                                                      nil)))))
                                                 ("2"
                                                  (replace -1 :dir rl)
                                                  (("2"
                                                    (split 1)
                                                    (("1"
                                                      (cross-mult 1)
                                                      (("1"
                                                        (typepred "T")
                                                        (("1"
                                                          (mult-by
                                                           -3
                                                           "viz-vsp")
                                                          (("1"
                                                            (assert)
                                                            nil)))))))
                                                     ("2"
                                                      (cross-mult 1)
                                                      (("2"
                                                        (typepred "T")
                                                        (("2"
                                                          (mult-by
                                                           -3
                                                           "viz-vsp")
                                                          (("2"
                                                            (assert)
                                                            nil)))))))))))))
                                               ("2" (assert) nil)))
                                             ("2"
                                              (expand "abs" 2)
                                              (("2"
                                                (lift-if)
                                                (("2"
                                                  (ground)
                                                  nil)))))))))))))
                                     ("2"
                                      (mult-by -1 "T-B")
                                      (("2" (assert) nil)))))
                                   ("2"
                                    (mult-by 2 "H")
                                    (("2"
                                      (mult-by 1 "H")
                                      (("2" (assert) nil)))))))))))))
                           ("2" (flatten)
                            (("2" (replace -1)
                              (("2"
                                (case "vsp > viz")
                                (("1"
                                  (case "sz + B*(vsp-viz) < H")
                                  (("1"
                                    (hide 1)
                                    (("1"
                                      (copy 2)
                                      (("1"
                                        (expand "conflict_vertical?")
                                        (("1"
                                          (inst + "B")
                                          (("1"
                                            (case
                                             "sz + B*(vsp-viz) <= -H")
                                            (("1"
                                              (name
                                               "newt"
                                               "-sz/(vsp-viz)")
                                              (("1"
                                                (case
                                                 "B <= newt and newt <= T")
                                                (("1"
                                                  (flatten)
                                                  (("1"
                                                    (inst + "newt")
                                                    (("1"
                                                      (case
                                                       "sz + newt*(vsp-viz) = 0")
                                                      (("1"
                                                        (assert)
                                                        nil)
                                                       ("2"
                                                        (replace
                                                         -3
                                                         :dir
                                                         rl)
                                                        (("2"
                                                          (name
                                                           "const3"
                                                           "vsp-viz")
                                                          (("2"
                                                            (replace
                                                             -1)
                                                            (("2"
                                                              (both-sides
                                                               "-"
                                                               "sz"
                                                               1)
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (cross-mult
                                                                   1)
                                                                  nil)))
                                                               ("2"
                                                                (assert)
                                                                nil)))))))))))
                                                     ("2"
                                                      (assert)
                                                      nil)))))
                                                 ("2"
                                                  (replace -1 :dir rl)
                                                  (("2"
                                                    (split 1)
                                                    (("1"
                                                      (cross-mult 1)
                                                      (("1"
                                                        (typepred "T")
                                                        (("1"
                                                          (mult-by
                                                           -3
                                                           "vsp-viz")
                                                          (("1"
                                                            (assert)
                                                            nil)))))))
                                                     ("2"
                                                      (cross-mult 1)
                                                      (("2"
                                                        (typepred "T")
                                                        (("2"
                                                          (mult-by
                                                           -3
                                                           "vsp-viz")
                                                          (("2"
                                                            (assert)
                                                            nil)))))))))))))
                                               ("2" (assert) nil)))
                                             ("2"
                                              (expand "abs" 2)
                                              (("2"
                                                (lift-if)
                                                (("2"
                                                  (ground)
                                                  nil)))))))
                                           ("2" (assert) nil)))))))))
                                   ("2"
                                    (typepred "T")
                                    (("2"
                                      (mult-by -3 "vsp-viz")
                                      (("2" (assert) nil)))))))
                                 ("2"
                                  (mult-by 1 "H")
                                  (("2"
                                    (mult-by 3 "H")
                                    (("2"
                                      (assert)
                                      nil)))))))))))))))))))))))))))
           ("2" (flatten)
            (("2" (replace -1)
              (("2" (hide -1)
                (("2" (replace -1)
                  (("2" (hide -1)
                    (("2" (expand "abs")
                      (("2" (lift-if)
                        (("2" (split -)
                          (("1" (flatten)
                            (("1" (neg-formula -2)
                              (("1"
                                (replace -1)
                                (("1"
                                  (case "vsp>viz")
                                  (("1"
                                    (case "sz + T*(vsp-viz) > -H")
                                    (("1"
                                      (copy 2)
                                      (("1"
                                        (expand "conflict_vertical?")
                                        (("1"
                                          (inst + "T")
                                          (("1"
                                            (case
                                             "sz + T*(vsp-viz) >= H")
                                            (("1"
                                              (name
                                               "newt"
                                               "-sz/(vsp-viz)")
                                              (("1"
                                                (case
                                                 "B <= newt and newt <= T")
                                                (("1"
                                                  (flatten)
                                                  (("1"
                                                    (case
                                                     "sz + newt*(vsp-viz) = 0")
                                                    (("1"
                                                      (inst + "newt")
                                                      (("1"
                                                        (assert)
                                                        nil)
                                                       ("2"
                                                        (assert)
                                                        nil)))
                                                     ("2"
                                                      (replace
                                                       -3
                                                       :dir
                                                       rl)
                                                      (("2"
                                                        (name
                                                         "const3"
                                                         "vsp-viz")
                                                        (("2"
                                                          (replace -1)
                                                          (("2"
                                                            (both-sides
                                                             "-"
                                                             "sz"
                                                             1)
                                                            (("1"
                                                              (assert)
                                                              (("1"
                                                                (cross-mult
                                                                 1)
                                                                nil)))
                                                             ("2"
                                                              (assert)
                                                              nil)))))))))))))
                                                 ("2"
                                                  (replace -1 :dir rl)
                                                  (("2"
                                                    (split +)
                                                    (("1"
                                                      (cross-mult 1)
                                                      (("1"
                                                        (typepred "T")
                                                        (("1"
                                                          (mult-by
                                                           -2
                                                           "vsp-viz")
                                                          (("1"
                                                            (assert)
                                                            nil)))))))
                                                     ("2"
                                                      (cross-mult 1)
                                                      (("2"
                                                        (typepred "T")
                                                        (("2"
                                                          (mult-by
                                                           -3
                                                           "vsp-viz")
                                                          (("2"
                                                            (assert)
                                                            nil)))))))))))))
                                               ("2" (assert) nil)))
                                             ("2"
                                              (expand "abs" 2)
                                              (("2"
                                                (lift-if)
                                                (("2"
                                                  (ground)
                                                  nil)))))))
                                           ("2" (assert) nil)))))))
                                     ("2"
                                      (typepred "T")
                                      (("2"
                                        (mult-by -3 "vsp-viz")
                                        (("2" (assert) nil)))))))
                                   ("2"
                                    (mult-by 1 "H")
                                    (("2"
                                      (mult-by 2 "H")
                                      (("2" (assert) nil)))))))))))))
                           ("2" (flatten)
                            (("2" (replace -1)
                              (("2"
                                (hide 1)
                                (("2"
                                  (case "vsp < viz")
                                  (("1"
                                    (case "sz + T*(vsp-viz) < H")
                                    (("1"
                                      (copy 2)
                                      (("1"
                                        (expand "conflict_vertical?")
                                        (("1"
                                          (inst + "T")
                                          (("1"
                                            (case
                                             "sz + T*(vsp-viz) <= -H")
                                            (("1"
                                              (name
                                               "newt"
                                               "-sz/(vsp-viz)")
                                              (("1"
                                                (case
                                                 "B <= newt and newt <= T")
                                                (("1"
                                                  (flatten)
                                                  (("1"
                                                    (case
                                                     "sz + newt*(vsp-viz) = 0")
                                                    (("1"
                                                      (inst + "newt")
                                                      (("1"
                                                        (assert)
                                                        nil)
                                                       ("2"
                                                        (assert)
                                                        nil)))
                                                     ("2"
                                                      (replace
                                                       -3
                                                       :dir
                                                       rl)
                                                      (("2"
                                                        (name
                                                         "const3"
                                                         "vsp-viz")
                                                        (("2"
                                                          (replace -1)
                                                          (("2"
                                                            (both-sides
                                                             "-"
                                                             "sz"
                                                             1)
                                                            (("1"
                                                              (assert)
                                                              (("1"
                                                                (cross-mult
                                                                 1)
                                                                nil)))
                                                             ("2"
                                                              (assert)
                                                              nil)))))))))))))
                                                 ("2"
                                                  (replace -1 :dir rl)
                                                  (("2"
                                                    (split +)
                                                    (("1"
                                                      (cross-mult 1)
                                                      (("1"
                                                        (typepred "T")
                                                        (("1"
                                                          (mult-by
                                                           -3
                                                           "viz-vsp")
                                                          (("1"
                                                            (assert)
                                                            nil)))))))
                                                     ("2"
                                                      (cross-mult 1)
                                                      (("2"
                                                        (typepred "T")
                                                        (("2"
                                                          (mult-by
                                                           -3
                                                           "viz-vsp")
                                                          (("2"
                                                            (assert)
                                                            nil)))))))))))))
                                               ("2" (assert) nil)))
                                             ("2"
                                              (expand "abs")
                                              (("2"
                                                (lift-if)
                                                (("2"
                                                  (ground)
                                                  nil)))))))
                                           ("2" (assert) nil)))))))
                                     ("2"
                                      (typepred "T")
                                      (("2"
                                        (mult-by -3 "viz-vsp")
                                        (("2" (assert) nil)))))))
                                   ("2"
                                    (mult-by 1 "H")
                                    (("2"
                                      (mult-by 2 "H")
                                      (("2"
                                        (assert)
                                        nil)))))))))))))))))))))))))))))))))
       ("2" (flatten)
        (("2" (case "vsp - viz = 0")
          (("1" (replace -1) (("1" (assert) nil)))
           ("2" (replace 1)
            (("2" (split -)
              (("1" (flatten)
                (("1" (replace -1)
                  (("1" (hide -1)
                    (("1" (replace -1)
                      (("1" (hide -1)
                        (("1" (expand "abs")
                          (("1" (lift-if)
                            (("1" (split -)
                              (("1"
                                (flatten)
                                (("1"
                                  (expand "conflict_vertical?")
                                  (("1"
                                    (skosimp*)
                                    (("1"
                                      (neg-formula -2)
                                      (("1"
                                        (replace -1)
                                        (("1"
                                          (case "vsp < viz")
                                          (("1"
                                            (mult-by -1 "H")
                                            (("1" (assert) nil)))
                                           ("2"
                                            (mult-by 1 "T-t!1")
                                            (("2"
                                              (expand "abs")
                                              (("2"
                                                (lift-if)
                                                (("2"
                                                  (ground)
                                                  nil)))))))))))))))))))
                               ("2"
                                (flatten)
                                (("2"
                                  (replace -1)
                                  (("2"
                                    (case "vsp > viz")
                                    (("1"
                                      (mult-by -1 "H")
                                      (("1" (assert) nil)))
                                     ("2"
                                      (expand "conflict_vertical?")
                                      (("2"
                                        (skosimp*)
                                        (("2"
                                          (mult-by 1 "T-t!1")
                                          (("2"
                                            (expand "abs")
                                            (("2"
                                              (lift-if)
                                              (("2"
                                                (ground)
                                                nil)))))))))))))))))))))))))))))))))
               ("2" (flatten)
                (("2" (replace -1)
                  (("2" (hide -1)
                    (("2" (replace -1)
                      (("2" (hide -1)
                        (("2" (expand "abs")
                          (("2" (lift-if)
                            (("2" (split -)
                              (("1"
                                (flatten)
                                (("1"
                                  (neg-formula -2)
                                  (("1"
                                    (replace -1)
                                    (("1"
                                      (case "vsp > viz")
                                      (("1"
                                        (mult-by -1 "H")
                                        (("1" (assert) nil)))
                                       ("2"
                                        (expand "conflict_vertical?")
                                        (("2"
                                          (skosimp*)
                                          (("2"
                                            (mult-by 1 "t!1-B")
                                            (("2"
                                              (expand "abs")
                                              (("2"
                                                (lift-if)
                                                (("2"
                                                  (ground)
                                                  nil)))))))))))))))))))
                               ("2"
                                (flatten)
                                (("2"
                                  (replace -1)
                                  (("2"
                                    (case "vsp < viz")
                                    (("1"
                                      (mult-by -1 "H")
                                      (("1" (assert) nil)))
                                     ("2"
                                      (expand "conflict_vertical?")
                                      (("2"
                                        (skosimp*)
                                        (("2"
                                          (mult-by 1 "t!1-B")
                                          (("2"
                                            (expand "abs")
                                            (("2"
                                              (lift-if)
                                              (("2"
                                                (ground)
                                                nil))))))))))))))))))))))))))))))))))))))))))))
    nil)
   ((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (mult_neg formula-decl nil extra_tegies nil)
    (neg_neg formula-decl nil extra_tegies nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (both_sides_times1_imp formula-decl nil extra_real_props nil)
    (H formal-const-decl "posreal" vs_bands nil)
    (T formal-const-decl "{AB: posreal | AB > B}" vs_bands nil)
    (B formal-const-decl "nnreal" vs_bands nil)
    (nnreal type-eq-decl nil real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (< const-decl "bool" reals nil)
    (both_sides_times_pos_lt1 formula-decl nil real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Lookahead type-eq-decl nil Lookahead nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (div_mult_neg_le1 formula-decl nil real_props nil)
    (div_mult_neg_le2 formula-decl nil real_props nil)
    (nonpos_real nonempty-type-eq-decl nil real_types nil)
    (negreal nonempty-type-eq-decl nil real_types nil)
    (viz skolem-const-decl "real" vs_bands nil)
    (vsp skolem-const-decl "real" vs_bands nil)
    (both_sides_times_pos_gt1 formula-decl nil real_props 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)
    (abs_nat formula-decl nil abs_lems "reals/")
    (NOT const-decl "[bool -> bool]" booleans nil)
    (times_div2 formula-decl nil real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (newt skolem-const-decl "real" vs_bands nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (conflict_vertical? const-decl "bool" cd_vertical nil)
    (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
     nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (both_sides_times1 formula-decl nil real_props nil)
    (both_sides_times_pos_le1_imp formula-decl nil extra_real_props
     nil)
    (div_mult_pos_le1 formula-decl nil real_props nil)
    (div_mult_pos_le2 formula-decl nil real_props nil)
    (div_cancel2 formula-decl nil real_props nil)
    (newt skolem-const-decl "real" vs_bands nil)
    (newt skolem-const-decl "real" vs_bands nil)
    (newt skolem-const-decl "real" vs_bands nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
 (band_critical_on_H 0
  (band_critical_on_H-3 "stop infinite loop on mult-by -1" 3508591107
   ("" (skeep)
    (("" (case "B = 0")
      (("1" (replace -1)
        (("1" (assert)
          (("1" (hide -1)
            (("1" (expand "sign" -3)
              (("1" (case "T * vsp1 - T * viz + sz >= 0")
                (("1" (assert)
                  (("1" (lift-if)
                    (("1" (ground)
                      (("1" (expand "abs" (-1 -2 -3 -4))
                        (("1" (hide -1)
                          (("1" (hide -1)
                            (("1" (case "sz + tlh*(vsp2-viz) < H")
                              (("1"
                                (hide -4)
                                (("1"
                                  (name "newt" "(H-sz+T*viz)/T")
                                  (("1"
                                    (case "sz + T*(newt-viz) = H")
                                    (("1"
                                      (inst + "newt")
                                      (("1"
                                        (expand "abs" +)
                                        (("1"
                                          (assert)
                                          (("1"
                                            (lemma
                                             "vs_bands_vertical_dir_exclusive")
                                            (("1"
                                              (inst
                                               -
                                               "T"
                                               "1"
                                               "sz"
                                               "viz"
                                               "newt")
                                              (("1"
                                                (expand "abs" -1)
                                                (("1"
                                                  (expand
                                                   "conflict_vertical?")
                                                  (("1"
                                                    (skosimp*)
                                                    (("1"
                                                      (case
                                                       "newt-viz = (H-sz)/T")
                                                      (("1"
                                                        (mult-by
                                                         -1
                                                         "t!1")
                                                        (("1"
                                                          (replace -1)
                                                          (("1"
                                                            (hide -1)
                                                            (("1"
                                                              (case
                                                               "sz + ((H-sz)/T)*t!1)
                                                              (("1"
                                                                (hide
                                                                 -2)
                                                                (("1"
                                                                  (mult-by
                                                                   -1
                                                                   "T")
                                                                  (("1"
                                                                    (mult-by
                                                                     -5
                                                                     "T-t!1")
                                                                    (("1"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (expand
                                                                 "abs"
                                                                 -1)
                                                                (("2"
                                                                  (lift-if)
                                                                  (("2"
                                                                    (ground)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (replace
                                                         -3
                                                         :dir
                                                         rl)
                                                        (("2"
                                                          (mult-by
                                                           1
                                                           "T")
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (case "vsp2 < viz")
                                        (("1"
                                          (case
                                           "sz + T*(vsp2-viz) < H")
                                          (("1"
                                            (typepred "band")
                                            (("1"
                                              (inst
                                               -
                                               "vsp2"
                                               "vsp1"
                                               "newt")
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (replace -4 :dir rl)
                                                  (("1"
                                                    (split 1)
                                                    (("1"
                                                      (cross-mult 1)
                                                      nil
                                                      nil)
                                                     ("2"
                                                      (cross-mult 1)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (mult-by -1 "T-tlh")
                                            (("2" (assert) nil nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (mult-by 1 "tlh")
                                          (("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (replace -1 :dir rl)
                                      (("2"
                                        (mult-by 1 "T")
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (expand "abs")
                                (("2"
                                  (lift-if)
                                  (("2" (ground) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (ground)
                  (("2" (expand "abs" (-1 -2))
                    (("2" (neg-formula -1)
                      (("2" (neg-formula -2)
                        (("2" (case "sz + tlh*(vsp2-viz) > -H")
                          (("1" (assert)
                            (("1" (case "sz >= 0")
                              (("1" (assert) nil nil)
                               ("2"
                                (assert)
                                (("2"
                                  (hide -4)
                                  (("2"
                                    (name "newt" "(-H-sz+T*viz)/T")
                                    (("2"
                                      (case "sz + T*(newt-viz) = -H")
                                      (("1"
                                        (inst + "newt")
                                        (("1"
                                          (expand "abs" +)
                                          (("1"
                                            (assert)
                                            (("1"
                                              (lemma
                                               "vs_bands_vertical_dir_exclusive")
                                              (("1"
                                                (inst
                                                 -
                                                 "T"
                                                 "1"
                                                 "sz"
                                                 "viz"
                                                 "newt")
                                                (("1"
                                                  (expand "abs" -1)
                                                  (("1"
                                                    (expand
                                                     "conflict_vertical?")
                                                    (("1"
                                                      (skosimp*)
                                                      (("1"
                                                        (case
                                                         "newt-viz = (-H-sz)/T")
                                                        (("1"
                                                          (case
                                                           "newt*t!1 - viz*t!1 = (-H - sz) / T*t!1")
                                                          (("1"
                                                            (hide -2)
                                                            (("1"
                                                              (hide -1)
                                                              (("1"
                                                                (case
                                                                 "sz + ((-H-sz)/T)*t!1>-H")
                                                                (("1"
                                                                  (hide
                                                                   -2)
                                                                  (("1"
                                                                    (case
                                                                     " sz*T + ((-H - sz)) * t!1 > -H*T")
                                                                    (("1"
                                                                      (hide
                                                                       -2)
                                                                      (("1"
                                                                        (mult-by
                                                                         -6
                                                                         "T-t!1")
                                                                        (("1"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (hide-all-but
                                                                       (-1
                                                                        1))
                                                                      (("2"
                                                                        (name-replace
                                                                         "div_T"
                                                                         "(-H - sz) / T")
                                                                        (("2"
                                                                          (mult-by
                                                                           -1
                                                                           "T")
                                                                          (("2"
                                                                            (expand
                                                                             "div_T")
                                                                            (("2"
                                                                              (assert)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (hide
                                                                   3
                                                                   4)
                                                                  (("2"
                                                                    (replace
                                                                     -3
                                                                     :dir
                                                                     rl
                                                                     :hide?
                                                                     t)
                                                                    (("2"
                                                                      (grind-reals)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (ground)
                                                            nil
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (hide-all-but
                                                           (-1 1))
                                                          (("2"
                                                            (cross-mult
                                                             1)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (case "vsp2 > viz")
                                          (("1"
                                            (case
                                             "sz + T*(vsp2-viz) > -H")
                                            (("1"
                                              (typepred "band")
                                              (("1"
                                                (inst
                                                 -
                                                 "vsp1"
                                                 "vsp2"
                                                 "newt")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (replace
                                                     -4
                                                     :dir
                                                     rl)
                                                    (("1"
                                                      (split 1)
                                                      (("1"
                                                        (cross-mult 1)
                                                        nil
                                                        nil)
                                                       ("2"
                                                        (cross-mult 1)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (mult-by -1 "T-tlh")
                                              (("2" (assert) nil nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (mult-by 1 "tlh")
                                            (("2" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (replace -1 :dir rl)
                                        (("2"
                                          (mult-by 1 "T")
                                          (("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (expand "abs" -)
                            (("2" (lift-if) (("2" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (assert)
        (("2" (expand "sign" -)
          (("2" (lift-if)
            (("2" (lift-if)
              (("2" (ground)
                (("1" (expand "abs" (-1 -2 -3 -4))
                  (("1" (hide -1)
                    (("1" (hide -1)
                      (("1" (case "sz + tlh*(vsp2-viz) < H")
                        (("1" (hide -4)
                          (("1" (name "newtb" "(H-sz+B*viz)/B")
                            (("1" (label "newtbname" -1)
                              (("1"
                                (case "sz + B*(newtb-viz) = H")
                                (("1"
                                  (name "newtt" "(H-sz+T*viz)/T")
                                  (("1"
                                    (label "newttname" -1)
                                    (("1"
                                      (case "sz + T*(newtt-viz) = H")
                                      (("1"
                                        (case "vsp2 >= viz")
                                        (("1"
                                          (case
                                           "sz + B*(vsp2-viz) < H")
                                          (("1"
                                            (inst + "newtb")
                                            (("1"
                                              (flatten)
                                              (("1"
                                                (hide 3)
                                                (("1"
                                                  (expand "abs" +)
                                                  (("1"
                                                    (assert)
                                                    (("1"
                                                      (lemma
                                                       "vs_bands_vertical_dir_exclusive")
                                                      (("1"
                                                        (inst
                                                         -
                                                         "B"
                                                         "-1"
                                                         "sz"
                                                         "viz"
                                                         "newtb")
                                                        (("1"
                                                          (expand
                                                           "abs"
                                                           -1)
                                                          (("1"
                                                            (expand
                                                             "conflict_vertical?")
                                                            (("1"
                                                              (skosimp*)
                                                              (("1"
                                                                (case
                                                                 "sz + t!1*(newtb - viz) < H")
                                                                (("1"
                                                                  (hide
                                                                   -2)
                                                                  (("1"
                                                                    (case
                                                                     "newtb - viz = (H-sz)/B")
                                                                    (("1"
                                                                      (replace
                                                                       -1)
                                                                      (("1"
                                                                        (hide
                                                                         -1)
                                                                        (("1"
                                                                          (both-sides
                                                                           "-"
                                                                           "sz"
                                                                           -1)
                                                                          (("1"
                                                                            (assert)
                                                                            (("1"
                                                                              (cross-mult
                                                                               -1)
                                                                              (("1"
                                                                                (case
                                                                                 "H < sz")
                                                                                (("1"
                                                                                  (mult-by
                                                                                   -4
                                                                                   "B")
                                                                                  (("1"
--> --------------------

--> maximum size reached

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

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


Bot Zugriff