|
(between_2D
(between_sym 0
(between_sym-1 nil 3408459467 ("" (grind) nil nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(* const-decl "real" vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil)
(between? const-decl "bool" between_2D nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil))
shostak))
(between_cos 0
(between_cos-1 nil 3408454966
("" (skeep)
(("" (assert)
(("" (expand "between?")
(("" (rewrite "norm_v_from")
(("" (rewrite "norm_v_from")
(("" (rewrite "norm_v_from")
(("" (expand "v_from")
(("" (expand "*")
(("" (expand "-")
(("" (lemma "cos_minus")
(("" (inst - "a3" "a1")
(("" (move-terms -1 R 1)
(("" (assert)
(("" (replace -1 * rl)
((""
(hide -1)
((""
(lemma "cos_minus")
((""
(inst - "a3" "a2")
((""
(move-terms -1 R 1)
((""
(assert)
((""
(replace -1 * rl)
((""
(hide -1)
((""
(lemma "cos_minus")
((""
(inst - "a2" "a1")
((""
(move-terms -1 R 1)
((""
(replace -1 * rl)
((""
(assert)
((""
(hide -1)
((""
(split +)
(("1"
(flatten)
(("1"
(div-by
-1
"k1*k2*k3")
(("1"
(assert)
(("1"
(div-by
-2
"k1*k2*k3")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(mult-by
-1
"k1*k2 * k3")
(("2"
(assert)
(("2"
(mult-by
-2
"k1*k2 * k3")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" trig_basic "trig/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(norm_v_from formula-decl nil angles_2D 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)
(real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(cos_minus formula-decl nil trig_basic "trig/")
(sin const-decl "real" trig_basic "trig/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(cos const-decl "real" trig_basic "trig/")
(= const-decl "[T, T -> boolean]" equalities nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(both_sides_div_pos_le1 formula-decl nil real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(both_sides_times_pos_le1_imp formula-decl nil extra_real_props
nil)
(- const-decl "Vector" vectors_2D nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(v_from const-decl "Vect2" angles_2D nil)
(sin_range application-judgement "trig_range" trig_basic "trig/")
(between? const-decl "bool" between_2D nil))
nil))
(is_between 0
(is_between-1 nil 3408724334
("" (skeep)
(("" (assert)
(("" (lemma "between_cos")
(("" (inst - "a1" "a2" "a3" "k1" "k2" "k3")
(("" (assert)
(("" (hide 2)
(("" (lemma "cos_decr")
(("" (inst - "a3-a1" "a3 - a2")
(("" (assert)
(("" (lemma "cos_decr")
(("" (inst - "a3-a1" "a2 - a1")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(cos_decr formula-decl nil trig_ineq "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/")
(between_cos formula-decl nil between_2D nil))
nil))
(is_between2 0
(is_between2-2 nil 3408724353
("" (skeep)
(("" (assert)
(("" (lemma "is_between")
(("" (inst - "a1" "a2" "a3" "k1" "k2" "k3")
(("" (assert) nil nil)) nil))
nil))
nil))
nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(real_minus_real_is_real application-judgement "real" reals nil)
(is_between formula-decl nil between_2D nil))
nil)
(is_between2-1 nil 3408460061
("" (skeep)
(("" (assert)
(("" (lemma "is_between_k")
(("" (inst - "a1" "a2" "a3" "k1" "k2" "k3")
(("" (assert) nil nil)) nil))
nil))
nil))
nil)
nil nil))
(between_lem 0
(between_lem-1 nil 3408460115
("" (skeep)
(("" (assert)
(("" (flatten)
(("" (lemma "between_cos")
(("" (inst - "a1" "a2" "a3" "k1" "k2" "k3")
(("" (assert)
(("" (assert)
(("" (flatten)
(("" (lemma "cos_decr")
(("" (inst - "a3-a1" "a2 - a1")
(("" (assert)
(("" (lemma "cos_decr")
(("" (inst - "a3-a1" "a3 - a2")
(("" (assert) (("" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(between_cos formula-decl nil between_2D nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" trig_basic "trig/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(cos_decr formula-decl nil trig_ineq "trig/")
(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))
nil))
(between_thm 0
(between_thm-1 nil 3408460160
("" (skeep)
(("" (assert)
(("" (flatten)
(("" (lemma "between_lem")
(("" (assert)
(("" (inst - "a1" "a2" "a3" "k1" "k2" "k3")
(("" (assert)
(("" (lemma "between_lem")
(("" (inst - "a3" "a2" "a1" "k3" "k2" "k1")
(("" (assert)
(("" (ground)
(("1" (rewrite "between_sym") nil nil)
("2" (rewrite "between_sym") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(between_lem formula-decl nil between_2D 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)
(between_sym formula-decl nil between_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(v_from const-decl "Vect2" angles_2D nil))
nil))
(betw_between 0
(betw_between-2 nil 3414494072
("" (skosimp*)
(("" (expand "betw?")
(("" (flatten)
(("" (lemma "is_between")
((""
(inst - "angle(v1!1)" "angle(xx!1)" "angle(v2!1)"
"norm(v1!1)" "norm(xx!1)" "norm(v2!1)")
(("1" (assert)
(("1" (rewrite "v_from_angle")
(("1" (rewrite "v_from_angle")
(("1" (rewrite "v_from_angle") nil nil)) nil))
nil))
nil)
("2" (typepred "v2!1")
(("2" (flatten) (("2" (assert) nil nil)) nil)) nil)
("3" (typepred "xx!1") (("3" (assert) nil nil)) nil)
("4" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((betw? const-decl "bool" between_2D nil)
(is_between formula-decl nil between_2D nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(angle const-decl "{alpha: Angle | u = v_from(alpha, norm(u))}"
angles_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(v_from const-decl "Vect2" angles_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Angle nonempty-type-eq-decl nil angles_2D nil)
(pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
"trig/")
(pi_ub const-decl "posreal" trig_basic "trig/")
(pi_lb const-decl "posreal" trig_basic "trig/")
(AND const-decl "[bool, bool -> bool]" booleans 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 "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors_2D 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)
(nz_norm_gt_0 application-judgement "posreal" vectors_2D nil))
nil)
(betw_between-1 nil 3414492803
("" (skosimp*)
(("" (lemma "between_cos")
((""
(inst - "angle(v1!1)" "angle(xx!1)" "angle(v2!1)" "norm(v1!1)"
"norm(xx!1)" "norm(v2!1)")
(("1" (assert)
(("1" (rewrite "v_from_angle")
(("1" (rewrite "v_from_angle")
(("1" (rewrite "v_from_angle")
(("1" (assert)
(("1" (hide 2)
(("1" (rewrite "cos_minus")
(("1" (rewrite "cos_minus")
(("1" (expand "betw?")
(("1" (flatten) (("1" (postpone) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (postpone) nil nil) ("3" (postpone) nil nil)
("4" (postpone) nil nil))
nil))
nil))
nil)
nil shostak))
(between_betw 0
(between_betw-1 nil 3414494158
("" (skosimp*)
(("" (lemma "between_lem")
((""
(inst - "angle(v1!1)" "angle(xx!1)" "angle(v2!1)" "norm(v1!1)"
"norm(xx!1)" "norm(v2!1)")
(("1" (assert)
(("1" (rewrite "v_from_angle")
(("1" (rewrite "v_from_angle")
(("1" (rewrite "v_from_angle")
(("1" (assert)
(("1" (expand "betw?") (("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil) ("3" (assert) nil nil)
("4" (assert) nil nil))
nil))
nil))
nil)
((between_lem formula-decl nil between_2D nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(betw? const-decl "bool" between_2D nil)
(angle const-decl "{alpha: Angle | u = v_from(alpha, norm(u))}"
angles_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(v_from const-decl "Vect2" angles_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Angle nonempty-type-eq-decl nil angles_2D nil)
(pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
"trig/")
(pi_ub const-decl "posreal" trig_basic "trig/")
(pi_lb const-decl "posreal" trig_basic "trig/")
(AND const-decl "[bool, bool -> bool]" booleans 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 "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(Nz_vect2 type-eq-decl nil vectors_2D nil)
(zero const-decl "Vector" vectors_2D nil)
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors_2D 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)
(nz_norm_gt_0 application-judgement "posreal" vectors_2D nil))
nil)))
¤ Dauer der Verarbeitung: 0.36 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
