| products/sources/formale Sprachen/PVS/ACCoRD/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: ide_win32_stubs.c Sprache: LispOriginal von: PVS© |
|
||||||
|
(trk_circle
(trk_circle_TCC1 0 (trk_circle_TCC1-1 nil 3431708640 ("" (skosimp*) (("" (rewrite "vect2_zero") nil nil)) nil) ((vect2_zero formula-decl nil vect_3D_2D "vectors/")) nil)) (trk_circle_TCC2 0 (trk_circle_TCC2-1 nil 3431708640 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil)) nil)) (trk_circle_TCC3 0 (trk_circle_TCC3-1 nil 3431708640 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sign_neg_clos application-judgement "Sign" sign "reals/") (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)) nil)) (trk_circle_TCC4 0 (trk_circle_TCC4-2 nil 3462838042 ("" (skeep) (("" (skeep 2) (("" (skeep 2) (("" (typepred "trk_only_circle(vect2(s), vect2(vo), vect2(vi),t, dir,irt)") (("1" (replaces -4 :dir rl) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((Nzv2_vect3 type-eq-decl nil definitions_3D nil) (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (trk_only_circle const-decl "{nvo | nvo /= zero => trk_only?(vo)(nvo)}" trk_only nil) (D formal-const-decl "posreal" trk_circle nil) (trk_only? const-decl "bool" definitions 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) (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 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) (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) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (/= const-decl "boolean" notequal nil) (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (nzv2 application-judgement "Nz_vect2" definitions_3D nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (vect2_eq_ext formula-decl nil vect_3D_2D "vectors/") (sign_neg_clos application-judgement "Sign" sign "reals/") (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)) nil) (trk_circle_TCC4-1 nil 3431708640 ("" (skosimp*) (("" (postpone) nil nil)) nil) nil nil)) (trk_circle_TCC5 0 (trk_circle_TCC5-2 nil 3431790884 ("" (skosimp*) (("" (rewrite "vect2_zero") nil nil)) nil) ((vect2_zero formula-decl nil vect_3D_2D "vectors/")) nil) (trk_circle_TCC5-1 nil 3431708640 ("" (skosimp*) (("" (assert) nil nil)) nil) nil nil)) (trk_vertical_irt_TCC1 0 (trk_vertical_irt_TCC1-1 nil 3471187768 ("" (skosimp*) (("" (replaces -1) (("" (hide -1) (("" (grind) nil nil)) nil)) nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil) (- const-decl "Vector" vectors_3D "vectors/")) nil)) (trk_vertical_irt_TCC2 0 (trk_vertical_irt_TCC2-1 nil 3471187768 ("" (skosimp*) (("" (assert) nil nil)) nil) ((sign_neg_clos application-judgement "Sign" sign "reals/") (real_ge_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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (trk_vertical_irt_TCC3 0 (trk_vertical_irt_TCC3-1 nil 3471187768 ("" (skosimp*) (("" (assert) nil nil)) nil) ((nzv2 application-judgement "Nz_vect2" definitions_3D nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sign_neg_clos application-judgement "Sign" sign "reals/") (real_ge_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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (trk_vertical_irt_TCC4 0 (trk_vertical_irt_TCC4-1 nil 3471187768 ("" (skosimp*) (("" (assert) (("" (typepred "trk_only_vertical(vect2(s!1), vect2(vo!1), vect2(vi!1), t!1, dir!1, irt!1)") (("" (assert) nil nil)) nil)) nil)) nil) ((sq_nz_pos application-judgement "posreal" sq "reals/") (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) (sign_mult_clos application-judgement "Sign" sign "reals/") (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (nzv2 application-judgement "Nz_vect2" definitions_3D nil) (sign_neg_clos application-judgement "Sign" sign "reals/") (real_ge_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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (vect2_eq_ext formula-decl nil vect_3D_2D "vectors/") (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (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) (>= 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) (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/") (zero const-decl "Vector" vectors_2D "vectors/") (trk_only? const-decl "bool" definitions nil) (D formal-const-decl "posreal" trk_circle nil) (trk_only_vertical const-decl "{nvo | nvo /= zero => trk_only?(vo)(nvo)}" trk_only nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Nzv2_vect3 type-eq-decl nil definitions_3D nil)) nil)) (trk_vertical_irt_TCC5 0 (trk_vertical_irt_TCC5-1 nil 3471187768 ("" (skosimp*) (("" (assert) nil nil)) nil) ((vect2_zero formula-decl nil vect_3D_2D "vectors/") (nzv2 application-judgement "Nz_vect2" definitions_3D nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sign_neg_clos application-judgement "Sign" sign "reals/") (real_ge_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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (trk_vertical_irt_TCC6 0 (trk_vertical_irt_TCC6-1 nil 3471187768 ("" (skosimp*) (("" (assert) nil nil)) nil) ((sign_neg_clos application-judgement "Sign" sign "reals/") (vect2_zero formula-decl nil vect_3D_2D "vectors/")) nil)) (trk_circle_nzvz 0 (trk_circle_nzvz-1 nil 3461943649 ("" (skeep) (("" (expand "trk_circle?") (("" (flatten) (("" (skeep -1) (("" (expand "trk_circle") (("" (assert) (("" (replaces -1) (("" (rewrite "vect2_zero") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((trk_circle? const-decl "bool" trk_circle nil) (vect2_zero formula-decl nil vect_3D_2D "vectors/") (trk_circle const-decl "{nvo | vect2(nvo) /= zero => trk_only?(vect2(vo))(vect2(nvo)) AND vo`z = nvo`z}" trk_circle nil)) shostak)) (trk_circle_solution_2D_TCC1 0 (trk_circle_solution_2D_TCC1-1 nil 3461943722 ("" (skeep) (("" (lemma "trk_circle_nzvz") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((trk_circle_nzvz formula-decl nil trk_circle nil) (real_minus_real_is_real application-judgement "real" reals nil) (Nzv2_vect3 type-eq-decl nil definitions_3D nil) (zero const-decl "Vector" vectors_2D "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (Vect3 type-eq-decl nil vectors_3D_def "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) (bool nonempty-type-eq-decl nil 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) (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)) nil)) (trk_circle_solution_2D 0 (trk_circle_solution_2D-1 nil 3461626185 ("" (skeep) (("" (expand "trk_circle?") (("" (flatten) (("" (skeep -1) (("" (expand "trk_circle") (("" (lift-if) (("" (split -) (("1" (flatten) (("1" (replaces -2) (("1" (rewrite "vect2_zero") nil nil)) nil)) nil) ("2" (flatten) (("2" (split -) (("1" (flatten) (("1" (name-replace "t" "Theta_H(s`z, vo`z - vi`z, -dir)") (("1" (name-replace "trk" "trk_only_circle(vect2(s), vect2(vo), vect2(vi),t,dir,irt)" :hide? nil) (("1" (rewrite "vect2_sub") (("1" (case-replace "vect2(nvo) = trk") (("1" (lemma "trk_only_circle_solution") (("1" (inst? -1) (("1" (assert) (("1" (inst -1 "vect2(vo)") (("1" (expand "trk_only_circle?") (("1" (inst 1 "irt") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (replaces -1) (("2" (expand "vect2") (("2" (decompose-equality 1) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replaces -1) (("2" (rewrite "vect2_zero") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((trk_circle? const-decl "bool" trk_circle nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (trk_only_circle const-decl "{nvo | nvo /= zero => trk_only?(vo)(nvo)}" trk_only nil) (D formal-const-decl "posreal" trk_circle nil) (trk_only? const-decl "bool" definitions nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (nzv2 application-judgement "Nz_vect2" definitions_3D nil) (t skolem-const-decl "real" trk_circle nil) (trk_only_circle? const-decl "bool" trk_only nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (trk_only_circle_solution formula-decl nil trk_only nil) (vect2_sub formula-decl nil vect_3D_2D "vectors/") (Nzv2_vect3 type-eq-decl nil definitions_3D nil) (zero const-decl "Vector" vectors_2D "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (Theta_H const-decl "real" vertical nil) (H formal-const-decl "posreal" trk_circle 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) (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) (bool nonempty-type-eq-decl nil 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) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal 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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sign_neg_clos application-judgement "Sign" sign "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (vect2_zero formula-decl nil vect_3D_2D "vectors/") (trk_circle const-decl "{nvo | vect2(nvo) /= zero => trk_only?(vect2(vo))(vect2(nvo)) AND vo`z = nvo`z}" trk_circle nil)) nil)) (trk_circle_solution 0 (trk_circle_solution-1 nil 3461667922 ("" (skeep) (("" (lemma "trk_circle_solution_2D") (("" (inst?) (("" (assert) (("" (expand "circle_solution?") (("" (expand "vertical_solution?") (("" (hide -1) (("" (expand "trk_circle?") (("" (flatten) (("" (skeep -1) (("" (expand "trk_circle") (("" (lift-if) (("" (split -) (("1" (flatten) (("1" (replaces -2) (("1" (rewrite "vect2_zero") nil nil)) nil)) nil) ("2" (flatten) (("2" (split -) (("1" (flatten) (("1" (lemma "Theta_H_on_H") (("1" (inst?) (("1" (skoletin -1) (("1" (replace -1 :dir rl) (("1" (assert) (("1" (split +) (("1" (rewrite "vz_distr_sub") (("1" (assert) nil nil)) nil) ("2" (rewrite "vz_distr_sub") (("2" (replaces -3) (("2" (assert) (("2" (lemma "Theta_H_vertical_dir") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replaces -1) (("2" (rewrite "vect2_zero") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((trk_circle_solution_2D formula-decl nil trk_circle nil) (sign_neg_clos application-judgement "Sign" sign "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (vertical_solution? const-decl "bool" vertical nil) (trk_circle? const-decl "bool" trk_circle nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nzreal nonempty-type-eq-decl nil reals nil) (vz_distr_sub formula-decl nil vectors_3D "vectors/") (Vector type-eq-decl nil vectors_3D "vectors/") (Theta_H_vertical_dir formula-decl nil vertical nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzv2 application-judgement "Nz_vect2" definitions_3D nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Theta_H const-decl "real" vertical nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (H formal-const-decl "posreal" trk_circle 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) (Theta_H_on_H formula-decl nil vertical nil) (vect2_zero formula-decl nil vect_3D_2D "vectors/") (trk_circle const-decl "{nvo | vect2(nvo) /= zero => trk_only?(vect2(vo))(vect2(nvo)) AND vo`z = nvo`z}" trk_circle nil) (circle_solution? const-decl "bool" circle_solutions nil) (Nzv2_vect3 type-eq-decl nil definitions_3D nil) (zero const-decl "Vector" vectors_2D "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (Vect3 type-eq-decl nil vectors_3D_def "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) (bool nonempty-type-eq-decl nil 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) (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)) nil)) (trk_circle_independence 0 (trk_circle_independence-2 nil 3431958632 ("" (skeep) (("" (lemma "trk_circle_solution") (("" (inst?) (("" (assert) (("" (lemma "circle_solution_independence") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((trk_circle_solution formula-decl nil trk_circle nil) (sign_neg_clos application-judgement "Sign" sign "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (nzreal nonempty-type-eq-decl nil reals nil) (Theta_H const-decl "real" vertical nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (Vector type-eq-decl nil vectors_3D "vectors/") (- const-decl "Vector" vectors_3D "vectors/") (H formal-const-decl "posreal" trk_circle nil) (D formal-const-decl "posreal" trk_circle 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) (circle_solution_independence formula-decl nil circle_solutions nil) (Nzv2_vect3 type-eq-decl nil definitions_3D nil) (zero const-decl "Vector" vectors_2D "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (Vect3 type-eq-decl nil vectors_3D_def "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) (bool nonempty-type-eq-decl nil 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) (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)) nil) (trk_circle_independence-1 nil 3431710189 ("" (skeep) (("" (skoletin 1 :postfix "p") (("" (flatten) (("" (case "vo`z = vi`z") (("1" (expand "trk_circle" :assert? none) (("1" (assert) nil nil)) nil) ("2" (lemma "trk_circle_D") (("2" (inst?) (("2" (assert) (("2" (lemma "trk_circle_H") (("2" (inst?) (("2" (assert) (("2" (replace -3 :dir rl) (("2" (expand "trk_circle" :assert? none) (("2" (lift-if) (("2" (split -) (("1" (flatten) nil nil) ("2" (flatten) (("2" (name-replace "t" "Theta_H(scal[3](s), scal[3](vo - vi), -eps)") (("2" (beta) (("2" (lift-if) (("2" (split -) (("1" (flatten) (("1" (split -) (("1" (flatten) nil nil) ("2" (flatten) (("2" (split -) (("1" (flatten) (("1" (replace -3 :dir rl) (("1" (lemma "circle_independence") (("1" (inst -1 "eps" "s + t * (nvop - vi)" "(nvop - vi)") (("1" (lemma "conflict_ever_shift") (("1" (inst? -1) (("1" (assert) (("1" (expand "circle_criterion?") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Sign type-eq-decl nil sign "reals/") (Nzv2_vect3 type-eq-decl nil definitions_3D nil) (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (sq_nz_pos application-judgement "posreal" sq "reals/") (sign_neg_clos application-judgement "Sign" sign "reals/") (Theta_H const-decl "real" vertical nil)) shostak)) (trk_circle_complete_TCC1 0 (trk_circle_complete_TCC1-1 nil 3464565407 ("" (skosimp*) (("" (expand "circle_solution?") (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil) ((circle_solution? const-decl "bool" circle_solutions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sign_neg_clos application-judgement "Sign" sign "reals/") (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) (nzv2 application-judgement "Nz_vect2" definitions_3D nil)) nil)) (trk_circle_complete 0 (trk_circle_complete-1 nil 3464081941 ("" (skeep) (("" (expand "circle_solution?") (("" (flatten) (("" (name-replace "t" "Theta_H(s`z, vo`z - vi`z, -dir)" :hide? nil) (("" (lemma "trk_only_circle_complete") (("" (rewrite "vect2_sub") (("" (inst -1 "dir" "nvo" "s" "t" "vi" "vo") (("1" (assert) (("1" (expand "trk_circle?") (("1" (expand "trk_only_circle?") (("1" (flatten) (("1" (assert) (("1" (skeep -1) (("1" (inst 4 "irt") (("1" (expand "trk_circle") (("1" (replaces -2) (("1" (replaces -1 :dir rl) (("1" (replaces -2) (("1" (hide-all-but 4) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((circle_solution? const-decl "bool" circle_solutions nil) (real_minus_real_is_real application-judgement "real" reals nil) (sign_neg_clos application-judgement "Sign" sign "reals/") (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities 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) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals 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) (bool nonempty-type-eq-decl nil booleans 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/") (>= 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) (H formal-const-decl "posreal" trk_circle nil) (Theta_H const-decl "real" vertical nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (Vector type-eq-decl nil vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Nzv2_vect3 type-eq-decl nil definitions_3D nil) (vect2_sub formula-decl nil vect_3D_2D "vectors/") (nzv2 application-judgement "Nz_vect2" definitions_3D nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (trk_only_circle? const-decl "bool" trk_only nil) (vect2_ext_id formula-decl nil vect_3D_2D "vectors/") (trk_circle const-decl "{nvo | vect2(nvo) /= zero => trk_only?(vect2(vo))(vect2(nvo)) AND vo`z = nvo`z}" trk_circle nil) (trk_circle? const-decl "bool" trk_circle nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (t skolem-const-decl "real" trk_circle nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (D formal-const-decl "posreal" trk_circle nil) (trk_only_circle_complete formula-decl nil trk_only nil)) nil)) (trk_vertical_eps 0 (trk_vertical_eps-1 nil 3471189119 ("" (skeep) (("" (skoletin 1 :postfix "p") (("" (flatten) (("" (expand "trk_vertical?") (("" (assert) (("" (expand "trk_vertical") (("" (lift-if) (("" (split -1) (("1" (flatten) (("1" (inst 2 "1") nil nil)) nil) ("2" (flatten) (("2" (split -1) (("1" (flatten) (("1" (inst 3 "-1") nil nil)) nil) ("2" (flatten) (("2" (inst 5 "1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((IFF const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (Vector type-eq-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Nzv2_vect3 type-eq-decl nil definitions_3D 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) (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) (bool nonempty-type-eq-decl nil booleans 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/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (trk_only? const-decl "bool" definitions nil) (trk_vertical const-decl "{nvo | vect2(nvo) /= zero => trk_only?(vect2(vo))(vect2(nvo)) AND vo`z = nvo`z}" trk_circle nil) (trk_vertical? const-decl "bool" trk_circle nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) shostak)) (trk_vertical_meets_horizontal_criterion 0 (trk_vertical_meets_horizontal_criterion-1 nil 3471187707 ("" (skeep) (("" (expand "trk_vertical?") (("" (flatten) (("" (skeep -1) (("" (expand "trk_vertical_irt" :assert? none) (("" (case-replace "vo`z = vi`z") (("1" (replaces -2) (("1" (assert) nil nil)) nil) ("2" (name "DIR" "sign(IF abs(sp`z) >= H THEN epsv * sign(sp`z) ELSE -1 ENDIF)") (("2" (case "IF abs(sp`z) >= H THEN epsv * sign(sp`z) ELSE -1 ENDIF = DIR") (("1" (hide -2) (("1" (replace -1) (("1" (assert) (("1" (lift-if -2) (("1" (split -2) (("1" (flatten) (("1" (split -3) (("1" (flatten) (("1" (replaces -2) (("1" (rewrite "vect2_sub") nil nil)) nil)) nil) ("2" (flatten) (("2" (replaces -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replaces -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (typepred "epsv") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((trk_vertical? const-decl "bool" trk_circle nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (real nonempty-type-from-decl nil reals nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Nzv2_vect3 type-eq-decl nil definitions_3D nil) (vect2_zero formula-decl nil vect_3D_2D "vectors/") (vect2_eq_ext formula-decl nil vect_3D_2D "vectors/") (nzv2 application-judgement "Nz_vect2" definitions_3D nil) (- const-decl "Vector" vectors_3D "vectors/") (Vector type-eq-decl nil vectors_3D "vectors/") (Theta_H const-decl "real" vertical nil) (nzreal nonempty-type-eq-decl nil reals nil) (trk_only_vertical const-decl "{nvo | nvo /= zero => trk_only?(vo)(nvo)}" trk_only nil) (trk_only? const-decl "bool" definitions nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (vect2_sub formula-decl nil vect_3D_2D "vectors/") (spv2 application-judgement "Sp_vect2[D]" trk_circle nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sign_neg_clos application-judgement "Sign" sign "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (odd_times_odd_is_odd application-judgement "odd_int" integers nil) (minus_real_is_real application-judgement "real" reals nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (sign_mult_clos application-judgement "Sign" sign "reals/") (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (minus_odd_is_odd application-judgement "odd_int" integers 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) (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) (bool nonempty-type-eq-decl nil booleans 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/") (sign const-decl "Sign" sign "reals/") (IF const-decl "[boolean, T, T -> T]" if_def nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (nnreal type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (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" trk_circle nil) (H formal-const-decl "posreal" trk_circle nil) (Sp2_vect3 type-eq-decl nil space_3D nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (trk_vertical_irt const-decl "{nvo | vect2(nvo) /= zero => trk_only?(vect2(vo))(vect2(nvo)) AND vo`z = nvo`z}" trk_circle nil)) nil)) (trk_vertical_meets_vertical_criterion 0 (trk_vertical_meets_vertical_criterion-1 nil 3471189334 ("" (skeep) (("" (expand "trk_vertical?") (("" (flatten) (("" (skeep -1) (("" (expand "trk_vertical_irt" :assert? none) (("" (case-replace "vo`z = vi`z") (("1" (replaces -2) (("1" (assert) nil nil)) nil) ("2" (name "DIR" "sign(IF abs(s`z) >= H THEN epsv * sign(s`z) ELSE -1 ENDIF)") (("2" (case "IF abs(s`z) >= H THEN epsv * sign(s`z) ELSE -1 ENDIF = DIR") (("1" (hide -2) (("1" (replace -1) (("1" (assert) (("1" (lift-if -2) (("1" (split -2) (("1" (flatten) (("1" (split -3) (("1" (flatten) (("1" (hide -1) (("1" (name-replace "trko" "trk_only_vertical(vect2(s), vect2(vo), vect2(vi), Theta_H(s`z, (vo - vi)`z, -DIR), DIR,irt)" :hide? nil) (("1" (lemma "trk_only_vertical_on_D") (("1" (inst -1 "DIR" "trko" "s" "Theta_H(s`z, (vo - vi)`z, -DIR)" "vi" "vo") (("1" (beta) (("1" (split -1) (("1" (flatten) (("1" (lemma "horizontal_meets_vertical_criterion") (("1" (inst -1 "epsv" "nvo" "s" "vi" "vo") (("1" (replaces -9) (("1" (replaces -6) (("1" (assert) (("1" (rewrite "vect2_sub") (("1" (rewrite "vect2_sub") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "trk_only_vertical?") (("2" (split 1) (("1" (flatten) (("1" (replaces -1) (("1" (replaces -2) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (inst 1 "irt") (("2" (replaces -1) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replaces -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replaces -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (typepred "epsv") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((trk_vertical? const-decl "bool" trk_circle nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (real nonempty-type-from-decl nil reals nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Nzv2_vect3 type-eq-decl nil definitions_3D nil) (vect2_zero formula-decl nil vect_3D_2D "vectors/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (- const-decl "Vector" vectors_3D "vectors/") (Vector type-eq-decl nil vectors_3D "vectors/") (Theta_H const-decl "real" vertical nil) (nzreal nonempty-type-eq-decl nil reals nil) (trk_only_vertical const-decl "{nvo | nvo /= zero => trk_only?(vo)(nvo)}" trk_only nil) (D formal-const-decl "posreal" trk_circle nil) (trk_only? const-decl "bool" definitions nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nzv2 application-judgement "Nz_vect2" definitions_3D nil) (s skolem-const-decl "Vect3" trk_circle nil) (vo skolem-const-decl "Nzv2_vect3" trk_circle nil) (vi skolem-const-decl "Nzv2_vect3" trk_circle nil) (DIR skolem-const-decl "Sign" trk_circle nil) (horizontal_meets_vertical_criterion formula-decl nil vertical_criterion nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (vect2_eq_ext formula-decl nil vect_3D_2D "vectors/") (vect2_sub formula-decl nil vect_3D_2D "vectors/") (trk_only_vertical? const-decl "bool" trk_only nil) (trk_only_vertical_on_D formula-decl nil trk_only nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sign_neg_clos application-judgement "Sign" sign "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (odd_times_odd_is_odd application-judgement "odd_int" integers nil) (minus_real_is_real application-judgement "real" reals nil) (sign_mult_clos application-judgement "Sign" sign "reals/") (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (minus_odd_is_odd application-judgement "odd_int" integers 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) (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) (bool nonempty-type-eq-decl nil booleans 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/") (sign const-decl "Sign" sign "reals/") (IF const-decl "[boolean, T, T -> T]" if_def nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (H formal-const-decl "posreal" trk_circle nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (trk_vertical_irt const-decl "{nvo | vect2(nvo) /= zero => trk_only?(vect2(vo))(vect2(nvo)) AND vo`z = nvo`z}" trk_circle nil)) nil))) ¤ Dauer der Verarbeitung: 0.70 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 |
