| products/Sources/formale Sprachen/PVS/graphs/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: similarity_props.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(select_minmax
(v_min_TCC1 0 (v_min_TCC1-1 nil 3292345986 ("" (skosimp*) (("" (typepred "node_set!1") (("" (expand "empty?") (("" (expand "image") (("" (expand "member") (("" (skosimp*) (("" (inst - "v!1(x!1)") (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (below type-eq-decl nil naturalnumbers nil) (N formal-const-decl "posnat" select_minmax nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals 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) (image const-decl "set[R]" function_image nil) (x!1 skolem-const-decl "below(N)" select_minmax nil) (node_set!1 skolem-const-decl "non_empty_finite_set[below(N)]" select_minmax nil) (T formal-nonempty-type-decl nil select_minmax nil) (vec type-eq-decl nil node nil) (member const-decl "bool" sets nil)) shostak)) (v_min_witness 0 (v_min_witness-1 nil 3292346160 ("" (skosimp*) (("" (expand "v_min") (("" (typepred "min(image(v!1, node_set!1))") (("1" (hide -2) (("1" (rewrite "image" -1) (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (use "v_min_TCC1") nil nil)) nil)) nil)) nil) ((v_min const-decl "T" select_minmax nil) (v_min_TCC1 subtype-tcc nil select_minmax nil) (finite_image application-judgement "finite_set[R]" function_image_aux 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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (N formal-const-decl "posnat" select_minmax nil) (below type-eq-decl nil naturalnumbers nil) (T formal-nonempty-type-decl nil select_minmax nil) (set type-eq-decl nil sets nil) (image const-decl "set[R]" function_image nil) (vec type-eq-decl nil node nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" select_minmax nil) (min const-decl "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES a <= x)}" finite_sets_minmax "finite_sets/")) shostak)) (v_max_witness 0 (v_max_witness-1 nil 3292346450 ("" (skosimp*) (("" (expand "v_max") (("" (typepred "max(image(v!1, node_set!1))") (("1" (hide -2) (("1" (rewrite "image" -1) (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (use "v_min_TCC1") nil nil)) nil)) nil)) nil) ((v_max const-decl "T" select_minmax nil) (v_min_TCC1 subtype-tcc nil select_minmax nil) (finite_image application-judgement "finite_set[R]" function_image_aux 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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (N formal-const-decl "posnat" select_minmax nil) (below type-eq-decl nil naturalnumbers nil) (T formal-nonempty-type-decl nil select_minmax nil) (set type-eq-decl nil sets nil) (image const-decl "set[R]" function_image nil) (vec type-eq-decl nil node nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" select_minmax nil) (max const-decl "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" finite_sets_minmax "finite_sets/")) shostak)) (v_min_is_min 0 (v_min_is_min-1 nil 3292346679 ("" (skosimp*) (("" (expand "v_min") (("" (typepred "min(image(v!1, node_set!1))") (("" (inst?) (("" (assert) (("" (rewrite "image" +) (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((v_min const-decl "T" select_minmax nil) (finite_image application-judgement "finite_set[R]" function_image_aux 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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (N formal-const-decl "posnat" select_minmax nil) (below type-eq-decl nil naturalnumbers nil) (T formal-nonempty-type-decl nil select_minmax nil) (set type-eq-decl nil sets nil) (image const-decl "set[R]" function_image nil) (vec type-eq-decl nil node nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" select_minmax nil) (min const-decl "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES a <= x)}" finite_sets_minmax "finite_sets/")) shostak)) (v_max_is_max 0 (v_max_is_max-1 nil 3292346777 ("" (skosimp*) (("" (expand "v_max") (("" (typepred "max(image(v!1, node_set!1))") (("" (inst?) (("" (assert) (("" (rewrite "image" +) (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((v_max const-decl "T" select_minmax nil) (finite_image application-judgement "finite_set[R]" function_image_aux 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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (N formal-const-decl "posnat" select_minmax nil) (below type-eq-decl nil naturalnumbers nil) (T formal-nonempty-type-decl nil select_minmax nil) (set type-eq-decl nil sets nil) (image const-decl "set[R]" function_image nil) (vec type-eq-decl nil node nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" select_minmax nil) (max const-decl "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" finite_sets_minmax "finite_sets/")) shostak)) (min_le_max 0 (min_le_max-1 nil 3292710492 ("" (skosimp*) (("" (assert) (("" (use "v_min_witness") (("" (skosimp*) (("" (use "v_max_is_max") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((v_max_is_max formula-decl nil select_minmax 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (N formal-const-decl "posnat" select_minmax nil) (below type-eq-decl nil naturalnumbers nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (T formal-nonempty-type-decl nil select_minmax nil) (vec type-eq-decl nil node nil) (v_min_witness formula-decl nil select_minmax nil)) shostak)) (min_le_max_alt 0 (min_le_max_alt-1 nil 3302017915 ("" (skosimp*) (("" (typepred "<=") (("" (expand* "total_order?" "partial_order?" "preorder?") (("" (prop) (("1" (expand "reflexive?") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (use "min_le_max") (("2" (expand "antisymmetric?") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((<= formal-const-decl "(total_order?[T])" select_minmax nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (T formal-nonempty-type-decl nil select_minmax nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil 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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (N formal-const-decl "posnat" select_minmax nil) (below type-eq-decl nil naturalnumbers nil) (vec type-eq-decl nil node nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (v_max const-decl "T" select_minmax nil) (reflexive? const-decl "bool" relations nil) (antisymmetric? const-decl "bool" relations nil) (v_min const-decl "T" select_minmax nil) (min_le_max formula-decl nil select_minmax nil) (preorder? const-decl "bool" orders nil) (partial_order? const-decl "bool" orders nil)) shostak)) (v_minmax_choose 0 (v_minmax_choose-1 nil 3408879737 ("" (skosimp*) (("" (prop) (("1" (lemma "v_min_witness") (("1" (inst?) (("1" (lemma "v_max_witness") (("1" (inst?) (("1" (expand "uniform?") (("1" (skosimp*) (("1" (inst-cp - "n!2") (("1" (inst - "n!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "v_min_witness") (("2" (inst?) (("2" (skosimp*) (("2" (expand "uniform?") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "uniform?") (("3" (skosimp*) (("3" (lemma "v_min_is_min") (("3" (inst?) (("3" (inst?) (("3" (assert) (("3" (lemma "v_max_is_max") (("3" (inst?) (("3" (inst?) (("3" (assert) (("3" (replace*) (("3" (hide -3 -4 -5) (("3" (typepred "<=") (("3" (expand "total_order?") (("3" (expand "partial_order?") (("3" (expand "antisymmetric?") (("3" (flatten) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (N formal-const-decl "posnat" select_minmax nil) (below type-eq-decl nil naturalnumbers nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (T formal-nonempty-type-decl nil select_minmax nil) (vec type-eq-decl nil node nil) (uniform? const-decl "bool" node nil) (v_max_witness formula-decl nil select_minmax nil) (v_min_witness formula-decl nil select_minmax nil) (antisymmetric? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" select_minmax nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (v_max_is_max formula-decl nil select_minmax nil) (v_min_is_min formula-decl nil select_minmax nil)) nil)) (v_minmax_choose_alt 0 (v_minmax_choose_alt-1 nil 3408879760 ("" (skosimp*) (("" (expand "uniform?") (("" (prop) (("1" (use "v_max_witness") (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (replace*) (("1" (use "reflexive") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "v_min_witness") (("2" (skosimp*) (("2" (inst?) (("2" (assert) (("2" (replace*) (("2" (use "reflexive") nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (lemma "antisymmetric") (("3" (invoke (inst - "<=" "%1" "%2") (! 1 l) (! 1 r)) (("3" (assert) (("3" (lemma "transitive") (("3" (prop) (("1" (use "v_max_is_max") (("1" (assert) (("1" (inst - "<=" "v!1(n!1)" "v_max(v!1, node_set!1)" "t!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (use "v_min_is_min") (("2" (inst - "<=" "t!1" "v_min(v!1, node_set!1)" "v!1(n!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((uniform? const-decl "bool" node nil) (antisymmetric? const-decl "bool" relations nil) (transitive formula-decl nil relations_extra nil) (v_min_is_min formula-decl nil select_minmax nil) (v_min const-decl "T" select_minmax nil) (v_max_is_max formula-decl nil select_minmax nil) (v_max const-decl "T" select_minmax nil) (transitive? const-decl "bool" relations nil) (antisymmetric formula-decl nil relations_extra nil) (v_min_witness formula-decl nil select_minmax nil) (v_max_witness formula-decl nil select_minmax nil) (vec type-eq-decl nil node nil) (T formal-nonempty-type-decl nil select_minmax nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (below type-eq-decl nil naturalnumbers nil) (N formal-const-decl "posnat" select_minmax nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals 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) (reflexive formula-decl nil relations_extra nil) (<= formal-const-decl "(total_order?[T])" select_minmax nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (reflexive? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil)) nil))) ¤ Dauer der Verarbeitung: 0.9 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 |
