Quelle general_properties.prf
Sprache: Lisp
(general_propertiesnil 3529776145 ("" (subtype-tcc) nil nil )NOT const-decl "[bool -> bool]" booleans nil )nil naturalnumbers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil integers nil )"bool" reals nil )nil integers 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 )"T" fseqs "structures/" ))nil ))nil 3530711428 ("" (subtype-tcc) nil nil ) nil nil ))nil 3529776160"" (skosimp)"" (expand "divides" )"" (skosimp*)"" (inst 1 "x!2 - x!3" )"" (replaces -2) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"bool" divides nil )"int" integers 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 number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"int" integers nil ))nil 3529776145 ("" (subtype-tcc) nil nil )"bool" divides nil )) nil ))nil 3529776181"" (skosimp)"" (expand "divides" )"" (skosimp)"" (lemma "rel_prime_lem" )"" (inst -1 "x!1" "k!1" )"" (assert )"" (expand "rel_prime" )"" (skosimp)"" (lemma "both_sides_times1" )"" (inst -1 "y!1" "1" "m!1 * x!1 + n!1 * k!1" )"1" (prop)"1" (hide (-2 -3 -5))"1" (assert )"1" (rewrite "identity_mult" )"1" "commutative_mult" )"1" "k!1" "n!1" )"1" "1" rewrite "associative_mult" "1" "1" "n!1*x!2 + m!1*y!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (prop)"2" (inst 1 "0" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" divides nil )nil gcd "ints/" )"(divides(m))" divides nil )"(divides(n))" divides nil )"int" integers nil )"boolean" notequal nil )"int" general_properties nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )nil number_fields nil )nil number_fields nil )nil number_fields nil )"even_int" integersnil )nil real_props nil )"bool" gcd "ints/" )nil integers nil )"bool" reals nil )nil integers 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 3530718323"" (skosimp*)"" (case "fs!1`length = 0" )"1" (grind) nil nil )"2" (expand * "divides" "product" )"2" (typepred "j!1" )"2" (typepred "fs!1`length" )"2" (lemma "product_middle" )"2" (inst?)"2" (inst -1 "j!1" )"2" (assert )"2" (replaces -1)"2" "product(0, j!1 - 1, fs!1`seq) * product(1 + j!1, length(fs!1) - 1, fs!1`seq)" )"1" (assert ) nil nil ) ("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil fseqs "structures/" )nil fseqs "structures/" )nil integers nil )"bool" reals nil )nil integers 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 naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )nil naturalnumbers nil )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil product "reals/" )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )"real" product "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"below(fs!1`length)" general_properties nil )"fseq[posnat]" general_properties nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"nnreal" product_nat "reals/" )"nat" product_nat "reals/" )"posreal" product_nat "reals/" )"posnat" product_nat "reals/" )"posint" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil product "reals/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil product "reals/" )"real" reals nil )"int" integers nil )"(total_order?[real])" nil )"bool" divides nil )"posnat" product_fseq_posnat "reals/" ))nil 3529776145 ("" (subtype-tcc) nil nil ) nil nil ))nil 3529776213"" (induct "i" )"1" (typepred "i!1" ) (("1" (propax) nil nil )) nil )"2" (assert ) nil nil )"3" (skosimp*)"3" (case-replace "j!1 = 0" :hide? T)"1" (hide (-1 -2)) (("1" (grind) nil nil )) nil )"2" (assert )"2" (inst -1 "p!1" )"2" (rewrite "expt_plus" )"2" (rewrite "expt_x1" )"2" "seq_power(p!1, 1 + j!1) = seq_power(p!1, j!1) o fseq1(p!1)" "1" (lemma "product_fseq_concat1" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil )"2" (hide 3)"2" (decompose-equality 1)"1" (grind) nil nil )"2" (decompose-equality 1)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil reals nil )nil exponentiation nil )"int" integers nil )"fseq" fseqs "structures/" )"fseq" fseqs "structures/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"posint" nil )nil product_fseq_posnat"reals/" )"(total_order?[real])" nil )"posnat" product_nat "reals/" )"posreal" product_nat "reals/" )"nat" product_nat "reals/" )nil exponentiation nil )"posint" exponentiation nil )"posint" nil )"odd_int" integers nil )"posnat" exponentiation nil )"posrat" nil )"(total_order?[real])" nil )"posint" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"posnat" product_fseq_posnat"reals/" )"(strict_total_order?[real])" real_props nil )"nnreal" product_nat "reals/" )"real" product "reals/" )"T" fseqs "structures/" )"real" exponentiation nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil naturalnumbers nil )"fseq" general_properties nil )"posnat" product_fseq_posnat "reals/" )nil fseqs "structures/" )nil fseqs "structures/" )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil integers nil )nil integers nil )"bool" reals nil )"[bool, bool -> bool]" booleans 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 3530711428 ("" (subtype-tcc) nil nil )"real" exponentiation nil )"bool" general_properties nil ))nil ))nil 3530711533"" (measure-induct+ "fs`length" "fs" )"" (skosimp*)"" (case "x!1`length = 0" )"1" (hide (-2 -3))"1" (inst 1 "0" )"1" (expand "product" )"1" (assert ) (("1" (rewrite "expt_x0" ) nil nil )) nil ))nil ))nil ))nil )"2" (inst -1 "fseqs_ops_def[posnat,default].rest(x!1)" )"2" (inst -1 "p!1" )"2" (prop)"1" (skosimp)"1" case "x!1 = fseq1(x!1`seq(0)) o fseqs_ops_def[posnat, default].rest(x!1)" )"1" (replace -1 2)"1" (expand "only_power_p" )"1" (inst -3 "0" )"1" (skosimp)"1" (inst 2 "n!1 + i!1" )"1" (rewrite "product_fseq_concat" )"1" "1" "1" "1" expand "product" )"1" expand "fseq1" )"1" assert )"1" rewrite "expt_plus" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 -2 3)) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide (-1 -2 3))"2" (decompose-equality 1)"1" (grind) nil nil )"2" "fseqs_ops_def[posnat, default].add_first_rest" )"2" (inst?)"2" (replace -1 1 rl)"2" (hide -1)"2" "2" expand *"add" "first" "fseq1" "rest" "o" "^" )"2" "2" "2" "2" "2" "2" "2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3)"2" (expand "only_power_p" )"2" (skosimp)"2" (inst -1 "j!1 + 1" )"1" (skosimp)"1" (inst 1 "i!1" )"1" "fseqs_ops_def[posnat, default].rest(x!1)`seq(j!1) = x!1`seq(j!1 + 1)" )"1" (hide (-1 2))"1" expand "rest" )"1" expand "^" )"1" "1" "1" (assert ) nil nil )"2" "j!1" )"2" (grind) nil nil ))nil )"3" "j!1" )"3" expand "rest" )"3" expand "^" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (typepred "j!1" )"2" (expand "rest" ) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide (-1 3)) (("3" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"fseq" fseqs_ops_def "structures/" )nil fseqs_def "structures/" )nil fseqs_def "structures/" )"T" fseqs "structures/" )"fseq" fseqs "structures/" )"fseq" fseqs "structures/" )nil product_fseq_posnat "reals/" )"(divides(m))" divides nil )"(divides(n))" divides nil )"posint" nil )"(total_order?[real])" nil )"posnat" product_fseq_posnat"reals/" )nil product "reals/" )nil exponentiation nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"nonneg_int" nil )nil naturalnumbers nil )"fseq[posnat]" general_properties nil )"(strict_total_order?[real])" real_props nil )"fseq" fseqs_def "structures/" )"fsq" fseqs_def "structures/" )"int" integers nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil fseqs_def "structures/" )"fseq[T, default]" fseqs_ops_def"structures/" )"fseq" fseqs_ops_def "structures/" )"posint" nil )"fseq" fseqs_ops_def "structures/" )"T" fseqs_ops_def "structures/" )nil fseqs_ops_def "structures/" )"posint" nil )"below(fseqs_ops_def[posnat, default].rest(x!1)`length)" nil )NOT const-decl "[bool -> bool]" booleans nil )nil exponentiation nil )"nnreal" product_nat "reals/" )"nat" product_nat "reals/" )"posreal" product_nat "reals/" )"posnat" product_nat "reals/" )"posint" exponentiation nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"posnat" product_fseq_posnat "reals/" )"[T, T -> boolean]" equalities nil )"bool" general_properties nil )"[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil fseqs "structures/" )nil fseqs "structures/" )nil integers nil )"bool" reals nil )nil integers 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 naturalnumbers nil )nil measure_induction nil )"bool" orders nil )nil defined_types nil ))nil 3530367448"" (skosimp)"" (expand "divides" )"" (case-replace "i!1 = 1" :hide? T)"1" (inst 1 "1" ) (("1" (grind) nil nil )) nil )"2" (inst 2 "p!1 ^ (i!1 - 1)" )"1" (lemma "expt_plus" )"1" (inst -1 "1" "i!1 - 1" "p!1" ) (("1" (grind) nil nil ))nil ))nil )"2" (typepred "p!1" "i!1" ) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )"bool" divides nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"int" integers nil )"posnat" general_properties nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"posnat" general_properties nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"int" integers nil )"posrat" nil )nil exponentiation nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"posint" exponentiation nil )"posnat" exponentiation nil )"posrat" nil )"(total_order?[real])" nil )"posint" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"real" exponentiation nil )"real" exponentiation nil )nil integers nil )"bool" reals nil )nil integers 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 3529776145 ("" (subtype-tcc) nil nil )"boolean" notequal nil )"bool" divides nil )"bool" primes "ints/" ))nil ))nil 3529776145 ("" (subtype-tcc) nil nil )"real" exponentiation nil )"bool" divides nil )"boolean" notequal nil )"bool" primes "ints/" ))nil ))nil 3529776240"" (skosimp*)"" (case "j!1=0" )"1" (replaces -1)"1" (inst 1 "0" )"1" (rewrite "expt_x0" )"1" (rewrite "one_div_one" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (expand "divides" )"2" (skosimp)"2" (lemma "prime_factors" )"2" (copy -1)"2" (inst -1 "q!1" )"2" (inst -2 "x!1" )"1" (skosimp*)"1" (lemma "product_power" )"1" (inst?)"1" (copy -7)"1" (replace -2 -1)"1" (replace -3 -1)"1" replace -5 -1)"1" "product_fseq_concat" )"1" "1" replace -1 -2 rl)"1" "1" "product_sort" )"1" "fs!1 o fs!2" )"1" replace -1 -2 rl)"1" "1" "Fundamental_Theorem_Arithmetic" )"1" "seq_power(p!1, j!1)" "sort(fs!1 o fs!2)" "product(seq_power(p!1, j!1))" )"1" assert )"1" "1" case "length(fs!1) = 0" )"1" "1" expand "product" )"1" assert )"1" "0" )"1" rewrite "expt_x0" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "fs!1 = seq_power(p!1,length(fs!1))" )"1" replace "1" "1" "product_power" )"1" "length(fs!1)" "p!1" )"1" replace "1" "1" assert )"1" "1" case "length(seq_power(p!1, j!1)) = length(sort(fs!1 o fs!2))" )"1" "1" nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" "1" nil nil ))nil )"2" "2" case "x!2 >= fs!1`length" )"1" "1" "fs!1`seq" )"1" "1" assert )"1" nil nil ))nil ))nil ))nil ))nil )"2" "sort_fseq_in?" )"2" "fs!1 o fs!2" "fs!1`seq(x!2)" )"2" "1" expand "in?" )"1" "1" replace "1" replace "1" expand "seq_power" "1" "1" "1" "1" "1" assert )nil nil )"2" "ii!2" )"2" replace "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "in?" )"2" "1" expand "o" "1" "1" "1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" assert )nil nil ))nil ))nil )"2" "2" expand "ordered_list_of_primes?" )"2" "1" expand "list_of_primes?" )"1" "1" expand "seq_power" )"1" "1" "i!1" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "non_decreasing?" )"2" "2" expand "seq_power" )"2" "2" "2" "2" "1" assert )nil nil )"2" "j!2" )"2" "2" nil nil ))nil ))nil )"3" "i!1" )"3" "3" nil nil ))nil ))nil )"4" "i!1" )"4" "4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "ordered_list_of_primes?" )"3" "1" "1" expand "list_of_primes?" )"1" "1" "sort_fseq_in" )"1" "fs!1 o fs!2" "i!1" )"1" expand "in?" )"1" "1" "1" expand "o" )"1" "1" "ii!1" )nil nil )"2" "ii!1 - fs!1`length" )"2" assert )nil nil ))nil )"3" "ii!1" )"3" expand "o" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "sort(fs!1 o fs!2)" )"2" "2" expand *"increasing?" "non_decreasing?" )"2" "2" "j!2" )"2" "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 )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (hide (-1 -2 3))"2" (typepred "p!1 ^ j!1" )"2" (replaces -2)"2" (typepred "q!1" )"2" (lemma "pos_times_gt" )"2" (inst?) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))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 divides nil )"(total_order?[real])" nil )nil integers nil )"bool" reals nil )nil integers nil )nil exponentiation nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"int" general_properties nil )nil general_properties nil )nil product_fseq_posnat "reals/" )nil product_perm_lems "numbers/" )nil "numbers/" )"(divides(m))" divides nil )"(divides(n))" divides nil )"posint" exponentiation nil )nil sort_fseq "structures/" )"below(length(fs!1 o fs!2))" nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"below(length(sort(fs!1 o fs!2)))" nil )"bool" prime_factorization "numbers/" )"bool" product_perm_lems "numbers/" )"bool" prime_factorization"numbers/" )"nnreal" product_nat "reals/" )"nat" product_nat "reals/" )"posreal" product_nat "reals/" )"posnat" product_nat "reals/" )nil sort_fseq "structures/" )"bool" reals nil )nil naturalnumbers nil )"bool" fsq "structures/" )"int" integers nil )"fseq[posnat]" general_properties nil )"fseq[posnat]" general_properties nil )"nat" general_properties nil )"(strict_total_order?[real])" real_props nil )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"T" fseqs "structures/" )nil sort_fseq "structures/" )"nonneg_int" nil )"fseq" general_properties nil )nil fsq "structures/" )"R" restrict nil )"bool" reals nil )"bool" permutations_fseq "structures/" )"bool" sort_fseq "structures/" )"{ss: fseq | permutation?[T, <=](s, ss) AND increasing?(ss)}" "structures/" )"posnat" product_fseq_posnat "reals/" )"(total_order?[S])" nil )"(dichotomous?[S])" nil )"(partial_order?[S])" nil )"(preorder?[S])" nil )"(transitive?[S])" nil )"(antisymmetric?[S])" nil )"(reflexive?[S])" nil )"fseq" fseqs "structures/" )nil fseqs "structures/" )nil fseqs "structures/" )"nat" general_properties nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )nil real_props nil )nil prime_factorization "numbers/" )"bool" divides nil ))nil 3529776145 ("" (subtype-tcc) nil nil ) nil nil ))nil 3529776343"" (skosimp)"" (lemma "rel_prime_lem" )"" (inst -1 "m!1" "1" )"" (assert )"" (expand "rel_prime" )"" (hide 2)"" (inst 1 "m!1 + 1" "-1" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil gcd "ints/" )"(divides(m))" divides nil )"(divides(n))" divides nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )"int" integers nil )"odd_int" integers nil )"bool" gcd "ints/" )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 3531211631 ("" (subtype-tcc) nil nil )"boolean" notequal nil )"bool" divides nil )"bool" primes "ints/" ))nil ))nil 3531211673"" (skosimp*)"" (expand "gcd" )"" (rewrite "max_def" )"1" (expand "maximum?" )"1" (flatten)"1" (inst -4 "p!1" )"1" (assert )"1" (rewrite "divides_reflexive" )"1" (lemma "prime_gt_1" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (prop)"1" (expand * "nonempty?" "empty?" "member" )"1" (inst -1 "p!1" )"1" (assert )"1" (rewrite "divides_reflexive" ) nil nil )) nil ))nil ))nil )"2" (inst?)"2" (skosimp)"2" (typepred "y!1" )"2" (hide-all-but (-3 -4 1))"2" (expand "prime?" )"2" (flatten)"2" (inst?)"2" (prop)"1" (hide -2) (("1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{k: posnat | divides(k, i) AND divides(k, j)}" gcd"ints/" )"bool" sets nil )"bool" sets nil )"bool" primes "ints/" )NOT const-decl "[bool -> bool]" booleans nil )"bool" max_bounded_posnat "ints/" )nil divides nil )nil naturalnumbers nil )"(total_order?[real])" nil )nil primes "ints/" )"bool" divides nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"bool" sets nil )set type-eq-decl nil sets nil )nil integers nil )"bool" reals nil )nil integers 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 max_bounded_posnat "ints/" ))nil 3531473201"" (skosimp*)"" (lemma "gcd_1_nd" )"" (inst -1 "m!1" "p!1" )"" (assert )"" (prop)"1" (expand "divides" )"1" (skosimp)"1" (replaces -1)"1" (replaces -3)"1" (inst 1 "x!2 * y!1" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "divides" )"2" (skosimp)"2" (replaces -1)"2" (replaces -3)"2" (inst 1 "x!1 * x!2" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil general_properties nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"bool" divides nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil integers nil )"bool" reals nil )nil integers 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 3531473746 ("" (subtype-tcc) nil nil )"bool" divides nil )"{k: posnat | divides(k, i) AND divides(k, j)}" gcd"ints/" )"boolean" notequal nil )"bool" primes "ints/" ))nil ))nil 3531473746 ("" (subtype-tcc) nil nil )"bool" divides nil )"{k: posnat | divides(k, i) AND divides(k, j)}" gcd"ints/" )"boolean" notequal nil )"bool" primes "ints/" ))nil ))nil 3531473752"" (skosimp*)"" (lemma "gcd_1_ndp" )"" (inst -1 "m!1" "p!1" "x!1" "y!1" )"" (assert )"" (flatten)"" (lemma "gcd_is_1" )"" (inst-cp -1 "x!1" "p!1" )"" (inst -1 "y!1" "p!1" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil general_properties nil )"(divides(m))" divides nil )"(divides(n))" divides nil )nil eq_mod "numbers/" )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers 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 ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.48 Sekunden
(vorverarbeitet am 2026-04-28)
¤ *© Formatika GbR, Deutschland
2026-05-26
