|
(distance_2D
(dist_eq_args 0
(dist_eq_args-1 nil 3285678295
("" (skosimp*)
(("" (expand "dist")
(("" (expand "sq_dist")
(("" (assert)
(("" (expand "sq")
(("" (assert) (("" (rewrite "sqrt_0") nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((dist const-decl "nnreal" distance_2D nil)
(sq_0 formula-decl nil sq "reals/")
(sqrt_0 formula-decl nil sqrt "reals/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq_dist const-decl "nnreal" distance_2D nil))
shostak))
(dist_zero_l 0
(dist_zero_l-1 nil 3285677920 ("" (grind) nil nil)
((comp_zero_x formula-decl nil vectors_2D nil)
(sq const-decl "nonneg_real" sq "reals/")
(comp_zero_y formula-decl nil vectors_2D nil)
(sq_dist const-decl "nnreal" distance_2D nil)
(dist const-decl "nnreal" distance_2D nil)
(* const-decl "real" vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(dist_zero_r 0
(dist_zero_r-1 nil 3285677983 ("" (grind :exclude ("zero")) nil nil)
((comp_zero_x formula-decl nil vectors_2D nil)
(sq const-decl "nonneg_real" sq "reals/")
(comp_zero_y formula-decl nil vectors_2D nil)
(sq_dist const-decl "nnreal" distance_2D nil)
(dist const-decl "nnreal" distance_2D nil)
(* const-decl "real" vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(norm const-decl "nnreal" vectors_2D nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(dist_sym 0
(dist_sym-1 nil 3255275743 ("" (skosimp*) (("" (grind) nil nil)) nil)
((sq const-decl "nonneg_real" sq "reals/")
(sq_dist const-decl "nnreal" distance_2D nil)
(dist const-decl "nnreal" distance_2D 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)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil))
nil))
(dist_eq_0 0
(dist_eq_0-2 nil 3256562733
("" (skosimp*)
(("" (prop)
(("1" (expand "dist")
(("1" (expand "sq_dist")
(("1" (rewrite "sq_eq" :dir rl)
(("1" (rewrite "sq_sqrt")
(("1" (rewrite "sq_0")
(("1"
(case "sq(p1!1`x - p2!1`x) = 0 AND sq(p1!1`y - p2!1`y) = 0")
(("1" (hide -2)
(("1" (flatten)
(("1" (apply-extensionality 1 :hide? t)
(("1" (rewrite "sq.sq_eq_0") nil nil)
("2" (hide -1)
(("2" (rewrite "sq.sq_eq_0") nil nil)) nil))
nil))
nil))
nil)
("2" (hide 2) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace -1) (("2" (rewrite "dist_eq_args") nil nil)) nil))
nil))
nil)
((sq_dist const-decl "nnreal" distance_2D nil)
(sq_sqrt formula-decl nil sqrt "reals/")
(sq_eq_0 formula-decl nil sq "reals/")
(AND const-decl "[bool, bool -> bool]" booleans nil)
(sq_0 formula-decl nil sq "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sq const-decl "nonneg_real" sq "reals/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types 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)
(sq_eq formula-decl nil sq "reals/")
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(dist const-decl "nnreal" distance_2D nil)
(dist_eq_args formula-decl nil distance_2D nil))
nil)
(dist_eq_0-1 nil 3255275743
("" (skosimp*)
(("" (prop)
(("1" (expand "dist")
(("1" (expand "sq_dist")
(("1" (rewrite "sq_eq" :dir rl)
(("1" (rewrite "sq_sqrt")
(("1" (rewrite "sq_0")
(("1"
(case "sq(v1!1`x - v2!1`x) = 0 AND sq(v1!1`y - v2!1`y) = 0")
(("1" (hide -2)
(("1" (flatten)
(("1" (apply-extensionality 1 :hide? t)
(("1" (rewrite "sq.sq_eq_0") nil nil)
("2" (hide -1)
(("2" (rewrite "sq.sq_eq_0") nil nil)) nil))
nil))
nil))
nil)
("2" (hide 2) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace -1) (("2" (rewrite "dist_refl") nil nil)) nil))
nil))
nil)
((sq_sqrt formula-decl nil sqrt "reals/")
(sq_eq_0 formula-decl nil sq "reals/")
(sq_0 formula-decl nil sq "reals/")
(sq const-decl "nonneg_real" sq "reals/")
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(sq_eq formula-decl nil sq "reals/"))
nil))
(dist_norm 0
(dist_norm-1 nil 3255275743
("" (skosimp*)
(("" (expand "dist")
(("" (expand "norm")
(("" (expand "sq_dist")
(("" (expand "sq")
(("" (assert)
(("" (expand "sqv")
(("" (expand "*")
(("" (expand "-") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((dist const-decl "nnreal" distance_2D nil)
(sq_dist const-decl "nnreal" distance_2D nil)
(* const-decl "real" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(sq const-decl "nonneg_real" sq "reals/")
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(norm const-decl "nnreal" vectors_2D nil))
nil))
(dist_rel 0
(dist_rel-1 nil 3255275743 ("" (skosimp*) (("" (grind) nil nil)) nil)
((real_plus_real_is_real application-judgement "real" reals nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(dist const-decl "nnreal" distance_2D nil)
(sq_dist const-decl "nnreal" distance_2D nil)
(sq const-decl "nonneg_real" sq "reals/")
(+ const-decl "Vector" vectors_2D nil))
nil))
(sq_dist_is_dist_sq 0
(sq_dist_is_dist_sq-1 nil 3255275743 ("" (grind) nil nil)
((nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq const-decl "nonneg_real" sq "reals/")
(sq_dist const-decl "nnreal" distance_2D nil)
(dist const-decl "nnreal" distance_2D 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))
nil))
(sq_dist_norm 0
(sq_dist_norm-1 nil 3255717113
("" (skosimp*)
(("" (rewrite "sq_dist_is_dist_sq")
(("" (rewrite "dist_norm") nil nil)) nil))
nil)
((sq_dist_is_dist_sq formula-decl nil distance_2D nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(dist_norm formula-decl nil distance_2D nil))
shostak))
(sq_dist_sym 0
(sq_dist_sym-1 nil 3255277056
("" (skosimp*)
(("" (rewrite "sq_dist_is_dist_sq")
(("" (rewrite "sq_dist_is_dist_sq")
(("" (rewrite "dist_sym") nil nil)) nil))
nil))
nil)
((sq_dist_is_dist_sq formula-decl nil distance_2D nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(dist_sym formula-decl nil distance_2D nil))
shostak))
(sq_dist_le 0
(sq_dist_le-1 nil 3256052713
("" (skosimp*)
(("" (expand "dist") (("" (rewrite "sqrt_le") nil nil)) nil)) nil)
((dist const-decl "nnreal" distance_2D nil)
(sq_dist const-decl "nnreal" distance_2D nil)
(nnreal type-eq-decl nil real_types nil)
(Vect2 type-eq-decl nil vectors_2D_def 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)
(sqrt_le formula-decl nil sqrt "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(sq_dist_lt 0
(sq_dist_lt-1 nil 3256052727
("" (skosimp*)
(("" (expand "dist") (("" (rewrite "sqrt_lt") nil nil)) nil)) nil)
((dist const-decl "nnreal" distance_2D nil)
(sq_dist const-decl "nnreal" distance_2D nil)
(nnreal type-eq-decl nil real_types nil)
(Vect2 type-eq-decl nil vectors_2D_def 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)
(sqrt_lt formula-decl nil sqrt "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(dist_ge_x 0
(dist_ge_x-2 nil 3256562809
("" (skosimp*)
(("" (expand "dist")
(("" (expand "sq_dist")
((""
(case "sqrt(sq(p1!1`x - p2!1`x) + sq(p1!1`y - p2!1`y)) >= sqrt(sq(p1!1`x - p2!1`x))")
(("1" (rewrite "sqrt_sq_abs") nil nil)
("2" (hide 2)
(("2" (rewrite "sqrt_ge") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((dist const-decl "nnreal" distance_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sq const-decl "nonneg_real" sq "reals/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types 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)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sqrt_sq_abs formula-decl nil sqrt "reals/")
(sqrt_ge formula-decl nil sqrt "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq_dist const-decl "nnreal" distance_2D nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil)
(dist_ge_x-1 nil 3256552897
("" (skosimp*)
(("" (expand "dist")
(("" (expand "sq_dist")
((""
(case "sqrt(sq(v1!1`x - v2!1`x) + sq(v1!1`y - v2!1`y)) >= sqrt(sq(v1!1`x - v2!1`x))")
(("1" (rewrite "sqrt_sq_abs") nil nil)
("2" (hide 2)
(("2" (rewrite "sqrt_ge") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((sq const-decl "nonneg_real" sq "reals/")
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(sqrt_sq_abs formula-decl nil sqrt "reals/")
(sqrt_ge formula-decl nil sqrt "reals/"))
nil))
(dist_ge_y 0
(dist_ge_y-2 nil 3256562825
("" (skosimp*)
(("" (expand "dist")
(("" (expand "sq_dist")
((""
(case "sqrt(sq(p1!1`x - p2!1`x) + sq(p1!1`y - p2!1`y)) >= sqrt(sq(p1!1`y - p2!1`y))")
(("1" (rewrite "sqrt_sq_abs") nil nil)
("2" (hide 2)
(("2" (rewrite "sqrt_ge") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((dist const-decl "nnreal" distance_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sq const-decl "nonneg_real" sq "reals/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types 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)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sqrt_sq_abs formula-decl nil sqrt "reals/")
(sqrt_ge formula-decl nil sqrt "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq_dist const-decl "nnreal" distance_2D nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil)
(dist_ge_y-1 nil 3256552923
("" (skosimp*)
(("" (expand "dist")
(("" (expand "sq_dist")
((""
(case "sqrt(sq(v1!1`x - v2!1`x) + sq(v1!1`y - v2!1`y)) >= sqrt(sq(v1!1`y - v2!1`y))")
(("1" (rewrite "sqrt_sq_abs") nil nil)
("2" (hide 2)
(("2" (rewrite "sqrt_ge") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((sq const-decl "nonneg_real" sq "reals/")
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(sqrt_sq_abs formula-decl nil sqrt "reals/")
(sqrt_ge formula-decl nil sqrt "reals/"))
nil))
(sq_dist_dist 0
(sq_dist_dist-1 nil 3445159520
("" (skosimp*)
(("" (lemma "sq_norm_dist")
(("" (inst -1 "p0!1" "p1!1" "p2!1")
(("" (assert)
(("" (assert)
(("" (rewrite "dist_norm")
(("" (rewrite "dist_norm")
(("" (rewrite "dist_norm") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sq_norm_dist formula-decl nil vectors_2D nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(dot_scal_left formula-decl nil vectors_2D nil)
(dist_norm formula-decl nil distance_2D nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(real nonempty-type-from-decl nil reals nil))
nil))
(dist_triangle 0
(dist_triangle-1 nil 3445159541
("" (skeep)
(("" (expand "dist")
(("" (expand "sq_dist")
((""
(case-replace
"sq(p0`x - p2`x) = sq(p0`x - p1`x + p1`x - p2`x)")
(("1" (hide -1)
(("1"
(case-replace
"sq(p0`y - p2`y) = sq(p0`y - p1`y + p1`y - p2`y)")
(("1" (hide -1)
(("1" (lemma "schwarz_cor")
(("1" (inst - "p0-p1" "p1-p2")
(("1" (grind) nil nil)) nil))
nil))
nil)
("2" (hide 2) (("2" (assert) nil nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
((dist const-decl "nnreal" distance_2D nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(sq const-decl "nonneg_real" sq "reals/")
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(schwarz_cor formula-decl nil vectors_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(* const-decl "real" vectors_2D nil)
(sqv const-decl "nnreal" vectors_2D nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Vector type-eq-decl nil vectors_2D nil)
(- const-decl "Vector" vectors_2D nil)
(sq_dist const-decl "nnreal" distance_2D nil))
nil))
(dist_tri_sub 0
(dist_tri_sub-2 nil 3445159979
("" (skeep)
(("" (lemma "dist_triangle")
(("" (inst-cp - "p0" "p1" "p2")
(("" (inst - "p1" "p0" "p2")
(("" (expand "abs")
(("" (lift-if)
(("" (ground)
(("" (lemma "dist_sym")
(("" (inst - "p0" "p1") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((dist_triangle formula-decl nil distance_2D nil)
(dist_sym formula-decl nil distance_2D nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(Vect2 type-eq-decl nil vectors_2D_def nil)
(real nonempty-type-from-decl nil reals nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil)
(dist_tri_sub-1 nil 3445099122
("" (skeep)
(("" (lemma "dist_triangle_lt")
(("" (inst-cp - "p0" "p1" "p2")
(("" (inst - "p1" "p0" "p2")
(("" (expand "abs")
(("" (lift-if)
(("" (ground)
(("" (lemma "dist_sym")
(("" (inst - "p0" "p1") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Vect2 type-eq-decl nil vectors_2D_def nil)) nil))
(on_segment_beg 0
(on_segment_beg-1 nil 3255349846
("" (skosimp*)
(("" (expand "on_segment?")
(("" (inst + "0")
(("" (grind) (("" (apply-extensionality 1 :hide? t) nil nil))
nil))
nil))
nil))
nil)
((on_segment? const-decl "bool" distance_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil)
(real_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)
(Vect2 type-eq-decl nil vectors_2D_def 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)
(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))
shostak))
(on_segment_end 0
(on_segment_end-1 nil 3255349879
("" (skosimp*)
(("" (expand "on_segment?")
(("" (inst + "1")
(("" (grind) (("" (apply-extensionality 1 :hide? t) nil nil))
nil))
nil))
nil))
nil)
((on_segment? const-decl "bool" distance_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil)
(real_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)
(Vect2 type-eq-decl nil vectors_2D_def 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)
(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))
shostak))
(on_line_beg 0
(on_line_beg-1 nil 3255689996
("" (skosimp*)
(("" (expand "on_line?")
(("" (inst + "0")
(("" (grind) (("" (apply-extensionality 1 :hide? t) nil nil))
nil))
nil))
nil))
nil)
((on_line? const-decl "bool" distance_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil)
(real_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)
(Vect2 type-eq-decl nil vectors_2D_def 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))
shostak))
(on_line_end 0
(on_line_end-1 nil 3255690905
("" (skosimp*)
(("" (expand "on_line?")
(("" (inst + "1")
(("" (grind) (("" (apply-extensionality 1 :hide? t) nil nil))
nil))
nil))
nil))
nil)
((on_line? const-decl "bool" distance_2D nil)
(+ const-decl "Vector" vectors_2D nil)
(* const-decl "Vector" vectors_2D nil)
(- const-decl "Vector" vectors_2D nil)
(real_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)
(Vect2 type-eq-decl nil vectors_2D_def 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))
shostak))
(on_segment_on_line 0
(on_segment_on_line-1 nil 3255349896
("" (skosimp*)
(("" (expand "on_segment?")
(("" (expand "on_line?")
(("" (skosimp*) (("" (inst?) nil nil)) nil)) nil))
nil))
nil)
((on_segment? const-decl "bool" distance_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)
(nnreal type-eq-decl nil real_types nil)
(<= const-decl "bool" reals nil)
(on_line? const-decl "bool" distance_2D nil))
shostak)))
¤ Dauer der Verarbeitung: 0.9 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.
|
