| products/Sources/formale Sprachen/PVS/orders/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: well_ordered_finite.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(well_ordered_finite
(nonempty_has_least 0 (nonempty_has_least-1 nil 3318621627 ("" (skolem-typepred) (("" (expand* "nonempty?" "empty?" "member") (("" (skolem!) (("" (lemma "non_empty_finite_has_least") (("" (inst - "{t | x!1(t) AND reflexive_closure(<)(t, x!2)}" "reflexive_closure(<)") (("1" (expand "has_least?") (("1" (skolem!) (("1" (inst + "t!1") (("1" (typepred "<") (("1" (grind :if-match nil) (("1" (inst -7 "r!1") (("1" (assert) nil nil) ("2" (inst - "t!1" "r!1") (("2" (inst - "r!1" "t!1" "x!2") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (inst - "r!1" "x!2") (("2" (assert) (("2" (inst -6 "r!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split) (("1" (use "finite_below") (("1" (expand "is_finite") (("1" (skolem!) (("1" (inst + "N!1 + 1" "LAMBDA (r: ({t | x!1(t) AND reflexive_closure[T](<)(t, x!2)})): IF r = x!2 THEN 0 ELSE f!1(r) + 1 ENDIF") (("1" (expand "injective?") (("1" (skosimp :preds? t) (("1" (lift-if) (("1" (lift-if) (("1" (ground) (("1" (lift-if) (("1" (split -1) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (inst - "x1!1" "x2!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil) ("3" (skosimp :preds? t) (("3" (expand* "below" "reflexive_closure" "union" "irreflexive_kernel" "difference" "member") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand* "reflexive_closure" "union" "empty?" "member") (("2" (inst - "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (non_empty_finite_has_least formula-decl nil minmax_orders nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (order? const-decl "bool" relations_extra nil) (prefix? const-decl "bool" ordered_subset nil) (below const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset nil) (f!1 skolem-const-decl "[(below(x!2, <)) -> below[N!1]]" well_ordered_finite nil) (below type-eq-decl nil nat_types nil) (N!1 skolem-const-decl "nat" well_ordered_finite 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) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (IF const-decl "[boolean, T, T -> T]" if_def nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (injective? const-decl "bool" functions nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil) (difference const-decl "set" sets nil) (finite_below formula-decl nil well_ordered_finite nil) (has_least? const-decl "bool" minmax_orders nil) (least? const-decl "bool" minmax_orders nil) (lower_bound? const-decl "bool" bounded_orders nil) (union const-decl "set" sets nil) (trichotomous? const-decl "bool" orders nil) (strict_order? const-decl "bool" orders nil) (transitive? const-decl "bool" relations nil) (irreflexive? const-decl "bool" relations nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (r!1 skolem-const-decl "(x!1)" well_ordered_finite nil) (total_order? const-decl "bool" orders nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (is_finite const-decl "bool" finite_sets nil) (x!1 skolem-const-decl "(nonempty?[T])" well_ordered_finite nil) (pred type-eq-decl nil defined_types nil) (PRED type-eq-decl nil defined_types nil) (reflexive? const-decl "bool" relations nil) (reflexive_closure const-decl "(reflexive?)" closure_ops nil) (strict_total_order? const-decl "bool" orders nil) (< formal-const-decl "(strict_total_order?[T])" well_ordered_finite nil) (x!2 skolem-const-decl "T" well_ordered_finite nil) (linear_order_to_total_order application-judgement "(total_order?)" well_ordered_finite nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil well_ordered_finite nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (finite_well_ordered 0 (finite_well_ordered-1 nil 3318621627 ("" (expand* "well_ordered?" "well_founded?") (("" (skosimp*) (("" (use "nonempty_has_least") (("1" (assert) (("1" (typepred "least[T](reflexive_closure[T](<))(p!1)") (("1" (inst + "least(reflexive_closure[T](<))(p!1)") (("1" (skolem!) (("1" (expand* "least?" "lower_bound?") (("1" (inst - "x!1") (("1" (expand "reflexive_closure" -2 :occurrence 1) (("1" (expand* "union" "member") (("1" (typepred "<") (("1" (expand* "strict_total_order?" "strict_order?" "irreflexive?" "transitive?") (("1" (flatten) (("1" (inst - "x!1") (("1" (inst - "x!1" "least(reflexive_closure[T](<))(p!1)" "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand* "nonempty?" "empty?" "member") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ((empty? const-decl "bool" sets nil) (linear_order_to_total_order application-judgement "(total_order?)" well_ordered_finite nil) (lower_bound? const-decl "bool" bounded_orders nil) (irreflexive? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (strict_order? const-decl "bool" orders nil) (union const-decl "set" sets nil) (member const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans 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) (PRED type-eq-decl nil defined_types nil) (reflexive? const-decl "bool" relations nil) (reflexive_closure const-decl "(reflexive?)" closure_ops nil) (strict_total_order? const-decl "bool" orders nil) (< formal-const-decl "(strict_total_order?[T])" well_ordered_finite nil) (p!1 skolem-const-decl "pred[T]" well_ordered_finite nil) (pred type-eq-decl nil defined_types nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil well_ordered_finite nil) (nonempty_has_least judgement-tcc nil well_ordered_finite nil) (well_ordered? const-decl "bool" orders nil) (well_founded? const-decl "bool" orders nil)) nil)) (nonlast_has_next 0 (nonlast_has_next-1 nil 3318621627 ("" (skolem-typepred) (("" (typepred "<") (("" (case "EXISTS (t: T): FORALL (r: (fullset[T])): (r < t) OR (r = t)") (("1" (grind :if-match nil) (("1" (typepred "greatest(union(<, =))(fullset[T])") (("1" (expand* "greatest?" "upper_bound?" "fullset") (("1" (inst - "x!1") (("1" (expand "union" -1 :occurrence 1) (("1" (expand "member") (("1" (assert) (("1" (inst -7 "greatest(union(<, =))({x: T | TRUE})") (("1" (assert) nil nil) ("2" (inst + "t!1") (("2" (skosimp) (("2" (inst - "r!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "t!1") nil nil)) nil)) nil) ("2" (inst + "x!1") (("2" (skosimp) (("2" (expand* "has_next?" "above" "nonempty?" "empty?" "irreflexive_kernel" "difference" "member" "well_ordered?" "strict_total_order?" "trichotomous?") (("2" (flatten) (("2" (inst - "r!1" "x!1") (("2" (inst - "r!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((finite_well_ordered name-judgement "(well_ordered?)" well_ordered_finite nil) (irreflexive? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (strict_order? const-decl "bool" orders nil) (trichotomous? const-decl "bool" orders nil) (well_founded? const-decl "bool" orders nil) (reflexive_closure const-decl "(reflexive?)" closure_ops nil) (member const-decl "bool" sets nil) (union const-decl "set" sets nil) (upper_bound? const-decl "bool" bounded_orders nil) (greatest? const-decl "bool" minmax_orders nil) (has_greatest? const-decl "bool" minmax_orders nil) (has_last? const-decl "bool" well_ordered_traversal nil) (last const-decl "(LAMBDA (t: T): greatest?(t, fullset[T], reflexive_closure(<)))" well_ordered_traversal nil) (irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil) (difference const-decl "set" sets nil) (above const-decl "(LAMBDA (S): suffix?(S, ord))" ordered_subset nil) (empty? const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil) (has_next? const-decl "bool" well_ordered_traversal nil) (linear_order_to_total_order application-judgement "(total_order?)" well_ordered_finite nil) (TRUE const-decl "bool" booleans nil) (greatest const-decl "{t: (S) | greatest?(t, S, <=)}" minmax_orders nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (fullset const-decl "set" sets nil) (< formal-const-decl "(strict_total_order?[T])" well_ordered_finite nil) (strict_total_order? const-decl "bool" orders nil) (nonlast const-decl "set[T]" well_ordered_traversal nil) (set type-eq-decl nil sets nil) (well_ordered? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (T formal-type-decl nil well_ordered_finite nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (nonfirst_has_prev 0 (nonfirst_has_prev-1 nil 3318621627 ("" (skolem-typepred) (("" (use "nonempty_has_least") (("1" (typepred "<") (("1" (use "finite_below") (("1" (lemma "non_empty_finite_has_greatest") (("1" (inst - "below(x!1, <)" "reflexive_closure(<)") (("1" (expand* "has_greatest?" "greatest?" "upper_bound?" "has_prev?") (("1" (skosimp) (("1" (inst + "t!1") (("1" (typepred "next(<)(t!1)") (("1" (expand* "least?" "lower_bound?") (("1" (flatten) (("1" (expand "below" -3) (("1" (expand* "above" "irreflexive_kernel" "difference" "reflexive_closure" "union" "member") (("1" (flatten) (("1" (inst - "x!1") (("1" (assert) (("1" (inst - "next(<)(t!1)") (("1" (assert) (("1" (expand* "well_ordered?" "strict_total_order?" "strict_order?" "irreflexive?" "transitive?") (("1" (flatten) (("1" (inst - "t!1") (("1" (inst - "t!1" "next(<)(t!1)" "t!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand* "below" "irreflexive_kernel" "difference" "member") nil nil)) nil)) nil) ("2" (expand* "above" "irreflexive_kernel" "difference" "member") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand* "has_next?" "nonempty?" "empty?" "member" "above" "below" "irreflexive_kernel" "difference" "member") (("2" (flatten) (("2" (inst - "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (rewrite "nonfirst") (("2" (lift-if) (("2" (expand "emptyset") (("2" (ground) (("2" (expand "first") (("2" (typepred "least(reflexive_closure(<))(fullset[T])") (("2" (expand* "least?" "fullset" "lower_bound?") (("2" (expand "reflexive_closure" -1 :occurrence 1) (("2" (expand* "union" "member") (("2" (inst - "x!1") (("2" (assert) (("2" (expand "below" -5) (("2" (expand* "empty?" "irreflexive_kernel" "difference" "member") (("2" (inst - "least(reflexive_closure(<))({x: T | TRUE})") (("1" (assert) nil nil) ("2" (expand "has_least?" +) (("2" (expand* "well_ordered?" "well_founded?") (("2" (flatten) (("2" (inst - "{x: T | TRUE}") (("2" (split) (("1" (skolem!) (("1" (inst + "y!1") (("1" (expand* "least?" "lower_bound?" "reflexive_closure" "union" "member") (("1" (skosimp) (("1" (inst - "r!1") (("1" (expand* "strict_total_order?" "trichotomous?") (("1" (flatten) (("1" (inst - "r!1" "y!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "x!1") 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" (grind :if-match all) nil nil)) nil)) nil) ((nonempty_has_least judgement-tcc nil well_ordered_finite nil) (nonempty? const-decl "bool" sets nil) (finite_well_ordered name-judgement "(well_ordered?)" well_ordered_finite nil) (finite_below formula-decl nil well_ordered_finite nil) (linear_order_to_total_order application-judgement "(total_order?)" well_ordered_finite nil) (empty? const-decl "bool" sets nil) (x!1 skolem-const-decl "(nonfirst(<))" well_ordered_finite nil) (below const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset nil) (prefix? const-decl "bool" ordered_subset nil) (order? const-decl "bool" relations_extra nil) (is_finite const-decl "bool" finite_sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (total_order? const-decl "bool" orders nil) (PRED type-eq-decl nil defined_types nil) (reflexive? const-decl "bool" relations nil) (reflexive_closure const-decl "(reflexive?)" closure_ops nil) (least? const-decl "bool" minmax_orders nil) (suffix? const-decl "bool" ordered_subset nil) (above const-decl "(LAMBDA (S): suffix?(S, ord))" ordered_subset nil) (next const-decl "(LAMBDA (t_1: T): least?(t_1, above(t, <), reflexive_closure(<)))" well_ordered_traversal nil) (irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil) (member const-decl "bool" sets nil) (union const-decl "set" sets nil) (difference const-decl "set" sets nil) (irreflexive? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (strict_order? const-decl "bool" orders nil) (lower_bound? const-decl "bool" bounded_orders nil) (t!1 skolem-const-decl "T" well_ordered_finite nil) (has_next? const-decl "bool" well_ordered_traversal nil) (has_greatest? const-decl "bool" minmax_orders nil) (upper_bound? const-decl "bool" bounded_orders nil) (has_prev? const-decl "bool" well_ordered_traversal nil) (greatest? const-decl "bool" minmax_orders nil) (emptyset const-decl "set" sets nil) (first const-decl "(LAMBDA (t: T): least?(t, fullset[T], reflexive_closure(<)))" well_ordered_traversal nil) (trichotomous? const-decl "bool" orders nil) (well_founded? const-decl "bool" orders nil) (TRUE const-decl "bool" booleans nil) (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil) (has_least? const-decl "bool" minmax_orders nil) (fullset const-decl "set" sets nil) (non_empty_finite_has_greatest formula-decl nil minmax_orders nil) (has_first? const-decl "bool" well_ordered_traversal nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (finite_emptyset name-judgement "finite_set[T]" well_ordered_finite nil) (< formal-const-decl "(strict_total_order?[T])" well_ordered_finite nil) (strict_total_order? const-decl "bool" orders nil) (nonfirst const-decl "set[T]" well_ordered_traversal nil) (set type-eq-decl nil sets nil) (well_ordered? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (T formal-type-decl nil well_ordered_finite nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (finite_last 0 (finite_last-1 nil 3318636396 ("" (typepred "<") (("" (expand* "has_last?" "has_greatest?" "greatest?" "fullset" "upper_bound?" "reflexive_closure" "union" "member") (("" (skosimp*) (("" (use "finite_below") (("" (expand* "is_finite" "is_finite_type") (("" (skolem!) (("" (inst + "1 + N!1" "LAMBDA (r: T): IF r = t!1 THEN N!1 ELSE f!1(r) ENDIF") (("1" (expand "injective?") (("1" (skosimp) (("1" (lift-if) (("1" (lift-if) (("1" (ground) (("1" (inst - "x1!1" "x2!1") (("1" (assert) (("1" (lift-if) (("1" (split -1) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (lift-if) (("2" (split -1) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (expand* "below" "irreflexive_kernel" "difference" "member" "well_ordered?" "strict_total_order?" "trichotomous?") (("2" (flatten) (("2" (ground) (("2" (inst -5 "x2!1") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil) ("3" (skosimp) (("3" (expand* "below" "irreflexive_kernel" "difference" "member" "well_ordered?" "strict_total_order?" "trichotomous?") (("3" (flatten) (("3" (inst - "r!1") (("3" (inst - "r!1" "t!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((has_greatest? const-decl "bool" minmax_orders nil) (fullset const-decl "set" sets nil) (reflexive_closure const-decl "(reflexive?)" closure_ops nil) (member const-decl "bool" sets nil) (union const-decl "set" sets nil) (upper_bound? const-decl "bool" bounded_orders nil) (greatest? const-decl "bool" minmax_orders nil) (has_last? const-decl "bool" well_ordered_traversal nil) (finite_below formula-decl nil well_ordered_finite nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (injective? const-decl "bool" functions nil) (TRUE const-decl "bool" booleans nil) (difference const-decl "set" sets nil) (trichotomous? const-decl "bool" orders nil) (irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil) (x2!1 skolem-const-decl "T" well_ordered_finite nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (< const-decl "bool" reals nil) (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) (N!1 skolem-const-decl "nat" well_ordered_finite nil) (below type-eq-decl nil nat_types nil) (f!1 skolem-const-decl "[(below(t!1, <)) -> below[N!1]]" well_ordered_finite nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset nil) (prefix? const-decl "bool" ordered_subset nil) (set type-eq-decl nil sets nil) (order? const-decl "bool" relations_extra nil) (t!1 skolem-const-decl "T" well_ordered_finite nil) (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (is_finite const-decl "bool" finite_sets nil) (is_finite_type const-decl "bool" finite_sets nil) (finite_well_ordered name-judgement "(well_ordered?)" well_ordered_finite nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil well_ordered_finite nil) (pred type-eq-decl nil defined_types nil) (well_ordered? const-decl "bool" orders nil) (strict_total_order? const-decl "bool" orders nil) (< formal-const-decl "(strict_total_order?[T])" well_ordered_finite nil)) shostak))) ¤ Dauer der Verarbeitung: 0.13 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 |
