Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Porder.thy Sprache: SML

Original von: PVS^©

(circle_optimum_2D
(intersects_circle_fun_scal 0
  (intersects_circle_fun_scal-1 nil 3527949260
   (""
    (case "FORALL (R: posreal, c: Vect2, k: posreal, v: Vect2):
                                    intersects_circle_fun?(v, c, R) IMPLIES
                                     intersects_circle_fun?(k * v, c, R)")
    (("1" (skeep)
      (("1" (ground)
        (("1" (inst?) (("1" (assert) nil nil)) nil)
         ("2" (inst - "R" "c" "1/k" "k*v") (("2" (assert) nil nil))
          nil))
        nil))
      nil)
     ("2" (hide 2)
      (("2" (skeep)
        (("2" (expand "intersects_circle_fun?")
          (("2" (flatten)
            (("2" (case "v = zero")
              (("1" (assert)
                (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)
               ("2" (case "k*v /= zero")
                (("1" (assert)
                  (("1" (flatten)
                    (("1" (lemma "Delta_scal[R]")
                      (("1" (inst - "-c" "k" "v")
                        (("1" (replace -1)
                          (("1" (hide -1)
                            (("1" (mult-by -1 "sq(k)")
                              (("1"
                                (assert)
                                (("1"
                                  (flatten)
                                  (("1"
                                    (assert)
                                    (("1"
                                      (mult-by -2 "k")
                                      (("1" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide-all-but (1 2))
                  (("2" (flatten)
                    (("2" (expand "zero")
                      (("2" (decompose-equality -1)
                        (("2" (decompose-equality +)
                          (("1" (mult-by 1 "k")
                            (("1" (rewrite "vx_scal")
                              (("1" (assert) nil nil)) nil))
                            nil)
                           ("2" (mult-by 1 "k")
                            (("2" (rewrite "vy_scal")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((= const-decl "[T, T -> boolean]" equalities nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (scal_zero formula-decl nil vectors_2D "vectors/")
    (dot_scal_right formula-decl nil vectors_2D "vectors/")
    (sqv_neg formula-decl nil vectors_2D "vectors/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (vx_scal formula-decl nil vectors_2D "vectors/")
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (both_sides_times1 formula-decl nil real_props nil)
    (vy_scal formula-decl nil vectors_2D "vectors/")
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (Delta_scal formula-decl nil horizontal nil)
    (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
     nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (Delta const-decl "real" horizontal nil)
    (* const-decl "real" vectors_2D "vectors/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (- const-decl "Vector" vectors_2D "vectors/")
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types 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)
    (scal_assoc formula-decl nil vectors_2D "vectors/")
    (scal_1 formula-decl nil vectors_2D "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)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (intersects_circle_fun? const-decl "bool" circle_optimum_2D nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (* const-decl "Vector" vectors_2D "vectors/"))
   shostak))
(intersects_circle_fun_def 0
  (intersects_circle_fun_def-1 nil 3527524122
   ("" (skeep)
    (("" (case "v = zero")
      (("1" (replace -1)
        (("1" (expand "intersects_circle_fun?")
          (("1" (expand "circle?")
            (("1" (expand "segment?")
              (("1" (ground)
                (("1" (inst + "zero")
                  (("1" (assert)
                    (("1" (rewrite "sq_eq" 1 :dir rl)
                      (("1" (rewrite "sq_norm") nil nil)) nil))
                    nil))
                  nil)
                 ("2" (skeep -1)
                  (("2" (skeep -2)
                    (("2" (replace -2)
                      (("2" (assert)
                        (("2" (rewrite "sqrt_eq" 1 :dir rl)
                          (("2" (rewrite "sqrt_sqv_norm") nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (ground)
        (("1" (expand "intersects_circle_fun?")
          (("1" (flatten)
            (("1" (inst + "Theta_D[R](-c,v,1)*v")
              (("1" (split +)
                (("1" (expand "circle?")
                  (("1" (lemma "Theta_D_unique[R]")
                    (("1" (inst - "v" "-c" "Theta_D[R](-c, v, 1)")
                      (("1" (assert)
                        (("1" (rewrite "sqrt_eq" :dir rl)
                          (("1" (rewrite "sqrt_sqv_norm")
                            (("1" (hide-all-but (-1 1))
                              (("1"
                                (grind :exclude ("norm" "Theta_D"))
                                nil
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (expand "segment?")
                  (("2" (inst?)
                    (("2" (lemma "Theta_D_ge_0[R]")
                      (("2" (case "NOT sqv(-c) <= sq(R)")
                        (("1" (assert)
                          (("1" (inst?)
                            (("1" (assert)
                              (("1"
                                (split -)
                                (("1"
                                  (lemma "Theta_D_le[R]")
                                  (("1"
                                    (inst?)
                                    (("1" (assert) nil nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (hide-all-but (-2 1))
                                  (("2" (grind) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (assert)
                          (("2" (hide -4)
                            (("2" (hide -2)
                              (("2"
                                (lemma
                                 "horizontal_los_inside_Theta[R]")
                                (("2"
                                  (inst?)
                                  (("2"
                                    (inst - "0")
                                    (("2"
                                      (assert)
                                      (("2"
                                        (lemma "Theta_D_unique[R]")
                                        (("2"
                                          (inst?)
                                          (("2"
                                            (inst - "0")
                                            (("2"
                                              (assert)
                                              (("2"
                                                (lemma "Theta_D_le[R]")
                                                (("2"
                                                  (inst?)
                                                  (("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (skeep -)
          (("2" (expand "segment?")
            (("2" (skeep -2)
              (("2" (replaces -2)
                (("2" (expand "intersects_circle_fun?")
                  (("2" (case "NOT Delta[R](-c, v) >= 0")
                    (("1" (hide 2)
                      (("1" (rewrite "Delta_ge_0")
                        (("1" (inst + "t")
                          (("1" (expand "circle?")
                            (("1" (rewrite "sqrt_eq" 1 :dir rl)
                              (("1"
                                (rewrite "sqrt_sqv_norm")
                                (("1" (grind :exclude "norm") nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (assert)
                      (("2" (flatten)
                        (("2" (case "t = 0")
                          (("1" (replace -1)
                            (("1" (expand "circle?")
                              (("1"
                                (assert)
                                (("1"
                                  (rewrite "sqrt_le" 2 :dir rl)
                                  (("1"
                                    (rewrite "sqrt_sqv_norm")
                                    (("1" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (expand "circle?")
                            (("2"
                              (lemma "horizontal_conflict[norm(c)]")
                              (("1"
                                (inst - "v" "-c")
                                (("1"
                                  (flatten)
                                  (("1"
                                    (hide -2)
                                    (("1"
                                      (split -)
                                      (("1"
                                        (flatten)
                                        (("1"
                                          (split -)
                                          (("1"
                                            (hide-all-but -1)
                                            (("1"
                                              (rewrite
                                               "sqrt_lt"
                                               :dir
                                               rl)
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (rewrite
                                                   "sqrt_sqv_norm")
                                                  (("1"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (hide-all-but (-1 2))
                                            (("2" (grind) nil nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (expand "horizontal_conflict?")
                                        (("2"
                                          (inst + "t")
                                          (("2"
                                            (rewrite
                                             "sqrt_lt"
                                             1
                                             :dir
                                             rl)
                                            (("2"
                                              (assert)
                                              (("2"
                                                (rewrite
                                                 "sqrt_sqv_norm")
                                                (("2"
                                                  (rewrite
                                                   "sqrt_le"
                                                   4
                                                   :dir
                                                   rl)
                                                  (("2"
                                                    (rewrite
                                                     "sqrt_sqv_norm")
                                                    (("2"
                                                      (assert)
                                                      (("2"
                                                        (hide -1)
                                                        (("2"
                                                          (grind
                                                           :exclude
                                                           "norm")
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (lemma "norm_eq_0")
                                (("2"
                                  (inst?)
                                  (("2"
                                    (assert)
                                    (("2"
                                      (replace -1)
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((zero const-decl "Vector" vectors_2D "vectors/")
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (intersects_circle_fun? const-decl "bool" circle_optimum_2D nil)
    (segment? const-decl "bool" circle_optimum_2D nil)
    (sqrt_eq formula-decl nil sqrt "reals/")
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (sq const-decl "nonneg_real" sq "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (sqrt_sq formula-decl nil sqrt "reals/")
    (sqrt_sqv_norm formula-decl nil vectors_2D "vectors/")
    (sq_eq formula-decl nil sq "reals/")
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (nnreal type-eq-decl nil real_types nil)
    (norm const-decl "nnreal" vectors_2D "vectors/")
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (sq_norm formula-decl nil vectors_2D "vectors/")
    (norm_neg formula-decl nil vectors_2D "vectors/")
    (sub_zero_left formula-decl nil vectors_2D "vectors/")
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (scal_zero formula-decl nil vectors_2D "vectors/")
    (circle? const-decl "bool" circle_optimum_2D nil)
    (sqrt_le formula-decl nil sqrt "reals/")
    (horizontal_conflict formula-decl nil horizontal nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sqrt_lt formula-decl nil sqrt "reals/")
    (horizontal_conflict? const-decl "bool" horizontal nil)
    (dot_zero_left formula-decl nil vectors_2D "vectors/")
    (sub_zero_right formula-decl nil vectors_2D "vectors/")
    (neg_zero formula-decl nil vectors_2D "vectors/")
    (norm_zero formula-decl nil vectors_2D "vectors/")
    (norm_eq_0 formula-decl nil vectors_2D "vectors/")
    (Delta_ge_0 formula-decl nil horizontal nil)
    (v skolem-const-decl "Vect2" circle_optimum_2D nil)
    (c skolem-const-decl "Vect2" circle_optimum_2D nil)
    (- const-decl "Vector" vectors_2D "vectors/")
    (Delta const-decl "real" horizontal nil)
    (R skolem-const-decl "posreal" circle_optimum_2D nil)
    (* const-decl "Vector" vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nzint nonempty-type-eq-decl nil integers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (Sign type-eq-decl nil sign "reals/")
    (Theta_D const-decl "real" horizontal nil)
    (Theta_D_ge_0 formula-decl nil horizontal nil)
    (scal_0 formula-decl nil vectors_2D "vectors/")
    (add_zero_right formula-decl nil vectors_2D "vectors/")
    (horizontal_los_inside_Theta formula-decl nil horizontal nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (* const-decl "real" vectors_2D "vectors/")
    (Theta_D_le formula-decl nil horizontal nil)
    (Sp_vect2 type-eq-decl nil horizontal nil)
    (<= const-decl "bool" reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (+ const-decl "Vector" vectors_2D "vectors/")
    (- const-decl "Vector" vectors_2D "vectors/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (sqv_neg formula-decl nil vectors_2D "vectors/")
    (Theta_D_unique formula-decl nil horizontal nil))
   nil))
(intersects_circle_fun_inc 0
  (intersects_circle_fun_inc-1 nil 3527947389
   (""
    (case "FORALL (R: posreal, c: Vect2, u, v: Vect2): sqv(u) = 1 AND sqv(v) = 1 AND
                             intersects_circle_fun?(v, c, R) AND ^(v) * c <= ^(u) * c IMPLIES
                              intersects_circle_fun?(u, c, R)")
    (("1" (skeep)
      (("1" (inst - "R" "c" "^(u)" "^(v)")
        (("1" (assert)
          (("1" (split -)
            (("1" (lemma "intersects_circle_fun_scal")
              (("1" (inst - "R" "c" "1/norm(u)" "u")
                (("1" (assert)
                  (("1" (expand "^") (("1" (propax) nil nil)) nil))
                  nil)
                 ("2" (split +)
                  (("1" (cross-mult 1)
                    (("1" (ground)
                      (("1" (lemma "norm_eq_0")
                        (("1" (inst?) (("1" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil)
                   ("2" (cross-mult 1)
                    (("2" (ground)
                      (("2" (lemma "norm_eq_0")
                        (("2" (inst?) (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("3" (ground)
                  (("3" (lemma "norm_eq_0")
                    (("3" (inst?) (("3" (assert) nil nil)) nil)) nil))
                  nil))
                nil))
              nil)
             ("2" (expand "^")
              (("2" (rewrite "sqv_scal")
                (("2" (rewrite "sq_div")
                  (("1" (rewrite "sq_norm") (("1" (assert) nil nil))
                    nil)
                   ("2" (lemma "norm_eq_0")
                    (("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
                  nil))
                nil))
              nil)
             ("3" (expand "^")
              (("3" (rewrite "sqv_scal")
                (("3" (rewrite "sq_div")
                  (("1" (rewrite "sq_norm") (("1" (assert) nil nil))
                    nil)
                   ("2" (lemma "norm_eq_0")
                    (("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
                  nil))
                nil))
              nil)
             ("4" (lemma "intersects_circle_fun_scal")
              (("4" (inst - "R" "c" "1/norm(v)" "v")
                (("1" (assert)
                  (("1" (expand "^") (("1" (propax) nil nil)) nil))
                  nil)
                 ("2" (split +)
                  (("1" (cross-mult 1)
                    (("1" (ground)
                      (("1" (lemma "norm_eq_0")
                        (("1" (inst?) (("1" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil)
                   ("2" (cross-mult 1)
                    (("2" (ground)
                      (("2" (lemma "norm_eq_0")
                        (("2" (inst?) (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("3" (lemma "norm_eq_0")
                  (("3" (inst?) (("3" (assert) nil nil)) nil)) nil))
                nil))
              nil)
             ("5" (case "FORALL (zpt:Nz_vect2): ^(^(zpt)) = ^(zpt)")
              (("1" (inst-cp - "u")
                (("1" (inst - "v") (("1" (assert) nil nil)) nil)) nil)
               ("2" (hide-all-but 1)
                (("2" (skeep)
                  (("2" (expand "^" + 1)
                    (("2" (typepred "^(zpt)")
                      (("2" (assert)
                        (("2" (replace -1) (("2" (assert) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (hide 2)
      (("2" (skeep)
        (("2" (label "sqvuv" (-1 -2))
          (("2" (case "^(v) = v AND ^(u) = u")
            (("1" (flatten)
              (("1" (replaces -1)
                (("1" (replaces -1)
                  (("1" (hide "sqvuv")
                    (("1" (expand "intersects_circle_fun?")
                      (("1" (case "NOT (v = zero OR u = zero)")
                        (("1" (flatten)
                          (("1" (assert)
                            (("1" (flatten)
                              (("1"
                                (label "uvnz" (1 2))
                                (("1"
                                  (hide "uvnz")
                                  (("1"
                                    (case
                                     "FORALL (bl1,bl2:bool): (bl1 OR bl2) IFF (bl1 OR (bl2 AND not bl1))")
                                    (("1"
                                      (label "final" 1)
                                      (("1"
                                        (hide "final")
                                        (("1"
                                          (rewrite -1)
                                          (("1"
                                            (hide -1)
                                            (("1"
                                              (reveal "final")
                                              (("1"
                                                (split -)
                                                (("1"
                                                  (split +)
                                                  (("1"
                                                    (expand "Delta")
                                                    (("1"
                                                      (reveal "sqvuv")
                                                      (("1"
                                                        (replace -1)
                                                        (("1"
                                                          (hide -1)
                                                          (("1"
                                                            (replace
                                                             -1)
                                                            (("1"
                                                              (hide -1)
                                                              (("1"
                                                                (case
                                                                 "sq(u*perpR(c)) <= sq(v*perpR(c))")
                                                                (("1"
                                                                  (hide
                                                                   -4)
                                                                  (("1"
                                                                    (grind)
                                                                    nil
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (hide
                                                                   (-2
                                                                    2))
                                                                  (("2"
                                                                    (lemma
                                                                     "orthogonal_basis")
                                                                    (("2"
                                                                      (inst
                                                                       -
                                                                       "c"
                                                                       "perpR(c)"
                                                                       _)
                                                                      (("2"
                                                                        (inst-cp
                                                                         -
                                                                         "u")
                                                                        (("2"
                                                                          (inst
                                                                           -
                                                                           "v")
                                                                          (("2"
                                                                            (assert)
                                                                            (("2"
                                                                              (case
                                                                               "c /= zero AND perpR(c) /= zero AND orthogonal?(c, perpR(c))")
                                                                              (("1"
                                                                                (flatten)
                                                                                (("1"
                                                                                  (assert)
                                                                                  (("1"
                                                                                    (lemma
                                                                                     "orthogonal_basis_sqv")
                                                                                    (("1"
                                                                                      (inst?)
                                                                                      (("1"
                                                                                        (assert)
                                                                                        (("1"
                                                                                          (label
                                                                                           "ddvc1"
                                                                                           -3)
                                                                                          (("1"
                                                                                            (hide
                                                                                             "ddvc1")
                                                                                            (("1"
                                                                                              (label
                                                                                               "ddvc2"
                                                                                               -1)
                                                                                              (("1"
                                                                                                (hide
                                                                                                 "ddvc2")
                                                                                                (("1"
                                                                                                  (lemma
                                                                                                   "orthogonal_basis_sqv")
                                                                                                  (("1"
                                                                                                    (inst?)
                                                                                                    (("1"
                                                                                                      (assert)
                                                                                                      (("1"
                                                                                                        (reveal
                                                                                                         "ddvc1")
                                                                                                        (("1"
                                                                                                          (reveal
                                                                                                           "ddvc2")
                                                                                                          (("1"
                                                                                                            (delabel
                                                                                                             "ddvc1")
                                                                                                            (("1"
                                                                                                              (delabel
                                                                                                               "ddvc2")
                                                                                                              (("1"
                                                                                                                (case
                                                                                                                 "sqv(perpR(c)) = sqv(c)")
                                                                                                                (("1"
                                                                                                                  (replace
                                                                                                                   -1)
                                                                                                                  (("1"
                                                                                                                    (hide
                                                                                                                     -1)
                                                                                                                    (("1"
                                                                                                                      (reveal
                                                                                                                       "sqvuv")
                                                                                                                      (("1"
                                                                                                                        (replace
                                                                                                                         -1)
                                                                                                                        (("1"
                                                                                                                          (replace
                                                                                                                           -2)
                                                                                                                          (("1"
                                                                                                                            (case
                                                                                                                             "sq(u*c) >= sq(v*c)")
                                                                                                                            (("1"
                                                                                                                              (rewrite
                                                                                                                               "sq_div")
                                                                                                                              (("1"
                                                                                                                                (rewrite
                                                                                                                                 "sq_div")
                                                                                                                                (("1"
                                                                                                                                  (rewrite
                                                                                                                                   "sq_div")
                                                                                                                                  (("1"
                                                                                                                                    (rewrite
                                                                                                                                     "sq_div")
                                                                                                                                    (("1"
                                                                                                                                      (mult-by
                                                                                                                                       3
                                                                                                                                       "sqv(c)/sq(sqv(c))")
                                                                                                                                      (("1"
                                                                                                                                        (mult-by
                                                                                                                                         -1
                                                                                                                                         "sqv(c)/sq(sqv(c))")
                                                                                                                                        (("1"
                                                                                                                                          (ground)
                                                                                                                                          nil
                                                                                                                                          nil)
                                                                                                                                         ("2"
                                                                                                                                          (real-props)
                                                                                                                                          nil
                                                                                                                                          nil))
                                                                                                                                        nil)
                                                                                                                                       ("2"
                                                                                                                                        (split
                                                                                                                                         +)
                                                                                                                                        (("1"
                                                                                                                                          (cross-mult
                                                                                                                                           1)
                                                                                                                                          nil
                                                                                                                                          nil)
                                                                                                                                         ("2"
                                                                                                                                          (cross-mult
                                                                                                                                           1)
                                                                                                                                          (("2"
                                                                                                                                            (rewrite
                                                                                                                                             "sq_ge")
                                                                                                                                            (("2"
                                                                                                                                              (lemma
                                                                                                                                               "sqv_eq_0")
                                                                                                                                              (("2"
                                                                                                                                                (inst?)
                                                                                                                                                (("2"
                                                                                                                                                  (assert)
                                                                                                                                                  nil
                                                                                                                                                  nil))
                                                                                                                                                nil))
                                                                                                                                              nil))
                                                                                                                                            nil))
                                                                                                                                          nil))
                                                                                                                                        nil))
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil)
                                                                                                                             ("2"
                                                                                                                              (rewrite
                                                                                                                               "sq_ge")
                                                                                                                              (("1"
                                                                                                                                (hide-all-but
                                                                                                                                 (-8
                                                                                                                                  1))
                                                                                                                                (("1"
                                                                                                                                  (grind)
                                                                                                                                  nil
                                                                                                                                  nil))
                                                                                                                                nil)
                                                                                                                               ("2"
                                                                                                                                (hide-all-but
                                                                                                                                 (-8
                                                                                                                                  -9
                                                                                                                                  1))
                                                                                                                                (("2"
                                                                                                                                  (grind)
                                                                                                                                  nil
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil)
                                                                                                                 ("2"
                                                                                                                  (hide-all-but
                                                                                                                   1)
                                                                                                                  (("2"
                                                                                                                    (grind)
                                                                                                                    nil
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (split
                                                                                 +)
                                                                                (("1"
                                                                                  (flatten)
                                                                                  (("1"
                                                                                    (replace
                                                                                     -1)
                                                                                    (("1"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("2"
                                                                                  (flatten)
                                                                                  (("2"
                                                                                    (case
                                                                                     "c = zero")
                                                                                    (("1"
                                                                                      (replace
                                                                                       -1)
                                                                                      (("1"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil)
                                                                                     ("2"
                                                                                      (hide-all-but
                                                                                       (-1
                                                                                        1))
                                                                                      (("2"
                                                                                        (expand
                                                                                         "zero")
                                                                                        (("2"
                                                                                          (expand
                                                                                           "perpR")
                                                                                          (("2"
                                                                                            (flatten)
                                                                                            (("2"
                                                                                              (decompose-equality)
                                                                                              nil
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("3"
                                                                                  (hide-all-but
                                                                                   1)
                                                                                  (("3"
                                                                                    (grind)
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (flatten)
                                                    (("2"
                                                      (hide-all-but
                                                       (-1 -3 1))
                                                      (("2"
                                                        (grind)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (assert)
                                                  (("2"
                                                    (flatten)
                                                    (("2"
                                                      (assert)
                                                      (("2"
                                                        (lemma
                                                         "Delta_ge_0_2[R]")
                                                        (("2"
                                                          (inst?)
                                                          (("2"
                                                            (assert)
                                                            (("2"
                                                              (inst
                                                               +
                                                               "0")
                                                              (("2"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (hide-all-but 1)
                                      (("2"
                                        (skeep)
                                        (("2" (ground) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (hide-all-but -1)
                          (("2" (reveal "sqvuv")
                            (("2" (split -)
                              (("1"
                                (replace -1)
                                (("1" (assert) nil nil))
                                nil)
                               ("2"
                                (replace -1)
                                (("2" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (case "norm(u) = 1 and norm(v) = 1")
              (("1" (expand "^" 1)
                (("1" (flatten)
                  (("1" (replaces -1)
                    (("1" (replaces -1) (("1" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil)
               ("2" (hide-all-but (-1 -2 1))
                (("2" (rewrite "sqrt_eq" -1 :dir rl)
                  (("2" (rewrite "sqrt_eq" -2 :dir rl)
                    (("2" (rewrite "sqrt_sqv_norm")
                      (("2" (rewrite "sqrt_sqv_norm")
                        (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("3" (hide 2)
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.122 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht 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.