| products/Sources/formale Sprachen/PVS/analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: cross_metric_spaces.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(cross_metric_spaces
(product_is_metric 0 (product_is_metric-1 nil 3459692307 ("" (lemma "fullset_metric_space1") (("" (lemma "fullset_metric_space2") (("" (expand "metric_space?") (("" (expand "space_zero?") (("" (expand "space_symmetric?") (("" (expand "space_triangle?") (("" (prop) (("1" (skosimp*) (("1" (expand "d") (("1" (prop) (("1" (grind) (("1" (apply-extensionality) nil nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil) ("2" (grind) nil nil) ("3" (skosimp*) (("3" (expand "d") (("3" (case "FORALL (x, y, z: (fullset[T1])): d1(x, z) <= d1(x, y) + d1(y, z)") (("1" (inst - "x!1`1" "y!1`1" "z!1`1") (("1" (case "FORALL (x, y, z: (fullset[T2])): d2(x, z) <= d2(x, y) + d2(y, z)") (("1" (inst - "x!1`2" "y!1`2" "z!1`2") (("1" (assert) nil nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil) ("3" (expand "fullset") (("3" (propax) nil nil)) nil) ("4" (expand "fullset") (("4" (propax) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil) ("3" (expand "fullset") (("3" (propax) nil nil)) nil) ("4" (expand "fullset") (("4" (propax) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((fullset_metric_space2 formula-decl nil cross_metric_spaces nil) (space_zero? const-decl "bool" metric_spaces_def nil) (space_triangle? const-decl "bool" metric_spaces_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (d1 formal-const-decl "[T1, T1 -> nnreal]" cross_metric_spaces nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (<= const-decl "bool" reals 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) (number nonempty-type-decl nil numbers nil) (d2 formal-const-decl "[T2, T2 -> nnreal]" cross_metric_spaces nil) (z!1 skolem-const-decl "(fullset[[T1, T2]])" cross_metric_spaces nil) (y!1 skolem-const-decl "(fullset[[T1, T2]])" cross_metric_spaces nil) (x!1 skolem-const-decl "(fullset[[T1, T2]])" cross_metric_spaces nil) (NOT const-decl "[bool -> bool]" booleans nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (T1 formal-nonempty-type-decl nil cross_metric_spaces nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T2 formal-nonempty-type-decl nil cross_metric_spaces nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (fullset const-decl "set" sets nil) (even_plus_even_is_even application-judgement "even_int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (d const-decl "nnreal" cross_metric_spaces nil) (space_symmetric? const-decl "bool" metric_spaces_def nil) (metric_space? const-decl "bool" metric_spaces_def nil) (fullset_metric_space1 formula-decl nil cross_metric_spaces nil)) shostak)) (product_is_metric_square 0 (product_is_metric_square-1 nil 3459757625 ("" (lemma "fullset_metric_space1") (("" (lemma "fullset_metric_space2") (("" (expand "metric_space?") (("" (prop) (("1" (expand "space_zero?") (("1" (skosimp*) (("1" (expand "d_square") (("1" (lemma "sqrt_eq_0") (("1" (inst - "sq(d1(x!1`1, y!1`1)) + sq(d2(x!1`2, y!1`2))") (("1" (prop) (("1" (expand "sq") (("1" (typepred "d1(x!1`1, y!1`1)") (("1" (typepred "d2(x!1`2, y!1`2)") (("1" (mult-ineq -1 -1) (("1" (mult-ineq -3 -3) (("1" (grind) (("1" (case "x!1 = (x!1`1,x!1`2)") (("1" (case "y!1 = (y!1`1,y!1`2)") (("1" (grind) nil nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil) ("2" (case "d2(y!1`2, y!1`2)=0") (("1" (replace -1) (("1" (lemma "sq_eq_0") (("1" (inst - "d1(y!1`1, x!1`1)") (("1" (expand "sq") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("3" (case "d1(y!1`1, y!1`1)=0") (("1" (replace -1) (("1" (lemma "sq_eq_0") (("1" (inst - "d2(y!1`2, x!1`2)") (("1" (expand "sq") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("4" (swap-rel -1) (("4" (case "d1(y!1`1, x!1`1) * d1(y!1`1, x!1`1) + d2(y!1`2, x!1`2) * d2(y!1`2, x!1`2) = 0") (("1" (hide -2) (("1" (lemma "posreal_times_posreal_is_posreal") (("1" (inst-cp - "d1(y!1`1, x!1`1)" "d1(y!1`1, x!1`1)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sqrt_0") (("2" (case "forall (z: nonneg_real): z = 0 implies sqrt(z) = 0") (("1" (inst - "sq(d1(x!1`1, y!1`1)) + sq(d2(x!1`2, y!1`2))") (("1" (prop) nil nil)) nil) ("2" (skosimp*) (("2" (replace -1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (case "x!1 = (x!1`1,x!1`2) and y!1 = (y!1`1,y!1`2)") (("1" (case "x!1`1 = y!1`1 and x!1`2 = y!1`2") (("1" (prop) (("1" (replace -1) (("1" (replace -2) (("1" (inst - "y!1`2" "y!1`2") (("1" (inst - "y!1`1" "y!1`1") (("1" (assert) (("1" (expand "sq") (("1" (case "d1(y!1`1, y!1`1) * d1(y!1`1, y!1`1) + d2(y!1`2, y!1`2) * d2(y!1`2, y!1`2) = 0") (("1" (replace -1) (("1" (lemma "sqrt_0") (("1" (propax) nil nil)) nil)) nil) ("2" (case "d2(y!1`2, y!1`2) = 0") (("1" (case "d1(y!1`1, y!1`1) = 0") (("1" (mult-eq -1 -1) (("1" (mult-eq -3 -3) (("1" (add-formulas -1 -2) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "space_symmetric?") (("2" (expand "d_square") (("2" (skosimp*) (("2" (inst - "x!1`2" "y!1`2") (("1" (inst - "x!1`1" "y!1`1") (("1" (case "d2(x!1`2, y!1`2) = d2(y!1`2, x!1`2)") (("1" (case "d1(x!1`1, y!1`1) = d1(y!1`1, x!1`1)") (("1" (replace -1) (("1" (replace -2) (("1" (propax) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil) ("3" (expand "fullset") (("3" (propax) nil nil)) nil)) nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil) ("3" (expand "fullset") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "space_triangle?") (("3" (expand "d_square") (("3" (skosimp*) (("3" (inst - "x!1`2" "y!1`2" "z!1`2") (("1" (inst - "x!1`1" "y!1`1" "z!1`1") (("1" (name "A" "d2(x!1`2, z!1`2)") (("1" (name "B" "d2(x!1`2, y!1`2)") (("1" (name "C" "d2(y!1`2, z!1`2)") (("1" (name "D" "d1(x!1`1, z!1`1)") (("1" (name "E" "d1(x!1`1, y!1`1)") (("1" (name "F" "d1(y!1`1, z!1`1)") (("1" (replace -1) (("1" (replace -2) (("1" (replace -3) (("1" (replace -4) (("1" (replace -5) (("1" (replace -6) (("1" (typepred "A") (("1" (typepred "B") (("1" (typepred "C") (("1" (typepred "D") (("1" (typepred "E") (("1" (typepred "F") (("1" (lemma "sqrt_cauchy") (("1" (inst - "B" "E" "C" "F") (("1" (add-formulas -1 -1) (("1" (case "A <= B + C") (("1" (case "D <= E + F") (("1" (mult-ineq -1 -1) (("1" (mult-ineq -3 -3) (("1" (expand "sq") (("1" (add-formulas -1 -2 :auto-step (skip)) (("1" (lemma "sq_le") (("1" (inst - "sqrt(A * A + D * D)" "sqrt(B * B + E * E) + sqrt(C * C + F * F)") (("1" (prop) (("1" (expand "sq") (("1" (lemma "sqrt_def") (("1" (inst-cp - "A*A + D*D") (("1" (replace -2) (("1" (inst-cp - "B*B + E*E") (("1" (replace -2) (("1" (inst-cp - "C*C + F*F") (("1" (replace -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil) ("3" (expand "fullset") (("3" (propax) nil nil)) nil) ("4" (expand "fullset") (("4" (propax) nil nil)) nil)) nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil) ("3" (expand "fullset") (("3" (propax) nil nil)) nil) ("4" (expand "fullset") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((fullset_metric_space2 formula-decl nil cross_metric_spaces nil) (sqrt_eq_0 formula-decl nil sqrt "reals/") (NOT const-decl "[bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (ge_times_ge_any1 formula-decl nil extra_real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (space_triangle? const-decl "bool" metric_spaces_def nil) (space_symmetric? const-decl "bool" metric_spaces_def nil) (sqrt_0 formula-decl nil sqrt "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (sq_eq_0 formula-decl nil sq "reals/") (posreal_times_posreal_is_posreal judgement-tcc nil real_types nil) (> const-decl "bool" reals 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) (IFF const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (y!1 skolem-const-decl "(fullset[[T1, T2]])" cross_metric_spaces nil) (even_plus_even_is_even application-judgement "even_int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (d2 formal-const-decl "[T2, T2 -> nnreal]" cross_metric_spaces nil) (fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil) (T2 formal-nonempty-type-decl nil cross_metric_spaces nil) (d1 formal-const-decl "[T1, T1 -> nnreal]" cross_metric_spaces nil) (nnreal type-eq-decl nil real_types nil) (T1 formal-nonempty-type-decl nil cross_metric_spaces 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) (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) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (d_square const-decl "nnreal" cross_metric_spaces nil) (space_zero? const-decl "bool" metric_spaces_def nil) (x!1 skolem-const-decl "(fullset[[T1, T2]])" cross_metric_spaces nil) (y!1 skolem-const-decl "(fullset[[T1, T2]])" cross_metric_spaces nil) (x!1 skolem-const-decl "(fullset[[T1, T2]])" cross_metric_spaces nil) (y!1 skolem-const-decl "(fullset[[T1, T2]])" cross_metric_spaces nil) (z!1 skolem-const-decl "(fullset[[T1, T2]])" cross_metric_spaces nil) (sqrt_cauchy formula-decl nil sqrt "reals/") (sqrt_def formula-decl nil sqrt "reals/") (sq_le formula-decl nil sq "reals/") (le_times_le_any1 formula-decl nil extra_real_props nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (metric_space? const-decl "bool" metric_spaces_def nil) (fullset_metric_space1 formula-decl nil cross_metric_spaces nil)) shostak)) (euclic_linear_lemma 0 (euclic_linear_lemma-1 nil 3459767870 ("" (skosimp*) (("" (mult-ineq -1 -1) (("" (lemma "sqrt_def") (("" (inst - "sq(a!1) + sq(b!1)") (("" (replace -1) (("" (case "sq(a!1) < (r!1 / 2) * (r!1 / 2) and sq(b!1) < (r!1 / 2) * (r!1 / 2)") (("1" (prop) (("1" (lemma "sq_rew") (("1" (inst - "(r!1 / 2)") (("1" (rewrite -1) (("1" (lemma "sq_lt") (("1" (inst-cp - "a!1" "(r!1/2)") (("1" (inst-cp - "b!1" "(r!1/2)") (("1" (prop) (("1" (case "a!1 < (r!1 / 2)") (("1" (case "b!1 < (r!1 / 2)") (("1" (add-formulas -1 -2) nil nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "sq(b!1)") (("2" (swap-rel -1) (("2" (case "sq(a!1) + sq(b!1) < (r!1 / 2) * (r!1 / 2)") (("1" (add-formulas -1 -2) (("1" (assert) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types 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) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (nnreal type-eq-decl nil real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sq const-decl "nonneg_real" sq "reals/") (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (lt_times_lt_any1 formula-decl nil extra_real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (sq_rew formula-decl nil sq "reals/") (div_cancel1 formula-decl nil real_props nil) (sq_lt formula-decl nil sq "reals/") (<= const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans 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) (NOT const-decl "[bool -> bool]" booleans nil) (sqrt_def formula-decl nil sqrt "reals/")) shostak)) (metric_equivalence_TCC1 0 (metric_equivalence_TCC1-1 nil 3459765087 ("" (lemma "product_is_metric") (("" (propax) nil nil)) nil) ((product_is_metric formula-decl nil cross_metric_spaces nil)) nil)) (metric_equivalence_TCC2 0 (metric_equivalence_TCC2-1 nil 3459765087 ("" (lemma "product_is_metric_square") (("" (propax) nil nil)) nil) ((product_is_metric_square formula-decl nil cross_metric_spaces nil)) nil)) (metric_equivalence 0 (metric_equivalence-1 nil 3459765088 ("" (skosimp*) (("" (expand "open_in?") (("" (expand "subset?") (("" (expand "intersection") (("" (expand "ball") (("" (expand "member") (("" (prop) (("1" (skosimp*) (("1" (typepred "s!1") (("1" (inst - "s!1") (("1" (skosimp*) (("1" (inst + "r!1/2") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (expand "d_square") (("1" (lemma "euclic_linear_lemma") (("1" (inst - "d1(s!1`1, x!1`1)" "d2(s!1`2, x!1`2)" "r!1") (("1" (prop) (("1" (typepred "d2(s!1`2, x!1`2)") (("1" (swap-rel -1) (("1" (expand "d") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "s!1") (("2" (skosimp*) (("2" (expand "d_square") (("2" (expand "d") (("2" (inst + "r!1") (("2" (skosimp*) (("2" (mult-ineq -1 -1) (("2" (lemma "sq_rew") (("2" (assert) (("2" (inst-cp - "d1(s!1`1, x!1`1)") (("2" (inst-cp - "d2(s!1`2, x!1`2)") (("2" (replace -2) (("2" (replace -3) (("2" (typepred "d1(s!1`1, x!1`1) * d2(s!1`2, x!1`2)") (("2" (case "sq(d1(s!1`1, x!1`1)) + d1(s!1`1, x!1`1) * d2(s!1`2, x!1`2) + d1(s!1`1, x!1`1) * d2(s!1`2, x!1`2) + sq(d2(s!1`2, x!1`2)) < r!1 * r!1") (("1" (swap-rel -2) (("1" (copy -2) (("1" (add-formulas -2 -3) (("1" (add-formulas -1 -2) (("1" (assert) (("1" (both-sides "-" "2 * (d1(s!1`1, x!1`1) * d2(s!1`2, x!1`2))" -1) (("1" (assert) (("1" (lemma "sqrt_lt") (("1" (inst - "sq(d1(s!1`1, x!1`1)) + sq(d2(s!1`2, x!1`2))" "r!1 * r!1") (("1" (prop) (("1" (case "FORALL (x: [T1, T2]): sqrt(sq(d1(s!1`1, x`1)) + sq(d2(s!1`2, x`2))) < r!1 AND U!1(x) => V!1(x)") (("1" (inst - "x!1") (("1" (assert) nil nil)) nil) ("2" (propax) 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((open_in? const-decl "bool" metric_spaces nil) (intersection const-decl "set" sets nil) (member const-decl "bool" sets nil) (sq_rew formula-decl nil sq "reals/") (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (sqrt_square formula-decl nil sqrt "reals/") (sqrt_pos application-judgement "posreal" sqrt "reals/") (sqrt_lt formula-decl nil sqrt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (both_sides_plus_lt1 formula-decl nil real_props nil) (neg_times_le formula-decl nil real_props nil) (neg_times_lt formula-decl nil real_props nil) (both_sides_times_pos_le2 formula-decl nil real_props nil) (both_sides_plus_le1 formula-decl nil real_props nil) (both_sides_times_pos_lt2 formula-decl nil real_props nil) (both_sides_minus_lt1 formula-decl nil real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_minus_real_is_real application-judgement "real" reals nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (sq const-decl "nonneg_real" sq "reals/") (lt_times_lt_any1 formula-decl nil extra_real_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (< const-decl "bool" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types 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) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (euclic_linear_lemma formula-decl nil cross_metric_spaces nil) (<= const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (d const-decl "nnreal" cross_metric_spaces nil) (nnreal type-eq-decl nil real_types nil) (d1 formal-const-decl "[T1, T1 -> nnreal]" cross_metric_spaces nil) (d2 formal-const-decl "[T2, T2 -> nnreal]" cross_metric_spaces nil) (d_square const-decl "nnreal" cross_metric_spaces nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T1 formal-nonempty-type-decl nil cross_metric_spaces nil) (T2 formal-nonempty-type-decl nil cross_metric_spaces nil) (set type-eq-decl nil sets nil) (ball const-decl "set[T]" metric_spaces nil) (subset? const-decl "bool" sets nil)) shostak)) (metric_equivalence2 0 (metric_equivalence2-1 nil 3459771920 ("" (skosimp*) (("" (lemma "metric_equivalence") (("" (inst - "fullset[[T1,T2]]" "V!1") (("" (lemma "open_in_fullset[[T1,T2],d]") (("" (lemma "open_in_fullset[[T1,T2],d_square]") (("" (inst - "V!1") (("" (inst - "V!1") (("" (replace -1) (("" (replace -2) (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((metric_equivalence formula-decl nil cross_metric_spaces nil) (d const-decl "nnreal" cross_metric_spaces nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (number nonempty-type-decl nil numbers nil) (open_in_fullset formula-decl nil metric_spaces nil) (d_square const-decl "nnreal" cross_metric_spaces nil) (fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T2 formal-nonempty-type-decl nil cross_metric_spaces nil) (T1 formal-nonempty-type-decl nil cross_metric_spaces nil)) shostak))) ¤ Dauer der Verarbeitung: 0.51 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 |
