Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
vect_3D_2D.prf
Sprache: Unknown
|
(vect_3D_2D
(vect2_add 0
(vect2_add-1 nil 3418464830 ("" (grind) nil nil)
((+ const-decl "Vector" vectors_3D nil)
(vect2 const-decl "Vect2" vect_3D_2D nil)
(+ const-decl "Vector" vectors_2D nil))
shostak))
(vect2_sub 0
(vect2_sub-1 nil 3418464835 ("" (grind) nil nil)
((- const-decl "Vector" vectors_3D nil)
(vect2 const-decl "Vect2" vect_3D_2D nil)
(- const-decl "Vector" vectors_2D nil))
shostak))
(vect2_scal 0
(vect2_scal-1 nil 3418464918 ("" (grind) nil nil)
((* const-decl "Vector" vectors_3D nil)
(vect2 const-decl "Vect2" vect_3D_2D nil)
(* const-decl "Vector" vectors_2D nil))
shostak))
(vect2_neg 0
(vect2_neg-1 nil 3430137150 ("" (grind) nil nil)
((- const-decl "Vector" vectors_3D nil)
(vect2 const-decl "Vect2" vect_3D_2D nil)
(- const-decl "Vector" vectors_2D nil))
shostak))
(vect2_zero 0
(vect2_zero-1 nil 3421059262
("" (expand "vect2")
(("" (apply-extensionality 1 :hide? t) nil nil)) nil)
((Vector type-eq-decl nil vectors_3D nil)
(zero const-decl "Vector" vectors_3D nil)
(Vector type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(comp_zero_y formula-decl nil vectors_3D nil)
(comp_zero_y formula-decl nil vectors_2D nil)
(comp_zero_x formula-decl nil vectors_3D nil)
(comp_zero_x formula-decl nil vectors_2D nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(vect2 const-decl "Vect2" vect_3D_2D nil))
shostak))
(vect2_eq 0
(vect2_eq-1 nil 3462008946 ("" (grind) nil nil)
((vect2 const-decl "Vect2" vect_3D_2D nil)) shostak))
(vect2_eq_ext 0
(vect2_eq_ext-1 nil 3462008952
("" (grind) (("" (decompose-equality 1) nil nil)) nil)
((Vect2 type-eq-decl nil vectors_2D_def nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(vect2 const-decl "Vect2" vect_3D_2D nil))
shostak))
(vect2_ext_id 0
(vect2_ext_id-1 nil 3462008999
("" (skeep)
(("" (name-replace "ww" "vect2(v) WITH [z |-> v`z]" :hide? nil)
(("" (case "ww`x=v`x AND ww`y=v`y AND ww`z=v`z")
(("1" (hide -2)
(("1" (flatten) (("1" (decompose-equality 1) nil nil)) nil))
nil)
("2" (hide 2)
(("2" (replaces -1 :dir rl)
(("2" (expand "vect2") (("2" (propax) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((real nonempty-type-from-decl nil reals 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(Vect3 type-eq-decl nil vectors_3D_def nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(vect2 const-decl "Vect2" vect_3D_2D nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil))
shostak)))
[ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
]
|
|
