| products/Sources/formale Sprachen/PVS/orders/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: skolemization.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(well_ordering
(ordered_set_order_TCC1 0 (ordered_set_order_TCC1-1 nil 3315836233 ("" (subtype-tcc) nil nil) ((ordered_set type-eq-decl nil well_ordering nil) (well_ordered? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil well_ordering nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil)) nil)) (ordered_set_order_TCC2 0 (ordered_set_order_TCC2-1 nil 3315836233 ("" (subtype-tcc) nil nil) ((ordered_set type-eq-decl nil well_ordering nil) (well_ordered? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil well_ordering nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil)) nil)) (ordered_set_order_TCC3 0 (ordered_set_order_TCC3-1 nil 3315836233 ("" (subtype-tcc) nil nil) ((ordered_set type-eq-decl nil well_ordering nil) (well_ordered? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (difference const-decl "set" sets nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil well_ordering nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil)) nil)) (partial_ordered_set 0 (partial_ordered_set-1 nil 3315836233 ("" (grind :if-match nil) (("1" (grind-with-ext) nil nil) ("2" (inst - "r!1") (("2" (assert) (("2" (inst -9 "t!1") (("1" (inst -9 "r!1") nil nil) ("2" (inst -7 "t!1") (("2" (inst -7 "r!1") (("2" (inst -9 "r!1" "t!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (inst-cp - "r!1") (("3" (inst - "t!1") (("3" (assert) (("3" (inst - "t!1" "r!1") (("3" (inst -8 "t!1" "r!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (inst-cp - "r!1") (("4" (inst - "t!1") (("4" (assert) (("4" (inst - "t!1" "r!1") (("4" (inst -8 "t!1" "r!1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("5" (inst - "x!2") (("5" (inst -4 "x!2") (("5" (assert) nil nil)) nil)) nil)) nil) ((y!1 skolem-const-decl "ordered_set" well_ordering nil) (z!1 skolem-const-decl "ordered_set" well_ordering nil) (x!1 skolem-const-decl "ordered_set" well_ordering nil) (t!1 skolem-const-decl "(difference(z!1`1, x!1`1))" well_ordering 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_ordering nil) (set type-eq-decl nil sets nil) (difference const-decl "set" sets nil) (pred type-eq-decl nil defined_types nil) (well_ordered? const-decl "bool" orders nil) (ordered_set type-eq-decl nil well_ordering nil) (restrict const-decl "R" restrict nil) (partial_order? const-decl "bool" orders nil) (antisymmetric? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (transitive? const-decl "bool" relations nil) (reflexive? const-decl "bool" relations nil) (ordered_set_order const-decl "bool" well_ordering nil) (upper_bound? const-decl "bool" bounded_orders nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil)) nil)) (ordered_set_union_TCC1 0 (ordered_set_union_TCC1-1 nil 3315836233 ("" (skolem-typepred) (("" (expand* "well_ordered?" "strict_total_order?" "strict_order?") (("" (split) (("1" (expand "irreflexive?") (("1" (skosimp* t) (("1" (typepred "ord!1`2") (("1" (expand* "well_ordered?" "strict_total_order?" "strict_order?" "irreflexive?") (("1" (flatten) (("1" (inst - "x!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "transitive?") (("2" (skosimp* t) (("2" (expand* "chain?" "restrict" "total_order?" "dichotomous?") (("2" (flatten) (("2" (inst - "ord!1" "ord!2") (("2" (split) (("1" (expand "ordered_set_order" -1) (("1" (flatten) (("1" (expand* "subset?" "member") (("1" (inst - "x!1") (("1" (assert) (("1" (inst + "ord!2") (("1" (typepred "ord!2`2") (("1" (expand* "well_ordered?" "strict_total_order?" "strict_order?" "transitive?") (("1" (flatten) (("1" (inst - "x!1" "y!1" "z!1") (("1" (inst - "x!1" "y!1") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "ordered_set_order" -1) (("2" (flatten) (("2" (expand* "subset?" "member") (("2" (inst - "z!1") (("2" (assert) (("2" (inst + "ord!1") (("2" (typepred "ord!1`2") (("2" (expand* "well_ordered?" "strict_total_order?" "strict_order?" "transitive?") (("2" (flatten) (("2" (inst - "x!1" "y!1" "z!1") (("2" (inst - "y!1" "z!1") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "trichotomous?") (("3" (skosimp* t) (("3" (expand* "chain?" "restrict" "total_order?" "dichotomous?") (("3" (flatten) (("3" (inst - "S!1" "S!2") (("3" (split) (("1" (expand "ordered_set_order" -1) (("1" (flatten) (("1" (expand* "subset?" "member") (("1" (inst - "x!1") (("1" (assert) (("1" (typepred "S!2`2") (("1" (expand* "well_ordered?" "strict_total_order?" "trichotomous?") (("1" (flatten) (("1" (inst - "x!1" "y!1") (("1" (inst + "S!2") (("1" (inst + "S!2") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "ordered_set_order" -1) (("2" (flatten) (("2" (expand* "subset?" "member") (("2" (inst - "y!1") (("2" (assert) (("2" (typepred "S!1`2") (("2" (expand* "well_ordered?" "strict_total_order?" "trichotomous?") (("2" (flatten) (("2" (inst - "x!1" "y!1") (("2" (inst + "S!1") (("2" (inst + "S!1") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "well_founded?") (("4" (skosimp* t) (("4" (typepred "S!1`2") (("4" (expand* "well_ordered?" "well_founded?") (("4" (flatten) (("4" (inst - "{t: (S!1`1) | p!1(t)}") (("1" (split) (("1" (skolem-typepred) (("1" (inst + "y!2") (("1" (skosimp* t) (("1" (expand* "chain?" "restrict" "total_order?" "dichotomous?") (("1" (flatten) (("1" (inst - "S!1" "ord!1") (("1" (split) (("1" (expand "ordered_set_order" -1) (("1" (flatten) (("1" (inst - "x!1" "y!2") (("1" (assert) (("1" (inst -10 "x!1") nil nil)) nil) ("2" (inst - "x!1") (("1" (expand* "restrict" "upper_bound?") (("1" (inst - "y!2") (("1" (typepred "ord!1`2") (("1" (expand* "well_ordered?" "strict_total_order?" "strict_order?" "irreflexive?" "transitive?") (("1" (flatten) (("1" (inst - "x!1") (("1" (inst - "x!1" "y!2" "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand* "difference" "member") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "ordered_set_order" -1) (("2" (flatten) (("2" (expand* "subset?" "member") (("2" (inst - "x!1") (("2" (assert) (("2" (inst - "x!1" "y!2") (("2" (inst -10 "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "y!1") nil nil)) nil) ("2" (skolem-typepred) (("2" (inst + "S!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((strict_total_order? const-decl "bool" orders nil) (strict_order? const-decl "bool" orders nil) (well_founded? const-decl "bool" orders nil) (p!1 skolem-const-decl "pred[({t | EXISTS (S: (C!1)): S`1(t)})]" well_ordering nil) (x!1 skolem-const-decl "(p!1)" well_ordering nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (upper_bound? const-decl "bool" bounded_orders nil) (ord!1 skolem-const-decl "(C!1)" well_ordering nil) (difference const-decl "set" sets nil) (y!1 skolem-const-decl "({t | EXISTS (S: (C!1)): S`1(t)})" well_ordering nil) (S!1 skolem-const-decl "(C!1)" well_ordering nil) (C!1 skolem-const-decl "chain[ordered_set, ordered_set_order]" well_ordering nil) (trichotomous? const-decl "bool" orders nil) (transitive? const-decl "bool" relations nil) (restrict const-decl "R" restrict nil) (dichotomous? const-decl "bool" orders nil) (total_order? const-decl "bool" orders nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (irreflexive? const-decl "bool" relations nil) (chain nonempty-type-eq-decl nil chain nil) (chain? const-decl "bool" chain nil) (ordered_set_order const-decl "bool" well_ordering nil) (ordered_set type-eq-decl nil well_ordering nil) (well_ordered? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil well_ordering nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (chain_upper_bound 0 (chain_upper_bound-1 nil 3315837585 ("" (skolem-typepred) (("" (expand* "bounded_above?" "upper_bound?") (("" (inst + "ordered_set_union(C!1)") (("" (skolem!) (("" (expand "ordered_set_order") (("" (split) (("1" (expand* "subset?" "member" "ordered_set_union") (("1" (skosimp) (("1" (inst?) nil nil)) nil)) nil) ("2" (skolem!) (("2" (prop) (("1" (expand "ordered_set_union") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (expand* "ordered_set_union" "chain?" "total_order?" "dichotomous?" "restrict") (("2" (skosimp) (("2" (inst - "r!1" "ord!1") (("2" (expand "ordered_set_order") (("2" (prop) (("1" (inst - "t!1" "r!2") (("1" (assert) nil nil)) nil) ("2" (inst - "t!1" "r!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skolem-typepred) (("3" (expand* "restrict" "difference" "member" "upper_bound?") (("3" (skosimp :preds? t) (("3" (expand* "ordered_set_union" "chain?" "total_order?" "dichotomous?" "restrict") (("3" (skosimp*) (("3" (inst - "S!2" "r!1") (("3" (expand* "ordered_set_order" "subset?" "member") (("3" (prop) (("1" (inst - "t!1") (("1" (assert) nil nil)) nil) ("2" (inst - "r!2") (("2" (assert) (("2" (inst - "t!1") (("1" (expand* "restrict" "upper_bound?") (("1" (inst - "r!2") (("1" (inst + "S!2") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand* "difference" "member") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((upper_bound? const-decl "bool" bounded_orders nil) (bounded_above? const-decl "bool" bounded_orders nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (total_order? const-decl "bool" orders 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) (restrict const-decl "R" restrict nil) (dichotomous? const-decl "bool" orders nil) (t!1 skolem-const-decl "(difference(ordered_set_union(C!1)`1, r!1`1))" well_ordering nil) (r!1 skolem-const-decl "(C!1)" well_ordering nil) (S!2 skolem-const-decl "(C!1)" well_ordering nil) (C!1 skolem-const-decl "chain[ordered_set, ordered_set_order]" well_ordering nil) (difference const-decl "set" sets nil) (ordered_set_union const-decl "ordered_set" well_ordering nil) (chain nonempty-type-eq-decl nil chain nil) (chain? const-decl "bool" chain nil) (ordered_set_order const-decl "bool" well_ordering nil) (ordered_set type-eq-decl nil well_ordering nil) (well_ordered? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil well_ordering nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (well_ordering 0 (well_ordering-1 nil 3315837896 ("" (lemma "chain_upper_bound") (("" (forward-chain "zorn") (("" (expand "bounded_above?") (("" (skolem!) (("" (expand* "fullset" "maximal?") (("" (typepred "t!1`2") (("" (case "full?(t!1`1)") (("1" (expand* "full?" "member") (("1" (inst 2 "LAMBDA (t, r: T): IF t!1`1(t) AND t!1`1(r) THEN t!1`2(t, r) ELSE FALSE ENDIF") (("1" (expand* "well_ordered?" "strict_total_order?" "strict_order?") (("1" (prop) (("1" (expand "irreflexive?") (("1" (skolem!) (("1" (prop) (("1" (inst -5 "x!1") nil nil)) nil)) nil)) nil) ("2" (expand "transitive?") (("2" (skosimp) (("2" (prop) (("2" (inst - "x!1" "y!1" "z!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (expand "trichotomous?") (("3" (skosimp) (("3" (inst-cp - "y!1") (("3" (inst - "x!1") (("3" (inst - "x!1" "y!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "well_founded?") (("4" (skosimp*) (("4" (inst - "y!1") (("4" (inst - "{t: (t!1`1) | p!1(t)}") (("4" (split) (("1" (skolem-typepred) (("1" (inst + "y!2") (("1" (skolem-typepred) (("1" (prop) (("1" (inst - "x!1") nil nil)) nil)) nil)) nil)) nil) ("2" (inst + "y!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (expand* "full?" "member") (("2" (skolem!) (("2" (inst + "(add(x!1, t!1`1), LAMBDA (t, r: (add(x!1, t!1`1))): IF t = x!1 THEN FALSE ELSIF (("1" (expand "ordered_set_order") (("1" (prop) (("1" (use "subset_add[T]") nil nil) ("2" (skolem!) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil) ("3" (expand* "restrict" "upper_bound?") (("3" (skosimp* t) (("3" (expand* "add" "difference" "member") (("3" (ground) nil nil)) nil)) nil)) nil) ("4" (replace -1 1) (("4" (beta) (("4" (expand* "add" "member") nil nil)) nil)) nil)) nil)) nil) ("2" (expand* "well_ordered?" "strict_total_order?" "strict_order?") (("2" (prop) (("1" (expand "irreflexive?") (("1" (skolem-typepred) (("1" (expand* "add" "member") (("1" (ground) (("1" (inst - "x!2") nil nil)) nil)) nil)) nil)) nil) ("2" (expand "transitive?") (("2" (skosimp :preds? t) (("2" (expand* "add" "member") (("2" (ground) (("2" (inst - "x!2" "y!1" "z!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "trichotomous?") (("3" (skosimp :preds? t) (("3" (expand* "add" "member") (("3" (ground) (("3" (inst - "x!2" "y!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "well_founded?") (("4" (skosimp* t) (("4" (expand* "add" "member") (("4" (inst - "{t: (t!1`1) | p!1(t)}") (("1" (split) (("1" (split) (("1" (skolem-typepred) (("1" (inst + "y!2") (("1" (skolem-typepred) (("1" (expand* "add" "member") (("1" (ground) (("1" (inst - "x!2") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst 2 "y!1") (("2" (skolem-typepred) (("2" (expand* "add" "member") (("2" (ground) (("2" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (split) (("1" (skolem-typepred) (("1" (inst + "y!2") (("1" (skolem-typepred) (("1" (expand* "add" "member") (("1" (ground) (("1" (inst - "x!2") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "y!1") nil nil)) nil)) nil) ("2" (skolem-typepred) (("2" (expand* "add" "member") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp :preds? t) (("3" (expand* "add" "member") (("3" (ground) nil nil)) nil)) nil) ("4" (skosimp :preds? t) (("4" (expand* "add" "member") (("4" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((zorn formula-decl nil zorn nil) (T formal-type-decl nil well_ordering nil) (set type-eq-decl nil sets nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (pred type-eq-decl nil defined_types nil) (well_ordered? const-decl "bool" orders nil) (ordered_set type-eq-decl nil well_ordering nil) (ordered_set_order const-decl "bool" well_ordering nil) (NOT const-decl "[bool -> bool]" booleans nil) (p!1 skolem-const-decl "pred[(add(x!1, t!1`1))]" well_ordering nil) (y!1 skolem-const-decl "(add(x!1, t!1`1))" well_ordering nil) (upper_bound? const-decl "bool" bounded_orders nil) (restrict const-decl "R" restrict nil) (difference const-decl "set" sets nil) (subset_add formula-decl nil sets_lemmas nil) (TRUE const-decl "bool" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (x!1 skolem-const-decl "T" well_ordering nil) (add const-decl "(nonempty?)" sets nil) (nonempty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (strict_total_order? const-decl "bool" orders nil) (strict_order? const-decl "bool" orders nil) (well_founded? const-decl "bool" orders nil) (y!1 skolem-const-decl "T" well_ordering nil) (trichotomous? const-decl "bool" orders nil) (t!1 skolem-const-decl "ordered_set" well_ordering nil) (x!1 skolem-const-decl "T" well_ordering nil) (y!1 skolem-const-decl "T" well_ordering nil) (transitive? const-decl "bool" relations nil) (irreflexive? const-decl "bool" relations nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (FALSE const-decl "bool" booleans nil) (full? const-decl "bool" sets nil) (fullset const-decl "set" sets nil) (maximal? const-decl "bool" minmax_orders nil) (bounded_above? const-decl "bool" bounded_orders nil) (chain_upper_bound formula-decl nil well_ordering nil)) shostak))) ¤ Dauer der Verarbeitung: 0.56 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 |
