| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/numbers/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 165 kB |
|
Impressum unique_scaf.prfInteraktion undPortierbarkeitLisp |
|||||||||||||||
|
(unique_scaf (gcd_primes_TCC1 0 (gcd_primes_TCC1-1 nil 3249308522 ("" (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) (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 "boolean" notequal nil) (divides const-decl "bool" divides nil) (prime? const-decl "bool" primes "ints/")) nil)) (gcd_primes 0 (gcd_primes-3 nil 3407859216 ("" (skosimp*) (("" (lemma "gcd_def") (("" (inst?) (("" (assert) (("" (replace -4) (("" (split +) (("1" (expand "divides") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "divides") (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (expand "divides") (("3" (skosimp*) (("3" (case "x!1 = 1 AND x!2 = 1") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (split +) (("1" (expand "prime?") (("1" (flatten) (("1" (inst -3 "mm!1") (("1" (case-replace "mm!1 = 1") (("1" (assert) nil nil) ("2" (assert) (("2" (case-replace "mm!1 = i!1") (("1" (assert) (("1" (hide -1 -3 -4 -5 -6 3 4 5) (("1" (lemma "both_sides_times1") (("1" (inst -1 "i!1" "1" "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "divides") (("2" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "prime?") (("2" (flatten) (("2" (case-replace "mm!1 = 1") (("1" (assert) nil nil) ("2" (assert) (("2" (case-replace "mm!1 = j!1") (("1" (assert) (("1" (hide -1 -2 -4 -5 -6 3 4 5) (("1" (lemma "both_sides_times1") (("1" (inst -1 "j!1" "1" "x!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst -5 "mm!1") (("2" (expand "divides") (("2" (assert) (("2" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((gcd_def formula-decl nil gcd "ints/") (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (divides const-decl "bool" divides nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (prime? const-decl "bool" primes "ints/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (both_sides_times1 formula-decl nil real_props nil) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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)) nil) (gcd_primes-2 nil 3407848300 ("" (skosimp*) (("" (lemma "gcd_def") (("" (inst?) (("" (assert) (("" (replace -4) (("" (split +) (("1" (expand "divides") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "divides") (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (expand "divides") (("3" (skosimp*) (("3" (case "k!1 = 1 AND k!2 = 1") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (split +) (("1" (expand "prime?") (("1" (flatten) (("1" (inst -3 "mm!1") (("1" (case-replace "mm!1 = 1") (("1" (assert) nil nil) ("2" (assert) (("2" (case-replace "mm!1 = i!1") (("1" (assert) (("1" (hide -1 -3 -4 -5 -6 3 4 5) (("1" (lemma "both_sides_times1") (("1" (inst -1 "i!1" "1" "k!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "divides") (("2" (inst + "k!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "prime?") (("2" (flatten) (("2" (case-replace "mm!1 = 1") (("1" (assert) nil nil) ("2" (assert) (("2" (case-replace "mm!1 = j!1") (("1" (assert) (("1" (hide -1 -2 -4 -5 -6 3 4 5) (("1" (lemma "both_sides_times1") (("1" (inst -1 "j!1" "1" "k!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst -5 "mm!1") (("2" (expand "divides") (("2" (assert) (("2" (inst + "k!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((gcd_def formula-decl nil gcd "ints/") (prime? const-decl "bool" primes "ints/")) nil) (gcd_primes-1 nil 3249308522 ("" (skosimp*) (("" (lemma "gcd_def") (("" (inst?) (("" (assert) (("" (replace -4) (("" (split +) (("1" (expand "divides") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "divides") (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (expand "divides") (("3" (skosimp*) (("3" (case "k!1 = 1 AND k!2 = 1") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (split +) (("1" (expand "prime?") (("1" (flatten) (("1" (inst -3 "mm!1") (("1" (case-replace "mm!1 = 1") (("1" (assert) nil nil) ("2" (assert) (("2" (case-replace "mm!1 = i!1") (("1" (assert) (("1" (hide -1 -3 -4 -5 -6 3 4 5) (("1" (lemma "both_sides_times1") (("1" (inst -1 "i!1" "1" "k!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "divides") (("2" (inst + "k!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "prime?") (("2" (flatten) (("2" (case-replace "mm!1 = 1") (("1" (assert) nil nil) ("2" (assert) (("2" (case-replace "mm!1 = j!1") (("1" (assert) (("1" (hide -1 -2 -4 -5 -6 3 4 5) (("1" (lemma "both_sides_times1") (("1" (inst -1 "j!1" "1" "k!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst -5 "mm!1") (("2" (expand "divides") (("2" (assert) (("2" (inst + "k!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((gcd_def formula-decl nil gcd "ints/") (prime? const-decl "bool" primes "ints/")) nil)) (len1 0 (len1-1 nil 3249308522 ("" (case "(FORALL (fs: fseq[posnat]),(m: nat): ordered_list_of_primes?(fs) AND product(fs) = 1 AND m = length(fs) IMPLIES length(fs) = 0)") (("1" (skosimp*) (("1" (inst -1 "fs!1" "length(fs!1)") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (case "length(fs!1) = 1") (("1" (expand "product") (("1" (assert) (("1" (expand "ordered_list_of_primes?") (("1" (flatten) (("1" (expand "list_of_primes?") (("1" (inst -2 "0") (("1" (expand "product") (("1" (assert) (("1" (replace -1) (("1" (assert) (("1" (expand "prime?") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "product_fseq_split") (("2" (lemma "real_props.product_1") (("2" (inst?) (("1" (assert) (("1" (flatten) (("1" (hide -1 -4 -5) (("1" (expand "ordered_list_of_primes?") (("1" (flatten) (("1" (expand "list_of_primes?") (("1" (inst?) (("1" (lemma "prime_gt_1") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (prod_posnat application-judgement "posnat" product_nat "reals/") (prod_pr application-judgement "posreal" product_nat "reals/") (prod_nat application-judgement "nat" product_nat "reals/") (prod_nnr application-judgement "nnreal" product_nat "reals/") (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (product_0_neg formula-decl nil product_nat "reals/") (odd_minus_odd_is_even application-judgement "even_int" integers nil) (prime? const-decl "bool" primes "ints/") (product def-decl "real" product "reals/") (list_of_primes? const-decl "bool" prime_factorization nil) (product_1 formula-decl nil real_props nil) (prime_gt_1 formula-decl nil primes "ints/") (^ const-decl "fseq" fseqs "structures/") (fs!1 skolem-const-decl "fseq[posnat]" unique_scaf nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (product_fseq_split formula-decl nil product_fseq_posnat "reals/") (nat nonempty-type-eq-decl nil naturalnumbers 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (ordered_list_of_primes? const-decl "bool" prime_factorization nil) (= const-decl "[T, T -> boolean]" equalities nil) (product const-decl "posnat" product_fseq_posnat "reals/")) nil)) (len3 0 (len3-1 nil 3249308522 ("" (skosimp*) (("" (lemma "len1") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((len1 formula-decl nil unique_scaf nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (nat nonempty-type-eq-decl nil naturalnumbers nil)) nil)) (ordered_list_of_primes_caret 0 (ordered_list_of_primes_caret-2 nil 3410544923 ("" (skosimp*) (("" (expand "ordered_list_of_primes?") (("" (flatten) (("" (prop) (("1" (hide -2) (("1" (expand "list_of_primes?") (("1" (skosimp*) (("1" (expand "^") (("1" (inst?) (("1" (assert) (("1" (typepred "i!1") (("1" (expand "^") (("1" (expand "min") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "i!1") (("2" (expand "^") (("2" (expand "min") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (expand "non_decreasing?") (("2" (expand "^") (("2" (skosimp*) (("2" (inst?) (("1" (assert) (("1" (expand "min") (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (typepred "j!1") (("1" (expand "^") (("1" (expand "min") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (typepred "j!1") (("2" (expand "^") (("2" (expand "min") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (typepred "i!1") (("3" (expand "^") (("3" (expand "min") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((ordered_list_of_primes? const-decl "bool" prime_factorization nil) (list_of_primes? const-decl "bool" prime_factorization nil) (^ const-decl "fseq" fseqs "structures/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans 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) (< 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (fs!1 skolem-const-decl "fseq[posnat]" unique_scaf nil) (below type-eq-decl nil naturalnumbers nil) (n!1 skolem-const-decl "below(length(fs!1))" unique_scaf nil) (i!1 skolem-const-decl "below(length(fs!1 ^ (0, n!1)))" unique_scaf nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (non_decreasing? const-decl "bool" product_perm_lems nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (j!1 skolem-const-decl "below(length(fs!1 ^ (0, n!1)))" unique_scaf nil) (i!1 skolem-const-decl "below(length(fs!1 ^ (0, n!1)))" unique_scaf nil)) nil) (ordered_list_of_primes_caret-1 nil 3249308522 ("" (skosimp*) (("" (expand "ordered_list_of_primes?") (("" (flatten) (("" (prop) (("1" (hide -2) (("1" (expand "list_of_primes?") (("1" (skosimp*) (("1" (expand "^") (("1" (inst?) (("1" (assert) (("1" (typepred "i!1") (("1" (expand "^") (("1" (expand "min") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (expand "non_decreasing?") (("2" (expand "^") (("2" (skosimp*) (("2" (inst?) (("1" (assert) nil nil) ("2" (assert) (("2" (typepred "j!1") (("2" (expand "^") (("2" (expand "min") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (typepred "i!1") (("3" (expand "^") (("3" (expand "min") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((ordered_list_of_primes? const-decl "bool" prime_factorization nil) (list_of_primes? const-decl "bool" prime_factorization nil) (non_decreasing? const-decl "bool" product_perm_lems nil)) nil)) (olop 0 (olop-7 nil 3410716143 ("" (skosimp*) (("" (lemma "prime_factors") (("" (inst -1 "m!1") (("1" (skosimp*) (("1" (inst + "sort(fs!1 o fseq1(pn!1))") (("1" (rewrite "product_sort") (("1" (lemma "product_fseq_concat1") (("1" (inst?) (("1" (assert) (("1" (prop) (("1" (typepred "sort(fs!1 o fseq1(pn!1))") (("1" (hide -3 -4 -6) (("1" (expand "ordered_list_of_primes?") (("1" (prop) (("1" (expand "list_of_primes?") (("1" (skosimp*) (("1" (lemma "perm_symmetric") (("1" (inst -1 "fs!1 o fseq1(pn!1)" "sort(fs!1 o fseq1(pn!1))") (("1" (hide -2) (("1" (assert) (("1" (expand "permutation?") (("1" (skosimp*) (("1" (inst?) (("1" (replace -2) (("1" (hide -2 -3 -5) (("1" (expand "o") (("1" (prop) (("1" (inst?) nil nil) ("2" (assert) (("2" (typepred "f!1(i!1)") (("2" (expand "o") (("2" (expand "fseq1") (("2" (hide -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "fseq1") (("3" (typepred "f!1(i!1)") (("3" (expand "o ") (("3" (expand "fseq1") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (expand "increasing?") (("2" (expand "non_decreasing?") (("2" (skosimp*) (("2" (inst -2 "i!1" "j!1") (("2" (assert) (("2" (typepred "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "sort(fs!1 o fseq1(pn!1))") (("2" (lemma "perm_symmetric") (("2" (inst -1 "fs!1 o fseq1(pn!1)" "sort(fs!1 o fseq1(pn!1))") (("2" (assert) (("2" (hide -2) (("2" (expand "permutation?") (("2" (skosimp*) (("2" (case "seqn(fs!1 o fseq1(pn!1))(length(fs!1)) = pn!1") (("1" (case "(EXISTS (jj: below(length(fs!1)+1)): f!1(jj) = length(fs!1))") (("1" (skosimp*) (("1" (inst + "jj!1") (("1" (inst - "jj!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "bijective?") (("2" (flatten) (("2" (expand "surjective?") (("2" (inst -3 "length(fs!1)") (("1" (skosimp*) (("1" (inst + "x!1") (("1" (assert) (("1" (typepred "x!1") (("1" (hide -2 -3 -4 -5 -6 -7 -8 -9 -10 -11) (("1" (rewrite "length_sort") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3 -4 -5 -6 -7 -8 -9 -10 -11 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -1 -2 -3 -4 -5 -6 -7 -8 -9 2) (("3" (grind) nil nil)) nil)) nil) ("2" (hide -1 -2 -3 -4 -5 -6 -7 -8 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((prime_factors formula-decl nil prime_factorization nil) (product_sort formula-decl nil product_perm_lems nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (i!1 skolem-const-decl "below(length(sort(fs!1 o fseq1(pn!1))))" unique_scaf nil) (f!1 skolem-const-decl "[below(length(sort(fs!1 o fseq1(pn!1)))) -> below(length(fs!1 o fseq1(pn!1)))]" unique_scaf nil) (pn!1 skolem-const-decl "posnat" unique_scaf nil) (fs!1 skolem-const-decl "fseq[posnat]" unique_scaf nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (perm_symmetric formula-decl nil permutations_fseq "structures/") (list_of_primes? const-decl "bool" prime_factorization nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sort_length formula-decl nil sort_fseq "structures/") (non_decreasing? const-decl "bool" product_perm_lems nil) (ordered_list_of_primes? const-decl "bool" prime_factorization nil) (NOT const-decl "[bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (x!1 skolem-const-decl "below(length(sort(fs!1 o fseq1(pn!1))))" unique_scaf nil) (length_sort formula-decl nil product_perm_lems nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (default const-decl "T" fseqs "structures/") (surjective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (product_fseq_concat1 formula-decl nil product_fseq_posnat "reals/") (fseq1 const-decl "fseq" fseqs "structures/") (O const-decl "fseq" fseqs "structures/") (sort const-decl "{ss: fseq | permutation?[T, <=](s, ss) AND increasing?(ss)}" sort_fseq "structures/") (increasing? const-decl "bool" sort_fseq "structures/") (permutation? const-decl "bool" permutations_fseq "structures/") (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (fsq type-eq-decl nil fsq "structures/") (AND const-decl "[bool, bool -> bool]" booleans nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (> 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) (m!1 skolem-const-decl "nat" unique_scaf nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil) (olop-6 nil 3410695321 ("" (skosimp*) (("" (lemma "prime_factors") (("" (inst -1 "m!1") (("1" (skosimp*) (("1" (inst + "sort(fs!1 o fseq1(pn!1))") (("1" (rewrite "product_sort") (("1" (lemma "product_fseq_concat1") (("1" (inst?) (("1" (assert) (("1" (prop) (("1" (typepred "sort(fs!1 o fseq1(pn!1))") (("1" (hide -3 -4 -6) (("1" (expand "ordered_list_of_primes?") (("1" (prop) (("1" (expand "list_of_primes?") (("1" (skosimp*) (("1" (lemma "perm_symmetric") (("1" (inst -1 "fs!1 o fseq1(pn!1)" "sort(fs!1 o fseq1(pn!1))") (("1" (hide -2) (("1" (assert) (("1" (expand "permutation?") (("1" (skosimp*) (("1" (inst?) (("1" (replace -2) (("1" (hide -2 -3 -5) (("1" (expand "o") (("1" (prop) (("1" (inst?) nil nil) ("2" (assert) (("2" (typepred "f!1(i!1)") (("2" (expand "o") (("2" (expand "fseq1") (("2" (hide -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "fseq1") (("3" (typepred "f!1(i!1)") (("3" (expand "o ") (("3" (expand "fseq1") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (expand "increasing?") (("2" (expand "non_decreasing?") (("2" (skosimp*) (("2" (inst -2 "i!1" "j!1") (("2" (assert) (("2" (typepred "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "sort(fs!1 o fseq1(pn!1))") (("2" (lemma "perm_symmetric") (("2" (inst -1 "fs!1 o fseq1(pn!1)" "sort(fs!1 o fseq1(pn!1))") (("2" (assert) (("2" (hide -2) (("2" (expand "permutation?") (("2" (skosimp*) (("2" (case "seq(fs!1 o fseq1(pn!1))(length(fs!1)) = pn!1") (("1" (case "(EXISTS (jj: below(length(fs!1)+1)): f!1(jj) = length(fs!1))") (("1" (skosimp*) (("1" (inst + "jj!1") (("1" (inst - "jj!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "bijective?") (("2" (flatten) (("2" (expand "surjective?") (("2" (inst -3 "length(fs!1)") (("1" (skosimp*) (("1" (inst + "x!1") (("1" (assert) (("1" (typepred "x!1") (("1" (hide -2 -3 -4 -5 -6 -7 -8 -9 -10 -11) (("1" (rewrite "length_sort") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3 -4 -5 -6 -7 -8 -9 -10 -11 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -1 -2 -3 -4 -5 -6 -7 -8 -9 2) (("3" (grind) nil nil)) nil)) nil) ("2" (hide -1 -2 -3 -4 -5 -6 -7 -8 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((prime_factors formula-decl nil prime_factorization nil) (product_sort formula-decl nil product_perm_lems nil) (perm_symmetric formula-decl nil permutations_fseq "structures/") (list_of_primes? const-decl "bool" prime_factorization nil) (sort_length formula-decl nil sort_fseq "structures/") (non_decreasing? const-decl "bool" product_perm_lems nil) (ordered_list_of_primes? const-decl "bool" prime_factorization nil) (length_sort formula-decl nil product_perm_lems nil) (default const-decl "T" fseqs "structures/") (fseq1 const-decl "fseq" fseqs "structures/") (O const-decl "fseq" fseqs "structures/") (sort const-decl "{ss: fseq | permutation?[T, <=](s, ss) AND increasing?(ss)}" sort_fseq "structures/") (increasing? const-decl "bool" sort_fseq "structures/") (permutation? const-decl "bool" permutations_fseq "structures/") (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/")) nil) (olop-5 nil 3410611863 ("" (skosimp*) (("" (lemma "prime_factors") (("" (inst -1 "m!1") (("1" (skosimp*) (("1" (inst + "sort(fs!1 o gen1(pn!1))") (("1" (rewrite "product_sort") (("1" (lemma "product_fseq_concat1") (("1" (inst?) (("1" (assert) (("1" (prop) (("1" (typepred "sort(fs!1 o gen1(pn!1))") (("1" (hide -1) (("1" (hide -3 -4 -6) (("1" (expand "ordered_list_of_primes?") (("1" (prop) (("1" (expand "list_of_primes?") (("1" (skosimp*) (("1" (lemma "perm_symmetric") (("1" (inst -1 "fs!1 o gen1(pn!1)" "sort(fs!1 o gen1(pn!1))") (("1" (hide -2) (("1" (assert) (("1" (expand "permutation?") (("1" (skosimp*) (("1" (inst?) (("1" (replace -2) (("1" (hide -2 -3 -5) (("1" (expand "o") (("1" (prop) (("1" (inst?) nil nil) ("2" (assert) (("2" (typepred "f!1(i!1)") (("2" (expand "o") (("2" (expand "gen1") (("2" (hide -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "gen1") (("3" (typepred "f!1(i!1)") (("3" (expand "o ") (("3" (expand "gen1") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (expand "increasing?") (("2" (expand "non_decreasing?") (("2" (skosimp*) (("2" (inst -2 "i!1" "j!1") (("2" (assert) (("2" (typepred "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "sort(fs!1 o gen1(pn!1))") (("2" (lemma "perm_symmetric") (("2" (inst -1 "fs!1 o gen1(pn!1)" "sort(fs!1 o gen1(pn!1))") (("2" (assert) (("2" (hide -2) (("2" (expand "permutation?") (("2" (skosimp*) (("2" (case "seq(fs!1 o gen1(pn!1))(length(fs!1)) = pn!1") (("1" (case "(EXISTS (jj: below(length(fs!1)+1)): f!1(jj) = length(fs!1))") (("1" (skosimp*) (("1" (inst + "jj!1") (("1" (inst - "jj!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "bijective?") (("2" (flatten) (("2" (expand "surjective?") (("2" (inst -3 "length(fs!1)") (("2" (skosimp*) (("2" (inst + "x!1") (("2" (assert) (("2" (typepred "x!1") (("2" (hide -2 -3 -4 -5 -6 -7 -8 -9 -10 -11) (("2" (rewrite "length_sort") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -1 -2 -3 -4 -5 -6 -7 -8 -9 -10 -11 2) (("3" (grind) nil nil)) nil)) nil) ("2" (hide -1 -2 -3 -4 -5 -6 -7 -8 -9 2) (("2" (grind) nil nil)) nil) ("3" (hide -1 -2 -3 -4 -5 -6 -7 -8 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((default const-decl "T" fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (O const-decl "fseq" fseqs "structures/") (length_sort formula-decl nil product_perm_lems nil) (list_of_primes? const-decl "bool" prime_factorization nil) (non_decreasing? const-decl "bool" product_perm_lems nil) (ordered_list_of_primes? const-decl "bool" prime_factorization nil) (product_sort formula-decl nil product_perm_lems nil) (prime_factors formula-decl nil prime_factorization nil)) nil) (olop-4 nil 3410545254 ("" (skosimp*) (("" (lemma "prime_factors") (("" (inst -1 "m!1") (("1" (skosimp*) (("1" (inst + "sort(fs!1 ++ gn1(pn!1))") (("1" (rewrite "product_sort") (("1" (lemma "product_concat1") (("1" (inst?) (("1" (assert) (("1" (prop) (("1" (typepred "sort(fs!1 ++ gn1(pn!1))") (("1" (hide -3 -4 -6) (("1" (expand "ordered_list_of_primes?") (("1" (prop) (("1" (expand "list_of_primes?") (("1" (skosimp*) (("1" (lemma "perm_symmetric") (("1" (inst -1 "fs!1 ++ gn1(pn!1)" "sort(fs!1 ++ gn1(pn!1))") (("1" (hide -2) (("1" (assert) (("1" (expand "permutation?") (("1" (skosimp*) (("1" (inst?) (("1" (replace -2) (("1" (hide -2 -3 -5) (("1" (expand "++") (("1" (prop) (("1" (inst?) nil nil) ("2" (assert) (("2" (typepred "f!1(i!1)") (("2" (expand "++") (("2" (expand "gn1") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (expand "increasing?") (("2" (expand "non_decreasing?") (("2" (skosimp*) (("2" (inst -2 "i!1" "j!1") (("2" (assert) (("2" (typepred "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "sort(fs!1 ++ gn1(pn!1))") (("2" (lemma "perm_symmetric") (("2" (inst -1 "fs!1 ++ gn1(pn!1)" "sort(fs!1 ++ gn1(pn!1))") (("2" (assert) (("2" (hide -2) (("2" (expand "permutation?") (("2" (skosimp*) (("2" (case "seq(fs!1 ++ gn1(pn!1))(length(fs!1)) = pn!1") (("1" (case "(EXISTS (jj: below(length(fs!1)+1)): f!1(jj) = length(fs!1))") (("1" (skosimp*) (("1" (inst + "jj!1") (("1" (inst - "jj!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "bijective?") (("2" (flatten) (("2" (expand "surjective?") (("2" (inst -3 "length(fs!1)") (("1" (skosimp*) (("1" (inst + "x!1") (("1" (assert) (("1" (typepred "x!1") (("1" (hide -2 -3 -4 -5 -6 -7 -8 -9 -10 -11) (("1" (rewrite "length_sort") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3 -4 -5 -6 -7 -8 -9 -10 -11 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -1 -2 -3 -4 -5 -6 -7 -8 -9 2) (("3" (skosimp*) (("3" (grind) nil nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3 -4 -5 -6 -7 -8 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((length_sort formula-decl nil product_perm_lems nil) (ordered_list_of_primes? const-decl "bool" prime_factorization nil) (non_decreasing? const-decl "bool" product_perm_lems nil) (list_of_primes? const-decl "bool" prime_factorization nil) (product_sort formula-decl nil product_perm_lems nil) (prime_factors formula-decl nil prime_factorization nil)) nil) (olop-3 nil 3410545082 ("" (skosimp*) (("" (lemma "prime_factors") (("" (inst -1 "m!1") (("1" (skosimp*) (("1" (inst + "sort(fs!1 ++ gen1(pn!1))") (("1" (rewrite "product_sort") (("1" (lemma "product_concat1") (("1" (inst?) (("1" (assert) (("1" (prop) (("1" (typepred "sort(fs!1 ++ gen1(pn!1))") (("1" (hide -3 -4 -6) (("1" (expand "ordered_list_of_primes?") (("1" (prop) (("1" (expand "list_of_primes?") (("1" (skosimp*) (("1" (lemma "perm_symmetric") (("1" (inst -1 "fs!1 ++ gen1(pn!1)" "sort(fs!1 ++ gen1(pn!1))") (("1" (hide -2) (("1" (assert) (("1" (expand "permutation?") (("1" (skosimp*) (("1" (inst?) (("1" (replace -2) (("1" (hide -2 -3 -5) (("1" (expand "o ") (("1" (prop) (("1" (inst?) nil) ("2" (assert) (("2" (typepred "f!1(i!1)") (("2" (expand "o ") (("2" (expand "gen1") (("2" (propax) nil))))))))))))))))))))))))))))))))))) ("2" (hide -1) (("2" (expand "increasing?") (("2" (expand "non_decreasing?") (("2" (skosimp*) (("2" (inst -2 "i!1" "j!1") (("2" (assert) (("2" (typepred "j!1") (("2" (assert) nil))))))))))))))))))))))) ("2" (typepred "sort(fs!1 ++ gen1(pn!1))") (("2" (lemma "perm_symmetric") (("2" (inst -1 "fs!1 ++ gen1(pn!1)" "sort(fs!1 ++ gen1(pn!1))") (("2" (assert) (("2" (hide -2) (("2" (expand "permutation?") (("2" (skosimp*) (("2" (case "seq(fs!1 ++ gen1(pn!1))(length(fs!1)) = pn!1") (("1" (case "(EXISTS (jj: below(length(fs!1)+1)): f!1(jj) = length(fs!1))") (("1" (skosimp*) (("1" (inst + "jj!1") (("1" (inst - "jj!1") (("1" (assert) nil) ("2" (hide -2 -3 -4 -5 -6 -7 -8 -9 2) (("2" (grind) nil))))) ("2" (hide -2 -3 -4 -5 -6 -7 -8 -9 -10 2) (("2" (grind) nil))))))) ("2" (hide 2) (("2" (expand "bijective?") (("2" (flatten) (("2" (expand "surjective?") (("2" (inst -3 "length(fs!1)") (("1" (skosimp*) (("1" (inst + "x!1") (("1" (assert) (("1" (typepred "x!1") (("1" (hide -2 -3 -4 -5 -6 -7 -8 -9 -10 -11) (("1" (rewrite "length_sort") (("1" (grind) nil))))))))))))) ("2" (hide -1 -2 -3 -4 -5 -6 -7 -8 -9 -10 -11 2) (("2" (grind) nil))))))))))))) ("3" (hide -1 -2 -3 -4 -5 -6 -7 -8 -9 2) (("3" (skosimp*) (("3" (grind) nil))))))) ("2" (hide -1 -2 -3 -4 -5 -6 -7 -8 2) (("2" (grind) nil))) ("3" (hide -1 -2 -3 -4 -5 -6 -7 -8 2) (("3" (grind) nil))))))))))))))))))))))))))))))))) ("2" (assert) nil)))))) nil) nil nil) (olop-2 nil 3410545021 (";;; Proof olop-1 for formula unique_factorization.olop" (skosimp*) ((";;; Proof olop-1 for formula unique_factorization.olop" (lemma "prime_factors") ((";;; Proof olop-1 for formula unique_factorization.olop" (inst -1 "m!1") (("1" (skosimp*) (("1" (inst + "sort(fs!1 ++ gen_seq1(pn!1))") (("1" (rewrite "product_sort") (("1" (lemma "product_concat1") (("1" (inst?) (("1" (assert) (("1" (prop) (("1" (typepred "sort(fs!1 ++ gen_seq1(pn!1))") (("1" (hide -3 -4 -6) (("1" (expand "ordered_list_of_primes?") (("1" (prop) (("1" (expand "list_of_primes?") (("1" (skosimp*) (("1" (lemma "perm_symmetric") (("1" (inst -1 "fs!1 ++ gen_seq1(pn!1)" "sort(fs!1 ++ gen_seq1(pn!1))") (("1" (hide -2) (("1" (assert) (("1" (expand "permutation?") (("1" (skosimp*) (("1" (inst?) (("1" (replace -2) (("1" (hide -2 -3 -5) (("1" (expand "o ") (("1" (prop) (("1" (inst?) nil) ("2" (assert) (("2" (typepred "f!1(i!1)") (("2" (expand "o ") (("2" (expand "gen_seq1") (("2" (propax) nil))))))))))))))))))))))))))))))))))) ("2" (hide -1) (("2" (expand "increasing?") (("2" (expand "non_decreasing?") (("2" (skosimp*) (("2" (inst -2 "i!1" "j!1") (("2" (assert) (("2" (typepred "j!1") (("2" (assert) nil))))))))))))))))))))))) ("2" (typepred "sort(fs!1 ++ gen_seq1(pn!1))") (("2" (lemma "perm_symmetric") (("2" (inst -1 "fs!1 ++ gen_seq1(pn!1)" "sort(fs!1 ++ gen_seq1(pn!1))") (("2" (assert) (("2" (hide -2) (("2" (expand "permutation?") (("2" (skosimp*) (("2" (case "seq(fs!1 ++ gen_seq1(pn!1))(length(fs!1)) = pn!1") (("1" (case "(EXISTS (jj: below(length(fs!1)+1)): f!1(jj) = length(fs!1))") (("1" (skosimp*) (("1" (inst + "jj!1") (("1" (inst - "jj!1") (("1" (assert) nil) ("2" (hide -2 -3 -4 -5 -6 -7 -8 -9 2) (("2" (grind) nil))))) ("2" (hide -2 -3 -4 -5 -6 -7 -8 -9 -10 2) (("2" (grind) nil))))))) ("2" (hide 2) (("2" (expand "bijective?") (("2" (flatten) (("2" (expand "surjective?") (("2" (inst -3 "length(fs!1)") (("1" (skosimp*) (("1" (inst + "x!1") (("1" (assert) (("1" (typepred "x!1") (("1" (hide -2 -3 -4 -5 -6 -7 -8 -9 -10 -11) (("1" (rewrite "length_sort") (("1" (grind) nil))))))))))))) ("2" (hide -1 -2 -3 -4 -5 -6 -7 -8 -9 -10 -11 2) (("2" (grind) nil))))))))))))) ("3" (hide -1 -2 -3 -4 -5 -6 -7 -8 -9 2) (("3" (skosimp*) (("3" (grind) nil))))))) ("2" (hide -1 -2 -3 -4 -5 -6 -7 -8 2) (("2" (grind) nil))) ("3" (hide -1 -2 -3 -4 -5 -6 -7 -8 2) (("3" (grind) nil))))))))))))))))))))))))))))))))) ("2" (assert) nil)))))) ";;; developed with shostak decision procedures") nil nil) (olop-1 nil 3249308522 ("" (skosimp*) (("" (lemma "prime_factors") (("" (inst -1 "m!1") (("1" (skosimp*) (("1" (inst + "sort(fs!1 o gen_seq1(pn!1))") (("1" (rewrite "product_sort") (("1" (lemma "product_concat1") (("1" (inst?) (("1" (assert) (("1" (prop) (("1" (typepred "sort(fs!1 o gen_seq1(pn!1))") (("1" (hide -3 -4 -6) (("1" (expand "ordered_list_of_primes?") (("1" (prop) (("1" (expand "list_of_primes?") (("1" (skosimp*) (("1" (lemma "perm_symmetric") (("1" (inst -1 "fs!1 o gen_seq1(pn!1)" "sort(fs!1 o gen_seq1(pn!1))") (("1" (hide -2) (("1" (assert) (("1" (expand "permutation?") (("1" (skosimp*) (("1" (inst?) (("1" (replace -2) (("1" (hide -2 -3 -5) (("1" (expand "o ") (("1" (prop) (("1" (inst?) nil nil) ("2" (assert) (("2" (typepred "f!1(i!1)") (("2" (expand "o ") (("2" (expand "gen_seq1") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (expand "increasing?") (("2" (expand "non_decreasing?") (("2" (skosimp*) (("2" (inst -2 "i!1" "j!1") (("2" (assert) (("2" (typepred "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "sort(fs!1 o gen_seq1(pn!1))") (("2" (lemma "perm_symmetric") (("2" (inst -1 "fs!1 o gen_seq1(pn!1)" "sort(fs!1 o gen_seq1(pn!1))") (("2" (assert) (("2" (hide -2) (("2" (expand "permutation?") (("2" (skosimp*) (("2" (case "seq(fs!1 o gen_seq1(pn!1))(length(fs!1)) = pn!1") (("1" (case "(EXISTS (jj: below(length(fs!1)+1)): f!1(jj) = length(fs!1))") (("1" (skosimp*) (("1" (inst + "jj!1") (("1" (inst - "jj!1") (("1" (assert) nil nil) ("2" (hide -2 -3 -4 -5 -6 -7 -8 -9 2) (("2" (grind) nil nil)) nil)) nil) ("2" (hide -2 -3 -4 -5 -6 -7 -8 -9 -10 2) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "bijective?") (("2" (flatten) (("2" (expand "surjective?") (("2" (inst -3 "length(fs!1)") (("1" (skosimp*) (("1" (inst + "x!1") (("1" (assert) (("1" (typepred "x!1") (("1" (hide -2 -3 -4 -5 -6 -7 -8 -9 -10 -11) (("1" (rewrite "length_sort") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3 -4 -5 -6 -7 -8 -9 -10 -11 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -1 -2 -3 -4 -5 -6 -7 -8 -9 2) (("3" (skosimp*) (("3" (grind) nil nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3 -4 -5 -6 -7 -8 2) (("2" (grind) nil nil)) nil) ("3" (hide -1 -2 -3 -4 -5 -6 -7 -8 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((prime_factors formula-decl nil prime_factorization nil) (product_sort formula-decl nil product_perm_lems nil) (list_of_primes? const-decl "bool" prime_factorization nil) (non_decreasing? const-decl "bool" product_perm_lems nil) (ordered_list_of_primes? const-decl "bool" prime_factorization nil) (length_sort formula-decl nil product_perm_lems nil)) nil)) (product_len_eq 0 (product_len_eq-4 nil 3410625717 ("" (skosimp*) (("" (case "length(fs2!1) = 0") (("1" (expand "product") (("1" (assert) (("1" (expand "product") (("1" (expand "ordered_list_of_primes?" -3) (("1" (flatten) (("1" (expand "list_of_primes?") (("1" (inst?) (("1" (lemma "prime_gt_1") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "product" -1 1) (("2" (assert) (("2" (replace -4) (("2" (assert) (("2" (rewrite "product_fseq_split") (("2" (hide -3) (("2" (expand "ordered_list_of_primes?") (("2" (flatten) (("2" (hide -3) (("2" (expand "list_of_primes?") (("2" (inst?) (("2" (name "NN" "seq(fs2!1)(length(fs2!1) - 1)") (("2" (replace -1) (("2" (expand "prime?") (("2" (flatten) (("2" (inst - "NN") (("2" (split -3) (("1" (expand "divides") (("1" (inst + "product(fs2!1 ^ (0, length(fs2!1) - 2))") (("1" (assert) nil nil)) nil)) nil) ("2" (reveal -4) (("2" (expand "ordered_list_of_primes?") (("2" (flatten) (("2" (expand "list_of_primes?") (("2" (inst?) (("2" (assert) (("2" (lemma "prime_gt_1") (("2" (inst -1 "seq(fs2!1)(length(fs2!1) - 1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (case "NN = seq(fs1!1)(0)") (("1" (replace -1 * rl) (("1" (hide -1 -2 1) (("1" (lemma "both_sides_times1") (("1" (inst -1 "NN" "1" "product(fs2!1 ^ (0, length(fs2!1) - 2))") (("1" (assert) (("1" (hide -2) (("1" (hide -2) (("1" (lemma "len1") (("1" (inst -1 "fs2!1 ^ (0, length(fs2!1) - 2)") (("1" (assert) (("1" (split -1) (("1" (expand "^") (("1" (assert) nil nil)) nil) ("2" (reveal -10) (("2" (rewrite "ordered_list_of_primes_caret") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers 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) (prod_posnat application-judgement "posnat" product_nat "reals/") (prod_pr application-judgement "posreal" product_nat "reals/") (prod_nat application-judgement "nat" product_nat "reals/") (prod_nnr application-judgement "nnreal" product_nat "reals/") (ordered_list_of_primes? const-decl "bool" prime_factorization nil) (list_of_primes? const-decl "bool" prime_factorization nil) (prime_gt_1 formula-decl nil primes "ints/") (product_0_neg formula-decl nil product_nat "reals/") (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (product def-decl "real" product "reals/") (product const-decl "posnat" product_fseq_posnat "reals/") (odd_minus_odd_is_even application-judgement "even_int" integers nil) (product_eq_arg formula-decl nil product "reals/") (prime? const-decl "bool" primes "ints/") (nonzero_real nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (len1 formula-decl nil unique_scaf nil) (ordered_list_of_primes_caret formula-decl nil unique_scaf nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (both_sides_times1 formula-decl nil real_props nil) (divides const-decl "bool" divides nil) (^ const-decl "fseq" fseqs "structures/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (product_fseq_split formula-decl nil product_fseq_posnat "reals/")) nil) (product_len_eq-3 nil 3410545421 (";;; Proof product_len_eq-2 for formula unique_factorization.product_len_eq" (skosimp*) ((";;; Proof product_len_eq-2 for formula unique_factorization.product_len_eq" (case "length(fs2!1) = 0") (("1" (expand "product") (("1" (assert) (("1" (expand "product_rec") (("1" (expand "ordered_list_of_primes?" -3) (("1" (flatten) (("1" (expand "list_of_primes?") (("1" (inst?) (("1" (lemma "prime_gt_1") (("1" (inst?) (("1" (assert) nil))))))))))))))))))) ("2" (expand "product" -1 1) (("2" (assert) (("2" (expand "product_rec") (("2" (rewrite "product_split") (("2" (hide -3) (("2" (expand "ordered_list_of_primes?") (("2" (flatten) (("2" (hide -3) (("2" (expand "list_of_primes?") (("2" (inst?) (("2" (name "NN" "seq(fs2!1)(length(fs2!1) - 1)") (("2" (replace -1) (("2" (expand "prime?") (("2" (flatten) (("2" (inst - "NN") (("2" (split -3) (("1" (expand "divides") (("1" (inst + "product(fs2!1 ^ (0, length(fs2!1) - 2))") (("1" (assert) nil))))) ("2" (reveal -4) (("2" (expand "ordered_list_of_primes?") (("2" (flatten) (("2" (expand "list_of_primes?") (("2" (inst?) (("2" (assert) (("2" (lemma "prime_gt_1") (("2" (inst -1 "seq(fs2!1)(length(fs2!1) - 1)") (("2" (assert) nil))))))))))))))))) ("3" (case "NN = seq(fs1!1)(0)") (("1" (replace -1 * rl) (("1" (hide -1 -2 1) (("1" (lemma "both_sides_times1") (("1" (inst -1 "NN" "1" "product(fs2!1 ^ (0, length(fs2!1) - 2))") (("1" (assert) (("1" (hide -2) (("1" (hide -2) (("1" (lemma "len1") (("1" (inst -1 "fs2!1 ^ (0, length(fs2!1) - 2)") (("1" (assert) (("1" (split -1) (("1" (expand "^") (("1" (expand "min") (("1" (assert) nil))))) ("2" (reveal -10) (("2" (rewrite "ordered_list_of_primes_caret") nil))))))))))))))))))))))))) ("2" (assert) nil)))))))))))))))))))))))))))))))))))))) ";;; developed with shostak decision procedures") nil nil) (product_len_eq-2 nil 3407848680 ("" (skosimp*) (("" (case "length(fs2!1) = 0") (("1" (expand "product") (("1" (assert) (("1" (expand "product_rec") (("1" (expand "ordered_list_of_primes?" -3) (("1" (flatten) (("1" (expand "list_of_primes?") (("1" (inst?) (("1" (lemma "prime_gt_1") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "product" -1 1) (("2" (assert) (("2" (expand "product_rec") (("2" (rewrite "product_split") (("2" (hide -3) (("2" (expand "ordered_list_of_primes?") (("2" (flatten) (("2" (hide -3) (("2" (expand "list_of_primes?") (("2" (inst?) (("2" (name "NN" "seq(fs2!1)(length(fs2!1) - 1)") (("2" (replace -1) (("2" (expand "prime?") (("2" (flatten) (("2" (inst - "NN") (("2" (split -3) (("1" (expand "divides") (("1" (inst + "product(fs2!1 ^ (0, length(fs2!1) - 2))") (("1" (assert) nil nil)) nil)) nil) ("2" (reveal -4) (("2" (expand "ordered_list_of_primes?") (("2" (flatten) (("2" (expand "list_of_primes?") (("2" (inst?) (("2" (assert) (("2" (lemma "prime_gt_1") (("2" (inst -1 "seq(fs2!1)(length(fs2!1) - 1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (case "NN = seq(fs1!1)(0)") (("1" (replace -1 * rl) (("1" (hide -1 -2 1) (("1" (lemma "both_sides_times1") (("1" (inst -1 "NN" "1" "product(fs2!1 ^ (0, length(fs2!1) - 2))") (("1" (assert) (("1" (hide -2) (("1" (hide -2) (("1" (lemma "len1") (("1" (inst -1 "fs2!1 ^ (0, length(fs2!1) - 2)") (("1" (assert) (("1" (split -1) (("1" (expand "^") (("1" (expand "min") (("1" (assert) nil nil)) nil)) nil) ("2" (reveal -10) (("2" (rewrite "ordered_list_of_primes_caret") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((ordered_list_of_primes? const-decl "bool" prime_factorization nil) (list_of_primes? const-decl "bool" prime_factorization nil) (prime_gt_1 formula-decl nil primes "ints/") (prime? const-decl "bool" primes "ints/")) nil) (product_len_eq-1 nil 3249308522 ("" (skosimp*) (("" (case "length(fs2!1) = 0") (("1" (expand "product") (("1" (assert) (("1" (expand "product_rec") (("1" (expand "ordered_list_of_primes?" -3) (("1" (flatten) (("1" (expand "list_of_primes?") (("1" (inst?) (("1" (lemma "prime_gt_1") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "product" -1 1) (("2" (assert) (("2" (expand "product_rec") (("2" (rewrite "product_split") (("2" (hide -3) (("2" (expand "ordered_list_of_primes?") (("2" (flatten) (("2" (hide -3) (("2" (expand "list_of_primes?") (("2" (inst?) (("2" (name "NN" "seq(fs2!1)(length(fs2!1) - 1)") (("2" (replace -1) (("2" (expand "prime?") (("2" (flatten) (("2" (inst - "NN") (("2" (split -3) (("1" (expand "divides") (("1" (inst + "product(fs2!1 ^ (0, length(fs2!1) - 2))") (("1" (assert) nil nil)) nil)) nil) ("2" (reveal -4) (("2" (expand "ordered_list_of_primes?") (("2" (flatten) (("2" (expand "list_of_primes?") (("2" (inst?) (("2" (assert) (("2" (lemma "prime_gt_1") (("2" (inst -1 "seq(fs2!1)(length(fs2!1) - 1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (case "NN = seq(fs1!1)(0)") (("1" (replace -1 * rl) (("1" (hide -1 -2 1) (("1" (lemma "both_sides_times1") (("1" (inst -1 "NN" "1" "product(fs2!1 ^ (0, length(fs2!1) - 2))") (("1" (assert) (("1" (hide -2) (("1" (hide -2) (("1" (lemma "len1") (("1" (inst -1 "fs2!1 ^ (0, length(fs2!1) - 2)") (("1" (assert) (("1" (split -1) (("1" (expand "^") (("1" (expand "min") (("1" (assert) nil nil)) nil)) nil) ("2" (reveal -10) (("2" (rewrite "ordered_list_of_primes_caret") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((prime_gt_1 formula-decl nil primes "ints/") (prime? const-decl "bool" primes "ints/")) nil)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.138Angebot (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-27) ¤*Eine klare Vorstellung vom Zielzustand |
|
||||||||||||||
2026-05-26