| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/reals/ (PVS Prover Version 6.0.9©) Datei vom 28.9.2014 mit Größe 166 kB |
|
Impressum old_sigma.prf Sprache: Lisp |
|||||||||||||||
|
(old_sigma (T_pred_lem 0 (T_pred_lem-1 nil 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) ((low!1 skolem-const-decl "T_low" old_sigma nil) (high!1 skolem-const-decl "T_high" old_sigma nil) (integer nonempty-type-from-decl nil integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (connected_domain formula-decl nil old_sigma nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil)) shostak)) (high_low_rewrite_TCC1 0 (high_low_rewrite_TCC1-1 nil 3352229091 ("" (skosimp*) (("" (inst + "high!1") (("1" (assert) nil nil) ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil)) nil)) nil) ((high!1 skolem-const-decl "T_high" old_sigma nil) (T_high type-eq-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil old_sigma nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (T_low type-eq-decl nil old_sigma nil) (T_pred_lem formula-decl nil old_sigma nil)) nil)) (high_low_rewrite 0 (high_low_rewrite-1 nil 3352228842 ("" (skosimp*) (("" (inst?) (("" (prop) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (high!1 skolem-const-decl "T_high" old_sigma nil) (low!1 skolem-const-decl "T_low" old_sigma nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (sigma_TCC1 0 (sigma_TCC1-1 nil 3255975799 ("" (skosimp*) (("" (use "T_pred_lem") (("" (assert) nil nil)) nil)) nil) ((T_pred_lem formula-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil old_sigma nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (T_high type-eq-decl nil old_sigma nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (sigma_TCC2 0 (sigma_TCC2-1 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) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (low!1 skolem-const-decl "T_low" old_sigma nil) (integer nonempty-type-from-decl nil integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (connected_domain formula-decl nil old_sigma nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil old_sigma nil) (T_high type-eq-decl nil old_sigma nil)) nil)) (sigma_TCC3 0 (sigma_TCC3-1 nil 3255975799 ("" (skosimp*) (("" (assert) (("" (typepred "high!1") (("" (prop) (("1" (inst 4 "high!1") (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (inst 4 "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (high!1 skolem-const-decl "T_high" old_sigma nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil old_sigma nil)) nil)) (sigma_TCC4 0 (sigma_TCC4-2 nil 3351941985 ("" (skosimp*) (("" (grind) nil nil)) nil) ((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (minus_int_is_int application-judgement "int" integers nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil) (sigma_TCC4-1 nil 3255975799 ("" (skosimp*) (("" (assert) nil nil)) nil) nil nil)) (sigma_rew_TCC1 0 (sigma_rew_TCC1-1 nil 3352522153 ("" (skosimp*) (("" (assert) (("" (lemma "T_pred_lem") (("" (inst - "high!1" "low!1" "high!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (T_pred_lem formula-decl nil old_sigma nil)) nil)) (sigma_rew_TCC2 0 (sigma_rew_TCC2-1 nil 3352522153 ("" (skosimp*) (("" (typepred "high!1") (("" (prop) (("1" (inst + "high!1") (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((T_high type-eq-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil old_sigma nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (high!1 skolem-const-decl "T_high" old_sigma nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (sigma_rew 0 (sigma_rew-1 nil 3352522445 ("" (skosimp*) (("" (grind) nil nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma def-decl "real" old_sigma nil)) shostak)) (sigma_spl_TCC1 0 (sigma_spl_TCC1-1 nil 3255975799 ("" (skosimp*) (("" (inst + "low!1 + nn!1 + rng!1") (("" (assert) nil nil)) nil)) nil) nil nil)) (sigma_spl_TCC2 0 (sigma_spl_TCC2-1 nil 3255975799 ("" (skosimp*) (("" (inst + "low!1 + nn!1 + rng!1") (("" (assert) nil nil)) nil)) nil) ((int_plus_int_is_int application-judgement "int" integers nil) (rng!1 skolem-const-decl "nat" old_sigma nil) (nn!1 skolem-const-decl "nat" old_sigma nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (low!1 skolem-const-decl "T_low" old_sigma nil) (T_low type-eq-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil old_sigma nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (sigma_spl_TCC3 0 (sigma_spl_TCC3-1 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) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil old_sigma nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) nil)) (sigma_spl 0 (sigma_spl-1 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) (("2" (lift-if) (("2" (ground) nil nil)) 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) ((low!1 skolem-const-decl "T_low" old_sigma nil) (nn!1 skolem-const-decl "nat" old_sigma nil) (rng!2 skolem-const-decl "nat" old_sigma nil) (low!1 skolem-const-decl "T_low" old_sigma nil) (nn!1 skolem-const-decl "nat" old_sigma nil) (rng!2 skolem-const-decl "nat" old_sigma nil) (T_pred_lem formula-decl nil old_sigma nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nat_induction formula-decl nil naturalnumbers nil) (sigma def-decl "real" old_sigma nil) (T_high type-eq-decl nil old_sigma nil) (= const-decl "[T, T -> boolean]" equalities nil) (pred type-eq-decl nil defined_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil old_sigma nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil)) (sigma_split_TCC1 0 (sigma_split_TCC1-1 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) ((high!1 skolem-const-decl "T_high" old_sigma nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil)) nil)) (sigma_split_TCC2 0 (sigma_split_TCC2-1 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_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (low!1 skolem-const-decl "T_low" old_sigma nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil)) nil)) (sigma_split 0 (sigma_split-1 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) ((T_low type-eq-decl nil old_sigma nil) (T_high type-eq-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil old_sigma nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma def-decl "real" old_sigma nil) (sigma_spl formula-decl nil old_sigma nil) (T_pred_lem formula-decl nil old_sigma nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (high!1 skolem-const-decl "T_high" old_sigma nil) (low!1 skolem-const-decl "T_low" old_sigma nil) (z!1 skolem-const-decl "int" old_sigma nil) (>= const-decl "bool" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil)) nil)) (sigma_diff 0 (sigma_diff-1 nil 3255975799 ("" (skosimp*) (("" (lemma "sigma_split") (("" (inst?) (("" (inst -1 "z!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((sigma_split formula-decl nil old_sigma nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (int_plus_int_is_int application-judgement "int" integers nil) (T_low type-eq-decl nil old_sigma nil) (T_high type-eq-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (T formal-subtype-decl nil old_sigma nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil)) (sigma_diff_neg 0 (sigma_diff_neg-1 nil 3255975799 ("" (skosimp*) (("" (lemma "sigma_diff") (("" (inst -1 "F!1" "high!1" "low!1" "z!1") (("" (assert) nil nil)) nil)) nil)) nil) ((sigma_diff formula-decl nil old_sigma nil) (int_plus_int_is_int application-judgement "int" integers nil) (minus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (T_low type-eq-decl nil old_sigma nil) (T_high type-eq-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (T formal-subtype-decl nil old_sigma nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil)) (sigma_eq_arg 0 (sigma_eq_arg-1 nil 3255975799 ("" (skosimp*) (("" (expand "sigma") (("" (expand "sigma") (("" (propax) nil nil)) nil)) nil)) nil) ((sigma def-decl "real" old_sigma nil)) nil)) (sigma_first_TCC1 0 (sigma_first_TCC1-1 nil 3255975799 ("" (skosimp*) (("" (use "T_pred_lem") (("" (assert) nil nil)) nil)) nil) ((T_pred_lem formula-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil old_sigma nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (T_high type-eq-decl nil old_sigma nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (sigma_first_TCC2 0 (sigma_first_TCC2-1 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) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (low!1 skolem-const-decl "T_low" old_sigma nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil)) nil)) (sigma_first 0 (sigma_first-1 nil 3255975799 ("" (skosimp*) (("" (lemma "sigma_split") (("" (inst?) (("" (inst -1 "low!1") (("" (rewrite "sigma_eq_arg") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((sigma_split formula-decl nil old_sigma nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_eq_arg formula-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil) (T_high type-eq-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (T formal-subtype-decl nil old_sigma nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil)) (sigma_last_TCC1 0 (sigma_last_TCC1-2 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) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (high!1 skolem-const-decl "T_high" old_sigma nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil)) nil) (sigma_last_TCC1-1 nil 3255975799 ("" (skosimp*) (("" (typepred "high!1") (("" (skosimp*) (("" (inst + "j!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil) nil nil)) (sigma_last_TCC2 0 (sigma_last_TCC2-1 nil 3351939915 ("" (skosimp*) (("" (use "T_pred_lem") (("" (assert) nil nil)) nil)) nil) ((T_pred_lem formula-decl nil old_sigma nil) (T_high type-eq-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil old_sigma nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (T_low type-eq-decl nil old_sigma nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (sigma_last 0 (sigma_last-1 nil 3255975799 ("" (skosimp*) (("" (rewrite "sigma") (("" (assert) (("" (lift-if) (("" (ground) (("" (expand "sigma") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma def-decl "real" old_sigma nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil old_sigma nil) (T_high type-eq-decl nil old_sigma nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (sigma_middle_TCC1 0 (sigma_middle_TCC1-1 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) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (high!1 skolem-const-decl "T_high" old_sigma nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil)) shostak)) (sigma_middle_TCC2 0 (sigma_middle_TCC2-1 nil 3256039673 ("" (skosimp*) (("" (inst + "i!1") (("" (assert) nil nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (sigma_middle 0 (sigma_middle-1 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) (("" (lift-if) (("" (ground) (("" (expand "sigma") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma_split formula-decl nil old_sigma nil) (sigma_rew formula-decl nil old_sigma nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma def-decl "real" old_sigma nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (T_low type-eq-decl nil old_sigma nil) (T_high type-eq-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (T formal-subtype-decl nil old_sigma nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (sigma_const 0 (sigma_const-1 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) ((high_low_rewrite formula-decl nil old_sigma nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil) (pred type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (sigma def-decl "real" old_sigma nil) (numfield nonempty-type-eq-decl nil number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (>= const-decl "bool" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (low!1 skolem-const-decl "T_low" old_sigma nil) (high!1 skolem-const-decl "T_high" old_sigma nil) (subrange type-eq-decl nil integers nil) (subrange_induction formula-decl nil subrange_inductions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (T_pred_lem formula-decl nil old_sigma nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (sigma_eq_arg formula-decl nil old_sigma nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (sigma_zero 0 (sigma_zero-1 nil 3255975799 ("" (skosimp*) (("" (rewrite "sigma_const") nil nil)) nil) ((mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (int_times_even_is_even application-judgement "even_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_const formula-decl nil old_sigma nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil)) nil)) (sigma_scal 0 (sigma_scal-1 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_times_real_is_real application-judgement "real" reals nil) (high_low_rewrite formula-decl nil old_sigma nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil) (pred type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (sigma def-decl "real" old_sigma nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (low!1 skolem-const-decl "T_low" old_sigma nil) (high!1 skolem-const-decl "T_high" old_sigma nil) (subrange type-eq-decl nil integers nil) (subrange_induction formula-decl nil subrange_inductions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (>= const-decl "bool" reals nil) (T_pred_lem formula-decl nil old_sigma nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_eq_arg formula-decl nil old_sigma nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (sigma_bound 0 (sigma_bound-1 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" (inst?) (("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" (prop) (("1" (inst + "high!1") nil nil) ("2" (skosimp*) (("2" (inst + "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_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (high_low_rewrite formula-decl nil old_sigma nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (>= const-decl "bool" reals nil) (sigma def-decl "real" old_sigma nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_plus_real_is_real application-judgement "real" reals nil) (low!1 skolem-const-decl "T_low" old_sigma nil) (high!1 skolem-const-decl "T_high" old_sigma nil) (subrange type-eq-decl nil integers nil) (F skolem-const-decl "[T -> real]" old_sigma nil) (B skolem-const-decl "real" old_sigma nil) (subrange_induction formula-decl nil subrange_inductions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_eq_arg formula-decl nil old_sigma nil) (T_pred_lem formula-decl nil old_sigma nil) (int_plus_int_is_int application-judgement "int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (sigma_abs 0 (sigma_abs-1 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) ((high_low_rewrite formula-decl nil old_sigma nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil) (pred type-eq-decl nil defined_types nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (sigma def-decl "real" old_sigma nil) (low!1 skolem-const-decl "T_low" old_sigma nil) (high!1 skolem-const-decl "T_high" old_sigma nil) (subrange type-eq-decl nil integers nil) (subrange_induction formula-decl nil subrange_inductions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (T_pred_lem formula-decl nil old_sigma nil) (sigma_eq_arg formula-decl nil old_sigma nil) (triangle formula-decl nil real_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (sigma_ge_0_TCC1 0 (sigma_ge_0_TCC1-1 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) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (T_pred_lem formula-decl nil old_sigma nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil)) nil)) (sigma_ge_0 0 (sigma_ge_0-1 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) ((high_low_rewrite formula-decl nil old_sigma nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (sigma def-decl "real" old_sigma nil) (low!1 skolem-const-decl "T_low" old_sigma nil) (high!1 skolem-const-decl "T_high" old_sigma nil) (F skolem-const-decl "[T -> real]" old_sigma nil) (subrange_induction formula-decl nil subrange_inductions nil) (sigma_eq_arg formula-decl nil old_sigma nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (T_pred_lem formula-decl nil old_sigma nil) (real_plus_real_is_real application-judgement "real" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (sigma_gt_0 0 (sigma_gt_0-1 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" (use "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) ((high_low_rewrite formula-decl nil old_sigma nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (sigma def-decl "real" old_sigma nil) (low!1 skolem-const-decl "T_low" old_sigma nil) (high!1 skolem-const-decl "T_high" old_sigma nil) (F skolem-const-decl "[T -> real]" old_sigma nil) (subrange_induction formula-decl nil subrange_inductions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (>= const-decl "bool" reals nil) (T_pred_lem formula-decl nil old_sigma nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma_eq_arg formula-decl nil old_sigma nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil)) nil)) (sigma_shift_T_TCC1 0 (sigma_shift_T_TCC1-1 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) ((low!1 skolem-const-decl "T_low" old_sigma nil) (int_plus_int_is_int application-judgement "int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (j!1 skolem-const-decl "T" old_sigma nil) (z!1 skolem-const-decl "int" old_sigma nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil old_sigma nil)) nil)) (sigma_shift_T_TCC2 0 (sigma_shift_T_TCC2-1 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) ((high!1 skolem-const-decl "T_high" old_sigma nil) (int_plus_int_is_int application-judgement "int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (j!1 skolem-const-decl "T" old_sigma nil) (z!1 skolem-const-decl "int" old_sigma nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil old_sigma nil)) nil)) (sigma_shift_T_TCC3 0 (sigma_shift_T_TCC3-1 nil 3352113941 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil)) (sigma_shift_T 0 (sigma_shift_T-1 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_plus_int_is_int application-judgement "int" integers nil) (high_low_rewrite formula-decl nil old_sigma nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (sigma def-decl "real" old_sigma nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (low!1 skolem-const-decl "T_low" old_sigma nil) (high!1 skolem-const-decl "T_high" old_sigma nil) (subrange type-eq-decl nil integers nil) (z skolem-const-decl "int" old_sigma nil) (subrange_induction formula-decl nil subrange_inductions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (>= const-decl "bool" reals nil) (sigma_eq_arg formula-decl nil old_sigma nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (T_pred_lem formula-decl nil old_sigma nil) (NOT const-decl "[bool -> bool]" booleans nil) (j!1 skolem-const-decl "T" old_sigma nil) (j!1 skolem-const-decl "T" old_sigma nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (high!1 skolem-const-decl "T_high" old_sigma nil) (j!2 skolem-const-decl "T" old_sigma nil) (j!1 skolem-const-decl "T" old_sigma nil) (low!1 skolem-const-decl "T_low" old_sigma nil) (j!1 skolem-const-decl "T" old_sigma nil)) nil)) (sigma_shift_T2_TCC1 0 (sigma_shift_T2_TCC1-2 nil 3351941788 ("" (skosimp*) (("" (inst + "low!1+z!1") (("" (assert) nil nil)) nil)) nil) nil nil) (sigma_shift_T2_TCC1-1 nil 3351939915 ("" (skosimp*) (("" (typepred "high!1") (("" (skosimp*) (("" (inst + "z!1+high!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil) nil nil)) (sigma_shift_T2_TCC2 0 (sigma_shift_T2_TCC2-1 nil 3352113941 ("" (skosimp*) (("" (inst + "high!1+z!1") (("" (assert) nil nil)) nil)) nil) nil nil)) (sigma_shift_T2 0 (sigma_shift_T2-1 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" (hide -1 2) (("2" (lemma "connected_domain") (("2" (inst?) (("2" (inst - "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_plus_int_is_int application-judgement "int" integers nil) (high_low_rewrite formula-decl nil old_sigma nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (sigma def-decl "real" old_sigma nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (low!1 skolem-const-decl "T_low" old_sigma nil) (high!1 skolem-const-decl "T_high" old_sigma nil) (subrange type-eq-decl nil integers nil) (z skolem-const-decl "int" old_sigma nil) (subrange_induction formula-decl nil subrange_inductions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (>= const-decl "bool" reals nil) (sigma_eq_arg formula-decl nil old_sigma nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (T_pred_lem formula-decl nil old_sigma nil) (real_plus_real_is_real application-judgement "real" reals nil) (integer nonempty-type-from-decl nil integers nil) (connected_domain formula-decl nil old_sigma nil) (NOT const-decl "[bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (sigma_sum 0 (sigma_sum-1 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" (skosimp*) (("3" (use "T_pred_lem") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_plus_real_is_real application-judgement "real" reals nil) (high_low_rewrite formula-decl nil old_sigma nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil) (pred type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma def-decl "real" old_sigma nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (low!1 skolem-const-decl "T_low" old_sigma nil) (high!1 skolem-const-decl "T_high" old_sigma nil) (subrange type-eq-decl nil integers nil) (subrange_induction formula-decl nil subrange_inductions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (>= const-decl "bool" reals nil) (T_pred_lem formula-decl nil old_sigma nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_eq_arg formula-decl nil old_sigma nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (sigma_minus 0 (sigma_minus-1 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" (skosimp*) (("3" (use "T_pred_lem") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil) (high_low_rewrite formula-decl nil old_sigma nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil) (pred type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma def-decl "real" old_sigma nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (low!1 skolem-const-decl "T_low" old_sigma nil) (high!1 skolem-const-decl "T_high" old_sigma nil) (subrange type-eq-decl nil integers nil) (subrange_induction formula-decl nil subrange_inductions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (>= const-decl "bool" reals nil) (T_pred_lem formula-decl nil old_sigma nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma_eq_arg formula-decl nil old_sigma nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (sigma_abs_bnd 0 (sigma_abs_bnd-1 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" (skosimp*) (("3" (use "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" (inst?) (("2" (inst - "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) ((high_low_rewrite formula-decl nil old_sigma nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (sigma def-decl "real" old_sigma nil) (low!1 skolem-const-decl "T_low" old_sigma nil) (high!1 skolem-const-decl "T_high" old_sigma nil) (F skolem-const-decl "[T -> real]" old_sigma nil) (G skolem-const-decl "[T -> real]" old_sigma nil) (subrange_induction formula-decl nil subrange_inductions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_eq_arg formula-decl nil old_sigma nil) (T_pred_lem formula-decl nil old_sigma nil) (real_plus_real_is_real application-judgement "real" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (sigma_restrict 0 (sigma_restrict-1 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) ((high_low_rewrite formula-decl nil old_sigma nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (>= const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (sigma def-decl "real" old_sigma nil) (restrict const-decl "[T -> real]" old_sigma nil) (low!1 skolem-const-decl "T_low" old_sigma nil) (high!1 skolem-const-decl "T_high" old_sigma nil) (subrange type-eq-decl nil integers nil) (l skolem-const-decl "T" old_sigma nil) (h skolem-const-decl "T" old_sigma nil) (subrange_induction formula-decl nil subrange_inductions nil) (T_pred_lem formula-decl nil old_sigma nil) (sigma_eq_arg formula-decl nil old_sigma nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (sigma_restrict_to 0 (sigma_restrict_to-1 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) ((T_low type-eq-decl nil old_sigma nil) (T_high type-eq-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil old_sigma nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma def-decl "real" old_sigma nil) (T_pred_lem formula-decl nil old_sigma nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_restrict formula-decl nil old_sigma nil)) nil)) (sigma_restrict_eq 0 (sigma_restrict_eq-1 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" (inst -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) ((T_low type-eq-decl nil old_sigma nil) (T_high type-eq-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil old_sigma nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma def-decl "real" old_sigma nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (T_pred_lem formula-decl nil old_sigma nil) (low!1 skolem-const-decl "T_low" old_sigma nil) (high!1 skolem-const-decl "T_high" old_sigma nil) (sigma_restrict formula-decl nil old_sigma nil)) nil)) (sigma_eq 0 (sigma_eq-1 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) ((sigma_restrict_eq formula-decl nil old_sigma nil) (restrict const-decl "[T -> real]" old_sigma nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (< const-decl "bool" reals nil) (> const-decl "bool" reals nil) (T_low type-eq-decl nil old_sigma nil) (T_high type-eq-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (T formal-subtype-decl nil old_sigma nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil)) (sigma_le 0 (sigma_le-1 nil 3255975799 ("" (skosimp*) (("" (lemma "sigma_ge_0") (("" (inst -1 "(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) ((sigma_ge_0 formula-decl nil old_sigma nil) (sigma_minus formula-decl nil old_sigma nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (subrange type-eq-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (T_low type-eq-decl nil old_sigma nil) (T_high type-eq-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (T formal-subtype-decl nil old_sigma nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (sigma_lt 0 (sigma_lt-1 nil 3255975799 ("" (skosimp*) (("" (lemma "sigma_gt_0") (("" (inst -1 "(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) ((sigma_gt_0 formula-decl nil old_sigma nil) (sigma_minus formula-decl nil old_sigma nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (T_low type-eq-decl nil old_sigma nil) (T_high type-eq-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (T formal-subtype-decl nil old_sigma nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (sigma_with 0 (sigma_with-1 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" (lemma "sigma_last") (("2" (inst-cp -1 "F!1" "i!1" "low!1") (("2" (inst -1 "G!1" "i!1" "low!1") (("2" (assert) (("2" (replace -1) (("2" (hide -1) (("2" (replace -1) (("2" (hide -1) (("2" (replace -3) (("2" (hide -3) (("2" (ground) (("2" (case-replace "sigma(low!1, i!1 - 1, G!1 WITH [i!1 := a!1]) = sigma(low!1, i!1 - 1, G!1)") (("1" (hide -1) (("1" (assert) (("1" (rewrite "sigma_eq") nil nil)) nil)) nil) ("2" (hide 4) (("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) ((T_low type-eq-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (T formal-subtype-decl nil old_sigma nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sigma_eq formula-decl nil old_sigma nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (T_high type-eq-decl nil old_sigma nil) (sigma_first formula-decl nil old_sigma nil) (sigma_split formula-decl nil old_sigma nil) (sigma def-decl "real" old_sigma nil) (sigma_last formula-decl nil old_sigma nil) (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil)) nil)) (sigma_nonneg 0 (sigma_nonneg-1 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) ((high_low_rewrite formula-decl nil old_sigma nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (>= const-decl "bool" reals nil) (sigma def-decl "real" old_sigma nil) (F skolem-const-decl "[T -> real]" old_sigma nil) (subrange type-eq-decl nil integers nil) (high!1 skolem-const-decl "T_high" old_sigma nil) (low!1 skolem-const-decl "T_low" old_sigma nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange_induction formula-decl nil subrange_inductions nil) (T_pred_lem formula-decl nil old_sigma nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_eq_arg formula-decl nil old_sigma nil) (real_plus_real_is_real application-judgement "real" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_plus_int_is_int application-judgement "int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (sigma_nonpos 0 (sigma_nonpos-2 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) ((high_low_rewrite formula-decl nil old_sigma nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (sigma def-decl "real" old_sigma nil) (F skolem-const-decl "[T -> real]" old_sigma nil) (subrange type-eq-decl nil integers nil) (high!1 skolem-const-decl "T_high" old_sigma nil) (low!1 skolem-const-decl "T_low" old_sigma nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange_induction formula-decl nil subrange_inductions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (>= const-decl "bool" reals nil) (T_pred_lem formula-decl nil old_sigma nil) (sigma_eq_arg formula-decl nil old_sigma nil) (real_plus_real_is_real application-judgement "real" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_plus_int_is_int application-judgement "int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil) (sigma_nonpos-1 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" (inst -1 "low!1" "1 + j!1 + low!1" "j!1 + low!1") (("1" (assert) nil nil) ("2" (hide-all-but (1 4)) (("2" (use "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)) (sigma_TCC5 0 (sigma_TCC5-1 nil 3255975799 ("" (skosimp*) (("" (rewrite "sigma_nonneg") (("" (skosimp*) (("" (assert) nil nil)) nil)) nil)) nil) ((sigma_nonneg formula-decl nil old_sigma nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (sigma_TCC6 0 (sigma_TCC6-2 nil 3351942569 ("" (skosimp*) (("" (rewrite "sigma_nonpos") (("" (skosimp*) (("" (assert) nil nil)) nil)) nil)) nil) ((sigma_nonpos formula-decl nil old_sigma nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (bool nonempty-type-eq-decl nil booleans nil) (<= const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil) (sigma_TCC6-1 nil 3255975799 ("" (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+ (("1" (inst -1 "high!1-low!1") (("1" (assert) nil nil) ("2" (expand "sigma") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "rng" 1) (("1" (expand "sigma") (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" 1) (("2" (split -1) (("1" (flatten) (("1" (ground) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "connected_domain") (("2" (inst -1 "low!1" "low!1 + (j!1 + 1)" "low!1 + j!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil nil)) (sigma_TCC7 0 (sigma_TCC7-3 nil 3352547044 ("" (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+ (("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" (inst - "low!1+j!1" "low!1" "low!1+j!1") (("1" (assert) nil nil) ("2" (assert) (("2" (inst + "1+j!1+low!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) nil nil) ("4" (skosimp*) nil nil) ("5" (skosimp*) nil nil) ("6" (skosimp*) nil nil) ("7" (skosimp*) nil nil) ("8" (skosimp*) nil nil) ("9" (skosimp*) nil nil) ("10" (skosimp*) nil nil) ("11" (skosimp*) nil nil)) nil)) nil) ("3" (skosimp*) nil nil) ("4" (skosimp*) nil nil) ("5" (skosimp*) nil nil)) nil)) nil)) nil)) nil) ((sigma def-decl "real" old_sigma nil) (T_high type-eq-decl nil old_sigma nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (T_low type-eq-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil old_sigma nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (nil application-judgement "nonneg_real" old_sigma nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (T_pred_lem formula-decl nil old_sigma nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (low!1 skolem-const-decl "T_low" old_sigma nil) (high!1 skolem-const-decl "T_high" old_sigma nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (Fnat!1 skolem-const-decl "[T -> nat]" old_sigma nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (sigma_eq_arg formula-decl nil old_sigma nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (j!1 skolem-const-decl "nat" old_sigma nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (closed_plus formula-decl nil integers nil) (closed_plus formula-decl nil rationals nil)) nil) (sigma_TCC7-2 nil 3351942623 ("" (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+ (("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) nil nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" +) (("2" (split -) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (lemma "T_pred_lem") (("2" (inst - "low!1+j!1" "low!1" "low!1+j!1") (("1" (assert) nil nil) ("2" (inst + "1+j!1+low!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (inst + "rng!2+low!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (inst + "rng!2+low!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("5" (skosimp*) (("5" (inst + "rng!2+low!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("6" (skosimp*) (("6" (inst + "rng!2+low!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("7" (skosimp*) (("7" (inst + "rng!2+low!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("8" (skosimp*) (("8" (inst + "rng!2+low!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("9" (skosimp*) (("9" (inst + "rng!2+low!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("10" (skosimp*) (("10" (inst + "rng!2+low!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("11" (skosimp*) (("11" (inst + "rng!2+low!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (inst + "rng!1+low!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (inst + "rng!1+low!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("5" (skosimp*) (("5" (inst + "rng!1+low!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "sigma") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) nil nil) (sigma_TCC7-1 nil 3351939915 ("" (judgement-tcc) nil nil) nil nil)) (sigma_TCC8 0 (sigma_TCC8-2 nil 3352547022 ("" (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+ (("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) nil nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" +) (("2" (split -) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (lemma "T_pred_lem") (("2" (inst - "low!1+j!1" "low!1" "low!1+j!1") (("1" (assert) nil nil) ("2" (inst + "1+j!1+low!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) nil nil) ("4" (skosimp*) nil nil) ("5" (skosimp*) nil nil) ("6" (skosimp*) nil nil) ("7" (skosimp*) nil nil) ("8" (skosimp*) nil nil) ("9" (skosimp*) nil nil) ("10" (skosimp*) nil nil) ("11" (skosimp*) nil nil)) nil)) nil) ("3" (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) ((T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (<= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (closed_plus formula-decl nil rationals nil) (closed_plus formula-decl nil integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (j!1 skolem-const-decl "nat" old_sigma nil) (npreal_plus_npreal_is_npreal application-judgement "npreal" real_types nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (sigma_eq_arg formula-decl nil old_sigma nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (Fnpi!1 skolem-const-decl "[T -> nonpos_int]" old_sigma nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (high!1 skolem-const-decl "T_high" old_sigma nil) (low!1 skolem-const-decl "T_low" old_sigma nil) (T_pred_lem formula-decl nil old_sigma nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (nil application-judgement "nonpos_real" old_sigma nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (sigma def-decl "real" old_sigma nil) (nonpos_int nonempty-type-eq-decl nil integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil) (sigma_TCC8-1 nil 3352522153 ("" (judgement-tcc) nil nil) nil nil)) (sigma_nonneg_eq_0 0 (sigma_nonneg_eq_0-1 nil 3255975799 ("" (skosimp*) (("" (lemma "sigma_middle") (("" (inst?) (("" (inst -1 "i!1") (("" (assert) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((sigma_middle formula-decl nil old_sigma nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (nil application-judgement "nonneg_real" old_sigma nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (T_low type-eq-decl nil old_sigma nil) (T_high type-eq-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (T formal-subtype-decl nil old_sigma nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (sigma_nn_ge_comps 0 (sigma_nn_ge_comps-2 nil 3256040402 ("" (skosimp*) (("" (lemma "sigma_middle") (("" (inst?) (("" (inst -1 "i!1") (("" (assert) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((sigma_middle formula-decl nil old_sigma nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nil application-judgement "nonneg_real" old_sigma nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (T_low type-eq-decl nil old_sigma nil) (T_high type-eq-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (T formal-subtype-decl nil old_sigma nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil) (sigma_nn_ge_comps-1 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)) (sum_it_def_TCC1 0 (sum_it_def_TCC1-1 nil 3255975799 ("" (skosimp*) (("" (inst + "low!1") (("1" (assert) nil nil) ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil)) nil)) nil) ((low!1 skolem-const-decl "T_low" old_sigma nil) (T_low type-eq-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil old_sigma nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (T_high type-eq-decl nil old_sigma nil) (T_pred_lem formula-decl nil old_sigma nil)) nil)) (sum_it_def_TCC2 0 (sum_it_def_TCC2-1 nil 3255975799 ("" (skosimp*) (("" (use "T_pred_lem") (("" (assert) nil nil)) nil)) nil) ((T_pred_lem formula-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil old_sigma nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (T_high type-eq-decl nil old_sigma nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (sum_it_def_TCC3 0 (sum_it_def_TCC3-1 nil 3352118808 ("" (subtype-tcc) nil nil) ((int_minus_int_is_int application-judgement "int" integers nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil old_sigma nil) (T_high type-eq-decl nil old_sigma nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil)) (sum_it_prop_TCC1 0 (sum_it_prop_TCC1-1 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_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (low!1 skolem-const-decl "T_low" old_sigma nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (T formal-subtype-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil)) nil)) (sum_it_prop 0 (sum_it_prop-1 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" (inst -1 "lambda(lh:T| low!1 <= lh AND lh <= high!1): sum_it_def((high!1-lh)+low!1, high!1, F!1, sigma (("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) (("2" (lift-if) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 -3 -4 3) (("2" (expand "sum_it_def") (("2" (expand "sum_it_def") (("2" (expand "sigma" + 2) (("2" (lift-if) (("2" (ground) (("2" (expand "sigma") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -1 -2 3) (("3" (use "T_pred_lem") (("3" (assert) nil nil)) nil)) nil) ("4" (hide -1 -2 3) (("4" (skosimp*) (("4" (ground) (("1" (expand "sum_it_def" 1) (("1" (rewrite "sigma_rew" -) 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" (inst - "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) ((T_low type-eq-decl nil old_sigma nil) (T_high type-eq-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil old_sigma nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sum_it_def def-decl "real" old_sigma nil) (sigma def-decl "real" old_sigma nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (high!1 skolem-const-decl "T_high" old_sigma nil) (low!1 skolem-const-decl "T_low" old_sigma nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (pred type-eq-decl nil defined_types nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (i!1 skolem-const-decl "T" old_sigma nil) (T_pred_lem formula-decl nil old_sigma nil) (sigma_rew formula-decl nil old_sigma nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (lh!1 skolem-const-decl "{lh: T | low!1 <= lh AND lh <= high!1}" old_sigma nil) (NOT const-decl "[bool -> bool]" booleans nil) (>= const-decl "bool" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (subrange_induction formula-decl nil subrange_inductions nil)) nil)) (sum_it_sigma 0 (sum_it_sigma-1 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) ((T_high type-eq-decl nil old_sigma nil) (T_low type-eq-decl nil old_sigma nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil old_sigma nil) (T_pred const-decl "[int -> boolean]" old_sigma nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (> const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sum_it_def def-decl "real" old_sigma nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma def-decl "real" old_sigma nil) (sum_it const-decl "real" old_sigma nil) (sum_it_prop formula-decl nil old_sigma nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_eq_arg formula-decl nil old_sigma nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil)))
¤ 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.134Bemerkung: ¤*Bot Zugriff |
|
||||||||||||||
2026-10-11