Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: sigma_fseq.pvs Sprache: Lisp

Original von: PVS^©

(horizontal
(ss_nzv 0
  (ss_nzv-1 nil 3432031102 ("" (judgement-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" reals nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (posreal nonempty-type-eq-decl nil real_types nil)
    (D formal-const-decl "posreal" horizontal nil)
    (Ss_vect2 type-eq-decl nil horizontal nil)
    (comp_zero_x formula-decl nil vectors_2D "vectors/")
    (comp_zero_y formula-decl nil vectors_2D "vectors/")
    (* const-decl "real" vectors_2D "vectors/")
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (/= const-decl "boolean" notequal nil))
   nil))
(ss_sp 0
  (ss_sp-1 nil 3432031102 ("" (judgement-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" reals nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (D formal-const-decl "posreal" horizontal nil)
    (Ss_vect2 type-eq-decl nil horizontal nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (* const-decl "real" vectors_2D "vectors/")
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (sq const-decl "nonneg_real" sq "reals/")
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
(neg_ss 0
  (neg_ss-1 nil 3431439330
   ("" (skeep) (("" (rewrite "sqv_neg") (("" (assert) nil nil)) nil))
    nil)
   ((sqv_neg formula-decl nil vectors_2D "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (> const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (posreal nonempty-type-eq-decl nil real_types nil)
    (D formal-const-decl "posreal" horizontal nil)
    (Ss_vect2 type-eq-decl nil horizontal nil)
    (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/"))
   nil))
(neg_sp 0
  (neg_sp-1 nil 3432031102 ("" (judgement-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (nnreal type-eq-decl nil real_types nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (D formal-const-decl "posreal" horizontal nil)
    (Sp_vect2 type-eq-decl nil horizontal nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (- const-decl "Vector" vectors_2D "vectors/")
    (* const-decl "real" vectors_2D "vectors/")
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (sq const-decl "nonneg_real" sq "reals/")
    (minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
(horizontal_conflict_sum_closed 0
  (horizontal_conflict_sum_closed-4 nil 3467395174
   ("" (skeep)
    (("" (expand "horizontal_conflict?")
      (("" (skosimp*)
        (("" (case "nnt!1 = 0 and nnt!2 = 0")
          (("1" (flatten)
            (("1" (inst + "0")
              (("1" (assert)
                (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil))
              nil))
            nil)
           ("2" (name "tt" "nnt!2/(nnt!1 + nnt!2)")
            (("1" (label "ttname" -1)
              (("1" (case "0<=tt AND tt<=1")
                (("1" (flatten)
                  (("1" (name "newt" "(nnt!1*nnt!2)/(nnt!1 + nnt!2)")
                    (("1" (label "newtname" -1)
                      (("1"
                        (case "tt*nnt!1 = newt AND (1-tt)*nnt!2 = newt")
                        (("1" (flatten)
                          (("1" (label "newttt" -1)
                            (("1" (label "newtomtt" -2)
                              (("1"
                                (inst + "newt")
                                (("1"
                                  (name "VV" "s + nnt!1 * v")
                                  (("1"
                                    (label "vvname" -1)
                                    (("1"
                                      (name "WW" "s + nnt!2 * w")
                                      (("1"
                                        (label "wwname" -1)
                                        (("1"
                                          (name "VVt" "s+nnt!1*v")
                                          (("1"
                                            (label "vvtname" -1)
                                            (("1"
                                              (name "WWt" "s+nnt!2*w")
                                              (("1"
                                                (label "wwtname" -1)
                                                (("1"
                                                  (replace "wwname")
                                                  (("1"
                                                    (replace "vvname")
                                                    (("1"
                                                      (lemma
                                                       "horiz_dist_convex_scaf")
                                                      (("1"
                                                        (inst
                                                         -
                                                         "VVt"
                                                         "WWt-VVt")
                                                        (("1"
                                                          (case
                                                           "s + newt * (v + w) = tt*VV+(1-tt)*WW")
                                                          (("1"
                                                            (label
                                                             "vectfin"
                                                             -1)
                                                            (("1"
                                                              (replace
                                                               "vectfin")
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (lemma
                                                                   "convex_wtd_av_lt")
                                                                  (("1"
                                                                    (inst
                                                                     -
                                                                     "0"
                                                                     "LAMBDA (ttt: real): horiz_dist_scaf(VVt)(ttt, WWt - VVt)"
                                                                     "0"
                                                                     "1")
                                                                    (("1"
                                                                      (assert)
                                                                      (("1"
                                                                        (expand
                                                                         "horiz_dist_scaf"
                                                                         -1
                                                                         1)
                                                                        (("1"
                                                                          (expand
                                                                           "horiz_dist_scaf"
                                                                           -1
                                                                           1)
                                                                          (("1"
                                                                            (assert)
                                                                            (("1"
                                                                              (case
                                                                               "VVt = VV AND VVt+(WWt-VVt) = WW")
                                                                              (("1"
                                                                                (flatten)
                                                                                (("1"
                                                                                  (assert)
                                                                                  (("1"
                                                                                    (inst
                                                                                     -
                                                                                     "tt")
                                                                                    (("1"
                                                                                      (assert)
                                                                                      (("1"
                                                                                        (expand
                                                                                         "horiz_dist_scaf")
                                                                                        (("1"
                                                                                          (case-replace
                                                                                           "VVt + (1 - tt) * (WWt - VVt) = tt * VV + (1 - tt) * WW")
                                                                                          (("1"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil)
                                                                                           ("2"
                                                                                            (hide-all-but
                                                                                             (-1
                                                                                              -2
                                                                                              1))
                                                                                            (("2"
                                                                                              (grind)
                                                                                              nil
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (hide-all-but
                                                                                 ("vvtname"
                                                                                  "vvname"
                                                                                  "wwtname"
                                                                                  "wwname"
                                                                                  1))
                                                                                (("2"
                                                                                  (replace
                                                                                   "wwtname"
                                                                                   +
                                                                                   rl)
                                                                                  (("2"
                                                                                    (replace
                                                                                     "vvtname"
                                                                                     +
                                                                                     rl)
                                                                                    (("2"
                                                                                      (replace
                                                                                       "vvname"
                                                                                       +
                                                                                       rl)
                                                                                      (("2"
                                                                                        (replace
                                                                                         "wwname"
                                                                                         +
                                                                                         rl)
                                                                                        (("2"
                                                                                          (hide-all-but
                                                                                           1)
                                                                                          (("2"
                                                                                            (grind)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (replace
                                                             "vvname"
                                                             +
                                                             rl)
                                                            (("2"
                                                              (replace
                                                               "wwname"
                                                               +
                                                               rl)
                                                              (("2"
                                                                (assert)
                                                                (("2"
                                                                  (hide
                                                                   (2
                                                                    3
                                                                    4
                                                                    5))
                                                                  (("2"
                                                                    (hide-all-but
                                                                     ("newttt"
                                                                      "newtomtt"
                                                                      1))
                                                                    (("2"
                                                                      (grind)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (lemma
                                   "nnreal_div_posreal_is_nnreal")
                                  (("2"
                                    (inst
                                     -
                                     "(nnt!1*nnt!2)"
                                     "nnt!1 + nnt!2")
                                    (("1"
                                      (replace "newtname")
                                      (("1" (propax) nil nil))
                                      nil)
                                     ("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (replace "newtname" + rl)
                          (("2" (replace "ttname" + rl)
                            (("2" (hide-all-but (1 2))
                              (("2"
                                (split 1)
                                (("1" (field) nil nil)
                                 ("2" (field) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (lemma "nnreal_div_posreal_is_nnreal")
                  (("2" (inst - "nnt!2" "nnt!1 + nnt!2")
                    (("1" (replace "ttname")
                      (("1" (assert)
                        (("1" (replace "ttname" + rl)
                          (("1" (cross-mult 1) (("1" (assert) nil nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (assert) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((horizontal_conflict? const-decl "bool" horizontal nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number nonempty-type-decl nil numbers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (add_zero_right formula-decl nil vectors_2D "vectors/")
    (scal_0 formula-decl nil vectors_2D "vectors/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (div_mult_pos_le1 formula-decl nil real_props nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (zero_times1 formula-decl nil real_props nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (both_sides_times1 formula-decl nil real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (div_cancel2 formula-decl nil real_props nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (nnreal_div_posreal_is_nnreal judgement-tcc nil real_types nil)
    (nnt!2 skolem-const-decl "nnreal" horizontal nil)
    (nnt!1 skolem-const-decl "nnreal" horizontal nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (+ const-decl "Vector" vectors_2D "vectors/")
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (* const-decl "Vector" vectors_2D "vectors/")
    (horiz_dist_convex_scaf formula-decl nil horizontal_dist_convexity
     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)
    (D formal-const-decl "posreal" horizontal nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (convex_wtd_av_lt formula-decl nil convex_functions "reals/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (scal_1 formula-decl nil vectors_2D "vectors/")
    (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (- const-decl "Vector" vectors_2D "vectors/")
    (newt skolem-const-decl "real" horizontal nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (<= const-decl "bool" reals nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (numfield nonempty-type-eq-decl nil 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 "[numfield, numfield -> numfield]" number_fields
       nil))
   nil)
  (horizontal_conflict_sum_closed-3 nil 3467395009
   ("" (skeep)
    (("" (expand "horizontal_conflict?")
      (("" (skosimp*)
        (("" (case "nnt!1 = 0 and nnt!2 = 0")
          (("1" (flatten)
            (("1" (inst + "0")
              (("1" (assert)
                (("1" (replace -1) (("1" (assert) nil)))))))))
           ("2" (name "tt" "nnt!2/(nnt!1 + nnt!2)")
            (("1" (label "ttname" -1)
              (("1" (case "0<=tt AND tt<=1")
                (("1" (flatten)
                  (("1" (name "newt" "(nnt!1*nnt!2)/(nnt!1 + nnt!2)")
                    (("1" (label "newtname" -1)
                      (("1"
                        (case "tt*nnt!1 = newt AND (1-tt)*nnt!2 = newt")
                        (("1" (flatten)
                          (("1" (label "newttt" -1)
                            (("1" (label "newtomtt" -2)
                              (("1"
                                (inst + "newt")
                                (("1"
                                  (name
                                   "VV"
                                   "vect2(s) + nnt!1 * vect2(v)")
                                  (("1"
                                    (label "vvname" -1)
                                    (("1"
                                      (name
                                       "WW"
                                       "vect2(s) + nnt!2 * vect2(w)")
                                      (("1"
                                        (label "wwname" -1)
                                        (("1"
                                          (name "VVt" "s+nnt!1*v")
                                          (("1"
                                            (label "vvtname" -1)
                                            (("1"
                                              (name "WWt" "s+nnt!2*w")
                                              (("1"
                                                (label "wwtname" -1)
                                                (("1"
                                                  (replace "wwname")
                                                  (("1"
                                                    (replace "vvname")
                                                    (("1"
                                                      (lemma
                                                       "horiz_dist_convex_scaf")
                                                      (("1"
                                                        (inst
                                                         -
                                                         "VVt"
                                                         "WWt-VVt")
                                                        (("1"
                                                          (case
                                                           "vect2(s) + newt * vect2(v + w) = tt*VV+(1-tt)*WW")
                                                          (("1"
                                                            (label
                                                             "vectfin"
                                                             -1)
                                                            (("1"
                                                              (replace
                                                               "vectfin")
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (lemma
                                                                   "convex_wtd_av_lt")
                                                                  (("1"
                                                                    (inst
                                                                     -
                                                                     "0"
                                                                     "LAMBDA (ttt): horiz_dist_scaf(VVt)(ttt, WWt - VVt)"
                                                                     "0"
                                                                     "1")
                                                                    (("1"
                                                                      (assert)
                                                                      (("1"
                                                                        (expand
                                                                         "horiz_dist_scaf"
                                                                         -1
                                                                         1)
                                                                        (("1"
                                                                          (expand
                                                                           "horiz_dist_scaf"
                                                                           -1
                                                                           1)
                                                                          (("1"
                                                                            (assert)
                                                                            (("1"
                                                                              (case
                                                                               "vect2(VVt) = VV AND vect2(VVt)+vect2(WWt-VVt) = WW")
                                                                              (("1"
                                                                                (flatten)
                                                                                (("1"
                                                                                  (assert)
                                                                                  (("1"
                                                                                    (inst
                                                                                     -
                                                                                     "tt")
                                                                                    (("1"
                                                                                      (assert)
                                                                                      (("1"
                                                                                        (expand
                                                                                         "horiz_dist_scaf")
                                                                                        (("1"
                                                                                          (case-replace
                                                                                           "vect2(VVt) + (1 - tt) * vect2(WWt - VVt) = tt * VV + (1 - tt) * WW")
                                                                                          (("1"
                                                                                            (assert)
                                                                                            nil)
                                                                                           ("2"
                                                                                            (hide-all-but
                                                                                             (-1
                                                                                              -2
                                                                                              1))
                                                                                            (("2"
                                                                                              (grind)
                                                                                              nil)))))))))))))))
                                                                               ("2"
                                                                                (hide-all-but
                                                                                 ("vvtname"
                                                                                  "vvname"
                                                                                  "wwtname"
                                                                                  "wwname"
                                                                                  1))
                                                                                (("2"
                                                                                  (replace
                                                                                   "wwtname"
                                                                                   +
                                                                                   rl)
                                                                                  (("2"
                                                                                    (replace
                                                                                     "vvtname"
                                                                                     +
                                                                                     rl)
                                                                                    (("2"
                                                                                      (replace
                                                                                       "vvname"
                                                                                       +
                                                                                       rl)
                                                                                      (("2"
                                                                                        (replace
                                                                                         "wwname"
                                                                                         +
                                                                                         rl)
                                                                                        (("2"
                                                                                          (rewrite
                                                                                           "vect2_add")
                                                                                          (("2"
                                                                                            (rewrite
                                                                                             "vect2_sub")
                                                                                            (("2"
                                                                                              (rewrite
                                                                                               "vect2_add")
                                                                                              (("2"
                                                                                                (rewrite
                                                                                                 "vect2_add")
                                                                                                (("2"
                                                                                                  (rewrite
                                                                                                   "vect2_scal")
                                                                                                  (("2"
                                                                                                    (rewrite
                                                                                                     "vect2_scal")
                                                                                                    (("2"
                                                                                                      (hide-all-but
                                                                                                       1)
                                                                                                      (("2"
                                                                                                        (grind)
                                                                                                        nil)))))))))))))))))))))))))))))))))))))))))))))
                                                           ("2"
                                                            (replace
                                                             "vvname"
                                                             +
                                                             rl)
                                                            (("2"
                                                              (replace
                                                               "wwname"
                                                               +
                                                               rl)
                                                              (("2"
                                                                (assert)
                                                                (("2"
                                                                  (hide
                                                                   (2
                                                                    3
                                                                    4
                                                                    5))
                                                                  (("2"
                                                                    (hide-all-but
                                                                     ("newttt"
                                                                      "newtomtt"
                                                                      1))
                                                                    (("2"
                                                                      (grind)
                                                                      nil)))))))))))))))))))))))))))))))))))))
                                 ("2"
                                  (lemma
                                   "nnreal_div_posreal_is_nnreal")
                                  (("2"
                                    (inst
                                     -
                                     "(nnt!1*nnt!2)"
                                     "nnt!1 + nnt!2")
                                    (("1"
                                      (replace "newtname")
                                      (("1" (propax) nil)))
                                     ("2" (assert) nil)))))))))))))
                         ("2" (replace "newtname" + rl)
                          (("2" (replace "ttname" + rl)
                            (("2" (hide-all-but (1 2))
                              (("2"
                                (split 1)
                                (("1" (field) nil)
                                 ("2" (field) nil)))))))))))))))))
                 ("2" (lemma "nnreal_div_posreal_is_nnreal")
                  (("2" (inst - "nnt!2" "nnt!1 + nnt!2")
                    (("1" (replace "ttname")
                      (("1" (assert)
                        (("1" (replace "ttname" + rl)
                          (("1" (cross-mult 1)
                            (("1" (assert) nil)))))))))
                     ("2" (assert) nil)))))))))
             ("2" (assert) nil))))))))))
    nil)
   nil nil)
  (horizontal_conflict_sum_closed-2 nil 3467392944
   ("" (skeep)
    (("" (expand "horizontal_conflict?")
      (("" (skosimp*)
        (("" (case "nnt!1 = 0 and nnt!2 = 0")
          (("1" (flatten)
            (("1" (inst + "0")
              (("1" (assert)
                (("1" (replace -1) (("1" (assert) nil)))))))))
           ("2" (name "tt" "nnt!2/(nnt!1 + nnt!2)")
            (("1" (label "ttname" -1)
              (("1" (case "0<=tt AND tt<=1")
                (("1" (flatten)
                  (("1" (name "newt" "(nnt!1*nnt!2)/(nnt!1 + nnt!2)")
                    (("1" (label "newtname" -1)
                      (("1"
                        (case "tt*nnt!1 = newt AND (1-tt)*nnt!2 = newt")
                        (("1" (flatten)
                          (("1" (label "newttt" -1)
                            (("1" (label "newtomtt" -2)
                              (("1"
                                (inst + "newt")
                                (("1"
                                  (name "VV" "s + nnt!1 * v")
                                  (("1"
                                    (label "vvname" -1)
                                    (("1"
                                      (name "WW" "s + nnt!2 * w")
                                      (("1"
                                        (label "wwname" -1)
                                        (("1"
                                          (name "VVt" "s+nnt!1*v")
                                          (("1"
                                            (label "vvtname" -1)
                                            (("1"
                                              (name "WWt" "s+nnt!2*w")
                                              (("1"
                                                (label "wwtname" -1)
                                                (("1"
                                                  (replace "wwname")
                                                  (("1"
                                                    (replace "vvname")
                                                    (("1"
                                                      (lemma
                                                       "horiz_dist_convex_scaf")
                                                      (("1"
                                                        (inst
                                                         -
                                                         "VVt"
                                                         "WWt-VVt")
                                                        (("1"
                                                          (case
                                                           "s + newt * (v + w) = tt*VV+(1-tt)*WW")
                                                          (("1"
                                                            (label
                                                             "vectfin"
                                                             -1)
                                                            (("1"
                                                              (replace
                                                               "vectfin")
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (lemma
                                                                   "convex_wtd_av_lt")
                                                                  (("1"
                                                                    (inst
                                                                     -
                                                                     "0"
                                                                     "LAMBDA (ttt): horiz_dist_scaf(VVt)(ttt, WWt - VVt)"
                                                                     "0"
                                                                     "1")
                                                                    (("1"
                                                                      (assert)
                                                                      (("1"
                                                                        (expand
                                                                         "horiz_dist_scaf"
                                                                         -1
                                                                         1)
                                                                        (("1"
                                                                          (expand
                                                                           "horiz_dist_scaf"
                                                                           -1
                                                                           1)
                                                                          (("1"
                                                                            (assert)
                                                                            (("1"
                                                                              (case
                                                                               "VVt = VV AND VVt+(WWt-VVt) = WW")
                                                                              (("1"
                                                                                (flatten)
                                                                                (("1"
                                                                                  (assert)
                                                                                  (("1"
                                                                                    (inst
                                                                                     -
                                                                                     "tt")
                                                                                    (("1"
                                                                                      (assert)
                                                                                      (("1"
                                                                                        (expand
                                                                                         "horiz_dist_scaf")
                                                                                        (("1"
                                                                                          (case-replace
                                                                                           "VVt + (1 - tt) * (WWt - VVt) = tt * VV + (1 - tt) * WW")
                                                                                          (("1"
                                                                                            (assert)
                                                                                            nil)
                                                                                           ("2"
                                                                                            (hide-all-but
                                                                                             (-1
                                                                                              -2
                                                                                              1))
                                                                                            (("2"
                                                                                              (grind)
                                                                                              nil)))))))))))))))
                                                                               ("2"
                                                                                (hide-all-but
                                                                                 ("vvtname"
                                                                                  "vvname"
                                                                                  "wwtname"
                                                                                  "wwname"
                                                                                  1))
                                                                                (("2"
                                                                                  (replace
                                                                                   "wwtname"
                                                                                   +
                                                                                   rl)
                                                                                  (("2"
                                                                                    (replace
                                                                                     "vvtname"
                                                                                     +
                                                                                     rl)
                                                                                    (("2"
                                                                                      (replace
                                                                                       "vvname"
                                                                                       +
                                                                                       rl)
                                                                                      (("2"
                                                                                        (replace
                                                                                         "wwname"
                                                                                         +
                                                                                         rl)
                                                                                        (("2"
                                                                                          (hide-all-but
                                                                                           1)
                                                                                          (("2"
                                                                                            (grind)
                                                                                            nil)))))))))))))))))))))))))))))))))
                                                           ("2"
                                                            (replace
                                                             "vvname"
                                                             +
                                                             rl)
                                                            (("2"
                                                              (replace
                                                               "wwname"
                                                               +
                                                               rl)
                                                              (("2"
                                                                (assert)
                                                                (("2"
                                                                  (hide
                                                                   (2
                                                                    3
                                                                    4
                                                                    5))
                                                                  (("2"
                                                                    (hide-all-but
                                                                     ("newttt"
                                                                      "newtomtt"
                                                                      1))
                                                                    (("2"
                                                                      (grind)
                                                                      nil)))))))))))))))))))))))))))))))))))))
                                 ("2"
                                  (lemma
                                   "nnreal_div_posreal_is_nnreal")
                                  (("2"
                                    (inst
                                     -
                                     "(nnt!1*nnt!2)"
                                     "nnt!1 + nnt!2")
                                    (("1"
                                      (replace "newtname")
                                      (("1" (propax) nil)))
                                     ("2" (assert) nil)))))))))))))
                         ("2" (replace "newtname" + rl)
                          (("2" (replace "ttname" + rl)
                            (("2" (hide-all-but (1 2))
                              (("2"
                                (split 1)
                                (("1" (field) nil)
                                 ("2" (field) nil)))))))))))))))))
                 ("2" (lemma "nnreal_div_posreal_is_nnreal")
                  (("2" (inst - "nnt!2" "nnt!1 + nnt!2")
                    (("1" (replace "ttname")
                      (("1" (assert)
                        (("1" (replace "ttname" + rl)
                          (("1" (cross-mult 1)
                            (("1" (assert) nil)))))))))
                     ("2" (assert) nil)))))))))
             ("2" (assert) nil))))))))))
    nil)
   nil nil)
  (horizontal_conflict_sum_closed-1 nil 3467392723
   ("" (skeep)
    (("" (expand "horizontal_conflict?")
      (("" (skosimp*)
        (("" (case "nnt!1 = 0 and nnt!2 = 0")
          (("1" (flatten)
            (("1" (inst + "0")
              (("1" (assert)
                (("1" (replace -1) (("1" (assert) nil)))))))))
           ("2" (name "tt" "nnt!2/(nnt!1 + nnt!2)")
            (("1" (label "ttname" -1)
              (("1" (case "0<=tt AND tt<=1")
                (("1" (flatten)
                  (("1" (name "newt" "(nnt!1*nnt!2)/(nnt!1 + nnt!2)")
                    (("1" (label "newtname" -1)
                      (("1"
                        (case "tt*nnt!1 = newt AND (1-tt)*nnt!2 = newt")
                        (("1" (flatten)
                          (("1" (label "newttt" -1)
                            (("1" (label "newtomtt" -2)
                              (("1"
                                (inst + "newt")
                                (("1"
                                  (name
                                   "VV"
                                   "vect2(s) + nnt!1 * vect2(v)")
                                  (("1"
                                    (label "vvname" -1)
                                    (("1"
                                      (name
                                       "WW"
                                       "vect2(s) + nnt!2 * vect2(w)")
                                      (("1"
                                        (label "wwname" -1)
                                        (("1"
                                          (name "VVt" "s+nnt!1*v")
                                          (("1"
                                            (label "vvtname" -1)
                                            (("1"
                                              (name "WWt" "s+nnt!2*w")
                                              (("1"
                                                (label "wwtname" -1)
                                                (("1"
                                                  (replace "wwname")
                                                  (("1"
                                                    (replace "vvname")
                                                    (("1"
                                                      (lemma
                                                       "horiz_dist_convex_scaf")
                                                      (("1"
                                                        (inst
                                                         -
                                                         "VVt"
                                                         "WWt-VVt")
                                                        (("1"
                                                          (case
                                                           "vect2(s) + newt * vect2(v + w) = tt*VV+(1-tt)*WW")
                                                          (("1"
                                                            (label
                                                             "vectfin"
                                                             -1)
                                                            (("1"
                                                              (replace
                                                               "vectfin")
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (lemma
                                                                   "convex_wtd_av_lt")
                                                                  (("1"
                                                                    (inst
                                                                     -
                                                                     "0"
                                                                     "LAMBDA (ttt): horiz_dist_scaf(VVt)(ttt, WWt - VVt)"
                                                                     "0"
                                                                     "1")
                                                                    (("1"
                                                                      (assert)
                                                                      (("1"
                                                                        (expand
                                                                         "horiz_dist_scaf"
                                                                         -1
                                                                         1)
                                                                        (("1"
                                                                          (expand
                                                                           "horiz_dist_scaf"
                                                                           -1
--> --------------------

--> maximum size reached

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

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