(criteria_3Dnil 3566321073 ("" (subtype-tcc) nil nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil vectors_3D_def "vectors/" )nil vectors_2D "vectors/" )nil real_types nil )nil vectors_2D_def "vectors/" )nil space_3D nil )"boolean" notequal nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )"[T, T -> boolean]" equalities nil )nil sign "reals/" )"Vect2" vect_3D_2D "vectors/" )"real" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )"real" det_2D "vectors/" )"posreal" criteria_3D nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" horizontal nil )"real" quadratic_2b "reals/" )"real" quadratic_2b "reals/" )"real" horizontal nil )"Vector" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"posreal" criteria_3D nil )"bool" vertical_criterion nil )"SignedCrit" vertical_criterionnil )"nnreal" horizontal_criteria nil )"bool" horizontal_criteria nil )"real" reals nil )"real" reals nil )"real" reals nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"Sign" sign "reals/" )"odd_int" integers nil )"posreal" nil )"real" reals nil )"real" reals nil )"nnreal" nil )"posreal" sq "reals/" ))nil ))nil 3566321145"" (skeep)"" (expand "criterion_3D?" )"" (split)"1" (flatten)"1" (lemma "horizontal_criterion_independence" )"1" (inst -1 "sp" "nv" )"1" (flatten)"1" (hide -2)"1" (split -1)"1" (hide-all-but (-4 1))"1" (lemma "vertical_horizontal_conflict" )"1" (inst?) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (inst? 1) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (hide -2)"2" (lemma "vertical_criterion_independence" )"2" (inst -1 "epsv" "nv" "sp" "v" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" criteria_3D nil )nil nil )nil vectors_2D_def "vectors/" )nil vectors_2D "vectors/" )nil real_types nil )"nnreal" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )nil horizontal nil )nil vectors_3D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" )OR const-decl "[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"posreal" criteria_3D nil )nil space_3D nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"boolean" notequal nil )nil integers nil )"[T, T -> boolean]" equalities nil )nil sign "reals/" )nil space_3D nil )nil nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" criteria_3D nil ))nil )nil 3566321081 ("" (postpone) nil nil )nil shostak))nil 3566321160"" (skeep)"" (expand "criterion_3D?" )"" (ground)"1" (lemma "horizontal_criterion_coordination" )"1" (inst - "epsh" "nvi" "nvo" "sp" "vi" "vo" )"1" (rewrite "vect2_sub" )"1" (rewrite "vect2_sub" )"1" (assert )"1" (rewrite "vect2_neg" )"1" (assert )"1" (split -)"1" (hide-all-but (-6 1))"1" (rewrite "vect2_sub" :dir rl)"1" "vertical_horizontal_conflict" )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-5 1))"2" (rewrite "vect2_sub" :dir rl)"2" "vertical_horizontal_conflict" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 -3)) (("2" (grind) nil nil )) nil )"3" (case "nvi-vo-(vi-vo) = nvi-vi" )"1" (replace -1)"1" (hide -1)"1" " horizontal_criterion_special_coordination" )"1" (inst - "epsh" "nvo" "nvi" "-sp" "vi" )"1" (rewrite "vect2_sub" :dir rl)"1" (rewrite "vect2_sub" :dir rl)"1" (rewrite "vect2_neg" :dir rl)"1" (assert )"1" (hide-all-but (-6 1))"1" (rewrite "vect2_neg" )"1" rewrite "vect2_sub" :dir rl)"1" "vect2(nvi-nvo)=-vect2(nvo-nvi)" )"1" rewrite "horizontal_conflict_symm" )"1" "vertical_horizontal_conflict" )"1" "1" (assert ) nil nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -) (("2" (grind) nil nil )) nil ))nil )"4" (hide-all-but (-1 -3)) (("4" (grind) nil nil )) nil )"5" (lemma "vertical_criterion_coordination" )"5" (inst -1 "epsv" "nvi" "nvo" "sp" "vi" "vo" )"5" (assert ) nil nil )) nil ))nil )"6" (lemma "vertical_criterion_coordination" )"6" (inst -1 "epsv" "nvi" "nvo" "sp" "vi" "vo" )"6" (assert ) nil nil )) nil ))nil )"7" (case "nvo-vi-(vo-vi) = nvo-vo" )"1" (replace -1)"1" (lemma " horizontal_criterion_special_coordination" )"1" (inst - "epsh" "nvi" "nvo" "sp" "vo" )"1" (hide -2)"1" (rewrite "vect2_sub" :dir rl)"1" (rewrite "vect2_sub" :dir rl)"1" (rewrite "vect2_sub" :dir rl)"1" (rewrite "vect2_neg" )"1" (assert )"1" (hide-all-but (-6 1))"1" "vertical_horizontal_conflict" )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -) (("2" (grind) nil nil )) nil ))nil )"8" (lemma "vertical_criterion_coordination" )"8" (inst -1 "epsv" "nvi" "nvo" "sp" "vi" "vo" )"8" (assert ) nil nil )) nil ))nil )"9" (lemma "vertical_criterion_coordination" )"9" (inst -1 "epsv" "nvi" "nvo" "sp" "vi" "vo" )"9" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"bool" criteria_3D nil )nil nil )"Vector" vectors_2D "vectors/" )nil horizontal nil )"real" reals nil )nil vectors_3D "vectors/" )nil nil )"real" reals nil )"real" reals nil )"real" reals nil )"posreal" nil )"real" vectors_2D "vectors/" )"Vector" vectors_3D "vectors/" )"posreal" criteria_3D nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nil )nil vect_3D_2D "vectors/" )"Nz_vect2" definitions_3D nil )nil vectors_2D "vectors/" )nil space_3D nil )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )nil vect_3D_2D "vectors/" )nil definitions_3D nil )"Vector" vectors_2D "vectors/" )nil space_3D nil )"posreal" criteria_3D nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )AND const-decl "[bool, bool -> bool]" booleans nil )nil horizontal nil )"nonneg_real" sq "reals/" )"nnreal" vectors_2D "vectors/" )nil real_types nil )nil vectors_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_3D_def "vectors/" )nil vectors_2D_def "vectors/" )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"boolean" notequal nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"(total_order?[real])" nil )"posreal" sq "reals/" )"(strict_total_order?[real])" real_props nil )"Sign" sign "reals/" )"Nz_vector" vectors_3D "vectors/" ))nil )))quality 100%
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
