|
(old_horiz_los_criterion
(horizontal_los_crit_symm 0
(horizontal_los_crit_symm-1 nil 3488034416 ("" (grind) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(/= const-decl "boolean" notequal 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/")
(real_minus_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(* const-decl "real" vectors_2D "vectors/")
(det const-decl "real" det_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(norm const-decl "nnreal" vectors_2D "vectors/")
(horizontal_los_crit? const-decl "bool" old_horiz_los_criterion
nil)
(- const-decl "Vector" vectors_2D "vectors/")
(real_times_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(horizontal_los_crit_independent 0
(horizontal_los_crit_independent-1 nil 3488118551
("" (skeep)
(("" (lemma "dot_nneg_divergent")
(("" (inst?)
(("1" (replace -1 :dir rl)
(("1" (hide -1)
(("1" (expand "horizontal_los_crit?")
(("1" (propax) nil nil)) nil))
nil))
nil)
("2" (ground) nil nil))
nil))
nil))
nil)
((dot_nneg_divergent formula-decl nil definitions nil)
(horizontal_los_crit? const-decl "bool" old_horiz_los_criterion
nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(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 "boolean" notequal nil)
(- const-decl "Vector" vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(nvo skolem-const-decl "Vect2" old_horiz_los_criterion nil)
(vi skolem-const-decl "Vect2" old_horiz_los_criterion nil)
(zero const-decl "Vector" vectors_2D "vectors/"))
shostak))
(horizontal_los_crit_coordinated 0
(horizontal_los_crit_coordinated-1 nil 3488034263
("" (skeep)
(("" (rewrite "dot_nneg_divergent" :dir rl)
(("1" (expand "horizontal_los_crit?")
(("1" (flatten)
(("1" (hide (-2 -3 -5 -6)) (("1" (grind) nil nil)) nil))
nil))
nil)
("2" (flatten)
(("2" (case "nvo-nvi = (nvo-vi) + (vo-nvi) - (vo-vi)")
(("1" (case "s*(nvo-nvi) = 0")
(("1" (replace -2 -1)
(("1" (rewrite "dot_sub_right")
(("1" (rewrite "dot_add_right")
(("1" (case "s*(vo-nvi) = -s*(nvi-vo)")
(("1" (assert)
(("1" (expand "horizontal_los_crit?")
(("1" (flatten) (("1" (assert) nil nil)) nil))
nil))
nil)
("2" (hide-all-but 1) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace -2) (("2" (assert) nil nil)) nil))
nil)
("2" (hide-all-but 1) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil)
((dot_nneg_divergent formula-decl nil definitions 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 "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(* const-decl "real" vectors_2D "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(horizontal_los_crit? const-decl "bool" old_horiz_los_criterion
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(+ const-decl "Vector" vectors_2D "vectors/")
(dot_zero_right formula-decl nil vectors_2D "vectors/")
(dot_add_right formula-decl nil vectors_2D "vectors/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(dot_sub_right formula-decl nil 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))
shostak)))
¤ Dauer der Verarbeitung: 0.1 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.
|
