Impressum sigma_2D.prf
Sprache: Lisp
(sigma_2Dnil 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_2D nil )"T_high" sigma_2D nil )nil integers nil )"(total_order?[real])" nil )nil sigma_2D nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"[int -> boolean]" sigma_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )nil sigma_2D 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_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )"[int -> boolean]" sigma_2D nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil sigma_2D nil )nil sigma_2D nil ))nil ))nil 3352228842"" (skosimp*)"" (inst?)"" (prop) (("" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )nil sigma_2D nil )"(total_order?[real])" nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"T_high" sigma_2D nil )"T_low" sigma_2D 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_2D nil )nil integers nil )"(total_order?[real])" nil )nil sigma_2D nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"[int -> boolean]" sigma_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )nil sigma_2D 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_2D nil )"bool" reals nil )nil sigma_2D nil )"[int -> boolean]" sigma_2D nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )"T_high" sigma_2D nil )"(strict_total_order?[real])" real_props nil )"int" integers nil ))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}" real_defsnil )"int" integers nil )"{j: nonneg_int | j >= i}" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"int" integers nil ))nil ))nil 3411477956"" (skosimp*)"" (assert )"" (typepred "low!1" )"" (typepred "high!1" )"" (ground)"" (skosimp*)"" (assert )"" (typepred "j!1" )"" (typepred "j!2" )"" (lemma "connected_domain" )"" (inst - "j!1" "j!2" "low!1" )"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )nil sigma_2D nil )nil sigma_2D 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]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"[int -> boolean]" sigma_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D 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 )nil vectors_2D nil )"Vector" sigma_2D nil )"(strict_total_order?[real])" real_props nil )"int" integers 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" integers nil )"nat" sigma_2D nil )"nat" sigma_2D nil )nil naturalnumbers nil )"bool" reals nil )"T_low" sigma_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[int -> boolean]" sigma_2D nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"(total_order?[real])" nil ))nil ))nil 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" integers nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"[int -> boolean]" sigma_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )"bool" reals nil )nil naturalnumbers nil ))nil ))nil 3255975799"" (induct "rng" )"1" (skosimp*)"1" (assert )"1" (expand "sigma" 1 3) (("1" (assert ) nil 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 )"2" (replace -2)"2" (hide -2)"2" (apply-extensionality 1 :hide? t)"1" (grind) nil nil ) ("2" (grind) nil nil )"3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*)"3" (inst + "low!1" )"1" (assert ) nil nil )"2" (typepred "low!1" )"2" (assert )"2" (skosimp*)"2" (lemma "connected_domain" )"2" (inst - "j!1" "low!1 + nn!1 + rng!2" "low!1" )"2" (assert ) nil 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_2D nil )"nat" sigma_2D nil )"nat" sigma_2D nil )NOT const-decl "[bool -> bool]" booleans nil )nil integers nil )nil sigma_2D nil )"T_low" sigma_2D nil )nil sigma_2D nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"real" reals nil )"(total_order?[real])" nil )"posint" nil )"posint" nil )nil vectors_2D nil )nil naturalnumbers nil )"Vector" vectors_2D nil )"Vector" sigma_2D nil )nil sigma_2D nil )"[T, T -> boolean]" equalities nil )nil vectors_2D nil )nil defined_types nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil ))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_2D nil )"(total_order?[real])" nil )"int" integers nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"[int -> boolean]" sigma_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )nil sigma_2D 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" integers nil )"int" integers nil )"(total_order?[real])" nil )"T_low" sigma_2D nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"[int -> boolean]" sigma_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )nil sigma_2D 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" (assert ) 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_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )"[int -> boolean]" sigma_2D nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil vectors_2D nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"Vector" sigma_2D nil )nil sigma_2D nil )nil sigma_2D nil )nil vectors_2D nil )nil naturalnumbers nil )"T_high" sigma_2D nil )"T_low" sigma_2D nil )"int" sigma_2D nil )"bool" reals nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil ))nil ))nil 3255975799"" (skosimp*)"" (lemma "sigma_split" )"" (inst?)"" (inst -1 "z!1" )"" (assert )"" (assert )"" (replace -1)"" (hide -1) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma_2D nil )nil vectors_2D nil )"(total_order?[real])" nil )"int" integers nil )"int" integers nil )nil sigma_2D nil )nil sigma_2D nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil vectors_2D nil )nil sigma_2D nil )"[int -> boolean]" sigma_2D nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3255975799"" (skosimp*)"" (lemma "sigma_diff" )"" (inst -1 "F!1" "high!1" "low!1" "z!1" )"" (assert )"" (replace -1 + rl)"" (assert )"" (expand "-" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil sigma_2D nil )"int" integers nil )"int" integers nil )"(total_order?[real])" nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )"real" reals nil )nil sigma_2D nil )nil sigma_2D nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil vectors_2D nil )nil sigma_2D nil )"[int -> boolean]" sigma_2D nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3255975799"" (skosimp*)"" (expand "sigma" )"" (expand "sigma" ) (("" (assert ) nil nil )) nil )) nil ))nil )"Vector" sigma_2D nil )nil vectors_2D nil ))nil ))nil 3255975799"" (skosimp*) (("" (use "T_pred_lem" ) (("" (assert ) nil nil )) nil ))nil )nil sigma_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )"[int -> boolean]" sigma_2D nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sigma_2D 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" integers nil )"(total_order?[real])" nil )"T_low" sigma_2D nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"[int -> boolean]" sigma_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )nil sigma_2D 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_2D nil )"int" integers nil )"(total_order?[real])" nil )"int" integers nil )"(total_order?[real])" nil )nil sigma_2D nil )nil sigma_2D nil )nil sigma_2D nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil vectors_2D nil )nil sigma_2D nil )"[int -> boolean]" sigma_2D nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 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" integers nil )"(total_order?[real])" nil )"T_high" sigma_2D nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"[int -> boolean]" sigma_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )nil sigma_2D 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_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )"[int -> boolean]" sigma_2D nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sigma_2D nil )"(total_order?[real])" nil )"(total_order?[real])" nil ))nil ))nil 3255975799"" (skosimp*)"" (rewrite "sigma" )"" (assert )"" (expand "sigma" )"" (lift-if)"" (ground)"" (expand "+ " ) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"Vector" sigma_2D nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )nil sigma_2D nil )nil vectors_2D nil )"(strict_total_order?[real])" real_props nil )nil vectors_2D nil )nil vectors_2D nil )"Vector" vectors_2D nil )"(total_order?[real])" nil )"int" integers nil ))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" integers nil )"(total_order?[real])" nil )"T_high" sigma_2D nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"[int -> boolean]" sigma_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )nil sigma_2D nil ))nil 3256039673"" (skosimp*) (("" (inst + "i!1" ) (("" (assert ) nil nil )) nil ))nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"[int -> boolean]" sigma_2D nil )nil sigma_2D nil )"(total_order?[real])" nil )"int" integers nil )"(total_order?[real])" nil ))nil 3256032001"" (skosimp*)"" (lemma "sigma_split" )"" (inst?)"" (inst -1 "i!1" )"" (assert )"" (rewrite "sigma_rew" -)"" (assert )"" (replace -1)"" (hide -1)"" (expand "sigma" 1 1)"" (ground)"" (expand "sigma" )"" expand "+ ") "" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma_2D nil )nil sigma_2D nil )"(strict_total_order?[real])" real_props nil )"Vector" sigma_2D nil )"Vector" vectors_2D nil )"(total_order?[real])" nil )"int" integers nil )"int" integers nil )"(total_order?[real])" nil )nil sigma_2D nil )nil sigma_2D nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil vectors_2D nil )nil sigma_2D nil )"[int -> boolean]" sigma_2D nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3255975799"" (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 )"1" (expand "const_vec" )"1" (expand "*" ) (("1" (propax) nil nil )) nil ))nil ))nil )"2" (use "T_pred_lem" ) (("2" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (expand "sigma" +)"2" (assert )"2" (replace -2)"2" (hide -2) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 3)"3" (skosimp*)"3" (inst + "high!1" )"1" (assert ) nil nil )"2" (use "T_pred_lem" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"int" integers nil )nil sigma_2D nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )nil sigma_2D nil )nil defined_types nil )nil vectors_2D nil )"[T, T -> boolean]" equalities nil )"Vector" sigma_2D nil )"Vector" vectors_2D nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" reals nil )"Vector" vectors_2D nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"Vector" vectors_2D nil )"int" integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"T_low" sigma_2D nil )"T_high" sigma_2D nil )nil integers nil )nil subrange_inductions nil )"(total_order?[real])" nil )nil sigma_2D nil )"(total_order?[real])" nil )nil vectors_2D nil )nil sigma_2D nil )"real" reals nil )"real" reals nil )"real" reals nil )"Vector" vectors_2D nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3255975799"" (skosimp*)"" (lemma "sigma_const" )"" (inst - "high!1" "low!1" "0" )"" (assert )"" (case-replace "const_vec(0) = zero" )"1" (assert ) nil nil )"2" (invoke (hide ($+n)) (? * "sigma" ))"2" (expand "const_vec" )"2" (expand "zero" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma_2D nil )"int" integers nil )"(total_order?[real])" nil )nil vectors_2D nil )"int" integers nil )nil vectors_2D nil )"[T, T -> boolean]" equalities nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )nil sigma_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )"[int -> boolean]" sigma_2D nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers 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 )"2" (replace -2 * lr)"2" (hide -2)"2" (apply-extensionality 1 :hide? t)"1" (grind) nil nil )"2" (grind) nil nil )"3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*)"3" (inst + "high!1" )"1" (assert ) nil nil )"2" (use "T_pred_lem" ) (("2" (assert ) nil nil ))nil ))nil ))nil )"4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma_2D nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )nil sigma_2D nil )nil defined_types nil )nil vectors_2D nil )"[T, T -> boolean]" equalities nil )"Vector" sigma_2D nil )"Vector" vectors_2D nil )AND const-decl "[bool, bool -> bool]" booleans nil )"T_low" sigma_2D nil )"T_high" sigma_2D nil )nil integers nil )nil subrange_inductions nil )"(total_order?[real])" nil )"bool" reals nil )nil sigma_2D nil )"(total_order?[real])" nil )nil sigma_2D nil )"int" integers nil )"real" reals nil )"int" integers nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"Vector" vectors_2D nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil vectors_2D 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_2D nil )"int" integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"T" sigma_2D nil )"int" sigma_2D nil )"(total_order?[real])" nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"[int -> boolean]" sigma_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D 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_2D nil )"int" integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"T" sigma_2D nil )"int" sigma_2D nil )"(total_order?[real])" nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"[int -> boolean]" sigma_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D 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]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"int" integers nil ))nil ))nil 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" (inst + "j!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (hide -1 2 3)"5" (skosimp* t)"5" (typepred "high!1" )"5" (prop)"1" (inst + "high!1+z" )"1" (assert ) nil nil ) ("2" (inst?) nil nil ))nil )"2" (skosimp*)"2" (inst + "j!1+z" )"1" (assert ) nil nil )"2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" (hide -1 2 3)"6" (skosimp* t)"6" (assert )"6" (typepred "low!1" )"6" (prop)"1" (inst?) nil nil )"2" (skosimp*)"2" (inst + "j!1+z" )"1" (assert ) nil nil )"2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"7" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (skosimp*) nil nil )"3" (hide 2)"3" (skosimp* t)"3" (hide -1 -4)"3" (assert )"3" (prop)"1" (typepred "high!1" )"1" (prop)"1" (assert ) (("1" (inst?) nil nil )) nil )"2" (skosimp*)"2" (inst + "j!1+z" )"1" (assert ) nil nil ) ("2" (inst?) nil nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (typepred "high!1" )"2" (prop)"1" (inst?) nil nil )"2" (skosimp*)"2" (inst + "j!2+z" )"1" (assert ) nil nil )"2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide 2)"4" (skosimp* t)"4" (hide -1)"4" (inst?)"4" (assert )"4" (skosimp*)"4" (reveal -1)"4" (inst + "j!1+z" )"1" (assert ) nil nil ) ("2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"int" integers nil )nil sigma_2D nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )nil sigma_2D nil )nil defined_types nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_2D nil )"[T, T -> boolean]" equalities nil )"Vector" sigma_2D nil )AND const-decl "[bool, bool -> bool]" booleans nil )"T_low" sigma_2D nil )"T_high" sigma_2D nil )nil integers nil )"int" sigma_2D nil )nil subrange_inductions nil )"(total_order?[real])" nil )"bool" reals nil )nil sigma_2D nil )"(total_order?[real])" nil )nil sigma_2D nil )NOT const-decl "[bool -> bool]" booleans nil )"T" sigma_2D nil )"T" sigma_2D nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"T_high" sigma_2D nil )"T" sigma_2D nil )"T" sigma_2D nil )"T_low" sigma_2D nil )"T" sigma_2D 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)"1" (replace -1) (("1" (propax) nil nil ))nil )"2" (invoke (hide ($+n)) (? * "sigma" ))"2" (lemma "connected_domain" )"2" (inst?)"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" (skosimp*)"3" (assert )"3" (use "T_pred_lem" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide-all-but 1) (("4" (skosimp*) nil nil )) nil )"5" (hide-all-but 1) (("5" (skosimp*) nil nil )) nil )"6" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2) (("2" (skosimp*) nil nil )) nil )"3" (hide 2) (("3" (skosimp*) nil nil )) nil ))nil ))nil )"int" integers nil )nil sigma_2D nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )nil sigma_2D nil )nil defined_types nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_2D nil )"[T, T -> boolean]" equalities nil )"Vector" sigma_2D nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"Vector" vectors_2D nil )"T_low" sigma_2D nil )"T_high" sigma_2D nil )nil integers nil )"int" sigma_2D nil )nil subrange_inductions nil )"(total_order?[real])" nil )"bool" reals nil )nil sigma_2D nil )"(total_order?[real])" nil )nil sigma_2D nil )nil integers nil )nil sigma_2D nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3411479595"" (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" (replace -2 + rl)"2" (hide -2) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (skosimp* t)"3" (typepred "high!1" )"3" (inst + "high!1" )"3" (assert )"3" (skosimp*)"3" (use "T_pred_lem" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma_2D nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )nil sigma_2D nil )nil defined_types nil )nil vectors_2D nil )"[T, T -> boolean]" equalities nil )"Vector" vectors_2D nil )"Vector" sigma_2D nil )AND const-decl "[bool, bool -> bool]" booleans nil )"T_low" sigma_2D nil )"T_high" sigma_2D nil )nil integers nil )nil subrange_inductions nil )"(total_order?[real])" nil )"bool" reals nil )nil sigma_2D nil )"(total_order?[real])" nil )nil sigma_2D nil )"real" reals nil )"int" integers nil )"int" integers nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil vectors_2D 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" (replace -2 + rl)"2" (hide -2)"2" (apply-extensionality 1 :hide? t)"1" (grind) nil nil ) ("2" (grind) nil nil )"3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (skosimp* t)"3" (typepred "high!1" )"3" (inst + "high!1" )"3" (assert )"3" (skosimp*)"3" (use "T_pred_lem" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil ))nil 3255975799"" (skolem 1 ("F" "G" _ _))"" (rewrite "high_low_rewrite" )"" (hide 2)"" (skosimp*)"" (prop)"1" (expand "sigma" )"1" (assert )"1" (expand "zero" )"1" (expand "-" ) (("1" (propax) nil nil )) nil ))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" (replace -2 + rl)"2" (hide -2)"2" (expand "+ " )"2" (expand "-" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (skosimp* t)"3" (typepred "high!1" )"3" (inst + "high!1" )"3" (assert )"3" (skosimp*)"3" (use "T_pred_lem" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma_2D nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )nil sigma_2D nil )nil defined_types nil )nil vectors_2D nil )"[T, T -> boolean]" equalities nil )"Vector" vectors_2D nil )"Vector" sigma_2D nil )AND const-decl "[bool, bool -> bool]" booleans nil )"T_low" sigma_2D nil )"T_high" sigma_2D nil )nil integers nil )nil subrange_inductions nil )"(total_order?[real])" nil )"bool" reals nil )nil sigma_2D nil )"(total_order?[real])" nil )nil sigma_2D nil )"Vector" vectors_2D nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil vectors_2D nil )nil vectors_2D 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_2D nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[int -> boolean]" sigma_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )nil sigma_2D nil )nil defined_types nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil vectors_2D nil )"[T, T -> boolean]" equalities nil )"Vector" sigma_2D nil )"[T -> Vector]" sigma_2D nil )"T_low" sigma_2D nil )"T_high" sigma_2D nil )nil integers nil )"T" sigma_2D nil )"T" sigma_2D nil )nil subrange_inductions nil )nil sigma_2D nil )nil sigma_2D nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"(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_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )"[int -> boolean]" sigma_2D nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"Vector" sigma_2D nil )nil sigma_2D nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil vectors_2D nil )nil sigma_2D 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_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )"[int -> boolean]" sigma_2D nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"Vector" sigma_2D nil )nil vectors_2D nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil sigma_2D nil )"T_low" sigma_2D nil )"T_high" sigma_2D nil )nil sigma_2D nil ))nil ))nil 3411477956"" (skosimp*)"" (typepred "n!1" )"" (typepred "low!1" )"" (typepred "high!1" )"" (lemma "connected_domain" )"" (ground)"1" (inst - "low!1" "high!1" "n!1" )"1" (assert ) nil nil )) nil )"2" (skosimp*)"2" (inst - "j!1" "high!1" "n!1" )"2" (assert ) nil nil )) nil ))nil )"3" (skosimp*)"3" (inst - "low!1" "j!1" "n!1" )"3" (assert ) nil nil )) nil ))nil )"4" (skosimp*)"4" (inst - "j!1" "j!2" "n!1" )"4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integers nil )nil sigma_2D nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil sigma_2D nil )nil sigma_2D nil )"[int -> boolean]" sigma_2D nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )nil integers nil )nil sigma_2D nil ))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_2D nil )"[T -> Vector]" sigma_2D nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" reals nil ) (> const-decl "bool" reals nil )"Vector" vectors_2D nil )nil sigma_2D nil )nil sigma_2D nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil vectors_2D nil )nil sigma_2D nil )"[int -> boolean]" sigma_2D nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3411479877"" (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" (replace -1)"1" (replace -5)"1" (hide -1 -5)"1" (assert )"1" (replace -1)"1" (assert )"1" (lemma "sigma_eq" )"1" (inst?)"1" "G!1" )"1" assert )"1" replace -1)"1" "1" rewrite "add_comm" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))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" (lemma "sigma_eq" )"1" (inst?)"1" "G!1" )"1" (assert ) nil nil ))nil ))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" (inst -1 "G!1" "high!1" "low!1" "i!1" )"2" (assert )"2" (replace -1)"2" (hide -1)"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 := v!1]) = sigma(low!1, i!1 - 1, G!1)" )"1" "1" case "sigma(1 + i!1, high!1, G!1 WITH [i!1 := v!1]) = sigma(1 + i!1, high!1, G!1 )" )"1" replace "1" "1" expand "+ " )"1" assert )"1" expand "-" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "sigma_eq" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "sigma_eq" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma_2D nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil sigma_2D nil )"[int -> boolean]" sigma_2D nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )nil vectors_2D nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil vectors_2D nil )"Vector" sigma_2D nil )nil sigma_2D nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"int" integers nil )nil sigma_2D nil )nil vectors_2D nil )nil sigma_2D nil )nil sigma_2D nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )"real" reals nil )nil sigma_2D nil )"int" integers nil )nil vectors_2D nil )"[numfield, numfield -> numfield]" number_fieldsnil ))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" (inst -1 "G!1" "high!1" "low!1" "i!1" )"2" (assert )"2" (replace -1)"2" (hide -1)"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 nil ))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_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )"[int -> boolean]" sigma_2D nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )nil sigma_2D nil )nil sigma_2D nil ))nil ))nil 3255975799"" (skosimp*) (("" (use "T_pred_lem" ) (("" (assert ) nil nil )) nil ))nil )nil sigma_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )"[int -> boolean]" sigma_2D nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sigma_2D nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil ))nil 3352118808 ("" (subtype-tcc) nil nil )"int" integers nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"[int -> boolean]" sigma_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )nil sigma_2D nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"{j: nonneg_int | j >= i}" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"int" integers nil ))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" integers nil )"int" integers nil )"(total_order?[real])" nil )"T_low" sigma_2D nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"[int -> boolean]" sigma_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )nil sigma_2D 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" (expand "+ " ) (("2" (propax) nil 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" (rewrite "add_comm" -4) nil nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-3 1))"2" (lemma "T_pred_lem" )"2" (inst?)"2" (inst - "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" (inst - "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_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )"[int -> boolean]" sigma_2D nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"Vector" sigma_2D nil )"Vector" sigma_2D nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"T_high" sigma_2D nil )"T_low" sigma_2D nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil defined_types nil )"bool" booleans nil )"R" extend nil )nil vectors_2D nil )"[T, T -> boolean]" equalities nil )"(strict_total_order?[real])" real_props nil )"T" sigma_2D nil )"Vector" vectors_2D nil )nil sigma_2D nil )"odd_int" integers nil )nil vectors_2D nil )"{lh: T | low!1 <= lh AND lh <= high!1}" nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )"(total_order?[real])" nil )nil subrange_inductions nil ))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_2D nil )nil sigma_2D nil )"bool" reals nil )nil sigma_2D nil )"[int -> boolean]" sigma_2D nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"Vector" sigma_2D nil )"(strict_total_order?[real])" real_props nil )"Vector" sigma_2D nil )"Vector" sigma_2D nil )nil sigma_2D nil )"int" integers nil )"(total_order?[real])" nil )nil sigma_2D nil )nil vectors_2D nil )nil vectors_2D nil )"int" integers nil ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.97 Sekunden
(vorverarbeitet am 2026-04-26)
¤ *© Formatika GbR, Deutschland
2026-05-26
