Impressum unique_factorization.prf
Sprache: Lisp
(unique_factorizationnil 3249308522 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )"boolean" notequal nil )"bool" divides nil )"bool" primes "ints/" )"bool" prime_factorization nil )"bool" product_perm_lems nil )"bool" prime_factorizationnil ))nil ))nil 3249308522 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )"boolean" notequal nil )"bool" divides nil )"bool" primes "ints/" )"bool" prime_factorization nil )"bool" product_perm_lems nil )"bool" prime_factorizationnil ))nil ))nil 3410715891"" (skosimp*)"" (rewrite "product_fseq_split" )"" (rewrite "product_fseq_split" -3)"" (lemma "gcd_primes" )"" "seq(fs11!1)(length(fs11!1) - 1)" "seq(fs21!1)(length(fs21!1) - 1)" )"1" (assert )"1" (split -1)"1" (lemma "gcd_factors" )"1" (inst?)"1" (assert )"1" (skosimp*)"1" (replace -2)"1" (hide -2)"1" "Pr2" "product(fs21!1 ^ (0, length(fs21!1) - 2))" )"1" replace -1)"1" case "(ip!1 * seq(fs11!1)(length(fs11!1) - 1) + jp!1 * seq(fs21!1)(length(fs21!1) - 1)) * Pr2 = Pr2" )"1" "1" "(ip!1 * seq(fs11!1)(length(fs11!1)-1) + jp!1 * seq(fs21!1)(length(fs21!1)-1)) ") "1" "1" case "divides(seq(fs11!1)(length(fs11!1) - 1), ") "1" "Pr2" )"1" "1" expand "divides" )"1" "1" "P1" "seq(fs11!1)(length(fs11!1) - 1)" )"1" replace -1)"1" "Q2" "seq(fs21!1)(length(fs21!1) - 1)" )"1" replace -1)"1" "olop" )"1" "1" assert )"1" assert )"1" "1" "1" replace "1" "fs!1" "fs21!1^ (0, length(fs21!1) - 2)" )"1" assert )"1" rewrite "ordered_list_of_primes_caret" )"1" "1" case "l(fs!1) = l(fs21!1 ^ (0, length(fs21!1) - 2))" )"1" case "seqn(fs!1)(i!1) = seqn(fs21!1 ^ (0, length(fs21!1) - 2))(i!1)" )"1" replace "1" "1" expand "ordered_list_of_primes?" "1" "1" expand "non_decreasing?" )"1" expand "^" )"1" "i!1" "length(fs21!1)-1" )"1" assert )"1" replace "1" "1" replace "1" "1" "1" assert )"1" expand "<" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "<" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"2" "2" "len3" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "len3" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "ordered_list_of_primes?" )"2" "2" expand "list_of_primes?" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" "pos_times_gt" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"3" assert )"3" "3" replace "3" "3" "both_sides_times_pos_gt1" )"3" "Pr2" "seq(fs21!1)(length(fs21!1) - 1)" "1" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace -1)"2" "2" "both_sides_times_pos_gt1" )"2" "Pr2" "seq(fs21!1)(length(fs21!1) - 1)" "1" )"2" assert )"2" "2" "2" expand "ordered_list_of_primes?" )"2" "2" expand "list_of_primes?" )"2" "2" "prime_gt_1" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "jp!1 * seq(fs21!1)(length(fs21!1) - 1) * Pr2 = jp!1 * j!1" )"1" replace -5)"1" "1" "divides_plus" )"1" "1" assert )"1" "1" "1" expand "divides" )"1" "Pr2*ip!1" )"1" assert )nil nil ))nil ))nil )"2" expand "divides" )"2" "P1" "product(fs11!1 ^ (0, length(fs11!1) - 2))" )"2" "jp!1*P1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 -2 -3 -5 -6 -7 -8 -9 2)"2" (expand "ordered_list_of_primes?" )"2" (flatten)"2" (expand "list_of_primes?" )"2" (inst?) nil nil )) nil ))nil ))nil ))nil )"3" (hide -1 -2 -3 -4 -6 -7 -8 -9 2)"3" (expand "ordered_list_of_primes?" )"3" (flatten)"3" (expand "list_of_primes?" )"3" (inst?) nil nil )) nil ))nil ))nil ))nil )"4" (expand "<" ) (("4" (assert ) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ) ("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )nil product_fseq_posnat "reals/" )nil naturalnumbers nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )nil fseqs "structures/" )nil fseqs "structures/" )"int" integers nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"posint" nil )nil unique_scaf nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil gcd "ints/" )"[T, T -> boolean]" equalities nil )"posnat" product_fseq_posnat "reals/" )"fseq" fseqs "structures/" )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"bool" divides nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posnat" unique_factorization nil )"posnat" unique_factorization nil )"int" unique_factorization nil )"posnat" unique_factorization nil )"int" unique_factorization nil )"int" unique_factorization nil )"bool" prime_factorization nil )nil naturalnumbers nil )"bool" reals nil )nil unique_scaf nil )"bool" prime_factorization nil )"bool" product_perm_lems nil )"fseq[posnat]" unique_factorization nil )"below(length(fs!1))" unique_factorizationnil )nil unique_scaf nil )nil real_props nil )nil real_types nil )nil real_types nil )nil real_props nil )nil unique_scaf nil )nil primes "ints/" )nil divides_lems "ints/" )"boolean" notequal nil )nil integers nil )"fseq[posnat]" unique_factorization nil )"fseq[posnat]" unique_factorization nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"(total_order?[real])" nil ))nil )nil 3410622718"" (skosimp*)"" (rewrite "product_fseq_split" )"" (rewrite "product_fseq_split" -3)"" (lemma "gcd_primes" )"" "seq(fs11!1)(length(fs11!1) - 1)" "seq(fs21!1)(length(fs21!1) - 1)" )"1" (assert )"1" (split -1)"1" (lemma "gcd_factors" )"1" (inst?)"1" (assert )"1" (skosimp*)"1" (replace -2)"1" (hide -2)"1" "Pr2" "product(fs21!1 ^ (0, length(fs21!1) - 2))" )"1" replace -1)"1" case "(ip!1 * seq(fs11!1)(length(fs11!1) - 1) + jp!1 * seq(fs21!1)(length(fs21!1) - 1)) * Pr2 = Pr2" )"1" "1" "(ip!1 * seq(fs11!1)(length(fs11!1)-1) + jp!1 * seq(fs21!1)(length(fs21!1)-1)) ") "1" "1" case "divides(seq(fs11!1)(length(fs11!1) - 1), ") "1" "Pr2" )"1" "1" expand "divides" )"1" "1" "P1" "seq(fs11!1)(length(fs11!1) - 1)" )"1" replace -1)"1" "Q2" "seq(fs21!1)(length(fs21!1) - 1)" )"1" replace -1)"1" "olop" )"1" "1" assert )"1" assert )"1" "1" "1" replace "1" "fs!1" "fs21!1^ (0, length(fs21!1) - 2)" )"1" assert )"1" rewrite "ordered_list_of_primes_caret" )"1" "1" case "length(fs!1) = length(fs21!1 ^ (0, length(fs21!1) - 2))" )"1" case "seq(fs!1)(i!1) = seq(fs21!1 ^ (0, length(fs21!1) - 2))(i!1)" )"1" replace "1" "1" expand "ordered_list_of_primes?" "1" "1" expand "non_decreasing?" )"1" expand "^" )"1" "i!1" "length(fs21!1)-1" )"1" assert )nil nil )"2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" assert )nil nil ))nil )"2" "2" "len3" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "len3" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "ordered_list_of_primes?" )"2" "2" expand "list_of_primes?" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" "pos_times_gt" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"3" assert )"3" "3" replace "3" "3" "both_sides_times_pos_gt1" )"3" "Pr2" "seq(fs21!1)(length(fs21!1) - 1)" "1" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace -1)"2" "2" "both_sides_times_pos_gt1" )"2" "Pr2" "seq(fs21!1)(length(fs21!1) - 1)" "1" )"2" assert )"2" "2" "2" expand "ordered_list_of_primes?" )"2" "2" expand "list_of_primes?" )"2" "2" "prime_gt_1" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "jp!1 * seq(fs21!1)(length(fs21!1) - 1) * Pr2 = jp!1 * j!1" )"1" replace -5)"1" "1" "divides_plus" )"1" "1" assert )"1" "1" "1" expand "divides" )"1" "Pr2*ip!1" )"1" assert )nil nil ))nil ))nil )"2" expand "divides" )"2" "P1" "product(fs11!1 ^ (0, length(fs11!1) - 2))" )"2" "jp!1*P1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 -2 -3 -5 -6 -7 -8 -9 2)"2" (expand "ordered_list_of_primes?" )"2" (flatten)"2" (expand "list_of_primes?" )"2" (inst?) nil nil )) nil ))nil ))nil ))nil )"3" (hide -1 -2 -3 -4 -6 -7 -8 -9 2)"3" (expand "ordered_list_of_primes?" )"3" (flatten)"3" (expand "list_of_primes?" )"3" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ) ("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )nil fseqs "structures/" )nil fseqs "structures/" )nil unique_scaf nil )nil gcd "ints/" )"fseq" fseqs "structures/" )"bool" prime_factorization nil )nil unique_scaf nil )"bool" prime_factorization nil )"bool" product_perm_lems nil )nil unique_scaf nil )nil unique_scaf nil )nil primes "ints/" )nil divides_lems "ints/" ))nil )nil 3410545718"" (skosimp*)"" (rewrite "product_split" )"" (rewrite "product_split" -3)"" (lemma "gcd_primes" )"" "seq(fs11!1)(length(fs11!1) - 1)" "seq(fs21!1)(length(fs21!1) - 1)" )"1" (assert )"1" (split -1)"1" (lemma "gcd_factors" )"1" (inst?)"1" (assert )"1" (skosimp*)"1" (replace -2)"1" (hide -2)"1" "Pr2" "product(fs21!1 ^^ (0, length(fs21!1) - 2))" )"1" replace -1)"1" case "(ip!1 * seq(fs11!1)(length(fs11!1) - 1) + jp!1 * seq(fs21!1)(length(fs21!1) - 1)) * Pr2 = Pr2" )"1" "1" "(ip!1 * seq(fs11!1)(length(fs11!1)-1) + jp!1 * seq(fs21!1)(length(fs21!1)-1)) ") "1" "1" case "divides(seq(fs11!1)(length(fs11!1) - 1), ") "1" "Pr2" )"1" "1" expand "divides" )"1" "1" "P1" "seq(fs11!1)(length(fs11!1) - 1)" )"1" replace -1)"1" "Q2" "seq(fs21!1)(length(fs21!1) - 1)" )"1" replace -1)"1" "olop" )"1" "1" assert )"1" "1" "1" replace "1" "fs!1" "fs21!1^^ (0, length(fs21!1) - 2)" )"1" assert )"1" rewrite "ordered_list_of_primes_caret" )"1" "1" case "length(fs!1) = length(fs21!1 ^^ (0, length(fs21!1) - 2))" )"1" case "seq(fs!1)(i!1) = seq(fs21!1 ^^ (0, length(fs21!1) - 2))(i!1)" )"1" replace "1" "1" expand "ordered_list_of_primes?" "1" "1" expand "non_decreasing?" )"1" expand "^^" )"1" "i!1" "length(fs21!1)-1" )"1" assert )nil nil )"2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil )"2" "2" "len3" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" "3" expand "ordered_list_of_primes?" )"3" "3" expand "list_of_primes?" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" "pos_times_gt" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"3" assert )"3" "3" replace "3" "3" "both_sides_times_pos_gt1" )"3" "Pr2" "seq(fs21!1)(length(fs21!1) - 1)" "1" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace -1)"2" "2" "both_sides_times_pos_gt1" )"2" "Pr2" "seq(fs21!1)(length(fs21!1) - 1)" "1" )"2" assert )"2" "2" "2" expand "ordered_list_of_primes?" )"2" "2" expand "list_of_primes?" )"2" "2" "prime_gt_1" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "jp!1 * seq(fs21!1)(length(fs21!1) - 1) * Pr2 = jp!1 * j!1" )"1" replace -5)"1" "1" "divides_plus" )"1" "1" assert )"1" "1" "1" expand "divides" )"1" "Pr2*ip!1" )"1" assert )nil nil ))nil ))nil )"2" expand "divides" )"2" "P1" "product(fs11!1 ^^ (0, length(fs11!1) - 2))" )"2" "jp!1*P1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 -2 -3 -5 -6 -7 -8 -9 2)"2" (expand "ordered_list_of_primes?" )"2" (flatten)"2" (expand "list_of_primes?" )"2" (inst?) nil nil )) nil ))nil ))nil ))nil )"3" (hide -1 -2 -3 -4 -6 -7 -8 -9 2)"3" (expand "ordered_list_of_primes?" )"3" (flatten)"3" (expand "list_of_primes?" )"3" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ) ("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )nil divides_lems "ints/" )nil primes "ints/" )"bool" prime_factorization nil )"bool" prime_factorization nil )"bool" product_perm_lems nil )nil gcd "ints/" ))nil )nil 3407848713"" (skosimp*)"" (rewrite "product_split" )"" (rewrite "product_split" -3)"" (lemma "gcd_primes" )"" "seq(fs11!1)(length(fs11!1) - 1)" "seq(fs21!1)(length(fs21!1) - 1)" )"1" (assert )"1" (split -1)"1" (lemma "gcd_factors" )"1" (inst?)"1" (assert )"1" (skosimp*)"1" (replace -2)"1" (hide -2)"1" "Pr2" "product(fs21!1 ^ (0, length(fs21!1) - 2))" )"1" replace -1)"1" case "(ip!1 * seq(fs11!1)(length(fs11!1) - 1) + jp!1 * seq(fs21!1)(length(fs21!1) - 1)) * Pr2 = Pr2" )"1" "1" "(ip!1 * seq(fs11!1)(length(fs11!1)-1) + jp!1 * seq(fs21!1)(length(fs21!1)-1)) ") "1" "1" case "divides(seq(fs11!1)(length(fs11!1) - 1), ") "1" "Pr2" )"1" "1" expand "divides" )"1" "1" "P1" "seq(fs11!1)(length(fs11!1) - 1)" )"1" replace -1)"1" "Q2" "seq(fs21!1)(length(fs21!1) - 1)" )"1" replace -1)"1" "olop" )"1" "1" assert )"1" "1" "1" replace "1" "fs!1" "fs21!1^ (0, length(fs21!1) - 2)" )"1" assert )"1" rewrite "ordered_list_of_primes_caret" )"1" "1" case "length(fs!1) = length(fs21!1 ^ (0, length(fs21!1) - 2))" )"1" case "seq(fs!1)(i!1) = seq(fs21!1 ^ (0, length(fs21!1) - 2))(i!1)" )"1" replace "1" "1" expand "ordered_list_of_primes?" "1" "1" expand "non_decreasing?" )"1" expand "^" )"1" "i!1" "length(fs21!1)-1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" expand "^" )"3" expand "min" )"3" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" "2" "len3" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" "3" expand "ordered_list_of_primes?" )"3" "3" expand "list_of_primes?" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" "pos_times_gt" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"3" assert )"3" "3" replace "3" "3" "both_sides_times_pos_gt1" )"3" "Pr2" "seq(fs21!1)(length(fs21!1) - 1)" "1" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace -1)"2" "2" "both_sides_times_pos_gt1" )"2" "Pr2" "seq(fs21!1)(length(fs21!1) - 1)" "1" )"2" assert )"2" "2" "2" expand "ordered_list_of_primes?" )"2" "2" expand "list_of_primes?" )"2" "2" "prime_gt_1" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "jp!1 * seq(fs21!1)(length(fs21!1) - 1) * Pr2 = jp!1 * j!1" )"1" replace -5)"1" "1" "divides_plus" )"1" "1" assert )"1" "1" "1" expand "divides" )"1" "Pr2*ip!1" )"1" assert )nil nil ))nil ))nil )"2" expand "divides" )"2" "P1" "product(fs11!1 ^ (0, length(fs11!1) - 2))" )"2" "jp!1*P1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 -2 -3 -5 -6 -7 -8 -9 2)"2" (expand "ordered_list_of_primes?" )"2" (flatten)"2" (expand "list_of_primes?" )"2" (inst?) nil nil )) nil ))nil ))nil ))nil )"3" (hide -1 -2 -3 -4 -6 -7 -8 -9 2)"3" (expand "ordered_list_of_primes?" )"3" (flatten)"3" (expand "list_of_primes?" )"3" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ) ("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )nil primes "ints/" )"bool" prime_factorization nil )"bool" prime_factorization nil )"bool" product_perm_lems nil )nil gcd "ints/" ))nil )nil 3306142955"" (skosimp*)"" (rewrite "product_split" )"" (rewrite "product_split" -3)"" (lemma "gcd_primes" )"" "seq(fs11!1)(length(fs11!1) - 1)" "seq(fs21!1)(length(fs21!1) - 1)" )"1" (assert )"1" (split -1)"1" (lemma "gcd_factors" )"1" (inst?)"1" (assert )"1" (skosimp*)"1" (replace -2)"1" (hide -2)"1" "Pr2" "product(fs21!1 ^ (0, length(fs21!1) - 2))" )"1" replace -1)"1" case "(ip!1 * seq(fs11!1)(length(fs11!1) - 1) + jp!1 * seq(fs21!1)(length(fs21!1) - 1)) * Pr2 = Pr2" )"1" "1" "(ip!1 * seq(fs11!1)(length(fs11!1)-1) + jp!1 * seq(fs21!1)(length(fs21!1)-1)) ") "1" "1" case "divides(seq(fs11!1)(length(fs11!1) - 1), ") "1" "Pr2" )"1" "1" expand "divides" )"1" "1" "P1" "seq(fs11!1)(length(fs11!1) - 1)" )"1" replace -1)"1" "Q2" "seq(fs21!1)(length(fs21!1) - 1)" )"1" replace -1)"1" "olop" )"1" "1" assert )"1" "1" "1" replace "1" "fs!1" "fs21!1^ (0, length(fs21!1) - 2)" )"1" assert )"1" rewrite "ordered_list_of_primes_caret" )"1" "1" case "length(fs!1) = length(fs21!1 ^ (0, length(fs21!1) - 2))" )"1" case "seq(fs!1)(i!1) = seq(fs21!1 ^ (0, length(fs21!1) - 2))(i!1)" )"1" replace "1" "1" expand "ordered_list_of_primes?" "1" "1" expand "non_decreasing?" )"1" expand "^" )"1" "i!1" "length(fs21!1)-1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" expand "^" )"3" expand "min" )"3" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" "2" "len3" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" "3" expand "ordered_list_of_primes?" )"3" "3" expand "list_of_primes?" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" "pos_times_gt" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"3" assert )"3" "3" replace "3" "3" "both_sides_times_pos_gt1" )"3" "Pr2" "seq(fs21!1)(length(fs21!1) - 1)" "1" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace -1)"2" "2" "both_sides_times_pos_gt1" )"2" "Pr2" "seq(fs21!1)(length(fs21!1) - 1)" "1" )"2" assert )"2" "2" "2" expand "ordered_list_of_primes?" )"2" "2" expand "list_of_primes?" )"2" "2" "prime_gt_1" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "jp!1 * seq(fs21!1)(length(fs21!1) - 1) * Pr2 = jp!1 * j!1" )"1" replace -5)"1" "1" "divides_plus" )"1" "1" assert )"1" "1" "1" expand "divides" )"1" "Pr2*ip!1" )"1" assert )nil nil ))nil ))nil )"2" expand "divides" )"2" "P1" "product(fs11!1 ^ (0, length(fs11!1) - 2))" )"2" "jp!1*P1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 -2 -3 -5 -6 -7 -8 -9 2)"2" (expand "ordered_list_of_primes?" )"2" (flatten)"2" (expand "list_of_primes?" )"2" (inst?) nil nil )) nil ))nil ))nil ))nil )"3" (hide -1 -2 -3 -4 -6 -7 -8 -9 2)"3" (expand "ordered_list_of_primes?" )"3" (flatten)"3" (expand "list_of_primes?" )"3" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ) ("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )nil gcd "ints/" )"bool" product_perm_lems nil )"bool" prime_factorization nil )"bool" prime_factorization nil )nil primes "ints/" ))nil )nil 3249308522"" (skosimp*)"" (rewrite "product_split" )"" (rewrite "product_split" -3)"" (lemma "gcd_primes" )"" "seq(fs1!1)(length(fs1!1) - 1)" "seq(fs2!1)(length(fs2!1) - 1)" )"1" (assert )"1" (split -1)"1" (lemma "gcd_factors" )"1" (inst?)"1" (assert )"1" (skosimp*)"1" (replace -2)"1" (hide -2)"1" "Pr2" "product(fs2!1 ^ (0, length(fs2!1) - 2))" )"1" replace -1)"1" case "(ip!1 * seq(fs1!1)(length(fs1!1) - 1) + jp!1 * seq(fs2!1)(length(fs2!1) - 1)) * Pr2 = Pr2" )"1" "1" "(ip!1 * seq(fs1!1)(length(fs1!1)-1) + jp!1 * seq(fs2!1)(length(fs2!1)-1)) ") "1" "1" case "divides(seq(fs1!1)(length(fs1!1) - 1), ") "1" "Pr2" )"1" "1" expand "divides" )"1" "1" "P1" "seq(fs1!1)(length(fs1!1) - 1)" )"1" replace -1)"1" "Q2" "seq(fs2!1)(length(fs2!1) - 1)" )"1" replace -1)"1" "olop" )"1" "1" assert )"1" "1" "1" replace "1" "fs!1" "fs2!1^ (0, length(fs2!1) - 2)" )"1" assert )"1" rewrite "ordered_list_of_primes_caret" )"1" "1" case "length(fs!1) = length(fs2!1 ^ (0, length(fs2!1) - 2))" )"1" case "seq(fs!1)(i!1) = seq(fs2!1 ^ (0, length(fs2!1) - 2))(i!1)" )"1" replace "1" "1" expand "ordered_list_of_primes?" "1" "1" expand "non_decreasing?" )"1" expand "^" )"1" "i!1" "length(fs2!1)-1" )"1" assert )nil nil )"2" expand "min" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" expand "^" )"3" expand "min" )"3" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" "2" "len3" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" "3" expand "ordered_list_of_primes?" )"3" "3" expand "list_of_primes?" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" "pos_times_gt" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"3" assert )"3" "3" replace "3" "3" "both_sides_times_pos_gt1" )"3" "Pr2" "seq(fs2!1)(length(fs2!1) - 1)" "1" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace -1)"2" "2" "both_sides_times_pos_gt1" )"2" "Pr2" "seq(fs2!1)(length(fs2!1) - 1)" "1" )"2" assert )"2" "2" "2" expand "ordered_list_of_primes?" )"2" "2" expand "list_of_primes?" )"2" "2" "prime_gt_1" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "jp!1 * seq(fs2!1)(length(fs2!1) - 1) * Pr2 = jp!1 * j!1" )"1" replace -5)"1" "1" "divides_plus" )"1" "1" assert )"1" "1" "1" expand "divides" )"1" "Pr2*ip!1" )"1" assert )nil nil ))nil ))nil )"2" expand "divides" )"2" "P1" "product(fs1!1 ^ (0, length(fs1!1) - 2))" )"2" "jp!1*P1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" assert )"2" "2" "both_sides_times1" )"2" "Pr2" "1" "ip!1 * seq(fs1!1)(length(fs1!1) - 1) + jp!1 * seq(fs2!1)(length(fs2!1) - 1)" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 -2 -3 -5 -6 -7 -8 -9 2)"2" (expand "ordered_list_of_primes?" )"2" (flatten)"2" (expand "list_of_primes?" )"2" (inst?) nil nil )) nil ))nil ))nil ))nil )"3" (hide -1 -2 -3 -4 -6 -7 -8 -9 2)"3" (expand "ordered_list_of_primes?" )"3" (flatten)"3" (expand "list_of_primes?" )"3" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ) ("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )nil gcd "ints/" )"bool" product_perm_lems nil )nil primes "ints/" ))nil ))nil 3410715948"" (induct "n" 1 "NAT_induction" )"" (skosimp*)"" (lemma "len0" )"" (inst-cp -1 "fs2!1" )"" (inst -1 "fs1!1" )"" (assert )"" (case "length(fs1!1) = 1" )"1" (hide -2)"1" (case "length(fs2!1) = 1" )"1" (expand "product" )"1" (expand "product" )"1" (assert )"1" (apply-extensionality 3 :hide? t)"1" (apply-extensionality 1 :hide? t)"1" case "x!1 < 1" )"1" (assert ) nil nil )"2" "fs1!1`seq" )"2" "2" assert )"2" "fs2!1`seq" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "product_fseq_split" )"2" (inst -1 "fs2!1" )"2" (assert )"2" (replace -1)"2" (hide -1)"2" expand "product" -2)"2" replace -2)"2" "2" expand "ordered_list_of_primes?" "2" "2" expand "list_of_primes?" )"2" "0" )"2" expand "prime?" )"2" "2" case "product(fs2!1 ^ (0, length(fs2!1) - 2)) = 1" )"1" replace -1)"1" "len1" )"1" "fs2!1 ^ (0, length(fs2!1) - 2)" )"1" rewrite "ordered_list_of_primes_caret" )"1" assert )"1" "1" expand "^" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "product(fs2!1 ^ (0, length(fs2!1) - 2))" )"2" assert )"2" "1" expand "divides" )"1" "seq(fs2!1)(length(fs2!1) - 1)" )"1" assert )"1" expand "product" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" "2" assert )"2" replace "2" "both_sides_times1" )"2" "seq(fs1!1)(0)" "1" "seq(fs2!1)(length(fs2!1) - 1)" )"2" assert )"2" expand "ordered_list_of_primes?" )"2" "2" expand "list_of_primes?" )"2" "2" assert )"2" "prime_gt_1" )"2" "seq(fs2!1)(length(fs2!1) - 1)" )"2" 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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "product_len_eq" )"2" (inst -1 "fs2!1" "fs1!1" )"2" (assert )"2" (rewrite "product_fseq_split" )"2" (rewrite "product_fseq_split" -3)"2" "seq(fs1!1)(length(fs1!1) - 1) = seq(fs2!1)(length(fs2!1) - 1)" )"1" (hide -1)"1" "FP" "seq(fs2!1)(length(fs2!1) - 1)" )"1" replace -1)"1" "P1" "product(fs1!1 ^ (0, length(fs1!1) - 2))" )"1" replace -1)"1" "P1" )"1" "1" "fs1!1^(0, length(fs1!1) - 2)" "fs2!1^ (0, length(fs2!1) - 2)" )"1" assert )"1" rewrite "ordered_list_of_primes_caret" )"1" rewrite "ordered_list_of_primes_caret" )"1" "1" assert )"1" "1" "1" case "length(fs1!1) = length(fs2!1)" )"1" "1" "1" case "x!1 < length(fs1!1) - 1" )"1" case "seqn(fs1!1 ^ (0, l(fs1!1) - 2))(x!1) = seqn(fs2!1 ^ (0, l(fs2!1) - 2))(x!1)" )"1" expand "^" )"1" assert )nil nil ))nil )"2" assert )nil nil ))nil )"2" assert )"2" "fs1!1`seq" )"2" "2" assert )"2" "fs2!1`seq" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "^" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "P2" "product(fs2!1 ^ (0, length(fs2!1) - 2))" )"2" "2" "both_sides_times1" )"2" "FP" "P1" "P2" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "len1" )"3" "fs1!1 ^ (0, length(fs1!1) - 2)" )"3" assert )"3" "1" assert )"1" "1" expand "^" )"1" assert )nil nil ))nil ))nil ))nil )"2" rewrite "ordered_list_of_primes_caret" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "both_sides_times_pos_lt1" )"2" replace -4)"2" "P1" "1" "FP" )"2" assert )"2" "2" expand "ordered_list_of_primes?" )"2" "2" expand "non_decreasing?" )"2" expand "list_of_primes?" )"2" "2" "prime_gt_1" )"2" "seq(fs2!1)(length(fs2!1) - 1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "seq(fs1!1)(length(fs1!1) - 1) > seq(fs2!1)(length(fs2!1) - 1)" )"1" "FTL_sym" )"1" "fs1!1" "fs2!1" "j!1" )"1" (assert ) nil nil ))nil ))nil )"2" "FTL_sym" )"2" "fs2!1" "fs1!1" "j!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )nil unique_scaf nil )nil unique_factorization nil )nil real_props nil )nil real_types nil )nil real_types nil )"bool" product_perm_lems nil )nil product_fseq_posnat "reals/" )"bool" prime_factorization nil )"bool" primes "ints/" )"fseq" fseqs "structures/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil unique_scaf nil )nil unique_scaf nil )"nat" product_nat "reals/" )"posreal" product_nat "reals/" )"posnat" product_nat "reals/" )"even_int" integersnil )nil product "reals/" )nil real_props nil )nil primes "ints/" )"boolean" notequal nil )nil reals nil )"bool" divides nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"nnreal" product_nat "reals/" )"int" integers nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"posint" nil )nil product_nat "reals/" )NOT const-decl "[bool -> bool]" booleans nil )"T" fseqs "structures/" )"(total_order?[real])" nil )"bool" reals nil )"real" product "reals/" )nil product_fseq_posnat "reals/" )nil naturalnumbers nil )"bool" prime_factorization nil )"posnat" product_fseq_posnat "reals/" )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil fseqs "structures/" )nil fseqs "structures/" )nil integers nil )"bool" reals nil )nil integers nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil )nil 3410714316";;; Proof FTL_prep-3 for formula unique_factorization.FTL_prep" "n" 1 "NAT_induction" )";;; Proof FTL_prep-3 for formula unique_factorization.FTL_prep" ";;; Proof FTL_prep-3 for formula unique_factorization.FTL_prep" "len0" )";;; Proof FTL_prep-3 for formula unique_factorization.FTL_prep" "fs2!1" )";;; Proof FTL_prep-3 for formula unique_factorization.FTL_prep" "fs1!1" )";;; Proof FTL_prep-3 for formula unique_factorization.FTL_prep" assert )";;; Proof FTL_prep-3 for formula unique_factorization.FTL_prep" case "length(fs1!1) = 1" )"1" (hide -2)"1" (case "length(fs2!1) = 1" )"1" (expand "product" )"1" (expand "product" )"1" (assert )"1" (apply-extensionality 3 :hide? t)"1" (apply-extensionality 1 :hide? t)"1" case "x!1 < 1" )"1" (assert ) nil )"2" "fs1!1`seq" )"2" "2" assert )"2" "fs2!1`seq" )"2" "2" assert )nil )))))))))))))))))))))))"2" (lemma "product_fseq_split" )"2" (inst -1 "fs2!1" )"2" (assert )"2" (replace -1)"2" (hide -1)"2" expand "product" -2)"2" replace -2)"2" "2" expand "ordered_list_of_primes?" "2" "2" expand "list_of_primes?" )"2" "0" )"2" expand "prime?" )"2" "2" case "product(fs2!1 ^ (0, length(fs2!1) - 2)) = 1" )"1" replace -1)"1" "len1" )"1" "fs2!1 ^ (0, length(fs2!1) - 2)" )"1" rewrite "ordered_list_of_primes_caret" )"1" assert )"1" "1" expand "^" )"1" assert )nil )))))))))))))))"2" "product(fs2!1 ^ (0, length(fs2!1) - 2))" )"2" assert )"2" "1" expand "divides" )"1" "seq(fs2!1)(length(fs2!1) - 1)" )"1" "product(fs2!1 ^ (0, length(fs2!1) - 2)) = seq(fs1!1)(0)" )"1" "seq(fs1!1)(0)" )"1" replace "1" assert )"1" "both_sides_times1" )"1" "seq(fs1!1)(0)" "seq(fs2!1)(length(fs2!1) - 1)" "1" )"1" assert )nil )))))))))))"2" replace "2" assert )nil )))))))))"2" "2" replace "2" replace "2" assert )"2" "seq(fs1!1)(0)" )"2" expand "ordered_list_of_primes?" )"2" "2" expand "list_of_primes?" )"2" "2" assert )"2" "prime_gt_1" )"2" "seq(fs2!1)(length(fs2!1) - 1)" )"2" assert )nil )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))"2" (lemma "product_len_eq" )"2" (inst -1 "fs2!1" "fs1!1" )"2" (assert )"2" (rewrite "product_fseq_split" )"2" (rewrite "product_fseq_split" -3)"2" "seq(fs1!1)(length(fs1!1) - 1) = seq(fs2!1)(length(fs2!1) - 1)" )"1" (hide -1)"1" "FP" "seq(fs2!1)(length(fs2!1) - 1)" )"1" replace -1)"1" "P1" "product(fs1!1 ^ (0, length(fs1!1) - 2))" )"1" replace -1)"1" "P1" )"1" "1" "fs1!1^(0, length(fs1!1) - 2)" "fs2!1^ (0, length(fs2!1) - 2)" )"1" assert )"1" rewrite "ordered_list_of_primes_caret" )"1" rewrite "ordered_list_of_primes_caret" )"1" "1" assert )"1" "1" "1" case "length(fs1!1) = length(fs2!1)" )"1" "1" "1" case "x!1 < length(fs1!1) - 1" )"1" case "seq(fs1!1 ^ (0, l(fs1!1) - 2))(x!1) = seq(fs2!1 ^ (0, l(fs2!1) - 2))(x!1)" )"1" expand "^" )"1" assert )nil )))"2" assert )nil )))"2" assert )"2" "fs1!1`seq" )"2" "2" assert )"2" "fs2!1`seq" )"2" "2" assert )nil )))))))))))))))))))"2" expand "^" )"2" assert )nil )))))))))))"2" "P2" "product(fs2!1 ^ (0, length(fs2!1) - 2))" )"2" "2" "both_sides_times1" )"2" "FP" "P1" "P2" )"2" assert )nil )))))))))"3" "len1" )"3" "fs1!1 ^ (0, length(fs1!1) - 2)" )"3" assert )"3" "1" assert )"1" "1" expand "^" )"1" assert )nil )))))))"2" rewrite "ordered_list_of_primes_caret" )nil )))))))))))))))))))"2" "2" "both_sides_times_pos_lt1" )"2" replace -4)"2" "P1" "1" "FP" )"2" assert )"2" "2" expand "ordered_list_of_primes?" )"2" "2" expand "non_decreasing?" )"2" expand "list_of_primes?" )"2" "2" "prime_gt_1" )"2" "seq(fs2!1)(length(fs2!1) - 1)" )"2" assert )nil )))))))))))))))))))))))))))))))))))))))))"2" case "seq(fs1!1)(length(fs1!1) - 1) > seq(fs2!1)(length(fs2!1) - 1)" )"1" "FTL_sym" )"1" "fs1!1" "fs2!1" "j!1" )"1" (assert ) nil )))))"2" "FTL_sym" )"2" "fs2!1" "fs1!1" "j!1" )"2" assert )nil ))))))))))))))))))))))))))))))))";;; developed with shostak decision procedures") nil nil )nil 3410545755"" (induct "n" 1 "NAT_induction" )"" (skosimp*)"" (lemma "len0" )"" (inst-cp -1 "fs2!1" )"" (inst -1 "fs1!1" )"" (assert )"" (case "length(fs1!1) = 1" )"1" (hide -2)"1" (case "length(fs2!1) = 1" )"1" (expand "product" )"1" (expand "product" )"1" (assert )"1" (apply-extensionality 3 :hide? t)"1" (apply-extensionality 1 :hide? t)"1" case "x!1 < 1" )"1" (assert ) nil nil )"2" "fs1!1`seq" )"2" "2" assert )"2" "fs2!1`seq" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "product_fseq_split" )"2" (inst -1 "fs2!1" )"2" (assert )"2" (replace -1)"2" (hide -1)"2" expand "product" -2)"2" replace -2)"2" "2" expand "ordered_list_of_primes?" "2" "2" expand "list_of_primes?" )"2" "0" )"2" expand "prime?" )"2" "2" case "product(fs2!1 ^ (0, length(fs2!1) - 2)) = 1" )"1" replace -1)"1" "len1" )"1" "fs2!1 ^ (0, length(fs2!1) - 2)" )"1" rewrite "ordered_list_of_primes_caret" )"1" assert )"1" "1" expand "^" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "product(fs2!1 ^ (0, length(fs2!1) - 2))" )"2" assert )"2" "1" expand "divides" )"1" "seq(fs2!1)(length(fs2!1) - 1)" )"1" "product(fs2!1 ^ (0, length(fs2!1) - 2)) = seq(fs1!1)(0)" )"1" "seq(fs1!1)(0)" )"1" replace "1" assert )"1" "both_sides_times1" )"1" "seq(fs1!1)(0)" "seq(fs2!1)(length(fs2!1) - 1)" "1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" replace "2" replace "2" assert )"2" "seq(fs1!1)(0)" )"2" expand "ordered_list_of_primes?" )"2" "2" expand "list_of_primes?" )"2" "2" assert )"2" "prime_gt_1" )"2" "seq(fs2!1)(length(fs2!1) - 1)" )"2" 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 ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "product_len_eq" )"2" (inst -1 "fs2!1" "fs1!1" )"2" (assert )"2" (rewrite "product_fseq_split" )"2" (rewrite "product_fseq_split" -3)"2" "seq(fs1!1)(length(fs1!1) - 1) = seq(fs2!1)(length(fs2!1) - 1)" )"1" (hide -1)"1" "FP" "seq(fs2!1)(length(fs2!1) - 1)" )"1" replace -1)"1" "P1" "product(fs1!1 ^ (0, length(fs1!1) - 2))" )"1" replace -1)"1" "P1" )"1" "1" "fs1!1^(0, length(fs1!1) - 2)" "fs2!1^ (0, length(fs2!1) - 2)" )"1" assert )"1" rewrite "ordered_list_of_primes_caret" )"1" rewrite "ordered_list_of_primes_caret" )"1" "1" assert )"1" "1" "1" case "length(fs1!1) = length(fs2!1)" )"1" "1" "1" case "x!1 < length(fs1!1) - 1" )"1" case "seq(fs1!1 ^ (0, length(fs1!1) - 2))(x!1) = seq(fs2!1 ^ (0, length(fs2!1) - 2))(x!1)" )"1" expand "^" )"1" assert )nil nil ))nil )"2" assert )nil nil ))nil )"2" assert )"2" "fs1!1`seq" )"2" "2" assert )"2" "fs2!1`seq" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "^" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "P2" "product(fs2!1 ^ (0, length(fs2!1) - 2))" )"2" "2" "both_sides_times1" )"2" "FP" "P1" "P2" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "len1" )"3" "fs1!1 ^ (0, length(fs1!1) - 2)" )"3" assert )"3" "1" assert )"1" "1" expand "^" )"1" assert )nil nil ))nil ))nil ))nil )"2" rewrite "ordered_list_of_primes_caret" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "both_sides_times_pos_lt1" )"2" replace -4)"2" "P1" "1" "FP" )"2" assert )"2" "2" expand "ordered_list_of_primes?" )"2" "2" expand "non_decreasing?" )"2" expand "list_of_primes?" )"2" "2" "prime_gt_1" )"2" "seq(fs2!1)(length(fs2!1) - 1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "seq(fs1!1)(length(fs1!1) - 1) > seq(fs2!1)(length(fs2!1) - 1)" )"1" "FTL_sym" )"1" "fs1!1" "fs2!1" "j!1" )"1" (assert ) nil nil ))nil ))nil )"2" "FTL_sym" )"2" "fs2!1" "fs1!1" "j!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil unique_scaf nil )"bool" product_perm_lems nil )"bool" prime_factorization nil )"bool" primes "ints/" )"fseq" fseqs "structures/" )nil unique_scaf nil )nil unique_scaf nil )nil primes "ints/" )nil product "reals/" )"posnat" product_nat "reals/" )"nat" product_nat "reals/" )nil product_nat "reals/" )"T" fseqs "structures/" )"real" product "reals/" )"bool" prime_factorization nil )nil fseqs "structures/" )nil fseqs "structures/" ))nil )nil 3407848746"" (induct "n" 1 "NAT_induction" )"" (skosimp*)"" (lemma "len0" )"" (inst-cp -1 "fs2!1" )"" (inst -1 "fs1!1" )"" (assert )"" (case "length(fs1!1) = 1" )"1" (hide -2)"1" (case "length(fs2!1) = 1" )"1" (expand "product" )"1" (expand "product_rec" )"1" (assert )"1" (apply-extensionality 3 :hide? t)"1" (apply-extensionality 1 :hide? t) nil nil ))nil ))nil ))nil ))nil )"2" (lemma "product_split" )"2" (inst -1 "fs2!1" )"2" (assert )"2" (replace -1)"2" (hide -1)"2" expand "product" -2)"2" expand "product_rec" -2)"2" replace -2)"2" "2" expand "ordered_list_of_primes?" "2" "2" expand "list_of_primes?" )"2" "0" )"2" expand "prime?" )"2" "2" case "product(fs2!1 ^ (0, length(fs2!1) - 2)) = 1" )"1" replace -1)"1" "len1" )"1" "fs2!1 ^ (0, length(fs2!1) - 2)" )"1" rewrite "ordered_list_of_primes_caret" )"1" assert )"1" "1" expand "^" )"1" expand "min" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "product(fs2!1 ^ (0, length(fs2!1) - 2))" )"2" assert )"2" "1" expand "divides" )"1" "seq(fs2!1)(length(fs2!1) - 1)" )nil nil ))nil )"2" "product(fs2!1 ^ (0, length(fs2!1) - 2)) = seq(fs1!1)(0)" )"1" "both_sides_times1" )"1" "seq(fs1!1)(0)" "seq(fs2!1)(length(fs2!1) - 1)" "1" )"1" assert )"1" "1" expand "ordered_list_of_primes?" )"1" "1" expand "list_of_primes?" )"1" "1" "prime_gt_1" )"1" "seq(fs2!1)(length(fs2!1) - 1)" )"1" assert )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 ))nil ))nil )"2" (lemma "product_len_eq" )"2" (inst -1 "fs2!1" "fs1!1" )"2" (assert )"2" (rewrite "product_split" )"2" (rewrite "product_split" -3)"2" "seq(fs1!1)(length(fs1!1) - 1) = seq(fs2!1)(length(fs2!1) - 1)" )"1" (hide -1)"1" "FP" "seq(fs2!1)(length(fs2!1) - 1)" )"1" replace -1)"1" "P1" "product(fs1!1 ^ (0, length(fs1!1) - 2))" )"1" replace -1)"1" "P1" )"1" "1" "fs1!1^(0, length(fs1!1) - 2)" "fs2!1^ (0, length(fs2!1) - 2)" )"1" assert )"1" rewrite "ordered_list_of_primes_caret" )"1" rewrite "ordered_list_of_primes_caret" )"1" "1" assert )"1" "1" "1" case "length(fs1!1) = length(fs2!1)" )"1" "1" "1" case "seq(fs1!1 ^ (0, length(fs1!1) - 2))(x!1) = seq(fs2!1 ^ (0, length(fs2!1) - 2))(x!1)" )"1" expand "^" )"1" nil nil ))nil )"2" assert )nil nil )"3" expand "^" )"3" expand "min" )"3" assert )nil nil ))nil ))nil )"4" expand "^" )"4" expand "min" )"4" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "^" )"2" "2" expand "min" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "P2" "product(fs2!1 ^ (0, length(fs2!1) - 2))" )"2" "2" "both_sides_times1" )"2" "FP" "P1" "P2" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "len1" )"3" "fs1!1 ^ (0, length(fs1!1) - 2)" )"3" assert )"3" "1" assert )"1" "1" expand "^" )"1" expand "min" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" rewrite "ordered_list_of_primes_caret" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "both_sides_times_pos_lt1" )"2" replace -4)"2" "P1" "1" "FP" )"2" assert )"2" "2" expand "ordered_list_of_primes?" )"2" "2" expand "non_decreasing?" )"2" expand "list_of_primes?" )"2" "2" "prime_gt_1" )"2" "seq(fs2!1)(length(fs2!1) - 1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "seq(fs1!1)(length(fs1!1) - 1) > seq(fs2!1)(length(fs2!1) - 1)" )"1" "FTL_sym" )"1" "fs1!1" "fs2!1" "j!1" )"1" (assert ) nil nil ))nil ))nil )"2" "FTL_sym" )"2" "fs2!1" "fs1!1" "j!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" product_perm_lems nil )nil primes "ints/" )"bool" primes "ints/" )"bool" prime_factorization nil )"bool" prime_factorizationnil ))nil )nil 3249308522"" (induct "n" 1 "NAT_induction" )"" (skosimp*)"" (lemma "len0" )"" (inst-cp -1 "fs2!1" )"" (inst -1 "fs1!1" )"" (assert )"" (case "length(fs1!1) = 1" )"1" (hide -2)"1" (case "length(fs2!1) = 1" )"1" (expand "product" )"1" (expand "product_rec" )"1" (assert )"1" (apply-extensionality 3 :hide? t)"1" (apply-extensionality 1 :hide? t)"1" "1" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "product_split" )"2" (inst -1 "fs2!1" )"2" (assert )"2" (replace -1)"2" (hide -1)"2" expand "product" -2)"2" expand "product_rec" -2)"2" replace -2)"2" "2" expand "ordered_list_of_primes?" "2" "2" expand "list_of_primes?" )"2" "0" )"2" expand "prime?" )"2" "2" case "product(fs2!1 ^ (0, length(fs2!1) - 2)) = 1" )"1" replace -1)"1" "len1" )"1" "fs2!1 ^ (0, length(fs2!1) - 2)" )"1" rewrite "ordered_list_of_primes_caret" )"1" assert )"1" "1" expand "^" )"1" expand "min" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "product(fs2!1 ^ (0, length(fs2!1) - 2))" )"2" assert )"2" "1" expand "divides" )"1" "seq(fs2!1)(length(fs2!1) - 1)" )nil nil ))nil )"2" "product(fs2!1 ^ (0, length(fs2!1) - 2)) = seq(fs1!1)(0)" )"1" "both_sides_times1" )"1" "seq(fs1!1)(0)" "seq(fs2!1)(length(fs2!1) - 1)" "1" )"1" assert )"1" "1" expand "ordered_list_of_primes?" )"1" "1" expand "list_of_primes?" )"1" "1" "prime_gt_1" )"1" "seq(fs2!1)(length(fs2!1) - 1)" )"1" assert )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 ))nil ))nil )"2" (lemma "product_len_eq" )"2" (inst -1 "fs2!1" "fs1!1" )"2" (assert )"2" (rewrite "product_split" )"2" (rewrite "product_split" -3)"2" "seq(fs1!1)(length(fs1!1) - 1) = seq(fs2!1)(length(fs2!1) - 1)" )"1" (hide -1)"1" "FP" "seq(fs2!1)(length(fs2!1) - 1)" )"1" replace -1)"1" "P1" "product(fs1!1 ^ (0, length(fs1!1) - 2))" )"1" replace -1)"1" "P1" )"1" "1" "fs1!1^(0, length(fs1!1) - 2)" "fs2!1^ (0, length(fs2!1) - 2)" )"1" assert )"1" rewrite "ordered_list_of_primes_caret" )"1" rewrite "ordered_list_of_primes_caret" )"1" "1" assert )"1" "1" "1" case "length(fs1!1) = length(fs2!1)" )"1" "1" "1" case "seq(fs1!1 ^ (0, length(fs1!1) - 2))(x!1) = seq(fs2!1 ^ (0, length(fs2!1) - 2))(x!1)" )"1" expand "^" )"1" nil nil ))nil )"2" assert )nil nil )"3" expand "^" )"3" expand "min" )"3" assert )nil nil ))nil ))nil )"4" expand "^" )"4" expand "min" )"4" assert )nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil )"2" expand "^" )"2" "2" expand "min" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "P2" "product(fs2!1 ^ (0, length(fs2!1) - 2))" )"2" "2" "both_sides_times1" )"2" "FP" "P1" "P2" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "len1" )"3" "fs1!1 ^ (0, length(fs1!1) - 2)" )"3" assert )"3" "1" assert )"1" "1" expand "^" )"1" expand "min" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" rewrite "ordered_list_of_primes_caret" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "both_sides_times_pos_lt1" )"2" replace -4)"2" "P1" "1" "FP" )"2" assert )"2" "2" expand "ordered_list_of_primes?" )"2" "2" expand "non_decreasing?" )"2" expand "list_of_primes?" )"2" "2" "prime_gt_1" )"2" "seq(fs2!1)(length(fs2!1) - 1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "seq(fs1!1)(length(fs1!1) - 1) > seq(fs2!1)(length(fs2!1) - 1)" )"1" "FTL_sym" )"1" "fs1!1" "fs2!1" "j!1" )"1" (assert ) nil nil ))nil ))nil )"2" "FTL_sym" )"2" "fs2!1" "fs1!1" "j!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" product_perm_lems nil )nil primes "ints/" )"bool" primes "ints/" ))nil ))nil 3249308522"" (skosimp*)"" (case "n!1 = 1" )"1" (lemma "len1" )"1" (inst?)"1" (assert )"1" (lemma "len1" )"1" (inst -1 "fs2!1" )"1" (assert )"1" (apply-extensionality 1 :hide? t)"1" (apply-extensionality 1 :hide? t)"1" (typepred "fs1!1`seq" )"1" (typepred "fs2!1`seq" )"1" (inst?)"1" (inst?) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "seq(fs1!1)(length(fs1!1)-1) < seq(fs2!1)(length(fs2!1)-1)" )"1" (lemma "FTL_prep" )"1" (inst -1 "fs2!1" "fs1!1" "n!1" )"1" (assert ) nil nil )) nil ))nil )"2" (lemma "FTL_prep" )"2" (inst -1 "fs1!1" "fs2!1" "n!1" )"2" (assert ) nil nil )) nil ))nil )"3" (lemma "len0" )"3" (hide -2) (("3" (inst?) (("3" (assert ) nil nil )) nil ))nil ))nil )"4" (lemma "len0" )"4" (inst?) (("4" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )nil integers nil )"bool" reals nil )nil integers nil )nil fseqs "structures/" )nil fseqs "structures/" )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"T" fseqs "structures/" )nil unique_scaf nil )nil product_fseq_posnat "reals/" )nil unique_factorization nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ 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.505Bemerkung:
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-30)
¤ *Eine klare Vorstellung vom Zielzustand
2026-05-26
