Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
circle_solutions.prf
Sprache: Unknown
|
(circle_solutions
(circle_solution_horizontal 0
(circle_solution_horizontal-1 nil 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_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(vertical_conflict? const-decl "bool" vertical nil)
(sign_neg_clos application-judgement "Sign" sign "reals/")
(nzreal nonempty-type-eq-decl nil reals nil)
(Sign type-eq-decl nil sign "reals/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nzint nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(vertical_solution_Theta_H formula-decl nil vertical 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(H formal-const-decl "posreal" circle_solutions nil)
(vertical_solution? const-decl "bool" vertical nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(real nonempty-type-from-decl nil reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(circle_solution? const-decl "bool" circle_solutions nil))
shostak))
(circle_solution_vertical_TCC1 0
(circle_solution_vertical_TCC1-1 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)
((rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(nzint nonempty-type-eq-decl nil integers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign "reals/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sign_neg_clos application-judgement "Sign" sign "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(circle_solution_2D_Delta_ge_0 formula-decl nil horizontal 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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(D formal-const-decl "posreal" circle_solutions nil)
(circle_solution? const-decl "bool" circle_solutions nil))
nil))
(circle_solution_vertical 0
(circle_solution_vertical-2 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)
((horizontal_conflict? const-decl "bool" horizontal nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(nzint nonempty-type-eq-decl nil integers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign "reals/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(circle_solution_2D_Theta_D formula-decl nil horizontal 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(D formal-const-decl "posreal" circle_solutions nil)
(circle_solution_2D? const-decl "bool" horizontal nil)
(scal_zero formula-decl nil vectors_2D "vectors/")
(add_zero_right formula-decl nil vectors_2D "vectors/")
(dot_zero_right formula-decl nil vectors_2D "vectors/")
(sign_neg_clos application-judgement "Sign" sign "reals/")
(real_times_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(real nonempty-type-from-decl nil reals nil)
(circle_solution? const-decl "bool" circle_solutions nil))
nil)
(circle_solution_vertical-1 nil 3466349211 ("" (postpone) nil nil)
nil shostak))
(circle_solution_meets_criterion 0
(circle_solution_meets_criterion-1 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)
((circle_solution? const-decl "bool" circle_solutions nil)
(circle_solution_2D? const-decl "bool" horizontal nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sign_neg_clos application-judgement "Sign" sign "reals/")
(vertical_solution? const-decl "bool" vertical nil)
(circle_criterion? const-decl "bool" circle_criterion nil)
(vect2_scal formula-decl nil vect_3D_2D "vectors/")
(vz_distr_add formula-decl nil vectors_3D "vectors/")
(vz_scal formula-decl nil vectors_3D "vectors/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(* const-decl "Vector" vectors_3D "vectors/")
(Vector type-eq-decl nil vectors_3D "vectors/")
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(real nonempty-type-from-decl nil reals nil)
(vect2_add formula-decl nil vect_3D_2D "vectors/"))
shostak))
(circle_solution_independence 0
(circle_solution_independence-1 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)
((circle_solution_meets_criterion formula-decl nil circle_solutions
nil)
(H formal-const-decl "posreal" circle_solutions nil)
(D formal-const-decl "posreal" circle_solutions nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(circle_criterion_at_independence formula-decl nil circle_criterion
nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(Sign type-eq-decl nil sign "reals/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(nzint nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
shostak)))
[ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
]
|
|
