|
(gs_circle
(gs_circle_TCC1 0
(gs_circle_TCC1-1 nil 3428841216
("" (skosimp*) (("" (rewrite "vect2_zero") nil nil)) nil)
((vect2_zero formula-decl nil vect_3D_2D "vectors/")) nil))
(gs_circle_TCC2 0
(gs_circle_TCC2-1 nil 3431777250
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_minus_real_is_real application-judgement "real" reals nil))
nil))
(gs_circle_TCC3 0
(gs_circle_TCC3-1 nil 3431777250
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sign_neg_clos application-judgement "Sign" sign "reals/")
(real_minus_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(gs_circle_TCC4 0
(gs_circle_TCC4-1 nil 3431777250
("" (skeep)
(("" (skeep 2)
(("" (skeep 2)
((""
(typepred
"gs_only_circle(vect2(s), vect2(vo), vect2(vi), t, dir, irt)")
(("1" (replaces -4 :dir rl)
(("1" (case-replace "vect2(nvo2 WITH [z |-> vo`z]) = nvo2")
(("1" (assert) nil nil)
("2" (hide-all-but 1)
(("2" (expand "vect2")
(("2" (decompose-equality 1) nil nil)) nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
((Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(gs_only_circle const-decl
"{nvo | nvo /= zero => gs_only?(vnzo)(nvo)}" gs_only nil)
(D formal-const-decl "posreal" gs_circle nil)
(gs_only? const-decl "bool" definitions nil)
(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)
(nzint nonempty-type-eq-decl nil integers 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)
(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)
(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)
(number nonempty-type-decl nil numbers nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(real nonempty-type-from-decl nil reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(nzv2 application-judgement "Nz_vect2" definitions_3D nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(sign_neg_clos application-judgement "Sign" sign "reals/")
(vect2_eq_ext formula-decl nil vect_3D_2D "vectors/"))
nil))
(gs_circle_TCC5 0
(gs_circle_TCC5-2 nil 3431791001
("" (skosimp*) (("" (rewrite "vect2_zero") nil nil)) nil)
((vect2_zero formula-decl nil vect_3D_2D "vectors/")) nil)
(gs_circle_TCC5-1 nil 3431777250
("" (skosimp*) (("" (assert) nil nil)) nil) nil nil))
(gs_vertical_TCC1 0
(gs_vertical_TCC1-1 nil 3471007818
("" (skeep)
(("" (skeep 2)
(("" (skeep 2)
(("" (replaces -1) (("" (hide -1) (("" (grind) nil nil)) nil))
nil))
nil))
nil))
nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(- const-decl "Vector" vectors_3D "vectors/"))
nil))
(gs_vertical_TCC2 0
(gs_vertical_TCC2-1 nil 3471007818
("" (skosimp*) (("" (assert) nil nil)) nil)
((sign_neg_clos application-judgement "Sign" sign "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(gs_vertical_TCC3 0
(gs_vertical_TCC3-1 nil 3471007818
("" (skosimp*) (("" (assert) nil nil)) nil)
((nzv2 application-judgement "Nz_vect2" definitions_3D nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(real_lt_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)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(gs_vertical_TCC4 0
(gs_vertical_TCC4-1 nil 3471007818
("" (skosimp*)
(("" (assert)
((""
(typepred
"gs_only_vertical(vect2(s!1), vect2(vo!1), vect2(vi!1), t!1, dir!1)")
(("" (assert) nil nil)) nil))
nil))
nil)
((sq_nz_pos application-judgement "posreal" sq "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(sign_mult_clos application-judgement "Sign" sign "reals/")
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(nzv2 application-judgement "Nz_vect2" definitions_3D nil)
(sign_neg_clos application-judgement "Sign" sign "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(vect2_eq_ext formula-decl nil vect_3D_2D "vectors/")
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(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)
(>= 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)
(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)
(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/")
(zero const-decl "Vector" vectors_2D "vectors/")
(gs_only? const-decl "bool" definitions nil)
(D formal-const-decl "posreal" gs_circle nil)
(gs_only_vertical const-decl
"{nvo | nvo /= zero => gs_only?(vo)(nvo)}" gs_only nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(Nzv2_vect3 type-eq-decl nil definitions_3D nil))
nil))
(gs_vertical_TCC5 0
(gs_vertical_TCC5-1 nil 3471185623
("" (skosimp*) (("" (assert) nil nil)) nil)
((vect2_zero formula-decl nil vect_3D_2D "vectors/")
(nzv2 application-judgement "Nz_vect2" definitions_3D nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(real_lt_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)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(gs_vertical_TCC6 0
(gs_vertical_TCC6-1 nil 3471185623
("" (skosimp*) (("" (assert) nil nil)) nil)
((sign_neg_clos application-judgement "Sign" sign "reals/")
(vect2_zero formula-decl nil vect_3D_2D "vectors/"))
nil))
(gs_circle_nzvz 0
(gs_circle_nzvz-1 nil 3461923125
("" (skeep)
(("" (expand "gs_circle?")
(("" (flatten)
(("" (skeep -1)
(("" (expand "gs_circle")
(("" (assert)
(("" (replaces -1) (("" (rewrite "vect2_zero") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((gs_circle? const-decl "bool" gs_circle nil)
(vect2_zero formula-decl nil vect_3D_2D "vectors/")
(gs_circle const-decl "{nvo |
vect2(nvo) /= zero =>
gs_only?(vect2(vo))(vect2(nvo)) AND vo`z = nvo`z}" gs_circle
nil))
shostak))
(gs_circle_solution_2D_TCC1 0
(gs_circle_solution_2D_TCC1-1 nil 3461922386
("" (skeep)
(("" (lemma "gs_circle_nzvz")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil)
((gs_circle_nzvz formula-decl nil gs_circle nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(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))
nil))
(gs_circle_solution_2D 0
(gs_circle_solution_2D-1 nil 3461673333
("" (skeep)
(("" (expand "gs_circle?")
(("" (flatten)
(("" (skeep -1)
(("" (expand "gs_circle")
(("" (lift-if)
(("" (split -)
(("1" (flatten)
(("1" (replaces -2)
(("1" (rewrite "vect2_zero") nil nil)) nil))
nil)
("2" (flatten)
(("2"
(name-replace "t"
"Theta_H(s`z, vo`z - vi`z, -dir)")
(("2" (split -)
(("1" (flatten)
(("1"
(name-replace "gsoc"
"gs_only_circle(vect2(s), vect2(vo), vect2(vi),t,dir,irt)"
:hide? nil)
(("1" (rewrite "vect2_sub")
(("1" (lemma "gs_only_circle_solution")
(("1"
(inst
-1
"dir"
"gsoc"
"s"
"t"
"vi"
"vo")
(("1"
(case-replace "vect2(nvo)=gsoc")
(("1"
(assert)
(("1"
(expand "gs_only_circle?")
(("1"
(inst 1 "irt")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(hide-all-but (-4 1))
(("2"
(replaces -1)
(("2"
(expand "vect2")
(("2"
(decompose-equality 1)
nil
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (flatten)
(("2" (replaces -1)
(("2" (rewrite "vect2_zero") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((gs_circle? const-decl "bool" gs_circle nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(gs_only_circle const-decl
"{nvo | nvo /= zero => gs_only?(vnzo)(nvo)}" gs_only nil)
(D formal-const-decl "posreal" gs_circle nil)
(gs_only? const-decl "bool" definitions nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(nzv2 application-judgement "Nz_vect2" definitions_3D nil)
(gs_only_circle_solution formula-decl nil gs_only nil)
(gs_only_circle? const-decl "bool" gs_only nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(t skolem-const-decl "real" gs_circle nil)
(vect2_sub formula-decl nil vect_3D_2D "vectors/")
(Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(Theta_H const-decl "real" vertical nil)
(H formal-const-decl "posreal" gs_circle 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)
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(nzint nonempty-type-eq-decl nil integers 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)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(sign_neg_clos application-judgement "Sign" sign "reals/")
(real_minus_real_is_real application-judgement "real" reals nil)
(vect2_zero formula-decl nil vect_3D_2D "vectors/")
(gs_circle const-decl "{nvo |
vect2(nvo) /= zero =>
gs_only?(vect2(vo))(vect2(nvo)) AND vo`z = nvo`z}" gs_circle
nil))
nil))
(gs_circle_solution 0
(gs_circle_solution-1 nil 3461673654
("" (skeep)
(("" (expand "circle_solution?")
(("" (expand "vertical_solution?")
(("" (lemma "gs_circle_solution_2D")
(("" (inst?)
(("" (assert)
(("" (hide -1)
(("" (expand "gs_circle?")
(("" (flatten)
(("" (skeep -1)
(("" (expand "gs_circle")
(("" (lift-if)
(("" (split -)
(("1" (flatten)
(("1"
(replaces -2)
(("1" (rewrite "vect2_zero") nil nil))
nil))
nil)
("2" (flatten)
(("2"
(split -)
(("1"
(flatten)
(("1"
(assert)
(("1"
(lemma "Theta_H_on_H")
(("1"
(inst? -1)
(("1"
(skoletin -1)
(("1"
(replace -1 :dir rl)
(("1"
(split +)
(("1"
(rewrite
"vz_distr_sub")
(("1"
(assert)
nil
nil))
nil)
("2"
(hide (-2 3))
(("2"
(rewrite
"vz_distr_sub")
(("2"
(replaces -3)
(("2"
(assert)
(("2"
(lemma
"Theta_H_vertical_dir")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(replaces -1)
(("2"
(rewrite "vect2_zero")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((circle_solution? const-decl "bool" circle_solutions nil)
(gs_circle_solution_2D formula-decl nil gs_circle nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(gs_circle? const-decl "bool" gs_circle nil)
(Theta_H_on_H formula-decl nil vertical 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" gs_circle nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Theta_H const-decl "real" vertical nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(vz_distr_sub formula-decl nil vectors_3D "vectors/")
(Vector type-eq-decl nil vectors_3D "vectors/")
(Theta_H_vertical_dir formula-decl nil vertical nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nzv2 application-judgement "Nz_vect2" definitions_3D nil)
(vect2_zero formula-decl nil vect_3D_2D "vectors/")
(gs_circle const-decl "{nvo |
vect2(nvo) /= zero =>
gs_only?(vect2(vo))(vect2(nvo)) AND vo`z = nvo`z}" gs_circle
nil)
(Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(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)
(vertical_solution? const-decl "bool" vertical nil)
(sign_neg_clos application-judgement "Sign" sign "reals/")
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(gs_circle_independence 0
(gs_circle_independence-3 nil 3461673680
("" (skeep)
(("" (lemma "gs_circle_solution")
(("" (inst?)
(("" (assert)
(("" (lemma "circle_solution_independence")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((gs_circle_solution formula-decl nil gs_circle nil)
(sign_neg_clos application-judgement "Sign" sign "reals/")
(real_minus_real_is_real application-judgement "real" reals nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(Theta_H const-decl "real" vertical nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Vector type-eq-decl nil vectors_3D "vectors/")
(- const-decl "Vector" vectors_3D "vectors/")
(H formal-const-decl "posreal" gs_circle nil)
(D formal-const-decl "posreal" gs_circle 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_solution_independence formula-decl nil circle_solutions
nil)
(Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(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))
nil)
(gs_circle_independence-2 nil 3431855533
("" (skeep)
(("" (skoletin 1 :postfix "p")
(("" (flatten)
(("" (case "vo`z = vi`z")
(("1" (expand "gs_circle" :assert? none)
(("1" (assert) nil nil)) nil)
("2" (lemma "gs_circle_meets_criterion")
(("2" (inst?)
(("2" (assert)
(("2" (replaces -2 :dir rl)
(("2"
(name-replace "t"
"Theta_H(scal[3](s), scal[3](vo - vi), -dir)")
(("2" (lemma "circle_criterion_at_independence")
(("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Theta_H const-decl "real" vertical nil)
(sign_neg_clos application-judgement "Sign" sign "reals/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(Sign type-eq-decl nil sign "reals/")
(Vector type-eq-decl nil vectors_3D "vectors/")
(zero const-decl "Vector" vectors_3D "vectors/"))
nil)
(gs_circle_independence-1 nil 3431777258
("" (skeep)
(("" (skoletin 1 :postfix "p")
(("" (flatten)
(("" (expand "gs_circle" :assert? none)
(("" (lift-if)
(("" (split -1)
(("1" (flatten) nil nil)
("2" (flatten)
(("2"
(name-replace "t"
"Theta_H(scal[3](s), scal[3](vo - vi), -eps)")
(("2" (beta)
(("2" (lift-if)
(("2" (split)
(("1" (flatten)
(("1" (split)
(("1" (flatten) nil nil)
("2" (flatten)
(("2"
(split -)
(("1"
(flatten)
(("1"
(replace -2 :dir rl)
(("1"
(lemma "circle_independence")
(("1"
(inst?)
(("1"
(assert)
(("1"
(lemma
"conflict_ever_shift")
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten) nil nil))
nil))
nil))
nil))
nil)
("2" (flatten) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Sign type-eq-decl nil sign "reals/")
(Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(Theta_H const-decl "real" vertical nil)
(sign_neg_clos application-judgement "Sign" sign "reals/"))
nil))
(gs_circle_complete 0
(gs_circle_complete-1 nil 3461924525
("" (skeep)
(("" (expand "circle_solution?")
(("" (flatten)
((""
(name-replace "t" "Theta_H(s`z, vo`z - vi`z, -dir)" :hide?
nil)
(("" (lemma "gs_only_circle_complete")
(("" (rewrite "vect2_sub")
(("" (inst -1 "dir" "nvo" "s" "t" "vi" "vo")
(("1" (assert)
(("1" (expand "gs_circle?")
(("1" (expand "gs_only_circle?")
(("1" (flatten)
(("1" (assert)
(("1" (skeep -1)
(("1" (inst 3 "irt")
(("1"
(expand "gs_circle")
(("1"
(replaces -2)
(("1"
(replaces -1 :dir rl)
(("1"
(replaces -2)
(("1"
(hide-all-but 3)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((circle_solution? const-decl "bool" circle_solutions nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(sign_neg_clos application-judgement "Sign" sign "reals/")
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals 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)
(nzint nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans 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/")
(>= 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" gs_circle nil)
(Theta_H const-decl "real" vertical nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(vect2_sub formula-decl nil vect_3D_2D "vectors/")
(nzv2 application-judgement "Nz_vect2" definitions_3D nil)
(gs_only_circle? const-decl "bool" gs_only nil)
(vect2_ext_id formula-decl nil vect_3D_2D "vectors/")
(gs_circle const-decl "{nvo |
vect2(nvo) /= zero =>
gs_only?(vect2(vo))(vect2(nvo)) AND vo`z = nvo`z}" gs_circle
nil)
(gs_circle? const-decl "bool" gs_circle nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(t skolem-const-decl "real" gs_circle nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(D formal-const-decl "posreal" gs_circle nil)
(gs_only_circle_complete formula-decl nil gs_only nil))
shostak))
(gs_vertical_meets_horizontal_criterion 0
(gs_vertical_meets_horizontal_criterion-1 nil 3471185813
("" (skeep)
(("" (expand "gs_vertical?")
(("" (flatten)
(("" (expand "gs_vertical" :assert? none)
(("" (case-replace "vo`z = vi`z")
(("1" (replaces -2) (("1" (assert) nil nil)) nil)
("2"
(name "DIR"
"sign(IF abs(sp`z) >= H THEN epsv * sign(sp`z) ELSE -1 ENDIF)")
(("2"
(case "IF abs(sp`z) >= H THEN epsv * sign(sp`z) ELSE -1 ENDIF = DIR")
(("1" (hide -2)
(("1" (replace -1)
(("1" (assert)
(("1" (lift-if -2)
(("1" (split -2)
(("1" (flatten)
(("1" (split -3)
(("1"
(flatten)
(("1"
(replaces -2)
(("1" (rewrite "vect2_sub") nil nil))
nil))
nil)
("2"
(flatten)
(("2"
(replaces -1)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (replaces -1)
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-1 1))
(("2" (typepred "epsv") (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((gs_vertical? const-decl "bool" gs_circle nil)
(gs_vertical const-decl "{nvo |
vect2(nvo) /= zero =>
gs_only?(vect2(vo))(vect2(nvo)) AND vo`z = nvo`z}" gs_circle
nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Sp2_vect3 type-eq-decl nil space_3D nil)
(H formal-const-decl "posreal" gs_circle nil)
(D formal-const-decl "posreal" gs_circle nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(sq const-decl "nonneg_real" sq "reals/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(sign const-decl "Sign" sign "reals/")
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(nzint nonempty-type-eq-decl nil integers 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_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)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(sign_mult_clos application-judgement "Sign" sign "reals/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(minus_real_is_real application-judgement "real" reals nil)
(odd_times_odd_is_odd application-judgement "odd_int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(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)
(spv2 application-judgement "Sp_vect2[D]" gs_circle nil)
(vect2_sub formula-decl nil vect_3D_2D "vectors/")
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(gs_only? const-decl "bool" definitions nil)
(gs_only_vertical const-decl
"{nvo | nvo /= zero => gs_only?(vo)(nvo)}" gs_only nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(Theta_H const-decl "real" vertical nil)
(Vector type-eq-decl nil vectors_3D "vectors/")
(- const-decl "Vector" vectors_3D "vectors/")
(nzv2 application-judgement "Nz_vect2" definitions_3D nil)
(vect2_eq_ext formula-decl nil vect_3D_2D "vectors/")
(vect2_zero formula-decl nil vect_3D_2D "vectors/")
(Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(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))
shostak))
(gs_vertical_meets_vertical_criterion 0
(gs_vertical_meets_vertical_criterion-1 nil 3471186475
("" (skeep)
(("" (expand "gs_vertical?")
(("" (flatten)
(("" (expand "gs_vertical" :assert? none)
(("" (case-replace "vo`z = vi`z")
(("1" (replaces -2) (("1" (assert) nil nil)) nil)
("2"
(name "DIR"
"sign(IF abs(s`z) >= H THEN epsv * sign(s`z) ELSE -1 ENDIF)")
(("2"
(case "IF abs(s`z) >= H THEN epsv * sign(s`z) ELSE -1 ENDIF = DIR")
(("1" (hide -2)
(("1" (replace -1)
(("1" (assert)
(("1" (lift-if -2)
(("1" (split -2)
(("1" (flatten)
(("1" (split -3)
(("1"
(flatten)
(("1"
(hide -1)
(("1"
(name-replace
"gso"
"gs_only_vertical(vect2(s), vect2(vo), vect2(vi),
Theta_H(s`z, (vo - vi)`z, -DIR), DIR)"
:hide?
nil)
(("1"
(lemma "gs_only_vertical_on_D")
(("1"
(inst
-1
"DIR"
"gso"
"s"
"Theta_H(s`z, (vo - vi)`z, -DIR)"
"vi"
"vo")
(("1"
(beta)
(("1"
(split -1)
(("1"
(flatten)
(("1"
(lemma
"horizontal_meets_vertical_criterion")
(("1"
(inst
-1
"epsv"
"nvo"
"s"
"vi"
"vo")
(("1"
(replaces -9)
(("1"
(replaces -6)
(("1"
(assert)
(("1"
(rewrite
"vect2_sub")
(("1"
(rewrite
"vect2_sub")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"gs_only_vertical?")
(("2"
(assert)
(("2"
(flatten)
(("2"
(replaces -1)
(("2"
(replaces -2)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(replaces -1)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (replaces -1)
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-1 1))
(("2" (typepred "epsv") (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((gs_vertical? const-decl "bool" gs_circle nil)
(gs_vertical const-decl "{nvo |
vect2(nvo) /= zero =>
gs_only?(vect2(vo))(vect2(nvo)) AND vo`z = nvo`z}" gs_circle
nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(H formal-const-decl "posreal" gs_circle nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(sign const-decl "Sign" sign "reals/")
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(nzint nonempty-type-eq-decl nil integers 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_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)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(sign_mult_clos application-judgement "Sign" sign "reals/")
(minus_real_is_real application-judgement "real" reals nil)
(odd_times_odd_is_odd application-judgement "odd_int" integers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(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)
(gs_only_vertical_on_D formula-decl nil gs_only nil)
(gs_only_vertical? const-decl "bool" gs_only nil)
(vect2_sub formula-decl nil vect_3D_2D "vectors/")
(vect2_eq_ext formula-decl nil vect_3D_2D "vectors/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(horizontal_meets_vertical_criterion formula-decl nil
vertical_criterion nil)
(DIR skolem-const-decl "Sign" gs_circle nil)
(vi skolem-const-decl "Nzv2_vect3" gs_circle nil)
(vo skolem-const-decl "Nzv2_vect3" gs_circle nil)
(s skolem-const-decl "Vect3" gs_circle nil)
(nzv2 application-judgement "Nz_vect2" definitions_3D nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(gs_only? const-decl "bool" definitions nil)
(D formal-const-decl "posreal" gs_circle nil)
(gs_only_vertical const-decl
"{nvo | nvo /= zero => gs_only?(vo)(nvo)}" gs_only nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(Theta_H const-decl "real" vertical nil)
(Vector type-eq-decl nil vectors_3D "vectors/")
(- const-decl "Vector" vectors_3D "vectors/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(vect2_zero formula-decl nil vect_3D_2D "vectors/")
(Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(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))
nil)))
¤ Dauer der Verarbeitung: 0.80 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
