sigma.prf
Interaktion und
(sigma (T_pred_lem 0nil 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" sigma nil )"T_high" sigma nil )nil integers nil )"(total_order?[real])" nil )nil sigma 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]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma 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" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )"[int -> boolean]" sigma nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil sigma nil )nil sigma nil ))nil ))nil 3352228842"" (skosimp*)"" (inst?)"" (prop) (("" (inst?) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma nil )"(total_order?[real])" nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"T_high" sigma nil )"T_low" sigma nil )"(strict_total_order?[real])" real_props nil ))nil 3403452046"" (skosimp* t)"" (assert )"" (skosimp*)"" (typepred "j!1" )"" (lemma "connected_domain" )"" (inst - "low!1" "j!1" "high!1" )"1" (assert ) nil nil )"2" (prop)"2" (skosimp*)"2" (lemma "connected_domain" )"2" (assert )"2" (inst - "j!2" "j!1" "low!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )"T_low" sigma nil )nil integers nil )"(total_order?[real])" nil )nil sigma 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]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma nil ))nil )nil 3255975799"" (skosimp*)"" (use "T_pred_lem" ) (("" (assert ) nil nil )) nil )) nil )nil nil ))nil 3403452083"" (skosimp*)"" (typepred "high!1" )"" (assert )"" (prop)"1" (inst + "high!1" ) (("1" (assert ) nil nil )) nil )"2" (skosimp*)"2" (typepred "j!1" )"2" (inst + "j!1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma nil )"bool" reals nil )nil sigma nil )"[int -> boolean]" sigma nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )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_high" sigma nil )"(strict_total_order?[real])" real_props nil )"int" integersnil ))nil )nil 3255975799"" (skosimp* t)"" (assert )"" (skosimp*)"" (typepred "j!1" )"" (lemma "connected_domain" )"" (inst - "low!1" "j!1" "high!1" )"1" (assert ) nil nil )"2" (prop)"2" (skosimp*)"2" (lemma "connected_domain" )"2" (assert )"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 3255975799"" (skosimp*) (("" (grind) nil nil )) nil )"{n: nonneg_real | n >= m AND n >= -m}" nil )"int" integers nil )"{j: nonneg_int | j >= i}" real_defs nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"int" integersnil )"int" integersnil ))nil ))nil 3403451849"" (skosimp*)"" (typepred "low!1" )"" (assert )"" (skosimp*)"" (replace -2)"" (typepred "j!1" )"" (typepred "high!1" )"" (assert )"" (skosimp*)"" (lemma "connected_domain" )"" (inst - "j!1" "j!2" "low!1" )"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma nil )"bool" reals nil )nil sigma nil )"[int -> boolean]" sigma nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )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 sigma nil )nil integers nil )nil sigma nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3352522445"" (skosimp*)"" (lift-if)"" (ground)"1" (expand "sigma" ) (("1" (propax) nil nil )) nil )"2" (expand "sigma" )"2" (expand "sigma" ) (("2" (assert ) nil nil )) nil ))nil )"3" (expand "sigma" 2 1) (("3" (propax) nil nil )) nil ))nil ))nil ))nil )"real" sigma nil )"(strict_total_order?[real])" real_props nil )"int" integersnil )"real" realsnil ))nil 3403459500"" (skosimp*)"" case "FORALL (rng: nat): T_pred(low!1+rng) IMPLIES ") "1" (inst - "high!1-low!1" )"1" (assert )"1" (typepred "high!1" )"1" (assert )"1" (skosimp*)"1" (typepred "j!1" )"1" (typepred "low!1" )"1" (lemma "connected_domain" )"1" (inst - "low!1" "j!1" "high!1" )"1" assert )"1" expand "sigma" )"1" expand "sigma2" )"1" (propax) nil nil ))nil ))nil ))nil )"2" assert )"2" "2" "connected_domain" )"2" "j!2" "j!1" "low!1" )"2" assert )"2" expand "sigma" )"2" expand "sigma2" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "sigma" )"2" (expand "sigma2" ) (("2" (assert ) nil nil )) nil ))nil ))nil )"2" (hide 2)"2" (induct "rng" )"1" (assert )"1" (flatten)"1" (expand "sigma" )"1" (expand "sigma" )"1" (expand "sigma2" )"1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (assert )"2" (expand "sigma" 1)"2" (expand "sigma2" 1)"2" (assert )"2" (hide 2)"2" (typepred "low!1" )"2" "j!1" )"2" assert )"2" "1" "connected_domain" )"1" "low!1" "j!1+1+low!1" "j!1+low!1" )"1" (assert ) nil nil ))nil ))nil )"2" "2" "connected_domain" )"2" "j!2" "j!1+1+low!1" "j!1+low!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2) (("3" (skosimp*) nil nil )) nil ))nil ))nil )"3" (skosimp*) nil nil ))nil ))nil )"real" sigma nil )"real" sigma nil )nil sigma nil )"[T, T -> boolean]" equalities nil )nil sigma nil )"bool" reals nil )nil sigma nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" nil )nil number_fields nil )"[int -> boolean]" sigma nil )"[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )"int" integersnil )"(strict_total_order?[real])" real_props nil )nil sigma nil )"(total_order?[real])" nil )nil integers nil )NOT const-decl "[bool -> bool]" booleans nil )"T_low" sigma nil )"T_high" sigma nil )"[numfield, numfield -> numfield]" nil )"int" integersnil )"(total_order?[real])" nil )nil defined_types nil )nil naturalnumbers nil )"posint" nil )"posint" nil ))nil ))nil 3255975799"" (skosimp*)"" (inst + "low!1 + nn!1 + rng!1" ) (("" (assert ) nil nil ))nil ))nil )nil nil ))nil 3255975799"" (skosimp*)"" (inst + "low!1 + nn!1 + rng!1" ) (("" (assert ) nil nil ))nil ))nil )"int" integersnil )"nat" sigma nil )"nat" sigma nil )nil naturalnumbers nil )"bool" reals nil )"T_low" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )"[numfield, numfield -> numfield]" nil )nil number_fields nil )"[int -> boolean]" sigma nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )"(total_order?[real])" nil ))nil ))nil 3351939915"" (skosimp* t)"" (prop)"1" (assert )"1" (inst + "low!1" ) (("1" (assert ) nil nil )) nil ))nil )"2" (skosimp*)"2" (inst + "j!1" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"int" integersnil )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]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )"bool" reals nil )nil naturalnumbers nil ))nil ))nil 3255975799"" (induct "rng" )"1" (assert )"1" (expand "sigma" ) (("1" (propax) nil nil )) nil )) nil )"2" (skosimp*)"2" (expand "sigma" + (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" sigma nil )"nat" sigma nil )"nat" sigma nil )"T_low" sigma nil )"nat" sigma nil )"nat" sigma nil )nil sigma nil )"(total_order?[real])" nil )"posint" nil )"real" realsnil )"posint" nil )nil naturalnumbers nil )"real" sigma nil )nil sigma nil )"[T, T -> boolean]" equalities nil )nil defined_types nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" nil )"int" integersnil ))nil ))nil 3255975799"" (skosimp* t)"" (prop)"1" (inst + "high!1" ) nil nil )"2" (inst + "high!1" ) nil nil )"3" (skosimp*)"3" (inst + "j!1" ) (("3" (assert ) nil nil )) nil )) nil )"4" (skosimp*)"4" (inst + "j!2" ) (("4" (assert ) nil nil )) nil )) nil ))nil ))nil )"T_high" sigma nil )"(total_order?[real])" nil )"int" integersnil )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]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma nil ))nil ))nil 3351939915"" (skosimp* t)"" (assert )"" (prop)"1" (inst + "low!1" ) (("1" (assert ) nil nil )) nil )"2" (skosimp*)"2" (inst + "j!1" ) (("2" (assert ) nil nil )) nil ))nil )"3" (skosimp*)"3" (inst + "low!1" ) (("3" (assert ) nil nil )) nil ))nil )"4" (skosimp*)"4" (inst + "j!1" ) (("4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"int" integersnil )"int" integersnil )"(total_order?[real])" nil )"T_low" sigma 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]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma nil ))nil ))nil 3255975799"" (skosimp*)"" (case "high!1<low!1" )"1" (expand "sigma" ) (("1" (assert ) nil nil )) nil )"2" (case-replace "z!1=low!1-1" )"1" (assert )"1" (expand "sigma" ) (("1" (propax) nil nil )) nil ))nil )"2" (lemma "sigma_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 sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )"[int -> boolean]" sigma nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integersnil )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]" nil )nil booleans nil )nil numbers nil )"int" integersnil )"real" realsnil )"(strict_total_order?[real])" real_props nil )"int" integersnil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" sigma nil )nil sigma nil )nil sigma nil )nil naturalnumbers nil )"T_high" sigma nil )"T_low" sigma nil )"int" sigma nil )"bool" reals nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" nil )nil number_fields nil )"[T, T -> boolean]" equalities nil ))nil ))nil 3255975799"" (skosimp*)"" (lemma "sigma_split" )"" (inst?)"" (inst -1 "z!1" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil sigma nil )"(total_order?[real])" nil )"int" integersnil )"real" realsnil )"int" integersnil )nil sigma nil )nil sigma nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil sigma nil )"[int -> boolean]" sigma nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil ))nil ))nil 3255975799"" (skosimp*)"" (lemma "sigma_diff" )"" (inst -1 "F!1" "high!1" "low!1" "z!1" )"" (assert ) nil nil )) nil ))nil ))nil )nil sigma nil )"int" integersnil )"real" reals nil )"real" realsnil )"int" integersnil )"(total_order?[real])" nil )nil sigma nil )nil sigma nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil sigma nil )"[int -> boolean]" sigma nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil ))nil ))nil 3255975799"" (skosimp*)"" (expand "sigma" )"" (expand "sigma" ) (("" (propax) nil nil )) nil )) nil ))nil )"real" sigma nil )) nil ))nil 3255975799"" (skosimp*)"" (use "T_pred_lem" ) (("" (assert ) nil nil )) nil )) nil )nil sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )"[int -> boolean]" sigma nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )nil sigma nil )"(total_order?[real])" nil )"(total_order?[real])" nil ))nil ))nil 3352113941"" (skosimp* t)"" (prop)"1" (inst + "low!1" ) (("1" (assert ) nil nil )) nil )"2" (skosimp*)"2" (inst + "j!1" ) (("2" (assert ) nil nil )) nil )) nil )"3" (inst + "low!1" ) (("3" (assert ) nil nil )) nil )"4" (skosimp*)"4" (inst + "j!1" ) (("4" (assert ) nil nil )) nil )) nil ))nil ))nil )"(total_order?[real])" nil )"int" integersnil )"(total_order?[real])" nil )"T_low" sigma 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]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma nil ))nil ))nil 3255975799"" (skosimp*)"" (lemma "sigma_split" )"" (inst?)"" (inst -1 "low!1" )"" (rewrite "sigma_eq_arg" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )nil sigma nil )"int" integersnil )"(total_order?[real])" nil )"int" integersnil )"real" realsnil )"(total_order?[real])" nil )nil sigma nil )nil sigma nil )nil sigma nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil sigma nil )"[int -> boolean]" sigma nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil ))nil ))nil 3351941334"" (skosimp* t)"" (prop)"1" (inst + "high!1" ) (("1" (assert ) nil nil )) nil )"2" (skosimp*)"2" (inst + "high!1" ) (("2" (assert ) nil nil )) nil ))nil )"3" (skosimp*)"3" (inst + "j!1" ) (("3" (assert ) nil nil )) nil )) nil )"4" (skosimp*)"4" (inst + "j!2" ) (("4" (assert ) nil nil )) nil )) nil ))nil ))nil )"(total_order?[real])" nil )"int" integersnil )"(total_order?[real])" nil )"T_high" sigma 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]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma nil ))nil )nil 3255975799"" (skosimp*)"" (typepred "high!1" )"" (skosimp*)"" (inst + "j!1" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil nil ))nil 3351939915"" (skosimp*)"" (use "T_pred_lem" ) (("" (assert ) nil nil )) nil )) nil )nil sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )"[int -> boolean]" sigma nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )nil sigma nil )"(total_order?[real])" nil )"(total_order?[real])" nil ))nil ))nil 3255975799"" (skosimp*)"" (rewrite "sigma" )"" (assert )"" (lift-if)"" (ground)"" (expand "sigma" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"real" sigma nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" realsnil )"int" integersnil ))nil ))nil 3256039673"" (skosimp* t)"" (prop)"1" (inst + "high!1" ) (("1" (assert ) nil nil )) nil )"2" (skosimp*)"2" (inst + "high!1" ) (("2" (assert ) nil nil )) nil ))nil )"3" (skosimp*)"3" (inst + "j!1" ) (("3" (assert ) nil nil )) nil )) nil )"4" (skosimp*)"4" (inst + "j!2" ) (("4" (assert ) nil nil )) nil )) nil ))nil ))nil )"(total_order?[real])" nil )"int" integersnil )"(total_order?[real])" nil )"T_high" sigma 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]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma nil ))nil 3256039673"" (skosimp*)"" (inst + "i!1" ) (("" (assert ) nil nil )) nil )) nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"[int -> boolean]" sigma nil )nil sigma nil )"(total_order?[real])" nil )"int" integersnil )"(total_order?[real])" nil ))nil 3256032001"" (skosimp*)"" (lemma "sigma_split" )"" (inst?)"" (inst -1 "i!1" )"" (assert )"" (rewrite "sigma_rew" -)"" (assert )"" (replace -1)"" (hide -1)"" (assert )"" (expand "sigma" 1 1)"" "" "" expand "sigma" )"" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma nil )nil sigma nil )"(strict_total_order?[real])" real_props nil )"real" sigma nil )"(total_order?[real])" nil )"real" realsnil )"int" integersnil )"int" integersnil )"(total_order?[real])" nil )nil sigma nil )nil sigma nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil sigma nil )"[int -> boolean]" sigma nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil ))nil 3255975799"" (skolem 1 (_ _ x))"" (rewrite "high_low_rewrite" )"" (hide 2)"" (skosimp*)"" (prop)"1" (expand "sigma" ) (("1" (assert ) nil nil )) nil )"2" (induct "n" 2)"1" (rewrite "sigma_eq_arg" )"1" (assert ) nil nil )"2" (use "T_pred_lem" ) (("2" (assert ) nil nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (expand "sigma" +)"2" (assert ) 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 )nil sigma nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma nil )nil defined_types nil )"[T, T -> boolean]" equalities nil )"real" sigma nil )nil number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" reals nil )"[numfield, numfield -> numfield]" nil )"[numfield, numfield -> numfield]" nil )"[numfield, numfield -> numfield]" nil )"real" realsnil )"real" realsnil )AND const-decl "[bool, bool -> bool]" booleans nil )"T_low" sigma nil )"T_high" sigma nil )nil integers nil )nil subrange_inductions nil )"(total_order?[real])" nil )nil sigma nil )"(total_order?[real])" nil )"real" realsnil )nil sigma nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3255975799"" (skosimp*) (("" (rewrite "sigma_const" ) nil nil )) nil )"(divides(m))" dividesnil )"(divides(n))" dividesnil )"even_int" nil )"(total_order?[real])" nil )nil sigma nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma nil ))nil ))nil 3255975799"" (skolem 1 ("F" "a" _ _))"" (rewrite "high_low_rewrite" )"" (hide 2)"" (skosimp*)"" (prop)"1" (expand "sigma" ) (("1" (assert ) nil nil )) nil )"2" (induct "n" 2)"1" (rewrite "sigma_eq_arg" )"1" (rewrite "sigma_eq_arg" ) nil nil )"2" (use "T_pred_lem" ) (("2" (assert ) nil nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (expand "sigma" +)"2" (assert ) 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 )"4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" realsnil )nil sigma nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma nil )nil defined_types nil )"[T, T -> boolean]" equalities nil )"real" sigma nil )nil number_fields nil )"[numfield, numfield -> numfield]" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"T_low" sigma nil )"T_high" sigma nil )nil integers nil )nil subrange_inductions nil )"(total_order?[real])" nil )"bool" reals nil )nil sigma nil )"(total_order?[real])" nil )nil sigma nil )"int" integersnil )"real" realsnil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3500821826"" (skeep)"" (lemma "sigma_scal" )"" (inst - "F" "a" "high" "low" ) (("" (assert ) nil nil ))nil ))nil ))nil )nil sigma nil )"real" realsnil )nil sigma nil )nil sigma nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil sigma nil )"[int -> boolean]" sigma nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil ))nil 3255975799"" (skolem 1 ("B" "F" _ _))"" (rewrite "high_low_rewrite" )"" (hide 2)"" (skosimp*)"" (prop)"1" (expand "sigma" ) (("1" (assert ) nil nil )) nil )"2" (induct "n" 2)"1" (skosimp*)"1" (rewrite "sigma_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" (expand "sigma" +)"2" (prop)"1" (inst?) (("1" (assert ) nil nil )) nil )"2" (skosimp*)"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*)"3" (hide-all-but (1 2))"3" (typepred "n!2" )"3" (assert )"3" (typepred "high!1" )"3" "1" (inst + "high!1" ) nil nil )"2" "2" "j!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"int" integersnil )"real" realsnil )nil sigma nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma 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]" nil )"bool" reals nil )"real" sigma nil )"[numfield, numfield -> numfield]" nil )"[numfield, numfield -> numfield]" nil )"real" realsnil )"T_low" sigma nil )"T_high" sigma nil )nil integers nil )"[T -> real]" sigma nil )"real" sigma nil )nil subrange_inductions nil )"(total_order?[real])" nil )nil sigma nil )nil sigma nil )"int" integersnil )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 )"real" realsnil ))nil ))nil 3255975799"" (skolem 1 ("F" _ _))"" (rewrite "high_low_rewrite" )"" (hide 2)"" (skosimp*)"" (prop)"1" (expand "sigma" )"1" (expand "abs" ) (("1" (assert ) nil nil )) nil ))nil )"2" (induct "n" 2)"1" (rewrite "sigma_eq_arg" )"1" (rewrite "sigma_eq_arg" )"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 "sigma" +)"2" (lemma "triangle" )"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" (use "T_pred_lem" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil )"4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma nil )nil defined_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" nil )"real" sigma nil )"T_low" sigma nil )"T_high" sigma nil )nil integers nil )nil subrange_inductions nil )"(total_order?[real])" nil )nil sigma nil )nil sigma nil )nil real_props nil )"nnreal" nil )"[numfield, numfield -> numfield]" nil )"int" integersnil )"real" realsnil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3255975799"" (skosimp* t)"" (prop)"1" (use "T_pred_lem" ) (("1" (assert ) nil nil )) nil )"2" (use "T_pred_lem" ) (("2" (assert ) nil nil )) nil )"3" (use "T_pred_lem" ) (("3" (assert ) nil nil )) nil )"4" (use "T_pred_lem" ) (("4" (assert ) nil nil )) nil ))nil ))nil )"(total_order?[real])" nil )nil sigma 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]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil ))nil ))nil 3255975799"" (skolem 1 ("F" _ _))"" (rewrite "high_low_rewrite" )"1" (hide 2)"1" (skosimp*)"1" (prop)"1" (expand "sigma" ) (("1" (assert ) nil nil )) nil )"2" (induct "n" 2)"1" (skosimp*)"1" (rewrite "sigma_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 "sigma" +)"2" (prop)"1" (inst?) (("1" (assert ) 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 sigma nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma 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" sigma nil )"T_low" sigma nil )"T_high" sigma nil )"[T -> real]" sigma nil )nil subrange_inductions nil )nil sigma nil )"(total_order?[real])" nil )nil sigma nil )"real" realsnil )nil number_fields nil )"[numfield, numfield -> numfield]" nil )"int" integersnil )"int" integersnil )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 3255975799"" (skolem 1 ("F" _ _))"" (rewrite "high_low_rewrite" )"1" (hide 2)"1" (skosimp*)"1" (prop)"1" (induct "n" 2)"1" (rewrite "sigma_eq_arg" )"1" (flatten) (("1" (inst?) nil nil )) nil )"2" (hide 2)"2" (use "T_pred_lem" )"2" (assert ) nil nil )) nil ))nil ))nil )"2" (skosimp*)"2" (hide 2)"2" (expand "sigma" +)"2" (prop)"1" (inst?) (("1" (assert ) nil nil )) nil )"2" (skosimp*) (("2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 3)"3" (skosimp* t)"3" (inst + "high!1" )"3" (assert )"3" (hide -1 -2 -3)"3" "T_pred_lem" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide 2 3)"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)"2" (skosimp* t)"2" (use "T_pred_lem" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma 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" sigma nil )"T_low" sigma nil )"T_high" sigma nil )"[T -> real]" sigma nil )nil subrange_inductions nil )"(total_order?[real])" nil )"bool" reals nil )nil sigma nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil sigma nil )"real" realsnil )"(strict_total_order?[real])" real_props nil )nil number_fields nil )"[numfield, numfield -> numfield]" nil )"int" integersnil )"int" integersnil )NOT const-decl "[bool -> bool]" booleans nil ))nil ))nil 3255975799"" (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" sigma nil )"int" integersnil )nil number_fields nil )"[numfield, numfield -> numfield]" nil )"T" sigma nil )"int" sigma 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]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil ))nil ))nil 3351939915"" (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" sigma nil )"int" integersnil )nil number_fields nil )"[numfield, numfield -> numfield]" nil )"T" sigma nil )"int" sigma 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]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil ))nil ))nil 3352113941 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"int" integersnil ))nil ))nil 3255975799"" (skolem 1 ("F" _ _ "z" ))"" (rewrite "high_low_rewrite" )"1" (hide 2)"1" (skosimp*)"1" (prop)"1" (expand "sigma" ) (("1" (assert ) nil nil )) nil )"2" (induct "n" 2)"1" (skosimp*)"1" (rewrite "sigma_eq_arg" )"1" (rewrite "sigma_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 "sigma" +)"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" "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" "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" "2" "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" "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" integersnil )nil sigma nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma nil )nil defined_types nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" nil )"[T, T -> boolean]" equalities nil )"real" sigma nil )AND const-decl "[bool, bool -> bool]" booleans nil )"T_low" sigma nil )"T_high" sigma nil )nil integers nil )"int" sigma nil )nil subrange_inductions nil )"(total_order?[real])" nil )"bool" reals nil )nil sigma nil )"(total_order?[real])" nil )nil sigma nil )NOT const-decl "[bool -> bool]" booleans nil )"T" sigma nil )"T" sigma nil )"int" integersnil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"T_high" sigma nil )"T" sigma nil )"T" sigma nil )"T_low" sigma nil )"T" sigma nil ))nil ))nil 3351941788"" (skosimp*)"" (inst + "low!1+z!1" ) (("" (assert ) nil nil )) nil )) nil )nil nil )nil 3351939915"" (skosimp*)"" (typepred "high!1" )"" (skosimp*)"" (inst + "z!1+high!1" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )nil nil ))nil 3352113941"" (skosimp*)"" (inst + "high!1+z!1" ) (("" (assert ) nil nil )) nil )) nil )nil nil ))nil 3304414785"" (skolem 1 ("F" _ _ "z" ))"" (rewrite "high_low_rewrite" )"1" (hide 2)"1" (skosimp*)"1" (prop)"1" (expand "sigma" ) (("1" (assert ) nil nil )) nil )"2" (induct "n" 2)"1" (flatten)"1" (rewrite "sigma_eq_arg" )"1" (rewrite "sigma_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 "sigma" +)"2" (assert )"2" (prop)"2" "2" "connected_domain" )"2" "2" "low!1+z" "1+k!1+z" )"2" (assert ) nil 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" "3" assert )"3" "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" integersnil )nil sigma nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma 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]" nil )"[T, T -> boolean]" equalities nil )"real" sigma nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"T_low" sigma nil )"T_high" sigma nil )nil integers nil )"int" sigma nil )nil subrange_inductions nil )"(total_order?[real])" nil )"bool" reals nil )nil sigma nil )"(total_order?[real])" nil )nil sigma nil )"real" realsnil )nil integers nil )nil sigma nil )NOT const-decl "[bool -> bool]" booleans nil )"int" integersnil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3255975799"" (skolem 1 ("F" "G" _ _))"" (rewrite "high_low_rewrite" )"" (hide 2)"" (skosimp*)"" (prop)"1" (expand "sigma" ) (("1" (assert ) nil nil )) nil )"2" (induct "n" 2)"1" (rewrite "sigma_eq_arg" )"1" (rewrite "sigma_eq_arg" )"1" (rewrite "sigma_eq_arg" ) nil nil )) nil )"2" (use "T_pred_lem" ) (("2" (assert ) nil nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (expand "sigma" +)"2" (propax) nil nil )) nil ))nil ))nil )"3" (hide-all-but 1)"3" (skosimp* t)"3" (typepred "high!1" )"3" (inst + "high!1" )"3" (assert )"3" "3" "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" realsnil )nil sigma nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma nil )nil defined_types nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" nil )"real" sigma nil )AND const-decl "[bool, bool -> bool]" booleans nil )"T_low" sigma nil )"T_high" sigma nil )nil integers nil )nil subrange_inductions nil )"(total_order?[real])" nil )"bool" reals nil )nil sigma nil )"(total_order?[real])" nil )nil sigma 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" "G" _ _))"" (rewrite "high_low_rewrite" )"" (hide 2)"" (skosimp*)"" (prop)"1" (expand "sigma" ) (("1" (assert ) nil nil )) nil )"2" (induct "n" 2)"1" (rewrite "sigma_eq_arg" )"1" (rewrite "sigma_eq_arg" )"1" (rewrite "sigma_eq_arg" ) nil nil )) nil )"2" (use "T_pred_lem" ) (("2" (assert ) nil nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (expand "sigma" +)"2" (propax) nil nil )) nil ))nil ))nil )"3" (hide-all-but 1)"3" (skosimp* t)"3" (typepred "high!1" )"3" (inst + "high!1" )"3" (assert )"3" "3" "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" realsnil )nil sigma nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma nil )nil defined_types nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" nil )"real" sigma nil )AND const-decl "[bool, bool -> bool]" booleans nil )"T_low" sigma nil )"T_high" sigma nil )nil integers nil )nil subrange_inductions nil )"(total_order?[real])" nil )"bool" reals nil )nil sigma nil )"(total_order?[real])" nil )"odd_int" integersnil )nil sigma 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" "G" _ _))"" (rewrite "high_low_rewrite" )"1" (hide 2)"1" (skosimp*)"1" (prop)"1" (expand "sigma" ) (("1" (assert ) nil nil )) nil )"2" (induct "n" 2)"1" (flatten)"1" (rewrite "sigma_eq_arg" )"1" (rewrite "sigma_eq_arg" )"1" (inst?) 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" (expand "sigma" +)"2" (prop)"1" (inst?) (("1" (assert ) nil nil )) nil )"2" (skosimp*) (("2" (inst?) 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" "3" "T_pred_lem" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide-all-but 1)"4" (skosimp* t)"4" (hide -1 -2)"4" (use "T_pred_lem" )"1" (assert ) nil nil )"2" (lemma "T_pred_lem" )"2" "2" "high!1" )"2" (assert ) nil nil ))nil ))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 sigma nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma nil )nil defined_types nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"bool" reals nil )nil real_types nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" nil )"real" sigma nil )"T_low" sigma nil )"T_high" sigma nil )"[T -> real]" sigma nil )"[T -> real]" sigma nil )nil subrange_inductions nil )"(total_order?[real])" nil )nil sigma nil )nil sigma nil )"real" realsnil )"[numfield, numfield -> numfield]" nil )"int" integersnil )"int" integersnil )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 3255975799"" (skolem 1 ("F" "h" _ "l" _))"" (rewrite "high_low_rewrite" )"1" (hide 2)"1" (skosimp*)"1" (prop)"1" (expand "sigma" ) (("1" (assert ) nil nil )) nil )"2" (induct "n" 2)"1" (rewrite "sigma_eq_arg" )"1" (rewrite "sigma_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 "sigma" +)"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 sigma nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma 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" sigma nil )"[T -> real]" sigma nil )"T_low" sigma nil )"T_high" sigma nil )nil integers nil )"T" sigma nil )"T" sigma nil )nil subrange_inductions nil )nil sigma nil )nil sigma nil )"[numfield, numfield -> numfield]" nil )nil number_fields nil )"int" integersnil )"real" realsnil )"(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 "sigma" ) (("1" (assert ) nil nil )) nil )"2" (rewrite "sigma_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 sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )"[int -> boolean]" sigma nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integersnil )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]" nil )nil booleans nil )nil numbers nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"real" sigma nil )nil sigma nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil sigma nil ))nil ))nil 3255975799"" (skosimp*)"" (case "high!1 < low!1" )"1" (expand "sigma" ) (("1" (assert ) nil nil )) nil )"2" (lemma "sigma_restrict" )"2" (inst?)"2" (inst -1 "high!1" "low!1" )"1" (assert )"1" (replace *)"1" (hide -1 -2)"1" (lemma "sigma_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 sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )"[int -> boolean]" sigma nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integersnil )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]" nil )nil booleans nil )nil numbers nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"real" sigma nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil sigma nil )"T_low" sigma nil )"T_high" sigma nil )nil sigma nil ))nil ))nil 3500813619"" (skeep)"" (skosimp*)"" (typepred "low1" )"" (typepred "high1" )"" case "(EXISTS (j: T): high1 <= j) AND (EXISTS (j: T): j <= low1)" )"1" (hide -2)"1" (hide -2)"1" (flatten)"1" (skosimp*)"1" (lemma "connected_domain" )"1" (inst - "j!2" "j!1" "low1+i!1" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (split +)"1" (split -1)"1" (inst + "high1" ) (("1" (assert ) nil nil ))nil )"2" (propax) nil nil ))nil )"2" (split -2)"1" (inst + "low1" ) (("1" (assert ) nil nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma nil )"T_high" sigma nil )"T_low" sigma nil )nil sigma nil )"int" integersnil )"(total_order?[real])" nil )nil integers nil )"[numfield, numfield -> numfield]" nil )"[numfield, numfield -> numfield]" nil )nil number_fields nil )nil integers nil )"int" integersnil )AND const-decl "[bool, bool -> bool]" booleans 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]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil ))nil ))nil 3500813619"" (skeep)"" (skosimp*)"" (typepred "low2" )"" (typepred "high2" )"" case "(EXISTS (j: T): high2 <= j) AND (EXISTS (j: T): j <= low2)") "1" (hide -2)"1" (hide -2)"1" (flatten)"1" (skosimp*)"1" (lemma "connected_domain" )"1" (inst - "j!2" "j!1" "low2+i!1" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (split +)"1" (split -1)"1" (inst + "high2" ) (("1" (assert ) nil nil ))nil )"2" (propax) nil nil ))nil )"2" (split -2)"1" (inst + "low2" ) (("1" (assert ) nil nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma nil )"T_high" sigma nil )"T_low" sigma nil )nil sigma nil )"int" integersnil )"(total_order?[real])" nil )nil integers nil )"[numfield, numfield -> numfield]" nil )"[numfield, numfield -> numfield]" nil )nil number_fields nil )nil integers nil )"int" integersnil )AND const-decl "[bool, bool -> bool]" booleans 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]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil ))nil ))nil 3500813619"" (skeep)"" case "FORALL (jj:nat): low1+jj<=high1 IMPLIES sigma(low1,low1+jj,F) = sigma(low2,low2+jj,G)" )"1" (inst - "high1-low1" )"1" (assert ) nil nil )"2" (expand "sigma" +)"2" (lift-if) (("2" (ground) nil nil )) nil )) nil ))nil )"2" (hide 2)"2" (induct "jj" )"1" (assert )"1" (flatten)"1" (expand "sigma" +)"1" (expand "sigma" +)"1" (inst - "0" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (assert )"2" (expand "sigma" +)"2" (replace -1)"2" (assert ) (("2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skeep)"3" (lemma "connected_domain" )"3" (inst - "low2" "high2" "jj+low2" )"1" (assert ) nil nil )"2" (assert )"2" (typepred "high2" )"2" (ground)"2" "2" "j!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (typepred "high2" )"3" (ground)"1" (inst + "high2" )"1" (ground) nil nil )) nil )"2" (skosimp*)"2" "j!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (assert ) nil nil )"5" (hide 2)"5" (skeep)"5" (typepred "high1" )"5" (ground)"1" (inst + "high1" ) nil nil )"2" (skosimp*)"2" (inst + "j!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" (assert ) nil nil ))nil ))nil )"3" (skeep)"3" (typepred "high2" )"3" (ground)"1" (inst + "high2" ) (("1" (assert ) nil nil )) nil )"2" (skosimp*)"2" (inst + "j!1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"4" (hide 2)"4" (skeep)"4" (typepred "high1" )"4" (ground)"1" (inst + "high1" ) nil nil )"2" (skosimp*)"2" (inst + "j!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" sigma nil )"[T, T -> boolean]" equalities nil )nil sigma nil )nil sigma nil )nil sigma nil )"[int -> boolean]" sigma nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" nil )nil number_fields nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )"int" integersnil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"T_low" sigma nil )"T_high" sigma nil )"[numfield, numfield -> numfield]" nil )"int" integersnil )"(total_order?[real])" nil )"T_low" sigma nil )nil defined_types nil )nil naturalnumbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"nat" sigma nil )"nat" sigma nil )"posint" nil )"posint" nil )"real" realsnil )"T_high" sigma nil )nil integers nil )NOT const-decl "[bool -> bool]" booleans nil )nil sigma nil ))nil 3497351599"" (skeep)"" (lemma "sigma_restrict_eq" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil )nil sigma nil )"real" realsnil )nil sigma nil )nil sigma nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil sigma nil )"[int -> boolean]" sigma nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil ))nil 3491824268"" (skeep)"" (lemma "sigma_restrict_eq" )"" (inst - "F" "(LAMBDA (tt:T): 0)" "high" "low" )"" (lemma "sigma_zero" )"" (inst?)"" (assert )"" (expand "restrict" )"" (decompose-equality)"" (lift-if)"" (inst - "x!1" )"1" (ground) nil nil )"2" (assert ) (("2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma nil )nil sigma 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 )"bool" reals nil )"(total_order?[real])" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"T_low" sigma nil )"T" sigma nil )"T_high" sigma nil )nil integers nil )"[T -> real]" sigma nil )nil sigma nil )nil sigma nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil sigma nil )"[int -> boolean]" sigma nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil ))nil 3594138610"" case "FORALL (F: [T -> real], high: T_high, low: T_low,k:nat):k<=high-low IMPLIES LAMBDA (n: T): abs(F(n)))") "1" (skeep)"1" (inst - "F" "high" "low" "high-low" )"1" (assert ) nil nil )"2" (assert )"2" (expand "sigma" +) (("2" (grind) nil nil )) nil ))nil ))nil ))nil )"2" (hide 2)"2" (induct "k" )"1" (skeep)"1" (assert )"1" (expand "sigma" +)"1" (expand "sigma" +) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (skeep)"2" (inst - "F" "high" "low" )"2" (assert )"2" (expand "sigma" +)"2" (expand "abs" )"2" (lift-if)"2" (lift-if)"2" "2" assert )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skeep)"3" (assert )"3" (typepred "high" )"3" (typepred "low" )"3" (lemma "connected_domain" )"3" (ground)"1" (inst - "low" "high" "low+k" )"1" (assert ) nil nil )) nil )"2" (skeep -1)"2" "low" "j" "k+low" )"2" (assert ) nil nil ))nil ))nil )"3" (skeep -)"3" "j" "high" "k+low" )"3" (assert ) nil nil ))nil ))nil )"4" (skosimp*)"4" "j!2" "j!1" "k+low" )"4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skeep)"3" (assert )"3" (typepred "high" )"3" (typepred "low" )"3" (lemma "connected_domain" )"3" (ground)"1" (inst - "low" "high" "low+k" )"1" (assert ) nil nil )) nil )"2" (skeep -1)"2" (inst - "low" "j" "k+low" )"2" (assert ) nil nil )) nil ))nil )"3" (skeep -)"3" (inst - "j" "high" "k+low" )"3" (assert ) nil nil )) nil ))nil )"4" (skosimp*)"4" (inst - "j!2" "j!1" "k+low" )"4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integers nil )nil sigma nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"posint" nil )"real" realsnil )nil naturalnumbers nil )nil defined_types nil )"posint" nil )"{j: nonneg_int | j >= i}" real_defs nil )"(total_order?[real])" nil )"T_low" sigma nil )"T_high" sigma nil )"(total_order?[real])" nil )"int" integersnil )"int" integersnil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"[int -> boolean]" sigma nil )nil sigma nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma nil )nil sigma nil )"bool" reals nil )nil naturalnumbers nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" nil )"real" sigma nil )"[numfield, numfield -> numfield]" nil ))nil 3497780826"" (skeep)"" (typepred "high" )"" (typepred "low" )"" case "(EXISTS (j: T): j <= low) AND (EXISTS (j: T): high <= j)") "1" (hide -2)"1" (hide -2)"1" (flatten)"1" (skosimp*)"1" (lemma "connected_domain" )"1" (inst - "j!1" "j!2" "i!1" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (split)"1" (assert )"1" (split -)"1" (inst + "low" ) (("1" (assert ) nil nil ))nil )"2" (propax) nil nil ))nil ))nil )"2" (hide -1)"2" (split -)"1" (inst + "high" ) (("1" (assert ) nil nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma nil )"bool" reals nil )nil sigma nil )"[int -> boolean]" sigma nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil numbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" nil )nil integers nil )"(total_order?[real])" nil )nil sigma nil )"T_high" sigma nil )"T_low" sigma nil )nil sigma nil ))nil ))nil 3497781196"" (skeep)"" (typepred "high" )"" (typepred "low" )"" case "(EXISTS (j: T): j <= low) AND (EXISTS (j: T): high <= j)") "1" (hide -2)"1" (hide -2)"1" (flatten)"1" (skosimp*)"1" (lemma "connected_domain" )"1" (inst - "j!1" "j!2" "i1!1" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (split)"1" (assert )"1" (split -)"1" (inst + "low" ) (("1" (assert ) nil nil ))nil )"2" (propax) nil nil ))nil ))nil )"2" (hide -1)"2" (split -)"1" (inst + "high" ) (("1" (assert ) nil nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma nil )"bool" reals nil )nil sigma nil )"[int -> boolean]" sigma nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil numbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" nil )nil integers nil )"(total_order?[real])" nil )nil sigma nil )"T_high" sigma nil )"T_low" sigma nil )nil sigma nil ))nil )nil 3497780826"" (subtype-tcc) nil nil ) nil nil ))nil 3497781273"" (skeep)"" (typepred "high" )"" (typepred "low" )"" case "(EXISTS (j: T): j <= low) AND (EXISTS (j: T): high <= j)") "1" (hide -2)"1" (hide -2)"1" (flatten)"1" (skosimp*)"1" (lemma "connected_domain" )"1" (inst - "j!1" "j!2" "z" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (split)"1" (assert )"1" (split -)"1" (inst + "low" ) (("1" (assert ) nil nil ))nil )"2" (propax) nil nil ))nil ))nil )"2" (hide -1)"2" (split -)"1" (inst + "high" ) (("1" (assert ) nil nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma nil )"bool" reals nil )nil sigma nil )"[int -> boolean]" sigma nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil numbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"(total_order?[real])" nil )nil sigma nil )"T_high" sigma nil )"T_low" sigma nil )nil sigma nil ))nil )nil 3497781249";;; Proof sigma_eq_one_arg_TCC2-2 for formula sigma.sigma_eq_one_arg_TCC2" ";;; Proof sigma_eq_one_arg_TCC2-2 for formula sigma.sigma_eq_one_arg_TCC2" "high" )";;; Proof sigma_eq_one_arg_TCC2-2 for formula sigma.sigma_eq_one_arg_TCC2" "low" )";;; Proof sigma_eq_one_arg_TCC2-2 for formula sigma.sigma_eq_one_arg_TCC2" case "(EXISTS (j: T): j <= low) AND (EXISTS (j: T): high <= j)") "1" (hide -2)"1" (hide -2)"1" (flatten)"1" (skosimp*)"1" (lemma "connected_domain" )"1" (inst - "j!1" "j!2" "i1!1" )"1" (assert ) nil )))))))))))))"2" (split)"1" (assert )"1" (split -)"1" (inst + "low" ) (("1" (assert ) nil )))"2" (propax) nil )))))"2" (hide -1)"2" (split -)"1" (inst + "high" ) (("1" (assert ) nil )))"2" (propax) nil ))))))))))))))";;; developed with shostak decision procedures") nil nil )nil 3497780826"" (subtype-tcc) nil nil ) nil nil ))nil 3497780826"" (skeep)"" (lemma "sigma_split" )"" (inst - "F" "high" "low" "z" )"" (assert )"" (replace -1 +)"" (hide -1)"" (lemma "sigma_split" )"" (inst - "F" "z" "low" "z-1" )"" (assert )"" (replace -1)"" (hide -1)"" case "sigma(1+z,high,F) = 0" )"1" replace -1)"1" case "sigma(low,z-1,F) = 0" )"1" replace -1)"1" expand "sigma" +)"1" expand "sigma" +)"1" (propax) nil nil ))nil ))nil ))nil )"2" rewrite "sigma_restrict_eq_0" )nil nil ))nil ))nil )"2" rewrite "sigma_restrict_eq_0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma nil )"int" integersnil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"real" sigma nil )"[numfield, numfield -> numfield]" nil )nil sigma nil )"real" realsnil )"int" integersnil )nil sigma nil )nil sigma nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil sigma nil )"[int -> boolean]" sigma nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil ))nil 3615045476"" (skeep)"" (lemma "connected_domain" )"" (typepred "low" )"" (typepred "high" )"" (ground)"1" (inst - "low" "high" "z" )"1" (assert ) nil nil )) nil )"2" (skosimp*)"2" (inst - "j!1" "high" "z" )"2" (assert ) nil nil )) nil ))nil )"3" (skosimp*)"3" (inst - "low" "j!1" "z" )"3" (assert ) nil nil )) nil ))nil )"4" (skosimp*)"4" (inst - "j!1" "j!2" "z" )"4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma nil )nil sigma nil )nil integers 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]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil ))nil ))nil 3615045478"" (skeep)"" (lemma "sigma_eq_one_arg" )"" (inst?)"" (assert )"" (split)"1" (skosimp*)"1" (inst - "i!1" ) (("1" (assert ) nil nil )) nil ))nil )"2" (skosimp*)"2" (inst - "i!1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" nil )"int" integersnil )"[numfield, numfield -> numfield]" nil )nil number_fields nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil sigma nil )nil sigma nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil sigma nil )"[int -> boolean]" sigma nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil ))nil 3615045724"" (skeep)"" (lemma "connected_domain" )"" (typepred "low" )"" (typepred "high" )"" (ground)"1" (inst - "low" "high" "z1" )"1" (assert ) nil nil )) nil )"2" (skosimp*)"2" (inst - "j!1" "high" "z1" )"2" (assert ) nil nil )) nil ))nil )"3" (skosimp*)"3" (inst - "low" "j!1" "z1" )"3" (assert ) nil nil )) nil ))nil )"4" (skosimp*)"4" (inst - "j!1" "j!2" "z1" )"4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma nil )nil sigma nil )nil integers 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]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil ))nil )nil 3615045684"" (skeep)"" (skosimp*)"" (lemma "connected_domain" )"" (typepred "low" )"" (typepred "high" )"" (ground)"1" (inst - "low" "high" "z2" )"1" (assert ) nil )))"2" (skosimp*)"2" (inst - "j!1" "high" "z2" )"2" (assert ) nil )))))"3" (skosimp*)"3" (inst - "low" "j!1" "z2" )"3" (assert ) nil )))))"4" (skosimp*)"4" (inst - "j!1" "j!2" "z2" )"4" (assert ) nil ))))))))))))))))nil )nil nil )nil 3615045631"" (skeep)"" (lemma "connected_domain" )"" (typepred "low" )"" (typepred "high" )"" (ground)"1" (inst - "low" "high" "z1" )"1" (assert ) nil nil )) nil )"2" (skosimp*)"2" (inst - "j!1" "high" "z1" )"2" (assert ) nil nil )) nil ))nil )"3" (skosimp*)"3" (inst - "low" "j!1" "z1" )"3" (assert ) nil nil )) nil ))nil )"4" (skosimp*)"4" (inst - "j!1" "j!2" "z1" )"4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil )nil 3615043942"" (subtype-tcc) nil nil ) nil nil ))nil 3615045702"" (skeep)"" (lemma "connected_domain" )"" (typepred "low" )"" (typepred "high" )"" (ground)"1" (inst - "low" "high" "z2" )"1" (assert ) nil nil )) nil )"2" (skosimp*)"2" (inst - "j!1" "high" "z2" )"2" (assert ) nil nil )) nil ))nil )"3" (skosimp*)"3" (inst - "low" "j!1" "z2" )"3" (assert ) nil nil )) nil ))nil )"4" (skosimp*)"4" (inst - "j!1" "j!2" "z2" )"4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma nil )nil sigma nil )nil integers 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]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil ))nil )nil 3615045619"" (skeep)"" (skosimp*)"" (lemma "connected_domain" )"" (typepred "low" )"" (typepred "high" )"" (ground)"1" (inst - "low" "high" "z" )"1" (assert ) nil )))"2" (skosimp*)"2" (inst - "j!1" "high" "z" )"2" (assert ) nil )))))"3" (skosimp*)"3" (inst - "low" "j!1" "z" )"3" (assert ) nil )))))"4" (skosimp*)"4" (inst - "j!1" "j!2" "z" )"4" (assert ) nil ))))))))))))))))nil )nil nil )nil 3615043942"" (subtype-tcc) nil nil ) nil nil ))nil 3615043943"" case "FORALL (F: [T -> real], high: T_high, low: T_low, z1, z2: int): AND z1 <= high AND low <= z2 AND z2 <= highAND z1 < z2AND FORALL (i: subrange(low, high)):AND i /= z2 IMPLIES F(i) = 0)") "1" (skeep)"1" (case "z1 < z2" )"1" (inst?) (("1" (assert ) nil nil )) nil )"2" (inst - "F" "high" "low" "z2" "z1" )"2" (assert )"2" (skosimp*)"2" (inst - "i!1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (lemma "sigma_split" )"2" (inst - "F" "high" "low" "z1" )"2" (assert )"2" (replaces -1)"2" (expand "sigma" + 2)"2" (lemma "sigma_split" )"2" (inst - "F" "high" "1+z1" "z2" )"2" (assert )"2" "2" expand "sigma" + 1)"2" assert )"2" rewrite "sigma_restrict_eq_0" )"1" rewrite "sigma_restrict_eq_0" )"1" rewrite "sigma_restrict_eq_0" )"1" "1" "i!1" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" "2" "i!1" )"2" (assert ) nil nil ))nil ))nil ))nil )"2" "2" "i!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skeep)"3" (lemma "connected_domain" )"3" (typepred "high" )"3" (typepred "low" )"3" (ground)"1" (inst - "low" "high" "z2" )"1" (assert ) nil nil )) nil )"2" (skosimp*)"2" (inst - "low" "j!1" "z2" )"2" (ground) nil nil )) nil ))nil )"3" (skosimp*)"3" (inst - "j!1" "high" "z2" )"3" (assert ) nil nil )) nil ))nil )"4" (skosimp*)"4" (inst - "j!2" "j!1" "z2" )"4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide 2)"4" (skeep)"4" (lemma "connected_domain" )"4" (typepred "low" )"4" (typepred "high" )"4" (ground)"1" (inst - "low" "high" "z1" )"1" (assert ) nil nil )) nil )"2" (skosimp*)"2" (inst - "j!1" "high" "z1" )"2" (assert ) nil nil )) nil ))nil )"3" (skosimp*)"3" (inst - "low" "j!1" "z1" )"3" (assert ) nil nil )) nil ))nil )"4" (skosimp*)"4" (inst - "j!1" "j!2" "z1" )"4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (hide 2)"5" (skeep)"5" (lemma "connected_domain" )"5" (typepred "low" )"5" (typepred "high" )"5" (skosimp*)"5" (ground)"1" (inst - "low" "high" "i!1" )"1" (assert ) nil nil )) nil )"2" (skosimp*)"2" (inst - "j!1" "high" "i!1" )"2" (assert ) nil nil )) nil ))nil )"3" (skosimp*)"3" (inst - "low" "j!1" "i!1" )"3" (assert ) nil nil )) nil ))nil )"4" (skosimp*)"4" (inst - "j!1" "j!2" "i!1" )"4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma nil )nil integers nil )NOT const-decl "[bool -> bool]" booleans nil )nil sigma nil )"int" integersnil )"int" integersnil )nil sigma nil )"[numfield, numfield -> numfield]" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" realsnil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"[int -> boolean]" sigma nil )nil sigma nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma nil )nil sigma nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil integers nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"real" sigma nil )nil number_fields nil )"[numfield, numfield -> numfield]" nil ))nil 3497351634"" (skeep)"" (lemma "sigma_restrict_eq_0" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil )nil sigma nil )"real" realsnil )nil sigma nil )nil sigma nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil sigma nil )"[int -> boolean]" sigma nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil ))nil 3255975799"" (skosimp*)"" (lemma "sigma_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 sigma nil )"[T -> real]" sigma 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 )"bool" reals nil )nil sigma nil )nil sigma nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil sigma nil )"[int -> boolean]" sigma nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil ))nil ))nil 3255975799"" (skosimp*)"" (lemma "sigma_ge_0" )"" "(LAMBDA (t:T): G!1(t) - F!1(t))" "high!1" "low!1" )"" (split -1)"1" (assert )"1" (lemma "sigma_minus" )"1" (inst?)"1" (replace -1 * rl)"1" (hide -1) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (assert )"2" (inst?) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma nil )nil sigma nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil sigma nil )nil sigma nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )"[numfield, numfield -> numfield]" nil )nil number_fields nil )nil sigma nil )"[int -> boolean]" sigma nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )"real" realsnil ))nil ))nil 3255975799"" (skosimp*)"" (lemma "sigma_gt_0" )"" "(LAMBDA (t:T): G!1(t) - F!1(t))" "high!1" "low!1" )"" (split -1)"1" (assert )"1" (lemma "sigma_minus" )"1" (inst?)"1" (replace -1 * rl)"1" (hide -1) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil )"3" (skosimp*)"3" (assert )"3" (inst?) (("3" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil sigma nil )nil sigma nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil sigma nil )nil sigma nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )"[numfield, numfield -> numfield]" nil )nil number_fields nil )nil sigma nil )"[int -> boolean]" sigma nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )"real" realsnil ))nil ))nil 3492506755"" (skeep)"" (lemma "sigma_le" )"" (inst - "G" "F" "high" "low" ) (("" (assert ) nil nil ))nil ))nil ))nil )nil sigma nil )"(total_order?[real])" nil )nil sigma nil )nil sigma nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil sigma nil )"[int -> boolean]" sigma nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil ))nil 3492506775"" (skeep)"" (lemma "sigma_lt" )"" (inst - "G" "F" "high" "low" ) (("" (assert ) nil nil ))nil ))nil ))nil )nil sigma nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil sigma nil )nil sigma nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil sigma nil )"[int -> boolean]" sigma nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil ))nil 3255975799"" (skosimp*)"" (case "i!1 = low!1" )"1" (rewrite "sigma_first" )"1" (lemma "sigma_first" )"1" (inst -1 "G!1" "high!1" "low!1" )"1" (assert )"1" (split -1)"1" (assert )"1" (replace -1)"1" (replace -5)"1" (hide -1 -5)"1" assert )"1" replace -1)"1" assert )"1" rewrite "sigma_eq" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "sigma" )"2" (assert )"2" (expand "sigma" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "sigma" )"2" (assert )"2" (expand "sigma" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (case-replace "i!1 = high!1" )"1" (rewrite "sigma_last" )"1" (lemma "sigma_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" (rewrite "sigma_eq" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "sigma_split" )"2" (inst?)"2" (inst -1 "i!1" )"2" (assert )"2" (replace -1)"2" (hide -1)"2" (lemma "sigma_split" )"2" "G!1" "high!1" "low!1" "i!1" )"2" assert )"2" replace -1)"2" "2" "sigma_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" "sigma(low!1, i!1 - 1, G!1 WITH [i!1 := a!1]) = sigma(low!1, i!1 - 1, G!1)" )"1" "1" assert )"1" rewrite "sigma_eq" )nil nil ))nil ))nil )"2" "2" rewrite "sigma_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 sigma nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil sigma nil )"[int -> boolean]" sigma nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"odd_int" integersnil )"[numfield, numfield -> numfield]" nil )nil number_fields nil )nil sigma nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"real" realsnil )"int" integersnil )"real" realsnil )nil sigma nil )nil sigma nil )nil sigma nil )"real" sigma nil )nil sigma nil )"int" integersnil )"[numfield, numfield -> numfield]" nil ))nil ))nil 3496049375 ("" (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]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma nil )"(total_order?[real])" nil )"int" integersnil )"int" integersnil ))nil ))nil 3496049376"" (skeep)"" (lemma "sigma_le" )"" "F" "LAMBDA (i:T): B/(high-low+1)" "high" "low" )"1" (split -)"1" case "FORALL (i:nat): i<= high-low IMPLIES sigma(low,low+i,LAMBDA (i:T):B/(high-low+1)) = (i+1)*B/(high-low+1)" )"1" (inst - "high-low" )"1" (case "(high-low+1)*B/(high-low+1) = B" )"1" (assert ) nil nil ) ("2" (field) nil nil )"3" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil )"2" (induct "i" )"1" (assert )"1" (expand "sigma" +)"1" (expand "sigma" +)"1" (assert ) nil nil )) nil ))nil ))nil )"2" (skeep)"2" (expand "sigma" +) (("2" (assert ) nil nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil )"4" (assert ) nil nil ) ("5" (assert ) nil nil )"6" (assert ) nil nil ) ("7" (assert ) nil nil )"8" (assert ) nil nil ) ("9" (assert ) nil nil )"10" (assert ) nil nil )"11" (skosimp*)"11" (lemma "T_pred_lem" )"11" (inst - "high" "low" "i!2 + low" )"11" (assert ) nil nil )) nil ))nil ))nil )"12" (skosimp*)"12" (lemma "T_pred_lem" )"12" (inst - "high" "low" "i!2 + low" )"12" (assert ) nil nil )) nil ))nil ))nil )"13" (skosimp*)"13" (lemma "T_pred_lem" )"13" (inst - "high" "low" "i!2 + low" )"13" (assert ) nil nil )) nil ))nil ))nil )"14" (skosimp*)"14" (lemma "T_pred_lem" )"14" (inst - "high" "low" "i!2 + low" )"14" (assert ) nil nil )) nil ))nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil )"4" (skosimp*) (("4" (assert ) nil nil )) nil )"5" (skosimp*)"5" (lemma "T_pred_lem" )"5" (inst - "high" "low" "i!1 + low" )"5" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst - "n!1" ) (("2" (assert ) nil nil )) nil ))nil ))nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )nil sigma nil )nil defined_types nil )nil naturalnumbers nil )"nat" sigma nil )"nat" sigma nil )"nat" sigma nil )"posint" nil )"posint" nil )nil sigma nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"real" realsnil )"real" realsnil )"real" realsnil )"[numfield, numfield -> numfield]" nil )"real" sigma nil )"[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, nznum -> numfield]" number_fieldsnil )nil number_fields nil )"boolean" notequal nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"[int -> boolean]" sigma nil )nil sigma nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" nil )"[numfield, numfield -> numfield]" nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma nil )"T_low" sigma nil )nil sigma nil )"T_high" sigma nil )"int" integersnil )"real" realsnil )"int" integersnil ))nil 3255975799"" (skolem 1 ("F" _ _))"" (rewrite "high_low_rewrite" )"" (hide 2)"" (skosimp*)"" (prop)"1" (expand "sigma" ) (("1" (assert ) nil nil )) nil )"2" (induct "n" 2)"1" (rewrite "sigma_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 "sigma" +)"2" (prop)"2" (inst?) (("2" (assert ) 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 sigma nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma nil )nil defined_types nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"real" sigma nil )"[T -> real]" sigma nil )nil integers nil )"T_high" sigma nil )"T_low" sigma nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil subrange_inductions nil )nil sigma nil )"(total_order?[real])" nil )nil sigma nil )"real" realsnil )nil number_fields nil )"[numfield, numfield -> numfield]" nil )"int" integersnil )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 3352253917"" (skolem 1 ("F" _ _))"" (rewrite "high_low_rewrite" )"" (hide 2)"" (skosimp*)"" (prop)"1" (expand "sigma" ) (("1" (assert ) nil nil )) nil )"2" (induct "n" 2)"1" (rewrite "sigma_eq_arg" )"1" (skosimp*) (("1" (inst?) 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 "sigma" +)"2" (prop)"2" (inst?) (("2" (assert ) 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 sigma nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma nil )nil defined_types nil )"[bool, bool -> bool]" booleans nil )"real" sigma nil )"[T -> real]" sigma nil )nil integers nil )"T_high" sigma nil )"T_low" sigma nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil subrange_inductions nil )"(total_order?[real])" nil )"bool" reals nil )nil sigma nil )nil sigma nil )"real" realsnil )nil number_fields nil )"[numfield, numfield -> numfield]" nil )"int" integersnil )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 3255975799"" (skosimp*)"" (case "high!1 < low!1" )"1" (expand "sigma" ) (("1" (assert ) nil nil )) nil )"2" case "(FORALL (rng:nat): T_pred(low!1+rng) IMPLIES sigma(low!1,low!1+rng, F!1) <= 0)" )"1" (inst -1 "high!1-low!1" )"1" (assert )"1" (hide-all-but (1 2))"1" (use "T_pred_lem" ) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (hide 3)"2" (induct "rng" )"1" (assert )"1" (rewrite "sigma_eq_arg" )"1" (inst?) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (skosimp*)"2" (assert )"2" (split -1)"1" (expand "sigma" 1)"1" (assert )"1" (inst?) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (lemma "connected_domain" )"2" "low!1" "1 + j!1 + low!1" "j!1 + low!1" )"1" (assert ) nil nil )"2" (hide-all-but (1 4))"2" "T_pred_lem" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*)"3" (inst + "low!1 + rng!2" )"1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil )"4" (skosimp*)"4" (inst + "low!1 + rng!2" )"1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (skosimp*)"3" (inst + "low!1 + rng!1" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )nil nil ))nil 3411475824"" (skosimp*)"" (rewrite "sigma_nonneg" )"" (skosimp*) (("" (assert ) nil nil )) nil )) nil ))nil )nil sigma nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"[int -> boolean]" sigma nil )nil sigma nil )nil booleans nil )"bool" reals nil )nil real_types nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma nil )nil sigma nil )"(total_order?[real])" nil ))nil )nil 3411475728 ("" (judgement-tcc) nil nil ) nil nil ))nil 3501424358"" (skosimp*)"" (rewrite "sigma_nonneg" )"" (skosimp*) (("" (assert ) nil nil )) nil )) nil ))nil )nil sigma nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"[int -> boolean]" sigma nil )nil sigma nil )nil booleans nil )"bool" reals nil )nil real_types nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma nil )nil sigma nil )"(total_order?[real])" nil ))nil )nil 3501424319 ("" (judgement-tcc) nil nil ) nil nil ))nil 3411475728"" (skosimp*)"" (rewrite "sigma_nonpos" )"" (skosimp*) (("" (assert ) nil nil )) nil )) nil ))nil )nil sigma nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"[int -> boolean]" sigma nil )nil sigma nil )nil booleans nil )"bool" reals nil )nil real_types nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil sigma nil )nil sigma nil )"(total_order?[real])" nil ))nil ))nil 3411475912"" (auto-rewrite-theory "integers" )"" (auto-rewrite-theory "rationals" )"" (skosimp*)"" case "(FORALL (rng: nat): T_pred(low!1+rng) IMPLIES (rational_pred(sigma(low!1, low!1+rng, Fnat!1)) AND integer_pred(sigma(low!1, low!1+rng, Fnat!1))) AND sigma(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 "sigma" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "sigma" ) (("2" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (induct "rng" )"1" (skosimp*)"1" (rewrite "sigma_eq_arg" )"1" (assert ) nil nil )) nil ))nil )"2" (skosimp*)"2" (expand "sigma" 1)"2" (split -1)"1" (flatten) (("1" (assert ) nil nil )) nil )"2" (hide 2)"2" (lemma "T_pred_lem" )"2" "low!1+j!1" "low!1" "low!1+j!1" )"1" (assert ) nil nil )"2" assert )"2" "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" sigma nil )nil sigma nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil sigma nil )"bool" reals nil )nil sigma nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" nil )nil number_fields nil )"[int -> boolean]" sigma nil )"[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )"nnreal" sigma nil )"int" integersnil )"(strict_total_order?[real])" real_props nil )nil sigma nil )"(total_order?[real])" nil )"T_low" sigma nil )"T_high" sigma nil )"[numfield, numfield -> numfield]" nil )"int" integersnil )"(total_order?[real])" nil )"[T -> nat]" sigma nil )nil defined_types nil )nil naturalnumbers nil )nil sigma nil )"posint" nil )"nnreal" nil )"nat" sigma nil )"posint" nil )nil integers nil )nil rationals nil ))nil )nil 3411475883";;; Proof for formula sigma.sigma_TCC5" (skosimp*) ";;; Proof for formula sigma.sigma_TCC5" rewrite "sigma_nonpos" )";;; Proof for formula sigma.sigma_TCC5" (skosimp*) ";;; Proof for formula sigma.sigma_TCC5" (assert) nil ))))))"" )nil nil )nil 3411475728 ("" (judgement-tcc) nil nil ) nil nil ))nil 3411475945"" (auto-rewrite-theory "integers" )"" (auto-rewrite-theory "rationals" )"" (skosimp*)"" (case "low!1<=high!1" )"1" case "(FORALL (rng: nat): T_pred(low!1+rng) IMPLIES (rational_pred(sigma(low!1, low!1+rng, Fnpi!1)) AND integer_pred(sigma(low!1, low!1+rng, Fnpi!1))) AND sigma(low!1, low!1+rng, Fnpi!1) <= 0)" )"1" (inst -1 "high!1-low!1" )"1" (assert )"1" (split -)"1" (propax) nil nil )"2" (use "T_pred_lem" )"2" (assert ) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (hide 2)"2" (induct "rng" 1)"1" (rewrite "sigma_eq_arg" )"1" (assert ) (("1" (grind) nil nil )) nil ))nil )"2" (skosimp*)"2" (expand "sigma" +)"2" (split -)"1" (flatten) (("1" (assert ) nil nil ))nil )"2" (hide 2)"2" assert )"2" "T_pred_lem" )"2" "low!1+j!1" "low!1" "low!1+j!1" )"1" (assert ) nil nil )"2" "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" (hide 2) (("3" (skosimp*) nil nil )) nil )"4" (skosimp*) nil nil ) ("5" (skosimp*) nil nil ))nil )"2" (expand "sigma" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )nil sigma nil )nil sigma nil )nil sigma nil )"[int -> boolean]" sigma nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integersnil )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]" nil )nil booleans nil )nil numbers nil )nil rationals nil )nil integers nil )"posint" nil )"nat" sigma nil )"npreal" nil )"posint" nil )nil sigma nil )nil naturalnumbers nil )nil defined_types nil )"[T -> nonpos_int]" sigma nil )"(total_order?[real])" nil )"int" integersnil )"[numfield, numfield -> numfield]" nil )"T_high" sigma nil )"T_low" sigma nil )nil sigma nil )"(total_order?[real])" nil )"int" integersnil )"nonpos_real" sigmanil )"bool" reals nil )nil naturalnumbers nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" sigma nil )nil integers nil )"(strict_total_order?[real])" real_props nil ))nil )nil 3411475728 ("" (judgement-tcc) nil nil )nil nil ))nil 3410183521"" (skolem 1 ("FF" _ _))"" (rewrite "high_low_rewrite" )"" (hide 2)"" (skosimp*)"" (prop)"" (induct "n" 2)"1" (rewrite "sigma_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 "sigma" +)"2" (assert ) 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 sigma nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma nil )nil defined_types nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"real" sigma nil )"bool" reals nil )nil integers nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"T_low" sigma nil )"T_high" sigma nil )nil integers nil )nil subrange_inductions nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil sigma nil )"(strict_total_order?[real])" real_props nil )"nat" sigma nil )"(strict_total_order?[real])" real_props nil )nil sigma nil )"int" integersnil )"posint" nil )NOT const-decl "[bool -> bool]" booleans nil ))nil ))nil 3412514934"" (skolem 1 ("FF" _ _))"" (rewrite "high_low_rewrite" )"" (hide 2)"" (skosimp*)"" (prop)"" (induct "n" 2)"1" (rewrite "sigma_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 "sigma" +)"2" (assert ) 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 sigma nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma nil )nil defined_types nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"real" sigma nil )"bool" reals nil )nil real_types nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"T_low" sigma nil )"T_high" sigma nil )nil integers nil )nil subrange_inductions nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil sigma nil )"(strict_total_order?[real])" real_props nil )"nnreal" sigma nil )"(strict_total_order?[real])" real_props nil )nil sigma nil )"int" integersnil )"posreal" real_types nil )NOT const-decl "[bool -> bool]" booleans nil ))nil ))nil 3255975799"" (skosimp*)"" (lemma "sigma_middle" )"" (inst?)"" (inst -1 "i!1" )"" (assert ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil sigma nil )"int" integersnil )"int" integersnil )"nnreal" sigma nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"nnreal" nil )nil sigma nil )nil sigma nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil sigma nil )"[int -> boolean]" sigma nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )"real" realsnil ))nil ))nil 3256040402"" (skosimp*)"" (lemma "sigma_middle" )"" (inst?)"" (inst -1 "i!1" )"" (assert ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil sigma nil )"int" integersnil )"int" integersnil )"(total_order?[real])" nil )"(total_order?[real])" nil )"nnreal" sigma nil )"nnreal" nil )nil sigma nil )nil sigma nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil sigma nil )"[int -> boolean]" sigma nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )"real" realsnil ))nil )nil 3255975877"" (skosimp*)"" (lemma "sigma_middle" )"" (inst?)"" (inst -1 "i!1" )"" (assert )"" (replace -1) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil shostak))nil 3255975799"" (skosimp*)"" (inst + "low!1" )"1" (assert ) nil nil )"2" (use "T_pred_lem" ) (("2" (assert ) nil nil )) nil ))nil ))nil )"T_low" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )"[int -> boolean]" sigma nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )"(strict_total_order?[real])" real_props nil )"int" integersnil )"(total_order?[real])" nil )nil sigma nil )nil sigma nil ))nil ))nil 3255975799"" (skosimp*)"" (use "T_pred_lem" ) (("" (assert ) nil nil )) nil )) nil )nil sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )"[int -> boolean]" sigma nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integersnil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )nil sigma nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil ))nil 3352118808 ("" (subtype-tcc) nil nil )"int" integersnil )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]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma nil )"{n: nonneg_real | n >= m AND n >= -m}" nil )"{j: nonneg_int | j >= i}" real_defs nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"int" integersnil ))nil ))nil 3352142246"" (skosimp* t)"" (prop)"1" (inst + "low!1" ) (("1" (assert ) nil nil )) nil )"2" (skosimp*)"2" (inst + "j!1" ) (("2" (assert ) nil nil )) nil )) nil )"3" (skosimp*)"3" (inst + "low!1" ) (("3" (assert ) nil nil )) nil ))nil )"4" (skosimp*)"4" (inst + "j!1" ) (("4" (assert ) nil nil )) nil )) nil ))nil ))nil )"int" integersnil )"int" integersnil )"(total_order?[real])" nil )"T_low" sigma 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]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integersnil )nil integers nil )"[int -> boolean]" sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )nil sigma nil ))nil ))nil 3255975799"" (skosimp*)"" (case "high!1<low!1" )"1" (assert )"1" (expand "sum_it_def" )"1" (expand "sigma" ) (("1" (propax) nil nil )) nil ))nil ))nil )"2" (lemma "subrange_induction[low!1,high!1]" )"1" "lambda(lh:T| low!1 <= lh AND lh <= high!1): sum_it_def((high!1-lh)+low!1, high!1, F!1, sigma(low!1,(high!1-lh)+low!1-1, F!1)) = sigma(low!1, high!1, F!1)" )"1" (expand "extend" )"1" (ground)"1" (inst -1 "high!1-i!1+low!1-1" )"1" (ground) nil nil )"2" (expand "sum_it_def" )"2" (expand "sigma" ) (("2" (assert ) nil nil ))nil ))nil ))nil )"2" (ground)"2" (hide -2 -3 -4 3)"2" (expand "sum_it_def" )"2" (expand "sum_it_def" )"2" (expand "sigma" + 2)"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (ground)"3" (expand "sigma" )"3" (assert )"3" (hide -1 -2 3)"3" (use "T_pred_lem" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"4" (hide -1 -2 3)"4" (skosimp*)"4" (ground)"1" (expand "sum_it_def" 1)"1" (expand "sigma" -)"1" assert )"1" expand "sigma" 1 2)"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-3 1))"2" (lemma "T_pred_lem" )"2" "2" "high!1" "low!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst + "high!1 -lh!1 +low!1" )"1" (assert ) nil nil )"2" (hide-all-but 1)"2" (lemma "T_pred_lem" )"2" "high!1" "low!1" "high!1-lh!1+low!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (skosimp*)"3" (typepred "high!1" )"3" (typepred "low!1" )"3" (assert )"3" (lemma "T_pred_lem" )"3" "high!1" "low!1" "(high!1 - lh!1) + low!1" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )nil sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )"[int -> boolean]" sigma nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integersnil )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]" nil )nil booleans nil )nil numbers nil )"real" sigma nil )"real" sigma nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integersnil )"int" integersnil )"[numfield, numfield -> numfield]" nil )"[numfield, numfield -> numfield]" nil )nil number_fields nil )"T_high" sigma nil )"T_low" sigma nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil defined_types nil )"bool" booleans nil )"R" extend nil )"[T, T -> boolean]" equalities nil )"real" realsnil )"(strict_total_order?[real])" real_props nil )"T" sigma nil )nil sigma nil )"{lh: T | low!1 <= lh AND lh <= high!1}" sigma nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )"(total_order?[real])" nil )nil subrange_inductionsnil ))nil ))nil 3255975799"" (skolem 1 ("F" "high" "low" ))"" (case "low > high" )"1" (expand "sum_it" )"1" (expand "sum_it_def" )"1" (expand "sigma" ) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (expand "sum_it" )"2" (expand "sum_it_def" )"2" (assert )"2" (lemma "sum_it_prop" )"2" (inst -1 "F" "high" "low" "low" )"2" (assert )"2" (rewrite "sigma_eq_arg" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma nil )nil sigma nil )"bool" reals nil )nil sigma nil )"[int -> boolean]" sigma nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integersnil )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]" nil )nil booleans nil )nil numbers nil )"real" sigma nil )"(strict_total_order?[real])" real_props nil )"real" sigma nil )"real" sigma nil )nil sigma nil )"int" integersnil )"(total_order?[real])" nil )nil sigma nil )"int" integersnil ))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.315Bemerkung:
(vorverarbeitet am 2026-04-26)
¤ *Bot Zugriff
2026-05-26
