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 )"real" reals nil )"posint" nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )"real" 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 )"real" reals nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" 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 )"real" reals nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" 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 )"real" reals 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 )"real" reals nil )"nzreal" nil )nil product nil ))nil 3410104588"" (skosimp*)"" (expand "product" )"" (expand "product" ) (("" (propax) nil nil )) nil )) nil ))nil )"real" 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 )"real" reals 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 )"real" 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 )"(total_order?[real])" nil )"real" reals 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 )"real" product nil )"(total_order?[real])" nil )"real" reals 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 )"real" product nil )"boolean" notequal nil )nil reals 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 )"(total_order?[real])" nil )"real" exponentiation nil )"nzreal" exponentiation nil )nil product nil )"real" reals nil )"nzreal" nil )"odd_int" integers nil )nil exponentiation nil )"odd_int" integersnil )nil exponentiation nil )"(strict_total_order?[real])" real_props 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 )"real" reals nil )"(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 )OR const-decl "[bool, bool -> bool]" booleans 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 )"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 )"real" reals 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 )"real" 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 )"int" integers nil )"T_low" product nil )"T_high" product nil )nil integers nil )"real" product nil )nil subrange_inductions nil )"(total_order?[real])" nil )nil product nil )"(total_order?[real])" nil )nil exponentiation nil )nil product nil )nil reals nil )"odd_int" integers nil )nil exponentiation nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3412957398"" (skeep)"" (skosimp*)"" (typepred "n!1" )"" (lemma "T_pred_lem" )"" (inst - "high" "low" "n!1" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )nil product nil )"(total_order?[real])" 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 )"bool" 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 )nil product nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil product nil )nil integers nil ))nil ))nil 3412957679"" (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" -3)"2" (mult-cases -3)"1" (inst?) nil nil )"2" (skosimp*)"2" (typepred "n!1" ) (("2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*)"3" (hide 3)"3" (typepred "n!2" )"3" (typepred "n!1" )"3" (lemma "T_pred_lem" )"3" (assert )"3" (inst - "high!1" "low!1" "n!2" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (skosimp*)"4" (typepred "n!1" )"4" (lemma "T_pred_lem" )"4" (inst - "high!1" "low!1" "n!1" )"4" (assert ) nil nil )) nil ))nil ))nil ))nil )"5" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (typepred "n!1" )"2" (lemma "T_pred_lem" )"2" (inst - "high!1" "low!1" "n!1" )"2" (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 )"[T, T -> boolean]" equalities nil )"real" product nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"T_low" product nil )"T_high" product nil )"[T -> real]" product 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 )nil real_props nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )NOT const-decl "[bool -> bool]" booleans nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil ))nil 3618849229"" (skeep)"" (typepred "low" )"" (typepred "high" )"" (typepred "n" )"" (lemma "connected_domain" )"" (ground)"1" (inst - "low" "high" "n" ) (("1" (assert ) nil nil ))nil )"2" (skosimp*)"2" (inst - "j!1" "high" "n" )"2" (assert ) nil nil )) nil ))nil )"3" (skosimp*)"3" (inst - "low" "j!1" "n" ) (("3" (assert ) nil nil ))nil ))nil )"4" (skosimp*)"4" (inst - "j!1" "j!2" "n" ) (("4" (assert ) 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 integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )nil integers nil )nil product nil )nil product nil ))nil ))nil 3618849033"" (skeep)"" (lemma "product_eq_0" )"" (inst?)"" (split 1)"1" (propax) nil nil )"2" (flatten)"2" (hide -2)"2" (skeep -1)"2" case "FORALL (k:nat): n+k<=high IMPLIES product(low,n+k,F)=0" )"1" (inst - "high-n" ) (("1" (assert ) nil nil )) nil )"2" (induct "k" )"1" (assert )"1" (expand "product" 1 1)"1" (assert ) nil nil )) nil ))nil )"2" (skeep)"2" (assert )"2" (expand "product" + 1)"2" (assert ) nil nil )) nil ))nil ))nil )"3" (assert )"3" (lemma "connected_domain" )"3" (skeep)"3" (inst - "low" "high" "k+n" )"1" (assert ) nil nil )"2" (assert )"2" "high" )"2" assert )"2" "2" "j!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (typepred "high" )"3" "1" (inst + "high" ) nil nil )"2" assert )"2" "2" "j!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*)"3" (typepred "high" )"3" (split -1)"1" (inst + "high" ) nil nil )"2" (skosimp*)"2" (inst + "j!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil product nil )"real" product nil )"[T, T -> boolean]" equalities nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )"int" integers nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )nil integers nil )nil product nil )"posint" nil )"posint" nil )"real" reals nil )nil naturalnumbers nil )nil defined_types nil )"subrange(low, high)" product nil )"T_high" product nil )"T_low" 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 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" (grind-reals) 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 )"real" product nil )"T_low" product nil )"T_high" product nil )"[T -> real]" product nil )nil subrange_inductions nil )nil product nil )"(total_order?[real])" nil )nil product nil )nil real_props nil )"real" reals 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 )"(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" (grind-reals) 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 )"real" product nil )"T_low" product nil )"T_high" product nil )"[T -> real]" 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 )"real" reals 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 ))nil ))nil 3412701767"" (skolem 1 ("F" _ _))"" (rewrite "high_low_rewrite" )"1" (hide 2)"1" (skosimp*)"1" (prop)"1" (expand "product" )"1" (lift-if) (("1" (ground) nil nil )) nil )) nil )"2" (induct "n" 2)"1" (skosimp*)"1" (rewrite "product_eq_arg" )"1" (inst?) (("1" (assert ) nil 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" (prop)"1" (expand "product" -3)"1" (mult-cases -3)"1" (inst?) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (skosimp*)"2" (inst?) (("2" (assert ) 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 )"boolean" notequal nil )"real" product nil )"T_low" product nil )"T_high" product nil )"[T -> real]" product nil )nil subrange_inductions nil )"(total_order?[real])" nil )"bool" reals nil )nil product nil )"(total_order?[real])" nil )nil product nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_props nil )"int" integers nil )NOT const-decl "[bool -> bool]" booleans nil )"real" reals nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil ))nil )nil 3412701748 ("" (postpone) nil nil ) nil shostak))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 )"real" 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 )"real" reals nil )NOT const-decl "[bool -> bool]" booleans nil )"T" product nil )"T" product nil )"(strict_total_order?[real])" real_props 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 )"real" 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 )"real" reals nil )nil integers nil )nil product nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props 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 )"real" reals 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 )"real" 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 3549725667"" (skeep)"" (lemma "product_prod" )"" (inst - "F" "G" "high" "low" ) (("" (assert ) nil nil )) nil ))nil ))nil )nil product nil )"real" 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 3536928586 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3536928676"" (skolem 1 ("F" "G" _ _))"" (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" (expand "product" )"1" (expand "product" )"1" (grind-reals) nil nil )) nil ))nil ))nil )"2" (skosimp*)"2" (split -2)"1" (expand "product" +) (("1" (assert ) nil nil ))nil )"2" (propax) nil nil ))nil ))nil )"3" (hide 2 3) (("3" (subtype-tcc) nil nil )) nil )"4" (hide 3)"4" (skeep :preds? t)"4" (use "T_pred_lem" ) (("4" (assert ) nil nil ))nil ))nil ))nil )"5" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2) (("2" (subtype-tcc) nil nil )) nil ))nil ))nil )"real" reals 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 )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"real" product nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"T_low" product nil )"T_high" product nil )nil integers nil )"[T -> real]" product nil )nil subrange_inductions nil )"(total_order?[real])" nil )"bool" reals nil )"int" integers nil )"(total_order?[real])" nil )nil product nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )NOT const-decl "[bool -> bool]" booleans 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 )"real" product nil )"[T -> real]" 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 )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(total_order?[real])" 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 )"(strict_total_order?[real])" real_props nil )"real" 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 )"(strict_total_order?[real])" real_props nil )"real" 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 -> real]" 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 3523363924"" (skeep)"" (lemma "product_eq" )"" (inst - "F" "LAMBDA (zzp:T): 1" "high" "low" )"" (assert )"" (replace -2)"" case "FORALL (ih:nat): T_high?(low+ih) IMPLIES product(low,low+ih,LAMBDA (zzp:T): 1) = 1" )"1" (case "high>=low" )"1" (inst - "high-low" )"1" (assert )"1" (typepred "high" )"1" (split -1)"1" (inst + "high" ) (("1" (assert ) nil nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (expand "product" +) (("2" (assert ) nil nil ))nil ))nil )"2" (hide-all-but 1)"2" case "FORALL (k:nat): FORALL (ih: nat): ih<=k IMPLIES LAMBDA (zzp: T): 1) = 1)") "1" (skeep)"1" (inst - "ih" )"1" (inst - "ih" ) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (hide 2)"2" (induct "k" )"1" (skeep)"1" (case "ih = 0" )"1" (replace -1)"1" (hide -1)"1" "1" assert )"1" expand "product" +)"1" expand "product" +)"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (skolem 1 "k" )"2" (flatten)"2" (skeep)"2" (case "ih /= k+1" )"1" "ih" )"1" (assert ) nil nil ))nil )"2" "2" replace -1)"2" "2" assert )"2" expand "product" +)"2" "k" )"2" assert )"2" "2" "j" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2) (("3" (skeep) nil nil )) nil ))nil ))nil )"3" (hide 2) (("3" (skeep) nil nil )) nil ))nil ))nil )"3" (hide 2) (("3" (skeep) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil product nil )"real" product nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"T_high" product nil )"T_low" product nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil defined_types nil )nil naturalnumbers nil )"posint" nil )"boolean" notequal nil )"posint" nil )"real" 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 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 )"real" reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" product nil )"[numfield, numfield -> numfield]" number_fields nil )nil product nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"real" reals 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 )"real" product nil )"[T -> real]" 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 )"real" reals 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 )"(strict_total_order?[real])" real_props nil ))nil ))nil 3410182448"" (skosimp*)"" (rewrite "product_nonneg" )"" (skosimp*) (("" (assert ) 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 )"[int -> boolean]" product nil )nil product nil )nil booleans nil )"bool" reals nil )nil real_types nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil product nil )nil product nil )"(total_order?[real])" nil ))nil ))nil 3410182448"" (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" (assert ) nil nil )"2" (use "T_pred_lem" ) (("2" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (expand "product" +)"2" (typepred "FF(1 + k!1)" )"2" (grind-reals) 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 )"real" product nil )"bool" reals nil )nil real_types nil )nil real_types 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 )"(total_order?[real])" nil )"nnreal" 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 )"nnreal" nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3410183251"" (auto-rewrite-theory "integers" )"" (auto-rewrite-theory "rationals" )"" (skosimp*)"" case "(FORALL (rng: nat): T_pred(low!1+rng) IMPLIES (rational_pred(product(low!1, low!1+rng, Fnat!1)) AND integer_pred(product(low!1, low!1+rng, Fnat!1))) AND product(low!1, low!1+rng, Fnat!1) >= 0)" )"1" (inst -1 "high!1-low!1" )"1" (assert )"1" (split -1)"1" (propax) nil nil )"2" (use "T_pred_lem" )"2" (assert )"2" (expand "product" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "product" ) (("2" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (induct "rng" )"1" (skosimp*)"1" (rewrite "product_eq_arg" )"1" (assert ) nil nil )) nil ))nil )"2" (skosimp*)"2" (expand "product" 1)"2" (split -1)"1" (flatten) (("1" (assert ) nil nil )) nil )"2" (hide 2)"2" (lemma "T_pred_lem" )"2" (inst - "low!1+j!1" "low!1" "low!1+j!1" )"1" (assert ) nil nil )"2" (assert )"2" (inst + "1+j!1+low!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*) nil nil ) ("4" (skosimp*) nil nil )"5" (skosimp*) nil nil ) ("6" (skosimp*) nil nil )"7" (skosimp*) nil nil ) ("8" (skosimp*) nil nil )"9" (skosimp*) nil nil ) ("10" (skosimp*) nil nil )"11" (skosimp*) nil nil ))nil ))nil )"3" (skosimp*) nil nil ) ("4" (skosimp*) nil nil )"5" (skosimp*) nil nil ))nil ))nil ))nil ))nil )"real" product nil )nil product nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil product nil )"bool" reals nil )nil product nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[int -> boolean]" product nil )"[bool, bool -> bool]" booleans 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 )"nnreal" product nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil product nil )"(total_order?[real])" nil )"T_low" product nil )"T_high" product nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"(total_order?[real])" nil )"[T -> nat]" product nil )nil defined_types nil )nil naturalnumbers nil )nil product nil )"posint" nil )"nnreal" nil )"nat" product nil )"posint" nil )nil integers nil )nil rationals nil ))nil )nil 3410182448"" (skosimp*)"" (lemma "product_nonneg" )"" (inst?)"" (assert )"" (split -1)"1" (assert )"1" (auto-rewrite-theory "integers" )"1" (postpone) nil nil )) nil ))nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )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" (mult-ineq -1 -3)"2" (assert ) nil 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 )"real" 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 )nil product nil )"nat" product nil )"posreal" 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 )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"(divides(n))" divides nil )"(divides(m))" divides nil ))nil ))nil 3536959316"" (skeep)"" (case "low > high" )"1" (grind) nil nil )"2" (lemma "for_induction" )"2" (expand "product_it" )"2" (inst?)"1" "LAMBDA(k:upto(1-low+high),a:real): a = product(low,low+k-1,F)" )"1" (split -1)"1" (assert ) nil nil )"2" (expand "product" ) (("2" (propax) nil nil )) nil )"3" (hide 3)"3" (skeep)"3" (expand "product" 1) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 3)"2" (skeep)"2" (lemma "T_pred_lem" )"2" (inst -1 "high" "low" "k-1+low" )"2" (assert )"2" (inst? 3)"1" (assert ) nil nil )"2" (lemma "T_pred_lem" )"2" (inst -1 "high" "low" "low" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (lemma "T_pred_lem" )"2" (inst -1 "high" "low" "i" )"2" (assert ) nil nil )) nil ))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 )"(strict_total_order?[real])" real_props nil )"real" reals nil )"real" product nil )"real" product nil )"T" for_iterate "structures/" )"{t: T | t = for_def(i, upto, a, ext2int(upfrom, upto, f))}" "structures/" )"int" integers nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil defined_types nil )"(total_order?[real])" nil )nil product nil )"[numfield, numfield -> numfield]" number_fields nil )nil for_iterate "structures/" )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"T_low" product nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"T_high" product nil )"bool" reals nil )"(total_order?[real])" nil )"int" integers nil )nil for_iterate "structures/" ))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.131Bemerkung:
(vorverarbeitet am 2026-04-30)
¤ *Bot Zugriff
2026-05-26
