(circle_solutionsnil 3466332995"" (skeep)"" (expand "vertical_conflict?" )"" (expand "circle_solution?" )"" (flatten)"" (case-replace "v`z = 0" )"1" (expand "vertical_solution?" -5)"1" (assert ) nil nil )) nil )"2" (assert )"2" (lemma "vertical_solution_Theta_H" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"real" reals nil )"bool" vertical nil )"Sign" sign "reals/" )nil reals nil )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )nil number_fields 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 )nil vertical nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" circle_solutions nil )"bool" vertical nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil vectors_3D_def "vectors/" )nil reals nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"bool" circle_solutions nil ))nil 3466342106"" (skeep)"" (assert )"" (expand "circle_solution?" )"" (flatten)"" (lemma "circle_solution_2D_Delta_ge_0" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"boolean" notequal nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_3D_def "vectors/" )nil vectors_2D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" )"(strict_total_order?[real])" real_props nil )"Sign" sign "reals/" )"(total_order?[real])" nil )nil horizontal 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" circle_solutions nil )"bool" circle_solutions nil ))nil ))nil 3466349252"" (skeep)"" (expand "horizontal_conflict?" )"" (expand "circle_solution?" )"" (flatten)"" (case-replace "vect2(v) = zero" )"1" (expand "circle_solution_2D?" -4)"1" (flatten) (("1" (assert ) nil nil )) nil )) nil )"2" (assert )"2" (lemma "circle_solution_2D_Theta_D" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" horizontal nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"boolean" notequal nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )nil vectors_2D "vectors/" )nil horizontal nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" circle_solutions nil )"bool" horizontal nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"Sign" sign "reals/" )"real" reals nil )"(total_order?[real])" nil )"posreal" sq "reals/" )"(strict_total_order?[real])" real_props nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_3D_def "vectors/" )"[T, T -> boolean]" equalities nil )nil booleans nil )nil vectors_2D_def "vectors/" )nil reals nil )"bool" circle_solutions nil ))nil )nil 3466349211 ("" (postpone) nil nil )nil shostak))nil 3461661297"" (skeep)"" (expand "circle_solution?" )"" (flatten)"" (expand "circle_solution_2D?" )"" (flatten)"" (expand "vertical_solution?" )"" (flatten)"" (expand "circle_criterion?" )"" (rewrite "vect2_add" )"" (rewrite "vect2_scal" )"" (assert )"" (rewrite "vz_distr_add" )"" (rewrite "vz_scal" )"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" circle_solutions nil )"bool" horizontal nil )"real" reals nil )"real" reals nil )"Sign" sign "reals/" )"bool" vertical nil )"bool" circle_criterion nil )nil vect_3D_2D "vectors/" )nil vectors_3D "vectors/" )nil vectors_3D "vectors/" )"(strict_total_order?[real])" real_props nil )"posreal" sq "reals/" )"(total_order?[real])" nil )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil vectors_3D_def "vectors/" )nil reals nil )nil vect_3D_2D "vectors/" ))nil 3461665991"" (skeep)"" (lemma "circle_solution_meets_criterion" )"" (inst?)"" (assert )"" (lemma "circle_criterion_at_independence" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil circle_solutionsnil )"posreal" circle_solutions nil )"posreal" circle_solutions nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil circle_criterionnil )nil vectors_3D_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 booleans nil )nil integers nil )"boolean" notequal nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))quality 100%
¤ Dauer der Verarbeitung: 0.26 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
