|
(trk_line
(trk_line_eps_irt_TCC1 0
(trk_line_eps_irt_TCC1-1 nil 3433242888
("" (skeep)
(("" (typepred "trk_only_line(tangent_line(sp, eps), vo, vi, irt)")
(("" (assert) nil nil)) nil))
nil)
((tangent_line const-decl "Nz_vect2" tangent_line nil)
(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)
(trk_only_line const-decl "{k: real, nvo: Vect2 |
nvo /= zero => trk_only?(vo)(nvo) AND k * vnz = nvo - vi}"
trk_only nil)
(D formal-const-decl "posreal" trk_line 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)
(- const-decl "Vector" vectors_2D "vectors/")
(* const-decl "Vector" 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(trk_line_eps_irt_TCC2 0
(trk_line_eps_irt_TCC2-1 nil 3433242888 ("" (skosimp*) nil nil) nil
nil))
(trk_line_eps_irt_tangent_line 0
(trk_line_eps_irt_tangent_line-3 nil 3445708958
("" (skeep)
(("" (expand "trk_line_eps_irt?")
(("" (flatten)
(("" (expand "trk_line_eps_irt" :assert? none)
(("" (skoletin -1 :postfix "a")
(("" (lift-if)
(("" (split -)
(("1" (flatten)
(("1"
(typepred
"trk_only_line(tangent_line(sp, eps),vo, vi,irt)")
(("1" (replaces (-4 -5) :dir rl)
(("1" (assert)
(("1" (flatten)
(("1" (expand "tangent_line?")
(("1" (inst?) (("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((trk_line_eps_irt? const-decl "bool" trk_line nil)
(trk_line_eps_irt const-decl
"{nvo: Vect2 | nvo /= zero => trk_only?(vo)(nvo)}" trk_line nil)
(tangent_line? const-decl "bool" tangent_line nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(tangent_line const-decl "Nz_vect2" tangent_line nil)
(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)
(trk_only_line const-decl "{k: real, nvo: Vect2 |
nvo /= zero => trk_only?(vo)(nvo) AND k * vnz = nvo - vi}"
trk_only nil)
(D formal-const-decl "posreal" trk_line 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)
(- const-decl "Vector" vectors_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(trk_only? const-decl "bool" definitions nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(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)
(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)
(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)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil))
nil)
(trk_line_eps_irt_tangent_line-2 nil 3445708324
(";;; Proof gs_line_eps_tangent_line-1 for formula gs_line.gs_line_eps_tangent_line"
(skeep)
((";;; Proof gs_line_eps_tangent_line-1 for formula gs_line.gs_line_eps_tangent_line"
(beta)
((";;; Proof gs_line_eps_tangent_line-1 for formula gs_line.gs_line_eps_tangent_line"
(flatten)
((";;; Proof gs_line_eps_tangent_line-1 for formula gs_line.gs_line_eps_tangent_line"
(name-replace "gso" "gs_line_eps(sp, vo, vi, eps)" :hide?
nil)
((";;; Proof gs_line_eps_tangent_line-1 for formula gs_line.gs_line_eps_tangent_line"
(expand "gs_line_eps" :assert? none)
((";;; Proof gs_line_eps_tangent_line-1 for formula gs_line.gs_line_eps_tangent_line"
(skoletin -1 :postfix "a")
((";;; Proof gs_line_eps_tangent_line-1 for formula gs_line.gs_line_eps_tangent_line"
(lift-if)
((";;; Proof gs_line_eps_tangent_line-1 for formula gs_line.gs_line_eps_tangent_line"
(split -)
(("1" (flatten)
(("1"
(typepred
"gs_only_line(tangent_line(sp, eps),vo, vi)")
(("1" (replaces (-4 -5) :dir rl)
(("1" (assert)
(("1" (flatten)
(("1" (expand "tangent_line?")
(("1"
(inst?)
(("1" (assert) nil)))))))))))))))
("2" (flatten) (("2" (assert) nil))))))))))))))))))
";;; developed with shostak decision procedures")
nil nil)
(trk_line_eps_irt_tangent_line-1 nil 3433243136
("" (skeep)
(("" (skoletin 1)
(("" (flatten)
(("" (expand "trk_line_eps_irt" :assert? none)
(("" (skoletin -1 :postfix "a")
(("" (lift-if)
(("" (split -)
(("1" (flatten)
(("1"
(typepred
"trk_only_line(tangent_line(sp, eps),vo, vi, irt)")
(("1" (assert)
(("1" (flatten)
(("1" (expand "tangent_line?")
(("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((zero const-decl "Vector" vectors_2D "vectors/")
(Sign type-eq-decl nil sign "reals/")
(Sp_vect2 type-eq-decl nil horizontal nil)
(sq const-decl "nonneg_real" sq "reals/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(tangent_line? const-decl "bool" tangent_line nil)
(Nz_vect2 type-eq-decl nil 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)
(tangent_line const-decl "Nz_vect2" tangent_line nil))
nil))
(trk_line_eps_irt_dot 0
(trk_line_eps_irt_dot-1 nil 3461085498
("" (skeep)
(("" (expand "trk_line_eps_irt?")
(("" (flatten)
(("" (expand "trk_line_eps_irt")
(("" (lift-if)
(("" (ground)
(("" (lemma "trk_only_line_lt")
(("" (expand "trk_only_line?")
(("" (inst?)
((""
(name-replace "trko1"
"trk_only_line(tangent_line(ss, eps), vo, vi, -1)"
:hide? nil)
((""
(name-replace "trko2"
"trk_only_line(tangent_line(ss, eps), vo, vi, 1)"
:hide? nil)
((""
(inst -3 "trko1`1" "trko2`1" "trko1`2"
"trko2`2")
((""
(typepred
" trk_only_line(tangent_line(ss, eps), vo, vi, -1)")
((""
(typepred
" trk_only_line(tangent_line(ss, eps), vo, vi, 1)")
((""
(ground)
(("1"
(replaces (-6 -7))
(("1"
(expand "tangent_line")
(("1"
(name-replace "k1" "trko1`1")
(("1"
(name-replace "k2" "trko2`1")
(("1"
(replaces (-7 -9) :dir rl)
(("1"
(case-replace
"nvo1 = k1 * Qs(ss, eps) + vi")
(("1"
(case-replace
"nvo2 = k2 * Qs(ss, eps) + vi")
(("1"
(rewrite
"dot_add_left")
(("1"
(rewrite
"dot_add_left")
(("1"
(lemma
"s_dot_Qs_lt_0")
(("1"
(inst?)
(("1"
(rewrite
"dot_comm")
(("1"
(mult-by
-1
"(k2-k1)")
(("1"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but (-6 1))
(("2"
(grind :exclude "Qs")
(("2"
(decompose-equality
1)
nil
nil))
nil))
nil))
nil)
("2"
(hide-all-but (-3 1))
(("2"
(grind :exclude "Qs")
(("2"
(decompose-equality
1)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (decompose-equality 1) nil nil)
("3" (decompose-equality 1) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((trk_line_eps_irt? const-decl "bool" trk_line nil)
(trk_line_eps_irt const-decl
"{nvo: Vect2 | nvo /= zero => trk_only?(vo)(nvo)}" trk_line nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(trk_only_line? const-decl "bool" trk_only 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/")
(* const-decl "Vector" vectors_2D "vectors/")
(trk_only? const-decl "bool" definitions nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(both_sides_times_pos_lt1 formula-decl nil real_props nil)
(* const-decl "real" vectors_2D "vectors/")
(k1 skolem-const-decl "real" trk_line nil)
(k2 skolem-const-decl "real" trk_line nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(add_cancel_neg2 formula-decl nil vectors_2D "vectors/")
(dot_comm formula-decl nil vectors_2D "vectors/")
(s_dot_Qs_lt_0 formula-decl nil tangent_line nil)
(dot_scal_left formula-decl nil vectors_2D "vectors/")
(real_plus_real_is_real application-judgement "real" reals nil)
(Qs_nzv application-judgement "Nz_vect2" trk_line nil)
(real_times_real_is_real application-judgement "real" reals nil)
(dot_add_left formula-decl nil vectors_2D "vectors/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(+ const-decl "Vector" vectors_2D "vectors/")
(Qs const-decl "Vect2" tangent_line nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(Ss_vect2 type-eq-decl nil horizontal nil)
(tangent_line const-decl "Nz_vect2" tangent_line 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)
(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)
(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/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(trk_only_line_lt formula-decl nil trk_only 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" trk_line nil))
shostak))
(irt_trk_line_eps 0
(irt_trk_line_eps-1 nil 3433244352
("" (skeep)
(("" (expand "trk_line_eps?")
(("" (expand "trk_line_eps_irt?")
(("" (flatten)
(("" (expand "trk_line_eps")
(("" (lift-if)
(("" (split -1)
(("1" (flatten)
(("1" (inst? 2) (("1" (assert) nil nil)) nil)) nil)
("2" (flatten)
(("2" (split -1)
(("1" (flatten)
(("1" (inst? 3) (("1" (assert) nil nil)) nil))
nil)
("2" (flatten)
(("2" (inst? 5) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((trk_line_eps? const-decl "bool" trk_line nil)
(minus_odd_is_odd application-judgement "odd_int" integers 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)
(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)
(trk_line_eps const-decl
"{nvo | nvo /= zero => trk_only?(vo)(nvo)}" trk_line nil)
(trk_line_eps_irt? const-decl "bool" trk_line nil))
nil))
(trk_line_eps_tangent_line 0
(trk_line_eps_tangent_line-1 nil 3433243309
("" (skeep)
(("" (lemma "irt_trk_line_eps")
(("" (inst?)
(("" (assert)
(("" (skeep -1)
(("" (lemma "trk_line_eps_irt_tangent_line")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((irt_trk_line_eps formula-decl nil trk_line nil)
(trk_line_eps_irt_tangent_line formula-decl nil trk_line nil)
(Sp_vect2 type-eq-decl nil horizontal nil)
(D formal-const-decl "posreal" trk_line nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(sq const-decl "nonneg_real" sq "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(>= const-decl "bool" reals nil)
(Vect2 type-eq-decl nil vectors_2D_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))
(trk_line_is_line_solution 0
(trk_line_is_line_solution-1 nil 3471194302
("" (skeep)
(("" (lemma "trk_line_eps_tangent_line")
(("" (inst?)
(("" (assert)
(("" (lemma "tangent_line_solution")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((trk_line_eps_tangent_line formula-decl nil trk_line nil)
(- const-decl "Vector" vectors_2D "vectors/")
(tangent_line_solution formula-decl nil tangent_line nil)
(Sp_vect2 type-eq-decl nil horizontal nil)
(D formal-const-decl "posreal" trk_line nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(sq const-decl "nonneg_real" sq "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(>= const-decl "bool" reals nil)
(Vect2 type-eq-decl nil vectors_2D_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))
(trk_line_complete 0
(trk_line_complete-1 nil 3444080087
("" (skeep)
(("" (skeep -2)
(("" (rewrite "tangent_line_solution" :dir rl)
(("" (expand "tangent_line?")
(("" (skeep -2)
(("" (lemma "trk_only_line_complete")
((""
(inst -1 "nnk" "nvo" "vi" "tangent_line(sp,eps)"
"vnzo")
(("" (assert)
(("" (expand "trk_only_line?")
(("" (skeep -1)
(("" (expand "trk_line?")
(("" (assert)
(("" (inst 2 "eps" "irt")
(("" (expand "trk_line_eps_irt")
((""
(decompose-equality -1)
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((tangent_line? const-decl "bool" tangent_line nil)
(trk_only_line_complete formula-decl nil trk_only nil)
(trk_line_eps_irt const-decl
"{nvo: Vect2 | nvo /= zero => trk_only?(vo)(nvo)}" trk_line nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(trk_only? const-decl "bool" definitions nil)
(* 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)
(trk_line? const-decl "bool" trk_line nil)
(trk_only_line? const-decl "bool" trk_only nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(tangent_line const-decl "Nz_vect2" tangent_line nil)
(D formal-const-decl "posreal" trk_line 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 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)
(- 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)
(Vector type-eq-decl nil vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_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)
(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)
(tangent_line_solution formula-decl nil tangent_line nil))
nil)))
¤ Dauer der Verarbeitung: 0.27 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.
|
