| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 221 kB |
|
Impressum omega_2D.prfSprache: Lisp |
|||||||||||||||
|
(omega_2D (IMP_metric_space_real_fun_TCC1 0 (IMP_metric_space_real_fun_TCC1-1 nil 3476187108 ("" (lemma "product_is_metric") (("" (propax) nil nil)) nil) ((product_is_metric formula-decl nil cross_metric_spaces "analysis/") (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) (real_dist const-decl "nnreal" real_metric_space "analysis/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (dist const-decl "nnreal" distance_2D "vectors/")) nil)) (IMP_ms_composition_cont_TCC1 0 (IMP_ms_composition_cont_TCC1-1 nil 3476187108 ("" (lemma "vect2_metric_space") (("" (propax) nil nil)) nil) ((vect2_metric_space formula-decl nil vect2_metric_space "vect_analysis/")) nil)) (IMP_ms_composition_cont_TCC2 0 (IMP_ms_composition_cont_TCC2-1 nil 3476187108 ("" (lemma "real_metric_space") (("" (inst?) nil nil)) nil) ((fullset const-decl "set" sets nil) (set type-eq-decl nil sets 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) (real_metric_space formula-decl nil real_metric_space "analysis/")) nil)) (horiz_dist_cont_scaf 0 (horiz_dist_cont_scaf-1 nil 3476187166 ("" (skosimp*) (("" (expand "horiz_dist_scaf") (("" (case "NOT (LAMBDA (t: real, v): sqv(s!1 + t * v) - sq(D)) = ((LAMBDA (t: real, v): sqv(s!1))+((LA (("1" (hide 2) (("1" (expand "+") (("1" (expand "-") (("1" (expand "*") (("1" (decompose-equality) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (hide -1) (("2" (rewrite "diff_continuous[[real,Vect2],d]") (("1" (hide 2) (("1" (rewrite "sum_continuous[[real,Vect2],d]") (("1" (hide 2) (("1" (rewrite "sum_continuous[[real,Vect2],d]") (("1" (hide 2) (("1" (expand "continuous?") (("1" (skeep) (("1" (expand "continuous_at?") (("1" (skosimp*) (("1" (inst + "1") (("1" (skeep) (("1" (expand "member") (("1" (expand "ball") (("1" (expand "real_dist") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "prod_continuous[[real,Vect2],d]") (("1" (hide 2) (("1" (expand "continuous?") (("1" (skosimp*) (("1" (expand "continuous_at?") (("1" (skosimp*) (("1" (inst + "1") (("1" (skeep) (("1" (expand "member") (("1" (expand "ball") (("1" (expand "real_dist") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "prod_continuous[[real,Vect2],d]") (("1" (hide 2) (("1" (expand "continuous?") (("1" (skosimp*) (("1" (expand "continuous_at?") (("1" (skosimp*) (("1" (inst + "epsilon!1") (("1" (skosimp*) (("1" (expand "member") (("1" (expand "ball") (("1" (expand "real_dist") (("1" (expand "d") (("1" (expand "real_dist") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "continuous?") (("2" (skosimp*) (("2" (lemma "dot_cont_vr") (("2" (inst - "(LAMBDA (v): s!1)" "(LAMBDA (v): v)") (("1" (expand "continuous_vr?") (("1" (expand "continuous_at?") (("1" (expand "continuous_vr?") (("1" (inst - "x!1`2") (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1`2") (("1" (expand "member") (("1" (expand "ball") (("1" (expand "real_dist") (("1" (lemma "abs_neg") (("1" (inst?) (("1" (assert) (("1" (expand "d") (("1" (expand "dist") (("1" (lemma "sq_dist_norm") (("1" (inst?) (("1" (lemma "sqrt_eq") (("1" (inst?) (("1" (assert) (("1" (case "norm(x!1`2 - y!1`2) = norm(y!1`2 - x!1`2)") (("1" (assert) 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)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "id_cont_vv_fun") nil nil) ("3" (lemma "const_cont_vv_fun") (("3" (inst - "s!1") (("3" (expand "const_fun") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "prod_continuous[[real,Vect2],d]") (("1" (hide 2) (("1" (case "NOT (LAMBDA (t: real, v): sq(t)) = (LAMBDA (t: real, v): t)*(LAMBDA (t: real, v): t)") (("1" (hide 2) (("1" (expand "*") (("1" (expand "sq") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (hide -1) (("2" (rewrite "prod_continuous[[real,Vect2],d]") (("1" (hide 2) (("1" (grind) nil nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "sqv_cont_vr") (("2" (inst - "(LAMBDA (v): v)") (("1" (expand "continuous?") (("1" (expand "continuous_vr?") (("1" (skosimp*) (("1" (inst - "x!1`2") (("1" (expand "continuous_vr?") (("1" (expand "continuous_at?") (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1`2") (("1" (assert) (("1" (expand "ball") (("1" (expand "real_dist") (("1" (lemma "abs_neg") (("1" (inst?) (("1" (assert) (("1" (expand "d") (("1" (expand "dist") (("1" (lemma "sq_dist_norm") (("1" (inst?) (("1" (lemma "sqrt_eq") (("1" (inst?) (("1" (assert) (("1" (case "norm(x!1`2 - y!1`2) = norm(y!1`2 - x!1`2)") (("1" (assert) 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "id_cont_vv") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sq_nz_pos application-judgement "posreal" sq "reals/") (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (diff_continuous formula-decl nil metric_space_real_fun "analysis/") (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (B formal-const-decl "nnreal" omega_2D nil) (T formal-const-decl "{AB: posreal | AB > B}" omega_2D nil) (Lookahead type-eq-decl nil Lookahead nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (fullset const-decl "set" sets nil) (real_dist const-decl "nnreal" real_metric_space "analysis/") (dist const-decl "nnreal" distance_2D "vectors/") (d const-decl "nnreal" cross_metric_spaces "analysis/") (sum_continuous formula-decl nil metric_space_real_fun "analysis/") (continuous? const-decl "bool" continuity_ms_def "analysis/") (continuous_at? const-decl "bool" continuity_ms_def "analysis/") (member const-decl "bool" sets nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (abs_0 formula-decl nil abs_lems "reals/") (ball const-decl "set[T]" metric_spaces "analysis/") (prod_continuous formula-decl nil metric_space_real_fun "analysis/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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_fun formula-decl nil cont_vect2_vect2 "vect_analysis/") (continuous_vr? const-decl "bool" cont_vect2_real "vect_analysis/") (continuous_vr? const-decl "bool" cont_vect2_real "vect_analysis/") (minus_real_is_real application-judgement "real" reals nil) (sq_dist_norm formula-decl nil distance_2D "vectors/") (sqrt_eq formula-decl nil sqrt "reals/") (sqrt_sq formula-decl nil sqrt "reals/") (sq_dist const-decl "nnreal" distance_2D "vectors/") (norm const-decl "nnreal" vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (abs_neg formula-decl nil abs_lems "reals/") (s!1 skolem-const-decl "Vect2" omega_2D nil) (continuous_vv? const-decl "bool" cont_vect2_vect2 "vect_analysis/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (sqv_cont_vr formula-decl nil vect_cont_2D "vect_analysis/") (id_cont_vv formula-decl nil vect_cont_2D "vect_analysis/") (continuous_vv_fun nonempty-type-eq-decl nil cont_vect2_vect2 "vect_analysis/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (real_plus_real_is_real application-judgement "real" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers 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) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (Vector type-eq-decl nil vectors_2D "vectors/") (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "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_2D nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (* const-decl "real" vectors_2D "vectors/")) nil)) (conflict_2D_on_open_interval 0 (conflict_2D_on_open_interval-1 nil 3476702880 ("" (skeep) (("" (split) (("1" (flatten) (("1" (expand "conflict_2D?") (("1" (skosimp*) (("1" (lemma "horiz_dist_cont_scaf") (("1" (inst - "s") (("1" (expand "continuous?") (("1" (inst - "(t!1,v)") (("1" (expand "continuous_at?") (("1" (inst - "sq(D) - sqv(s+t!1*v)") (("1" (skosimp*) (("1" (expand "member") (("1" (expand "ball") (("1" (expand "real_dist") (("1" (expand "horiz_dist_scaf") (("1" (expand "d") (("1" (expand "real_dist") (("1" (case "t!1 = B") (("1" (replace -1) (("1" (hide -1) (("1" (name "newt" "min(B+delta!1/2,(B+T)/2)") (("1" (case "B < newt AND newt < T") (("1" (flatten) (("1" (inst -4 "(newt,v)") (("1" (assert) (("1" (split -4) (("1" (inst + "newt") (("1" (assert) nil nil)) nil) ("2" (replace -3 :dir rl) (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "extend") (("2" (assert) (("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 :dir rl) (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "t!1 = T") (("1" (replace -1) (("1" (hide -1) (("1" (name "newt" "max(T-delta!1/2,(B+T)/2)") (("1" (case "B < newt AND newt < T") (("1" (flatten) (("1" (inst -4 "(newt,v)") (("1" (assert) (("1" (split -4) (("1" (inst + "newt") (("1" (assert) nil nil)) nil) ("2" (replace -3 :dir rl) (("2" (expand "abs") (("2" (typepred "max(T - delta!1 / 2, (B + T) / 2)") (("2" (name "AA" "max(T - delta!1 / 2, (B + T) / 2)") (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "extend") (("2" (assert) (("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 :dir rl) (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "t!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (expand "extend") (("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (skosimp*) (("2" (expand "conflict_2D?") (("2" (inst + "topen!1") nil nil)) nil)) nil)) nil)) nil)) nil) ((conflict_2D? const-decl "bool" cd2d nil) (horiz_dist_cont_scaf formula-decl nil omega_2D nil) (continuous? const-decl "bool" continuity_ms_def "analysis/") (continuous_at? const-decl "bool" continuity_ms_def "analysis/") (ball const-decl "set[T]" metric_spaces "analysis/") (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (newt skolem-const-decl "{p: real | p >= T - delta!1 / 2 AND p >= (B + T) / 2}" omega_2D nil) (NOT const-decl "[bool -> bool]" booleans nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_min application-judgement "{z: posreal | z <= x AND z <= y}" real_defs nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (dist_eq_args formula-decl nil distance_2D "vectors/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (newt skolem-const-decl "{z: posreal | z <= B + delta!1 / 2 AND z <= (B + T) / 2}" omega_2D nil) (delta!1 skolem-const-decl "posreal" omega_2D nil) (< const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (d const-decl "nnreal" cross_metric_spaces "analysis/") (real_dist const-decl "nnreal" real_metric_space "analysis/") (member const-decl "bool" sets nil) (* const-decl "Vector" vectors_2D "vectors/") (s skolem-const-decl "Vect2" omega_2D nil) (+ const-decl "Vector" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (D formal-const-decl "posreal" omega_2D nil) (sq const-decl "nonneg_real" sq "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_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_gt_is_strict_total_order name-judgement "(strict_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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (B formal-const-decl "nnreal" omega_2D 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) (T formal-const-decl "{AB: posreal | AB > B}" omega_2D nil) (Lookahead type-eq-decl nil Lookahead nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil) (t!1 skolem-const-decl "Lookahead[B, T]" omega_2D nil) (v skolem-const-decl "Vect2" omega_2D nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil)) shostak)) (circle_hit 0 (circle_hit-1 nil 3476190111 ("" (skeep) (("" (name "ep" "M - horiz_dist_scaf(s)(t,v)") (("" (lemma "horiz_dist_cont_scaf") (("" (inst - "s") (("" (expand "continuous?") (("" (inst - "(t,v)") (("1" (expand "continuous_at?") (("1" (inst - "ep") (("1" (skeep -1) (("1" (inst + "delta") (("1" (skeep) (("1" (inst - "(t1,v)") (("1" (expand "member") (("1" (expand "ball") (("1" (expand "d") (("1" (expand "real_dist") (("1" (assert) (("1" (prop) (("1" (name "A1" "horiz_dist_scaf(s)(t,v)") (("1" (replace -1) (("1" (name "B2" "horiz_dist_scaf(s)(t1,v)") (("1" (replace -1) (("1" (hide -1) (("1" (hide -1) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "extend") (("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (expand "extend") (("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Lookahead type-eq-decl nil Lookahead nil) (T formal-const-decl "{AB: posreal | AB > B}" omega_2D nil) (B formal-const-decl "nnreal" omega_2D nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nnreal type-eq-decl nil real_types nil) (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (D formal-const-decl "posreal" omega_2D 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) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil) (t skolem-const-decl "Lookahead[B, T]" omega_2D nil) (v skolem-const-decl "Vect2" omega_2D 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) (ep skolem-const-decl "real" omega_2D nil) (t1 skolem-const-decl "Lookahead[B, T]" omega_2D nil) (ball const-decl "set[T]" metric_spaces "analysis/") (real_dist const-decl "nnreal" real_metric_space "analysis/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_real_is_real application-judgement "real" reals nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (dist_eq_args formula-decl nil distance_2D "vectors/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (d const-decl "nnreal" cross_metric_spaces "analysis/") (member const-decl "bool" sets nil) (continuous_at? const-decl "bool" continuity_ms_def "analysis/") (continuous? const-decl "bool" continuity_ms_def "analysis/") (horiz_dist_cont_scaf formula-decl nil omega_2D nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (horiz_dist_scaf_bounded_below 0 (horiz_dist_scaf_bounded_below-1 nil 3476190147 ("" (skosimp*) (("" (expand "bounded_below?") (("" (inst + "-sq(D)") (("" (skeep) (("" (expand "horiz_dist_scaf") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((bounded_below? const-decl "bool" real_fun_preds "reals/") (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (D formal-const-decl "posreal" omega_2D nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (sq const-decl "nonneg_real" sq "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) nil)) (omega_2D_TCC1 0 (omega_2D_TCC1-1 nil 3476187108 ("" (skeep) (("" (expand "bounded_below?") (("" (inst + "-sq(D)") (("" (skeep) (("" (expand "horiz_dist_scaf") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((bounded_below? const-decl "bool" real_fun_preds "reals/") (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (D formal-const-decl "posreal" omega_2D nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (sq const-decl "nonneg_real" sq "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) nil)) (omega_2D_TCC2 0 (omega_2D_TCC2-1 nil 3476187108 ("" (inst + "B") (("" (assert) nil nil)) nil) ((Lookahead type-eq-decl nil Lookahead nil) (T formal-const-decl "{AB: posreal | AB > B}" omega_2D 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) (B formal-const-decl "nnreal" omega_2D nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (tau_2D_nonempty 0 (tau_2D_nonempty-1 nil 3476190288 ("" (skosimp*) (("" (lemma "curried_min_exists_2D") (("" (inst - "(LAMBDA (t: real, v: Vect2): IF (B<= t AND t <= T) THEN horiz_dist_scaf(s!1)(t,v) ELSE 0 ENDIF)" "B" "T") (("1" (ground) (("1" (inst - "v!1") (("1" (ground) (("1" (hide-all-but (-4 1)) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (skosimp*) (("1" (inst -2 "tmin!1") (("1" (typepred "tmin!1") (("1" (assert) (("1" (expand "omega_2D") (("1" (expand "inf") (("1" (lemma "glb_lem") (("1" (inst -1 "Im(LAMBDA (t: Lookahead): horiz_dist_scaf(s!1)(t, v!1))" "horiz_dist_scaf(s!1)(tmin!1, v!1)") (("1" (assert) (("1" (expand "greatest_lower_bound?") (("1" (hide 2) (("1" (split 1) (("1" (expand "lower_bound?") (("1" (skosimp*) (("1" (typepred "s!2") (("1" (expand "Im" -) (("1" (skosimp*) (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "lower_bound?") (("2" (inst - "horiz_dist_scaf(s!1)(tmin!1, v!1)") (("2" (expand "Im") (("2" (inst + "tmin!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "tmin!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "horiz_dist_cont_scaf") (("2" (inst - "s!1") (("2" (expand "continuous?") (("2" (skosimp*) (("2" (inst - "x!1") (("1" (expand "continuous_at?") (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1") (("1" (assert) (("1" (typepred "y!1") (("1" (expand "extend") (("1" (split -1) (("1" (flatten) (("1" (assert) (("1" (expand "ball") (("1" (expand "real_dist") (("1" (typepred "x!1") (("1" (expand "extend") (("1" (split -1) (("1" (flatten) (("1" (assert) (("1" (expand "horiz_dist_scaf") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "y!1") (("2" (expand "extend") (("2" (ground) (("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "x!1") (("2" (expand "extend") (("2" (ground) (("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((curried_min_exists_2D formula-decl nil vect2_Heine "vect_analysis/") (nonempty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (tmin!1 skolem-const-decl "(LAMBDA (x: real): B <= x AND x <= T)" omega_2D nil) (Lookahead type-eq-decl nil Lookahead nil) (inf const-decl "real" real_fun_supinf "analysis/") (nonempty_image application-judgement "(nonempty?[real])" real_fun_supinf "analysis/") (Im const-decl "setof[real]" real_fun_props "reals/") (setof type-eq-decl nil defined_types nil) (bounded_below? const-decl "bool" bounded_real_defs nil) (set type-eq-decl nil sets nil) (greatest_lower_bound? const-decl "bool" bounded_real_defs nil) (lower_bound? const-decl "bool" bounded_real_defs nil) (v!1 skolem-const-decl "Vect2" omega_2D nil) (s!1 skolem-const-decl "Vect2" omega_2D nil) (glb_lem formula-decl nil bounded_real_defs nil) (omega_2D const-decl "real" omega_2D nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (horiz_dist_cont_scaf formula-decl nil omega_2D nil) (continuous? const-decl "bool" continuity_ms_def "analysis/") (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (fullset const-decl "set" sets nil) (x!1 skolem-const-decl "(extend [[real, Vect2], [(LAMBDA (x: real): B <= x AND x <= T), Vect2], bool, FALSE] (fullset[[(LAMBDA (x: real): B <= x AND x <= T), Vect2]]))" omega_2D nil) (ball const-decl "set[T]" metric_spaces "analysis/") (sq_nz_pos application-judgement "posreal" sq "reals/") (real_dist const-decl "nnreal" real_metric_space "analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (y!1 skolem-const-decl "(extend [[real, Vect2], [(LAMBDA (x: real): B <= x AND x <= T), Vect2], bool, FALSE] (fullset[[(LAMBDA (x: real): B <= x AND x <= T), Vect2]]))" omega_2D nil) (continuous_at? const-decl "bool" continuity_ms_def "analysis/") (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (D formal-const-decl "posreal" omega_2D nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (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) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (B formal-const-decl "nnreal" omega_2D 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) (T formal-const-decl "{AB: posreal | AB > B}" omega_2D nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (tau_2D_TCC1 0 (tau_2D_TCC1-1 nil 3476187108 ("" (skeep) (("" (lemma "tau_2D_nonempty") (("" (inst - "s" "v") nil nil)) nil)) nil) ((tau_2D_nonempty formula-decl nil omega_2D nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil)) nil)) (tau_2D_def 0 (tau_2D_def-1 nil 3476193764 ("" (skeep) (("" (name "ttau" "tau_2D(s,v)") (("" (replace -1) (("" (expand "tau_2D") (("" (typepred "choose({t: Lookahead | horiz_dist_scaf(s)(t, v) = omega_2D(s)(v)})") (("1" (replace -5) (("1" (propax) nil nil)) nil) ("2" (lemma "tau_2D_nonempty") (("2" (inst - "s" "v") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((tau_2D const-decl "Lookahead" omega_2D nil) (Lookahead type-eq-decl nil Lookahead nil) (T formal-const-decl "{AB: posreal | AB > B}" omega_2D 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) (B formal-const-decl "nnreal" omega_2D nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (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) (Vect2 type-eq-decl nil vectors_2D_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) (tau_2D_nonempty formula-decl nil omega_2D nil) (NOT const-decl "[bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (D formal-const-decl "posreal" omega_2D nil) (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (omega_2D const-decl "real" omega_2D nil)) shostak)) (omega_2D_min_rew_TCC1 0 (omega_2D_min_rew_TCC1-1 nil 3476192327 ("" (skeep) (("" (split) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "horiz_dist_scaf(s)(B,v)") (("1" (inst + "B") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "below_bounded") (("2" (inst + "-sq(D)") (("2" (expand "lower_bound") (("2" (skosimp*) (("2" (typepred "z!1") (("2" (skosimp*) (("2" (expand "horiz_dist_scaf") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "ext") (("3" (lemma "tau_2D_nonempty") (("3" (inst - "s" "v") (("3" (expand "nonempty?") (("3" (expand "empty?") (("3" (expand "member") (("3" (skosimp*) (("3" (inst + "x!1") (("3" (replace -1) (("3" (hide -1) (("3" (lemma "inf_def") (("3" (inst?) (("1" (inst - "omega_2D(s)(v)") (("1" (assert) (("1" (hide 2) (("1" (expand "greatest_lower_bound") (("1" (split) (("1" (expand "lower_bound") (("1" (skosimp*) (("1" (typepred "z!1") (("1" (skosimp*) (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (expand "omega_2D") (("1" (expand "inf") (("1" (lemma "glb_is_bound") (("1" (inst?) (("1" (hide 2) (("1" (expand "Im") (("1" (inst + "t!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "lower_bound") (("2" (inst?) (("2" (inst + "tau_2D(s,v)") (("2" (lemma "tau_2D_def") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "horiz_dist_scaf(s)(B,v)") (("1" (inst + "B") nil nil)) nil)) nil)) nil)) nil) ("2" (expand "below_bounded") (("2" (inst + "-sq(D)") (("2" (expand "lower_bound") (("2" (skosimp*) (("2" (typepred "z!1") (("2" (skosimp*) (("2" (expand "horiz_dist_scaf") (("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) ((empty? const-decl "bool" sets 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) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (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_2D nil) (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (nnreal type-eq-decl nil real_types nil) (B formal-const-decl "nnreal" omega_2D nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T formal-const-decl "{AB: posreal | AB > B}" omega_2D nil) (Lookahead type-eq-decl nil Lookahead nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (member const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (sq const-decl "nonneg_real" sq "reals/") (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (lower_bound const-decl "bool" bound_defs "reals/") (sq_nz_pos application-judgement "posreal" sq "reals/") (below_bounded const-decl "bool" bounded_reals "reals/") (tau_2D_nonempty formula-decl nil omega_2D nil) (setof type-eq-decl nil defined_types nil) (v skolem-const-decl "Vect2" omega_2D nil) (s skolem-const-decl "Vect2" omega_2D nil) (set type-eq-decl nil sets nil) (inf_set type-eq-decl nil bounded_reals "reals/") (greatest_lower_bound const-decl "bool" bound_defs "reals/") (tau_2D_def formula-decl nil omega_2D nil) (tau_2D const-decl "Lookahead" omega_2D nil) (glb_is_bound formula-decl nil real_facts "reals/") (t!1 skolem-const-decl "Lookahead[B, T]" omega_2D nil) (bounded_below? const-decl "bool" bounded_real_defs nil) (Im const-decl "setof[real]" real_fun_props "reals/") (nonempty_image application-judgement "(nonempty?[real])" real_fun_supinf "analysis/") (inf const-decl "real" real_fun_supinf "analysis/") (omega_2D const-decl "real" omega_2D nil) (inf_def formula-decl nil bounded_reals "reals/") (ext const-decl "set[real]" bounded_reals "reals/")) nil)) (omega_2D_min_rew 0 (omega_2D_min_rew-2 nil 3477047000 ("" (skeep) (("" (lemma "min_def") (("" (inst - "{r: real | EXISTS (t: Lookahead): horiz_dist_scaf(s)(t, v) = r}" "omega_2D(s)(v)") (("1" (assert) (("1" (hide 2) (("1" (expand "minimum?") (("1" (split) (("1" (lemma "tau_2D_nonempty") (("1" (inst?) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (skosimp*) (("1" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "lower_bound") (("2" (skeep) (("2" (typepred "z") (("2" (skeep -1) (("2" (replace -1 :dir rl) (("2" (hide -1) (("2" (expand "omega_2D") (("2" (expand "inf") (("2" (lemma "glb_is_bound") (("2" (inst?) (("2" (hide 2) (("2" (expand "Im") (("2" (inst + "t") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "curried_min_exists_2D") (("2" (inst - "(LAMBDA (t: real, v: Vect2): horiz_dist_scaf(s)(t,v))" "B" "T") (("1" (split -1) (("1" (inst - "v") (("1" (flatten) (("1" (split 1) (("1" (hide-all-but (-1 1)) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (expand "member") (("1" (skosimp*) (("1" (inst + "t!1") (("1" (assert) nil nil) ("2" (typepred "t!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (expand "below_bounded") (("2" (skosimp*) (("2" (inst + "n!1") (("2" (expand "lower_bound") (("2" (skosimp*) (("2" (inst - "z!1") (("2" (typepred "z!1") (("2" (skosimp*) (("2" (inst + "t!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-3 1)) (("3" (expand "ext") (("3" (skosimp*) (("3" (inst + "t!1") (("1" (case "{r: real | EXISTS (t_1: (LAMBDA (x: real): B <= x AND x <= T)): r = horiz_dist_scaf(s)(t_1, v)} = {r: real | EXISTS (t: Lookahead): horiz_dist_scaf[D](s)(t, v) = r}") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (decompose-equality) (("2" (iff) (("2" (ground) (("1" (skosimp*) (("1" (inst + "t!2") (("1" (assert) nil nil) ("2" (typepred "t!2") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "t!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "t!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "horiz_dist_cont_scaf") (("2" (inst - "s") (("2" (expand "continuous?") (("2" (skosimp*) (("2" (inst - "x!1") (("1" (expand "continuous_at?") (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1") (("1" (assert) (("1" (expand "horiz_dist_scaf") (("1" (propax) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "y!1") (("2" (expand "extend") (("2" (ground) (("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "x!1") (("2" (expand "extend") (("2" (ground) (("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) 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) (min_def formula-decl nil bounded_reals "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (continuous_at? const-decl "bool" continuity_ms_def "analysis/") (y!1 skolem-const-decl "(extend [[real, Vect2], [(LAMBDA (x: real): B <= x AND x <= T), Vect2], bool, FALSE] (fullset[[(LAMBDA (x: real): B <= x AND x <= T), Vect2]]))" omega_2D nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (x!1 skolem-const-decl "(extend [[real, Vect2], [(LAMBDA (x: real): B <= x AND x <= T), Vect2], bool, FALSE] (fullset[[(LAMBDA (x: real): B <= x AND x <= T), Vect2]]))" omega_2D nil) (fullset const-decl "set" sets nil) (extend const-decl "R" extend nil) (FALSE const-decl "bool" booleans nil) (continuous? const-decl "bool" continuity_ms_def "analysis/") (horiz_dist_cont_scaf formula-decl nil omega_2D nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (t!1 skolem-const-decl "(LAMBDA (x: real): B <= x AND x <= T)" omega_2D nil) (z!1 skolem-const-decl "{r: real | EXISTS (t: Lookahead[B, T]): horiz_dist_scaf[D](s)(t, v) = r}" omega_2D nil) (t!1 skolem-const-decl "(LAMBDA (x: real): B <= x AND x <= T)" omega_2D nil) (t!2 skolem-const-decl "(LAMBDA (x: real): B <= x AND x <= T)" omega_2D nil) (curried_min_exists_2D formula-decl nil vect2_Heine "vect_analysis/") (minimum? const-decl "bool" bounded_reals "reals/") (lower_bound const-decl "bool" bound_defs "reals/") (NOT const-decl "[bool -> bool]" booleans nil) (glb_is_bound formula-decl nil real_facts "reals/") (t skolem-const-decl "Lookahead[B, T]" omega_2D nil) (bounded_below? const-decl "bool" bounded_real_defs nil) (Im const-decl "setof[real]" real_fun_props "reals/") (nonempty_image application-judgement "(nonempty?[real])" real_fun_supinf "analysis/") (inf const-decl "real" real_fun_supinf "analysis/") (tau_2D_nonempty formula-decl nil omega_2D nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (omega_2D const-decl "real" omega_2D nil) (min_set type-eq-decl nil bounded_reals "reals/") (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (B formal-const-decl "nnreal" omega_2D 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) (T formal-const-decl "{AB: posreal | AB > B}" omega_2D nil) (Lookahead type-eq-decl nil Lookahead nil) (= const-decl "[T, T -> boolean]" equalities nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (D formal-const-decl "posreal" omega_2D nil) (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (s skolem-const-decl "Vect2" omega_2D nil) (v skolem-const-decl "Vect2" omega_2D nil) (setof type-eq-decl nil defined_types nil) (below_bounded const-decl "bool" bounded_reals "reals/") (inf_set type-eq-decl nil bounded_reals "reals/") (ext const-decl "set[real]" bounded_reals "reals/") (pred type-eq-decl nil defined_types nil) (greatest_lower_bound const-decl "bool" bound_defs "reals/") (inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}" bounded_reals "reals/")) nil) (omega_2D_min_rew-1 nil 3476192327 ("" (skeep) (("" (lemma "min_def") (("" (inst - "{r: real | EXISTS (t: Lookahead): horiz_dist_scaf(s)(t, v) = r}" "omega_2D(s)(v)") (("1" (assert) (("1" (hide 2) (("1" (expand "minimum?") (("1" (split) (("1" (lemma "tau_2D_nonempty") (("1" (inst?) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (skosimp*) (("1" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "lower_bound") (("2" (skeep) (("2" (typepred "z") (("2" (skeep -1) (("2" (replace -1 :dir rl) (("2" (hide -1) (("2" (expand "omega_2D") (("2" (expand "inf") (("2" (lemma "glb_is_bound") (("2" (inst?) (("2" (hide 2) (("2" (expand "Im") (("2" (inst + "t") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "curried_min_exists_2D") (("2" (inst - "(LAMBDA (t: real, v: Vect2): horiz_dist_scaf(s)(t,v))" "B" "T") (("1" (split -1) (("1" (inst - "v") (("1" (flatten) (("1" (split 1) (("1" (hide-all-but (-1 1)) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (expand "member") (("1" (skosimp*) (("1" (inst + "t!1") (("1" (assert) nil nil) ("2" (typepred "t!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (expand "below_bounded") (("2" (skosimp*) (("2" (inst + "n!1") (("2" (expand "lower_bound") (("2" (skosimp*) (("2" (inst - "z!1") (("2" (typepred "z!1") (("2" (skosimp*) (("2" (inst + "t!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-3 1)) (("3" (expand "ext") (("3" (skosimp*) (("3" (inst + "t!1") (("1" (case "{r: real | EXISTS (t_1: (LAMBDA (x: real): B <= x AND x <= T)): r = horiz_dist_scaf(s)(t_1, v)} = {r: real | EXISTS (t: Lookahead[D, B, T]): horiz_dist_scaf[D](s)(t, v) = r}") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (decompose-equality) (("2" (iff) (("2" (ground) (("1" (skosimp*) (("1" (inst + "t!2") (("1" (assert) nil nil) ("2" (typepred "t!2") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "t!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "t!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "horiz_dist_cont_scaf") (("2" (inst - "s") (("2" (expand "continuous?") (("2" (skosimp*) (("2" (inst - "x!1") (("1" (expand "continuous_at?") (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1") (("1" (assert) (("1" (expand "horiz_dist_scaf") (("1" (propax) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "y!1") (("2" (expand "extend") (("2" (ground) (("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "x!1") (("2" (expand "extend") (("2" (ground) (("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((min_def formula-decl nil bounded_reals "reals/") (sq_nz_pos application-judgement "posreal" sq "reals/") (curried_min_exists_2D formula-decl nil vect2_Heine "vect_analysis/") (minimum? const-decl "bool" bounded_reals "reals/") (lower_bound const-decl "bool" bound_defs "reals/") (glb_is_bound formula-decl nil real_facts "reals/") (nonempty_image application-judgement "(nonempty?[real])" real_fun_supinf "analysis/") (inf const-decl "real" real_fun_supinf "analysis/") (min_set type-eq-decl nil bounded_reals "reals/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (below_bounded const-decl "bool" bounded_reals "reals/") (inf_set type-eq-decl nil bounded_reals "reals/") (ext const-decl "set[real]" bounded_reals "reals/") (greatest_lower_bound const-decl "bool" bound_defs "reals/") (inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}" bounded_reals "reals/")) shostak)) (tau_2D_min 0 (tau_2D_min-2 nil 3477047026 ("" (skeep) (("" (lemma "tau_2D_def") (("" (inst?) (("" (replace -1) (("" (hide -1) (("" (rewrite "omega_2D_min_rew") (("" (lemma "min_def") (("" (inst - "{r: real | EXISTS (t: Lookahead): horiz_dist_scaf(s)(t, v) = r}" "omega_2D(s)(v)") (("1" (flatten) (("1" (hide -2) (("1" (split -1) (("1" (expand "minimum?") (("1" (flatten) (("1" (expand "lower_bound") (("1" (inst - "horiz_dist_scaf(s)(t,v)") (("1" (rewrite "omega_2D_min_rew") nil nil) ("2" (inst + "t") nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite "omega_2D_min_rew") nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (inst - "horiz_dist_scaf(s)(T,v)") (("1" (expand "member") (("1" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "below_bounded") (("2" (inst + "-sq(D)") (("2" (expand "lower_bound") (("2" (skosimp*) (("2" (typepred "z!1") (("2" (skosimp*) (("2" (expand "horiz_dist_scaf") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "ext") (("3" (lemma "tau_2D_def") (("3" (inst - "s" "v") (("3" (inst + "tau_2D(s,v)") (("3" (lemma "inf_def") (("3" (inst - "{r: real | EXISTS (t: Lookahead): horiz_dist_scaf[D](s)(t, v) = r}" "horiz_dist_scaf[D](s)(tau_2D(s, v), v)") (("1" (assert) (("1" (hide 2) (("1" (expand "greatest_lower_bound") (("1" (split) (("1" (expand "lower_bound") (("1" (skosimp*) (("1" (typepred "z!1") (("1" (skosimp*) (("1" (expand "omega_2D") (("1" (replace -2) (("1" (replace -1 :dir rl) (("1" (expand "inf") (("1" (lemma "glb_is_bound") (("1" (inst?) (("1" (hide 2) (("1" (expand "Im") (("1" (inst + "t!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "lower_bound") (("2" (inst - "horiz_dist_scaf(s)(tau_2D(s,v),v)") (("2" (inst + "tau_2D(s,v)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "horiz_dist_scaf(s)(tau_2D(s,v),v)") (("1" (inst + "tau_2D(s,v)") nil nil)) nil)) nil)) nil)) nil) ("2" (expand "below_bounded") (("2" (inst + "-sq(D)") (("2" (expand "lower_bound") (("2" (skosimp*) (("2" (typepred "z!1") (("2" (skosimp*) (("2" (expand "horiz_dist_scaf") (("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) ((tau_2D_def formula-decl nil omega_2D nil) (omega_2D_min_rew formula-decl nil omega_2D nil) (inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}" bounded_reals "reals/") (greatest_lower_bound const-decl "bool" bound_defs "reals/") (pred type-eq-decl nil defined_types nil) (ext const-decl "set[real]" bounded_reals "reals/") (inf_set type-eq-decl nil bounded_reals "reals/") (below_bounded const-decl "bool" bounded_reals "reals/") (setof type-eq-decl nil defined_types nil) (v skolem-const-decl "Vect2" omega_2D nil) (s skolem-const-decl "Vect2" omega_2D nil) (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (D formal-const-decl "posreal" omega_2D nil) (= const-decl "[T, T -> boolean]" equalities nil) (Lookahead type-eq-decl nil Lookahead nil) (T formal-const-decl "{AB: posreal | AB > B}" omega_2D 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) (B formal-const-decl "nnreal" omega_2D nil) (<= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (min_set type-eq-decl nil bounded_reals "reals/") (omega_2D const-decl "real" omega_2D nil) (minimum? const-decl "bool" bounded_reals "reals/") (lower_bound const-decl "bool" bound_defs "reals/") (t skolem-const-decl "Lookahead[B, T]" omega_2D nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (sq const-decl "nonneg_real" sq "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (tau_2D const-decl "Lookahead" omega_2D nil) (inf const-decl "real" real_fun_supinf "analysis/") (nonempty_image application-judgement "(nonempty?[real])" real_fun_supinf "analysis/") (Im const-decl "setof[real]" real_fun_props "reals/") (bounded_below? const-decl "bool" bounded_real_defs nil) (t!1 skolem-const-decl "Lookahead[B, T]" omega_2D nil) (glb_is_bound formula-decl nil real_facts "reals/") (inf_def formula-decl nil bounded_reals "reals/") (min_def formula-decl nil bounded_reals "reals/") (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) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil)) nil) (tau_2D_min-1 nil 3476193869 ("" (skeep) (("" (lemma "tau_2D_def") (("" (inst?) (("" (replace -1) (("" (hide -1) (("" (rewrite "omega_2D_min_rew") (("" (lemma "min_def") (("" (inst - "{r: real | EXISTS (t: Lookahead): horiz_dist_scaf(s)(t, v) = r}" "omega_2D(s)(v)") (("1" (flatten) (("1" (hide -2) (("1" (split -1) (("1" (expand "minimum?") (("1" (flatten) (("1" (expand "lower_bound") (("1" (inst - "horiz_dist_scaf(s)(t,v)") (("1" (rewrite "omega_2D_min_rew") nil nil) ("2" (inst + "t") nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite "omega_2D_min_rew") nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (inst - "horiz_dist_scaf(s)(T,v)") (("1" (expand "member") (("1" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "below_bounded") (("2" (inst + "-sq(D)") (("2" (expand "lower_bound") (("2" (skosimp*) (("2" (typepred "z!1") (("2" (skosimp*) (("2" (expand "horiz_dist_scaf") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "ext") (("3" (lemma "tau_2D_def") (("3" (inst - "s" "v") (("3" (inst + "tau_2D(s,v)") (("3" (lemma "inf_def") (("3" (inst - "{r: real | EXISTS (t: Lookahead[D, B, T]): horiz_dist_scaf[D](s)(t, v) = r}" "horiz_dist_scaf[D](s)(tau_2D(s, v), v)") (("1" (assert) (("1" (hide 2) (("1" (expand "greatest_lower_bound") (("1" (split) (("1" (expand "lower_bound") (("1" (skosimp*) (("1" (typepred "z!1") (("1" (skosimp*) (("1" (expand "omega_2D") (("1" (replace -2) (("1" (replace -1 :dir rl) (("1" (expand "inf") (("1" (lemma "glb_is_bound") (("1" (inst?) (("1" (hide 2) (("1" (expand "Im") (("1" (inst + "t!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "lower_bound") (("2" (inst - "horiz_dist_scaf(s)(tau_2D(s,v),v)") (("2" (inst + "tau_2D(s,v)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "horiz_dist_scaf(s)(tau_2D(s,v),v)") (("1" (inst + "tau_2D(s,v)") nil nil)) nil)) nil)) nil)) nil) ("2" (expand "below_bounded") (("2" (inst + "-sq(D)") (("2" (expand "lower_bound") (("2" (skosimp*) (("2" (typepred "z!1") (("2" (skosimp*) (("2" (expand "horiz_dist_scaf") (("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) ((inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}" bounded_reals "reals/") (greatest_lower_bound const-decl "bool" bound_defs "reals/") (ext const-decl "set[real]" bounded_reals "reals/") (inf_set type-eq-decl nil bounded_reals "reals/") (below_bounded const-decl "bool" bounded_reals "reals/") (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (min_set type-eq-decl nil bounded_reals "reals/") (minimum? const-decl "bool" bounded_reals "reals/") (lower_bound const-decl "bool" bound_defs "reals/") (sq const-decl "nonneg_real" sq "reals/") (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (sq_nz_pos application-judgement "posreal" sq "reals/") (inf const-decl "real" real_fun_supinf "analysis/") (nonempty_image application-judgement "(nonempty?[real])" real_fun_supinf "analysis/") (glb_is_bound formula-decl nil real_facts "reals/") (inf_def formula-decl nil bounded_reals "reals/") (min_def formula-decl nil bounded_reals "reals/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/")) shostak)) (omega_2D_continuous 0 (omega_2D_continuous-1 nil 3476191109 ("" (skosimp*) (("" (lemma "curried_min_is_cont_2D") (("" (inst - "(LAMBDA (t: real, v: Vect2): IF (B <= t AND t <= T) THEN horiz_dist_scaf(s!1)(t,v) ELSE 0 ENDIF)" "B" "T") (("1" (ground) (("1" (expand "continuous?") (("1" (expand "continuous?") (("1" (expand "continuous_at?") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1") (("1" (expand "member") (("1" (expand "ball") (("1" (lemma "omega_2D_min_rew") (("1" (inst-cp - "s!1" "x!1") (("1" (inst - "s!1" "y!1") (("1" (assert) (("1" (case "{r: real | EXISTS (t: Lookahead): horiz_dist_scaf(s!1)(t, y!1) = r} = {r: real | EXISTS (t_1: (LAMBDA (x: real): B <= x AND x <= T)): r = horiz_dist_scaf(s!1)(t_1, y!1)} AND {r: real | EXISTS (t: Lookahead): horiz_dist_scaf(s!1)(t, x!1) = r} = {r: real | EXISTS (t_1: (LAMBDA (x: real): B <= x AND x <= T)): r = horiz_dist_scaf(s!1)(t_1, x!1)}") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (split) (("1" (decompose-equality) (("1" (iff) (("1" (ground) (("1" (skosimp*) (("1" (inst + "t!1") (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "t!1") (("1" (assert) nil nil) ("2" (typepred "t!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (decompose-equality) (("2" (iff) (("2" (ground) (("1" (skosimp*) (("1" (inst + "t!1") (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "t!1") (("1" (assert) nil nil) ("2" (typepred "t!1") (("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) ("2" (hide 2) (("2" (lemma "horiz_dist_cont_scaf") (("2" (inst - "s!1") (("2" (expand "continuous?") (("2" (skosimp*) (("2" (inst - "x!1") (("1" (expand "continuous_at?") (("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" (typepred "y!1") (("1" (expand "extend") (("1" (ground -1) (("1" (typepred "x!1") (("1" (expand "extend") (("1" (ground -1) (("1" (expand "horiz_dist_scaf") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "y!1") (("2" (expand "extend") (("2" (ground) (("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "x!1") (("2" (expand "extend") (("2" (ground) (("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((curried_min_is_cont_2D formula-decl nil vect2_Heine "vect_analysis/") (continuous? const-decl "bool" continuity_ms_def "analysis/") (ball const-decl "set[T]" metric_spaces "analysis/") (t!1 skolem-const-decl "(LAMBDA (x: real): B <= x AND x <= T)" omega_2D nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (t!1 skolem-const-decl "(LAMBDA (x: real): B <= x AND x <= T)" omega_2D nil) (NOT const-decl "[bool -> bool]" booleans nil) (Lookahead type-eq-decl nil Lookahead nil) (= const-decl "[T, T -> boolean]" equalities nil) (omega_2D_min_rew formula-decl nil omega_2D nil) (member const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil) (continuous_at? const-decl "bool" continuity_ms_def "analysis/") (continuous? const-decl "bool" continuity_ms_def "analysis/") (horiz_dist_cont_scaf formula-decl nil omega_2D nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (x!1 skolem-const-decl "(extend [[real, Vect2], [(LAMBDA (x: real): B <= x AND x <= T), Vect2], bool, FALSE] (fullset[[(LAMBDA (x: real): B <= x AND x <= T), Vect2]]))" omega_2D nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (y!1 skolem-const-decl "(extend [[real, Vect2], [(LAMBDA (x: real): B <= x AND x <= T), Vect2], bool, FALSE] (fullset[[(LAMBDA (x: real): B <= x AND x <= T), Vect2]]))" omega_2D nil) (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (D formal-const-decl "posreal" omega_2D nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (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) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (B formal-const-decl "nnreal" omega_2D 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) (T formal-const-decl "{AB: posreal | AB > B}" omega_2D nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (tau_2D_unique 0 (tau_2D_unique-1 nil 3476195872 ("" (skeep) (("" (lemma "horiz_dist_strictly_convex_scaf") (("" (inst - "s" "v") (("" (assert) (("" (lemma "strictly_convex_btw_pt_lt") (("" (case "tau_2D(s,v) < t") (("1" (inst - "tau_2D(s,v)" "t" "horiz_dist_scaf(s)(tau_2D(s,v),v)" "LAMBDA (ttt): horiz_dist_scaf(s)(ttt, v)" "(1/2)*tau_2D(s,v) + (1/2)*t") (("1" (assert) (("1" (lemma "tau_2D_min") (("1" (inst - "s" "(1 / 2) * tau_2D(s, v) + (1 / 2) * t" "v") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst - "t" "tau_2D(s,v)" "horiz_dist_scaf(s)(tau_2D(s,v),v)" "LAMBDA (ttt): horiz_dist_scaf(s)(ttt, v)" "(1/2)*tau_2D(s,v) + (1/2)*t") (("2" (assert) (("2" (lemma "tau_2D_min") (("2" (inst - "s" "(1 / 2) * tau_2D(s, v) + (1 / 2) * t" "v") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((D formal-const-decl "posreal" omega_2D 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) (horiz_dist_strictly_convex_scaf formula-decl nil horizontal_dist_convexity nil) (tau_2D const-decl "Lookahead" omega_2D nil) (Lookahead type-eq-decl nil Lookahead nil) (T formal-const-decl "{AB: posreal | AB > B}" omega_2D nil) (B formal-const-decl "nnreal" omega_2D nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nnreal type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (tau_2D_min formula-decl nil omega_2D nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal 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) (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (strictly_convex_btw_pt_lt formula-decl nil convex_functions "reals/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/")) shostak)) (tau_2D_connected 0 (tau_2D_connected-1 nil 3476196677 ("" (skeep) (("" (lemma "tau_2D_unique") (("" (inst - "s" "t" "v") (("" (assert) (("" (split -1) (("1" (skeep) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (replace -1) (("2" (expand "horiz_dist_scaf") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((tau_2D_unique formula-decl nil omega_2D nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (add_zero_right formula-decl nil vectors_2D "vectors/") (scal_zero formula-decl nil vectors_2D "vectors/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (Lookahead type-eq-decl nil Lookahead nil) (T formal-const-decl "{AB: posreal | AB > B}" omega_2D 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) (B formal-const-decl "nnreal" omega_2D nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil)) shostak)) (tau_2D_v2 0 (tau_2D_v2-1 nil 3476551724 ("" (skeep) (("" (lemma "horizontal_omega_min") (("" (inst - "v" "s" "tau_2D(s,v)") (("" (lemma "tau_2D_min") (("" (expand "horizontal_omega") (("" (expand "horiz_dist_scaf") (("" (inst - "s" "tau_v2(s,v)" "v") (("" (lemma "tau_2D_unique") (("" (inst?) (("" (expand "horiz_dist_scaf") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-const-decl "{AB: posreal | AB > B}" omega_2D nil) (B formal-const-decl "nnreal" omega_2D nil) (nnreal type-eq-decl nil real_types nil) (D formal-const-decl "posreal" omega_2D 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) (horizontal_omega_min formula-decl nil cd2d nil) (tau_2D_min formula-decl nil omega_2D nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (tau_2D_unique formula-decl nil omega_2D nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (tau_v2 const-decl "Lookahead" cd2d nil) (horizontal_omega const-decl "nnreal" cd2d nil) (tau_2D const-decl "Lookahead" omega_2D nil) (Lookahead type-eq-decl nil Lookahead nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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/")) nil)) (omega_2D_horizontal_omega 0 (omega_2D_horizontal_omega-1 nil 3476551686 ("" (skeep) (("" (lemma "tau_2D_v2") (("" (inst - "s" "v") (("" (expand "horizontal_omega") (("" (lemma "tau_2D_def") (("" (inst?) (("" (expand "horiz_dist_scaf") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((tau_2D_v2 formula-decl nil omega_2D nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (horizontal_omega const-decl "nnreal" cd2d nil) (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (tau_2D_def formula-decl nil omega_2D nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil)) shostak)) (omega_2D_conflict 0 (omega_2D_conflict-1 nil 3476199173 ("" (skeep) (("" (ground) (("1" (expand "conflict_2D?") (("1" (inst + "tau_2D(s,v)") (("1" (lemma "tau_2D_def") (("1" (inst?) (("1" (expand "horiz_dist_scaf") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "conflict_2D?") (("2" (skosimp*) (("2" (lemma "tau_2D_def") (("2" (inst?) (("2" (lemma "tau_2D_min") (("2" (inst - "s" "t!1" "v") (("2" (expand "horiz_dist_scaf") (("2" (assert) nil 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) (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) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (B formal-const-decl "nnreal" omega_2D 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) (T formal-const-decl "{AB: posreal | AB > B}" omega_2D nil) (Lookahead type-eq-decl nil Lookahead nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (tau_2D const-decl "Lookahead" omega_2D nil) (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (tau_2D_def formula-decl nil omega_2D nil) (conflict_2D? const-decl "bool" cd2d nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (tau_2D_min formula-decl nil omega_2D nil)) shostak)) (omega_2D_eq_0 0 (omega_2D_eq_0-1 nil 3476199315 ("" (skeep) (("" (lemma "tau_2D_def") (("" (inst?) (("" (expand "horiz_dist_scaf") (("" (ground) nil nil)) nil)) nil)) nil)) nil) ((tau_2D_def formula-decl nil omega_2D nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (real_minus_real_is_real application-judgement "real" reals nil) (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil)) shostak)) (parts_of_v_nonzero_2D 0 (parts_of_v_nonzero_2D-1 nil 3476199361 ("" (skeep) (("" (lemma "tau_2D_def") (("" (inst?) (("" (expand "horiz_dist_scaf") (("" (replace -3) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((tau_2D_def formula-decl nil omega_2D nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (scal_zero formula-decl nil vectors_2D "vectors/") (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/") (real_minus_real_is_real application-judgement "real" reals nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil)) shostak)) (lower_circle_hit_solution 0 (lower_circle_hit_solution-2 nil 3476627083 ("" (skeep) (("" (expand "circle_solution_2D?") (("" (assert) (("" (case "v = zero") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (case "B >= -(s * v)/sqv(v)") (("1" (lemma "dot_add_left") (("1" (inst - "v" "s" "B*v") (("1" (replace -1) (("1" (hide -1) (("1" (neg-formula -1) (("1" (cross-mult -1) (("1" (split -1) (("1" (flatten) (("1" (hide-all-but (-2 2)) (("1" (grind) nil nil)) nil)) nil) ("2" (flatten) (("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "quad_min_mono_dec") (("2" (inst - "sqv(v)" "2*(s*v)" "sqv(s)" "B" "min(-(s*v)/sqv(v),T)") (("2" (assert) (("2" (split -1) (("1" (name "mymin" "min(-(s * v) / sqv(v), T)") (("1" (replace -1) (("1" (lemma "tau_2D_min") (("1" (inst - "s" "mymin" "v") (("1" (case "tau_2D(s,v) = B") (("1" (replace -1) (("1" (expand "quadratic") (("1" (expand "horiz_dist_scaf") (("1" (rewrite "sqv_add") (("1" (rewrite "sqv_add") (("1" (rewrite "sqv_scal") (("1" (rewrite "sqv_scal") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "tau_2D_def") (("2" (inst - "s" "v") (("2" (expand "horiz_dist_scaf") (("2" (lemma "tau_2D_unique") (("2" (inst - "s" "B" "v") (("2" (assert) (("2" (expand "horiz_dist_scaf") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "min") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil) ("3" (expand "min") (("3" (lift-if) (("3" (ground) nil nil)) nil)) nil) ("4" (expand "min") (("4" (lift-if) (("4" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "sqv_eq_0") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((circle_solution_2D? const-decl "bool" horizontal 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) (scal_zero formula-decl nil vectors_2D "vectors/") (add_zero_right formula-decl nil vectors_2D "vectors/") (dot_zero_right formula-decl nil vectors_2D "vectors/") (real_times_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (quad_min_mono_dec formula-decl nil quad_minmax "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (tau_2D_min formula-decl nil omega_2D nil) (tau_2D const-decl "Lookahead" omega_2D nil) (quadratic const-decl "real" quadratic "reals/") (sqv_add formula-decl nil vectors_2D "vectors/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (dot_scal_canon formula-decl nil vectors_2D "vectors/") (sqv_scal formula-decl nil vectors_2D "vectors/") (real_minus_real_is_real application-judgement "real" reals 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) (Lookahead type-eq-decl nil Lookahead nil) (mymin skolem-const-decl "{p: real | p <= -(s * v) / sqv(v) AND p <= T}" omega_2D nil) (v skolem-const-decl "Vect2" omega_2D nil) (s skolem-const-decl "Vect2" omega_2D nil) (T formal-const-decl "{AB: posreal | AB > B}" omega_2D 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) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (dot_add_left formula-decl nil vectors_2D "vectors/") (minus_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (mult_neg formula-decl nil extra_tegies nil) (neg_neg formula-decl nil extra_tegies nil) (neg_div formula-decl nil extra_tegies nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (both_sides_times_neg_ge1_imp formula-decl nil extra_real_props nil) (<= const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (real_plus_real_is_real application-judgement "real" reals nil) (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (dot_scal_left formula-decl nil vectors_2D "vectors/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_mult_pos_neg_ge1 formula-decl nil extra_real_props nil) (* const-decl "Vector" vectors_2D "vectors/") (real_div_nzreal_is_real application-judgement "real" reals nil) (number nonempty-type-decl nil numbers 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (B formal-const-decl "nnreal" omega_2D nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (* const-decl "real" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (sq_nz_pos application-judgement "posreal" sq "reals/")) nil) (lower_circle_hit_solution-1 nil 3476625094 ("" (skeep) (("" (expand "circle_solution_2D?") (("" (assert) (("" (postpone) nil nil)) nil)) nil)) nil) nil shostak)) (circle_hit_solution 0 (circle_hit_solution-2 "" 3504844495 ("" (skeep) (("" (case "not sqv(s) >= sq(D)") (("1" (lemma "tau_2D_def") (("1" (inst?) (("1" (replace -2) (("1" (expand "horiz_dist_scaf") (("1" (case "tau_2D(s,v) > B") (("1" (lemma "strictly_convex_btw_pt_lt") (("1" (lemma "horiz_dist_strictly_convex_scaf") (("1" (inst -2 "0" "tau_2D(s,v)" "0" "LAMBDA (trt:real): horiz_dist_scaf(s)(trt, v)" "B") (("1" (inst - "s" "v") (("1" (assert) (("1" (hide -1) (("1" (case "B = 0") (("1" (replace -1) (("1" (lemma "tau_2D_min") (("1" (inst - "s" "B" "v") (("1" (expand "horiz_dist_scaf") (("1" (replace -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "horiz_dist_scaf") (("2" (assert) (("2" (lemma "tau_2D_min") (("2" (inst - "s" "B" "v") (("2" (expand "horiz_dist_scaf") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "line_solution_rewrite") (("2" (inst?) (("2" (replace -1) (("2" (hide -1) (("2" (lemma "tau_2D_def") (("2" (inst?) (("2" (inst + "tau_2D(s,v)") (("2" (expand "horiz_dist_scaf") (("2" (assert) (("2" (lemma "tau_2D_v2") (("2" (inst?) (("2" (assert) (("2" (expand "tau_v2") (("2" (expand "min") (("2" (expand "max") (("2" (lift-if) (("2" (lift-if) (("2" (ground) (("1" (expand "horizontal_tca") (("1" (real-props) (("1" (lemma "dot_add_left") (("1" (inst - "v" "s" "T*v") (("1" (expand "circle_solution_2D?") (("1" (replace -1) (("1" (neg-formula -2) (("1" (cross-mult -2) (("1" (split -2) (("1" (flatten) (("1" (hide-all-but (-2 4)) (("1" (grind) nil nil)) nil)) nil) ("2" (flatten) (("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "horizontal_tca") (("2" (replace -1) (("2" (expand "sqv") (("2" (rewrite "dot_add_left") (("2" (rewrite "dot_add_left") (("2" (rewrite "dot_add_left") (("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) ((D formal-const-decl "posreal" omega_2D nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (sq const-decl "nonneg_real" sq "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (Vector type-eq-decl nil vectors_2D "vectors/") (>= const-decl "bool" reals 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (strictly_convex_btw_pt_lt formula-decl nil convex_functions "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (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) (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (tau_2D_min formula-decl nil omega_2D nil) (scal_0 formula-decl nil vectors_2D "vectors/") (add_zero_right formula-decl nil vectors_2D "vectors/") (horiz_dist_strictly_convex_scaf formula-decl nil horizontal_dist_convexity nil) (tau_2D const-decl "Lookahead" omega_2D nil) (Lookahead type-eq-decl nil Lookahead nil) (T formal-const-decl "{AB: posreal | AB > B}" omega_2D nil) (B formal-const-decl "nnreal" omega_2D nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (tau_2D_def formula-decl nil omega_2D nil) (line_solution_rewrite formula-decl nil line_solutions nil) (tau_v2 const-decl "Lookahead" cd2d nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (+ const-decl "Vector" vectors_2D "vectors/") (horizontal_tca const-decl "real" definitions nil) (dot_add_left formula-decl nil vectors_2D "vectors/") (circle_solution_2D? const-decl "bool" horizontal nil) (neg_neg formula-decl nil extra_tegies nil) (neg_div formula-decl nil extra_tegies nil) (mult_neg formula-decl nil extra_tegies nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (both_sides_times_neg_gt1 formula-decl nil real_props nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (negreal nonempty-type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (* const-decl "real" vectors_2D "vectors/") (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (real_plus_real_is_real application-judgement "real" reals nil) (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (dot_scal_left formula-decl nil vectors_2D "vectors/") (nonzero_real nonempty-type-eq-decl nil reals nil) (div_mult_pos_neg_gt2 formula-decl nil extra_real_props nil) (* const-decl "Vector" vectors_2D "vectors/") (minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (tau_2D_v2 formula-decl nil omega_2D nil) (/= const-decl "boolean" notequal nil) (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (Sp_vect2 type-eq-decl nil horizontal nil)) shostak) (circle_hit_solution-1 nil 3476199571 ("" (skeep) (("" (case "not sqv(s) >= sq(D)") (("1" (lemma "tau_2D_def") (("1" (inst?) (("1" (replace -2) (("1" (expand "horiz_dist_scaf") (("1" (case "tau_2D(s,v) > B") (("1" (lemma "strictly_convex_btw_pt_lt") (("1" (lemma "horiz_dist_strictly_convex_scaf") (("1" (inst -2 "0" "tau_2D(s,v)" "0" "LAMBDA (trt:real): horiz_dist_scaf(s)(trt, v)" "B") (("1" (inst - "s" "v") (("1" (assert) (("1" (hide -1) (("1" (case "B = 0") (("1" (replace -1) (("1" (lemma "tau_2D_min") (("1" (inst - "s" "B" "v") (("1" (expand "horiz_dist_scaf") (("1" (replace -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "horiz_dist_scaf") (("2" (assert) (("2" (lemma "tau_2D_min") (("2" (inst - "s" "B" "v") (("2" (expand "horiz_dist_scaf") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "line_solution_rewrite") (("2" (inst?) (("2" (replace -1) (("2" (hide -1) (("2" (lemma "tau_2D_def") (("2" (inst?) (("2" (inst + "tau_2D(s,v)") (("2" (expand "horiz_dist_scaf") (("2" (assert) (("2" (lemma "tau_2D_v2") (("2" (inst?) (("2" (assert) (("2" (expand "tau_v2") (("2" (expand "min") (("2" (expand "max") (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (ground) (("1" (expand "horizontal_tca") (("1" (real-props) (("1" (lemma "dot_add_left") (("1" (inst - "v" "s" "T*v") (("1" (expand "circle_solution_2D?") (("1" (replace -1) (("1" (neg-formula -4) (("1" (cross-mult -4) (("1" (split -4) (("1" (flatten) (("1" (hide-all-but (-2 5)) (("1" (grind) nil nil)) nil)) nil) ("2" (flatten) (("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "horizontal_tca") (("2" (replace -2) (("2" (expand "sqv") (("2" (rewrite "dot_add_left") (("2" (rewrite "dot_add_left") (("2" (rewrite "dot_add_left") (("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) ((sq const-decl "nonneg_real" sq "reals/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (sq_nz_pos application-judgement "posreal" sq "reals/") (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (strictly_convex_btw_pt_lt formula-decl nil convex_functions "reals/") (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (scal_0 formula-decl nil vectors_2D "vectors/") (add_zero_right formula-decl nil vectors_2D "vectors/") (horiz_dist_strictly_convex_scaf formula-decl nil horizontal_dist_convexity nil) (Lookahead type-eq-decl nil Lookahead nil) (line_solution_rewrite formula-decl nil line_solutions nil) (tau_v2 const-decl "Lookahead" cd2d nil) (+ const-decl "Vector" vectors_2D "vectors/") (horizontal_tca const-decl "real" definitions nil) (dot_add_left formula-decl nil vectors_2D "vectors/") (circle_solution_2D? const-decl "bool" horizontal nil) (* const-decl "real" vectors_2D "vectors/") (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (dot_scal_left formula-decl nil vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (Sp_vect2 type-eq-decl nil horizontal nil)) shostak)) (no_horiz_speed_on_D 0 (no_horiz_speed_on_D-1 nil 3476204083 ("" (skeep) (("" (lemma "tau_2D_def") (("" (inst?) (("" (expand "horiz_dist_scaf") (("" (replace -3) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((tau_2D_def formula-decl nil omega_2D nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (scal_zero formula-decl nil vectors_2D "vectors/") (add_zero_right formula-decl nil vectors_2D "vectors/") (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil)) shostak)) (omega_2D_Delta 0 (omega_2D_Delta-1 nil 3476204118 ("" (skeep) (("" (case "v = zero") (("1" (replace -1) (("1" (expand "Delta") (("1" (assert) (("1" (expand "det") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "Delta_ge_0_2") (("2" (inst - "v" "s") (("1" (assert) (("1" (inst + "tau_2D(s,v)") (("1" (lemma "tau_2D_def") (("1" (inst?) (("1" (expand "horiz_dist_scaf") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) 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) (sq_nz_pos application-judgement "posreal" sq "reals/") (Delta const-decl "real" horizontal nil) (real_times_real_is_real application-judgement "real" reals nil) (det const-decl "real" det_2D "vectors/") (sq_0 formula-decl nil sq "reals/") (comp_zero_x formula-decl nil vectors_2D "vectors/") (comp_zero_y formula-decl nil vectors_2D "vectors/") (sqv_zero formula-decl nil vectors_2D "vectors/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (/= const-decl "boolean" notequal nil) (v skolem-const-decl "Vect2" omega_2D nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (tau_2D const-decl "Lookahead" omega_2D nil) (Lookahead type-eq-decl nil Lookahead nil) (T formal-const-decl "{AB: posreal | AB > B}" omega_2D nil) (B formal-const-decl "nnreal" omega_2D nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nnreal type-eq-decl nil real_types nil) (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (tau_2D_def formula-decl nil omega_2D nil) (Delta_ge_0_2 formula-decl nil horizontal nil) (number nonempty-type-decl nil numbers 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) (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_2D nil)) shostak)) (Theta_Ds_equal_line_sol_2D_TCC1 0 (Theta_Ds_equal_line_sol_2D_TCC1-1 nil 3476187108 ("" (skeep) (("" (lemma "tau_2D_def") (("" (inst?) (("" (expand "horiz_dist_scaf") (("" (case "v = zero") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (lemma "Delta_ge_0") (("2" (inst - "v" "s") (("2" (assert) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((tau_2D_def formula-decl nil omega_2D nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (tau_2D const-decl "Lookahead" omega_2D nil) (Lookahead type-eq-decl nil Lookahead nil) (T formal-const-decl "{AB: posreal | AB > B}" omega_2D nil) (B formal-const-decl "nnreal" omega_2D nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nnreal type-eq-decl nil real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (Delta_ge_0 formula-decl nil horizontal nil) (number nonempty-type-decl nil numbers 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) (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_2D nil) (real_minus_real_is_real application-judgement "real" reals nil) (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (add_zero_right formula-decl nil vectors_2D "vectors/") (scal_zero formula-decl nil vectors_2D "vectors/") (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (Vector type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil)) nil)) (Theta_Ds_equal_line_sol_2D_TCC2 0 (Theta_Ds_equal_line_sol_2D_TCC2-1 nil 3476187108 ("" (subtype-tcc) nil nil) ((real_div_nzreal_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonempty_image application-judgement "(nonempty?[real])" real_fun_supinf "analysis/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (* const-decl "real" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (discr2b const-decl "real" quadratic_2b "reals/") (root2b const-decl "real" quadratic_2b "reals/") (D formal-const-decl "posreal" omega_2D 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) (Theta_D const-decl "real" horizontal nil) (* const-decl "Vector" vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (inf const-decl "real" real_fun_supinf "analysis/") (omega_2D const-decl "real" omega_2D nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types 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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) nil)) (Theta_Ds_equal_line_sol_2D 0 (Theta_Ds_equal_line_sol_2D-1 nil 3476204263 ("" (skeep) (("" (lemma "Theta_D_lt") (("" (inst?) (("" (lemma "omega_2D_Delta") (("" (inst?) (("" (assert) (("" (expand "line_solution?") (("" (lemma "Delta_zero_eps_line_equality") (("" (inst - "v" "s") (("" (assert) (("" (case "v = zero") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (split -1) (("1" (propax) nil nil) ("2" (lemma "dot_nneg_divergent") (("2" (inst - "v" "s") (("2" (assert) (("2" (expand "divergent?") (("2" (inst - "tau_2D(s,v)") (("1" (assert) (("1" (expand "dist") (("1" (lemma "sq_lt") (("1" (inst?) (("1" (assert) (("1" (rewrite "sq_dist_norm") (("1" (rewrite "sq_dist_norm") (("1" (rewrite "sqrt_sqv_norm" :dir rl) (("1" (rewrite "sqrt_sqv_norm" :dir rl) (("1" (rewrite "sq_sqrt") (("1" (rewrite "sq_sqrt") (("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)) nil)) nil)) nil)) nil) ("2" (lemma "tau_2D_def") (("2" (inst?) (("2" (expand "horiz_dist_scaf") (("2" (case "tau_2D(s,v) = 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((D formal-const-decl "posreal" omega_2D 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) (Theta_D_lt formula-decl nil horizontal nil) (omega_2D_Delta formula-decl nil omega_2D nil) (real_le_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/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Delta_zero_eps_line_equality formula-decl nil horizontal_criteria nil) (divergent? const-decl "bool" closest_approach_2D "vectors/") (scal_0 formula-decl nil vectors_2D "vectors/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (scal_zero formula-decl nil vectors_2D "vectors/") (add_zero_right formula-decl nil vectors_2D "vectors/") (sq_lt formula-decl nil sq "reals/") (sq_sqrt formula-decl nil sqrt "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (tau_2D_def formula-decl nil omega_2D nil) (sqrt_sqv_norm formula-decl nil vectors_2D "vectors/") (sub_zero_right formula-decl nil vectors_2D "vectors/") (sq_dist_norm formula-decl nil distance_2D "vectors/") (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (sq_dist const-decl "nnreal" distance_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (dist const-decl "nnreal" distance_2D "vectors/") (v skolem-const-decl "Vect2" omega_2D nil) (s skolem-const-decl "Vect2" omega_2D nil) (tau_2D const-decl "Lookahead" omega_2D nil) (Lookahead type-eq-decl nil Lookahead nil) (T formal-const-decl "{AB: posreal | AB > B}" omega_2D nil) (B formal-const-decl "nnreal" omega_2D nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (dot_nneg_divergent formula-decl nil definitions nil) (dot_zero_right formula-decl nil vectors_2D "vectors/") (= const-decl "[T, T -> boolean]" equalities 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/") (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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (line_solution? const-decl "bool" line_solutions nil) (real_times_real_is_real application-judgement "real" reals nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/")) nil)) (critical_points_2D 0 (critical_points_2D-1 nil 3476204808 ("" (skeep) (("" (lemma "circle_hit_solution") (("" (inst?) (("" (assert) (("" (split -1) (("1" (propax) nil nil) ("2" (replace -1) (("2" (lemma "tau_2D_def") (("2" (inst - "s" "v") (("2" (replace -2) (("2" (expand "horiz_dist_scaf") (("2" (assert) (("2" (lemma "line_solution_zero") (("2" (inst - "s") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "lower_circle_hit_solution") (("3" (inst - "s" "v") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((circle_hit_solution formula-decl nil omega_2D nil) (real_ge_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/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (lower_circle_hit_solution formula-decl nil omega_2D nil) (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (D formal-const-decl "posreal" omega_2D 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (line_solution_zero formula-decl nil line_solutions nil) (Vector 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_zero formula-decl nil vectors_2D "vectors/") (real_minus_real_is_real application-judgement "real" reals nil) (tau_2D_def formula-decl nil omega_2D nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil)) shostak)))
¤ 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.0.205Bemerkung: (vorverarbeitet am 2026-04-27) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26