| products/Sources/formale Sprachen/PVS/ACCoRD/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: node.pvs Sprache: LispOriginal von: PVS© |
|
||||||
|
(gs_only
(k_l_det 0 (k_l_det-2 nil 3441562959 ("" (skeep) (("" (split +) (("1" (grind) nil nil) ("2" (rewrite "comps_eq") (("2" (flatten) (("2" (mult-by -1 "v`y") (("2" (mult-by -2 "v`x") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((det const-decl "real" det_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (both_sides_times1_imp formula-decl nil extra_real_props nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (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) (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil) (comps_eq formula-decl nil vectors_2D "vectors/")) nil) (k_l_det-1 nil 3441562916 ("" (postpone) nil nil) nil shostak)) (k_l_det_nz 0 (k_l_det_nz-1 nil 3441562983 ("" (skeep) (("" (replaces -) (("" (grind) (("1" (field 2) nil nil) ("2" (field 2) nil nil)) nil)) nil)) nil) ((= const-decl "[T, T -> boolean]" equalities nil) (number_field nonempty-type-from-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (both_sides_times1 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_cancel2 formula-decl nil real_props nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (minus_odd_is_odd application-judgement "odd_int" integers 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) (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) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real nonempty-type-from-decl nil reals nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real_div_nzreal_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) (- const-decl "Vector" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (det const-decl "real" det_2D "vectors/")) nil)) (gs_only_line_k_l_TCC1 0 (gs_only_line_k_l_TCC1-3 nil 3460224238 ("" (skeep) (("" (skeep 2) (("" (skeep 2) (("" (case-replace "max(l,0)=l") (("1" (hide -1) (("1" (lemma "k_l_det_nz") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((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) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (>= const-decl "bool" reals nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (k_l_det_nz formula-decl nil gs_only nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil) (gs_only_line_k_l_TCC1-2 nil 3460222808 ("" (skosimp*) (("" (assert) nil nil)) nil) nil nil) (gs_only_line_k_l_TCC1-1 nil 3460222678 ("" (skeep) (("" (skeep 2) (("" (skeep 2) (("" (assert) nil nil)) nil)) nil)) nil) nil nil)) (gs_only_line_k_l_TCC2 0 (gs_only_line_k_l_TCC2-2 nil 3460222860 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil) (gs_only_line_k_l_TCC2-1 nil 3460222678 ("" (subtype-tcc) nil nil) nil nil)) (gs_only_line_k_l_complete 0 (gs_only_line_k_l_complete-1 nil 3460223297 ("" (skeep) (("" (case-replace "vo=zero") (("1" (rewrite "det_zero_left") (("1" (rewrite "det_zero_right") (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "k_l_det") (("2" (inst -1 "k" "v" "vi" "vo" "l") (("2" (split -1) (("1" (flatten) (("1" (name-replace "gso" "gs_only_line_k_l(v,vo, vi)" :hide? nil) (("1" (expand "gs_only_line_k_l") (("1" (lift-if) (("1" (split -1) (("1" (flatten) (("1" (div-by -2 "det(vo,v)") (("1" (div-by -3 "det(vo,v)") (("1" (replaces (-2 -3) :dir rl) (("1" (case-replace "max(l,0)=l") (("1" (case-replace "max(l,0)=0") (("1" (assert) nil nil) ("2" (hide-all-but (1 2)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replaces -2) (("2" (hide-all-but 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real nonempty-type-from-decl nil reals nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (Vector type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (det_zero_right formula-decl nil det_2D "vectors/") (sub_zero_left formula-decl nil vectors_2D "vectors/") (scal_zero formula-decl nil vectors_2D "vectors/") (det_zero_left formula-decl nil det_2D "vectors/") (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (add_cancel2 formula-decl nil vectors_2D "vectors/") (real_times_real_is_real application-judgement "real" reals nil) (both_sides_div1 formula-decl nil real_props nil) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (det const-decl "real" det_2D "vectors/") (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (times_div_cancel2 formula-decl nil extra_real_props nil) (max_nnreal_0 formula-decl nil min_max "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonneg_real_max application-judgement "{z: nonneg_real | z >= x AND z >= y}" real_defs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (gs_only_line_k_l const-decl "{k: real, l: nnreal | l > 0 => k * v = l * vo - vi}" gs_only nil) (- const-decl "Vector" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nnreal type-eq-decl nil real_types nil) (k_l_det formula-decl nil gs_only nil)) nil)) (gs_only_line_TCC1 0 (gs_only_line_TCC1-2 nil 3443969346 ("" (skeep) (("" (case-replace "l=0") (("1" (assert) nil nil) ("2" (rewrite "gs_only_scal") (("2" (typepred "gs_only_line_k_l(v,vo,vi)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (scal_0 formula-decl nil vectors_2D "vectors/") (gs_only_line_k_l const-decl "{k: real, l: nnreal | l > 0 => k * v = l * vo - vi}" gs_only nil) (- const-decl "Vector" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans 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) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (gs_only_scal formula-decl nil definitions nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil) (gs_only_line_TCC1-1 nil 3443969286 ("" (subtype-tcc) nil nil) nil nil)) (same_gs_only_line 0 (same_gs_only_line-1 nil 3443962519 ("" (skeep) (("" (expand "gs_only_line") (("" (expand "gs_only_line_k_l") (("" (replaces -1) (("" (rewrite "det_scal_left") (("" (name-replace "dvi" "det(vi,v)") (("" (name-replace "dv1" "det(v1,v)") (("" (case "dv1 = 0") (("1" (assert) nil nil) ("2" (assert) (("2" (copy 1) (("2" (mult-by 1 "l") (("2" (assert) (("2" (case-replace "dvi/(l*dv1) = (1/l)*(dvi/dv1)") (("1" (hide -1) (("1" (lemma "nneg_mult_max") (("1" (inst -1 "1/l" "dvi/dv1" "0") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((gs_only_line const-decl "{k: real, nvo: Vect2 | nvo /= zero => gs_only?(vo)(nvo) AND k * v = nvo - vi}" gs_only nil) (det const-decl "real" det_2D "vectors/") (= const-decl "[T, T -> boolean]" equalities nil) (scal_0 formula-decl nil vectors_2D "vectors/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal type-eq-decl nil real_types nil) (nneg_mult_max formula-decl nil min_max "reals/") (posreal_div_posreal_is_posreal application-judgement "posreal" real_types 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) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (both_sides_times1 formula-decl nil real_props nil) (scal_assoc formula-decl nil vectors_2D "vectors/") (real_div_nzreal_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (det_scal_left formula-decl nil det_2D "vectors/") (gs_only_line_k_l const-decl "{k: real, l: nnreal | l > 0 => k * v = l * vo - vi}" gs_only nil)) nil)) (gs_only_line_complete 0 (gs_only_line_complete-1 nil 3443983668 ("" (skeep) (("" (expand "gs_only_line?") (("" (case "nvo=zero") (("1" (replaces -1) (("1" (rewrite "gs_only_zero_right") (("1" (replaces -1) (("1" (rewrite "det_zero_left") (("1" (rewrite "det_zero_right") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "gs_only?") (("2" (skeep -1) (("2" (lemma "gs_only_line_k_l_complete") (("2" (inst?) (("2" (inst?) (("2" (inst?) (("2" (assert) (("2" (split -1) (("1" (expand "gs_only_line") (("1" (replaces -1 :dir rl) (("1" (assert) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((gs_only_line? const-decl "bool" gs_only nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (gs_only_line const-decl "{k: real, nvo: Vect2 | nvo /= zero => gs_only?(vo)(nvo) AND k * v = nvo - vi}" gs_only 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) (gs_only_line_k_l_complete formula-decl nil gs_only nil) (gs_only? const-decl "bool" definitions nil) (det_zero_right formula-decl nil det_2D "vectors/") (sub_zero_left formula-decl nil vectors_2D "vectors/") (det_zero_left formula-decl nil det_2D "vectors/") (gs_only_zero_right formula-decl nil definitions nil) (real nonempty-type-from-decl nil reals nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (Vector type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/")) nil)) (gs_only_dot_TCC1 0 (gs_only_dot_TCC1-2 nil 3445697631 ("" (skeep) (("" (name-replace "gso" "gs_only_line(Vdir(u, vo - vi), vo, vi + W0(u, j))") (("" (typepred "gso") (("" (assert) (("" (flatten) (("" (assert) (("" (case "W0(u,j) + gso`1 * Vdir(u, vo - vi) = gso`2 - vi") (("1" (replaces -1 :dir rl) (("1" (rewrite "W_dot") nil nil)) nil) ("2" (replaces -2) (("2" (hide-all-but 1) (("2" (grind :exclude "W0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (zero const-decl "Vector" vectors_2D "vectors/") (AND const-decl "[bool, bool -> bool]" booleans nil) (gs_only? const-decl "bool" definitions nil) (* const-decl "Vector" vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (gs_only_line const-decl "{k: real, nvo: Vect2 | nvo /= zero => gs_only?(vo)(nvo) AND k * v = nvo - vi}" gs_only nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (Vdir const-decl "Nz_vect2" definitions nil) (+ const-decl "Vector" vectors_2D "vectors/") (W0 const-decl "Vect2" definitions nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (W_dot formula-decl nil definitions nil) (NOT const-decl "[bool -> bool]" booleans nil)) nil) (gs_only_dot_TCC1-1 nil 3445697622 ("" (subtype-tcc) nil nil) nil nil)) (gs_only_dot_complete 0 (gs_only_dot_complete-1 nil 3459320682 ("" (skeep) (("" (case "nvo=zero") (("1" (expand "gs_only?") (("1" (replaces -1) (("1" (skeep -1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "gs_only_dot") (("2" (lemma "dot_W") (("2" (inst? -1) (("2" (inst? -1) (("2" (assert) (("2" (skeep -1) (("2" (lemma "gs_only_line_complete") (("2" (expand "gs_only_line?") (("2" (inst -1 "k" "nvo" "Vdir(u,vnzo-vi)" "vi+W0(u,j)" "vnzo") (("2" (assert) (("2" (split) (("1" (propax) nil nil) ("2" (hide-all-but (-1 1)) (("2" (grind :exclude ("W0" "Vdir")) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((zero const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil) (nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/") (gs_only? const-decl "bool" definitions nil) (dot_W formula-decl nil definitions nil) (gs_only_line? const-decl "bool" gs_only 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) (* const-decl "Vector" vectors_2D "vectors/") (Vdir const-decl "Nz_vect2" definitions nil) (+ const-decl "Vector" vectors_2D "vectors/") (W0 const-decl "Vect2" definitions nil) (gs_only_line_complete formula-decl nil gs_only nil) (- const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal 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) (gs_only_dot const-decl "{nvo | nvo /= zero => gs_only?(vo)(nvo) AND u * (nvo - vi) = j}" gs_only nil)) nil)) (gs_only_circle_TCC1 0 (gs_only_circle_TCC1-2 nil 3459321977 ("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (case "l>0") (("1" (expand "max") (("1" (assert) (("1" (hide-all-but (-1 -9 2)) (("1" (replaces -2) (("1" (rewrite "gs_only_scal") nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-8 1 2)) (("2" (case-replace "max(l,0)=0") (("1" (assert) nil nil) ("2" (hide-all-but (1 2)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((scal_0 formula-decl nil vectors_2D "vectors/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (gs_only_scal formula-decl nil definitions nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (real_times_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (> const-decl "bool" reals nil)) nil) (gs_only_circle_TCC1-1 nil 3459321845 ("" (subtype-tcc) nil nil) nil nil)) (gs_only_circle_TCC2 0 (gs_only_circle_TCC2-1 nil 3461670291 ("" (skosimp*) nil nil) nil nil)) (gs_only_circle_TCC3 0 (gs_only_circle_TCC3-1 nil 3461670291 ("" (skosimp*) nil nil) nil nil)) (gs_only_circle_solution 0 (gs_only_circle_solution-2 nil 3565275328 ("" (skeep) (("" (expand "circle_solution_2D?") (("" (expand "gs_only_circle?") (("" (flatten) (("" (skeep -1) (("" (expand "gs_only_circle" :assert? none) (("" (skoletin* -1 :old? t) (("" (lift-if) (("" (split -2) (("1" (flatten) (("1" (skoletin* -2 :postfix "p" :old? t) (("1" (case "lp > 0") (("1" (expand "max") (("1" (assert) (("1" (lift-if) (("1" (split -3) (("1" (flatten) (("1" (assert) (("1" (lemma "quad2b_eq_0") (("1" (inst? -1) (("1" (inst -1 "lp") (("1" (flatten) (("1" (hide -1) (("1" (assert) (("1" (split -1) (("1" (replaces (-3 -5)) (("1" (hide-all-but (-1 -6 -7 -8 -9 2)) (("1" (grind) nil nil)) nil)) nil) ("2" (inst 1 "irt") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) nil nil)) nil)) nil)) nil)) nil) ("2" (case-replace "max(lp,0)=0") (("1" (assert) (("1" (lift-if) (("1" (split -3) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((circle_solution_2D? const-decl "bool" horizontal nil) (gs_only_circle const-decl "{nvo | nvo /= zero => gs_only?(vnzo)(nvo)}" gs_only nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (quadratic const-decl "real" quadratic "reals/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (quad2b_eq_0 formula-decl nil quadratic_2b "reals/") (scal_0 formula-decl nil vectors_2D "vectors/") (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (discr2b const-decl "real" quadratic_2b "reals/") (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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 "[numfield -> numfield]" number_fields nil) (Sign type-eq-decl nil sign "reals/") (* const-decl "real" vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (AND const-decl "[bool, bool -> bool]" booleans nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (root2b const-decl "real" quadratic_2b "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnreal type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (D formal-const-decl "posreal" gs_only nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (* const-decl "Vector" vectors_2D "vectors/") (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) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (IFF const-decl "[bool, bool -> bool]" booleans nil) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (gs_only_circle? const-decl "bool" gs_only nil)) nil) (gs_only_circle_solution-1 nil 3461670946 ("" (skeep) (("" (expand "circle_solution_2D?") (("" (expand "gs_only_circle?") (("" (flatten) (("" (skeep -1) (("" (expand "gs_only_circle" :assert? none) (("" (skoletin* -1) (("" (lift-if) (("" (split -2) (("1" (flatten) (("1" (skoletin* -2 :postfix "p") (("1" (case "lp > 0") (("1" (expand "max") (("1" (assert) (("1" (lift-if) (("1" (split -3) (("1" (flatten) (("1" (assert) (("1" (lemma "quad2b_eq_0") (("1" (inst? -1) (("1" (inst -1 "lp") (("1" (flatten) (("1" (hide -1) (("1" (assert) (("1" (split -1) (("1" (replaces (-3 -5)) (("1" (hide-all-but (-1 -6 -7 -8 -9 2)) (("1" (grind) nil nil)) nil)) nil) ("2" (inst 1 "irt") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) nil nil)) nil)) nil)) nil)) nil) ("2" (case-replace "max(lp,0)=0") (("1" (assert) (("1" (lift-if) (("1" (split -3) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((circle_solution_2D? const-decl "bool" horizontal nil) (quadratic const-decl "real" quadratic "reals/") (quad2b_eq_0 formula-decl nil quadratic_2b "reals/") (scal_0 formula-decl nil vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (sqv const-decl "nnreal" vectors_2D "vectors/") (root2b const-decl "real" quadratic_2b "reals/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (Sign type-eq-decl nil sign "reals/") (discr2b const-decl "real" quadratic_2b "reals/") (Vector type-eq-decl nil vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (sq_nz_pos application-judgement "posreal" sq "reals/") (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")) nil)) (gs_only_circle_complete 0 (gs_only_circle_complete-1 nil 3459321586 ("" (skeep) (("" (expand "circle_solution_2D?") (("" (flatten) (("" (expand "gs_only_circle?") (("" (case-replace "nvo=zero") (("1" (rewrite "gs_only_zero_right") nil nil) ("2" (assert) (("2" (expand "gs_only?") (("2" (skeep -1) (("2" (lemma "quad2b_eq_0") (("2" (name "w" "s-t*vi") (("2" (name "a" "sq(t)*sqv(vnzo)") (("2" (name "b" "t*(w*vnzo)") (("2" (name "c" "sqv(w)-sq(D)") (("2" (inst -5 "a" "b" "c" "l") (("2" (flatten) (("2" (hide -6) (("2" (split -5) (("1" (flatten) (("1" (skeep -2) (("1" (inst 2 "eps") (("1" (expand "gs_only_circle") (("1" (replaces :from -6 :to -3) (("1" (assert) (("1" (replaces -2 :dir rl) (("1" (case-replace "max(l,0)=l") (("1" (assert) nil nil) ("2" (case "max(l,0)=0") (("1" (assert) nil nil) ("2" (hide-all-but (1 2)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -7 2 3) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((circle_solution_2D? const-decl "bool" horizontal nil) (gs_only_circle? const-decl "bool" gs_only nil) (real_times_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (* const-decl "Vector" vectors_2D "vectors/") (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 "vectors/") (* const-decl "real" vectors_2D "vectors/") (nzreal nonempty-type-eq-decl nil reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (+ const-decl "Vector" vectors_2D "vectors/") (quadratic const-decl "real" quadratic "reals/") (Sign type-eq-decl nil sign "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nzint nonempty-type-eq-decl nil integers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/") (max_nnreal_0 formula-decl nil min_max "reals/") (gs_only_circle const-decl "{nvo | nvo /= zero => gs_only?(vnzo)(nvo)}" gs_only nil) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (D formal-const-decl "posreal" gs_only nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_minus_real_is_real application-judgement "real" reals nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (sq const-decl "nonneg_real" sq "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (quad2b_eq_0 formula-decl nil quadratic_2b "reals/") (gs_only? const-decl "bool" definitions nil) (gs_only_zero_right formula-decl nil definitions nil) (/= const-decl "boolean" notequal nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil)) nil)) (gs_only_vertical_TCC1 0 (gs_only_vertical_TCC1-1 nil 3471002852 ("" (skeep) (("" (lemma "Delta_gt_0_nzv") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((D formal-const-decl "posreal" gs_only nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (Delta_gt_0_nzv formula-decl nil horizontal nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/")) nil)) (gs_only_vertical_TCC2 0 (gs_only_vertical_TCC2-3 nil 3471110192 ("" (skeep) (("" (skeep) (("" (lemma "scal_eq_zero") (("" (inst?) (("" (assert) (("" (rewrite "sqv_eq_0" :dir rl) (("" (replaces -5) (("" (lemma "Theta_D_on_D") (("" (inst?) (("" (assert) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (Vector type-eq-decl nil vectors_2D "vectors/") (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (Theta_D_on_D formula-decl nil horizontal nil) (D formal-const-decl "posreal" gs_only nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Sign type-eq-decl nil sign "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nzint nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (scal_eq_zero formula-decl nil vectors_2D "vectors/")) nil) (gs_only_vertical_TCC2-2 nil 3471022326 ("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep 2) (("" (expand "gs_only?") (("" (inst? 3) (("" (rewrite "max_gt") (("" (case-replace "max(k,0)=0") (("1" (assert) nil nil) ("2" (hide-all-but (1 2)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((gs_only? const-decl "bool" definitions nil) (scal_0 formula-decl nil vectors_2D "vectors/")) nil) (gs_only_vertical_TCC2-1 nil 3471002852 ("" (skosimp*) (("" (postpone) nil nil)) nil) nil nil)) (gs_only_vertical_TCC3 0 (gs_only_vertical_TCC3-1 nil 3471021482 ("" (skeep) (("" (skeep) (("" (typepred "gs_only_dot(t * p, vo, vi, sq(D) - s * p)") (("" (assert) nil nil)) nil)) nil)) nil) ((dot_scal_left formula-decl nil vectors_2D "vectors/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (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) (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (gs_only? const-decl "bool" definitions nil) (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "real" vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (gs_only_dot const-decl "{nvo | nvo /= zero => gs_only?(vo)(nvo) AND u * (nvo - vi) = j}" gs_only nil) (* const-decl "Vector" vectors_2D "vectors/") (>= 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (sq const-decl "nonneg_real" sq "reals/") (D formal-const-decl "posreal" gs_only nil) (sq_nz_pos application-judgement "posreal" sq "reals/")) nil)) (gs_only_vertical_TCC4 0 (gs_only_vertical_TCC4-1 nil 3471021482 ("" (skosimp*) nil nil) nil nil)) (gs_only_vertical_on_D 0 (gs_only_vertical_on_D-1 nil 3471022777 ("" (skeep) (("" (beta) (("" (flatten) (("" (expand "gs_only_vertical?") (("" (flatten) (("" (expand "gs_only_vertical") (("" (lift-if) (("" (split -1) (("1" (flatten) (("1" (assert) (("1" (typepred "gs_only_dot(t * (s + Theta_D(s, vo - vi, dir) * (vo - vi)), vo, vi, sq(D) - s * (s + Theta_D(s, vo - vi, dir) * (vo - vi)))") (("1" (replaces -4 :dir rl) (("1" (assert) (("1" (flatten) (("1" (hide-all-but (-2 2)) (("1" (grind :exclude "Theta_D") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((gs_only_vertical? const-decl "bool" gs_only nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (gs_only_vertical const-decl "{nvo | nvo /= zero => gs_only?(vo)(nvo)}" gs_only nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (dot_scal_left formula-decl nil vectors_2D "vectors/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (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) (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (gs_only? const-decl "bool" definitions nil) (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "real" vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (gs_only_dot const-decl "{nvo | nvo /= zero => gs_only?(vo)(nvo) AND u * (nvo - vi) = j}" gs_only nil) (* const-decl "Vector" vectors_2D "vectors/") (>= 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) (+ const-decl "Vector" vectors_2D "vectors/") (D formal-const-decl "posreal" gs_only nil) (Delta const-decl "real" horizontal nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nzint nonempty-type-eq-decl nil integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (Sign type-eq-decl nil sign "reals/") (Theta_D const-decl "real" horizontal nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (sq const-decl "nonneg_real" sq "reals/")) nil))) ¤ Dauer der Verarbeitung: 0.131 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 |
