| products/sources/formale Sprachen/PVS/exact_real_arith/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Rgeom.v Sprache: LispOriginal von: PVS© |
|
||||||
|
(mul
(D1 0 (D1-1 nil 3250064094 ("" (grind) 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) (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) (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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil)) (D2 0 (D2-1 nil 3250064094 ("" (grind) 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) (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) (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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (D3 0 (D3-1 nil 3250064094 ("" (grind) 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) (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) (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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (negreal_times_posreal_is_negreal 0 (negreal_times_posreal_is_negreal-1 nil 3250064094 ("" (skosimp*) (("" (lemma "neg_lt" ("x" "nx!1")) (("" (lemma "posreal_times_posreal_is_posreal" ("px" "py!1" "py" "-nx!1")) (("" (grind) nil nil)) nil)) nil)) nil) ((negreal nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (nonpos_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) (neg_lt formula-decl nil real_props nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_times_posreal_is_posreal judgement-tcc nil real_types 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 "[numfield -> numfield]" number_fields nil)) nil)) (lt_times_lt_nonneg1 0 (lt_times_lt_nonneg1-1 nil 3250064094 ("" (skosimp*) (("" (case "nnx!1=0") (("1" (replace -1) (("1" (lemma "both_sides_times_pos_lt2" ("pz" "x!1" "x" "nny!1" "y" "y!1")) (("1" (replace -1 -4 rl) (("1" (lemma "both_sides_times_pos_lt2" ("pz" "nny!1" "x" "0" "y" "x!1")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (case "0 (("1" (lemma "lt_times_lt_pos1" ("px" "nnx!1" "nnz" "nny!1" "y" "x!1" "w" "y!1")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) 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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (both_sides_times_pos_lt2 formula-decl nil real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (lt_times_lt_pos1 formula-decl nil real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (< const-decl "bool" reals nil)) nil)) (lt_times_lt_nonneg2 0 (lt_times_lt_nonneg2-1 nil 3250064094 ("" (skosimp*) (("" (typepred "nnx!1") (("" (expand ">=") (("" (expand "<=") (("" (split) (("1" (lemma "both_sides_times_neg_lt2" ("nz" "-1" "x" "x!1" "y" "nnx!1")) (("1" (lemma "lt_times_lt_neg1" ("ny" "-1 * nnx!1" "x" "-1 * x!1" "z" "y!1" "npw" "npy!1")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (replace -1 (-2 1) rl) (("2" (lemma "both_sides_times_pos_lt2" ("pz" "x!1" "y" "npy!1" "x" "y!1")) (("1" (lemma "negreal_times_posreal_is_negreal" ("nx" "y!1" "py" "x!1")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nonneg_real nonempty-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) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (<= const-decl "bool" reals nil) (negreal_times_posreal_is_negreal formula-decl nil mul nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (both_sides_times_pos_lt2 formula-decl nil real_props nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (negreal nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (both_sides_times_neg_lt2 formula-decl nil real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (lt_times_lt_neg1 formula-decl nil real_props nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (D_pp 0 (D_pp-1 nil 3250064094 ("" (skosimp*) (("" (lemma "D3" ("x" "px!1" "n" "n!1")) (("" (lemma "D3" ("x" "py!1" "n" "m!1")) (("" (lemma "lt_times_lt_nonneg1" ("nnx" "px!1" "x" "1+n!1" "nny" "py!1" "y" "1+m!1")) (("" (grind) (("" (case "1<=n!1") (("1" (case "1<=m!1") (("1" (lemma "lt_times_lt_nonneg1" ("nnx" "n!1 - 1" "x" "px!1" "nny" "m!1 - 1" "y" "py!1")) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil) ("2" (case "m!1=0") (("1" (grind) nil nil) ("2" (grind) (("2" (expand "<=" -5) (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "le_equiv_not_lt" ("x" "1" "y" "n!1")) (("2" (replace -1 1 lr) (("2" (hide -1) (("2" (rewrite "lt_equiv_le_plus_one") (("2" (lemma "both_sides_plus_le1" ("x" "n!1" "y" "0" "z" "1")) (("2" (replace -1 -2 lr) (("2" (hide -1) (("2" (lemma "total_le") (("2" (expand "total_order?") (("2" (expand "partial_order?") (("2" (expand "antisymmetric?") (("2" (flatten) (("2" (inst -2 "n!1" "0") (("2" (prop) (("2" (replace -1) (("2" (case "1<=m!1") (("1" (lemma "lt_times_lt_nonneg1" ("nnx" "0" "x" "px!1" "nny" "m!1 - 1" "y" "py!1")) (("1" (grind) nil nil) ("2" (assert) 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) ((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) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (D3 formula-decl nil mul nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (lt_times_lt_nonneg1 formula-decl nil mul nil) (int_plus_int_is_int application-judgement "int" integers nil) (<= const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (lt_equiv_le_plus_one formula-decl nil prelude_aux nil) (odd_minus_even_is_odd application-judgement "odd_int" integers nil) (total_le formula-decl nil real_props nil) (partial_order? const-decl "bool" orders nil) (even_times_int_is_even application-judgement "even_int" integers nil) (antisymmetric? const-decl "bool" relations nil) (total_order? const-decl "bool" orders nil) (both_sides_plus_le1 formula-decl nil real_props nil) (le_equiv_not_lt formula-decl nil prelude_aux nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (minus_int_is_int application-judgement "int" integers nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (D_pn 0 (D_pn-1 nil 3250064094 ("" (skosimp*) (("" (lemma "D_pp" ("px" "px!1" "n" "n!1" "py" "-ny!1" "m" "-m!1")) (("" (grind) nil nil)) nil)) nil) ((negreal nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (nonpos_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 "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 "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (D_pp formula-decl nil mul nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers 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)) nil)) (D_nn 0 (D_nn-1 nil 3250064094 ("" (skosimp*) (("" (lemma "D_pp" ("px" "-nx!1" "n" "-n!1" "py" "-ny!1" "m" "-m!1")) (("" (grind) nil nil)) nil)) nil) ((negreal nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (nonpos_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 "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 "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (D_pp formula-decl nil mul nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (negreal_times_negreal_is_posreal application-judgement "posreal" real_types nil) (int_plus_int_is_int application-judgement "int" integers nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (int_minus_int_is_int application-judgement "int" integers 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)) nil)) (D_p0 0 (D_p0-1 nil 3250064094 ("" (skosimp*) (("" (lemma "D1" ("x" "y!1" "n" "m!1")) (("" (lemma "D3" ("x" "px!1" "n" "n!1")) (("" (grind) nil nil)) nil)) nil)) nil) ((int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (D1 formula-decl nil mul nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (minus_int_is_int application-judgement "int" integers nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (D3 formula-decl nil mul 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)) nil)) (D_n0 0 (D_n0-1 nil 3250064094 ("" (skosimp*) (("" (lemma "D_p0" ("px" "-nx!1" "n" "-n!1" "y" "y!1" "m" "m!1")) (("" (grind) nil nil)) nil)) nil) ((negreal nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (nonpos_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 "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 "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (D_p0 formula-decl nil mul nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_times_real_is_real application-judgement "real" reals nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers 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)) nil)) (D 0 (D-1 nil 3250064094 ("" (skosimp*) (("" (lemma "trich_lt" ("x" "x!1" "y" "0")) (("" (split) (("1" (lemma "trich_lt" ("x" "y!1" "y" "0")) (("1" (split) (("1" (lemma "D_nn" ("n" "n!1" "m" "m!1" "nx" "x!1" "ny" "y!1")) (("1" (grind) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil) ("2" (lemma "D_n0" ("n" "n!1" "m" "m!1" "nx" "x!1" "y" "y!1")) (("1" (grind) nil nil) ("2" (assert) nil nil)) nil) ("3" (lemma "D_pn" ("m" "n!1" "n" "m!1" "ny" "x!1" "px" "y!1")) (("1" (grind) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "trich_lt" ("x" "y!1" "y" "0")) (("2" (split) (("1" (lemma "D_n0" ("m" "n!1" "n" "m!1" "y" "x!1" "nx" "y!1")) (("1" (grind) nil nil) ("2" (assert) nil nil)) nil) ("2" (grind) nil nil) ("3" (lemma "D_p0" ("m" "n!1" "n" "m!1" "y" "x!1" "px" "y!1")) (("1" (grind) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("3" (lemma "trich_lt" ("x" "y!1" "y" "0")) (("3" (split) (("1" (lemma "D_pn" ("n" "n!1" "m" "m!1" "ny" "y!1" "px" "x!1")) (("1" (grind) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil) ("2" (lemma "D_p0" ("n" "n!1" "m" "m!1" "y" "y!1" "px" "x!1")) (("1" (grind) nil nil) ("2" (assert) nil nil)) nil) ("3" (lemma "D_pp" ("n" "n!1" "m" "m!1" "py" "y!1" "px" "x!1")) (("1" (grind) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) 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) (trich_lt formula-decl nil real_props nil) (D_pp formula-decl nil mul nil) (D_p0 formula-decl nil mul nil) (even_minus_odd_is_odd application-judgement "odd_int" integers 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) (D_pn formula-decl nil mul nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_int_is_int application-judgement "int" integers nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (D_n0 formula-decl nil mul nil) (negreal nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (D_nn formula-decl nil mul nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil)) (mul_p1 0 (mul_p1-1 nil 3250064094 ("" (skosimp*) (("" (typepred "cx!1") (("" (expand "cauchy_real?") (("" (skolem!) (("" (expand "cauchy_prop") (("" (inst - "0") (("" (lemma "dich_le" ("x" "cx!1(0)" "y" "0")) (("" (name "r!1" "floor(log2(abs(cx!1(0))+2))") (("" (replace -1) (("" (lemma "lemma_A3" ("i" "r!1" "px" "abs(cx!1(0)) + 2")) (("" (replace -2) (("" (simplify -1) (("" (flatten) (("" (split -4) (("1" (lemma "abs_nonpos" ("npx" "cx!1(0)")) (("1" (replace -1) (("1" (lemma "both_sides_plus1" ("x" "s!1-3" "y" "r!1" "z" "3")) (("1" (simplify -1) (("1" (replace -1 -9) (("1" (lemma "expt_plus" ("n0x" "2" "i" "s!1-2" "j" "-1")) (("1" (simplify -1) (("1" (replace -10 1) (("1" (replace -10 -6 rl) (("1" (simplify -6) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (lemma "abs_nonneg" ("nnx" "cx!1(0)")) (("1" (lemma "lemma_A3" ("i" "r!1" "px" "abs(cx!1(0)) + 2")) (("1" (replace -6 -1) (("1" (replace -2) (("1" (simplify -1) (("1" (flatten) (("1" (lemma "both_sides_plus1" ("x" "s!1-3" "y" "r!1" "z" "3")) (("1" (replace -1 -11) (("1" (replace -11 -7 rl) (("1" (replace -11 -6 rl) (("1" (assert) 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) ((cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_real? const-decl "bool" cauchy nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (log2 const-decl "real" prelude_aux 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) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (lemma_A3 formula-decl nil appendix nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (posrat_exp application-judgement "posrat" exponentiation nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (minus_int_is_int application-judgement "int" integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (expt_plus formula-decl nil exponentiation nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (both_sides_plus1 formula-decl nil real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (npreal type-eq-decl nil real_types nil) (abs_nonpos formula-decl nil prelude_aux nil) (nnreal type-eq-decl nil real_types nil) (abs_nonneg formula-decl nil prelude_aux nil) (dich_le formula-decl nil real_props nil) (cauchy_prop const-decl "bool" cauchy nil) (posint_exp application-judgement "posint" exponentiation nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil)) nil)) (mul_p2 0 (mul_p2-1 nil 3250064094 ("" (skosimp*) (("" (split) (("1" (typepred "cx!1") (("1" (expand "cauchy_real?") (("1" (skolem!) (("1" (expand "cauchy_prop") (("1" (inst-cp - "p!1") (("1" (inst - "0") (("1" (expand "^" -1) (("1" (expand "expt") (("1" (flatten) (("1" (lemma "trich_lt" ("x" "x!1" "y" "0")) (("1" (split) (("1" (lemma "expt_ge1" ("b" "2" "n" "p!1-1")) (("1" (lemma "expt_ge1" ("b" "2" "n" "p!1")) (("1" (lemma "expt_plus" ("n0x" "2" "i" "p!1-1" "j" "1")) (("1" (expand "^" -1 3) (("1" (expand "expt") (("1" (expand "expt") (("1" (expand ">=") (("1" (lemma "both_sides_times_pos_le1" ("x" "1" "y" "2 ^ (p!1 - 1)" "pz" "2")) (("1" (replace -4) (("1" (replace -2 -1 rl) (("1" (simplify -1) (("1" (lemma "strict_lt") (("1" (expand "strict_total_order?") (("1" (expand "strict_order?") (("1" (expand "transitive?") (("1" (flatten) (("1" (inst-cp - "cx!1(0) - 1" "x!1" "0") (("1" (lemma "both_sides_times_pos_lt1" ("x" "x!1" "y" "0" "pz" "2^p!1")) (("1" (rewrite "zero_times1") (("1" (inst-cp - "cx!1(p!1) - 1" "x!1 * 2 ^ p!1" "0") (("1" (replace -11) (("1" (replace -14) (("1" (replace -12) (("1" (replace -1) (("1" (simplify) (("1" (rewrite "lt_equiv_le_plus_one" -4) (("1" (rewrite "lt_equiv_le_plus_one" -5) (("1" (lemma "abs_nonpos" ("npx" "cx!1(0)")) (("1" (lemma "abs_nonpos" ("npx" "cx!1(p!1)")) (("1" (replace -19) (("1" (replace -1) (("1" (replace -2) (("1" (lemma "both_sides_times_neg_le1" ("y" "1 + -cx!1(p!1)" "x" "2 * 2 ^ p!1 + -cx!1(0) * 2 ^ p!1" "nz" "-1")) (("1" (replace -1 1 rl) (("1" (simplify 1) (("1" (simplify 1) (("1" (lemma "both_sides_minus_lt1" ("x" "x!1 * 2 ^ p!1" "y" "1 + cx!1(p!1)" "z" "2")) (("1" (replace -1 -19 rl) (("1" (simplify -19) (("1" (lemma "both_sides_times_pos_lt1" ("x" "cx!1(0) - 1" "y" "x!1" "pz" "2^p!1")) (("1" (replace -1 -17 rl) (("1" (lemma "lt_minus_lt2" ("x" "(cx!1(0) - 1) * 2 ^ p!1" "y" "x!1 * 2 ^ p!1" "w" "2" "z" "2 ^ p!1")) (("1" (replace -13) (("1" (replace -18) (("1" (simplify -1) (("1" (inst - "cx!1(0) * 2 ^ p!1 - 2 * 2 ^ p!1" "x!1 * 2 ^ p!1 - 2" "cx!1(p!1) - 1") (("1" (assert) nil nil)) 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)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (replace -1) (("2" (rewrite "lt_equiv_le_plus_one") (("2" (rewrite "lt_plus_one_equiv_le") (("2" (rewrite "zero_times1") (("2" (rewrite "lt_equiv_le_plus_one") (("2" (rewrite "lt_plus_one_equiv_le") (("2" (lemma "total_le") (("2" (expand "total_order?") (("2" (expand "partial_order?") (("2" (expand "antisymmetric?") (("2" (flatten) (("2" (inst-cp - "cx!1(0)" "0") (("2" (inst - "cx!1(p!1)" "0") (("2" (replace -6) (("2" (replace -7) (("2" (replace -8) (("2" (replace -9) (("2" (simplify) (("2" (replace -2) (("2" (replace -3) (("2" (replace -11) (("2" (expand "abs") (("2" (lemma "expt_ge1" ("b" "2" --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.65 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 |
