| products/sources/formale sprachen/PVS/sets_aux/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: set_of_functions.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(nat_indexed_sets
(IUnion_0_def 0 (IUnion_0_def-1 nil 3450516457 ("" (skosimp) (("" (apply-extensionality :hide? t) (("" (expand "IUnion") (("" (expand "image") (("" (expand "Union") (("" (case-replace "A!1(0)(x!1)") (("1" (inst + "A!1(0)") (("1" (inst + "0") nil nil)) nil) ("2" (assert) (("2" (skosimp) (("2" (typepred "a!1") (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil nat_indexed_sets nil) (boolean nonempty-type-decl nil booleans nil) (IUnion const-decl "set[T]" nat_indexed_sets nil) (sequence type-eq-decl nil sequences nil) (set type-eq-decl nil sets 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) (number nonempty-type-decl nil numbers nil) (image const-decl "set[R]" function_image nil) (TRUE const-decl "bool" booleans nil) (<= const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (NOT const-decl "[bool -> bool]" booleans nil) (Union const-decl "set" sets nil)) shostak)) (IUnion_n_def 0 (IUnion_n_def-1 nil 3450516511 ("" (skosimp) (("" (apply-extensionality :hide? t) (("" (expand "union") (("" (expand "member") (("" (case-replace "A!1(1 + n!1)(x!1)") (("1" (expand "IUnion") (("1" (expand "image") (("1" (expand "Union") (("1" (inst + "A!1(1 + n!1)") (("1" (inst + "1+n!1") nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "IUnion") (("2" (expand "image") (("2" (expand "Union") (("2" (case-replace "EXISTS (a: ({y: set[T] | EXISTS (x: ({i | i <= n!1})): y = A!1(x)})): a(x!1)") (("1" (skosimp) (("1" (typepred "a!1") (("1" (skosimp) (("1" (inst + "a!1") (("1" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil) ("2" (replace 1 3) (("2" (assert) (("2" (skosimp) (("2" (typepred "a!1") (("2" (skosimp) (("2" (typepred "x!2") (("2" (inst + "A!1(x!2)") (("1" (assert) nil nil) ("2" (inst + "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil nat_indexed_sets nil) (boolean nonempty-type-decl nil booleans nil) (union const-decl "set" sets nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (IUnion const-decl "set[T]" nat_indexed_sets nil) (sequence type-eq-decl nil sequences nil) (set type-eq-decl nil sets 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) (number nonempty-type-decl nil numbers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (member const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (a!1 skolem-const-decl "({y: set[T] | EXISTS (x: ({i | i <= n!1})): y = A!1(x)})" nat_indexed_sets nil) (x!2 skolem-const-decl "({i | i <= 1 + n!1})" nat_indexed_sets nil) (Union const-decl "set" sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (A!1 skolem-const-decl "sequence[set[T]]" nat_indexed_sets nil) (n!1 skolem-const-decl "nat" nat_indexed_sets nil) (<= const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (image const-decl "set[R]" function_image nil)) shostak)) (increasing_indexed_TCC1 0 (increasing_indexed_TCC1-1 nil 3450160073 ("" (expand "increasing_indexed?") (("" (split) (("1" (apply-extensionality :hide? t) (("1" (grind) nil nil)) nil) ("2" (grind) nil nil)) nil)) 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) (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) (set type-eq-decl nil sets nil) (IUnion const-decl "set[T]" indexed_sets nil) (fullset const-decl "set" sets nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil nat_indexed_sets nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (increasing? const-decl "bool" fun_preds_partial "structures/") (increasing_indexed? const-decl "bool" nat_indexed_sets nil)) nil)) (increasing_IUnion 0 (increasing_IUnion-1 nil 3449816575 ("" (skosimp) (("" (name "BB" "lambda n: IUnion(lambda (i:nat): if i <= n then A!1(i) else emptyset[T] endif)") (("" (inst + "BB") (("" (split) (("1" (hide -1) (("1" (expand "increasing?") (("1" (expand "subset?") (("1" (expand "member") (("1" (skolem + ("i!1" "j!1")) (("1" (flatten) (("1" (skosimp) (("1" (expand "BB") (("1" (expand "IUnion") (("1" (skosimp) (("1" (expand "emptyset") (("1" (prop) (("1" (inst + "i!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (expand "BB") (("2" (apply-extensionality :hide? t) (("2" (expand "IUnion") (("2" (case-replace "A!1(0)(x!1)") (("1" (inst + "0") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (skosimp) (("2" (expand "emptyset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp) (("3" (apply-extensionality :hide? t) (("3" (expand "union") (("3" (expand "member") (("3" (case-replace "BB(1 + n!1)(x!1)") (("1" (flatten) (("1" (expand "BB") (("1" (expand "IUnion") (("1" (expand "emptyset") (("1" (skosimp) (("1" (prop) (("1" (expand "<=" -1) (("1" (split -1) (("1" (inst + "i!1") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (split -1) (("1" (expand "BB") (("1" (expand "IUnion") (("1" (expand "emptyset") (("1" (skosimp) (("1" (inst + "i!1") (("1" (assert) (("1" (prop) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "BB") (("2" (expand "IUnion") (("2" (expand "emptyset") (("2" (inst + "1+n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide -1) (("4" (apply-extensionality :hide? t) (("4" (expand "IUnion") (("4" (case-replace "EXISTS (i: nat): A!1(i)(x!1)") (("1" (skosimp) (("1" (inst + "i!1") (("1" (expand "BB") (("1" (expand "IUnion") (("1" (inst + "i!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (skosimp) (("2" (expand "BB") (("2" (expand "IUnion") (("2" (skosimp) (("2" (expand "emptyset") (("2" (prop) (("2" (inst + "i!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((emptyset const-decl "set" sets nil) (sequence type-eq-decl nil sequences nil) (<= const-decl "bool" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (IUnion const-decl "set[T]" indexed_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil nat_indexed_sets 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) (increasing? const-decl "bool" fun_preds_partial "structures/") (member const-decl "bool" sets nil) (BB skolem-const-decl "[nat -> set[T]]" nat_indexed_sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (subset? const-decl "bool" sets nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (union const-decl "set" sets nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil)) shostak)) (decreasing_IIntersection 0 (decreasing_IIntersection-1 nil 3449817484 ("" (skosimp) (("" (name "BB" "lambda n: IIntersection(lambda (i:nat): if i <= n then A!1(i) else fullset[T] endif)") (("" (hide -1) (("" (inst + "BB") (("" (split) (("1" (expand "decreasing?") (("1" (skolem + ("i!1" "j!1")) (("1" (flatten) (("1" (expand "subset?") (("1" (expand "member") (("1" (skosimp) (("1" (expand "BB") (("1" (expand "IIntersection") (("1" (skosimp) (("1" (expand "fullset") (("1" (prop) (("1" (inst - "i!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "BB") (("2" (apply-extensionality :hide? t) (("2" (case-replace " A!1(0)(x!1)") (("1" (expand "IIntersection") (("1" (skosimp) (("1" (expand "fullset") (("1" (prop) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "IIntersection") (("2" (inst - "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (apply-extensionality :hide? t) (("3" (expand "intersection") (("3" (expand "member") (("3" (case-replace "BB(1 + n!1)(x!1)") (("1" (expand "BB") (("1" (expand "IIntersection") (("1" (expand "fullset") (("1" (inst-cp - "1+n!1") (("1" (assert) (("1" (skosimp) (("1" (prop) (("1" (inst - "i!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (expand "BB") (("2" (expand "IIntersection") (("2" (expand "fullset") (("2" (skosimp) (("2" (prop) (("2" (expand "<=" -1) (("2" (split) (("1" (inst - "i!1") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (apply-extensionality :hide? t) (("4" (expand "IIntersection") (("4" (case-replace "FORALL (i: nat): A!1(i)(x!1)") (("1" (skosimp) (("1" (expand "BB") (("1" (expand "IIntersection") (("1" (skosimp) (("1" (expand "fullset") (("1" (prop) (("1" (inst - "i!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (skosimp) (("2" (expand "BB") (("2" (expand "IIntersection") (("2" (expand "fullset") (("2" (inst - "i!1") (("2" (inst - "i!1") (("2" (prop) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((fullset const-decl "set" sets nil) (sequence type-eq-decl nil sequences nil) (<= const-decl "bool" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (IIntersection const-decl "set[T]" indexed_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil nat_indexed_sets 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) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (intersection const-decl "set" sets nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (decreasing? const-decl "bool" fun_preds_partial "structures/") (member const-decl "bool" sets nil) (BB skolem-const-decl "[nat -> set[T]]" nat_indexed_sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (subset? const-decl "bool" sets nil)) shostak)) (disjoint_IUnion 0 (disjoint_IUnion-1 nil 3450506639 ("" (skosimp) (("" (lemma "increasing_IUnion" ("A" "A!1")) (("" (skosimp) (("" (inst + "lambda (j:nat): if j=0 then A!1(0) else difference(B!1(j),B!1(j-1)) endif") (("1" (case-replace "disjoint?(LAMBDA (j: nat): IF j = 0 THEN A!1(0) ELSE difference(B!1(j), B!1(j - 1)) ENDIF)") (("1" (case "FORALL n: IUnion(n, LAMBDA (j: nat): IF j = 0 THEN A!1(0) ELSE difference(B!1(j), B!1(j - 1)) ENDIF) = B!1(n)") (("1" (name-replace "CC" "LAMBDA (j: nat): IF j = 0 THEN A!1(0) ELSE difference(B!1(j), B!1(j - 1)) ENDIF") (("1" (split) (("1" (induct "n") (("1" (inst - "0") (("1" (rewrite "IUnion_0_def") (("1" (rewrite "IUnion_0_def") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (rewrite "IUnion_n_def" 1) (("2" (replace -1) (("2" (rewrite "IUnion_n_def" 1) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "union" 1) (("2" (expand "member") (("2" (case-replace "IUnion(j!1, A!1)(x!1)") (("2" (replace 1) (("2" (expand "CC") (("2" (expand "difference") (("2" (expand "member") (("2" (case-replace "B!1(j!1)(x!1)") (("1" (assert) (("1" (inst -4 "j!1") (("1" (replace -4 -1 rl) (("1" (expand "IUnion" -1) (("1" (expand "image") (("1" (expand "Union") (("1" (skosimp) (("1" (typepred "a!1") (("1" (skosimp) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst -6 "j!1") (("2" (replace -6 3) (("2" (assert) (("2" (expand "union") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "forall n: IUnion(n,A!1)=B!1(n)") (("1" (skosimp) (("1" (assert) (("1" (inst - "n!1") (("1" (replace -1) (("1" (inst -6 "n!1") (("1" (replace -6) (("1" (hide-all-but 1) (("1" (apply-extensionality :hide? t) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (rewrite "IUnion_0_def") (("1" (assert) nil nil)) nil) ("2" (skosimp) (("2" (rewrite "IUnion_n_def") (("2" (replace -1) (("2" (inst -6 "j!1") (("2" (replace -6) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (apply-extensionality :hide? t) (("3" (replace -6) (("3" (hide -4 -5 -6) (("3" (case-replace "IUnion(B!1)(x!1)") (("1" (expand "IUnion") (("1" (skosimp) (("1" (inst -2 "i!1") (("1" (replace -2 -1 rl) (("1" (hide -2) (("1" (expand "image") (("1" (expand "Union") (("1" (skosimp) (("1" (typepred "a!1") (("1" (skosimp) (("1" (inst + "x!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "IUnion") (("2" (skosimp) (("2" (inst - "i!1") (("2" (inst + "i!1") (("2" (replace -2 1 rl) (("2" (expand "image") (("2" (expand "Union") (("2" (inst + "CC(i!1)") (("2" (inst + "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (rewrite "IUnion_0_def") (("1" (assert) nil nil)) nil) ("2" (skosimp) (("2" (rewrite "IUnion_n_def") (("2" (apply-extensionality :hide? t) (("1" (expand "union") (("1" (expand "member") (("1" (replace -1) (("1" (expand "difference") (("1" (expand "member") (("1" (case-replace "B!1(j!1)(x!1)") (("1" (expand "increasing?") (("1" (inst -4 "j!1" "j!1+1") (("1" (assert) (("1" (expand "subset?") (("1" (inst -4 "x!1") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "disjoint?") (("2" (skosimp) (("2" (replace -2 2 :dir rl) (("2" (hide-all-but (-1 1 2)) (("2" (expand "disjoint?") (("2" (expand "difference") (("2" (expand "intersection") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp) (("2" (case-replace "i!1=0") (("1" (assert) (("1" (flatten) (("1" (expand "increasing?") (("1" (inst - "0" "j!1-1") (("1" (assert) (("1" (expand "subset?") (("1" (inst - "x!1") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (assert) (("2" (case-replace "j!1=0") (("1" (expand "increasing?") (("1" (inst - "0" "i!1-1") (("1" (assert) (("1" (expand "subset?") (("1" (inst - "x!1") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (expand "increasing?") (("2" (expand "subset?") (("2" (expand "member") (("2" (lemma "trich_lt" ("x" "i!1" "y" "j!1")) (("2" (split) (("1" (inst - "i!1" "j!1-1") (("1" (assert) (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (inst - "j!1" "i!1-1") (("3" (assert) (("3" (inst - "x!1") (("3" (assert) 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)) nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((sequence type-eq-decl nil sequences nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil nat_indexed_sets 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) (increasing_IUnion formula-decl nil nat_indexed_sets nil) (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (difference const-decl "set" sets nil) (empty? const-decl "bool" sets nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (trich_lt formula-decl nil real_props nil) (intersection const-decl "set" sets nil) (disjoint? const-decl "bool" sets nil) (IUnion const-decl "set[T]" nat_indexed_sets nil) (union const-decl "set" sets nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (member const-decl "bool" sets nil) (Union const-decl "set" sets nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (image const-decl "set[R]" function_image nil) (CC skolem-const-decl "[nat -> set[T]]" nat_indexed_sets nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (IUnion_n_def formula-decl nil nat_indexed_sets nil) (IUnion_0_def formula-decl nil nat_indexed_sets nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (i!1 skolem-const-decl "nat" nat_indexed_sets nil) (IUnion const-decl "set[T]" indexed_sets nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (increasing? const-decl "bool" fun_preds_partial "structures/") (subset? const-decl "bool" sets nil) (disjoint? const-decl "bool" indexed_sets_aux nil)) shostak))) ¤ Dauer der Verarbeitung: 0.114 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 |
