| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/structures/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 3 kB |
|
SSL permutation_ops.prf Sprache: Lisp |
|||||||||
|
(permutation_ops
(sorted_iff_id_lem 0 (sorted_iff_id_lem-1 nil 3262700911 ("" (induct "m") (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst?) (("2" (replace -4) (("2" (assert) (("2" (skosimp*) (("2" (case-replace "i!1 = jb!1") (("1" (case "pi!1(jb!1) > jb!1") (("1" (inst - "pi!1(jb!1)") (("1" (assert) (("1" (typepred "pi!1") (("1" (expand "bijective?") (("1" (flatten) (("1" (expand "injective?") (("1" (inst - "jb!1" "pi!1(jb!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "pi!1") (("2" (expand "bijective?") (("2" (flatten) (("2" (expand "surjective?") (("2" (inst - "jb!1") (("2" (skosimp*) (("2" (inst -7 "x!1" "jb!1") (("2" (assert) (("2" (case-replace "x!1 = jb!1") (("2" (inst - "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((injective? const-decl "bool" functions nil) (NOT const-decl "[bool -> bool]" booleans nil) (surjective? const-decl "bool" functions nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (below_induction formula-decl nil bounded_nat_inductions 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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" 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) (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" permutation_ops nil) (<= const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (permutation nonempty-type-eq-decl nil permutation nil) (bijective? const-decl "bool" functions nil) (pred type-eq-decl nil defined_types nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) shostak)) (sorted_iff_id 0 (sorted_iff_id-1 nil 3262700349 ("" (skosimp*) (("" (prop) (("1" (decompose-equality) (("1" (expand* "sorted?" "id") (("1" (lemma "sorted_iff_id_lem") (("1" (inst - "x!1" "N" "pi!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (replace -1 :hide? t) (("2" (expand* "sorted?" "id") (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((sorted? const-decl "bool" sort_array nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sorted_iff_id_lem formula-decl nil permutation_ops 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" permutation_ops nil) (below type-eq-decl nil naturalnumbers nil) (id const-decl "(bijective?[T, T])" identity nil) (permutation nonempty-type-eq-decl nil permutation nil) (bijective? const-decl "bool" functions nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak))) ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28