| products/Sources/formale Sprachen/PVS/orders/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: relation_iterate.pvs Sprache: PVSOriginal von: PVS© |
|
||||||
|
(bounded_integers
(non_empty_bounded_above_has_greatest_lem 0 (non_empty_bounded_above_has_greatest_lem-1 nil 3314629024 ("" (induct "c" :name "NAT_induction") (("" (skosimp*) (("" (case "upper_bound?[T](i!1, S!1, restrict[[real, real], [T, T], boolean](<=))") (("1" (expand* "has_greatest?" "greatest?") (("1" (inst? +) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "upper_bound?" +) (("2" (expand "restrict" 1) (("2" (skolem!) (("2" (inst - "j!2 - r!1") (("1" (assert) (("1" (inst - "S!1" "r!1" "j!2") (("1" (assert) nil nil)) nil)) nil) ("2" (expand* "upper_bound?" "restrict") (("2" (inst - "r!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (r!1 skolem-const-decl "(S!1)" bounded_integers nil) (S!1 skolem-const-decl "set[T]" bounded_integers nil) (j!2 skolem-const-decl "T" bounded_integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (greatest? const-decl "bool" minmax_orders nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (NAT_induction formula-decl nil naturalnumbers nil) (has_greatest? const-decl "bool" minmax_orders nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (upper_bound? const-decl "bool" bounded_orders nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (T formal-subtype-decl nil bounded_integers nil) (T_pred const-decl "[int -> boolean]" bounded_integers nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers 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)) shostak)) (non_empty_bounded_above_has_greatest 0 (non_empty_bounded_above_has_greatest-1 nil 3314628965 ("" (skolem-typepred) (("" (expand* "non_empty_bounded_above?" "bounded_above?") (("" (flatten) (("" (rewrite "nonempty_exists") (("" (skosimp* :preds? t) (("" (hide -2 -1) (("" (lemma "non_empty_bounded_above_has_greatest_lem") (("" (inst?) (("" (inst?) (("" (inst - "t!1 - x!2") (("1" (assert) nil nil) ("2" (expand* "upper_bound?" "restrict") (("2" (inst - "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_above? const-decl "bool" bounded_orders nil) (nonempty_exists formula-decl nil sets_lemmas nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (x!2 skolem-const-decl "(x!1)" bounded_integers nil) (x!1 skolem-const-decl "(non_empty_bounded_above?)" bounded_integers nil) (t!1 skolem-const-decl "T" bounded_integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (upper_bound? const-decl "bool" bounded_orders nil) (restrict const-decl "R" restrict nil) (non_empty_bounded_above_has_greatest_lem formula-decl nil bounded_integers nil) (non_empty_bounded_above? const-decl "bool" non_empty_bounded_sets nil) (set type-eq-decl nil sets nil) (T formal-subtype-decl nil bounded_integers nil) (T_pred const-decl "[int -> boolean]" bounded_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) (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)) (non_empty_bounded_below_has_least_lem 0 (non_empty_bounded_below_has_least_lem-1 nil 3314629266 ("" (induct "c" :name "NAT_induction") (("" (skosimp*) (("" (case "lower_bound?[T](i!1, S!1, restrict[[real, real], [T, T], boolean](<=))") (("1" (expand* "has_least?" "least?") (("1" (inst? +) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "lower_bound?" +) (("2" (expand "restrict" 1) (("2" (skolem!) (("2" (inst - "r!1 - j!2") (("1" (assert) (("1" (inst - "S!1" "r!1" "j!2") (("1" (assert) nil nil)) nil)) nil) ("2" (expand* "lower_bound?" "restrict") (("2" (inst - "r!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (j!2 skolem-const-decl "T" bounded_integers nil) (r!1 skolem-const-decl "(S!1)" bounded_integers nil) (S!1 skolem-const-decl "set[T]" bounded_integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (least? const-decl "bool" minmax_orders nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (NAT_induction formula-decl nil naturalnumbers nil) (has_least? const-decl "bool" minmax_orders nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (lower_bound? const-decl "bool" bounded_orders nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (T formal-subtype-decl nil bounded_integers nil) (T_pred const-decl "[int -> boolean]" bounded_integers nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers 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)) shostak)) (non_empty_bounded_below_has_least 0 (non_empty_bounded_below_has_least-1 nil 3314628965 ("" (skolem-typepred) (("" (expand* "non_empty_bounded_below?" "bounded_below?") (("" (flatten) (("" (rewrite "nonempty_exists") (("" (skosimp* :preds? t) (("" (hide -2 -1) (("" (lemma "non_empty_bounded_below_has_least_lem") (("" (inst?) (("" (inst?) (("" (inst - "x!2 - t!1") (("1" (assert) nil nil) ("2" (expand* "lower_bound?" "restrict") (("2" (inst - "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_below? const-decl "bool" bounded_orders nil) (nonempty_exists formula-decl nil sets_lemmas nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (t!1 skolem-const-decl "T" bounded_integers nil) (x!2 skolem-const-decl "(x!1)" bounded_integers nil) (x!1 skolem-const-decl "(non_empty_bounded_below?)" bounded_integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (lower_bound? const-decl "bool" bounded_orders nil) (restrict const-decl "R" restrict nil) (non_empty_bounded_below_has_least_lem formula-decl nil bounded_integers nil) (non_empty_bounded_below? const-decl "bool" non_empty_bounded_sets nil) (set type-eq-decl nil sets nil) (T formal-subtype-decl nil bounded_integers nil) (T_pred const-decl "[int -> boolean]" bounded_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) (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)) (remove_least_TCC1 0 (remove_least_TCC1-1 nil 3314628965 ("" (skosimp) (("" (rewrite "non_empty_bounded_below_has_least") (("" (expand "non_empty_bounded_below?") (("" (propax) nil nil)) nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (remove_preserves_bounded_below application-judgement "(LAMBDA (S: set[T]): bounded_below?(S, R))" bounded_integers nil) (non_empty_bounded_below_has_least judgement-tcc nil bounded_integers 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) (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) (T_pred const-decl "[int -> boolean]" bounded_integers nil) (T formal-subtype-decl nil bounded_integers nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (non_empty_bounded_below? const-decl "bool" non_empty_bounded_sets nil) (remove const-decl "set" sets nil) (pred type-eq-decl nil defined_types nil) (has_least? const-decl "bool" minmax_orders nil) (least? const-decl "bool" minmax_orders nil) (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil) (restrict const-decl "R" restrict nil) (<= const-decl "bool" reals nil)) nil)) (remove_least 0 (remove_least-1 nil 3314629437 ("" (skosimp) (("" (invoke (typepred "%1" "%2") (! 1 l) (! 1 r)) (("" (hide -4 -1) (("" (invoke (name-replace "X" "%1") (! 1 l)) (("" (invoke (name-replace "Y" "%1") (! 1 r)) (("" (expand* "least?" "remove" "member" "/=" "lower_bound?" "restrict") (("" (flatten) (("" (inst - "Y") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((remove_preserves_bounded_below application-judgement "(LAMBDA (S: set[T]): bounded_below?(S, R))" bounded_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) (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) (T_pred const-decl "[int -> boolean]" bounded_integers nil) (T formal-subtype-decl nil bounded_integers nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (has_least? const-decl "bool" minmax_orders nil) (least? const-decl "bool" minmax_orders nil) (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil) (restrict const-decl "R" restrict nil) (<= const-decl "bool" reals nil) (non_empty_bounded_below? const-decl "bool" non_empty_bounded_sets nil) (remove const-decl "set" sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal nil) (lower_bound? const-decl "bool" bounded_orders nil) (member const-decl "bool" sets nil) (Sl!1 skolem-const-decl "(non_empty_bounded_below?)" bounded_integers nil) (X skolem-const-decl "{t: (Sl!1) | least?(t, Sl!1, restrict[[real, real], [T, T], bool](<=))}" bounded_integers nil) (Y skolem-const-decl "{t: (remove(X, Sl!1)) | least?(t, remove(X, Sl!1), restrict[[real, real], [T, T], bool](<=))}" bounded_integers 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)) shostak)) (remove_least_monotone 0 (remove_least_monotone-1 nil 3314629975 ("" (expand* "subset?" "remove" "member") (("" (skosimp*) (("" (inst-cp - "x!1") (("" (prop) (("" (invoke (typepred "%1") (! -1 l)) (("" (replace -4 :hide? t) (("" (use "antisymmetric_restrict[real, T]") (("" (rewrite "least_def") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((least_def formula-decl nil minmax_orders nil) (lower_bound? const-decl "bool" bounded_orders nil) (Sl2!1 skolem-const-decl "(non_empty_bounded_below?)" bounded_integers nil) (Sl1!1 skolem-const-decl "(non_empty_bounded_below?)" bounded_integers nil) (r!1 skolem-const-decl "(Sl1!1)" bounded_integers nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (antisymmetric? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (antisymmetric_restrict judgement-tcc nil restrict_order_props nil) (non_empty_bounded_below? const-decl "bool" non_empty_bounded_sets nil) (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil) (least? const-decl "bool" minmax_orders nil) (has_least? const-decl "bool" minmax_orders nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (T formal-subtype-decl nil bounded_integers nil) (T_pred const-decl "[int -> boolean]" bounded_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) (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) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (remove const-decl "set" sets nil)) shostak)) (remove_greatest_TCC1 0 (remove_greatest_TCC1-1 nil 3314628965 ("" (skosimp) (("" (rewrite "non_empty_bounded_above_has_greatest") (("" (expand "non_empty_bounded_above?") (("" (propax) nil nil)) nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (remove_preserves_bounded_above application-judgement "(LAMBDA (S: set[T]): bounded_above?(S, R))" bounded_integers nil) (non_empty_bounded_above_has_greatest judgement-tcc nil bounded_integers 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) (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) (T_pred const-decl "[int -> boolean]" bounded_integers nil) (T formal-subtype-decl nil bounded_integers nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (non_empty_bounded_above? const-decl "bool" non_empty_bounded_sets nil) (remove const-decl "set" sets nil) (pred type-eq-decl nil defined_types nil) (has_greatest? const-decl "bool" minmax_orders nil) (greatest? const-decl "bool" minmax_orders nil) (greatest const-decl "{t: (S) | greatest?(t, S, <=)}" minmax_orders nil) (restrict const-decl "R" restrict nil) (<= const-decl "bool" reals nil)) nil)) (remove_greatest 0 (remove_greatest-1 nil 3314629695 ("" (skosimp) (("" (invoke (typepred "%1" "%2") (! 1 r) (! 1 l)) (("" (hide -4 -1) (("" (invoke (name-replace "X" "%1") (! 1 l)) (("" (invoke (name-replace "Y" "%1") (! 1 r)) (("" (expand* "greatest?" "remove" "member" "/=" "upper_bound?" "restrict") (("" (flatten) (("" (inst - "X") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((remove_preserves_bounded_above application-judgement "(LAMBDA (S: set[T]): bounded_above?(S, R))" bounded_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) (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) (T_pred const-decl "[int -> boolean]" bounded_integers nil) (T formal-subtype-decl nil bounded_integers nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (has_greatest? const-decl "bool" minmax_orders nil) (greatest? const-decl "bool" minmax_orders nil) (greatest const-decl "{t: (S) | greatest?(t, S, <=)}" minmax_orders nil) (restrict const-decl "R" restrict nil) (<= const-decl "bool" reals nil) (non_empty_bounded_above? const-decl "bool" non_empty_bounded_sets nil) (remove const-decl "set" sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal nil) (upper_bound? const-decl "bool" bounded_orders nil) (member const-decl "bool" sets nil) (Su!1 skolem-const-decl "(non_empty_bounded_above?)" bounded_integers nil) (X skolem-const-decl "{t: (remove(greatest[T](restrict[[real, real], [T, T], bool](<=))(Su!1), Su!1)) | greatest?(t, remove(greatest[T] (restrict[[real, real], [T, T], bool](<=)) (Su!1), Su!1), restrict[[real, real], [T, T], bool](<=))}" bounded_integers 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)) shostak)) (remove_greatest_monotone 0 (remove_greatest_monotone-1 nil 3314630088 ("" (expand* "subset?" "remove" "member") (("" (skosimp*) (("" (inst-cp - "x!1") (("" (prop) (("" (invoke (typepred "%1") (! -1 l)) (("" (replace -4 :hide? t) (("" (use "antisymmetric_restrict[real, T]") (("" (rewrite "greatest_def") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((greatest_def formula-decl nil minmax_orders nil) (upper_bound? const-decl "bool" bounded_orders nil) (Su2!1 skolem-const-decl "(non_empty_bounded_above?)" bounded_integers nil) (Su1!1 skolem-const-decl "(non_empty_bounded_above?)" bounded_integers nil) (r!1 skolem-const-decl "(Su1!1)" bounded_integers nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (antisymmetric? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (antisymmetric_restrict judgement-tcc nil restrict_order_props nil) (non_empty_bounded_above? const-decl "bool" non_empty_bounded_sets nil) (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (greatest const-decl "{t: (S) | greatest?(t, S, <=)}" minmax_orders nil) (greatest? const-decl "bool" minmax_orders nil) (has_greatest? const-decl "bool" minmax_orders nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (T formal-subtype-decl nil bounded_integers nil) (T_pred const-decl "[int -> boolean]" bounded_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) (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) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (remove const-decl "set" sets nil)) shostak)) (intersection_greatest 0 (intersection_greatest-1 nil 3314634466 ("" (skosimp :preds? t) (("" (lemma "non_empty_bounded_above_has_greatest") (("" (inst-cp - "Su2!1") (("" (inst - "Su1!1") (("" (expand* "disjoint?" "empty?" "member") (("" (expand "restrict") (("" (skolem!) (("" (lemma "non_empty_bounded_above_has_greatest_lem") (("" (inst - "intersection(Su1!1, Su2!1)" "max(greatest[T](restrict[[real, real], [T, T], bool](<=))(Su1!1), greatest[T](restrict[[real, real], [T, T], bool](<=))(Su2!1)) - x!1" "x!1" "max(greatest[T](restrict[[real, real], [T, T], bool](<=))(Su1!1), greatest[T](restrict[[real, real], [T, T], bool](<=))(Su2!1))") (("1" (assert) (("1" (expand "restrict") (("1" (expand* "upper_bound?" "max") (("1" (skolem-typepred) (("1" (expand* "intersection" "member") (("1" (lift-if) (("1" (prop) (("1" (lemma "greatest_ge") (("1" (inst - "restrict[[real, real], [T, T], bool](<=)" "Su2!1" "r!1") (("1" (expand "restrict") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "greatest_ge") (("2" (inst - "restrict[[real, real], [T, T], bool](<=)" "Su1!1" "r!1") (("2" (expand "restrict") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "max") (("2" (expand* "max" "intersection" "member") (("2" (expand "restrict") (("2" (propax) nil nil)) nil)) nil)) nil) ("3" (expand* "max" "intersection" "member") (("3" (lift-if) (("3" (prop) (("1" (lemma "greatest_ge") (("1" (inst - "restrict[[real, real], [T, T], bool](<=)" "Su2!1" "x!1") (("1" (expand "restrict" -1 :occurrence 1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "greatest_ge") (("2" (inst - "restrict[[real, real], [T, T], bool](<=)" "Su1!1" "x!1") (("2" (expand "restrict" -1 :occurrence 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((non_empty_bounded_above_has_greatest judgement-tcc nil bounded_integers nil) (restrict const-decl "R" restrict nil) (non_empty_bounded_above_has_greatest_lem formula-decl nil bounded_integers nil) (upper_bound? const-decl "bool" bounded_orders nil) (r!1 skolem-const-decl "(intersection(Su1!1, Su2!1))" bounded_integers nil) (greatest_ge formula-decl nil minmax_orders nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (intersection const-decl "set" sets nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (x!1 skolem-const-decl "T" bounded_integers nil) (Su2!1 skolem-const-decl "(non_empty_bounded_above?)" bounded_integers nil) (Su1!1 skolem-const-decl "(non_empty_bounded_above?)" bounded_integers nil) (<= const-decl "bool" reals nil) (greatest const-decl "{t: (S) | greatest?(t, S, <=)}" minmax_orders nil) (greatest? const-decl "bool" minmax_orders nil) (has_greatest? const-decl "bool" minmax_orders nil) (pred type-eq-decl nil defined_types nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (>= const-decl "bool" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_max application-judgement "{k: int | i <= k AND j <= k}" real_defs nil) (rat_max application-judgement "{s: rat | s >= q AND s >= r}" real_defs 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_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (disjoint? const-decl "bool" sets nil) (intersection1_preserves_bounded_above application-judgement "(LAMBDA (S: set[T]): bounded_above?(S, R))" bounded_integers nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets 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) (T_pred const-decl "[int -> boolean]" bounded_integers nil) (T formal-subtype-decl nil bounded_integers nil) (set type-eq-decl nil sets nil) (non_empty_bounded_above? const-decl "bool" non_empty_bounded_sets nil)) shostak)) (intersection_least 0 (intersection_least-1 nil 3314635936 ("" (auto-rewrite "restrict") (("" (skosimp :preds? t) (("" (lemma "non_empty_bounded_below_has_least") (("" (inst-cp - "Sl2!1") (("" (inst - "Sl1!1") (("" (expand* "disjoint?" "empty?" "member") (("" (skolem!) (("" (lemma "non_empty_bounded_below_has_least_lem") (("" (inst - "intersection(Sl1!1, Sl2!1)" "x!1 - min(least[T](restrict[[real, real], [T, T], bool](<=))(Sl1!1), least[T](restrict[[real, real], [T, T], bool](<=))(Sl2!1))" "x!1" "min(least[T](restrict[[real, real], [T, T], bool](<=))(Sl1!1), least[T](restrict[[real, real], [T, T], bool](<=))(Sl2!1))") (("1" (assert) (("1" (expand* "lower_bound?" "min") (("1" (skolem-typepred) (("1" (expand* "intersection" "member") (("1" (lift-if) (("1" (prop) (("1" (lemma "least_le") (("1" (inst - "restrict[[real, real], [T, T], bool](<=)" "Sl2!1" "r!1") nil nil)) nil) ("2" (lemma "least_le") (("2" (inst - "restrict[[real, real], [T, T], bool](<=)" "Sl1!1" "r!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "min") (("2" (expand* "min" "intersection" "member") (("2" (prop) (("1" (lemma "least_le") (("1" (inst - "restrict[[real, real], [T, T], bool](<=)" "Sl2!1" "x!1") (("1" (expand "restrict" -1 :occurrence 1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "least_le") (("2" (inst - "restrict[[real, real], [T, T], bool](<=)" "Sl1!1" "x!1") (("2" (expand "restrict" -1 :occurrence 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand* "min" "intersection" "member") (("3" (lift-if) (("3" (prop) (("1" (lemma "least_le") (("1" (inst - "restrict[[real, real], [T, T], bool](<=)" "Sl2!1" "x!1") (("1" (expand "restrict" -1 :occurrence 1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "least_le") (("2" (inst - "restrict[[real, real], [T, T], bool](<=)" "Sl1!1" "x!1") (("2" (expand "restrict" -1 :occurrence 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((non_empty_bounded_below? const-decl "bool" non_empty_bounded_sets nil) (set type-eq-decl nil sets nil) (T formal-subtype-decl nil bounded_integers nil) (T_pred const-decl "[int -> boolean]" bounded_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) (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) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (intersection1_preserves_bounded_below application-judgement "(LAMBDA (S: set[T]): bounded_below?(S, R))" bounded_integers nil) (disjoint? const-decl "bool" sets nil) (non_empty_bounded_below_has_least_lem formula-decl nil bounded_integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (least_le formula-decl nil minmax_orders nil) (r!1 skolem-const-decl "(intersection(Sl1!1, Sl2!1))" bounded_integers nil) (lower_bound? const-decl "bool" bounded_orders nil) (intersection const-decl "set" sets nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (Sl2!1 skolem-const-decl "(non_empty_bounded_below?)" bounded_integers nil) (Sl1!1 skolem-const-decl "(non_empty_bounded_below?)" bounded_integers nil) (restrict const-decl "R" restrict nil) (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil) (least? const-decl "bool" minmax_orders nil) (has_least? const-decl "bool" minmax_orders nil) (pred type-eq-decl nil defined_types nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (x!1 skolem-const-decl "T" bounded_integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (>= const-decl "bool" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs 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_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (non_empty_bounded_below_has_least judgement-tcc nil bounded_integers nil)) shostak))) ¤ Dauer der Verarbeitung: 0.73 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 |
