|
(omega_v2
(omega_v2_generic 0
(omega_v2_generic-1 nil 3476630573
("" (skeep)
(("" (expand "omega_v2")
(("" (lift-if) (("" (replace 1) (("" (propax) nil nil)) nil))
nil))
nil))
nil)
((omega_v2 const-decl "real" omega_v2 nil)) shostak))
(omega_v2_conflict 0
(omega_v2_conflict-1 nil 3476206246
("" (skeep)
(("" (expand "omega_v2")
(("" (lift-if)
(("" (split)
(("1" (flatten)
(("1" (lemma "on_D_conflict")
(("1" (inst?)
(("1" (replace -3)
(("1" (assert) (("1" (ground) nil nil)) nil)) nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (lemma "omega_2D_conflict")
(("2" (inst?)
(("2" (expand "conflict_2D?") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((omega_v2 const-decl "real" omega_v2 nil)
(T formal-const-decl "{AB: posreal | AB > B}" omega_v2 nil)
(B formal-const-decl "nnreal" omega_v2 nil)
(nnreal type-eq-decl nil real_types nil)
(D formal-const-decl "posreal" omega_v2 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)
(on_D_conflict formula-decl nil cd2d nil)
(add_zero_right formula-decl nil vectors_2D "vectors/")
(scal_0 formula-decl nil vectors_2D "vectors/")
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(omega_2D_conflict formula-decl nil omega_2D nil))
shostak))
(omega_v2_2D_eq_0 0
(omega_v2_2D_eq_0-1 nil 3476206331
("" (skeep)
(("" (expand "omega_v2")
(("" (lift-if)
(("" (split)
(("1" (flatten)
(("1" (lemma "line_solution_rewrite")
(("1" (case "v /= zero")
(("1" (inst - "v" "s")
(("1" (ground)
(("1" (hide -2)
(("1" (lemma "line_solution_independence")
(("1" (inst - "s" "v")
(("1" (replace -2)
(("1" (expand "horizontal_conflict_ever?")
(("1"
(inst + "tau_2D(s,v)")
(("1"
(lemma "tau_2D_min")
(("1"
(inst - "s" "0" "v")
(("1"
(expand "horiz_dist_scaf")
(("1"
(assert)
(("1"
(lemma "tau_2D_unique")
(("1"
(inst - "s" "0" "v")
(("1"
(assert)
(("1"
(expand
"horiz_dist_scaf")
(("1"
(assert)
(("1"
(lemma
"tau_2D_def")
(("1"
(inst?)
(("1"
(expand
"horiz_dist_scaf")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst + "0") (("2" (assert) nil nil)) nil))
nil)
("2" (assert) nil nil))
nil)
("2" (flatten)
(("2" (replace -1)
(("2" (lemma "tau_2D_def")
(("2" (inst?)
(("2" (expand "horiz_dist_scaf")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten) nil nil))
nil))
nil))
nil))
nil)
((omega_v2 const-decl "real" omega_v2 nil)
(D formal-const-decl "posreal" omega_v2 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)
(line_solution_rewrite formula-decl nil line_solutions nil)
(dot_zero_right formula-decl nil vectors_2D "vectors/")
(scal_zero 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_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(v skolem-const-decl "Vect2" omega_v2 nil)
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(s skolem-const-decl "Vect2" omega_v2 nil)
(sq const-decl "nonneg_real" sq "reals/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(Sp_vect2 type-eq-decl nil horizontal nil)
(horizontal_conflict_ever? const-decl "bool" horizontal nil)
(tau_2D_min formula-decl nil omega_2D nil)
(horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil)
(tau_2D_unique formula-decl nil omega_2D nil)
(tau_2D_def formula-decl nil omega_2D nil)
(add_zero_right formula-decl nil vectors_2D "vectors/")
(scal_0 formula-decl nil vectors_2D "vectors/")
(real_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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(B formal-const-decl "nnreal" omega_v2 nil)
(T formal-const-decl "{AB: posreal | AB > B}" omega_v2 nil)
(Lookahead type-eq-decl nil Lookahead nil)
(tau_2D const-decl "Lookahead" omega_2D nil)
(line_solution_independence formula-decl nil line_solutions nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/"))
shostak))
(omega_v2_critical_points 0
(omega_v2_critical_points-1 nil 3476206620
("" (skeep)
(("" (expand "omega_v2")
(("" (lift-if)
(("" (split -1)
(("1" (flatten)
(("1" (assert)
(("1" (lemma "line_solution_rewrite")
(("1" (inst?)
(("1" (replace -1)
(("1" (inst + "0") (("1" (assert) nil nil)) nil))
nil)
("2" (flatten)
(("2" (lemma "line_solution_zero")
(("2" (inst - "s") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (lemma "omega_2D.critical_points_2D")
(("2" (inst?)
(("2" (assert)
(("2" (split -1)
(("1" (propax) nil nil)
("2" (expand "circle_solution_2D?")
(("2" (flatten)
(("2" (case "B = 0")
(("1" (replace -1) (("1" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((omega_v2 const-decl "real" omega_v2 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)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(v skolem-const-decl "Vect2" omega_v2 nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(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)
(add_zero_right formula-decl nil vectors_2D "vectors/")
(scal_0 formula-decl nil vectors_2D "vectors/")
(line_solution_zero formula-decl nil line_solutions nil)
(line_solution_rewrite formula-decl nil line_solutions 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" omega_v2 nil)
(T formal-const-decl "{AB: posreal | AB > B}" omega_v2 nil)
(B formal-const-decl "nnreal" omega_v2 nil)
(critical_points_2D formula-decl nil omega_2D nil)
(circle_solution_2D? const-decl "bool" horizontal nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(omega_v2_continuous 0
(omega_v2_continuous-2 "" 3504831504
("" (skeep)
(("" (expand "omega_v2")
(("" (case "sqv(s) = sq(D) AND B = 0")
(("1" (flatten)
(("1" (assert)
(("1" (lemma "dot_cont_vr")
(("1" (inst - "(LAMBDA (v): s)" "(lambda (v): v)")
(("1" (hide -2)
(("1" (expand "continuous_vr?")
(("1" (expand "continuous?")
(("1" (expand "continuous?")
(("1" (skosimp*)
(("1" (inst - "x!1")
(("1" (expand "continuous_at?")
(("1"
(expand "continuous_vr?")
(("1"
(skosimp*)
(("1"
(inst - "epsilon!1")
(("1"
(skosimp*)
(("1"
(inst + "delta!1")
(("1"
(skosimp*)
(("1"
(inst - "y!1")
(("1"
(expand "member")
(("1"
(expand "ball")
(("1"
(rewrite "dist_norm")
(("1"
(case
"norm(y!1-x!1) = norm(x!1-y!1)")
(("1"
(assert)
(("1"
(hide -1)
(("1"
(expand
"real_dist")
(("1"
(hide -2)
(("1"
(grind)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "id_cont_vv") nil nil)
("3" (lemma "const_cont_vv_fun")
(("3" (inst - "s")
(("3" (expand "const_fun") (("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (replace 1)
(("2" (lemma "omega_2D_continuous")
(("2" (hide 1)
(("2" (inst?)
(("2"
(case "omega_2D(s) = (LAMBDA (v): omega_2D(s)(v))")
(("1" (assert) nil nil)
("2" (hide-all-but 1)
(("2" (decompose-equality) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((omega_v2 const-decl "real" omega_v2 nil)
(omega_2D_continuous formula-decl nil omega_2D nil)
(T formal-const-decl "{AB: posreal | AB > B}" omega_v2 nil)
(omega_2D const-decl "real" omega_2D nil)
(dot_cont_vr formula-decl nil vect2_cont_dot "vect_analysis/")
(const_cont_vv_fun formula-decl nil cont_vect2_vect2
"vect_analysis/")
(const_fun const-decl "[Vect2 -> Vect2]" limit_vect2_vect2
"vect_analysis/")
(id_cont_vv formula-decl nil vect_cont_2D "vect_analysis/")
(continuous? const-decl "bool" continuity_ms_def "analysis/")
(continuous_at? const-decl "bool" continuity_ms_def "analysis/")
(member const-decl "bool" sets nil)
(dist_norm formula-decl nil distance_2D "vectors/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_dist const-decl "nnreal" real_metric_space "analysis/")
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(* const-decl "real" vectors_2D "vectors/")
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(minus_real_is_real application-judgement "real" reals nil)
(- const-decl "Vector" vectors_2D "vectors/")
(norm const-decl "nnreal" vectors_2D "vectors/")
(ball const-decl "set[T]" metric_spaces "analysis/")
(continuous_vr? const-decl "bool" cont_vect2_real "vect_analysis/")
(real_minus_real_is_real application-judgement "real" reals nil)
(set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil)
(continuous? const-decl "bool" continuity_ms_def "analysis/")
(continuous_vr? const-decl "bool" cont_vect2_real "vect_analysis/")
(s skolem-const-decl "Vect2" omega_v2 nil)
(continuous_vv? const-decl "bool" cont_vect2_vect2
"vect_analysis/")
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real nonempty-type-from-decl nil reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(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)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sq const-decl "nonneg_real" sq "reals/")
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(D formal-const-decl "posreal" omega_v2 nil)
(B formal-const-decl "nnreal" omega_v2 nil))
shostak)
(omega_v2_continuous-1 nil 3476206812
("" (skeep)
(("" (expand "omega_v2")
(("" (lift-if)
(("" (split)
(("1" (flatten)
(("1" (lemma "dot_cont_vr")
(("1" (inst - "(LAMBDA (v): s)" "(lambda (v): v)")
(("1" (hide -2)
(("1" (expand "continuous_vr?")
(("1" (expand "continuous?")
(("1" (expand "continuous?")
(("1" (skosimp*)
(("1" (inst - "x!1")
(("1" (expand "continuous_at?")
(("1"
(expand "continuous_vr?")
(("1"
(skosimp*)
(("1"
(inst - "epsilon!1")
(("1"
(skosimp*)
(("1"
(inst + "delta!1")
(("1"
(skosimp*)
(("1"
(inst - "y!1")
(("1"
(expand "member")
(("1"
(expand "ball")
(("1"
(rewrite "dist_norm")
(("1"
(case
"norm(y!1-x!1) = norm(x!1-y!1)")
(("1"
(assert)
(("1"
(hide -1)
(("1"
(expand
"real_dist")
(("1"
(hide -2)
(("1"
(grind)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "id_cont_vv") nil nil)
("3" (lemma "const_cont_vv_fun")
(("3" (inst - "s")
(("3" (expand "const_fun") (("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (lemma "omega_2D_continuous")
(("2" (hide 1)
(("2" (inst?)
(("2"
(case "omega_2D(s) = (LAMBDA (v): omega_2D(s)(v))")
(("1" (assert) nil nil)
("2" (hide-all-but 1)
(("2" (decompose-equality) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((omega_2D_continuous formula-decl nil omega_2D nil)
(omega_2D const-decl "real" omega_2D nil)
(dot_cont_vr formula-decl nil vect2_cont_dot "vect_analysis/")
(const_cont_vv_fun formula-decl nil cont_vect2_vect2
"vect_analysis/")
(const_fun const-decl "[Vect2 -> Vect2]" limit_vect2_vect2
"vect_analysis/")
(id_cont_vv formula-decl nil vect_cont_2D "vect_analysis/")
(dist_norm formula-decl nil distance_2D "vectors/")
(real_dist const-decl "nnreal" real_metric_space "analysis/")
(* const-decl "real" vectors_2D "vectors/")
(norm const-decl "nnreal" vectors_2D "vectors/")
(ball const-decl "set[T]" metric_spaces "analysis/")
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(sq const-decl "nonneg_real" sq "reals/"))
nil)))
¤ Dauer der Verarbeitung: 0.35 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
