| products/Sources/formale Sprachen/PVS/reals/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: product_fseq.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(product_fseq
(product_TCC1 0 (product_TCC1-1 nil 3407849048 ("" (subtype-tcc) 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)) (len0 0 (len0-1 nil 3407849052 ("" (grind) nil nil) ((product const-decl "real" product_fseq nil) (int_minus_int_is_int application-judgement "int" integers nil)) shostak)) (product_fseq_shift_TCC1 0 (product_fseq_shift_TCC1-1 nil 3410606942 ("" (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_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil)) nil)) (product_fseq_shift_TCC2 0 (product_fseq_shift_TCC2-1 nil 3410606942 ("" (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_lt_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)) (product_fseq_shift_TCC3 0 (product_fseq_shift_TCC3-1 nil 3410606942 ("" (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_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (product_fseq_shift 0 (product_fseq_shift-3 nil 3411837933 ("" (skeep) (("" (lemma "product_shift") (("" (inst - "fs`seq" "l2 - 1" "0" "l1") (("" (assert) (("" (hide -1) (("" (lemma "product_shift_i") (("" (inst - "_" "l1 - 1 + l2" "_" "l1") (("" (inst - "fs`seq" "-l1") (("" (assert) (("" (replace -1) (("" (hide -1) (("" (real-props :simple? t) (("" (rewrite "product_restrict_eq[nat]") (("1" (hide 2) (("1" (expand "restrict") (("1" (propax) nil nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((product_shift formula-decl nil product_nat 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) (int_plus_int_is_int application-judgement "int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (product_shift_i formula-decl nil product_nat nil) (minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield -> numfield]" number_fields nil) (add_neg formula-decl nil extra_tegies nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (restrict const-decl "[T -> real]" product nil) (product_restrict_eq formula-decl nil product nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (< const-decl "bool" reals nil) (fsq type-eq-decl nil fsq "structures/") (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil product nil) (T_low type-eq-decl nil product nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (T formal-nonempty-subtype-decl nil product_fseq nil) (T_pred const-decl "[real -> boolean]" product_fseq 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)) nil) (product_fseq_shift-2 nil 3411837653 (";;; Proof product_fseq_shift-1 for formula product_fseq.product_fseq_shift" (skeep) ((";;; Proof product_fseq_shift-1 for formula product_fseq.product_fseq_shift" (lemma "product_shift" [nat]) ((";;; Proof product_fseq_shift-1 for formula product_fseq.product_fseq_shift" (inst - "fs`seq" "l2 - 1" "0" "l1") ((";;; Proof product_fseq_shift-1 for formula product_fseq.product_fseq_shift" (assert) ((";;; Proof product_fseq_shift-1 for formula product_fseq.product_fseq_shift" (hide -1) ((";;; Proof product_fseq_shift-1 for formula product_fseq.product_fseq_shift" (lemma "product_shift_i[nat]") ((";;; Proof product_fseq_shift-1 for formula product_fseq.product_fseq_shift" (inst - "_" "l1 - 1 + l2" "_" "l1") ((";;; Proof product_fseq_shift-1 for formula product_fseq.product_fseq_shift" (inst - "fs`seq" "-l1") ((";;; Proof product_fseq_shift-1 for formula product_fseq.product_fseq_shift" (assert) ((";;; Proof product_fseq_shift-1 for formula product_fseq.product_fseq_shift" (assert) ((";;; Proof product_fseq_shift-1 for formula product_fseq.product_fseq_shift" (real-props) ((";;; Proof product_fseq_shift-1 for formula product_fseq.product_fseq_shift" (replace -1) ((";;; Proof product_fseq_shift-1 for formula product_fseq.product_fseq_shift" (hide -1) ((";;; Proof product_fseq_shift-1 for formula product_fseq.product_fseq_shift" (rewrite "product_restrict_eq[nat]") (("1" (hide 2) (("1" (expand "restrict") (("1" (propax) nil))))) ("2" (skosimp*) (("2" (assert) nil)))))))))))))))))))))))))))))) ";;; developed with shostak decision procedures") nil nil) (product_fseq_shift-1 nil 3410261125 ("" (skeep) (("" (lemma "product_shift") (("" (inst - "fs`seq" "l2 - 1" "0" "l1") (("" (assert) (("" (hide -1) (("" (lemma "product_shift_i") (("" (inst - "_" "l1 - 1 + l2" "_" "l1") (("" (inst - "fs`seq" "-l1") (("" (assert) (("" (assert) (("" (real-props) (("" (replace -1) (("" (hide -1) (("" (rewrite "product_restrict_eq") (("1" (hide 2) (("1" (expand "restrict") (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T_low type-eq-decl nil product nil) (T_high type-eq-decl nil product nil) (product_restrict_eq formula-decl nil product nil) (restrict const-decl "[T -> real]" product nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/")) shostak)) (product_fseq_concat 0 (product_fseq_concat-2 nil 3411837713 ("" (skeep) (("" (expand "product") (("" (lift-if) (("" (lift-if) (("" (lift-if) (("" (expand "o ") (("" (lift-if) (("" (lift-if) (("" (lift-if) (("" (ground) (("1" (replace -1) (("1" (assert) (("1" (lemma "product_restrict_eq[nat]") (("1" (inst - "LAMBDA (n: nat): IF n < fs2`length THEN fs2`seq(n) ELSE default ENDIF" "fs2`seq" "length(fs2)-1" "0") (("1" (assert) (("1" (hide 3) (("1" (decompose-equality +) (("1" (expand "restrict") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (hide -1) (("2" (assert) (("2" (assert) (("2" (lemma "product_restrict_eq[nat]") (("2" (inst?) (("2" (assert) (("2" (expand "restrict") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "product_split[nat]") (("3" (inst?) (("1" (inst - "length(fs1) - 1") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "product_restrict_eq[nat]") (("1" (inst?) (("1" (inst - "fs1`seq") (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (cancel-by 2 "product(0, length(fs1) - 1, fs1`seq)") (("1" (lemma "product_fseq_shift") (("1" (inst - "fs2" "l(fs1)" "l(fs2)" "fs1") (("1" (assert) (("1" (replace -1 + rl) (("1" (hide -1) (("1" (lemma "product_restrict_eq[nat]") (("1" (inst?) (("1" (assert) (("1" (hide 4) (("1" (expand "restrict") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide 3) (("2" (expand "restrict") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((product const-decl "real" product_fseq nil) (O const-decl "fseq" fseqs "structures/") (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers 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) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (odd_times_odd_is_odd application-judgement "odd_int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (T_pred const-decl "[real -> boolean]" product_fseq nil) (T formal-nonempty-subtype-decl nil product_fseq nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (< const-decl "bool" reals nil) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (default const-decl "T" fseqs "structures/") (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil product nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (T_low type-eq-decl nil product nil) (restrict const-decl "[T -> real]" product nil) (product_restrict_eq formula-decl nil product 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) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (fs2 skolem-const-decl "fseq[T]" product_fseq nil) (fs1 skolem-const-decl "fseq[T]" product_fseq nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (product def-decl "real" product nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal nil) (CBD_92 skolem-const-decl "real" product_fseq nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (both_sides_times1 formula-decl nil real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (fsq type-eq-decl nil fsq "structures/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (product_fseq_shift formula-decl nil product_fseq nil) (product_split formula-decl nil product nil)) nil) (product_fseq_concat-1 nil 3411837109 (";;; Proof product_fseq_mult-2 for formula product_fseq.product_fseq_mult" (skeep) ((";;; Proof product_fseq_mult-2 for formula product_fseq.product_fseq_mult" (expand "product") ((";;; Proof product_fseq_mult-2 for formula product_fseq.product_fseq_mult" (lift-if) ((";;; Proof product_fseq_mult-2 for formula product_fseq.product_fseq_mult" (lift-if) ((";;; Proof product_fseq_mult-2 for formula product_fseq.product_fseq_mult" (lift-if) ((";;; Proof product_fseq_mult-2 for formula product_fseq.product_fseq_mult" (expand "o ") ((";;; Proof product_fseq_mult-2 for formula product_fseq.product_fseq_mult" (ground) (("1" (replace -1) (("1" (assert) (("1" (rewrite "product_restrict_eq") (("1" (hide 3) (("1" (expand "restrict") (("1" (propax) nil))))))))))) ("2" (replace -1) (("2" (hide -1) (("2" (assert) (("2" (assert) (("2" (lemma "product_restrict_eq") (("2" (inst?) (("2" (assert) (("2" (inst - "fs2`seq") (("2" (assert) (("2" (expand "restrict") (("2" (propax) nil))))))))))))))))))))) ("3" (lemma "product_split") (("3" (inst?) (("1" (inst - "length(fs1) - 1") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "product_restrict_eq") (("1" (inst?) (("1" (inst - "fs1`seq") (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (cancel-by 2 "product(0, length(fs1) - 1, fs1`seq)") (("1" (lemma "product_fseq_shift") (("1" (inst - "fs2" "l(fs1)" "l(fs2)" "fs1") (("1" (assert) (("1" (replace -1 + rl) (("1" (hide -1) (("1" (lemma "product_restrict_eq") (("1" (inst?) (("1" (assert) (("1" (hide 4) (("1" (expand "restrict") (("1" (propax) nil))))))) ("2" (skosimp*) (("2" (assert) nil))) ("3" (skosimp*) (("3" (assert) nil))))))))))))))))) ("2" (skosimp*) (("2" (assert) nil))))))))))) ("2" (assert) (("2" (hide 3) (("2" (expand "restrict") (("2" (propax) nil))))))))))) ("2" (skosimp*) (("2" (assert) nil))))))))))))))) ("2" (skosimp*) (("2" (assert) nil)))))))))))))))))))) ";;; developed with shostak decision procedures") nil nil)) (product_fseq_empty_seq 0 (product_fseq_empty_seq-1 nil 3410603231 ("" (grind) nil nil) ((T formal-nonempty-subtype-decl nil product_fseq nil) (T_pred const-decl "[real -> boolean]" product_fseq 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) (default const-decl "T" fseqs "structures/") (empty_seq const-decl "fsq" fseqs "structures/") (product const-decl "real" product_fseq nil) (empty_seq_fseq name-judgement "fseq[T]" product_fseq nil)) shostak)) (product_fseq_split_TCC1 0 (product_fseq_split_TCC1-1 nil 3410602985 ("" (subtype-tcc) 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (product_fseq_split_TCC2 0 (product_fseq_split_TCC2-1 nil 3410602985 ("" (subtype-tcc) 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (product_fseq_split 0 (product_fseq_split-1 nil 3410603287 ("" (skosimp*) (("" (expand "product") (("" (lift-if) (("" (lift-if) (("" (expand "^") (("" (expand "empty_seq") (("" (assert) (("" (lemma "product_last[nat]") (("" (inst?) (("" (assert) (("" (replace -1) (("" (hide -1) (("" (lemma "product_restrict_eq[nat]") (("" (inst?) (("" (inst - "( LAMBDA (x: nat): IF x < length(fs!1) - 1 THEN fs!1`seq(x) ELSE default ENDIF)") (("" (assert) (("" (hide 2) (("" (expand "restrict") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((product const-decl "real" product_fseq nil) (empty_seq const-decl "fsq" fseqs "structures/") (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) (product_last formula-decl nil product nil) (restrict const-decl "[T -> real]" product nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (< const-decl "bool" reals nil) (default const-decl "T" fseqs "structures/") (product_restrict_eq formula-decl nil product nil) (T_low type-eq-decl nil product nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (T_high type-eq-decl nil product nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (T formal-nonempty-subtype-decl nil product_fseq nil) (T_pred const-decl "[real -> boolean]" product_fseq nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (^ const-decl "fseq" fseqs "structures/")) nil)) (product_fseq1 0 (product_fseq1-1 nil 3410609736 ("" (grind) nil nil) ((T formal-nonempty-subtype-decl nil product_fseq nil) (T_pred const-decl "[real -> boolean]" product_fseq 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) (default const-decl "T" fseqs "structures/") (fseq1 const-decl "fseq" fseqs "structures/") (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) (product def-decl "real" product nil) (product const-decl "real" product_fseq nil)) shostak))) ¤ Dauer der Verarbeitung: 0.42 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 |
