| products/Sources/formale Sprachen/PVS/orders/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: range_real.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(range_real
(real_no_minimum 0 (real_no_minimum-1 nil 3318613635 ("" (grind :if-match nil) (("" (inst - "t!1 - 1") (("" (assert) nil nil)) nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (no_least const-decl "bool" range nil) (has_least? const-decl "bool" minmax_orders nil) (least? const-decl "bool" minmax_orders nil) (lower_bound? const-decl "bool" bounded_orders 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) (restrict const-decl "R" restrict nil)) nil)) (real_no_maximum 0 (real_no_maximum-1 nil 3318613635 ("" (grind :if-match nil) (("" (inst - "t!1 + 1") (("" (assert) nil nil)) nil)) nil) ((real_plus_real_is_real application-judgement "real" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (no_greatest const-decl "bool" range nil) (has_greatest? const-decl "bool" minmax_orders nil) (greatest? const-decl "bool" minmax_orders nil) (upper_bound? const-decl "bool" bounded_orders 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) (restrict const-decl "R" restrict nil)) nil)) (ntc_range_infinite 0 (ntc_range_infinite-1 nil 3318613635 ("" (skolem-typepred) (("" (lemma "nat_infinite") (("" (expand* "is_finite" "is_finite_type") (("" (skolem!) (("" (inst + "N!1" "LAMBDA (n: nat): f!1((greatest[real](lesseq)(x!1) - least[real](lesseq)(x!1)) / (("1" (expand "injective?") (("1" (skosimp) (("1" (inst - "least[real](lesseq)(x!1) + (greatest[real](lesseq)(x!1) - least[real](lesseq)(x "least[real](lesseq)(x!1) + (greatest[real](lesseq)(x!1) - least[real](lesseq)(x (("1" (assert) (("1" (use "both_sides_div2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem!) (("2" (inst - "least[real](lesseq)(x!1)" "greatest[real](lesseq)(x!1)" "least[real](lesseq)(x!1) + (greatest[real](lesseq)(x!1) - least[real](lesseq)(x (("2" (expand "member") (("2" (assert) (("2" (split) (("1" (both-sides "-" "least[real](lesseq)(x!1)") (("1" (assert) (("1" (both-sides "*" "1 + n!1") (("1" (use "div_cancel2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (both-sides "-" "least[real](lesseq)(x!1)") (("2" (assert) (("2" (rewrite "div_mult_pos_le1") (("2" (lemma "le_times_le_pos") (("2" (inst - "greatest[real](lesseq)(x!1) - least[real](lesseq)(x!1)" "1" "1 + n!1" "greatest[real](lesseq)(x!1) - least[real](lesseq)(x!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nat_infinite formula-decl nil numbers_infinite nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (div_mult_pos_le2 formula-decl nil real_props nil) (zero_times1 formula-decl nil real_props nil) (div_cancel2 formula-decl nil real_props nil) (> const-decl "bool" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_times_real_is_real application-judgement "real" reals nil) (mult_divides2 application-judgement "(divides(m))" divides 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) (both_sides_minus_le1 formula-decl nil real_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (le_times_le_pos formula-decl nil real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (div_mult_pos_le1 formula-decl nil real_props nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (injective? const-decl "bool" functions nil) (both_sides_div2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props 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) (below type-eq-decl nil nat_types nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (x!1 skolem-const-decl "ntc_range" range_real nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" 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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (is_finite const-decl "bool" finite_sets nil) (is_finite_type const-decl "bool" finite_sets nil) (ntc_range type-eq-decl nil range nil) (greatest const-decl "{t: (S) | greatest?(t, S, <=)}" minmax_orders nil) (greatest? const-decl "bool" minmax_orders nil) (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil) (least? const-decl "bool" minmax_orders nil) (< const-decl "bool" reals nil) (c_range nonempty-type-eq-decl nil range nil) (has_greatest? const-decl "bool" minmax_orders nil) (restrict const-decl "R" restrict nil) (has_least? const-decl "bool" minmax_orders nil) (pred type-eq-decl nil defined_types nil) (range nonempty-type-eq-decl nil range nil) (member const-decl "bool" sets nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (set type-eq-decl nil sets 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)) nil)) (nto_range_infinite 0 (nto_range_infinite-1 nil 3318613635 ("" (skolem-typepred) (("" (expand* "nonempty?" "empty?" "member") (("" (skolem!) (("" (case "EXISTS (r: (x!1)): x!2 < r") (("1" (skolem!) (("1" (lemma "ntc_range_infinite") (("1" (inst - "nontrivial_closed_range(x!2, r!1)") (("1" (expand* "nontrivial_closed_range" "is_finite") (("1" (skolem!) (("1" (inst + "N!1" "LAMBDA (n: ({r: real | x!2 <= r AND r <= r!1})): f!1(n)") (("1" (expand "injective?") (("1" (skosimp :preds? t) (("1" (inst-cp - "x!2" "r!1" "x2!1") (("1" (inst - "x!2" "r!1" "x1!1") (("1" (assert) (("1" (inst - "x1!1" "x2!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem-typepred) (("2" (inst - "x!2" "r!1" "n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand* "has_greatest?" "has_non_greatest?") (("2" (split -3) (("1" (inst + "x!2") (("1" (expand* "greatest?" "upper_bound?") (("1" (assert) (("1" (skolem!) (("1" (expand "restrict" 1) (("1" (inst + "r!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -2 "(x!2 + r!1) / 2") (("2" (inst-cp - "x!2") (("2" (assert) (("2" (skolem!) (("2" (inst - "t!1") (("2" (inst + "t!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((empty? const-decl "bool" sets nil) (< const-decl "bool" reals nil) (ntc_range_infinite judgement-tcc nil range_real nil) (is_finite const-decl "bool" finite_sets nil) (below type-eq-decl nil nat_types 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_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (injective? const-decl "bool" functions nil) (nontrivial_closed_range const-decl "ntc_range" range nil) (ntc_range type-eq-decl nil range nil) (greatest const-decl "{t: (S) | greatest?(t, S, <=)}" minmax_orders nil) (greatest? const-decl "bool" minmax_orders nil) (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil) (least? const-decl "bool" minmax_orders nil) (c_range nonempty-type-eq-decl nil range nil) (x!2 skolem-const-decl "real" range_real nil) (x!1 skolem-const-decl "nto_range" range_real nil) (r!1 skolem-const-decl "(x!1)" range_real nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (upper_bound? const-decl "bool" bounded_orders nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_plus_real_is_real application-judgement "real" reals nil) (nto_range type-eq-decl nil range nil) (nonempty? const-decl "bool" sets nil) (o_range nonempty-type-eq-decl nil range nil) (has_non_greatest? const-decl "bool" range nil) (has_greatest? const-decl "bool" minmax_orders nil) (has_non_least? const-decl "bool" range nil) (restrict const-decl "R" restrict nil) (has_least? const-decl "bool" minmax_orders nil) (pred type-eq-decl nil defined_types nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (range nonempty-type-eq-decl nil range nil) (member const-decl "bool" sets nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (set type-eq-decl nil sets 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)) nil))) ¤ Dauer der Verarbeitung: 0.4 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 |
