| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/orders/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 9 kB |
|
Quelle relations_extra.prf Sprache: Lisp |
|||||||||
|
(relations_extra
(strict_order_is_asymmetric 0 (strict_order_is_asymmetric-1 nil 3314539726 ("" (grind :if-match nil) (("" (inst - "x!2" "y!1" "x!2") (("" (assert) (("" (inst?) nil nil)) nil)) nil)) nil) ((irreflexive? const-decl "bool" relations nil) (transitive? const-decl "bool" relations 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 relations_extra nil) (pred type-eq-decl nil defined_types nil) (strict_order? const-decl "bool" orders nil) (asymmetric? const-decl "bool" relations_extra nil)) nil)) (asymmetric_is_antisymmetric 0 (asymmetric_is_antisymmetric-1 nil 3314539726 ("" (judgement-tcc) nil 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 relations_extra nil) (pred type-eq-decl nil defined_types nil) (asymmetric? const-decl "bool" relations_extra nil) (antisymmetric? const-decl "bool" relations nil)) nil)) (asymmetric_is_irreflexive 0 (asymmetric_is_irreflexive-1 nil 3314539726 ("" (judgement-tcc) nil 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 relations_extra nil) (pred type-eq-decl nil defined_types nil) (asymmetric? const-decl "bool" relations_extra nil) (irreflexive? const-decl "bool" relations nil)) nil)) (dichotomous_is_trichotomous 0 (dichotomous_is_trichotomous-1 nil 3314539726 ("" (judgement-tcc) nil 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 relations_extra nil) (pred type-eq-decl nil defined_types nil) (dichotomous? const-decl "bool" orders nil) (trichotomous? const-decl "bool" orders nil)) nil)) (order_is_transitive 0 (order_is_transitive-1 nil 3318180445 ("" (skolem-typepred) (("" (expand "order?") (("" (flatten) nil nil)) nil)) nil) ((order? const-decl "bool" relations_extra nil) (pred type-eq-decl nil defined_types nil) (T formal-type-decl nil relations_extra nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (order_is_antisymmetric 0 (order_is_antisymmetric-1 nil 3318180445 ("" (judgement-tcc) nil 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 relations_extra nil) (pred type-eq-decl nil defined_types nil) (order? const-decl "bool" relations_extra nil) (transitive? const-decl "bool" relations nil) (antisymmetric? const-decl "bool" relations nil)) nil)) (partial_order_is_order 0 (partial_order_is_order-1 nil 3318180445 ("" (judgement-tcc) nil 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 relations_extra nil) (pred type-eq-decl nil defined_types nil) (partial_order? const-decl "bool" orders nil) (preorder? const-decl "bool" orders nil) (reflexive? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (antisymmetric? const-decl "bool" relations nil) (order? const-decl "bool" relations_extra nil)) nil)) (strict_order_is_order 0 (strict_order_is_order-1 nil 3318180445 ("" (grind :if-match nil) (("" (inst - "x!2") (("" (inst - "x!2" "y!1" "x!2") (("" (assert) nil nil)) nil)) nil)) nil) ((irreflexive? const-decl "bool" relations 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 relations_extra nil) (pred type-eq-decl nil defined_types nil) (strict_order? const-decl "bool" orders nil) (order? const-decl "bool" relations_extra nil) (antisymmetric? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil)) nil)) (total_order_is_linear 0 (total_order_is_linear-1 nil 3318180445 ("" (grind :if-match all) nil 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 relations_extra nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (dichotomous? const-decl "bool" orders nil) (partial_order? const-decl "bool" orders nil) (preorder? const-decl "bool" orders nil) (reflexive? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (antisymmetric? const-decl "bool" relations nil) (order? const-decl "bool" relations_extra nil) (trichotomous? const-decl "bool" orders nil) (linear_order? const-decl "bool" relations_extra nil)) nil)) (strict_total_order_is_linear 0 (strict_total_order_is_linear-1 nil 3318180445 ("" (grind :if-match all) nil 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 relations_extra nil) (pred type-eq-decl nil defined_types nil) (strict_total_order? const-decl "bool" orders nil) (strict_order? const-decl "bool" orders nil) (irreflexive? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (antisymmetric? const-decl "bool" relations nil) (order? const-decl "bool" relations_extra nil) (trichotomous? const-decl "bool" orders nil) (linear_order? const-decl "bool" relations_extra nil)) nil)) (reflexive 0 (reflexive-1 nil 3318876242 ("" (skolem-typepred) (("" (expand "reflexive?") (("" (propax) nil nil)) nil)) nil) ((reflexive? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (T formal-type-decl nil relations_extra nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (irreflexive 0 (irreflexive-1 nil 3318876269 ("" (skolem-typepred) (("" (expand "irreflexive?") (("" (propax) nil nil)) nil)) nil) ((irreflexive? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (T formal-type-decl nil relations_extra nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (symmetric 0 (symmetric-1 nil 3318876272 ("" (skolem-typepred) (("" (expand "symmetric?") (("" (propax) nil nil)) nil)) nil) ((symmetric? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (T formal-type-decl nil relations_extra nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (antisymmetric 0 (antisymmetric-1 nil 3318876279 ("" (skolem-typepred) (("" (expand "antisymmetric?") (("" (propax) nil nil)) nil)) nil) ((antisymmetric? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (T formal-type-decl nil relations_extra nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (asymmetric 0 (asymmetric-1 nil 3318876283 ("" (skolem-typepred) (("" (expand "asymmetric?") (("" (propax) nil nil)) nil)) nil) ((asymmetric? const-decl "bool" relations_extra nil) (pred type-eq-decl nil defined_types nil) (T formal-type-decl nil relations_extra nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (transitive 0 (transitive-1 nil 3318876286 ("" (skolem-typepred) (("" (expand "transitive?") (("" (propax) nil nil)) nil)) nil) ((transitive? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (T formal-type-decl nil relations_extra nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (dichotomous 0 (dichotomous-1 nil 3318876303 ("" (skolem-typepred) (("" (expand "dichotomous?") (("" (propax) nil nil)) nil)) nil) ((dichotomous? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (T formal-type-decl nil relations_extra nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (trichotomous 0 (trichotomous-1 nil 3318876327 ("" (skolem-typepred) (("" (expand "trichotomous?") (("" (propax) nil nil)) nil)) nil) ((trichotomous? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (T formal-type-decl nil relations_extra 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_founded 0 (well_founded-1 nil 3318876333 ("" (skolem-typepred) (("" (expand "well_founded?") (("" (propax) nil nil)) nil)) nil) ((well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (T formal-type-decl nil relations_extra nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak))) ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28