| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/vectors/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 190 kB |
|
Quellcode-Bibliothek intersections_2D.prfSprache: Lisp |
|||||||||||||||
|
(intersections_2D (det_line 0 (det_line-1 nil 3430227348 ("" (skosimp*) (("" (assert) (("" (flatten) (("" (split +) (("1" (expand "det") (("1" (assert) (("1" (grind) nil nil)) nil)) nil) ("2" (expand "det") (("2" (assert) (("2" (grind) (("2" (move-terms -1 r 1) (("2" (mult-by -1 "L0!1`v`y") (("2" (replace -1 * rl) (("2" (hide -1) (("2" (assert) (("2" (move-terms -1 r 1) (("2" (mult-by -1 "L0!1`v`x") (("2" (replace -1 * rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (+ const-decl "Vector" vectors_2D nil) (* const-decl "Vector" vectors_2D nil) (- const-decl "Vector" vectors_2D nil) (real_plus_real_is_real application-judgement "real" reals nil) (det const-decl "real" det_2D nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (Vect2 type-eq-decl nil vectors_2D_def nil) (Nz_vect2 type-eq-decl nil vectors_2D nil) (Line2D type-eq-decl nil lines_2D nil) (* const-decl "[numfield, numfield -> numfield]" 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 "[numfield, numfield -> numfield]" number_fields nil) (both_sides_times1_imp formula-decl nil extra_real_props nil)) nil)) (intersect_pt_TCC1 0 (intersect_pt_TCC1-1 nil 3267433756 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (/= const-decl "boolean" notequal nil) (real nonempty-type-from-decl nil reals nil) (Vect2 type-eq-decl nil vectors_2D_def 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) (Nz_vect2 type-eq-decl nil vectors_2D nil) (Line2D type-eq-decl nil lines_2D nil) (real_minus_real_is_real application-judgement "real" reals nil) (- const-decl "Vector" vectors_2D nil) (det const-decl "real" det_2D nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (same_line_sym 0 (same_line_sym-1 nil 3267891274 ("" (skosimp*) (("" (expand "same_line?") (("" (flatten) (("" (rewrite "cross_asym" +) (("" (assert) (("" (expand "cross") (("" (grind) (("" (mult-by -2 "L1!1`v`y") (("" (assert) (("" (mult-by 1 "L0!1`v`y") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) (("2" (assert) (("2" (mult-cases -3) (("1" (replace -1) (("1" (assert) (("1" (case "L1!1`v`y = 0") (("1" (hide -4) (("1" (replace -1) (("1" (assert) (("1" (typepred "L0!1`v") (("1" (flatten) (("1" (lemma "norm_xy_eq_0") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (typepred "L0!1`v") (("2" (flatten) (("2" (lemma "norm_xy_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (factor 1 l) (("2" (reveal -3) (("2" (assert) (("2" (replace -2) (("2" (replace -3) (("2" (assert) (("2" (factor 1 l) (("2" (factor -1 l) (("2" (mult-cases -1) (("2" (typepred "L0!1`v") (("2" (flatten) (("2" (lemma "norm_xy_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((same_line? const-decl "bool" intersections_2D nil) (both_sides_times1_imp formula-decl nil extra_real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (Line2D type-eq-decl nil lines_2D nil) (Nz_vect2 type-eq-decl nil vectors_2D nil) (Vect2 type-eq-decl nil vectors_2D_def 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) (both_sides_times1 formula-decl nil real_props nil) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (L0!1 skolem-const-decl "Line2D" intersections_2D nil) (= const-decl "[T, T -> boolean]" equalities nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (zero_times3 formula-decl nil real_props nil) (nz_norm_gt_0 application-judgement "posreal" vectors_2D nil) (norm_xy_eq_0 formula-decl nil vectors_2D nil) (zero const-decl "Vector" vectors_2D nil) (Vector type-eq-decl nil vectors_2D nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (det const-decl "real" det_2D nil) (- const-decl "Vector" vectors_2D nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (intersect_not_parallel 0 (intersect_not_parallel-1 nil 3267453794 ("" (skosimp*) (("" (expand "intersect?") (("" (expand "parallel?") (("" (flatten) (("" (skosimp*) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((intersect? const-decl "bool" intersections_2D nil) (nz_nzv application-judgement "Nz_vector" vectors_2D nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (det const-decl "real" det_2D nil) (* const-decl "Vector" vectors_2D nil) (parallel? const-decl "bool" vectors_2D nil)) shostak)) (intersection_lem 0 (intersection_lem-2 nil 3430226638 ("" (skosimp*) (("" (skoletin* 2) (("" (replace -1) (("" (replace -2) (("" (hide -1 -2) (("" (apply-extensionality 1 :hide? t) (("1" (expand "*") (("1" (expand "+") (("1" (field 1) (("1" (replace -1) (("1" (expand "det") (("1" (assert) (("1" (expand "-") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "*") (("2" (expand "+") (("2" (field 1) (("2" (replace -1) (("2" (expand "-") (("2" (expand "det") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((NOT const-decl "[bool -> bool]" booleans nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_2D nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (- const-decl "Vector" vectors_2D nil) (Vect2 type-eq-decl nil vectors_2D_def nil) (Nz_vect2 type-eq-decl nil vectors_2D nil) (Line2D type-eq-decl nil lines_2D nil) (number nonempty-type-decl nil numbers nil) (/= const-decl "boolean" notequal 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) (det const-decl "real" det_2D nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "Vector" vectors_2D nil) (* const-decl "Vector" vectors_2D nil) (real_minus_real_is_real application-judgement "real" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (both_sides_times1 formula-decl nil real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil) (intersection_lem-1 nil 3267438142 ("" (skosimp*) (("" (skoletin 2) (("" (skoletin 1) (("" (skoletin 1) (("" (replace -1) (("" (replace -2) (("" (hide -1 -2) (("" (apply-extensionality 1 :hide? t) (("1" (expand "*") (("1" (expand "+") (("1" (field 1) (("1" (replace -2) (("1" (expand "cross") (("1" (assert) (("1" (expand "-") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "*") (("2" (expand "+") (("2" (field 1) (("2" (replace -2) (("2" (expand "-") (("2" (expand "cross") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Line2D type-eq-decl nil lines_2D nil) (Nz_vect2 type-eq-decl nil vectors_2D nil) (Vect2 type-eq-decl nil vectors_2D_def nil) (Vector type-eq-decl nil vectors_2D nil) (+ const-decl "Vector" vectors_2D nil) (* const-decl "Vector" vectors_2D nil)) nil)) (lines_intersection_TCC1 0 (lines_intersection_TCC1-1 nil 3543442415 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_2D nil) (zero const-decl "Vector" vectors_2D nil) (Nz_vect2 type-eq-decl nil vectors_2D nil) (number nonempty-type-decl nil numbers nil) (Vect2 type-eq-decl nil vectors_2D_def 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_minus_real_is_real application-judgement "real" reals nil) (- const-decl "Vector" vectors_2D nil) (det const-decl "real" det_2D nil) (/= const-decl "boolean" notequal nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (lines_intersection_sound 0 (lines_intersection_sound-1 nil 3543444841 ("" (skeep :preds? t) (("" (lemma "intersection_lem") (("" (inst -1 "(so,vo)" "(si,vi)") (("" (assert) (("" (expand "lines_intersection") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((intersection_lem formula-decl nil intersections_2D nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (lines_intersection const-decl "[real, real]" intersections_2D nil) (det const-decl "real" det_2D 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) (zero const-decl "Vector" vectors_2D nil) (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D nil) (real nonempty-type-from-decl nil reals nil) (Line2D type-eq-decl nil lines_2D nil) (Nz_vect2 type-eq-decl nil vectors_2D nil) (Vect2 type-eq-decl nil vectors_2D_def nil)) nil)) (pt_intersect 0 (pt_intersect-9 nil 3430227167 ("" (skosimp*) (("" (expand "on_line?") (("" (skosimp*) (("" (expand "intersect?") (("" (flatten) (("" (replace -1) (("" (hide -1) (("" (name "DELTA" "L1!1`p - L0!1`p") (("" (case "x!1 * v(L0!1) - x!2 * v(L1!1) = DELTA") (("1" (hide -3) (("1" (expand "same_line?") (("1" (assert) (("1" (case "det(L0!1`v,L1!1`v)*x!2 = det(DELTA,L0!1`v) ") (("1" (case "det(L0!1`v,L1!1`v)*x!1 = det(DELTA,L1!1`v) ") (("1" (replace -5) (("1" (assert) nil nil)) nil) ("2" (hide -1 2) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (expand "det") (("2" (assert) (("2" (expand "-") (("2" (expand "*") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (expand "det") (("2" (expand "-") (("2" (expand "*") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace -1 * rl) (("2" (lemma "add_move_right") (("2" (hide -2) (("2" (inst?) (("2" (assert) (("2" (replace -1) (("2" (hide -2) (("2" (apply-extensionality 1 :hide? t) (("1" (expand "-") (("1" (expand "*") (("1" (expand "+") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "-") (("2" (expand "+ ") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((on_line? const-decl "bool" lines_2D nil) (intersect? const-decl "bool" intersections_2D nil) (Line2D type-eq-decl nil lines_2D nil) (Nz_vect2 type-eq-decl nil vectors_2D nil) (Vect2 type-eq-decl nil vectors_2D_def nil) (- const-decl "Vector" vectors_2D nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D nil) (real nonempty-type-from-decl nil reals nil) (add_move_right formula-decl nil vectors_2D nil) (+ const-decl "Vector" vectors_2D nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (det const-decl "real" det_2D nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_times_real_is_real application-judgement "real" reals nil) (same_line? const-decl "bool" intersections_2D 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) (* const-decl "Vector" vectors_2D nil)) nil) (pt_intersect-8 nil 3269337859 ("" (skosimp*) (("" (expand "on_line?") (("" (skosimp*) (("" (expand "intersect?") (("" (flatten) (("" (replace -1) (("" (hide -1) (("" (name "DELTA" "L1!1`p - L0!1`p") (("" (case "x!1 * v(L0!1) - x!2 * v(L1!1) = DELTA") (("1" (hide -3) (("1" (expand "same_line?") (("1" (assert) (("1" (case "cross(L0!1`v,L1!1`v)*x!2 = cross(DELTA,L0!1`v) ") (("1" (case "cross(L0!1`v,L1!1`v)*x!1 = cross(DELTA,L1!1`v) ") (("1" (replace -5) (("1" (assert) nil nil)) nil) ("2" (hide -1 2) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (expand "cross") (("2" (assert) (("2" (expand "-") (("2" (expand "*") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (expand "cross") (("2" (expand "-") (("2" (expand "*") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace -1 * rl) (("2" (lemma "add_move_right") (("2" (hide -2) (("2" (inst?) (("2" (assert) (("2" (replace -1) (("2" (hide -2) (("2" (apply-extensionality 1 :hide? t) (("1" (expand "-") (("1" (expand "*") (("1" (expand "+") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "-") (("2" (expand "+ ") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((on_line? const-decl "bool" lines_2D nil) (Line2D type-eq-decl nil lines_2D nil) (Nz_vect2 type-eq-decl nil vectors_2D nil) (Vect2 type-eq-decl nil vectors_2D_def nil) (Vector type-eq-decl nil vectors_2D nil) (add_move_right formula-decl nil vectors_2D nil) (+ const-decl "Vector" vectors_2D nil) (* const-decl "Vector" vectors_2D nil)) nil) (pt_intersect-7 nil 3269337834 ("" (skosimp*) (("" (expand "on_line?") (("" (skosimp*) (("" (expand "intersect?") (("" (flatten) (("" (replace -1) (("" (hide -1) (("" (name "DELTA" "L1!1`p - L0!1`p") (("" (case "x!1 * v(L0!1) - x!2 * v(L1!1) = DELTA") (("1" (hide -3) (("1" (expand "same_line?") (("1" (assert) (("1" (case "cross(L0!1`v,L1!1`v)*x!2 = cross(DELTA,L0!1`v) ") (("1" (case "cross(L0!1`v,L1!1`v)*x!1 = cross(DELTA,L1!1`v) ") (("1" (replace -5) (("1" (assert) nil))) ("2" (hide -1 2) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (expand "cross") (("2" (assert) (("2" (expand "-") (("2" (expand "*") (("2" (assert) nil))))))))))))))))) ("2" (hide 2) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (expand "cross") (("2" (expand "-") (("2" (expand "*") (("2" (assert) nil))))))))))))))))))))) ("2" (assert) (("2" (replace -1 * rl) (("2" (lemma "add_move_left") (("2" (hide -2) (("2" (inst -1 "p(L1!1)" "x!2 * v(L1!1)" "p(L0!1) + x!1 * v(L0!1)") (("2" (assert) (("2" (hide -2) (("2" (apply-extensionality 1 :hide? t) (("1" (expand "-") (("1" (expand "*") (("1" (expand "+") (("1" (lemma "comp_eq_x") (("1" (inst?) (("1" (assert) nil))))))))))) ("2" (expand "-") (("2" (expand "+ ") (("2" (expand "*") (("2" (lemma "comp_eq_y") (("2" (inst?) (("2" (assert) nil)))))))))))))))))))))))))))))))))))))))))))) nil) nil nil) (pt_intersect-6 nil 3269337779 ("" (skosimp*) (("" (expand "on_line?") (("" (skosimp*) (("" (expand "intersect?") (("" (flatten) (("" (replace -1) (("" (hide -1) (("" (name "DELTA" "L1!1`p - L0!1`p") (("" (case "x!1 * v(L0!1) - x!2 * v(L1!1) = DELTA") (("1" (hide -3) (("1" (expand "same_line?") (("1" (assert) (("1" (case "cross(L0!1`v,L1!1`v)*x!2 = cross(DELTA,L0!1`v) ") (("1" (case "cross(L0!1`v,L1!1`v)*x!1 = cross(DELTA,L1!1`v) ") (("1" (replace -5) (("1" (assert) nil))) ("2" (hide -1 2) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (expand "cross") (("2" (assert) (("2" (expand "-") (("2" (expand "*") (("2" (assert) nil))))))))))))))))) ("2" (hide 2) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (expand "cross") (("2" (expand "-") (("2" (expand "*") (("2" (assert) nil))))))))))))))))))))) ("2" (assert) (("2" (replace -1 * rl) (("2" (lemma "add_move_right") (("2" (hide -2) (("2" (inst -1 "p(L1!1)" "x!2 * v(L1!1)" "p(L0!1) + x!1 * v(L0!1)") (("2" (assert) (("2" (hide -2) (("2" (apply-extensionality 1 :hide? t) (("1" (expand "-") (("1" (expand "*") (("1" (expand "+") (("1" (lemma "comp_eq_x") (("1" (inst?) (("1" (assert) nil))))))))))) ("2" (expand "-") (("2" (expand "+ ") (("2" (expand "*") (("2" (lemma "comp_eq_y") (("2" (inst?) (("2" (assert) nil)))))))))))))))))))))))))))))))))))))))))))) nil) nil nil) (pt_intersect-5 nil 3269337644 ("" (skosimp*) (("" (expand "on_line?") (("" (skosimp*) (("" (expand "intersect?") (("" (flatten) (("" (replace -1) (("" (hide -1) (("" (name "DELTA" "L1!1`p - L0!1`p") (("" (case "x!1 * v(L0!1) - x!2 * v(L1!1) = DELTA") (("1" (hide -3) (("1" (expand "same_line?") (("1" (assert) (("1" (case "cross(L0!1`v,L1!1`v)*x!2 = cross(DELTA,L0!1`v) ") (("1" (case "cross(L0!1`v,L1!1`v)*x!1 = cross(DELTA,L1!1`v) ") (("1" (replace -5) (("1" (assert) nil))) ("2" (hide -1 2) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (expand "cross") (("2" (assert) (("2" (expand "-") (("2" (expand "*") (("2" (assert) nil))))))))))))))))) ("2" (hide 2) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (expand "cross") (("2" (expand "-") (("2" (expand "*") (("2" (assert) nil))))))))))))))))))))) ("2" (assert) (("2" (replace -1 * rl) (("2" (lemma "add_move_right") (("2" (hide -2) (("2" (inst -1 "p(L1!1)" "x!2 * v(L1!1)" "p(L0!1) + x!1 * v(L0!1)") (("2" (assert) (("2" (hide -2) (("2" (apply-extensionality 1 :hide? t) (("1" (expand "-") (("1" (expand "*") (("1" (expand "+") (("1" (lemma "comp_x_eq") (("1" (inst?) (("1" (assert) nil))))))))))) ("2" (expand "-") (("2" (expand "+ ") (("2" (expand "*") (("2" (lemma "comp_y_eq") (("2" (inst?) (("2" (assert) nil)))))))))))))))))))))))))))))))))))))))))))) nil) nil nil) (pt_intersect-4 nil 3269337590 ("" (skosimp*) (("" (expand "on_line?") (("" (skosimp*) (("" (expand "intersect?") (("" (flatten) (("" (replace -1) (("" (hide -1) (("" (name "DELTA" "L1!1`p - L0!1`p") (("" (case "x!1 * v(L0!1) - x!2 * v(L1!1) = DELTA") (("1" (hide -3) (("1" (expand "same_line?") (("1" (assert) (("1" (case "cross(L0!1`v,L1!1`v)*x!2 = cross(DELTA,L0!1`v) ") (("1" (case "cross(L0!1`v,L1!1`v)*x!1 = cross(DELTA,L1!1`v) ") (("1" (replace -5) (("1" (assert) nil))) ("2" (hide -1 2) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (expand "cross") (("2" (assert) (("2" (expand "-") (("2" (expand "*") (("2" (assert) nil))))))))))))))))) ("2" (hide 2) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (expand "cross") (("2" (expand "-") (("2" (expand "*") (("2" (assert) nil))))))))))))))))))))) ("2" (assert) (("2" (replace -1 * rl) (("2" (lemma "add_move_right") (("2" (hide -2) (("2" (inst -1 "p(L1!1)" "x!2 * v(L1!1)" "p(L0!1) + x!1 * v(L0!1)") (("2" (assert) (("2" (hide -2) (("2" (apply-extensionality 1 :hide? t) (("1" (expand "-") (("1" (expand "*") (("1" (expand "+") (("1" (lemma "comp_eq_x") (("1" (inst?) (("1" (assert) nil))))))))))) ("2" (expand "-") (("2" (expand "+ ") (("2" (expand "*") (("2" (lemma "comp_eq_y") (("2" (inst?) (("2" (assert) nil)))))))))))))))))))))))))))))))))))))))))))) nil) nil nil) (pt_intersect-3 nil 3269337494 ("" (skosimp*) (("" (expand "on_line?") (("" (skosimp*) (("" (expand "intersect?") (("" (flatten) (("" (replace -1) (("" (hide -1) (("" (name "DELTA" "L1!1`p - L0!1`p") (("" (case "x!1 * v(L0!1) - x!2 * v(L1!1) = DELTA") (("1" (hide -3) (("1" (expand "same_line?") (("1" (assert) (("1" (case "cross(L0!1`v,L1!1`v)*x!2 = cross(DELTA,L0!1`v) ") (("1" (case "cross(L0!1`v,L1!1`v)*x!1 = cross(DELTA,L1!1`v) ") (("1" (replace -5) (("1" (assert) nil))) ("2" (hide -1 2) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (expand "cross") (("2" (assert) (("2" (expand "-") (("2" (expand "*") (("2" (assert) nil))))))))))))))))) ("2" (hide 2) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (expand "cross") (("2" (expand "-") (("2" (expand "*") (("2" (assert) nil))))))))))))))))))))) ("2" (assert) (("2" (replace -1 * rl) (("2" (lemma "add_cancel_left") (("2" (hide -2) (("2" (inst -1 "p(L1!1)" "x!2 * v(L1!1)" "p(L0!1) + x!1 * v(L0!1)") (("2" (assert) (("2" (hide -2) (("2" (apply-extensionality 1 :hide? t) (("1" (expand "-") (("1" (expand "*") (("1" (expand "+") (("1" (lemma "comp_eq_x") (("1" (inst?) (("1" (assert) nil))))))))))) ("2" (expand "-") (("2" (expand "+ ") (("2" (expand "*") (("2" (lemma "comp_eq_y") (("2" (inst?) (("2" (assert) nil)))))))))))))))))))))))))))))))))))))))))))) nil) nil nil) (pt_intersect-2 nil 3269337451 ("" (skosimp*) (("" (expand "on_line?") (("" (skosimp*) (("" (expand "intersect?") (("" (flatten) (("" (replace -1) (("" (hide -1) (("" (name "DELTA" "L1!1`p - L0!1`p") (("" (case "x!1 * v(L0!1) - x!2 * v(L1!1) = DELTA") (("1" (hide -3) (("1" (expand "same_line?") (("1" (assert) (("1" (case "cross(L0!1`v,L1!1`v)*x!2 = cross(DELTA,L0!1`v) ") (("1" (case "cross(L0!1`v,L1!1`v)*x!1 = cross(DELTA,L1!1`v) ") (("1" (replace -5) (("1" (assert) nil))) ("2" (hide -1 2) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (expand "cross") (("2" (assert) (("2" (expand "-") (("2" (expand "*") (("2" (assert) nil))))))))))))))))) ("2" (hide 2) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (expand "cross") (("2" (expand "-") (("2" (expand "*") (("2" (assert) nil))))))))))))))))))))) ("2" (assert) (("2" (replace -1 * rl) (("2" (lemma "add_move_left") (("2" (hide -2) (("2" (inst -1 "p(L1!1)" "x!2 * v(L1!1)" "p(L0!1) + x!1 * v(L0!1)") (("2" (assert) (("2" (hide -2) (("2" (apply-extensionality 1 :hide? t) (("1" (expand "-") (("1" (expand "*") (("1" (expand "+") (("1" (lemma "comp_eq_x") (("1" (inst?) (("1" (assert) nil))))))))))) ("2" (expand "-") (("2" (expand "+ ") (("2" (expand "*") (("2" (lemma "comp_eq_y") (("2" (inst?) (("2" (assert) nil)))))))))))))))))))))))))))))))))))))))))))) nil) nil nil) (pt_intersect-1 nil 3267457715 ("" (skosimp*) (("" (expand "on_line?") (("" (skosimp*) (("" (expand "intersect?") (("" (flatten) (("" (replace -1) (("" (hide -1) (("" (name "DELTA" "L1!1`p - L0!1`p") (("" (case "x!1 * v(L0!1) - x!2 * v(L1!1) = DELTA") (("1" (hide -3) (("1" (expand "same_line?") (("1" (assert) (("1" (case "cross(L0!1`v,L1!1`v)*x!2 = cross(DELTA,L0!1`v) ") (("1" (case "cross(L0!1`v,L1!1`v)*x!1 = cross(DELTA,L1!1`v) ") (("1" (replace -5) (("1" (assert) nil nil)) nil) ("2" (hide -1 2) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (expand "cross") (("2" (assert) (("2" (expand "-") (("2" (expand "*") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (expand "cross") (("2" (expand "-") (("2" (expand "*") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace -1 * rl) (("2" (lemma "move_left") (("2" (hide -2) (("2" (inst -1 "p(L1!1)" "x!2 * v(L1!1)" "p(L0!1) + x!1 * v(L0!1)") (("2" (assert) (("2" (hide -2) (("2" (apply-extensionality 1 :hide? t) (("1" (expand "-") (("1" (expand "*") (("1" (expand "+ ") (("1" (lemma "comp_eq_x") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "-") (("2" (expand "+ ") (("2" (expand "*") (("2" (lemma "comp_eq_y") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((add_move_right formula-decl nil vectors_2D nil) (comp_eq_y formula-decl nil vectors_2D nil) (comp_eq_x formula-decl nil vectors_2D nil) (on_line? const-decl "bool" lines_2D nil) (Line2D type-eq-decl nil lines_2D nil) (Nz_vect2 type-eq-decl nil vectors_2D nil) (Vector type-eq-decl nil vectors_2D nil) (+ const-decl "Vector" vectors_2D nil) (* const-decl "Vector" vectors_2D nil)) shostak)) (intersect_pt_unique_TCC1 0 (intersect_pt_unique_TCC1-1 nil 3267450311 ("" (skosimp*) (("" (expand "intersect?") (("" (assert) nil nil)) nil)) nil) ((intersect? const-decl "bool" intersections_2D nil)) shostak)) (intersect_pt_unique 0 (intersect_pt_unique-1 nil 3267438517 ("" (skosimp*) (("" (expand "on_line?") (("" (skosimp*) (("" (expand "intersect?") (("" (expand "intersect_pt") (("" (replace -2) (("" (hide -2) (("" (name "DELTA" "L1!1`p - L0!1`p") (("" (replace -1) (("" (case "x!1 = det(DELTA,L1!1`v)/det(L0!1`v,L1!1`v)") (("1" (case "x!2 = det(DELTA,L0!1`v)/det(L0!1`v,L1!1`v)") (("1" (replace -2) (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (lemma "intersection_lem") (("2" (inst?) (("2" (assert) (("2" (replace -3) (("2" (replace -2 * rl) (("2" (replace -1) (("2" (hide -1) (("2" (lemma "scal_cancel") (("2" (hide -2 -3) (("2" (inst?) (("2" (inst -1 "L1!1`v") (("2" (assert) (("2" (hide 2) (("2" (lemma "add_cancel_left") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (cross-mult 1) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (expand "det") (("2" (expand "-") (("2" (case "p(L0!1)`x + x!1 * v(L0!1)`x = p(L1!1)`x + x!2 * v(L1!1)`x") (("1" (case "p(L0!1)`y + x!1 * v(L0!1)`y = p(L1!1)`y + x!2 * v(L1!1)`y") (("1" (hide -4) (("1" (mult-by -1 "L1!1`v`x") (("1" (mult-by -2 "L1!1`v`y") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (hide -1 -2) (("2" (lemma "comp_eq_y") (("2" (inst?) (("2" (split -1) (("1" (expand "+ ") (("1" (assert) (("1" (expand "*") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "comp_eq_x") (("2" (inst?) (("2" (expand "*") (("2" (expand "+ ") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((on_line? const-decl "bool" lines_2D nil) (intersect? const-decl "bool" intersections_2D nil) (Line2D type-eq-decl nil lines_2D nil) (Nz_vect2 type-eq-decl nil vectors_2D nil) (Vect2 type-eq-decl nil vectors_2D_def nil) (- const-decl "Vector" vectors_2D nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D nil) (real nonempty-type-from-decl nil reals nil) (det const-decl "real" det_2D 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) (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) (real_div_nzreal_is_real application-judgement "real" reals nil) (scal_cancel formula-decl nil vectors_2D nil) (add_cancel_left formula-decl nil vectors_2D nil) (* const-decl "Vector" vectors_2D nil) (zero const-decl "Vector" vectors_2D nil) (Nz_vector type-eq-decl nil vectors_2D nil) (intersection_lem formula-decl nil intersections_2D nil) (div_cancel4 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (real_times_real_is_real application-judgement "real" reals nil) (comp_eq_x formula-decl nil vectors_2D nil) (both_sides_times1_imp formula-decl nil extra_real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (comp_eq_y formula-decl nil vectors_2D nil) (+ const-decl "Vector" vectors_2D nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_plus_real_is_real application-judgement "real" reals nil) (intersect_pt const-decl "Vect2" intersections_2D nil)) shostak)) (same_line_lem 0 (same_line_lem-4 nil 3440252936 ("" (skosimp*) (("" (lemma "pt_intersect") (("" (inst - "L0!1" "L1!1" "p1!1") (("" (assert) (("" (expand "intersect?") (("" (flatten) (("" (expand "same_line?") (("" (hide 3) (("" (expand "det") (("" (expand "on_line?") (("" (skosimp*) (("" (replace -1) (("" (hide -1) (("" (replace -2) (("" (hide -2) (("" (case-replace " x!1 * v(L0!1) - x!2 * v(L1!1) = p(L1!1) - p(L0!1)") (("1" (hide -2) (("1" (case-replace " x!3 * v(L0!1) - x!4 * v(L1!1) = p(L1!1) - p(L0!1)") (("1" (hide -3) (("1" (replace -1 * rl) (("1" (hide -1) (("1" (assert) (("1" (case-replace "(x!1 - x!3)*v(L0!1) = (x!2 - x!4) * v(L1!1)") (("1" (case-replace "(x!2 - x!4) = 0") (("1" (assert) (("1" (move-terms -1 l 2) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "x!1 = x!3") (("1" (case-replace "v(L0!1) = zero") (("1" (assert) nil nil) ("2" (hide -2 3 4) (("2" (lemma "scal_eq_zero") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "v(L1!1) = ((x!1 - x!3)/(x!2 - x!4))* v(L0!1)") (("1" (lemma "comp_eq_x") (("1" (inst?) (("1" (expand "*" -1) (("1" (assert) (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "comp_eq_y") (("1" (inst?) (("1" (expand "*" -1) (("1" (split -1) (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (replace -1) (("2" (apply-extensionality 1 :hide? t) (("1" (assert) (("1" (expand "*") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "*") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "*") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3 4) (("2" (expand "*") (("2" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil) ("2" (apply-extensionality 1 :hide? t) (("1" (hide 2 3) (("1" (lemma "comp_eq_x") (("1" (inst - "x!1 * v(L0!1) - x!2 * v(L1!1)" "x!3 * v(L0!1) - x!4 * v(L1!1)") (("1" (expand "-") (("1" (expand "*") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (lemma "comp_eq_y") (("2" (inst - "x!1 * v(L0!1) - x!2 * v(L1!1)" "x!3 * v(L0!1) - x!4 * v(L1!1)") (("2" (expand "*") (("2" (expand "-") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (apply-extensionality 1 :hide? t) (("1" (hide -1) (("1" (lemma "comp_eq_x") (("1" (inst - "p(L0!1) + x!3 * v(L0!1)" "p(L1!1) + x!4 * v(L1!1)") (("1" (expand "+ ") (("1" (expand "*") (("1" (assert) (("1" (expand "-") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (lemma "comp_eq_y") (("2" (inst - "p(L0!1) + x!3 * v(L0!1)" "p(L1!1) + x!4 * v(L1!1)") (("2" (expand "*") (("2" (expand "-") (("2" (expand "+ ") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2 3) (("2" (apply-extensionality 1 :hide? t) (("1" (lemma "comp_eq_x") (("1" (inst?) (("1" (expand "*") (("1" (expand "-") (("1" (expand "+ ") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "comp_eq_y") (("2" (inst?) (("2" (expand "*") (("2" (expand "-") (("2" (expand "+ ") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((pt_intersect formula-decl nil intersections_2D nil) (on_line? const-decl "bool" lines_2D nil) (Vector type-eq-decl nil vectors_2D nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (- const-decl "Vector" vectors_2D 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) (* const-decl "Vector" vectors_2D nil) (real_minus_real_is_real application-judgement "real" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (real_plus_real_is_real application-judgement "real" reals nil) (scal_eq_zero formula-decl nil vectors_2D nil) (zero const-decl "Vector" vectors_2D nil) (scal_0 formula-decl nil vectors_2D nil) (comp_eq_x formula-decl nil vectors_2D nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (scal_assoc formula-decl nil vectors_2D nil) (comp_eq_y formula-decl nil vectors_2D nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "Vector" vectors_2D nil) (det const-decl "real" det_2D nil) (real_times_real_is_real application-judgement "real" reals nil) (same_line? const-decl "bool" intersections_2D nil) (intersect? const-decl "bool" intersections_2D nil) (real nonempty-type-from-decl nil reals nil) (Line2D type-eq-decl nil lines_2D nil) (Nz_vect2 type-eq-decl nil vectors_2D nil) (Vect2 type-eq-decl nil vectors_2D_def nil)) nil) (same_line_lem-3 nil 3440246298 ("" (skosimp*) (("" (lemma "pt_intersect") (("" (inst - "L0!1" "L1!1" "p1!1") (("" (assert) (("" (expand "intersect?") (("" (flatten) (("" (expand "same_line?") (("" (hide 3) (("" (expand "det") (("" (expand "on_line?") (("" (skosimp*) (("" (replace -1) (("" (hide -1) (("" (replace -2) (("" (hide -2) (("" (case-replace " x!1 * v(L0!1) - x!2 * v(L1!1) = p(L1!1) - p(L0!1)") (("1" (hide -2) (("1" (case-replace " x!3 * v(L0!1) - x!4 * v(L1!1) = p(L1!1) - p(L0!1)") (("1" (hide -3) (("1" (replace -1 * rl) (("1" (hide -1) (("1" (assert) (("1" (case-replace "(x!1 - x!3)*v(L0!1) = (x!2 - x!4) * v(L1!1)") (("1" (case-replace "(x!2 - x!4) = 0") (("1" (assert) (("1" (move-terms -1 l 2) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "x!1 = x!3") (("1" (case-replace "v(L0!1) = zero") (("1" (assert) nil nil) ("2" (hide -2 3 4) (("2" (lemma "scal_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "v(L1!1) = ((x!1 - x!3)/(x!2 - x!4))* v(L0!1)") (("1" (lemma "comp_eq_x") (("1" (inst?) (("1" (expand "*" -1) (("1" (assert) (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "comp_eq_y") (("1" (inst?) (("1" (expand "*" -1) (("1" (split -1) (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (replace -1) (("2" (apply-extensionality 1 :hide? t) (("1" (assert) (("1" (expand "*") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "*") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "*") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3 4) (("2" (expand "*") (("2" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil) ("2" (apply-extensionality 1 :hide? t) (("1" (hide 2 3) (("1" (lemma "comp_eq_x") (("1" (inst - "x!1 * v(L0!1) - x!2 * v(L1!1)" "x!3 * v(L0!1) - x!4 * v(L1!1)") (("1" (expand "-") (("1" (expand "*") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (lemma "comp_eq_y") (("2" (inst - "x!1 * v(L0!1) - x!2 * v(L1!1)" "x!3 * v(L0!1) - x!4 * v(L1!1)") (("2" (expand "*") (("2" (expand "-") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (apply-extensionality 1 :hide? t) (("1" (hide -1) (("1" (lemma "comp_eq_x") (("1" (inst - "p(L0!1) + x!3 * v(L0!1)" "p(L1!1) + x!4 * v(L1!1)") (("1" (expand "+ ") (("1" (expand "*") (("1" (assert) (("1" (expand "-") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (lemma "comp_eq_y") (("2" (inst - "p(L0!1) + x!3 * v(L0!1)" "p(L1!1) + x!4 * v(L1!1)") (("2" (expand "*") (("2" (expand "-") (("2" (expand "+ ") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2 3) (("2" (apply-extensionality 1 :hide? t) (("1" (lemma "comp_eq_x") (("1" (inst?) (("1" (expand "*") (("1" (expand "-") (("1" (expand "+ ") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "comp_eq_y") (("2" (inst?) (("2" (expand "*") (("2" (expand "-") (("2" (expand "+ ") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Vect2 type-eq-decl nil vectors_2D_def nil) (Nz_vect2 type-eq-decl nil vectors_2D nil) (Line2D type-eq-decl nil lines_2D nil) (det const-decl "real" det_2D nil) (+ const-decl "Vector" vectors_2D nil) (comp_eq_y formula-decl nil vectors_2D nil) (scal_assoc formula-decl nil vectors_2D nil) (comp_eq_x formula-decl nil vectors_2D nil) (scal_0 formula-decl nil vectors_2D nil) (zero const-decl "Vector" vectors_2D nil) (* const-decl "Vector" vectors_2D nil) (Vector type-eq-decl nil vectors_2D nil) (on_line? const-decl "bool" lines_2D nil)) nil) (same_line_lem-2 nil 3430227209 ("" (skosimp*) (("" (lemma "pt_intersect") (("" (inst - "L0!1" "L1!1" "p1!1") (("" (assert) (("" (expand "intersect?") (("" (flatten) (("" (expand "same_line?") (("" (hide 3) (("" (expand "det") (("" (expand "on_line?") (("" (skosimp*) (("" (replace -1) (("" (hide -1) (("" (replace -2) (("" (hide -2) (("" (case-replace " x!1 * v(L0!1) - x!2 * v(L1!1) = p(L1!1) - p(L0!1)") (("1" (hide -2) (("1" (case-replace " x!3 * v(L0!1) - x!4 * v(L1!1) = p(L1!1) - p(L0!1)") (("1" (hide -3) (("1" (replace -1 * rl) (("1" (hide -1) (("1" (assert) (("1" (case-replace "(x!1 - x!3)*v(L0!1) = (x!2 - x!4) * v(L1!1)") (("1" (case-replace "(x!2 - x!4) = 0") (("1" (assert) (("1" (move-terms -1 l 2) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "x!1 = x!3") (("1" (case-replace "v(L0!1) = zero") (("1" (assert) nil nil) ("2" (hide -2 3 4) (("2" (lemma "scal_eq_zero") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "v(L1!1) = ((x!1 - x!3)/(x!2 - x!4))* v(L0!1)") (("1" (lemma "comp_eq_x") (("1" (inst?) (("1" (expand "*" -1) (("1" (assert) (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "comp_eq_y") (("1" (inst?) (("1" (expand "*" -1) (("1" (split -1) (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (replace -1) (("2" (apply-extensionality 1 :hide? t) (("1" (assert) (("1" (expand "*") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "*") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "*") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3 4) (("2" (expand "*") (("2" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil) ("2" (apply-extensionality 1 :hide? t) (("1" (hide 2 3) (("1" (lemma "comp_eq_x") (("1" (inst - "x!1 * v(L0!1) - x!2 * v(L1!1)" "x!3 * v(L0!1) - x!4 * v(L1!1)") (("1" (expand "-") (("1" (expand "*") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (lemma "comp_eq_y") (("2" (inst - "x!1 * v(L0!1) - x!2 * v(L1!1)" "x!3 * v(L0!1) - x!4 * v(L1!1)") (("2" (expand "*") (("2" (expand "-") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (apply-extensionality 1 :hide? t) (("1" (hide -1) (("1" (lemma "comp_eq_x") (("1" (inst - "p(L0!1) + x!3 * v(L0!1)" "p(L1!1) + x!4 * v(L1!1)") (("1" (expand "+ ") (("1" (expand "*") (("1" (assert) (("1" (expand "-") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (lemma "comp_eq_y") (("2" (inst - "p(L0!1) + x!3 * v(L0!1)" "p(L1!1) + x!4 * v(L1!1)") (("2" (expand "*") (("2" (expand "-") (("2" (expand "+ ") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2 3) (("2" (apply-extensionality 1 :hide? t) (("1" (lemma "comp_eq_x") (("1" (inst?) (("1" (expand "*") (("1" (expand "-") (("1" (expand "+ ") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "comp_eq_y") (("2" (inst?) (("2" (expand "*") (("2" (expand "-") (("2" (expand "+ ") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((on_line? const-decl "bool" lines_2D nil) (Vector type-eq-decl nil vectors_2D nil) (* const-decl "Vector" vectors_2D nil) (norm const-decl "nnreal" vectors_2D nil) (zero const-decl "Vector" vectors_2D nil) (scal_0 formula-decl nil vectors_2D nil) (comp_eq_x formula-decl nil vectors_2D nil) (comp_eq_y formula-decl nil vectors_2D nil) (+ const-decl "Vector" vectors_2D nil) (det const-decl "real" det_2D nil) (Line2D type-eq-decl nil lines_2D nil) (Nz_vect2 type-eq-decl nil vectors_2D nil) (Vect2 type-eq-decl nil vectors_2D_def nil)) nil) (same_line_lem-1 nil 3267536081 ("" (skosimp*) (("" (lemma "pt_intersect") (("" (inst - "L0!1" "L1!1" "p1!1") (("" (assert) (("" (expand "intersect?") (("" (flatten) (("" (expand "same_line?") (("" (hide 3) (("" (expand "cross") (("" (expand "on_line?") (("" (skosimp*) (("" (replace -1) (("" (hide -1) (("" (replace -2) (("" (hide -2) (("" (case-replace " x!1 * v(L0!1) - x!2 * v(L1!1) = p(L1!1) - p(L0!1)") (("1" (hide -2) (("1" (case-replace " x!3 * v(L0!1) - x!4 * v(L1!1) = p(L1!1) - p(L0!1)") (("1" (hide -3) (("1" (replace -1 * rl) (("1" (hide -1) (("1" (assert) (("1" (case-replace "(x!1 - x!3)*v(L0!1) = (x!2 - x!4) * v(L1!1)") (("1" (case-replace "(x!2 - x!4) = 0") (("1" (assert) (("1" (move-terms -1 l 2) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "x!1 = x!3") (("1" (case-replace "v(L0!1) = zero") (("1" (assert) nil nil) ("2" (hide -2 3 4) (("2" (lemma "scal_eq_zero") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "v(L1!1) = ((x!1 - x!3)/(x!2 - x!4))* v(L0!1)") (("1" (lemma "comp_eq_x") (("1" (inst?) (("1" (expand "*" -1) (("1" (assert) (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "comp_eq_y") (("1" (inst?) (("1" (expand "*" -1) (("1" (split -1) (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (replace -1) (("2" (apply-extensionality 1 :hide? t) (("1" (assert) (("1" (expand "*") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "*") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "*") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (hide 3 4) (("2" (expand "*") (("2" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil) ("2" (apply-extensionality 1 :hide? t) (("1" (hide 2 3) (("1" (lemma "comp_eq_x") (("1" (inst - "x!1 * v(L0!1) - x!2 * v(L1!1)" "x!3 * v(L0!1) - x!4 * v(L1!1)") (("1" (expand "-") (("1" (expand "*") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (lemma "comp_eq_y") (("2" (inst - "x!1 * v(L0!1) - x!2 * v(L1!1)" "x!3 * v(L0!1) - x!4 * v(L1!1)") (("2" (expand "*") (("2" (expand "-") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (apply-extensionality 1 :hide? t) (("1" (hide -1) (("1" (lemma "comp_eq_x") (("1" (inst - "p(L0!1) + x!3 * v(L0!1)" "p(L1!1) + x!4 * v(L1!1)") (("1" (expand "+ ") (("1" (expand "*") (("1" (assert) (("1" (expand "-") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (lemma "comp_eq_y") (("2" (inst - "p(L0!1) + x!3 * v(L0!1)" "p(L1!1) + x!4 * v(L1!1)") (("2" (expand "*") (("2" (expand "-") (("2" (expand "+ ") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2 3) (("2" (apply-extensionality 1 :hide? t) (("1" (lemma "comp_eq_x") (("1" (inst?) (("1" (expand "*") (("1" (expand "-") (("1" (expand "+ ") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "comp_eq_y") (("2" (inst?) (("2" (expand "*") (("2" (expand "-") (("2" (expand "+ ") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((on_line? const-decl "bool" lines_2D nil) (Vector type-eq-decl nil vectors_2D nil) (* const-decl "Vector" vectors_2D nil) (norm const-decl "nnreal" vectors_2D nil) (zero const-decl "Vector" vectors_2D nil) (scal_0 formula-decl nil vectors_2D nil) (comp_eq_x formula-decl nil vectors_2D nil) (comp_eq_y formula-decl nil vectors_2D nil) (+ const-decl "Vector" vectors_2D nil) (Line2D type-eq-decl nil lines_2D nil) (Nz_vect2 type-eq-decl nil vectors_2D nil) (Vect2 type-eq-decl nil vectors_2D_def nil)) shostak)) (not_same_line 0 (not_same_line-2 nil 3430227235 ("" (skeep) (("" (expand "on_line?") (("" (skeep -1) (("" (expand "same_line?") (("" (flatten) (("" (lemma "parallel_det_0") (("" (inst?) (("" (assert) (("" (hide -3) (("" (expand "parallel?") (("" (skeep -1) (("" (lemma "parallel_det_0") (("" (inst?) (("1" (assert) (("1" (hide -4) (("1" (expand "parallel?") (("1" (skolem -1 "nzk2") (("1" (replaces -3) (("1" (replaces -2) (("1" (inst 1 "nzk*(x-nzk2)") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nz_vector?") (("2" (flatten) (("2" (hide -4) (("2" (replaces -3) (("2" (rewrite "sub_eq_zero") (("2" (replaces -1) (("2" (replaces -1) (("2" (inst 1 "x*nzk") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((on_line? const-decl "bool" lines_2D nil) (same_line? const-decl "bool" intersections_2D nil) (parallel_det_0 formula-decl nil parallel_2D nil) (parallel? const-decl "bool" vectors_2D nil) (scal_assoc formula-decl nil vectors_2D nil) (sub_eq_zero formula-decl nil vectors_2D nil) (nz_nzv application-judgement "Nz_vector" vectors_2D nil) (real_times_real_is_real application-judgement "real" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nzreal nonempty-type-eq-decl nil reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (+ const-decl "Vector" vectors_2D nil) (* const-decl "Vector" vectors_2D nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (L0 skolem-const-decl "Line2D" intersections_2D nil) (L1 skolem-const-decl "Line2D" intersections_2D nil) (- const-decl "Vector" vectors_2D nil) (Line2D type-eq-decl nil lines_2D nil) (Nz_vect2 type-eq-decl nil vectors_2D nil) (Vect2 type-eq-decl nil vectors_2D_def nil) (Nz_vector type-eq-decl nil vectors_2D nil) (zero const-decl "Vector" vectors_2D nil) (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D nil) (real nonempty-type-from-decl nil reals nil)) nil) (not_same_line-1 nil 3267869462 ("" (skosimp*) (("" (expand "on_line?") (("" (skosimp*) (("" (expand "same_line?") (("" (flatten) (("" (replace -1) (("" (hide -1) (("" (name "DELTA" "L1!1`p - L0!1`p") (("" (case "EXISTS (x: real): x!1 * v(L0!1) = DELTA + x * v(L1!1)") (("1" (skosimp*) (("1" (inst + "x!2") (("1" (assert) (("1" (replace -2) (("1" (replace -2 * rl) (("1" (replace -1) (("1" (hide -) (("1" (apply-extensionality :hide? t) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (replace -1) (("2" (expand "cross") (("2" (hide -1) (("2" (case "v(L1!1)`x = 0") (("1" (replace -1) (("1" (assert) (("1" (case "v(L1!1)`y = 0") (("1" (case "v(L1!1) = zero") (("1" (assert) nil nil) ("2" (apply-extensionality 1 :hide? t) nil nil)) nil) ("2" (inst + "(x!1 * v(L0!1)`y - DELTA`y)/ v(L1!1)`y") (("1" (apply-extensionality 2 :hide? t) (("1" (expand "*") (("1" (expand "+ ") (("1" (field 1) (("1" (flatten) (("1" (mult-cases -2) (("1" (replace -2) (("1" (assert) (("1" (replace -1) (("1" (assert) (("1" (mult-cases -3) (("1" (reveal 1) (("1" (case "v(L0!1) = zero") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "+ ") (("2" (expand "*") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst + "(x!1 * v(L0!1)`x - DELTA`x)/ v(L1!1)`x") (("1" (apply-extensionality 2 :hide? t) (("1" (expand "+ ") (("1" (expand "*") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "*") (("2" (expand "+ ") (("2" (move-terms -2 l 2) (("2" (assert) (("2" (field 1) (("2" (move-terms -2 l 2) (("2" (assert) (("2" (div-by -2 "v(L1!1)`x") (("2" (replace -2 + rl) (("2" (assert) (("2" (case-replace "v(L1!1)`x * (L0!1`v`x * L1!1`v`y / v(L1!1)`x) = L0!1`v`x * L1!1`v`y ") (("1" (case "L0!1`v`x = 0") (("1" (replace -1) (("1" (assert) (("1" (case "L0!1`v`y = 0") (("1" (replace -1) (("1" (assert) (("1" (case "v(L0!1) = zero") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (div-by -4 "L0!1`v`x") (("2" (replace -4 + rl) (("2" (assert) (("2" (replace -3 * rl) (("2" (assert) (("2" (real-props 2) (("2" (field 2) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((on_line? const-decl "bool" lines_2D nil) (Line2D type-eq-decl nil lines_2D nil) (Nz_vect2 type-eq-decl nil vectors_2D nil) (Vect2 type-eq-decl nil vectors_2D_def nil) (Vector type-eq-decl nil vectors_2D nil) (norm const-decl "nnreal" vectors_2D nil) (zero const-decl "Vector" vectors_2D nil) (comp_zero_x formula-decl nil vectors_2D nil) (comp_zero_y formula-decl nil vectors_2D nil) (* const-decl "Vector" vectors_2D nil) (+ const-decl "Vector" vectors_2D nil)) shostak)) (intersect_pt_lem_TCC1 0 (intersect_pt_lem_TCC1-2 nil 3430227382 ("" (skosimp*) (("" (expand "on_line?") (("" (skosimp*) (("" (replace -2) (("" (hide -2) (("" (lemma "det_line") (("" (inst?) (("" (assert) (("" (replace -2) (("" (flatten) (("" (expand "same_line?") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((on_line? const-decl "bool" lines_2D nil) (det_line formula-decl nil intersections_2D nil) (real_times_real_is_real application-judgement "real" reals nil) (same_line? const-decl "bool" intersections_2D 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) (Line2D type-eq-decl nil lines_2D nil) (Nz_vect2 type-eq-decl nil vectors_2D nil) (Vect2 type-eq-decl nil vectors_2D_def nil)) nil) (intersect_pt_lem_TCC1-1 nil 3268038074 ("" (skosimp*) (("" (expand "on_line?") (("" (skosimp*) (("" (replace -2) (("" (hide -2) (("" (lemma "cross_lem") (("" (inst?) (("" (assert) (("" (replace -2) (("" (flatten) (("" (expand "same_line?") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((on_line? const-decl "bool" lines_2D nil) (Line2D type-eq-decl nil lines_2D nil) (Nz_vect2 type-eq-decl nil vectors_2D nil) (Vect2 type-eq-decl nil vectors_2D_def nil)) shostak)) (intersect_pt_lem 0 (intersect_pt_lem-1 nil 3267804562 ("" (skosimp*) (("" (lemma "intersect_pt_unique") (("" (inst - "L0!1" "L1!1" "pnot!1") (("" (assert) (("" (expand "intersect?") (("" (expand "same_line?") (("" (assert) (("" (flatten) (("" (lemma "pt_intersect") (("" (inst - "L0!1" "L1!1" "pnot!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((intersect_pt_unique formula-decl nil intersections_2D nil) (same_line? const-decl "bool" intersections_2D nil) (pt_intersect formula-decl nil intersections_2D nil) (intersect? const-decl "bool" intersections_2D nil) (real nonempty-type-from-decl nil reals nil) (Line2D type-eq-decl nil lines_2D nil) (Nz_vect2 type-eq-decl nil vectors_2D nil) (Vect2 type-eq-decl nil vectors_2D_def nil)) shostak)))
¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.146Bemerkung: (vorverarbeitet am 2026-04-27) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26