|
(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)
(("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)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.78 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
