Quelle product.prf
Sprache: Lisp
(productnil 3352120046"" (skosimp* t)"" (prop)"1" (lemma "connected_domain" )"1" (inst - "low!1" "high!1" "z!1" ) (("1" (assert ) nil nil ))nil ))nil )"2" (skosimp*)"2" (lemma "connected_domain" )"2" (inst - "j!1" "high!1" "z!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil )"3" (skosimp*)"3" (lemma "connected_domain" )"3" (inst - "low!1" "j!1" "z!1" ) (("3" (assert ) nil nil ))nil ))nil ))nil )"4" (skosimp*)"4" (lemma "connected_domain" )"4" (inst - "low!1" "j!2" "z!1" )"1" (assert ) nil nil )"2" (lemma "connected_domain" )"2" (inst - "j!1" "j!2" "low!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"T_low" product nil )"T_high" product nil )nil integers nil )"(total_order?[real])" nil )nil product nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, 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 )"[int -> boolean]" product nil )nil product nil )"bool" reals nil )nil product nil )nil product nil ))nil 3352229091"" (skosimp*)"" (inst + "high!1" )"1" (assert ) nil nil )"2" (use "T_pred_lem" ) (("2" (assert ) nil nil )) nil ))nil ))nil )"T_high" product nil )nil product nil )"bool" reals nil )nil product nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )"[int -> boolean]" product 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 )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil product nil )nil product nil ))nil ))nil 3352228842"" (skosimp*)"" (inst?)"" (prop) (("" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))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 )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" product nil )nil product nil )"bool" reals nil )nil product nil )nil product nil )"(total_order?[real])" nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"T_high" product nil )"T_low" product nil )"(strict_total_order?[real])" real_props nil ))nil 3410094710"" (skosimp*)"" (typepred "low!1" )"" (typepred "high!1" )"" (assert )"" (skosimp*)"" (typepred "j!1" )"" (lemma "connected_domain" )"" (inst - "low!1" "j!1" "high!1" )"1" (assert ) nil nil )"2" (assert )"2" (skosimp*)"2" (lemma "connected_domain" )"2" (inst - "j!2" "j!1" "low!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil product nil )"bool" reals nil )nil product nil )"[int -> boolean]" product 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 numbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(strict_total_order?[real])" real_props nil )"T_low" product nil )nil integers nil )"(total_order?[real])" nil )nil product nil )nil product nil ))nil ))nil 3410094710"" (skeep)"" (typepred "high" )"" (typepred "low" )"" (assert )"" (ground)"1" (inst + "high" ) (("1" (assert ) nil nil )) nil )"2" (skosimp*)"2" (inst + "j!1" ) (("2" (assert ) nil nil )) nil )) nil )"3" (skosimp*)"3" (inst + "high" ) (("3" (assert ) nil nil )) nil )) nil )"4" (skosimp*)"4" (inst + "j!1" ) (("4" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil product nil )"bool" reals nil )nil product nil )"[int -> boolean]" product 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 numbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil product nil ))nil ))nil 3410094710 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, 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 )"[int -> boolean]" product nil )nil product nil )"bool" reals nil )nil product nil )nil product nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"int" integers nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"int" integers nil ))nil ))nil 3410103726 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, 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 )"[int -> boolean]" product nil )nil product nil )"bool" reals nil )nil product nil )"bool" reals nil )nil naturalnumbers nil )"int" integers nil ))nil ))nil 3410103726"" (skeep)"" (inst + "low + nn + rng" ) (("" (assert ) nil nil )) nil )) nil )"int" integers nil )"nat" product nil )"nat" product nil )nil naturalnumbers nil )"bool" reals nil )"T_low" product nil )nil product nil )"bool" reals nil )nil product nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[int -> boolean]" product 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 )"(total_order?[real])" nil ))nil ))nil 3410103726"" (skeep)"" (typepred "low" )"" (split -1)"1" (inst + "low" ) (("1" (assert ) nil nil )) nil )"2" (skosimp*)"2" (inst + "j!1" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil product nil )"bool" reals nil )nil product nil )"[int -> boolean]" product 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 numbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"T_low" product nil )"int" integers nil )"(total_order?[real])" nil ))nil ))nil 3410103740"" (induct "rng" )"1" (assert )"1" (expand "product" ) (("1" (propax) nil nil )) nil )) nil )"2" (skosimp*)"2" (expand "product" + (1 3))"2" (inst?)"2" (assert )"2" (lemma "T_pred_lem" )"2" (inst?)"2" (inst - "1+j!1+low!1+nn!1" "low!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skosimp*)"3" (inst + "low!1+nn!1" )"1" (assert ) nil nil )"2" (lemma "T_pred_lem" )"2" (inst?)"2" (inst - "low!1+nn!1+rng!2" "low!1" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"4" (hide 2)"4" (skosimp*)"4" (inst + "low!1+nn!1+rng!2" ) (("4" (assert ) nil nil ))nil ))nil ))nil )"5" (hide 2) (("5" (skosimp*) nil nil )) nil ))nil )"T_low" product nil )"nat" product nil )"nat" product nil )"T_low" product nil )"nat" product nil )"nat" product nil )nil product nil )"(total_order?[real])" nil )"posint" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"posint" nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )"int" product nil )nil product nil )"[T, T -> boolean]" equalities nil )nil defined_types 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 )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" product nil )nil product nil )"bool" reals nil )nil product nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil ))nil ))nil 3410103726"" (skeep)"" (typepred "high" )"" (assert )"" (split -1)"1" (inst + "high" ) nil nil )"2" (skosimp*)"2" (inst + "j!1" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil product nil )"bool" reals nil )nil product nil )"[int -> boolean]" product 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 numbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"T_high" product nil )"(total_order?[real])" nil )"int" integers nil ))nil ))nil 3410103726"" (skeep)"" (typepred "low" )"" (split -1)"1" (inst + "low" ) (("1" (assert ) nil nil )) nil )"2" (skosimp*)"2" (inst + "j!1" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil product nil )"bool" reals nil )nil product nil )"[int -> boolean]" product 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 numbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"T_low" product nil )"(total_order?[real])" nil )"int" integers nil )"int" integers nil ))nil ))nil 3410103810"" (skosimp*)"" (case "high!1<low!1" )"1" (expand "product" ) (("1" (assert ) nil nil )) nil )"2" (case-replace "z!1=low!1-1" )"1" (assert )"1" (expand "product" ) (("1" (assert ) nil nil )) nil )) nil )"2" (lemma "product_spl" )"2" (inst - "F!1" "low!1" "z!1-low!1" "high!1-z!1" )"1" (assert )"1" (hide-all-but (1 3))"1" (use "T_pred_lem" ) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ) ("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )nil product nil )nil product nil )"bool" reals nil )nil product nil )"[int -> boolean]" product nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" product nil )nil product nil )nil product nil )nil naturalnumbers nil )"T_high" product nil )"T_low" product nil )"int" product nil )"bool" reals nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil ))nil ))nil 3410104326"" (skeep)"" (cross-mult 2)"" (lemma "product_split" )"" (inst - "F" "high" "low" "z" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil )"rat" rationals nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"int" product nil )nil product nil )nil product nil )"bool" reals nil )nil product nil )"[int -> boolean]" product nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"boolean" notequal nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"int" integers nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"(total_order?[real])" nil )"int" integers nil )nil product nil ))nil 3410104551"" (skeep)"" (cross-mult 2)"" (lemma "product_split" )"" (inst - "F" "high" "low" "z" ) (("" (assert ) nil nil ))nil ))nil ))nil ))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 )"[int -> boolean]" product nil )nil product nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil product nil )nil product nil )"(total_order?[real])" nil )"int" integers nil )"rat" rationals nil )"nzrat" rationalsnil )nil product nil ))nil 3410104588"" (skosimp*)"" (expand "product" )"" (expand "product" ) (("" (propax) nil nil )) nil )) nil ))nil )"int" product nil )) shostak))nil 3410104637"" (skeep)"" (typepred "low" )"" (assert )"" (skosimp*)"" (typepred "high" )"" (assert )"" (split -1)"1" (lemma "connected_domain" )"1" (assert )"1" (inst - "j!1" "high" "low" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (skosimp*)"2" (lemma "connected_domain" )"2" (inst - "j!1" "j!2" "low" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil product nil )"bool" reals nil )nil product nil )"[int -> boolean]" product 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 numbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )nil product nil )nil integers nil )nil product nil )"(total_order?[real])" nil ))nil ))nil 3410104637"" (skeep)"" (typepred "low" )"" (assert )"" (split -1)"1" (inst + "low" ) (("1" (assert ) nil nil )) nil )"2" (skosimp*)"2" (inst + "j!1" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil product nil )"bool" reals nil )nil product nil )"[int -> boolean]" product 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 numbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )"T_low" product nil )"(total_order?[real])" nil )"int" integers nil ))nil ))nil 3410104659"" (skosimp*)"" (lemma "product_split" )"" (inst?)"" (inst -1 "low!1" )"" (rewrite "product_eq_arg" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )nil product nil )"int" integers nil )"(total_order?[real])" nil )"int" integers nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"(total_order?[real])" nil )nil product nil )nil product nil )nil product nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil product nil )"[int -> boolean]" product 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 3410104637"" (skeep)"" (typepred "high" )"" (split -1)"1" (inst + "high" ) (("1" (assert ) nil nil )) nil )"2" (skosimp*)"2" (inst + "j!1" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil product nil )"bool" reals nil )nil product nil )"[int -> boolean]" product 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 numbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"T_high" product nil )"(total_order?[real])" nil )"int" integers nil )"(total_order?[real])" nil ))nil ))nil 3410104637"" (skeep)"" (typepred "high" )"" (assert )"" (skosimp*)"" (lemma "connected_domain" )"" (inst - "low" "j!1" "high" )"1" (assert ) nil nil )"2" (typepred "low" )"2" (assert )"2" (skosimp*)"2" (lemma "connected_domain" )"2" (assert )"2" (inst - "j!2" "j!1" "low" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil product nil )"bool" reals nil )nil product nil )"[int -> boolean]" product 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 numbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil product nil )"T_low" product nil )nil integers nil )"(total_order?[real])" nil )nil product nil )"(total_order?[real])" nil ))nil ))nil 3410104722"" (skosimp*)"" (rewrite "product" ) (("" (assert ) nil nil )) nil )) nil )"int" product 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 )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" product nil )nil product nil )"bool" reals nil )nil product nil )nil product nil )"(strict_total_order?[real])" real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"(total_order?[real])" nil )"int" integers nil ))nil ))nil 3410104812"" (skeep)"" (typepred "i" ) (("" (inst + "i" ) (("" (assert ) nil nil )) nil ))nil ))nil )nil product nil )"[int -> boolean]" product 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 numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )"int" integers nil )"(total_order?[real])" nil ))nil ))nil 3410104812"" (skeep)"" (typepred "i" ) (("" (inst + "i" ) (("" (assert ) nil nil )) nil ))nil ))nil )nil product nil )"[int -> boolean]" product 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 numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )"int" integers nil )"(total_order?[real])" nil ))nil ))nil 3410104844"" (skosimp*)"" (lemma "product_split" )"" (inst?)"" (inst -1 "i!1" )"" (assert )"" (assert )"" (replace -1)"" (hide -1)"" (expand "product" 1 1) (("" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil product nil )"int" product nil )"(total_order?[real])" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"int" integers nil )"int" integers nil )"(total_order?[real])" nil )nil product nil )nil product nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil product nil )"[int -> boolean]" product 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 3410104812 ("" (subtype-tcc) nil nil )"int" integers nil ))nil ))nil 3410105217"" (skolem 1 (_ _ nzr))"" (rewrite "high_low_rewrite" )"" (hide 2)"" (skosimp*)"" (prop)"1" (expand "product" ) (("1" (assert ) nil nil )) nil )"2" (induct "n" 2)"1" (rewrite "product_eq_arg" )"1" (assert )"1" (expand "^" )"1" (expand "expt" )"1" (expand "expt" ) (("1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (use "T_pred_lem" ) (("2" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (expand "product" +)"2" (assert )"2" (lemma "expt_plus" )"2" (inst - "(1 - low!1 + k!1)" "1" "nzr" )"2" (replace -1)"2" (hide -1)"2" rewrite "expt_x1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 3)"3" (skosimp*)"3" (inst + "high!1" )"1" (assert ) nil nil )"2" (use "T_pred_lem" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"[bool, bool -> bool]" booleans nil )"int" integers nil )nil product 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 )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" product nil )nil product nil )"bool" reals nil )nil product nil )nil product nil )nil defined_types nil )"[T, T -> boolean]" equalities nil )"int" product nil )"boolean" notequal nil )nil integers nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" reals nil )"real" exponentiation nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"T_low" product nil )"T_high" product nil )nil integers nil )nil subrange_inductions nil )"(total_order?[real])" nil )nil product nil )"int" exponentiation nil )"(total_order?[real])" nil )"real" exponentiation nil )"nzreal" exponentiation nil )"rat" exponentiation nil )nil product nil )nil reals nil )"nzrat" rationalsnil )"odd_int" integers nil )nil exponentiation nil )"odd_int" integersnil )nil exponentiation nil )"(strict_total_order?[real])" real_props nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"(strict_total_order?[real])" real_props nil ))nil )nil 3410104877"" (skolem 1 (_ _ x))"" (rewrite "high_low_rewrite" )"1" (hide 2)"1" (skosimp*)"1" (prop)"1" (expand "product" ) (("1" (assert ) nil nil )) nil )"2" (induct "n" 2)"1" (rewrite "product_eq_arg" )"1" (assert )"1" (expand "^" )"1" (expand "expt" )"1" (expand "expt" ) (("1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (use "T_pred_lem" ) (("2" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (expand "product" +)"2" (assert )"2" (lemma "expt_plus" )"2" (inst - "(1 - low!1 + k!1)" "1" "x" )"1" (replace -1)"1" (hide -1)"1" rewrite "expt_x1" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (flatten) (("2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 3)"3" (skosimp*)"3" (inst + "high!1" )"1" (assert ) nil nil )"2" (use "T_pred_lem" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"4" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil )nil nil ))nil 3410105243"" (skosimp*)"" (rewrite "product_first" ) (("" (assert ) nil nil )) nil )) nil )nil product 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 )"[int -> boolean]" product nil )nil product nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil product nil )nil product nil )"int" integers nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"(total_order?[real])" nil )"(total_order?[real])" nil ))nil 3410105938 ("" (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 )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" product nil )nil product nil )"bool" reals nil )nil product nil )nil product nil )"boolean" notequal nil )"int" integers nil ))nil ))nil 3410105347"" (skolem 1 ("F" "a" _ _))"" (rewrite "high_low_rewrite" )"1" (hide 2)"1" (skosimp*)"1" (ground)"1" (induct "n" 2)"1" (rewrite "product_eq_arg" )"1" (rewrite "product_eq_arg" )"1" (assert ) (("1" (rewrite "expt_x1" ) nil nil ))nil ))nil )"2" (use "T_pred_lem" ) (("2" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (expand "product" +)"2" (assert )"2" (replace -2)"2" (hide -2)"2" (lemma "expt_plus" )"2" (inst - "(1 - low!1 + k!1)" "1" "a" )"2" assert )"2" replace -1)"2" "2" rewrite "expt_x1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*)"3" (inst + "high!1" )"1" (assert ) nil nil )"2" (use "T_pred_lem" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2) (("2" (skosimp*) nil nil )) nil ))nil ))nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"int" integers nil )nil product 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 )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" product nil )nil product nil )"bool" reals nil )nil product nil )nil product nil )nil defined_types nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"int" product nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )"real" exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"rat" exponentiation nil )"int" integers nil )"T_low" product nil )"T_high" product nil )nil integers nil )"int" product nil )nil subrange_inductions nil )"(total_order?[real])" nil )nil product nil )"(total_order?[real])" nil )nil exponentiation nil )"int" exponentiation nil )nil product nil )"rat" rationals nil )nil reals nil )"odd_int" integers nil )nil exponentiation nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3410107098"" (skosimp*)"" (typepred "n!1" )"" (typepred "low!1" )"" (assert )"" (typepred "high!1" )"" (lemma "connected_domain" )"" (split -2)"1" (split -3)"1" (inst - "low!1" "high!1" "n!1" )"1" (assert ) nil nil )) nil )"2" (skosimp*)"2" (inst - "j!1" "high!1" "n!1" )"2" (assert ) nil nil )) nil ))nil ))nil )"2" (skosimp*)"2" (inst - "low!1" "j!1" "n!1" )"1" (assert ) nil nil )"2" (assert )"2" (skosimp*)"2" (lemma "connected_domain" )"2" (inst - "j!2" "j!1" "low!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integers nil )nil product nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil product nil )nil product nil )"[int -> boolean]" product nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )nil product nil )nil integers nil )"T_high" product nil )"T_low" product nil ))nil ))nil 3410107124"" (skolem 1 ("F" _ _))"" (rewrite "high_low_rewrite" )"1" (hide 2)"1" (skosimp*)"1" (prop)"1" (expand "product" ) (("1" (assert ) nil nil )) nil )"2" (induct "n" 2)"1" (skosimp*)"1" (rewrite "product_eq_arg" )"1" (inst?) nil nil )"2" (hide -1 2)"2" (use "T_pred_lem" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (expand "product" +)"2" (prop)"1" (inst?)"1" (assert ) (("1" (grind-reals) nil nil ))nil ))nil )"2" (skosimp*) (("2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (hide 3)"3" (skosimp*)"3" (inst + "high!1" )"1" (assert ) nil nil )"2" (hide -1)"2" (use "T_pred_lem" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"4" (hide-all-but 1)"4" (skosimp* t)"4" (hide -1)"4" (use "T_pred_lem" ) (("4" (assert ) nil nil ))nil ))nil ))nil ))nil )"5" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp* t)"2" (use "T_pred_lem" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil product 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 )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" product nil )nil product nil )"bool" reals nil )nil product nil )nil product nil )nil defined_types nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"bool" reals nil )"int" product nil )"T_low" product nil )"T_high" product nil )"[T -> int]" product nil )nil subrange_inductions nil )nil product nil )"(total_order?[real])" nil )nil product nil )nil real_props nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"int" integers nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3410107170"" (skolem 1 ("F" _ _))"" (rewrite "high_low_rewrite" )"1" (hide 2)"1" (skosimp*)"1" (prop)"1" (expand "product" ) (("1" (assert ) nil nil )) nil )"2" (induct "n" 2)"1" (skosimp*)"1" (rewrite "product_eq_arg" )"1" (inst?) nil nil )"2" (hide -1 2)"2" (use "T_pred_lem" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (expand "product" +)"2" (prop)"1" (inst?)"1" (assert ) (("1" (grind-reals) nil nil ))nil ))nil )"2" (skosimp*) (("2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (hide 3)"3" (skosimp*)"3" (inst + "high!1" )"1" (assert ) nil nil )"2" (hide -1)"2" (use "T_pred_lem" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"4" (hide-all-but 1)"4" (skosimp* t)"4" (hide -1)"4" (use "T_pred_lem" ) (("4" (assert ) nil nil ))nil ))nil ))nil ))nil )"5" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp* t)"2" (use "T_pred_lem" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil product 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 )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" product nil )nil product nil )"bool" reals nil )nil product nil )nil product nil )nil defined_types nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"bool" reals nil )"int" product nil )"T_low" product nil )"T_high" product nil )"[T -> int]" product nil )nil subrange_inductions nil )"(total_order?[real])" nil )"bool" reals nil )nil product nil )"(total_order?[real])" nil )nil product nil )nil real_props nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"int" integers nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(divides(n))" divides nil )"(divides(m))" divides nil ))nil ))nil 3410108130"" (skosimp* t)"" (prop)"1" (inst - "low!1" ) nil nil )"2" (skosimp*)"2" (inst + "j!1+z!1" )"1" (assert ) nil nil ) ("2" (inst?) nil nil )) nil ))nil ))nil ))nil )"T_low" product nil )"int" integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"T" product nil )"int" product nil )"(total_order?[real])" nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, 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 )"[int -> boolean]" product nil )nil product nil )"bool" reals nil )nil product nil ))nil ))nil 3410109140"" (skosimp* t)"" (prop)"1" (inst?) nil nil )"2" (skosimp*)"2" (inst + "z!1+j!1" )"1" (inst?) (("1" (assert ) nil nil )) nil )"2" (inst?) nil nil ))nil ))nil ))nil ))nil )"T_high" product nil )"int" integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"T" product nil )"int" product nil )"(total_order?[real])" nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, 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 )"[int -> boolean]" product nil )nil product nil )"bool" reals nil )nil product nil ))nil )nil 3410108130 ("" (subtype-tcc) nil nil ) nil nil ))nil 3410108130 ("" (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 )"int" integers nil ))nil ))nil 3410108147"" (skolem 1 ("F" _ _ "z" ))"" (rewrite "high_low_rewrite" )"1" (hide 2)"1" (skosimp*)"1" (prop)"1" (expand "product" ) (("1" (assert ) nil nil )) nil )"2" (induct "n" 2)"1" (skosimp*)"1" (rewrite "product_eq_arg" )"1" (rewrite "product_eq_arg" )"1" (hide -1 2)"1" (use "T_pred_lem" ) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (hide 2)"2" (inst?)"2" (use "T_pred_lem" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (expand "product" +) (("2" (assert ) nil nil ))nil ))nil ))nil )"3" (skosimp*) nil nil )"4" (hide-all-but 1)"4" (skosimp* t)"4" (typepred "high!1" )"4" (prop)"1" (inst + "high!1" ) nil nil )"2" (skosimp*)"2" (inst + "j!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (hide -1 2 3)"5" (skosimp* t)"5" (typepred "high!1" )"5" (prop)"1" (inst + "high!1+z" )"1" (assert ) nil nil ) ("2" (inst?) nil nil ))nil )"2" (skosimp*)"2" (inst + "j!1+z" )"1" (assert ) nil nil )"2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" (hide -1 2 3)"6" (skosimp* t)"6" (assert )"6" (typepred "low!1" )"6" (prop)"1" (inst?) nil nil )"2" (skosimp*)"2" (inst + "j!1+z" )"1" (assert ) nil nil )"2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"7" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (skosimp*) nil nil )"3" (hide 2)"3" (skosimp* t)"3" (hide -1 -4)"3" (assert )"3" (prop)"1" (typepred "high!1" )"1" (prop)"1" (assert ) (("1" (inst?) nil nil )) nil )"2" (skosimp*)"2" (inst + "j!1+z" )"1" (assert ) nil nil ) ("2" (inst?) nil nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (typepred "high!1" )"2" (prop)"1" (inst?) nil nil )"2" (skosimp*)"2" (inst + "j!2+z" )"1" (assert ) nil nil )"2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide 2)"4" (skosimp* t)"4" (hide -1)"4" (inst?)"4" (assert )"4" (skosimp*)"4" (reveal -1)"4" (inst + "j!1+z" )"1" (assert ) nil nil ) ("2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"int" integers nil )nil product 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 )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" product nil )nil product nil )"bool" reals nil )nil product nil )nil product nil )nil defined_types nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )"int" product nil )AND const-decl "[bool, bool -> bool]" booleans nil )"T_low" product nil )"T_high" product nil )nil integers nil )"int" product nil )nil subrange_inductions nil )"(total_order?[real])" nil )"bool" reals nil )nil product nil )"(total_order?[real])" nil )nil product nil )NOT const-decl "[bool -> bool]" booleans nil )"T" product nil )"T" product nil )"(strict_total_order?[real])" real_props nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"(strict_total_order?[real])" real_props nil )"T_high" product nil )"T" product nil )"T" product nil )"T_low" product nil )"T" product nil ))nil ))nil 3410111446 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, 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 )"[int -> boolean]" product nil )nil product nil )"bool" reals nil )nil product nil )nil product nil )"int" integers nil ))nil ))nil 3410111446 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, 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 )"[int -> boolean]" product nil )nil product nil )"bool" reals nil )nil product nil )nil product nil )"int" integers nil ))nil ))nil 3410111473"" (skolem 1 ("F" _ _ "z" ))"" (rewrite "high_low_rewrite" )"1" (hide 2)"1" (skosimp*)"1" (prop)"1" (expand "product" ) (("1" (assert ) nil nil )) nil )"2" (induct "n" 2)"1" (flatten)"1" (rewrite "product_eq_arg" )"1" (rewrite "product_eq_arg" )"1" (assert ) nil nil )"2" (hide -1 -2 2)"2" (use "T_pred_lem" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (expand "product" +)"2" (assert )"2" (split -2)"1" (assert ) nil nil )"2" (hide 2)"2" (lemma "connected_domain" )"2" (inst - "low!1+z" "1+k!1+z" "k!1+z" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (skosimp* t)"3" (typepred "high!1" )"3" (inst + "high!1" )"3" (assert )"3" (skosimp*)"3" (assert )"3" (use "T_pred_lem" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide-all-but 1) (("4" (skosimp*) nil nil )) nil )"5" (hide-all-but 1) (("5" (skosimp*) nil nil )) nil )"6" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2) (("2" (skosimp*) nil nil )) nil )"3" (hide 2) (("3" (skosimp*) nil nil )) nil ))nil ))nil )"int" integers nil )nil product 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 )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" product nil )nil product nil )"bool" reals nil )nil product nil )nil product nil )nil defined_types nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )"int" product nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"T_low" product nil )"T_high" product nil )nil integers nil )"int" product nil )nil subrange_inductions nil )"(total_order?[real])" nil )"bool" reals nil )nil product nil )"(total_order?[real])" nil )nil product nil )nil integers nil )nil product nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3410109740"" (skolem 1 ("F" "G" _ _))"" (rewrite "high_low_rewrite" )"" (hide 2)"" (skosimp*)"" (prop)"1" (expand "product" ) (("1" (assert ) nil nil )) nil )"2" (induct "n" 2)"1" (rewrite "product_eq_arg" )"1" (rewrite "product_eq_arg" )"1" (rewrite "product_eq_arg" ) nil nil )) nil )"2" (use "T_pred_lem" ) (("2" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (expand "product" +)"2" (replace -2 * rl) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (skosimp* t)"3" (typepred "high!1" )"3" (inst + "high!1" )"3" (assert )"3" (skosimp*)"3" (use "T_pred_lem" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil product 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 )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" product nil )nil product nil )"bool" reals nil )nil product nil )nil product nil )nil defined_types nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" product nil )AND const-decl "[bool, bool -> bool]" booleans nil )"T_low" product nil )"T_high" product nil )nil integers nil )nil subrange_inductions nil )"(total_order?[real])" nil )"bool" reals nil )nil product nil )"(total_order?[real])" nil )nil product nil )"int" integers nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3255975799"" (skolem 1 ("F" "h" _ "l" _))"" (rewrite "high_low_rewrite" )"1" (hide 2)"1" (skosimp*)"1" (prop)"1" (expand "product" ) (("1" (assert ) nil nil )) nil )"2" (induct "n" 2)"1" (rewrite "product_eq_arg" )"1" (rewrite "product_eq_arg" )"1" (expand "restrict" )"1" (flatten) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (hide 2)"2" (use "T_pred_lem" ) (("2" (assert ) nil nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (expand "product" +)"2" (rewrite "restrict" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (skosimp*)"3" (inst + "h" ) (("3" (assert ) nil nil )) nil )) nil )"4" (skosimp*)"4" (inst + "l" ) (("4" (assert ) nil nil )) nil )) nil )"5" (hide-all-but 1)"5" (skosimp* t)"5" (hide -3 -4)"5" (inst + "n!2" )"1" (assert ) nil nil )"2" (use "T_pred_lem" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"6" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (inst + "h" ) (("2" (assert ) nil nil )) nil )) nil ))nil )"3" (hide 2)"3" (skosimp*)"3" (inst + "l" ) (("3" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil product 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 )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" product nil )nil product nil )"bool" reals nil )nil product nil )nil product nil )nil defined_types nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )"int" product nil )"[T -> int]" product nil )"T_low" product nil )"T_high" product nil )nil integers nil )"T" product nil )"T" product nil )nil subrange_inductions nil )nil product nil )nil product nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3255975799"" (skosimp*)"" (case "high!1 < low!1" )"1" (expand "product" ) (("1" (assert ) nil nil )) nil )"2" (rewrite "product_restrict" )"1" (use "T_pred_lem" ) (("1" (assert ) nil nil )) nil )"2" (use "T_pred_lem" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )nil product nil )nil product nil )"bool" reals nil )nil product nil )"[int -> boolean]" product nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"(strict_total_order?[real])" real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"(strict_total_order?[real])" real_props nil )"int" product nil )nil product nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil product nil ))nil ))nil 3255975799"" (skosimp*)"" (case "high!1 < low!1" )"1" (expand "product" ) (("1" (assert ) nil nil )) nil )"2" (lemma "product_restrict" )"2" (inst?)"2" (inst -1 "high!1" "low!1" )"1" (assert )"1" (replace *)"1" (hide -1 -2)"1" (lemma "product_restrict" )"1" "G!1" "high!1" "high!1" "low!1" "low!1" )"1" (assert ) nil nil )"2" (use "T_pred_lem" ) (("2" (assert ) nil nil ))nil )"3" (use "T_pred_lem" ) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (use "T_pred_lem" ) (("2" (assert ) nil nil )) nil )"3" (use "T_pred_lem" ) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil product nil )nil product nil )"bool" reals nil )nil product nil )"[int -> boolean]" product nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"(strict_total_order?[real])" real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"(strict_total_order?[real])" real_props nil )"int" product nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil product nil )"T_low" product nil )"T_high" product nil )nil product nil ))nil ))nil 3255975799"" (skosimp*)"" (lemma "product_restrict_eq" )"" (inst?)"" (assert )"" (hide 2)"" (expand "restrict" )"" (apply-extensionality 1 :hide? t)"" (lift-if)"" (ground) (("" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil product nil )"[T -> int]" product nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil product nil )nil product nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil product nil )"[int -> boolean]" product 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 3255975799"" (skosimp*)"" (case "i!1 = low!1" )"1" (rewrite "product_first" )"1" (lemma "product_first" )"1" (inst -1 "G!1" "high!1" "low!1" )"1" (assert )"1" (assert )"1" (replace -1)"1" (replace -5)"1" (hide -1 -5)"1" (assert )"1" (replace -1)"1" (assert )"1" "a!1 * (G!1(low!1) * product(1 + low!1, high!1, G!1)) / G!1(low!1) = ") "1" "1" "product_eq" )"1" "1" "G!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case-replace "i!1 = high!1" )"1" (rewrite "product_last" )"1" (lemma "product_last" )"1" (inst -1 "G!1" "high!1" "low!1" )"1" (assert )"1" (replace -1)"1" (hide -1)"1" (assert )"1" (replace -4)"1" (assert )"1" "a!1 * (product(low!1, high!1 - 1, G!1) * G!1(high!1)) / G!1(high!1) = ") "1" (hide -1)"1" "product_eq" )"1" "1" "G!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 3) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "product_split" )"2" (inst?)"2" (inst -1 "i!1" )"2" (assert )"2" (replace -1)"2" (hide -1)"2" (lemma "product_split" )"2" (inst -1 "G!1" "high!1" "low!1" "i!1" )"2" (assert )"2" (replace -1)"2" (hide -1)"2" "product_last" )"2" "F!1" "i!1" "low!1" )"2" "G!1" "i!1" "low!1" )"2" assert )"2" replace -1)"2" "2" replace -1)"2" "2" replace -3)"2" "2" "2" "product(low!1, i!1 - 1, G!1 WITH [i!1 := a!1]) = product(low!1, i!1 - 1, G!1)" )"1" "1" assert )"1" " a!1 * ") "1" "1" "product_eq" )"1" "1" "G!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "product_eq" )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 product nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil product nil )"[int -> boolean]" product 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 )"rat" rationals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" product nil )"[numfield, numfield -> numfield]" number_fields nil )nil product nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"int" integers nil )nil product nil )nil product nil )nil product nil )nil product nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil ))nil 3255975799"" (skolem 1 ("F" _ _))"" (rewrite "high_low_rewrite" )"" (hide 2)"" (skosimp*)"" (prop)"1" (expand "product" ) (("1" (assert ) nil nil )) nil )"2" (induct "n" 2)"1" (rewrite "product_eq_arg" )"1" (skosimp*) (("1" (inst?) nil nil )) nil )"2" (use "T_pred_lem" ) (("2" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (expand "product" +)"2" (prop)"2" (inst?) (("2" (grind-reals) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (skosimp* t)"3" (use "T_pred_lem" ) (("3" (assert ) nil nil ))nil ))nil ))nil )"4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil product 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 )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" product nil )nil product nil )"bool" reals nil )nil product nil )nil product nil )nil defined_types nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"int" product nil )"[T -> int]" product nil )nil integers nil )"T_high" product nil )"T_low" product nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil subrange_inductions nil )nil product nil )"(total_order?[real])" nil )nil product nil )nil real_props nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3410177295"" (skosimp*)"" (lemma "product_nonneg" )"" (inst?)"" (assert ) (("" (skosimp*) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )nil product nil )"(total_order?[real])" nil )nil product nil )nil product nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil product nil )"[int -> boolean]" product 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 3410176926"" (skolem 1 ("FF" _ _))"" (rewrite "high_low_rewrite" )"" (hide 2)"" (skosimp*)"" (prop)"1" (expand "product" ) (("1" (assert ) nil nil )) nil )"2" (induct "n" 2)"1" (rewrite "product_eq_arg" )"1" (use "T_pred_lem" ) (("1" (assert ) nil nil )) nil )"2" (hide 2)"2" (use "T_pred_lem" ) (("2" (assert ) nil nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (expand "product" +)"2" (typepred "FF(1 + k!1)" )"2" (assert ) (("2" (grind-reals) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (skosimp* t)"3" (use "T_pred_lem" ) (("3" (assert ) nil nil ))nil ))nil ))nil )"4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil product 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 )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" product nil )nil product nil )"bool" reals nil )nil product nil )nil product nil )nil defined_types nil )"bool" reals nil )"int" product nil )"bool" reals nil )nil integers nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"T_low" product nil )"T_high" product nil )nil integers nil )nil subrange_inductions nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil product nil )"nat" product nil )nil product nil )"int" integers nil )NOT const-decl "[bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"nonneg_int" nil )"(divides(n))" divides nil )"(divides(m))" divides nil ))nil )))
Messung V0.5 in Prozent C=99 H=99 G=98
¤ Dauer der Verarbeitung: 0.58 Sekunden
(vorverarbeitet am 2026-05-05)
¤ *© Formatika GbR, Deutschland
2026-05-26
