Quelle for_examples.prf
Sprache: Lisp
(for_examplesnil 3505593379 ("" (grind) nil nil )"{t: T | t = for_def(i, upto, a, ext2int(upfrom, upto, f))}" nil )"T" for_iterate nil )"real" for_examples nil )"(strict_total_order?[real])" real_props nil )"real" reals nil ))nil 3508441056 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3508441066"" (skeep)"" (expand "expit" )"" (lemma "for_induction[real]" )"" (inst?)"" (inst -1 "LAMBDA(i:upto(n),a:real): a = x^i" )"" (rewrite "expt_x0" )"" (assert )"" (hide 2)"" (skeep)"" (case-replace "x=0" )"1" (grind) nil nil )"2" (rewrite "expt_plus" )"2" (rewrite "expt_x1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" for_examples nil )"real" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil integers nil )nil for_iterate nil )"[numfield, numfield -> numfield]" number_fields nil )nil exponentiation nil )"int" integers nil )"nat" exponentiation nil )"nat" exponentiation nil )"nzrat" rationalsnil )"(total_order?[real])" nil )"int" integers nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"real" exponentiation nil )nil exponentiation nil )nil exponentiation nil )nil reals nil )nil naturalnumbers nil )nil defined_types nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )nil for_iterate nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil ))nil 3505593275 ("" (grind) nil nil )"nonneg_int" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"nat" for_examples nil )"T" for_iterate nil )"T" for_iterate nil )"{t: T | t = for_def(i, upto, a, ext2int(upfrom, upto, f))}" nil ))nil 3508421087"" (skeep)"" (expand "factit" )"" (lemma "for_down_induction[nat]" )"" (inst? -1)"" "LAMBDA(i:upto(n),a:nat): a = factorial(n)/factorial(n-i)" )"" (assert )"" (hide 2)"" (skeep)"" (expand "factorial" -1 2)"" (grind-reals) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nat" for_examples nil )"posint" nil )"(total_order?[real])" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nonneg_int" nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil for_iterate nil )"[numfield, numfield -> numfield]" number_fields nil )nil factorial "ints/" )nil real_props nil )"int" integers nil )"nzrat" rationalsnil )nil naturalnumbers nil )nil defined_types nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" factorial "ints/" )"[numfield, numfield -> numfield]" number_fields nil )"posrat" nil )"int" integers nil )nil for_iterate 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 naturalnumbers nil ))nil 3505593581 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[list -> boolean]" list_adt nil )"(total_order?[real])" nil )"nat" list_props nil ))nil ))nil 3508362429 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[list -> boolean]" list_adt nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil ))nil ))nil 3505593776 ("" (grind) nil nil )"nat" list_props nil )"T" list_props nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"{t: T | t = for_def(i, upto, a, ext2int(upfrom, upto, f))}" nil )"T" for_iterate nil )"T" for_iterate nil )"real" for_examples nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"int" integers nil ))nil 3508424536"" (skeep)"" (expand "maxit" )"" (lemma "iterate_left_induction[real]" )"" (inst? -1)"1" "LAMBDA(n:below(length(l)),a:real):FORALL(k:upto(n)):nth(l,k) <= a" )"1" (split -1)"1" (inst -1 "i" ) nil nil )"2" (hide 2) (("2" (grind) nil nil )) nil )"3" (hide 2)"3" (skosimp*)"3" (rewrite "le_max" )"3" (flatten)"3" (inst? -1) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp) (("2" (ground) nil nil )) nil )) nil ))nil )"2" (hide 2) (("2" (skosimp) (("2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"real" for_examples nil )"(total_order?[real])" nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )"(cons?[real])" for_examples nil )"[list -> boolean]" list_adt nil )"nat" list_props nil )nil naturalnumbers nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil ) (< const-decl "bool" reals nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil integers nil )nil integers nil )nil for_iterate nil )nil naturalnumbers nil )nil nat_types nil )"T" list_props nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posint" nil )"upto(1 + k!1)" for_examples nil )"below(length(l) - 1)" for_examples nil )"nonneg_int" nil )"posint" nil )nil real_defs nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )nil for_iterate nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil ))nil 3508284859 ("" (grind) nil nil )"nat" list_props nil )"T" list_props nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"{t: T | t = for_def(i, upto, a, ext2int(upfrom, upto, f))}" nil )"T" for_iterate nil )"T" for_iterate nil )"T" for_iterate nil )"real" for_examples nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"int" integers nil ))nil 3508461473"" (skeep)"" (expand "minit" )"" (lemma "iterate_right_induction[real]" )"" (inst?)"1" "LAMBDA(n:below(length(l)),a:real): LET ll = length(l)-1 IN FORALL(k:subrange(ll-n,ll)) :a <= nth(l,k)" )"1" (assert )"1" (split)"1" (inst? -1) nil nil )"2" (hide 2)"2" (skosimp* :preds? t)"2" (rewrite "min_le" )"2" (flatten)"2" (inst?) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp) (("2" (ground) nil nil )) nil )) nil )"3" (hide 2)"3" (skosimp*) (("3" (ground) nil nil )) nil )) nil ))nil )"2" (hide 2)"2" (skosimp*) (("2" (ground) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"real" for_examples nil )"(total_order?[real])" nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )"(cons?[real])" for_examples nil )"[list -> boolean]" list_adt nil )"nat" list_props nil )nil naturalnumbers nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil ) (< const-decl "bool" reals nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil integers nil )nil integers nil )nil for_iterate nil )nil naturalnumbers nil )nil nat_types nil )"T" list_props nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"(total_order?[real])" nil )nil real_defs nil )"below(length(l) - 1)" for_examples nil )"subrange(length(l) - 2 - k!1, length(l) - 1)" for_examples nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"[bool, bool -> bool]" booleans nil )"int" integers nil )nil for_iterate nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil ))quality 100%
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
2026-03-28
