| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/reals/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 64 kB |
|
Quellcode-Bibliothek product_seq_scaf.prf Sprache: Lisp |
|||||||||
|
(product_seq_scaf
(product_rec_TCC1 0 (product_rec_TCC1-1 nil 3407849048 ("" (subtype-tcc) nil nil) nil nil)) (product_rec_TCC2 0 (product_rec_TCC2-1 nil 3407849048 ("" (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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (product_rec_TCC3 0 (product_rec_TCC3-1 nil 3407849048 ("" (termination-tcc) nil nil) nil nil)) (product_rec_mult_TCC1 0 (product_rec_mult_TCC1-1 nil 3407849048 ("" (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) (O const-decl "finseq" finite_sequences nil)) nil)) (product_rec_mult_TCC2 0 (product_rec_mult_TCC2-1 nil 3407849048 ("" (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) (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_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (O const-decl "finseq" finite_sequences nil)) nil)) (product_rec_mult_TCC3 0 (product_rec_mult_TCC3-1 nil 3495989673 ("" (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) (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_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (O const-decl "finseq" finite_sequences nil)) nil)) (product_rec_mult 0 (product_rec_mult-1 nil 3407849048 ("" (skeep) (("" (lift-if) (("" (split) (("1" (flatten) (("1" (case "FORALL (n: nat): n < length(fs1) AND n < length(fs1 o fs2) IMPLIES product_rec(fs1 o fs2, n) = product_rec(fs1, n)") (("1" (inst - "n") (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (induct "n" 1) (("1" (flatten) (("1" (grind) nil nil)) nil) ("2" (skolem 1 "nn") (("2" (flatten) (("2" (expand "product_rec" +) (("2" (assert) (("2" (replace -1) (("2" (grind :exclude ("length" "product_rec")) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split +) (("1" (flatten) (("1" (case "fs1 o fs2 = fs2") (("1" (assert) nil nil) ("2" (hide-all-but (-1 1)) (("2" (decompose-equality) (("1" (grind) nil nil) ("2" (decompose-equality) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "FORALL (n:nat): length(fs1)+n < length(fs1 o fs2) IMPLIES product_rec(fs1 o fs2,length(fs1)+n) = product_rec(fs1,length(fs1)-1)*product_rec(fs2,n)") (("1" (inst - "n-length(fs1)") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (hide 3) (("2" (induct "n" 1) (("1" (assert) (("1" (expand "product_rec" + 1) (("1" (case "seq(fs1 o fs2)(length(fs1)) = seq(fs2)(0)") (("1" (case "product_rec(fs1 o fs2,length(fs1)-1) = product_rec(fs1,length(fs1)-1)") (("1" (expand "product_rec" + 3) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (case "FORALL (mm:nat): mm < length(fs1) IMPLIES product_rec(fs1 o fs2, mm) = product_rec(fs1, mm)") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (induct "mm" 1) (("1" (flatten) (("1" (expand "product_rec" 1) (("1" (hide-all-but (1 3)) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (skeep) (("2" (assert) (("2" (expand "product_rec" 1) (("2" (case "seq(fs1 o fs2)(1+j) = seq(fs1)(1+j)") (("1" (assert) nil nil) ("2" (hide-all-but (-2 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (grind) nil nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (assert) (("2" (expand "product_rec" 1 1) (("2" (expand "product_rec" 1 3) (("2" (replace -1) (("2" (case "seq(fs2)(1+j) = seq(fs1 o fs2)(1+length(fs1)+j)") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (grind) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (grind) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((NOT const-decl "[bool -> bool]" booleans nil) (fs2 skolem-const-decl "finite_sequence[posnat]" product_seq_scaf nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (n skolem-const-decl "nat" product_seq_scaf nil) (fs1 skolem-const-decl "finite_sequence[posnat]" product_seq_scaf nil) (int_plus_int_is_int application-judgement "int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (finite_sequence type-eq-decl nil finite_sequences nil) (finseq type-eq-decl nil finite_sequences nil) (O const-decl "finseq" finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (product_rec def-decl "posnat" product_seq_scaf nil)) nil)) (product_rec_caret_TCC1 0 (product_rec_caret_TCC1-1 nil 3407849048 ("" (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) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (^ const-decl "finseq" finite_sequences nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_min application-judgement "{k: int | 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (product_rec_caret 0 (product_rec_caret-1 nil 3407849048 ("" (induct "n") (("1" (skosimp*) (("1" (expand "product_rec") (("1" (ground) (("1" (expand "^") (("1" (propax) nil))))))))) ("2" (skosimp*) (("2" (expand "product_rec" 1) (("2" (inst?) (("2" (assert) (("2" (replace -1) (("2" (hide -1) (("2" (expand "^") (("2" (propax) nil))))))))))))))) ("3" (hide 2) (("3" (skosimp*) (("3" (expand "^") (("3" (lift-if) (("3" (expand "min") (("3" (lift-if) (("3" (ground) nil))))))))))))) ("4" (hide 2) (("4" (skosimp*) nil)))) nil) ((min const-decl "{p: real | p <= m AND p <= n}" real_defs 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) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nat_induction formula-decl nil naturalnumbers nil) (product_rec def-decl "posnat" product_seq_scaf nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (pred type-eq-decl nil defined_types 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) (below type-eq-decl nil nat_types nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (finite_sequence type-eq-decl nil finite_sequences nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (finseq type-eq-decl nil finite_sequences nil) (^ const-decl "finseq" finite_sequences nil)) nil))) ¤ 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.0.2Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28