|
(opt_vertical
(opt_vertical_TCC1 0
(opt_vertical_TCC1-1 nil 3471190121
("" (skosimp*) (("" (assert) nil nil)) nil)
((vect2_zero formula-decl nil vect_3D_2D "vectors/")) nil))
(opt_vertical_TCC2 0
(opt_vertical_TCC2-1 nil 3471190121
("" (skosimp*)
(("" (replaces -1) (("" (hide -1) (("" (grind) nil nil)) nil))
nil))
nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(- const-decl "Vector" vectors_3D "vectors/"))
nil))
(opt_vertical_TCC3 0
(opt_vertical_TCC3-1 nil 3471190121
("" (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))
(opt_vertical_TCC4 0
(opt_vertical_TCC4-1 nil 3471199495
("" (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))
(opt_vertical_TCC5 0
(opt_vertical_TCC5-1 nil 3471199495 ("" (skosimp*) nil nil) nil nil))
(opt_vertical_TCC6 0
(opt_vertical_TCC6-1 nil 3471199495
("" (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))
(opt_vertical_TCC7 0
(opt_vertical_TCC7-1 nil 3471199495
("" (skosimp*) (("" (assert) nil nil)) nil)
((sign_neg_clos application-judgement "Sign" sign "reals/")
(vect2_zero formula-decl nil vect_3D_2D "vectors/"))
nil))
(opt_vertical_meets_horizontal_criterion 0
(opt_vertical_meets_horizontal_criterion-1 nil 3471190475
("" (skeep)
(("" (expand "opt_vertical?")
(("" (flatten)
(("" (expand "opt_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)
((opt_vertical? const-decl "bool" opt_vertical nil)
(opt_vertical const-decl
"{nvo | vect2(nvo) /= zero => vo`z = nvo`z}" opt_vertical nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Sp2_vect3 type-eq-decl nil space_3D nil)
(H formal-const-decl "posreal" opt_vertical nil)
(D formal-const-decl "posreal" opt_vertical 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]" opt_vertical nil)
(vect2_sub formula-decl nil vect_3D_2D "vectors/")
(opt_trk_gs_vertical const-decl "Vect2" opt_trk_gs 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))
nil))
(opt_vertical_meets_vertical_criterion 0
(opt_vertical_meets_vertical_criterion-1 nil 3471190526
("" (skeep)
(("" (expand "opt_vertical?")
(("" (flatten)
(("" (expand "opt_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
"opto"
"opt_trk_gs_vertical(vect2(s), vect2(vo), vect2(vi),
Theta_H(s`z, (vo - vi)`z, -DIR), DIR)"
:hide?
nil)
(("1"
(lemma
"opt_trk_gs_vertical_on_D")
(("1"
(inst
-1
"DIR"
"opto"
"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
"opt_trk_gs_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)
((opt_vertical? const-decl "bool" opt_vertical nil)
(opt_vertical const-decl
"{nvo | vect2(nvo) /= zero => vo`z = nvo`z}" opt_vertical nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(H formal-const-decl "posreal" opt_vertical 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)
(opt_trk_gs_vertical_on_D formula-decl nil opt_trk_gs nil)
(opt_trk_gs_vertical? const-decl "bool" opt_trk_gs 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" opt_vertical nil)
(vi skolem-const-decl "Nzv2_vect3" opt_vertical nil)
(vo skolem-const-decl "Nzv2_vect3" opt_vertical nil)
(s skolem-const-decl "Vect3" opt_vertical nil)
(nzv2 application-judgement "Nz_vect2" definitions_3D nil)
(D formal-const-decl "posreal" opt_vertical nil)
(opt_trk_gs_vertical const-decl "Vect2" opt_trk_gs 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.24 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.
|
