|
(cd2d_inf
(detection_2D_inf_TCC1 0
(detection_2D_inf_TCC1-1 nil 3483958897 ("" (subtype-tcc) nil nil)
((real_gt_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)
(NOT const-decl "[bool -> bool]" booleans nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(sq const-decl "nonneg_real" sq "reals/")
(* const-decl "real" vectors_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(det const-decl "real" det_2D "vectors/")
(D formal-const-decl "posreal" cd2d_inf 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)
(Delta const-decl "real" horizontal 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))
nil))
(detection_2D_inf_correct 0
(detection_2D_inf_correct-1 nil 3483958907
("" (skeep)
(("" (assert)
(("" (expand "detection_2D_inf")
(("" (lift-if)
(("" (assert)
(("" (ground)
(("" (lemma "horizontal_los_inside_Theta")
(("" (inst?)
(("" (assert)
(("" (expand "max" -3)
(("" (lift-if) (("" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sq_nz_pos application-judgement "posreal" sq "reals/")
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal type-eq-decl nil real_types 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/")
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(horizontal_los_inside_Theta formula-decl nil horizontal 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" cd2d_inf nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(detection_2D_inf const-decl "[nnreal, nnreal]" cd2d_inf nil))
shostak))
(detection_2D_inf_complete 0
(detection_2D_inf_complete-1 nil 3483959002
("" (skeep)
(("" (assert)
(("" (flatten)
(("" (expand "detection_2D_inf")
(("" (lift-if)
(("" (assert)
(("" (lemma "Delta_gt_0")
(("" (inst?)
(("" (assert)
(("" (split -)
(("1" (assert)
(("1" (lemma "horizontal_los_inside_Theta")
(("1" (inst?)
(("1" (assert)
(("1"
(flatten)
(("1"
(expand "max")
(("1"
(lift-if)
(("1"
(lift-if)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "horizontal_conflict_ever?")
(("2" (inst + "t") 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)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(detection_2D_inf const-decl "[nnreal, nnreal]" cd2d_inf nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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/")
(horizontal_los_inside_Theta formula-decl nil horizontal nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(nnreal type-eq-decl nil real_types nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(horizontal_conflict_ever? const-decl "bool" horizontal nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Delta_gt_0 formula-decl nil horizontal 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" cd2d_inf nil))
shostak))
(conflict_detection_2D_inf 0
(conflict_detection_2D_inf-1 nil 3483959293
("" (skeep)
(("" (assert)
(("" (ground)
(("1" (lemma "detection_2D_inf_complete")
(("1" (expand "horizontal_conflict?")
(("1" (skosimp*)
(("1" (inst - "nzv" "s" "nnt!1") (("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2"
(name "tav"
"(detection_2D_inf(s, nzv)`1 + detection_2D_inf(s, nzv)`2)/2")
(("2" (lemma "detection_2D_inf_correct")
(("2" (inst - "nzv" "s" "tav")
(("2" (assert)
(("2" (split -)
(("1" (expand "horizontal_conflict?")
(("1" (inst + "tav") nil nil)) nil)
("2" (hide 2) (("2" (assert) nil nil)) nil)
("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(detection_2D_inf const-decl "[nnreal, nnreal]" cd2d_inf nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(detection_2D_inf_correct formula-decl nil cd2d_inf nil)
(detection_2D_inf_complete formula-decl nil cd2d_inf nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(boolean nonempty-type-decl nil booleans nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(real nonempty-type-from-decl nil reals nil)
(horizontal_conflict? const-decl "bool" horizontal nil))
nil))
(cd2d_inf 0
(cd2d_inf-1 nil 3483959557
("" (skeep)
(("" (ground)
(("1" (expand "cd2d_inf?")
(("1" (case "v = zero")
(("1" (replace -1)
(("1" (expand "horizontal_conflict?")
(("1" (skosimp*) (("1" (assert) nil nil)) nil)) nil))
nil)
("2" (flatten)
(("2" (lemma "Delta_gt_0")
(("2" (inst?)
(("2" (assert)
(("2" (lemma "horizontal_conflict_ever")
(("2" (inst?)
(("2" (assert)
(("2" (lemma "sdotv_lt_0")
(("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "cd2d_inf?")
(("2" (split -)
(("1" (expand "horizontal_conflict?")
(("1" (inst + "0") (("1" (assert) nil nil)) nil)) nil)
("2" (flatten)
(("2" (lemma "horizontal_tca_los")
(("2" (inst?)
(("1" (assert)
(("1" (expand "horizontal_conflict?")
(("1" (inst + "horizontal_tca(s,v)")
(("1" (assert)
(("1" (expand "horizontal_tca")
(("1" (cross-mult 1)
(("1" (assert)
(("1"
(ground)
(("1"
(lemma "sqv_eq_0")
(("1"
(inst?)
(("1"
(assert)
(("1"
(replace -1)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (replace -1) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((zero const-decl "Vector" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(real nonempty-type-from-decl nil reals nil)
(horizontal_conflict? const-decl "bool" horizontal nil)
(scal_zero formula-decl nil vectors_2D "vectors/")
(add_zero_right formula-decl nil vectors_2D "vectors/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(D formal-const-decl "posreal" cd2d_inf 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_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)
(Delta_gt_0 formula-decl nil horizontal nil)
(real_gt_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)
(sdotv_lt_0 formula-decl nil horizontal nil)
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(sq const-decl "nonneg_real" sq "reals/")
(Sp_vect2 type-eq-decl nil horizontal nil)
(horizontal_conflict_ever formula-decl nil horizontal nil)
(cd2d_inf? const-decl "bool" cd2d_inf nil)
(scal_0 formula-decl nil vectors_2D "vectors/")
(horizontal_tca_los formula-decl nil horizontal nil)
(horizontal_tca const-decl "real" definitions nil)
(s skolem-const-decl "Vect2" cd2d_inf nil)
(sqv_eq_0 formula-decl nil vectors_2D "vectors/")
(sqv_zero formula-decl nil vectors_2D "vectors/")
(dot_zero_right formula-decl nil vectors_2D "vectors/")
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(minus_real_is_real application-judgement "real" reals nil)
(* const-decl "real" vectors_2D "vectors/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(div_mult_pos_neg_ge1 formula-decl nil extra_real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(v skolem-const-decl "Vect2" cd2d_inf nil)
(/= const-decl "boolean" notequal nil))
shostak)))
¤ Dauer der Verarbeitung: 0.26 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.
|
