|
(trk_only
(trk_only_line_TCC1 0
(trk_only_line_TCC1-2 nil 3444053303
("" (skeep)
(("" (skeep)
(("" (skeep)
(("" (skeep)
(("" (split)
(("1" (expand "trk_only?")
(("1" (rewrite "norms_eq_sqv")
(("1" (lemma "quad2b_eq_0")
(("1" (inst?)
(("1" (inst?)
(("1" (assert)
(("1" (expand "quadratic")
(("1" (rewrite "sqv_add")
(("1" (rewrite "sqv_scal")
(("1"
(assert)
(("1" (inst 1 "irt") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((- const-decl "Vector" vectors_2D "vectors/")
(trk_only? const-decl "bool" definitions nil)
(quad2b_eq_0 formula-decl nil quadratic_2b "reals/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(quadratic const-decl "real" quadratic "reals/")
(sqv_scal formula-decl nil vectors_2D "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)
(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)
(dot_scal_left formula-decl nil vectors_2D "vectors/")
(scal_assoc formula-decl nil vectors_2D "vectors/")
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sqv_add formula-decl nil vectors_2D "vectors/")
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nzreal nonempty-type-eq-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)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(* const-decl "Vector" vectors_2D "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)
(+ const-decl "Vector" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(real nonempty-type-from-decl nil reals nil)
(norms_eq_sqv formula-decl nil vectors_2D "vectors/"))
nil)
(trk_only_line_TCC1-1 nil 3444053253 ("" (subtype-tcc) nil nil) nil
nil))
(trk_only_line_TCC2 0
(trk_only_line_TCC2-1 nil 3444053253 ("" (skosimp*) nil nil) nil
nil))
(same_trk_only_line 0
(same_trk_only_line-2 nil 3444053902
("" (skeep)
(("" (expand "trk_only_line")
(("" (lift-if)
(("" (lift-if)
(("" (lemma "norms_eq_sqv")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((trk_only_line const-decl "{k: real, nvo: Vect2 |
nvo /= zero => trk_only?(vo)(nvo) AND k * vnz = nvo - vi}"
trk_only nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(real_minus_real_is_real application-judgement "real" reals nil)
(norms_eq_sqv formula-decl nil vectors_2D "vectors/"))
nil)
(same_trk_only_line-1 nil 3444053825 ("" (postpone) nil nil) nil
shostak))
(trk_only_line_complete 0
(trk_only_line_complete-1 nil 3444056979
("" (skeep)
(("" (expand "trk_only_line?")
(("" (case-replace "nvo=zero")
(("1" (rewrite "trk_only_zero_right") nil nil)
("2" (assert)
(("2" (lemma "add_move_both")
(("2" (inst -1 "k*vnz" "nvo" "vi")
(("2" (assert)
(("2" (lemma "quad2b_eq_0")
(("2"
(inst -1 "sqv(vnz)" "vnz*vi" "sqv(vi)-sqv(vnzo)"
"k")
(("2" (flatten)
(("2" (hide -2)
(("2" (split -1)
(("1" (flatten)
(("1" (skeep -2)
(("1"
(inst 2 "eps")
(("1"
(expand "trk_only_line")
(("1"
(lift-if)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide (-3 2 3))
(("2" (replaces -1)
(("2"
(expand "trk_only?")
(("2"
(rewrite "norms_eq_sqv")
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((trk_only_line? const-decl "bool" trk_only 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)
(* const-decl "Vector" vectors_2D "vectors/")
(quad2b_eq_0 formula-decl nil quadratic_2b "reals/")
(trk_only_line const-decl "{k: real, nvo: Vect2 |
nvo /= zero => trk_only?(vo)(nvo) AND k * vnz = nvo - vi}"
trk_only nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props 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 "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign "reals/")
(+ const-decl "Vector" vectors_2D "vectors/")
(norms_eq_sqv formula-decl nil vectors_2D "vectors/")
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(quadratic const-decl "real" quadratic "reals/")
(sq const-decl "nonneg_real" sq "reals/")
(trk_only? const-decl "bool" definitions nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "real" vectors_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(real_minus_real_is_real application-judgement "real" reals nil)
(add_move_both formula-decl nil vectors_2D "vectors/")
(trk_only_zero_right formula-decl nil definitions nil)
(/= const-decl "boolean" notequal nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "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))
nil))
(trk_only_line_lt 0
(trk_only_line_lt-1 nil 3461084294
("" (skeep)
(("" (expand "trk_only_line?")
(("" (flatten)
((""
(name-replace "trko1" "trk_only_line(vnz, vo, vi, -1)" :hide?
nil)
((""
(name-replace "trko2" "trk_only_line(vnz, vo, vi, 1)"
:hide? nil)
(("" (decompose-equality -3)
(("" (decompose-equality -5)
(("" (expand "trk_only_line")
(("" (lift-if)
(("" (split -)
(("1" (flatten)
(("1" (assert)
(("1" (replaces (-2 -7) :dir rl)
(("1" (beta)
(("1"
(lemma "root_le")
(("1"
(inst
-1
"sqv(vnz)"
"2*vnz*vi"
"sqv(vi)-sqv(vo)")
(("1"
(lemma "discr2b_discr_ge_0")
(("1"
(inst?)
(("1"
(assert)
(("1"
(rewrite "root2b_root")
(("1"
(rewrite "root2b_root")
(("1"
(lemma "sign_eq_1")
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((trk_only_line? const-decl "bool" trk_only nil)
(minus_odd_is_odd application-judgement "odd_int" integers 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)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(= const-decl "[T, T -> boolean]" equalities nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(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/")
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(trk_only? const-decl "bool" definitions nil)
(* const-decl "Vector" vectors_2D "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(trk_only_line const-decl "{k: real, nvo: Vect2 |
nvo /= zero => trk_only?(vo)(nvo) AND k * vnz = nvo - vi}"
trk_only nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "real" vectors_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(root2b_root formula-decl nil quadratic_2b "reals/")
(sign_eq_1 formula-decl nil sign "reals/")
(sign_neg_clos application-judgement "Sign" sign "reals/")
(dot_scal_left formula-decl nil vectors_2D "vectors/")
(real_times_real_is_real application-judgement "real" reals nil)
(nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
(discr2b_discr_ge_0 formula-decl nil quadratic_2b "reals/")
(root_le formula-decl nil quadratic "reals/"))
shostak))
(trk_only_dot_TCC1 0
(trk_only_dot_TCC1-1 nil 3445622106
("" (skeep)
((""
(name-replace "trko"
"trk_only_line(Vdir(u, vo - vi), vo, vi + W0(u, j),
irt)")
(("" (typepred "trko")
(("" (assert)
(("" (flatten)
(("" (assert)
((""
(case "W0(u,j) + trko`1 * Vdir(u, vo - vi) = trko`2 - vi")
(("1" (replaces -1 :dir rl)
(("1" (rewrite "W_dot") nil nil)) nil)
("2" (replaces -2)
(("2" (hide-all-but 1)
(("2" (grind :exclude "W0") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(= const-decl "[T, T -> boolean]" equalities nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(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/")
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(trk_only? const-decl "bool" definitions nil)
(* const-decl "Vector" vectors_2D "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(trk_only_line const-decl "{k: real, nvo: Vect2 |
nvo /= zero => trk_only?(vo)(nvo) AND k * vnz = nvo - vi}"
trk_only nil)
(Vdir const-decl "Nz_vect2" definitions nil)
(+ const-decl "Vector" vectors_2D "vectors/")
(W0 const-decl "Vect2" definitions nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(W_dot formula-decl nil definitions nil)
(NOT const-decl "[bool -> bool]" booleans nil))
nil))
(trk_only_dot_complete 0
(trk_only_dot_complete-1 nil 3459199769
("" (skeep)
(("" (case "nvo=zero")
(("1" (expand "trk_only?")
(("1" (replaces -1) (("1" (assert) nil nil)) nil)) nil)
("2" (expand "trk_only_dot")
(("2" (lemma "dot_W")
(("2" (inst? -1)
(("2" (inst? -1)
(("2" (assert)
(("2" (skeep -1)
(("2" (lemma "trk_only_line_complete")
(("2" (expand "trk_only_line?")
(("2"
(inst -1 "k" "nvo" "vi+W0(u,j)"
"Vdir(u,vnzo-vi)" "vnzo")
(("2" (assert)
(("2" (split -1)
(("1" (skeep -1)
(("1"
(decompose-equality -1)
(("1" (inst 2 "irt") nil nil))
nil))
nil)
("2" (hide-all-but (-1 1))
(("2"
(grind :exclude ("W0" "Vdir"))
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((zero const-decl "Vector" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "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)
(nz_norm_gt_0 application-judgement "posreal" vectors_2D
"vectors/")
(norm_zero formula-decl nil vectors_2D "vectors/")
(trk_only? const-decl "bool" definitions nil)
(dot_W formula-decl nil definitions nil)
(trk_only_line? const-decl "bool" trk_only nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(trk_only_line const-decl "{k: real, nvo: Vect2 |
nvo /= zero => trk_only?(vo)(nvo) AND k * vnz = nvo - vi}"
trk_only nil)
(* const-decl "Vector" vectors_2D "vectors/")
(IMPLIES const-decl "[bool, bool -> bool]" booleans 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)
(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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(+ const-decl "Vector" vectors_2D "vectors/")
(W0 const-decl "Vect2" definitions nil)
(Vdir const-decl "Nz_vect2" definitions nil)
(trk_only_line_complete formula-decl nil trk_only nil)
(- const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(/= const-decl "boolean" notequal 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)
(trk_only_dot const-decl
"{nvo | nvo /= zero => trk_only?(vo)(nvo) AND u * (nvo - vi) = j}"
trk_only nil))
shostak))
(trk_only_circle_eq_dot 0
(trk_only_circle_eq_dot-1 nil 3445678968
("" (skeep)
(("" (beta)
(("" (flatten)
(("" (expand "trk_only?")
(("" (rewrite "norms_eq_sqv")
(("" (replaces -1 :dir rl) (("" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((real_div_nzreal_is_real application-judgement "real" reals nil)
(trk_only? const-decl "bool" definitions nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(- const-decl "Vector" vectors_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(+ const-decl "Vector" vectors_2D "vectors/")
(* const-decl "real" vectors_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(sq const-decl "nonneg_real" sq "reals/")
(real_plus_real_is_real application-judgement "real" reals nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(real nonempty-type-from-decl nil reals nil)
(norms_eq_sqv formula-decl nil vectors_2D "vectors/"))
nil))
(trk_spc_on_D 0
(trk_spc_on_D-1 nil 3468062449
("" (skeep)
(("" (expand "trk_special_case?")
(("" (flatten)
(("" (expand "trk_only?")
(("" (rewrite "norms_eq_sqv")
(("" (rewrite "scal_sub_right")
(("" (replace -1 :dir rl)
(("" (case-replace "s + (t*nvo - s) = t*nvo")
(("1" (hide -1)
(("1" (rewrite "sqv_scal")
(("1" (rewrite "sq_div") (("1" (assert) nil nil))
nil))
nil))
nil)
("2" (hide-all-but 1) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((trk_special_case? const-decl "bool" trk_only nil)
(trk_only? const-decl "bool" definitions nil)
(scal_sub_right formula-decl nil vectors_2D "vectors/")
(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)
(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)
(= const-decl "[T, T -> boolean]" equalities nil)
(+ const-decl "Vector" vectors_2D "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(sqv_scal formula-decl nil vectors_2D "vectors/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sq_div formula-decl nil sq "reals/")
(D formal-const-decl "posreal" trk_only nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(real nonempty-type-from-decl nil reals nil)
(norms_eq_sqv formula-decl nil vectors_2D "vectors/"))
nil))
(trk_spc_Delta_ge_0 0
(trk_spc_Delta_ge_0-1 nil 3468062095
("" (skeep)
(("" (case-replace "vo-vi=zero")
(("1" (rewrite "Delta_zero_eq_0") (("1" (assert) nil nil)) nil)
("2" (rewrite "Delta_ge_0")
(("2" (lemma "trk_spc_on_D")
(("2" (inst?)
(("2" (inst -1 "vo")
(("2" (rewrite "trk_only_id")
(("2" (assert) (("2" (inst 2 "t") nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(- const-decl "Vector" vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(D formal-const-decl "posreal" trk_only 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)
(bool nonempty-type-eq-decl nil booleans 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)
(Delta_zero_eq_0 formula-decl nil horizontal nil)
(trk_spc_on_D formula-decl nil trk_only nil)
(trk_only_id formula-decl nil definitions nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(Delta_ge_0 formula-decl nil horizontal nil))
shostak))
(trk_spc_dot 0
(trk_spc_dot-1 nil 3459319283
("" (skeep)
(("" (expand "trk_special_case?")
(("" (flatten)
(("" (rewrite "scal_sub_right")
(("" (replaces -1 :dir rl)
(("" (case-replace "s + (t*nvo-s) = t*nvo")
(("1" (hide -1)
(("1" (expand "trk_only?")
(("1" (rewrite "norms_eq_sqv")
(("1" (rewrite "dot_scal_left")
(("1" (rewrite "dot_sub_right")
(("1" (rewrite "sqv" :dir rl)
(("1" (replaces -2 :dir rl)
(("1" (rewrite "dot_comm")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((trk_special_case? const-decl "bool" trk_only nil)
(scal_sub_right formula-decl nil vectors_2D "vectors/")
(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)
(Vector type-eq-decl nil vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(= const-decl "[T, T -> boolean]" equalities nil)
(+ const-decl "Vector" vectors_2D "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(trk_only? const-decl "bool" definitions nil)
(dot_scal_left formula-decl nil vectors_2D "vectors/")
(real_times_real_is_real application-judgement "real" reals nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(dot_comm formula-decl nil vectors_2D "vectors/")
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(dot_sub_right formula-decl nil vectors_2D "vectors/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(norms_eq_sqv formula-decl nil vectors_2D "vectors/")
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(trk_spc_line_solution 0
(trk_spc_line_solution-1 nil 3467982761
("" (skeep)
(("" (case-replace "vo-vi = zero")
(("1" (lemma "line_solution_zero") (("1" (inst?) nil nil)) nil)
("2" (lemma "line_solution_rewrite")
(("2" (inst - "vo-vi" "sp")
(("1" (ground)
(("1" (hide 4)
(("1" (inst + "t")
(("1" (assert)
(("1" (lemma "trk_spc_on_D")
(("1" (inst - "vo" "sp" "t" "vi" "vo")
(("1" (assert)
(("1" (expand "trk_only?")
(("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
((real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(- const-decl "Vector" vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(Sp_vect2 type-eq-decl nil horizontal nil)
(sq const-decl "nonneg_real" sq "reals/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(line_solution_zero formula-decl nil line_solutions 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" trk_only nil)
(/= const-decl "boolean" notequal nil)
(vo skolem-const-decl "Vect2" trk_only nil)
(vi skolem-const-decl "Vect2" trk_only nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(trk_only? const-decl "bool" definitions nil)
(trk_spc_on_D formula-decl nil trk_only nil)
(line_solution_rewrite formula-decl nil line_solutions nil))
shostak))
(trk_spc_horizontal_dir 0
(trk_spc_horizontal_dir-2 nil 3461620238
("" (skeep)
(("" (use "trk_spc_dot")
(("" (assert)
(("" (mult-by -1 "t")
(("" (replaces -1 :dir rl)
(("" (ground)
(("1" (mult-by -1 "t") (("1" (assert) nil nil)) nil)
("2" (mult-by 1 "t") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((trk_spc_dot formula-decl nil trk_only 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)
(bool nonempty-type-eq-decl nil booleans 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)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(real nonempty-type-from-decl nil reals nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(both_sides_times1_imp formula-decl nil extra_real_props nil)
(- const-decl "Vector" vectors_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(+ const-decl "Vector" vectors_2D "vectors/")
(* const-decl "real" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(D formal-const-decl "posreal" trk_only nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(sq const-decl "nonneg_real" sq "reals/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(div_cancel2 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(Sign type-eq-decl nil sign "reals/")
(- const-decl "[numfield -> numfield]" 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)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(both_sides_times_pos_le1_imp formula-decl nil extra_real_props
nil)
(both_sides_times_pos_le1 formula-decl nil real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil)
(trk_spc_horizontal_dir-1 nil 3461615147
(";;; Proof trk_spc_horizontal_entry-1 for formula trk_only.trk_spc_horizontal_entry"
(skeep)
((";;; Proof trk_spc_horizontal_entry-1 for formula trk_only.trk_spc_horizontal_entry"
(split)
(("1" (flatten)
(("1" (neg-formula -1)
(("1" (neg-formula 1)
(("1" (use "trk_spc_dot")
(("1" (assert)
(("1" (replaces -1)
(("1" (cross-mult -1) nil)))))))))))))
("2" (flatten)
(("2" (neg-formula -1)
(("2" (neg-formula 1)
(("2" (use "trk_spc_dot")
(("2" (assert)
(("2" (replaces -1)
(("2" (cross-mult 1) nil))))))))))))))))
";;; developed with shostak decision procedures")
nil nil))
(trk_only_circle_TCC1 0
(trk_only_circle_TCC1-3 nil 3459215951
("" (skeep)
(("" (skeep)
(("" (skeep 2)
(("" (typepred "trk_only_dot(w, vo, vnzi, e, irt)")
(("" (assert) nil nil)) nil))
nil))
nil))
nil)
((trk_only_dot const-decl
"{nvo | nvo /= zero => trk_only?(vo)(nvo) AND u * (nvo - vi) = j}"
trk_only nil)
(- const-decl "Vector" vectors_2D "vectors/")
(* const-decl "real" vectors_2D "vectors/")
(trk_only? const-decl "bool" definitions nil)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(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)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "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)
(nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(real_times_real_is_real application-judgement "real" reals nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil)
(trk_only_circle_TCC1-2 nil 3444245629
("" (skeep)
(("" (expand "trk_special_case?")
(("" (flatten) (("" (replaces -3) (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((scal_zero formula-decl nil vectors_2D "vectors/")) nil)
(trk_only_circle_TCC1-1 nil 3444081733
("" (skosimp*) (("" (assert) nil nil)) nil)
((sign_mult_clos application-judgement "Sign" sign "reals/")
(sq_nz_pos application-judgement "posreal" sq "reals/"))
nil))
(trk_only_circle_TCC2 0
(trk_only_circle_TCC2-3 nil 3459216036
("" (skeep) (("" (skeep) (("" (skeep 2) nil nil)) nil)) nil) nil
nil)
(trk_only_circle_TCC2-2 nil 3459210720
("" (skeep)
((""
(name-replace "trko" "trk_only_dot(vi, vo, zero, sq(d/t), irt)")
(("" (typepred "trko")
(("" (assert)
(("" (flatten)
(("" (assert)
(("" (lemma "trk_special_case_sq_d")
(("" (inst?) (("" (inst?) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(Sign type-eq-decl nil sign "reals/")
(* const-decl "real" vectors_2D "vectors/")
(sq const-decl "nonneg_real" sq "reals/")
(sub_zero_right formula-decl nil vectors_2D "vectors/")
(sq_nz_pos application-judgement "posreal" sq "reals/"))
nil)
(trk_only_circle_TCC2-1 nil 3444081733 ("" (skosimp*) nil nil) nil
nil))
(trk_only_circle_TCC3 0
(trk_only_circle_TCC3-2 nil 3459210567 ("" (skosimp*) nil nil) nil
nil)
(trk_only_circle_TCC3-1 nil 3459210420 ("" (subtype-tcc) nil nil) nil
nil))
(trk_only_circle_solution 0
(trk_only_circle_solution-2 nil 3565296154
("" (skeep)
(("" (expand "trk_only_circle?")
(("" (flatten)
(("" (skeep -1)
(("" (expand "circle_solution_2D?")
(("" (expand "trk_only_circle" :assert? none)
(("" (skoletin* -1 :old? t)
(("" (lift-if)
(("" (split -2)
(("1" (flatten)
(("1" (skoletin -1 :postfix "p" :old? t)
(("1" (lift-if)
(("1" (split -2)
(("1"
(typepred
"trk_only_dot(w, vo, vnzi, e, irt)")
(("1"
(replaces -3 :dir rl)
(("1"
(flatten)
(("1"
(replaces -3 :dir rl)
(("1"
(assert)
(("1"
(flatten)
(("1"
(lemma
"trk_only_circle_eq_dot")
(("1"
(inst?)
(("1"
(inst?)
(("1"
(assert)
(("1"
(assert)
nil
nil))
nil))
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)
((trk_only_circle? const-decl "bool" trk_only nil)
(trk_only_circle const-decl
"{nvo | nvo /= zero => trk_only?(vo)(nvo)}" trk_only nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(trk_only_circle_eq_dot formula-decl nil trk_only nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(trk_only? const-decl "bool" definitions nil)
(* const-decl "real" vectors_2D "vectors/")
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields 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 "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign "reals/")
(+ const-decl "Vector" vectors_2D "vectors/")
(trk_only_dot const-decl
"{nvo | nvo /= zero => trk_only?(vo)(nvo) AND u * (nvo - vi) = j}"
trk_only nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sq const-decl "nonneg_real" sq "reals/")
(D formal-const-decl "posreal" trk_only nil)
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(/= const-decl "boolean" notequal 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)
(bool nonempty-type-eq-decl nil booleans nil)
(* const-decl "Vector" vectors_2D "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)
(number nonempty-type-decl nil numbers nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(real nonempty-type-from-decl nil reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(real_minus_real_is_real application-judgement "real" reals nil)
(circle_solution_2D? const-decl "bool" horizontal nil))
nil)
(trk_only_circle_solution-1 nil 3461613536
("" (skeep)
(("" (expand "trk_only_circle?")
(("" (flatten)
(("" (skeep -1)
(("" (expand "circle_solution_2D?")
(("" (expand "trk_only_circle" :assert? none)
(("" (skoletin* -1)
(("" (lift-if)
(("" (split -2)
(("1" (flatten)
(("1" (skoletin -1 :postfix "p")
(("1" (lift-if)
(("1" (split -2)
(("1"
(typepred
"trk_only_dot(w, vo, vnzi, e, irt)")
(("1"
(replaces -3 :dir rl)
(("1"
(flatten)
(("1"
(replaces -3 :dir rl)
(("1"
(assert)
(("1"
(flatten)
(("1"
(lemma
"trk_only_circle_eq_dot")
(("1"
(inst?)
(("1"
(inst?)
(("1"
(assert)
(("1"
(assert)
nil
nil))
nil))
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)
((sqv const-decl "nnreal" vectors_2D "vectors/")
(sq const-decl "nonneg_real" sq "reals/")
(+ const-decl "Vector" vectors_2D "vectors/")
(Sign type-eq-decl nil sign "reals/")
(* const-decl "real" vectors_2D "vectors/")
(trk_only? const-decl "bool" definitions nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(circle_solution_2D? const-decl "bool" horizontal nil))
nil))
(trk_only_circle_complete 0
(trk_only_circle_complete-2 nil 3565296180
("" (skeep)
(("" (case-replace "nvo=zero")
(("1" (expand "trk_only?") (("1" (assert) nil nil)) nil)
("2" (expand "circle_solution_2D?")
(("2" (flatten)
(("2" (expand "trk_only_circle?")
(("2" (assert)
(("2" (lemma "trk_only_circle_eq_dot")
(("2" (inst -1 "nvo" "s" "t" "vnzi" "vnzo")
(("2" (skoletin* -1 :postfix "p" :old? t)
(("2" (assert)
(("2" (case-replace "wp=zero")
(("1" (expand "trk_special_case?")
(("1" (lemma "sub_eq_zero")
(("1" (inst?)
(("1"
(assert)
(("1"
(replaces -1)
(("1"
(rewrite "scal_sub_right")
(("1"
(case-replace
"t * vnzi + (t * nvo - t * vnzi) = t*nvo")
(("1"
(hide-all-but (-7 -8 2))
(("1"
(expand "trk_only?")
(("1"
(rewrite "norms_eq_sqv")
(("1"
(rewrite "sqv_scal")
(("1"
(rewrite "sq_div")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "trk_only_circle")
(("2"
(replaces (-1 -3 -4) :dir rl :hide? nil)
(("2" (assert)
(("2"
(lemma "trk_only_dot_complete")
(("2"
(inst? -1)
(("2"
(inst? -1)
(("2"
(inst? -1)
(("2"
(inst? -1)
(("2"
(split -1)
(("1"
(skeep -1)
(("1"
(inst 4 "irt")
(("1"
(replaces -1 :dir rl)
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2" (propax) nil nil)
("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(norm_zero formula-decl nil vectors_2D "vectors/")
(nz_norm_gt_0 application-judgement "posreal" vectors_2D
"vectors/")
(trk_only? const-decl "bool" definitions nil)
(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/")
(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)
(/= const-decl "boolean" notequal nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(trk_only_circle const-decl
"{nvo | nvo /= zero => trk_only?(vo)(nvo)}" trk_only nil)
(Sign type-eq-decl nil sign "reals/")
(- const-decl "[numfield -> numfield]" number_fields 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)
(trk_only_dot_complete formula-decl nil trk_only nil)
(trk_special_case? const-decl "bool" trk_only nil)
(sqv_scal formula-decl nil vectors_2D "vectors/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sq_div formula-decl nil sq "reals/")
(norms_eq_sqv formula-decl nil vectors_2D "vectors/")
(real_plus_real_is_real application-judgement "real" reals nil)
(scal_sub_right formula-decl nil vectors_2D "vectors/")
(dot_zero_left formula-decl nil vectors_2D "vectors/")
(sub_eq_zero formula-decl nil vectors_2D "vectors/")
(real_div_nzreal_is_real application-judgement "real" reals nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(+ const-decl "Vector" vectors_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(sq const-decl "nonneg_real" sq "reals/")
(D formal-const-decl "posreal" trk_only nil)
(* const-decl "real" vectors_2D "vectors/")
(numfield nonempty-type-eq-decl nil number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "Vector" vectors_2D "vectors/")
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
(real_minus_real_is_real application-judgement "real" reals nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(trk_only_circle_eq_dot formula-decl nil trk_only nil)
(trk_only_circle? const-decl "bool" trk_only nil)
(circle_solution_2D? const-decl "bool" horizontal nil))
nil)
(trk_only_circle_complete-1 nil 3459202565
("" (skeep)
(("" (case-replace "nvo=zero")
(("1" (expand "trk_only?") (("1" (assert) nil nil)) nil)
("2" (expand "circle_solution_2D?")
(("2" (flatten)
(("2" (expand "trk_only_circle?")
(("2" (assert)
(("2" (lemma "trk_only_circle_eq_dot")
(("2" (inst -1 "nvo" "s" "t" "vnzi" "vnzo")
(("2" (skoletin* -1 :postfix "p")
(("2" (assert)
(("2" (case-replace "wp=zero")
(("1" (expand "trk_special_case?")
(("1" (lemma "sub_eq_zero")
(("1" (inst?)
(("1"
(assert)
(("1"
(replaces -1)
(("1"
(rewrite "scal_sub_right")
(("1"
(case-replace
"t * vnzi + (t * nvo - t * vnzi) = t*nvo")
(("1"
(hide-all-but (-7 -8 2))
(("1"
(expand "trk_only?")
(("1"
(rewrite "norms_eq_sqv")
(("1"
(rewrite "sqv_scal")
(("1"
(rewrite "sq_div")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "trk_only_circle")
(("2"
(replaces (-1 -3 -4) :dir rl :hide? nil)
(("2" (assert)
(("2"
(lemma "trk_only_dot_complete")
(("2"
(inst? -1)
(("2"
(inst? -1)
(("2"
(inst? -1)
(("2"
(inst? -1)
(("2"
(split -1)
(("1"
(skeep -1)
(("1"
(inst 4 "irt")
(("1"
(replaces -1 :dir rl)
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2" (propax) nil nil)
("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(norm_zero formula-decl nil vectors_2D "vectors/")
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.109 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.
|
