| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/Sturm/pvsbin/ (Beweissystem der NASA Version 6.0.9©) Datei vom 8.10.2014 mit Größe 469 kB |
|
SSL bags.prf Sprache: unbekannt |
|
|
(bags
(delete_TCC1 0 (delete_TCC1-1 nil 3286291749 ("" (ground) (("" (skolem!) (("" (apply (then (ground) (assert))) nil nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (emptybag_is_empty? 0 (emptybag_is_empty?-1 nil 3286291749 ("" (skosimp*) (("" (split) (("1" (flatten) (("1" (expand "empty?") (("1" (expand "emptybag") (("1" (apply-extensionality 1) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replace -1) (("2" (expand "empty?") (("2" (expand "emptybag") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((empty? const-decl "bool" bags nil) (bag type-eq-decl nil bags nil) (T formal-type-decl nil bags 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) (emptybag const-decl "bag" bags nil)) nil)) (delete_purge 0 (delete_purge-1 nil 3286291749 ("" (skosimp*) (("" (expand "delete") (("" (expand "purge") (("" (apply-extensionality 1) (("" (hide 2) (("" (lift-if) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((delete const-decl "bag" bags nil) (T formal-type-decl nil bags 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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (bag type-eq-decl nil bags nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (numfield nonempty-type-eq-decl nil number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (purge const-decl "bag" bags nil)) nil)) (insert_unique 0 (insert_unique-1 nil 3286291749 ("" (skosimp*) (("" (expand "insert") (("" (apply-extensionality 1) (("" (case "(LAMBDA (t: T): IF x!1 = t THEN 1 + a!1(t) ELSE a!1(t) ENDIF)(x!2) = (LAMBDA (t: T): IF x!1 = t THEN 1 + b!1(t) ELSE b!1(t) ENDIF)(x!2)") (("1" (hide -2) (("1" (beta -1) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((insert const-decl "bag" bags nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (bag type-eq-decl nil bags 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) (T formal-type-decl nil bags nil)) nil)) (insert_exchange 0 (insert_exchange-1 nil 3286291749 ("" (skosimp*) (("" (expand "insert") (("" (apply-extensionality :hide? t) (("" (lift-if) (("" (ground) nil nil)) nil)) nil)) nil)) nil) ((insert const-decl "bag" bags nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (bag type-eq-decl nil bags 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) (T formal-type-decl nil bags nil)) nil)) (delete_insert_TCC1 0 (delete_insert_TCC1-1 nil 3286291749 ("" (subtype-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) (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (delete_insert 0 (delete_insert-1 nil 3286291749 ("" (skosimp*) (("" (expand "insert") (("" (expand "delete") (("" (apply-extensionality 1 :hide? t) (("" (case "x!1 = x!2") (("1" (lift-if) (("1" (assert) nil nil)) nil) ("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((insert const-decl "bag" bags nil) (T formal-type-decl nil bags 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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (bag type-eq-decl nil bags nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (delete const-decl "bag" bags nil)) nil)) (insert_delete 0 (insert_delete-1 nil 3286291749 ("" (skosimp*) (("" (apply-extensionality 1) (("" (expand "insert") (("" (expand "delete") (("" (propax) nil nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil bags 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) (delete const-decl "bag" bags nil) (insert const-decl "bag" bags nil) (bag type-eq-decl nil bags nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (delete_insert_diff 0 (delete_insert_diff-1 nil 3286291749 ("" (skosimp*) (("" (expand "delete") (("" (expand "insert") (("" (apply-extensionality 2 :hide? t) (("" (lift-if) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((delete const-decl "bag" bags nil) (T formal-type-decl nil bags 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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (bag type-eq-decl nil bags nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (insert const-decl "bag" bags nil)) nil)) (decomposition 0 (decomposition-1 nil 3286291749 ("" (skosimp*) (("" (expand "empty?") (("" (skosimp*) (("" (inst 2 "(LAMBDA t: IF t = x!1 THEN b!1(t) - 1 ELSE b!1(t) ENDIF)" "x!1") (("1" (expand "insert") (("1" (apply-extensionality 2) nil nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((empty? const-decl "bool" bags nil) (int_minus_int_is_int application-judgement "int" integers nil) (b!1 skolem-const-decl "bag" bags nil) (bag type-eq-decl nil bags nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (x!1 skolem-const-decl "T" bags nil) (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil bags nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (insert const-decl "bag" bags nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (bag_equality 0 (bag_equality-1 nil 3286291749 ("" (skosimp*) (("" (split 1) (("1" (flatten) (("1" (expand "eqmult") (("1" (skosimp*) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "eqmult") (("2" (apply-extensionality 1) nil nil)) nil)) nil)) nil)) nil) ((eqmult const-decl "bool" bags 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) (T formal-type-decl nil bags nil) (bag type-eq-decl nil bags nil)) nil)) (subbag_empty 0 (subbag_empty-1 nil 3286291749 ("" (skosimp*) (("" (expand "subbag?") (("" (expand "emptybag") (("" (skosimp*) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((subbag? const-decl "bool" bags nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (emptybag const-decl "bag" bags nil)) nil)) (subbag_equality 0 (subbag_equality-1 nil 3286291749 ("" (skosimp*) (("" (expand "subbag?") (("" (split 1) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (apply-extensionality 1) (("2" (hide 2) (("2" (inst?) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((subbag? const-decl "bool" bags nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (bag type-eq-decl nil bags 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) (T formal-type-decl nil bags nil)) nil)) (subbag_trans 0 (subbag_trans-1 nil 3288965621 ("" (grind) nil nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (T formal-type-decl nil bags nil) (subbag? const-decl "bool" bags nil)) shostak)) (bag_plus_union 0 (bag_plus_union-1 nil 3286291749 ("" (skosimp*) (("" (apply-extensionality 1 :hide? t) (("" (expand "union") (("" (expand "plus") (("" (expand "intersection") (("" (expand "max") (("" (expand "min") (("" (lift-if) (("" (lift-if) (("" (ground) (("" (lift-if) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil bags 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) (intersection const-decl "bag" bags nil) (union const-decl "bag" bags nil) (plus const-decl "bag" bags nil) (bag type-eq-decl nil bags nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)) nil)) (bag_plus_comm 0 (bag_plus_comm-1 nil 3286291749 ("" (skosimp*) (("" (expand "plus") (("" (propax) nil nil)) nil)) nil) ((plus const-decl "bag" bags nil)) nil)) (plus_emptybag 0 (plus_emptybag-1 nil 3286291749 ("" (skosimp*) (("" (expand "plus") (("" (expand "emptybag") (("" (apply-eta "a!1") nil nil)) nil)) nil)) nil) ((plus const-decl "bag" bags nil) (= const-decl "[T, T -> boolean]" equalities nil) (bag type-eq-decl nil bags 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) (T formal-type-decl nil bags nil) (emptybag const-decl "bag" bags nil)) nil)) (bag_plus_insert 0 (bag_plus_insert-1 nil 3286291749 ("" (skosimp*) (("" (apply-extensionality 1 :hide? t) (("" (expand "plus") (("" (expand "insert") (("" (lift-if) (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil bags 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) (insert const-decl "bag" bags nil) (plus const-decl "bag" bags nil) (bag type-eq-decl nil bags nil)) nil)) (bag_distributive 0 (bag_distributive-1 nil 3286291749 ("" (skosimp*) (("" (expand "union") (("" (expand "intersection") (("" (apply-extensionality 1) (("1" (hide 2) (("1" (grind) nil nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((union const-decl "bag" bags nil) (T formal-type-decl nil bags 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) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (bag type-eq-decl nil bags nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (a!1 skolem-const-decl "bag" bags nil) (b!1 skolem-const-decl "bag" bags nil) (c!1 skolem-const-decl "bag" bags nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (intersection const-decl "bag" bags nil)) nil)) (extract_subbag 0 (extract_subbag-1 nil 3286291771 ("" (skosimp*) (("" (expand "subbag?") (("" (skosimp*) (("" (expand "extract") (("" (lift-if) (("" (split) (("1" (flatten) (("1" (assert) nil))) ("2" (flatten) (("2" (assert) nil)))))))))))))) nil) ((subbag? const-decl "bool" bags nil) (extract const-decl "bag" bags nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (extract_disj 0 (extract_disj-1 nil 3286292091 ("" (skosimp*) (("" (grind) nil)) nil) ((disjoint? const-decl "bool" bags nil) (empty? const-decl "bool" bags nil) (intersection const-decl "bag" bags nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (extract const-decl "bag" bags nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (bag_disj_comm 0 (bag_disj_comm-1 nil 3286292236 ("" (grind) nil nil) ((T formal-type-decl nil bags nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (intersection const-decl "bag" bags nil) (empty? const-decl "bool" bags nil) (disjoint? const-decl "bool" bags nil)) nil)) (bag_union_comm 0 (bag_union_comm-1 nil 3286292266 ("" (skosimp*) (("" (decompose-equality +) (("" (expand "union") (("" (expand "max") (("" (lift-if) (("" (split) (("1" (flatten) (("1" (lift-if) (("1" (split) (("1" (flatten) (("1" (assert) nil))) ("2" (propax) nil))))))) ("2" (flatten) (("2" (lift-if) (("2" (split) (("1" (propax) nil) ("2" (flatten) (("2" (assert) nil)))))))))))))))))))) nil) ((bag type-eq-decl nil bags nil) (union const-decl "bag" bags 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) (T formal-type-decl nil bags nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (bag_union_fix_pt 0 (bag_union_fix_pt-1 nil 3286292546 ("" (skosimp*) (("" (decompose-equality +) (("" (expand "union") (("" (expand "max") (("" (propax) nil)))))))) nil) ((bag type-eq-decl nil bags nil) (union const-decl "bag" bags 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) (T formal-type-decl nil bags nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)) nil)) (bag_purge_extract 0 (bag_purge_extract-1 nil 3286292562 ("" (skosimp*) (("" (decompose-equality +) (("" (expand "union") (("" (expand "max") (("" (expand "purge") (("" (lift-if) (("" (lift-if) (("" (expand "extract") (("" (lift-if) (("" (split) (("1" (prop) (("1" (assert) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bag type-eq-decl nil bags nil) (union const-decl "bag" bags nil) (purge const-decl "bag" bags nil) (extract const-decl "bag" bags 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) (T formal-type-decl nil bags nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)) nil)) (bag_disj_extract_perge 0 (bag_disj_extract_perge-1 nil 3286292587 ("" (grind) nil nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (extract const-decl "bag" bags nil) (purge const-decl "bag" bags nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (intersection const-decl "bag" bags nil) (empty? const-decl "bool" bags nil) (disjoint? const-decl "bool" bags nil)) nil)) (bag_extract_union_subbag 0 (bag_extract_union_subbag-1 nil 3286292609 ("" (skosimp*) (("" (lemma "extract_disj") (("" (inst - "a!1" "x!1" "y!1") (("" (assert) (("" (expand "subbag?") (("" (skosimp*) (("" (expand "union") (("" (expand "max") (("" (lift-if) (("" (expand "disjoint?") (("" (expand "intersection") (("" (expand "empty?") (("" (inst?) (("" (expand "min") (("" (lift-if) (("" (grind) nil)))))))))))))))))))))))))))))) nil) ((extract_disj formula-decl nil bags nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (disjoint? const-decl "bool" bags nil) (empty? const-decl "bool" bags nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (extract const-decl "bag" bags nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (intersection const-decl "bag" bags nil) (union const-decl "bag" bags nil) (subbag? const-decl "bool" bags nil) (bag type-eq-decl nil bags 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) (T formal-type-decl nil bags nil)) nil)) (union_upper_bound 0 (union_upper_bound-1 nil 3287522217 ("" (grind) nil nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (T formal-type-decl nil bags nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (subbag? const-decl "bool" bags nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (union const-decl "bag" bags nil)) shostak))) [ 0.43Quellennavigators Projekt ] |
2026-03-28