| products/sources/formale Sprachen/PVS/ACCoRD/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: ppvernac.ml Sprache: LispOriginal von: PVS© |
|
||||||
|
(vs_only
(vs_only_TCC1 0 (vs_only_TCC1-2 nil 3465560929 ("" (skeep) (("" (assert) (("" (lemma "Delta_gt_0_nzv") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((sq_nz_pos application-judgement "posreal" sq "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Delta_gt_0_nzv formula-decl nil horizontal nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (D formal-const-decl "posreal" vs_only nil)) nil) (vs_only_TCC1-1 nil 3451819894 ("" (skeep) (("" (assert) nil nil)) nil) ((sq_nz_pos application-judgement "posreal" sq "reals/")) nil)) (vs_only_TCC2 0 (vs_only_TCC2-2 nil 3465683789 ("" (skeep) (("" (lemma "Theta_D_neq_0") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((D formal-const-decl "posreal" vs_only 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_neq_0 formula-decl nil horizontal nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Ss_vect2 type-eq-decl nil horizontal nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Sign type-eq-decl nil sign "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nzint nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal 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) (Vector type-eq-decl nil vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (s skolem-const-decl "Vect3" vs_only nil) (sq const-decl "nonneg_real" sq "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/")) nil) (vs_only_TCC2-1 nil 3465683704 ("" (subtype-tcc) nil nil) nil nil)) (vs_only_TCC3 0 (vs_only_TCC3-1 nil 3466271452 ("" (subtype-tcc) nil nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nzint nonempty-type-eq-decl nil integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (Sign type-eq-decl nil sign "reals/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (det const-decl "real" det_2D "vectors/") (D formal-const-decl "posreal" vs_only nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (Delta const-decl "real" horizontal nil) (/= const-decl "boolean" notequal nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (circle_vs_only_ge 0 (circle_vs_only_ge-2 nil 3470157239 ("" (skeep) (("" (expand "circle_criterion?") (("" (flatten) (("" (rewrite "vect2_add") (("" (rewrite "vect2_add") (("" (rewrite "vect2_scal") (("" (rewrite "vect2_scal") (("" (assert) (("" (lemma "vertical_sep_dir_at") (("" (inst -1 "-eps" "nnt" "v`z" "s`z" "vz") (("" (assert) (("" (hide -2 -4) (("" (expand* "+" "*") (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sign_neg_clos application-judgement "Sign" sign "reals/") (real_times_real_is_real application-judgement "real" reals nil) (circle_criterion? const-decl "bool" circle_criterion nil) (vect2_add formula-decl nil vect_3D_2D "vectors/") (real nonempty-type-from-decl nil reals nil) (Vect3 type-eq-decl nil vectors_3D_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) (Vector type-eq-decl nil vectors_3D "vectors/") (* const-decl "Vector" vectors_3D "vectors/") (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (vect2_scal formula-decl nil vect_3D_2D "vectors/") (vect2_eq formula-decl nil vect_3D_2D "vectors/") (real_plus_real_is_real application-judgement "real" reals nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (Sign type-eq-decl nil sign "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nzint nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal 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) (+ const-decl "Vector" vectors_3D "vectors/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (H formal-const-decl "posreal" vs_only 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) (vertical_sep_dir_at formula-decl nil vz_criteria nil)) nil) (circle_vs_only_ge-1 nil 3451818153 ("" (skeep) (("" (expand "circle_criterion?") (("" (flatten) (("" (rewrite "vect2_add") (("" (rewrite "vect2_scal") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((sign_neg_clos application-judgement "Sign" sign "reals/") (vect2_add formula-decl nil vect_3D_2D "vectors/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (Vector type-eq-decl nil vectors_3D "vectors/") (* const-decl "Vector" vectors_3D "vectors/") (sq_nz_pos application-judgement "posreal" sq "reals/") (vect2_scal formula-decl nil vect_3D_2D "vectors/")) nil)) (vs_entry_meets_circle_criterion_TCC1 0 (vs_entry_meets_circle_criterion_TCC1-2 nil 3471099308 ("" (skeep) (("" (rewrite "horizontal_conflict") (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil) ((nzv2 application-judgement "Nz_vect2" definitions_3D nil) (horizontal_conflict formula-decl nil horizontal 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/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Nzv2_vect3 type-eq-decl nil definitions_3D nil) (nnreal type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (H formal-const-decl "posreal" vs_only nil) (Ss2_vect3 type-eq-decl nil space_3D 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" vs_only nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_times_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/") (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ssv2 application-judgement "Ss_vect2[D]" vs_only nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil) (vs_entry_meets_circle_criterion_TCC1-1 nil 3471099160 ("" (subtype-tcc) nil nil) nil nil)) (vs_entry_meets_circle_criterion_TCC2 0 (vs_entry_meets_circle_criterion_TCC2-2 nil 3471099331 ("" (skeep) (("" (lemma "Theta_D_entry_gt_0") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((D formal-const-decl "posreal" vs_only 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_entry_gt_0 formula-decl nil horizontal nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Ss2_vect3 type-eq-decl nil space_3D nil) (H formal-const-decl "posreal" vs_only nil) (Ss_vect2 type-eq-decl nil horizontal nil) (sq const-decl "nonneg_real" sq "reals/") (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (Nzv2_vect3 type-eq-decl nil definitions_3D nil) (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vect3 type-eq-decl nil vectors_3D_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/") (nzv2 application-judgement "Nz_vect2" definitions_3D nil) (ssv2 application-judgement "Ss_vect2[D]" vs_only nil)) nil) (vs_entry_meets_circle_criterion_TCC2-1 nil 3471099160 ("" (subtype-tcc) nil nil) nil nil)) (vs_entry_meets_circle_criterion 0 (vs_entry_meets_circle_criterion-1 nil 3471099160 ("" (skeep) (("" (lemma "horizontal_conflict") (("" (inst?) (("" (assert) (("" (flatten) (("" (lemma "Theta_D_entry_gt_0") (("" (inst?) (("" (assert) (("" (name-replace "tentry" "Theta_D(ss,vgs,Entry)" :hide? nil) (("" (lemma "circle_vs_only_ge") (("" (inst -1 "Entry" "tentry" "ss" "vgs" "vs_at(ss`z, tentry, eps)") (("1" (skoletin -1) (("1" (assert) (("1" (hide 2) (("1" (lemma "vs_at_H") (("1" (inst?) (("1" (expand "circle_criterion?") (("1" (rewrite "vect2_add") (("1" (rewrite "vect2_scal") (("1" (case-replace "(ss + tentry * (vgs WITH [z := vs_at(ss`z, tentry, eps)]))`z = ss`z+tentry*vs_at(ss`z,tentry,eps)") (("1" (hide -1) (("1" (replaces -1) (("1" (lemma "Theta_D_on_D") (("1" (inst?) (("1" (assert) (("1" (lemma "sdotv_lt_0") (("1" (inst? -1) (("1" (rewrite "horizontal_conflict_entry") (("1" (assert) (("1" (rewrite "sign_abs") (("1" (lemma "sign_mult_pos") (("1" (inst -1 "H" "eps") (("1" (assert) (("1" (replaces -1) (("1" (rewrite "sign_id") (("1" (assert) (("1" (case-replace "eps*(eps*H) = H" :hide? nil) (("1" (assert) (("1" (expand "vs_at") (("1" (hide-all-but (-1 -6 -10 -11 1)) (("1" (grind-reals) (("1" (cancel-by 1 "H") nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "eps") (("2" (hide -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) ("2" (hide-all-but 1) (("2" (expand* "+" "*") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((D formal-const-decl "posreal" vs_only 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_conflict formula-decl nil horizontal nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ssv2 application-judgement "Ss_vect2[D]" vs_only nil) (Theta_D_entry_gt_0 formula-decl nil horizontal nil) (circle_vs_only_ge formula-decl nil vs_only nil) (real_plus_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sign const-decl "Sign" sign "reals/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (circle_criterion? const-decl "bool" circle_criterion nil) (Vector type-eq-decl nil vectors_3D "vectors/") (+ const-decl "Vector" vectors_3D "vectors/") (* const-decl "Vector" vectors_3D "vectors/") (<= const-decl "bool" reals nil) (vect2_add formula-decl nil vect_3D_2D "vectors/") (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (sdotv_lt_0 formula-decl nil horizontal nil) (horizontal_conflict_entry formula-decl nil horizontal nil) (sign_abs formula-decl nil sign "reals/") (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 "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (both_sides_times_pos_ge1 formula-decl nil real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (times_div2 formula-decl nil real_props nil) (times_div1 formula-decl nil real_props nil) (zero_times1 formula-decl nil real_props nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (div_mult_pos_ge2 formula-decl nil real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (sign_id formula-decl nil sign "reals/") (sign_mult_pos formula-decl nil sign "reals/") (Sp_vect2 type-eq-decl nil horizontal nil) (+ const-decl "Vector" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (Theta_D_on_D formula-decl nil horizontal nil) (vect2_eq formula-decl nil vect_3D_2D "vectors/") (vect2_scal formula-decl nil vect_3D_2D "vectors/") (vs_at_H formula-decl nil vertical nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nzreal nonempty-type-eq-decl nil reals nil) (vs_at const-decl "real" vertical nil) (tentry skolem-const-decl "real" vs_only nil) (Theta_D const-decl "real" horizontal nil) (Sign type-eq-decl nil sign "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (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) (Delta const-decl "real" horizontal nil) (= const-decl "[T, T -> boolean]" equalities nil) (Ss_vect2 type-eq-decl nil horizontal nil) (Ss2_vect3 type-eq-decl nil space_3D nil) (H formal-const-decl "posreal" vs_only nil) (sq const-decl "nonneg_real" sq "reals/") (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (Nzv2_vect3 type-eq-decl nil definitions_3D nil) (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vect3 type-eq-decl nil vectors_3D_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/") (nzv2 application-judgement "Nz_vect2" definitions_3D nil)) nil)) (vs_exit_meets_circle_criterion_TCC1 0 (vs_exit_meets_circle_criterion_TCC1-2 nil 3471099258 ("" (skeep) (("" (rewrite "horizontal_conflict") (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil) ((nzv2 application-judgement "Nz_vect2" definitions_3D nil) (horizontal_conflict formula-decl nil horizontal 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/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Nzv2_vect3 type-eq-decl nil definitions_3D 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" vs_only nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_times_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/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil) (vs_exit_meets_circle_criterion_TCC1-1 nil 3471099186 ("" (subtype-tcc) nil nil) nil nil)) (vs_exit_meets_circle_criterion_TCC2 0 (vs_exit_meets_circle_criterion_TCC2-2 nil 3471099282 ("" (skeep) (("" (rewrite "horizontal_conflict") (("" (flatten) (("" (lemma "Theta_D_exit_gt_0") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((nzv2 application-judgement "Nz_vect2" definitions_3D nil) (horizontal_conflict formula-decl nil horizontal 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/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Nzv2_vect3 type-eq-decl nil definitions_3D 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" vs_only nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_times_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/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Theta_D_exit_gt_0 formula-decl nil horizontal nil)) nil) (vs_exit_meets_circle_criterion_TCC2-1 nil 3471099186 ("" (subtype-tcc) nil nil) nil nil)) (vs_exit_meets_circle_criterion 0 (vs_exit_meets_circle_criterion-1 nil 3471099186 ("" (skeep) (("" (lemma "horizontal_conflict") (("" (inst?) (("" (assert) (("" (flatten) (("" (lemma "Theta_D_exit_gt_0") (("" (inst?) (("" (assert) (("" (replaces -1) (("" (name-replace "texit" "Theta_D(s, vgs, Exit)" :hide? nil) (("" (expand "circle_criterion?") (("" (lemma "vs_at_H") (("" (inst?) (("" (case-replace "(s+texit*vgs)`z = s`z+texit*vgs`z") (("1" (hide -1) (("1" (replace -7 :dir rl) (("1" (replaces -1) (("1" (rewrite "vect2_add") (("1" (rewrite "vect2_scal") (("1" (lemma "Theta_D_on_D") (("1" (inst?) (("1" (assert) (("1" (case "abs(eps*H) >= H") (("1" (assert) (("1" (split 1) (("1" (lemma "not_horizontal_conflict_exit") (("1" (inst?) (("1" (assert) (("1" (lemma "horizontal_conflict") (("1" (inst?) (("1" (assert) (("1" (lemma "Delta_eq") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replaces -8) (("2" (expand "vs_at") (("2" (cancel-by 1 "H") (("2" (hide-all-but (-7 2)) (("2" (typepred "eps") (("2" (cross-mult 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "eps") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand* "+" "*") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((D formal-const-decl "posreal" vs_only 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_conflict formula-decl nil horizontal nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (Theta_D_exit_gt_0 formula-decl nil horizontal nil) (= const-decl "[T, T -> boolean]" equalities nil) (Delta const-decl "real" horizontal nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nzint nonempty-type-eq-decl nil integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (Sign type-eq-decl nil sign "reals/") (Theta_D const-decl "real" horizontal nil) (vs_at_H formula-decl nil vertical nil) (H formal-const-decl "posreal" vs_only nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "Vector" vectors_3D "vectors/") (+ const-decl "Vector" vectors_3D "vectors/") (Vector type-eq-decl nil vectors_3D "vectors/") (real_plus_real_is_real application-judgement "real" reals nil) (vect2_add formula-decl nil vect_3D_2D "vectors/") (Theta_D_on_D formula-decl nil horizontal nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (both_sides_times_pos_ge1 formula-decl nil real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (zero_div formula-decl nil extra_tegies nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (vs_at const-decl "real" vertical nil) (real_minus_real_is_real application-judgement "real" reals nil) (not_horizontal_conflict_exit formula-decl nil horizontal nil) (* const-decl "Vector" vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (Delta_eq formula-decl nil horizontal nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (vect2_scal formula-decl nil vect_3D_2D "vectors/") (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal nonempty-type-eq-decl nil reals nil) (circle_criterion? const-decl "bool" circle_criterion 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/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Nzv2_vect3 type-eq-decl nil definitions_3D nil) (nzv2 application-judgement "Nz_vect2" definitions_3D nil)) nil))) ¤ Dauer der Verarbeitung: 0.209 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
