| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 85 kB |
|
Quelle cd2d.prf Sprache: Lisp |
|||||||||
|
(cd2d
(conflict_2D_horizontal 0 (conflict_2D_horizontal-1 nil 3476542449 ("" (skeep) (("" (expand "conflict_2D?") (("" (expand "horizontal_conflict?") (("" (skeep -1) (("" (inst 1 "t") nil nil)) nil)) nil)) nil)) nil) ((conflict_2D? const-decl "bool" cd2d nil) (Lookahead type-eq-decl nil Lookahead nil) (T formal-const-decl "{AB: posreal | AB > B}" cd2d 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" cd2d 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) (horizontal_conflict? const-decl "bool" horizontal nil)) nil)) (on_D_conflict 0 (on_D_conflict-1 nil 3476542471 ("" (skeep) (("" (split) (("1" (flatten) (("1" (expand "conflict_2D?") (("1" (skeep -1) (("1" (name "tt" "t-B") (("1" (name "w" "s+B*v") (("1" (replace -1) (("1" (case "s+t*v = w + tt*v") (("1" (replace -1) (("1" (case "tt > 0 and tt <= T-B") (("1" (hide -2) (("1" (hide -2) (("1" (hide -2) (("1" (flatten) (("1" (replaces -4 :dir rl) (("1" (rewrite "sqv_add") (("1" (both-sides "-" "sqv(w)" -3) (("1" (assert) (("1" (rewrite "sqv_scal") (("1" (expand "sq") (("1" (cancel-by -3 "tt") (("1" (lemma "posreal_times_posreal_is_posreal") (("1" (inst - "tt" "sqv(v)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (replace -1 :dir rl) (("2" (replace -2 :dir rl) (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "conflict_2D?") (("2" (case-replace "v=zero") (("1" (assert) nil nil) ("2" (replaces -2 :dir rl) (("2" (name "tt" "-(s*v)/sqv(v)") (("1" (case "tt > B") (("1" (case "tt < T") (("1" (inst + "tt") (("1" (lemma "quad_min_mono_dec") (("1" (inst - "sqv(v)" "2*(s*v)" "sqv(s)" "B" "tt") (("1" (assert) (("1" (split -1) (("1" (expand "quadratic") (("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) ("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil) ("3" (assert) nil nil) ("4" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (inst 3 "T") (("1" (lemma "quad_min_mono_dec") (("1" (inst - "sqv(v)" "2*(s*v)" "sqv(s)" "B" "T") (("1" (assert) (("1" (split -1) (("1" (expand "quadratic") (("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) ("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil) ("3" (assert) nil nil) ("4" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (replace -1 :dir rl) (("2" (neg-formula 1) (("2" (cross-mult 1) (("2" (split 1) (("1" (flatten) (("1" (rewrite "dot_add_left") (("1" (expand "sqv") (("1" (assert) nil 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) ("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((conflict_2D? const-decl "bool" cd2d nil) (Lookahead type-eq-decl nil Lookahead nil) (T formal-const-decl "{AB: posreal | AB > B}" cd2d 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" cd2d 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) (- 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) (real_minus_real_is_real application-judgement "real" reals nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (< const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "real" vectors_2D "vectors/") (NOT const-decl "[bool -> bool]" booleans nil) (both_sides_minus_lt1 formula-decl nil real_props nil) (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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sqv_scal formula-decl nil vectors_2D "vectors/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (/= const-decl "boolean" notequal nil) (CBD_60 skolem-const-decl "real" cd2d nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (pos_div_gt formula-decl nil real_props nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (zero_times1 formula-decl nil real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (zero_div formula-decl nil extra_tegies nil) (posreal_times_posreal_is_posreal judgement-tcc nil real_types nil) (sq const-decl "nonneg_real" sq "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (dot_scal_left formula-decl nil vectors_2D "vectors/") (dot_scal_right formula-decl nil vectors_2D "vectors/") (real_plus_real_is_real application-judgement "real" reals 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_times_real_is_real application-judgement "real" reals nil) (sqv_add formula-decl nil vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (tt skolem-const-decl "real" cd2d nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (quadratic const-decl "real" quadratic "reals/") (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (minus_real_is_real application-judgement "real" reals nil) (quad_min_mono_dec formula-decl nil quad_minmax "reals/") (neg_neg formula-decl nil extra_tegies nil) (neg_div formula-decl nil extra_tegies nil) (mult_neg formula-decl nil extra_tegies nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (both_sides_times_neg_le1_imp formula-decl nil extra_real_props nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (dot_add_left formula-decl nil vectors_2D "vectors/") (div_mult_pos_neg_gt2 formula-decl nil extra_real_props nil) (- const-decl "[numfield -> numfield]" number_fields 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/") (zero const-decl "Vector" vectors_2D "vectors/")) nil)) (tau_v2_TCC1 0 (tau_v2_TCC1-1 nil 3476554326 ("" (skeep) (("" (lemma "B_lt_T") (("" (grind :exclude "horizontal_tca") nil nil)) nil)) nil) ((real_ge_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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)) nil)) (tau_vv 0 (tau_vv-1 nil 3476542502 ("" (skeep) (("" (expand "tau_vv") (("" (expand "tau_v2") (("" (rewrite "nneg_mult_min") (("" (rewrite "nneg_mult_max") (("" (expand "horizontal_tca") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (tau_vv const-decl "real" cd2d nil) (nneg_mult_min formula-decl nil min_max "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) (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) (Vector type-eq-decl nil vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (AND const-decl "[bool, bool -> bool]" booleans nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (B formal-const-decl "nnreal" cd2d nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (horizontal_tca const-decl "real" definitions 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}" cd2d nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (real_times_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nneg_mult_max formula-decl nil min_max "reals/") (tau_v2 const-decl "Lookahead" cd2d nil)) nil)) (tau_vv_continuous 0 (tau_vv_continuous-2 nil 3476542521 ("" (skeep) (("" (expand "tau_vv") (("" (rewrite "min_cont_vr") (("1" (rewrite "mult_cont_vr") (("1" (rewrite "const_cont_vr") nil nil)) nil) ("2" (rewrite "max_cont_vr") (("1" (rewrite "neg_cont_vr") (("1" (rewrite "dot_cont_vr") (("1" (rewrite "id_cont_vv") nil nil) ("2" (rewrite "const_cont_vv") nil nil)) nil)) nil) ("2" (rewrite "mult_cont_vr") (("2" (rewrite "const_cont_vr") nil nil)) nil)) nil)) nil)) nil)) nil) ((tau_vv const-decl "real" cd2d nil) (max_cont_vr formula-decl nil vect_cont_2D "vect_analysis/") (continuous_vv? const-decl "bool" cont_vect2_vect2 "vect_analysis/") (dot_cont_vr formula-decl nil vect2_cont_dot "vect_analysis/") (id_cont_vv formula-decl nil vect_cont_2D "vect_analysis/") (const_cont_vv formula-decl nil vect_cont_2D "vect_analysis/") (neg_cont_vr formula-decl nil vect_cont_2D "vect_analysis/") (mult_cont_vr formula-decl nil vect_cont_2D "vect_analysis/") (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (const_cont_vr formula-decl nil vect_cont_2D "vect_analysis/") (T formal-const-decl "{AB: posreal | AB > B}" cd2d 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 "real" vectors_2D "vectors/") (- const-decl "[numfield -> numfield]" number_fields nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (B formal-const-decl "nnreal" cd2d nil) (nnreal type-eq-decl nil real_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (>= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (continuous_vr_fun nonempty-type-eq-decl nil cont_vect2_real "vect_analysis/") (continuous_vr? const-decl "bool" cont_vect2_real "vect_analysis/") (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) (min_cont_vr formula-decl nil vect_cont_2D "vect_analysis/") (minus_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) nil) (tau_vv_continuous-1 nil 3476542420 ("" (judgement-tcc) nil nil) nil nil)) (horizontal_omega_min 0 (horizontal_omega_min-1 nil 3476542942 ("" (skeep) (("" (expand "horizontal_omega") (("" (expand "tau_v2") (("" (case "horizontal_tca(s,nzv) (("1" (expand "max") (("1" (assert) (("1" (expand "min") (("1" (expand "horizontal_tca") (("1" (lemma "quad_min_mono_inc") (("1" (inst -1 "sqv(nzv)" "2*s*nzv" "sqv(s)" "t" "B") (("1" (assert) (("1" (typepred "t") (("1" (assert) (("1" (expand "quadratic") (("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)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "horizontal_tca(s,nzv) > T") (("1" (expand "max") (("1" (assert) (("1" (expand "min") (("1" (expand "horizontal_tca") (("1" (lemma "quad_min_mono_dec") (("1" (inst -1 "sqv(nzv)" "2*s*nzv" "sqv(s)" "t" "T") (("1" (assert) (("1" (typepred "t") (("1" (assert) (("1" (expand "quadratic") (("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)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "max(B,horizontal_tca(s,nzv)) = horizontal_tca(s,nzv)") (("1" (hide -1) (("1" (expand "min") (("1" (lift-if) (("1" (assert) (("1" (rewrite "horizontal_sq_dtca_eq" :dir rl) (("1" (rewrite "horizontal_tca_min") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (expand "max") (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((horizontal_omega const-decl "nnreal" cd2d nil) (B formal-const-decl "nnreal" cd2d nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (horizontal_tca const-decl "real" definitions nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (Vector type-eq-decl nil vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (< 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) (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (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) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (nonzero_real nonempty-type-eq-decl nil reals nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (AND const-decl "[bool, bool -> bool]" 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) (T formal-const-decl "{AB: posreal | AB > B}" cd2d nil) (Lookahead type-eq-decl nil Lookahead nil) (NOT const-decl "[bool -> bool]" booleans nil) (quadratic const-decl "real" quadratic "reals/") (sqv_scal formula-decl nil vectors_2D "vectors/") (dot_scal_right formula-decl nil vectors_2D "vectors/") (real_plus_real_is_real application-judgement "real" reals nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sqv_add formula-decl nil vectors_2D "vectors/") (dot_scal_left formula-decl nil vectors_2D "vectors/") (real_div_nzreal_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types 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) (quad_min_mono_inc formula-decl nil quad_minmax "reals/") (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (= const-decl "[T, T -> boolean]" equalities nil) (horizontal_tca_min formula-decl nil definitions nil) (horizontal_sq_dtca_eq formula-decl nil definitions nil) (quad_min_mono_dec formula-decl nil quad_minmax "reals/") (nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/") (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (tau_v2 const-decl "Lookahead" cd2d nil)) nil)) (horizontal_omega_conflict 0 (horizontal_omega_conflict-1 nil 3476543011 ("" (skeep) (("" (split) (("1" (flatten) (("1" (expand "conflict_2D?") (("1" (assert) (("1" (skeep -1) (("1" (lemma "horizontal_omega_min") (("1" (inst -1 "nzv" "s" "t") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "conflict_2D?") (("2" (assert) (("2" (expand "horizontal_omega") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((conflict_2D? const-decl "bool" cd2d nil) (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (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) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (B formal-const-decl "nnreal" cd2d 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}" cd2d nil) (Lookahead type-eq-decl nil Lookahead nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (horizontal_omega_min formula-decl nil cd2d nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (horizontal_omega const-decl "nnreal" cd2d nil) (tau_v2 const-decl "Lookahead" cd2d nil)) nil)) (omega_vv_continuous 0 (omega_vv_continuous-3 "" 3504844894 ("" (skeep) (("" (expand "omega_vv") (("" (case "sqv(s) = sq(D) AND B = 0") (("1" (flatten) (("1" (assert) (("1" (rewrite "dot_cont_vr") (("1" (rewrite "id_cont_vv") nil nil) ("2" (rewrite "const_cont_vv") nil nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (rewrite "sub_cont_vr") (("1" (rewrite "mult_cont_vr") (("1" (rewrite "const_cont_vr") nil nil)) nil) ("2" (rewrite "add_cont_vr") (("1" (rewrite "mult_cont_vr") (("1" (rewrite "const_cont_vr") nil nil)) nil) ("2" (rewrite "add_cont_vr") (("1" (rewrite "mult_cont_vr") (("1" (rewrite "mult_cont_vr") (("1" (rewrite "dot_cont_vr") (("1" (rewrite "id_cont_vv") nil nil) ("2" (rewrite "const_cont_vv") nil nil)) nil) ("2" (case-replace "(LAMBDA (v): tau_vv(s)(v)) = tau_vv(s)") (("1" (assert) nil nil) ("2" (decompose-equality) nil nil)) nil)) nil) ("2" (rewrite "const_cont_vr") nil nil)) nil) ("2" (rewrite "sq_cont_vr") (("2" (case-replace "(LAMBDA (v): tau_vv(s)(v)) = tau_vv(s)") (("1" (assert) nil nil) ("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_times_real_is_real application-judgement "real" reals nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (omega_vv const-decl "real" cd2d nil) (add_cont_vr formula-decl nil vect_cont_2D "vect_analysis/") (sq_cont_vr formula-decl nil vect_cont_2D "vect_analysis/") (tau_vv_continuous application-judgement "continuous_vr_fun" cd2d nil) (mult_cont_vr formula-decl nil vect_cont_2D "vect_analysis/") (const_cont_vr formula-decl nil vect_cont_2D "vect_analysis/") (* const-decl "real" vectors_2D "vectors/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (tau_vv const-decl "real" cd2d nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (continuous_vr_fun nonempty-type-eq-decl nil cont_vect2_real "vect_analysis/") (continuous_vr? const-decl "bool" cont_vect2_real "vect_analysis/") (sub_cont_vr formula-decl nil vect_cont_2D "vect_analysis/") (real_plus_real_is_real application-judgement "real" reals nil) (continuous_vv? const-decl "bool" cont_vect2_vect2 "vect_analysis/") (dot_cont_vr formula-decl nil vect2_cont_dot "vect_analysis/") (id_cont_vv formula-decl nil vect_cont_2D "vect_analysis/") (const_cont_vv formula-decl nil vect_cont_2D "vect_analysis/") (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (sq const-decl "nonneg_real" sq "reals/") (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (D formal-const-decl "posreal" cd2d nil) (B formal-const-decl "nnreal" cd2d nil)) shostak) (omega_vv_continuous-2 nil 3476542620 ("" (skeep) (("" (expand "omega_vv") (("" (lift-if) (("" (split 1) (("1" (flatten) (("1" (rewrite "dot_cont_vr") (("1" (rewrite "id_cont_vv") nil nil) ("2" (rewrite "const_cont_vv") nil nil)) nil)) nil) ("2" (flatten) (("2" (rewrite "sub_cont_vr") (("1" (rewrite "mult_cont_vr") (("1" (rewrite "const_cont_vr") nil nil)) nil) ("2" (rewrite "add_cont_vr") (("1" (rewrite "mult_cont_vr") (("1" (rewrite "const_cont_vr") nil nil)) nil) ("2" (rewrite "add_cont_vr") (("1" (rewrite "mult_cont_vr") (("1" (rewrite "mult_cont_vr") (("1" (rewrite "dot_cont_vr") (("1" (rewrite "id_cont_vv") nil nil) ("2" (rewrite "const_cont_vv") nil nil)) nil) ("2" (case-replace "(LAMBDA (v): tau_vv(s)(v)) = tau_vv(s)") (("1" (assert) nil nil) ("2" (decompose-equality) nil nil)) nil)) nil) ("2" (rewrite "const_cont_vr") nil nil)) nil) ("2" (rewrite "sq_cont_vr") (("2" (case-replace "(LAMBDA (v): tau_vv(s)(v)) = tau_vv(s)") (("1" (assert) nil nil) ("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sq_nz_pos application-judgement "posreal" sq "reals/") (add_cont_vr formula-decl nil vect_cont_2D "vect_analysis/") (sq_cont_vr formula-decl nil vect_cont_2D "vect_analysis/") (mult_cont_vr formula-decl nil vect_cont_2D "vect_analysis/") (const_cont_vr formula-decl nil vect_cont_2D "vect_analysis/") (sub_cont_vr formula-decl nil vect_cont_2D "vect_analysis/") (continuous_vr_fun nonempty-type-eq-decl nil cont_vect2_real "vect_analysis/") (* const-decl "real" vectors_2D "vectors/") (dot_cont_vr formula-decl nil vect2_cont_dot "vect_analysis/") (id_cont_vv formula-decl nil vect_cont_2D "vect_analysis/") (const_cont_vv formula-decl nil vect_cont_2D "vect_analysis/") (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (Vector type-eq-decl nil vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (sq const-decl "nonneg_real" sq "reals/")) nil) (omega_vv_continuous-1 nil 3476542420 ("" (judgement-tcc) nil nil) nil nil)) (omega_vv 0 (omega_vv-1 nil 3476542639 ("" (skeep) (("" (expand "omega_vv") (("" (expand "horizontal_omega") (("" (rewrite "sqv_add") (("" (assert) (("" (rewrite "sqv_scal") (("" (rewrite "tau_vv") (("" (assert) (("" (rewrite "sq_times") (("" (expand "sq") (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_times_real_is_real application-judgement "real" reals nil) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (sq_nz_pos application-judgement "posreal" sq "reals/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (omega_vv const-decl "real" cd2d nil) (sqv_add formula-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (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) (* const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (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" cd2d 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}" cd2d nil) (Lookahead type-eq-decl nil Lookahead nil) (tau_v2 const-decl "Lookahead" cd2d nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (dot_scal_right formula-decl nil vectors_2D "vectors/") (dot_scal_left formula-decl nil vectors_2D "vectors/") (sqv_scal formula-decl nil vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (sq_times formula-decl nil sq "reals/") (sqv const-decl "nnreal" vectors_2D "vectors/") (tau_vv formula-decl nil cd2d nil) (real_minus_real_is_real application-judgement "real" reals nil) (horizontal_omega const-decl "nnreal" cd2d nil)) nil)) (omega_vv_conflict 0 (omega_vv_conflict-1 nil 3476542662 ("" (skeep) (("" (case "on_D?(s) and B = 0") (("1" (flatten) (("1" (lemma "on_D_conflict") (("1" (inst?) (("1" (replace -3) (("1" (assert) (("1" (expand "omega_vv") (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "v=zero") (("1" (replaces -1) (("1" (assert) (("1" (expand "omega_vv") (("1" (assert) (("1" (replace 1) (("1" (expand "conflict_2D?") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -1) (("2" (rewrite "omega_vv") (("2" (lemma "horizontal_omega_conflict") (("2" (inst - "v" "s") (("2" (assert) (("2" (replace -1) (("2" (hide-all-but (1 3)) (("2" (case "sqv(v) > 0") (("1" (ground) (("1" (mult-by 1 "sqv(v)") (("1" (assert) nil nil)) nil) ("2" (mult-by -1 "sqv(v)") (("2" (assert) nil nil)) nil)) nil) ("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((B formal-const-decl "nnreal" cd2d nil) (D formal-const-decl "posreal" cd2d 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) (>= const-decl "bool" 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) (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (on_D_conflict formula-decl nil cd2d nil) (omega_vv const-decl "real" cd2d nil) (add_zero_right formula-decl nil vectors_2D "vectors/") (scal_0 formula-decl nil vectors_2D "vectors/") (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (sq_nz_pos application-judgement "posreal" sq "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (omega_vv_continuous application-judgement "continuous_vr_fun" cd2d nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (omega_vv formula-decl nil cd2d nil) (real_minus_real_is_real application-judgement "real" reals nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (horizontal_omega const-decl "nnreal" cd2d nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (< const-decl "bool" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (horizontal_omega_conflict formula-decl nil cd2d nil) (real_times_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (scal_zero formula-decl nil vectors_2D "vectors/") (tau_vv_continuous application-judgement "continuous_vr_fun" cd2d nil) (conflict_2D? const-decl "bool" cd2d nil) (sqv_zero formula-decl nil vectors_2D "vectors/") (dot_zero_right formula-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/")) nil)) (omega_vv_zero_TCC1 0 (omega_vv_zero_TCC1-1 nil 3476542420 ("" (subtype-tcc) nil nil) ((* const-decl "real" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (/= const-decl "boolean" notequal nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (omega_vv_zero 0 (omega_vv_zero-1 nil 3476542678 ("" (skeep) (("" (case "v=zero") (("1" (assert) (("1" (replaces -1) (("1" (expand "omega_vv") (("1" (assert) (("1" (expand "tau_vv") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "omega_vv") (("2" (assert) (("2" (split 3) (("1" (flatten) (("1" (mult-by 1 "sqv(v)") (("1" (assert) nil nil) ("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (mult-by -1 "sqv(v)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((zero const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil) (dot_zero_right formula-decl nil vectors_2D "vectors/") (sqv_zero formula-decl nil vectors_2D "vectors/") (max_id formula-decl nil min_max "reals/") (min_id formula-decl nil min_max "reals/") (sq_0 formula-decl nil sq "reals/") (tau_vv const-decl "real" cd2d nil) (omega_vv const-decl "real" cd2d nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (sq_nz_pos application-judgement "posreal" sq "reals/") (omega_vv_continuous application-judgement "continuous_vr_fun" cd2d nil) (both_sides_times1_imp formula-decl nil extra_real_props nil) (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (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) (sqv const-decl "nnreal" vectors_2D "vectors/") (v skolem-const-decl "Vect2" cd2d nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (horizontal_omega const-decl "nnreal" cd2d nil) (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" cd2d nil) (both_sides_times1 formula-decl nil real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (omega_vv formula-decl nil cd2d nil)) nil)) (omega_half_line 0 (omega_half_line-1 nil 3476542761 ("" (skeep :preds? t) (("" (expand "omega_half") (("" (expand "max") (("" (lift-if) (("" (split -) (("1" (flatten) (("1" (rewrite "sqv_add") (("1" (rewrite "sqv_scal") (("1" (sq-simp) (("1" (expand "sq" -2) (("1" (real-props) (("1" (case-replace "sqv(nzv) * (ss * nzv) * (ss * nzv) / (sqv(nzv) * sqv(nzv)) = ((ss * nzv) * (ss (("1" (hide -1) (("1" (move-terms -2 l 1) (("1" (case-replace "((ss * nzv) * (ss * nzv)) / sqv(nzv) - (2 * ((ss * nzv) * (ss * nzv))) / sqv(nz (("1" (hide -1) (("1" (neg-formula -2) (("1" (expand "line_solution?") (("1" (case "sq(R(ss) * det(ss, nzv)) = sq(ss*nzv)") (("1" (lemma "sq_eq_sign") (("1" (inst -1 "ss * nzv" "R(ss) * det(ss, nzv)") (("1" (assert) (("1" (skeep -1) (("1" (inst + "eps") (("1" (assert) (("1" (replaces -1) (("1" (cancel-by -3 "R(ss)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "sq" :dir rl) (("2" (rewrite "sq" :dir rl) (("2" (expand "R") (("2" (sq-simp) (("2" (rewrite "sq_det") (("2" (cross-mult -1) (("2" (field 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind-reals) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind-reals) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((minus_real_is_real application-judgement "real" reals nil) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (omega_half const-decl "nnreal" cd2d nil) (add_zero_right formula-decl nil vectors_2D "vectors/") (scal_0 formula-decl nil vectors_2D "vectors/") (sqv_scal formula-decl nil vectors_2D "vectors/") (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (real_minus_real_is_real application-judgement "real" reals nil) (R_gt_0 application-judgement "posreal" cd2d nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (line_solution? const-decl "bool" line_solutions nil) (sq_det formula-decl nil det_2D "vectors/") (both_sides_times1 formula-decl nil real_props nil) (div_cancel2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_cancel3 formula-decl nil real_props nil) (sq_times formula-decl nil sq "reals/") (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_sqrt formula-decl nil sqrt "reals/") (sq_eq_sign formula-decl nil sign "reals/") (Sign type-eq-decl nil sign "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (nzint nonempty-type-eq-decl nil integers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (det const-decl "real" det_2D "vectors/") (R const-decl "nnreal" horizontal_criteria nil) (Sp_vect2 type-eq-decl nil horizontal nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (both_sides_times1_imp formula-decl nil extra_real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (neg_div formula-decl nil extra_tegies nil) (neg_neg formula-decl nil extra_tegies nil) (mult_neg formula-decl nil extra_tegies nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (zero_times1 formula-decl nil real_props nil) (neg_lt formula-decl nil real_props nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (times_div2 formula-decl nil real_props nil) (times_div1 formula-decl nil real_props nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (sq_div formula-decl nil sq "reals/") (sq_neg formula-decl nil sq "reals/") (dot_scal_left formula-decl nil vectors_2D "vectors/") (dot_scal_right formula-decl nil vectors_2D "vectors/") (real_plus_real_is_real application-judgement "real" reals nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/") (real_times_real_is_real application-judgement "real" reals nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (- const-decl "[numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "Vector" vectors_2D "vectors/") (Ss_vect2 type-eq-decl nil horizontal nil) (D formal-const-decl "posreal" cd2d nil) (posreal nonempty-type-eq-decl nil real_types nil) (sq const-decl "nonneg_real" sq "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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/") (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil) (sqv_add formula-decl nil vectors_2D "vectors/") (real_div_nzreal_is_real application-judgement "real" reals nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)) nil)) (detection_2D_TCC1 0 (detection_2D_TCC1-2 nil 3459698359 ("" (skeep) (("" (assert) (("" (assert) nil nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil) (detection_2D_TCC1-1 nil 3459692027 ("" (subtype-tcc) nil nil) ((comp_zero_y formula-decl nil vectors_2D "vectors/") (comp_zero_x formula-decl nil vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (* const-decl "real" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (det const-decl "real" det_2D "vectors/") (Delta const-decl "real" horizontal nil)) nil)) (detection_2D_TCC2 0 (detection_2D_TCC2-1 nil 3459701862 ("" (skeep) (("" (lemma "B_lt_T") (("" (assert) nil nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (detection_2D_TCC3 0 (detection_2D_TCC3-2 nil 3459702138 ("" (skeep) (("" (assert) (("" (use "Delta_gt_0_nzv") (("" (assert) nil nil)) nil)) nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (D formal-const-decl "posreal" cd2d nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (Delta_gt_0_nzv formula-decl nil horizontal nil)) nil) (detection_2D_TCC3-1 nil 3459701862 ("" (skeep) (("" (skeep 2) (("" (skeep 2) (("" (rewrite "min_ge") (("" (rewrite "min_le") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) nil nil)) (detection_2D_TCC4 0 (detection_2D_TCC4-1 nil 3459701862 ("" (lemma "B_lt_T") (("" (skeep) (("" (skeep 2) (("" (skeep 2) (("" (hide -2) (("" (hide -2) (("" (hide -2) (("" (hide 1) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_ge_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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (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) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (Delta const-decl "real" horizontal nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (D formal-const-decl "posreal" cd2d nil) (det const-decl "real" det_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/")) nil)) (detection_2D_TCC5 0 (detection_2D_TCC5-2 nil 3476622370 ("" (lemma "B_lt_T") (("" (skeep) (("" (skeep 2) (("" (skeep 2) (("" (hide -2) (("" (hide -2) (("" (hide -2) (("" (hide 1) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.47 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28