Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: cross_3D.prf Sprache: Lisp

Original von: PVS^©

(cross_3D
(cross_zero_left 0
  (cross_zero_left-1 nil 3411298681 ("" (grind) nil nil)
   ((zero const-decl "Vector" vectors_3D nil)
    (cross const-decl "Vector" cross_3D nil))
   shostak))
(cross_zero_right 0
  (cross_zero_right-1 nil 3411298686 ("" (grind) nil nil)
   ((zero const-decl "Vector" vectors_3D nil)
    (cross const-decl "Vector" cross_3D nil))
   shostak))
(cross_anticomm 0
  (cross_anticomm-1 nil 3411298784 ("" (grind) nil nil)
   ((cross const-decl "Vector" cross_3D nil)
    (- const-decl "Vector" vectors_3D nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
(cross_scal_left 0
  (cross_scal_left-1 nil 3411304371 ("" (grind) nil nil)
   ((* const-decl "Vector" vectors_3D nil)
    (cross const-decl "Vector" cross_3D nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
(cross_scal_right 0
  (cross_scal_right-1 nil 3411304376 ("" (grind) nil nil)
   ((* const-decl "Vector" vectors_3D nil)
    (cross const-decl "Vector" cross_3D nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
(cross_dist 0
  (cross_dist-1 nil 3411304380 ("" (grind) nil nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (cross const-decl "Vector" cross_3D nil)
    (+ const-decl "Vector" vectors_3D nil))
   shostak))
(Lagrange_Identity 0
  (Lagrange_Identity-1 nil 3411304569 ("" (grind) nil nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (* const-decl "real" vectors_3D nil)
    (cross const-decl "Vector" cross_3D nil))
   shostak))
(cross_cross 0
  (cross_cross-1 nil 3411304744 ("" (grind) nil nil)
   ((cross const-decl "Vector" cross_3D nil)
    (* const-decl "real" vectors_3D nil)
    (* const-decl "Vector" vectors_3D nil)
    (- const-decl "Vector" vectors_3D nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
(lin_indep_cross 0
  (lin_indep_cross-3 nil 3411482800
   ("" (skeep)
    (("" (expand "linearly_dependent?")
      (("" (expand "zero")
        (("" (expand "cross")
          (("" (expand "+ ")
            (("" (expand "*")
              (("" (split +)
                (("1" (flatten)
                  (("1" (skosimp*)
                    (("1" (move-terms -2 l 2)
                      (("1" (move-terms -3 l 2)
                        (("1" (move-terms -4 l 2)
                          (("1" (assert)
                            (("1" (split -1)
                              (("1"
                                (flatten)
                                (("1"
                                  (isolate-mult -1 l 2)
                                  (("1"
                                    (isolate-mult -3 l 2)
                                    (("1"
                                      (isolate-mult -5 l 2)
                                      (("1"
                                        (flatten)
                                        (("1"
                                          (replaces -)
                                          (("1" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (flatten)
                                (("2"
                                  (isolate-mult -1 r 3)
                                  (("2"
                                    (isolate-mult -3 r 3)
                                    (("2"
                                      (isolate-mult -5 r 3)
                                      (("2"
                                        (flatten)
                                        (("2"
                                          (assert)
                                          (("2"
                                            (prop)
                                            (("1"
                                              (replaces - :dir rl)
                                              (("1" (field 1) nil nil))
                                              nil)
                                             ("2"
                                              (replace -1 + rl)
                                              (("2"
                                                (replace -3 + rl)
                                                (("2"
                                                  (move-terms 1 l 2)
                                                  (("2"
                                                    (cross-mult 1)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("3"
                                              (replaces - :dir rl)
                                              (("3" (field 1) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (flatten)
                  (("2" (typepred "nzu")
                    (("2" (rewrite "nzv_xyz_neq_0")
                      (("2" (typepred "nzv")
                        (("2" (rewrite "nzv_xyz_neq_0")
                          (("2" (case-replace "nzu`z = 0")
                            (("1" (case-replace "nzu`y = 0")
                              (("1"
                                (case-replace "nzv`z = 0")
                                (("1"
                                  (case-replace "nzv`y = 0")
                                  (("1"
                                    (inst + "nzv`x" "-nzu`x")
                                    (("1" (assert) nil nil))
                                    nil)
                                   ("2" (assert) nil nil))
                                  nil)
                                 ("2" (assert) nil nil))
                                nil)
                               ("2"
                                (case-replace "nzu`x = 0")
                                (("1"
                                  (inst + "nzv`y" "-nzu`y")
                                  (("1" (assert) nil nil))
                                  nil)
                                 ("2"
                                  (case-replace "nzv`z = 0")
                                  (("1"
                                    (case-replace "nzv`x = 0")
                                    (("1"
                                      (assert)
                                      (("1" (mult-cases -8) nil nil))
                                      nil)
                                     ("2"
                                      (inst + "nzv`y" "-nzu`y")
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil)
                                   ("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (case-replace "nzv`z = 0")
                              (("1"
                                (inst + "-nzv`z" "nzu`z")
                                (("1" (assert) nil nil))
                                nil)
                               ("2"
                                (inst + "-nzv`z" "nzu`z")
                                (("2" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((linearly_dependent? const-decl "bool" cross_3D nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (cross const-decl "Vector" cross_3D nil)
    (* const-decl "Vector" vectors_3D nil)
    (nzv_xyz_neq_0 formula-decl nil vectors_3D nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (even_minus_even_is_even application-judgement "even_int" integers
     nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (zero_times3 formula-decl nil real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" 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)
    (Vector type-eq-decl nil vectors_3D nil)
    (/= const-decl "boolean" notequal nil)
    (Nz_vect3 type-eq-decl nil vectors_3D nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (both_sides_div1 formula-decl nil real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (k1!1 skolem-const-decl "real" cross_3D nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (times_div_cancel1 formula-decl nil extra_real_props nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (times_div2 formula-decl nil real_props nil)
    (k2!1 skolem-const-decl "real" cross_3D nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (+ const-decl "Vector" vectors_3D nil)
    (zero const-decl "Vector" vectors_3D nil))
   nil)
  (lin_indep_cross-2 nil 3411482724
   ("" (skeep)
    (("" (expand "linearly_dependent?")
      (("" (expand "zero")
        (("" (expand "cross")
          (("" (expand "+ ")
            (("" (expand "*")
              (("" (split +)
                (("1" (flatten)
                  (("1" (skosimp*)
                    (("1" (move-terms -2 l 2)
                      (("1" (move-terms -3 l 2)
                        (("1" (move-terms -4 l 2)
                          (("1" (assert)
                            (("1" (split -1)
                              (("1"
                                (flatten)
                                (("1"
                                  (isolate-mult -1 l 2)
                                  (("1"
                                    (isolate-mult -3 l 2)
                                    (("1"
                                      (isolate-mult -5 l 2)
                                      (("1"
                                        (flatten)
                                        (("1"
                                          (replaces -)
                                          (("1"
                                            (assert)
                                            nil)))))))))))))
                               ("2"
                                (flatten)
                                (("2"
                                  (isolate-mult -1 r 3)
                                  (("2"
                                    (isolate-mult -3 r 3)
                                    (("2"
                                      (isolate-mult -5 r 3)
                                      (("2"
                                        (flatten)
                                        (("2"
                                          (assert)
                                          (("2"
                                            (prop)
                                            (("1"
                                              (replaces - :dir rl)
                                              (("1" (field 1) nil)))
                                             ("2"
                                              (replace -1 + rl)
                                              (("2"
                                                (replace -3 + rl)
                                                (("2"
                                                  (move-terms 1 l 2)
                                                  (("2"
                                                    (cross-mult 1)
                                                    nil)))))))
                                             ("3"
                                              (replaces - :dir rl)
                                              (("3"
                                                (field 1)
                                                nil)))))))))))))))))))))))))))))))
                 ("2" (flatten)
                  (("2" (typepred "a")
                    (("2" (hide -1)
                      (("2" (typepred "b")
                        (("2" (hide -1)
                          (("2" (case-replace "x`z = 0")
                            (("1" (case-replace "x`y = 0")
                              (("1"
                                (assert)
                                (("1"
                                  (case-replace "y`z = 0")
                                  (("1"
                                    (assert)
                                    (("1"
                                      (case-replace "y`y = 0")
                                      (("1"
                                        (assert)
                                        (("1"
                                          (flatten)
                                          (("1"
                                            (inst + "y`x" "-x`x")
                                            (("1" (assert) nil)))))))
                                       ("2"
                                        (flatten)
                                        (("2"
                                          (assert)
                                          (("2"
                                            (case-replace "y`x = 0")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (mult-cases -6)
                                                nil)))
                                             ("2"
                                              (mult-cases -7)
                                              nil)))))))))))
                                   ("2"
                                    (flatten)
                                    (("2"
                                      (assert)
                                      (("2"
                                        (case-replace "y`x = 0")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (mult-cases -6)
                                            (("1"
                                              (isolate-mult -5 l 2)
                                              (("1" (assert) nil)))))))
                                         ("2"
                                          (isolate-mult -5 l 2)
                                          (("2"
                                            (assert)
                                            nil)))))))))))))
                               ("2"
                                (assert)
                                (("2"
                                  (assert)
                                  (("2"
                                    (case-replace "x`x = 0")
                                    (("1"
                                      (assert)
                                      (("1"
                                        (isolate-mult -6 l 2)
                                        (("1"
                                          (assert)
                                          (("1"
                                            (real-props)
                                            (("1"
                                              (flatten)
                                              (("1"
                                                (inst + "y`y" "-x`y")
                                                (("1"
                                                  (assert)
                                                  nil)))))))))))))
                                     ("2"
                                      (assert)
                                      (("2"
                                        (case-replace "y`z = 0")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (case-replace "y`x = 0")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (flatten)
                                                (("1"
                                                  (mult-cases -4)
                                                  nil)))))
                                             ("2"
                                              (assert)
                                              (("2"
                                                (inst + "y`y" "-x`y")
                                                (("2"
                                                  (ground)
                                                  nil)))))))))
                                         ("2"
                                          (assert)
                                          (("2"
                                            (case-replace "y`x = 0")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (mult-cases -3)
                                                nil)))
                                             ("2"
                                              (assert)
                                              (("2"
                                                (mult-cases -4)
                                                nil)))))))))))))))))))
                             ("2" (case-replace "y`z = 0")
                              (("1"
                                (assert)
                                (("1"
                                  (inst + "-y`z" "x`z")
                                  (("1" (ground) nil)))))
                               ("2"
                                (assert)
                                (("2"
                                  (ground)
                                  (("1"
                                    (inst + "-y`z" "x`z")
                                    (("1" (ground) nil)))
                                   ("2"
                                    (inst + "-y`z" "x`z")
                                    (("2" (ground) nil)))
                                   ("3"
                                    (inst + "-y`z" "x`z")
                                    (("3" (ground) nil)))
                                   ("4"
                                    (inst + "-y`z" "x`z")
                                    (("4"
                                      (ground)
                                      nil))))))))))))))))))))))))))))))))))
    nil)
   nil nil)
  (lin_indep_cross-1 nil 3411482496
   (";;; Proof lin_indep_cross-1 for formula linear_independence_3D.lin_indep_cross"
    (skeep)
    ((";;; Proof lin_indep_cross-1 for formula linear_independence_3D.lin_indep_cross"
      (expand "linearly_dependent?")
      ((";;; Proof lin_indep_cross-1 for formula linear_independence_3D.lin_indep_cross"
        (expand "zero")
        ((";;; Proof lin_indep_cross-1 for formula linear_independence_3D.lin_indep_cross"
          (expand "cross")
          ((";;; Proof lin_indep_cross-1 for formula linear_independence_3D.lin_indep_cross"
            (expand "+ ")
            ((";;; Proof lin_indep_cross-1 for formula linear_independence_3D.lin_indep_cross"
              (expand "*")
              ((";;; Proof lin_indep_cross-1 for formula linear_independence_3D.lin_indep_cross"
                (split +)
                (("1" (flatten)
                  (("1" (skosimp*)
                    (("1" (move-terms -2 l 2)
                      (("1" (move-terms -3 l 2)
                        (("1" (move-terms -4 l 2)
                          (("1" (assert)
                            (("1" (split -1)
                              (("1"
                                (flatten)
                                (("1"
                                  (isolate-mult -1 l 2)
                                  (("1"
                                    (isolate-mult -3 l 2)
                                    (("1"
                                      (isolate-mult -5 l 2)
                                      (("1"
                                        (flatten)
                                        (("1"
                                          (replaces -)
                                          (("1"
                                            (assert)
                                            nil)))))))))))))
                               ("2"
                                (flatten)
                                (("2"
                                  (isolate-mult -1 r 3)
                                  (("2"
                                    (isolate-mult -3 r 3)
                                    (("2"
                                      (isolate-mult -5 r 3)
                                      (("2"
                                        (flatten)
                                        (("2"
                                          (assert)
                                          (("2"
                                            (prop)
                                            (("1"
                                              (replaces - :dir rl)
                                              (("1" (field 1) nil)))
                                             ("2"
                                              (replace -1 + rl)
                                              (("2"
                                                (replace -3 + rl)
                                                (("2"
                                                  (move-terms 1 l 2)
                                                  (("2"
                                                    (cross-mult 1)
                                                    nil)))))))
                                             ("3"
                                              (replaces - :dir rl)
                                              (("3"
                                                (field 1)
                                                nil)))))))))))))))))))))))))))))))
                 ("2" (flatten)
                  (("2" (typepred "a")
                    (("2" (hide -1)
                      (("2" (typepred "b")
                        (("2" (hide -1)
                          (("2" (case-replace "aa`z = 0")
                            (("1" (case-replace "aa`y = 0")
                              (("1"
                                (assert)
                                (("1"
                                  (case-replace "bb`z = 0")
                                  (("1"
                                    (assert)
                                    (("1"
                                      (case-replace "bb`y = 0")
                                      (("1"
                                        (assert)
                                        (("1"
                                          (flatten)
                                          (("1"
                                            (inst + "bb`x" "-aa`x")
                                            (("1" (assert) nil)))))))
                                       ("2"
                                        (flatten)
                                        (("2"
                                          (assert)
                                          (("2"
                                            (case-replace "bb`x = 0")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (mult-cases -6)
                                                nil)))
                                             ("2"
                                              (mult-cases -7)
                                              nil)))))))))))
                                   ("2"
                                    (flatten)
                                    (("2"
                                      (assert)
                                      (("2"
                                        (case-replace "bb`x = 0")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (mult-cases -6)
                                            (("1"
                                              (isolate-mult -5 l 2)
                                              (("1" (assert) nil)))))))
                                         ("2"
                                          (isolate-mult -5 l 2)
                                          (("2"
                                            (assert)
                                            nil)))))))))))))
                               ("2"
                                (assert)
                                (("2"
                                  (assert)
                                  (("2"
                                    (case-replace "aa`x = 0")
                                    (("1"
                                      (assert)
                                      (("1"
                                        (isolate-mult -6 l 2)
                                        (("1"
                                          (assert)
                                          (("1"
                                            (real-props)
                                            (("1"
                                              (flatten)
                                              (("1"
                                                (inst + "bb`y" "-aa`y")
                                                (("1"
                                                  (assert)
                                                  nil)))))))))))))
                                     ("2"
                                      (assert)
                                      (("2"
                                        (case-replace "bb`z = 0")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (case-replace "bb`x = 0")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (flatten)
                                                (("1"
                                                  (mult-cases -4)
                                                  nil)))))
                                             ("2"
                                              (assert)
                                              (("2"
                                                (inst + "bb`y" "-aa`y")
                                                (("2"
                                                  (ground)
                                                  nil)))))))))
                                         ("2"
                                          (assert)
                                          (("2"
                                            (case-replace "bb`x = 0")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (mult-cases -3)
                                                nil)))
                                             ("2"
                                              (assert)
                                              (("2"
                                                (mult-cases -4)
                                                nil)))))))))))))))))))
                             ("2" (case-replace "bb`z = 0")
                              (("1"
                                (assert)
                                (("1"
                                  (inst + "-bb`z" "aa`z")
                                  (("1" (ground) nil)))))
                               ("2"
                                (assert)
                                (("2"
                                  (ground)
                                  (("1"
                                    (inst + "-bb`z" "aa`z")
                                    (("1" (ground) nil)))
                                   ("2"
                                    (inst + "-bb`z" "aa`z")
                                    (("2" (ground) nil)))
                                   ("3"
                                    (inst + "-bb`z" "aa`z")
                                    (("3" (ground) nil)))
                                   ("4"
                                    (inst + "-bb`z" "aa`z")
                                    (("4"
                                      (ground)
                                      nil))))))))))))))))))))))))))))))))))
    ";;; developed with shostak decision procedures")
   nil nil))
(mixed_prod_perm 0
  (mixed_prod_perm-1 nil 3411305088 ("" (grind) nil nil)
   ((cross const-decl "Vector" cross_3D nil)
    (* const-decl "real" vectors_3D nil)
    ([\|\|] const-decl "real" cross_3D nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
(mixed_prod_perm2 0
  (mixed_prod_perm2-1 nil 3411305117 ("" (grind) nil nil)
   ((cross const-decl "Vector" cross_3D nil)
    (* const-decl "real" vectors_3D nil)
    ([\|\|] const-decl "real" cross_3D nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
(mixed_prod_perm_neg 0
  (mixed_prod_perm_neg-1 nil 3411305157 ("" (grind) nil nil)
   ((cross const-decl "Vector" cross_3D nil)
    (* const-decl "real" vectors_3D nil)
    ([\|\|] const-decl "real" cross_3D nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
(mixed_prod_scal1 0
  (mixed_prod_scal1-1 nil 3411305302 ("" (grind) nil nil)
   ((* const-decl "Vector" vectors_3D nil)
    (cross const-decl "Vector" cross_3D nil)
    (* const-decl "real" vectors_3D nil)
    ([\|\|] const-decl "real" cross_3D nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
(mixed_prod_scal2 0
  (mixed_prod_scal2-1 nil 3411305307 ("" (grind) nil nil)
   ((* const-decl "Vector" vectors_3D nil)
    (cross const-decl "Vector" cross_3D nil)
    (* const-decl "real" vectors_3D nil)
    ([\|\|] const-decl "real" cross_3D nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
(mixed_prod_scal3 0
  (mixed_prod_scal3-1 nil 3411305311 ("" (grind) nil nil)
   ((* const-decl "Vector" vectors_3D nil)
    (cross const-decl "Vector" cross_3D nil)
    (* const-decl "real" vectors_3D nil)
    ([\|\|] const-decl "real" cross_3D nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
(mixed_prod_dist 0
  (mixed_prod_dist-1 nil 3411305229 ("" (grind) nil nil)
   ((+ const-decl "Vector" vectors_3D nil)
    (cross const-decl "Vector" cross_3D nil)
    (* const-decl "real" vectors_3D nil)
    ([\|\|] const-decl "real" cross_3D nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
(cross_cross_mixed 0
  (cross_cross_mixed-1 nil 3411305430 ("" (grind) nil nil)
   ((cross const-decl "Vector" cross_3D nil)
    (* const-decl "real" vectors_3D nil)
    ([\|\|] const-decl "real" cross_3D nil)
    (* const-decl "Vector" vectors_3D nil)
    (- const-decl "Vector" vectors_3D nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak)))

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