| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/trig/ (Algebra von RWTH Aachen Version 4.15.1©) Datei vom 28.9.2014 mit Größe 146 kB |
|
SSL det_2D.prf Sprache: Lisp |
|||||||||
|
(det_2D
(det_zero_left 0 (det_zero_left-1 nil 3430576915 ("" (grind) nil nil) ((comp_zero_x formula-decl nil vectors_2D nil) (comp_zero_y formula-decl nil vectors_2D nil) (det const-decl "real" det_2D nil)) shostak)) (det_zero_right 0 (det_zero_right-1 nil 3430576923 ("" (grind) nil nil) ((comp_zero_y formula-decl nil vectors_2D nil) (comp_zero_x formula-decl nil vectors_2D nil) (det const-decl "real" det_2D nil)) shostak)) (det_eq_0 0 (det_eq_0-1 nil 3442660049 ("" (grind) nil nil) ((det const-decl "real" det_2D nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (det_scal_left 0 (det_scal_left-1 nil 3442660093 ("" (grind) nil nil) ((* const-decl "Vector" vectors_2D nil) (det const-decl "real" det_2D nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (det_scal_right 0 (det_scal_right-1 nil 3442660120 ("" (grind) nil nil) ((* const-decl "Vector" vectors_2D nil) (det const-decl "real" det_2D nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (det_add_left 0 (det_add_left-1 nil 3445611398 ("" (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) (det const-decl "real" det_2D nil) (+ const-decl "Vector" vectors_2D nil)) shostak)) (det_add_right 0 (det_add_right-1 nil 3445611403 ("" (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) (det const-decl "real" det_2D nil) (+ const-decl "Vector" vectors_2D nil)) shostak)) (det_sub_left 0 (det_sub_left-1 nil 3445611407 ("" (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) (det const-decl "real" det_2D nil) (- const-decl "Vector" vectors_2D nil)) shostak)) (det_sub_right 0 (det_sub_right-1 nil 3445611412 ("" (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) (det const-decl "real" det_2D nil) (- const-decl "Vector" vectors_2D nil)) shostak)) (det_symm 0 (det_symm-1 nil 3427039921 ("" (grind) nil nil) ((det const-decl "real" det_2D nil) (- const-decl "Vector" vectors_2D nil) (minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (det_asym 0 (det_asym-1 nil 3424620570 ("" (grind) nil nil) ((real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (det const-decl "real" det_2D nil)) shostak)) (det_symm_0 0 (det_symm_0-1 nil 3430576931 ("" (skeep) (("" (rewrite "det_asym") (("" (ground) nil nil)) nil)) nil) ((det_asym formula-decl nil det_2D nil) (real nonempty-type-from-decl nil reals nil) (Vect2 type-eq-decl nil vectors_2D_def nil) (minus_real_is_real application-judgement "real" reals nil)) shostak)) (sq_det 0 (sq_det-1 nil 3427040084 ("" (grind) nil nil) ((det const-decl "real" det_2D nil) (sq const-decl "nonneg_real" sq "reals/") (* const-decl "real" vectors_2D nil) (sqv const-decl "nnreal" vectors_2D 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)) (det_norm 0 (det_norm-1 nil 3424441927 ("" (skeep) (("" (lemma "sq_le") (("" (inst?) (("1" (assert) (("1" (hide 2) (("1" (rewrite "sq_det") (("1" (rewrite "sq_times") (("1" (rewrite "sq_norm") (("1" (rewrite "sq_norm") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((sq_le formula-decl nil sq "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_det formula-decl nil det_2D nil) (real_minus_real_is_real application-judgement "real" reals nil) (sq_norm formula-decl nil vectors_2D nil) (sq_times formula-decl nil sq "reals/") (norm const-decl "nnreal" vectors_2D nil) (nnreal type-eq-decl nil real_types nil) (Vector type-eq-decl nil vectors_2D nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (Vect2 type-eq-decl nil vectors_2D_def nil) (det const-decl "real" det_2D nil) (u skolem-const-decl "Vect2" det_2D nil) (v skolem-const-decl "Vect2" det_2D nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (det_perpR 0 (det_perpR-1 nil 3442581053 ("" (grind) nil nil) ((det const-decl "real" det_2D nil) (perpR const-decl "Vect2" perpendicular_2D nil) (* const-decl "real" vectors_2D nil) (minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (det_perpL 0 (det_perpL-1 nil 3424441540 ("" (grind) nil nil) ((det const-decl "real" det_2D nil) (perpL const-decl "Vect2" perpendicular_2D nil) (* const-decl "real" vectors_2D nil) (minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (dot_perpR 0 (dot_perpR-1 nil 3459876088 ("" (grind) nil nil) ((* const-decl "real" vectors_2D nil) (perpR const-decl "Vect2" perpendicular_2D nil) (det const-decl "real" det_2D nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (dot_perpL 0 (dot_perpL-1 nil 3459876093 ("" (grind) nil nil) ((* const-decl "real" vectors_2D nil) (perpL const-decl "Vect2" perpendicular_2D nil) (det const-decl "real" det_2D nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (perpR_dot 0 (perpR_dot-1 nil 3442581061 ("" (grind) nil nil) ((perpR const-decl "Vect2" perpendicular_2D nil) (* const-decl "real" vectors_2D nil) (det const-decl "real" det_2D nil) (real_minus_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)) shostak)) (perpL_dot 0 (perpL_dot-1 nil 3442581074 ("" (grind) nil nil) ((perpL const-decl "Vect2" perpendicular_2D nil) (* const-decl "real" vectors_2D nil) (det const-decl "real" det_2D nil) (real_minus_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)) shostak)) (det_dot_0 0 (det_dot_0-1 nil 3443825916 ("" (skeep) (("" (lemma "sq_eq") (("" (inst -1 "det(nzu,nzv)" "0") (("1" (assert) (("1" (rewrite "sq_det") (("1" (replaces -3) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((sq_eq formula-decl nil sq "reals/") (sq_0 formula-decl nil sq "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D nil) (sq_det formula-decl nil det_2D nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (Vect2 type-eq-decl nil vectors_2D_def nil) (det const-decl "real" det_2D nil) (Vector type-eq-decl nil vectors_2D nil) (/= const-decl "boolean" notequal nil) (zero const-decl "Vector" vectors_2D nil) (Nz_vect2 type-eq-decl nil vectors_2D nil) (nzu skolem-const-decl "Nz_vect2" det_2D nil) (nzv skolem-const-decl "Nz_vect2" det_2D nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak))) ¤ 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.0.20Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28