|
(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" sigma nil)
(high!1 skolem-const-decl "T_high" 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 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]" sigma nil)
(T formal-subtype-decl nil sigma nil)
(<= const-decl "bool" reals nil)
(T_high type-eq-decl nil sigma nil)
(T_low type-eq-decl nil 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" sigma nil)
(T_high type-eq-decl nil sigma nil)
(<= const-decl "bool" reals nil)
(T formal-subtype-decl nil sigma nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T_pred const-decl "[int -> boolean]" 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 sigma nil)
(T_pred_lem formula-decl nil 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]" sigma nil)
(T formal-subtype-decl nil sigma nil)
(<= const-decl "bool" reals nil)
(T_high type-eq-decl nil sigma nil)
(T_low type-eq-decl nil 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" sigma nil)
(low!1 skolem-const-decl "T_low" sigma nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(sigma_TCC1 0
(sigma_TCC1-2 nil 3403452046
("" (skosimp* t)
(("" (assert)
(("" (skosimp*)
(("" (typepred "j!1")
(("" (lemma "connected_domain")
(("" (inst - "low!1" "j!1" "high!1")
(("1" (assert) nil nil)
("2" (prop)
(("2" (skosimp*)
(("2" (lemma "connected_domain")
(("2" (assert)
(("2" (inst - "j!2" "j!1" "low!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(low!1 skolem-const-decl "T_low" 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 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]" sigma nil)
(T formal-subtype-decl nil sigma nil)
(<= const-decl "bool" reals nil)
(T_low type-eq-decl nil sigma nil)
(T_high type-eq-decl nil sigma nil))
nil)
(sigma_TCC1-1 nil 3255975799
("" (skosimp*)
(("" (use "T_pred_lem") (("" (assert) nil nil)) nil)) nil)
nil nil))
(sigma_TCC2 0
(sigma_TCC2-2 nil 3403452083
("" (skosimp*)
(("" (typepred "high!1")
(("" (assert)
(("" (prop)
(("1" (inst + "high!1") (("1" (assert) nil nil)) nil)
("2" (skosimp*)
(("2" (typepred "j!1")
(("2" (inst + "j!1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T_high type-eq-decl nil sigma nil)
(<= const-decl "bool" reals nil)
(T formal-subtype-decl nil sigma nil)
(T_pred const-decl "[int -> boolean]" 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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(high!1 skolem-const-decl "T_high" 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))
nil)
(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)
nil nil))
(sigma_TCC3 0
(sigma_TCC3-1 nil 3255975799
("" (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))
(sigma2_TCC1 0
(sigma2_TCC1-1 nil 3403451849
("" (skosimp*)
(("" (typepred "low!1")
(("" (assert)
(("" (skosimp*)
(("" (replace -2)
(("" (typepred "j!1")
(("" (typepred "high!1")
(("" (assert)
(("" (skosimp*)
(("" (lemma "connected_domain")
(("" (inst - "j!1" "j!2" "low!1")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T_low type-eq-decl nil sigma nil)
(<= const-decl "bool" reals nil)
(T formal-subtype-decl nil sigma nil)
(T_pred const-decl "[int -> boolean]" 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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(connected_domain formula-decl nil sigma nil)
(integer nonempty-type-from-decl nil integers nil)
(T_high type-eq-decl nil sigma nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(sigma_rew 0
(sigma_rew-1 nil 3352522445
("" (skosimp*)
(("" (lift-if)
(("" (ground)
(("1" (expand "sigma") (("1" (propax) nil nil)) nil)
("2" (expand "sigma")
(("2" (expand "sigma") (("2" (assert) nil nil)) nil))
nil)
("3" (expand "sigma" 2 1) (("3" (propax) nil nil)) nil))
nil))
nil))
nil)
((sigma def-decl "real" 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_plus_real_is_real application-judgement "real" reals
nil))
shostak))
(sigma_rew2 0
(sigma_rew2-1 nil 3403459500
("" (skosimp*)
((""
(case "FORALL (rng: nat): T_pred(low!1+rng) IMPLIES
sigma(low!1, low!1+rng, F!1) = sigma2(low!1, low!1+rng, F!1)")
(("1" (inst - "high!1-low!1")
(("1" (assert)
(("1" (typepred "high!1")
(("1" (assert)
(("1" (skosimp*)
(("1" (typepred "j!1")
(("1" (typepred "low!1")
(("1" (lemma "connected_domain")
(("1" (inst - "low!1" "j!1" "high!1")
(("1"
(assert)
(("1"
(expand "sigma")
(("1"
(expand "sigma2")
(("1" (propax) nil nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(skosimp*)
(("2"
(lemma "connected_domain")
(("2"
(inst - "j!2" "j!1" "low!1")
(("2"
(assert)
(("2"
(expand "sigma")
(("2"
(expand "sigma2")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "sigma")
(("2" (expand "sigma2") (("2" (assert) nil nil)) nil))
nil))
nil)
("2" (hide 2)
(("2" (induct "rng")
(("1" (assert)
(("1" (flatten)
(("1" (expand "sigma")
(("1" (expand "sigma")
(("1" (expand "sigma2")
(("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (assert)
(("2" (expand "sigma" 1)
(("2" (expand "sigma2" 1)
(("2" (assert)
(("2" (hide 2)
(("2" (typepred "low!1")
(("2"
(typepred "j!1")
(("2"
(assert)
(("2"
(prop)
(("1"
(lemma "connected_domain")
(("1"
(inst
-
"low!1"
"j!1+1+low!1"
"j!1+low!1")
(("1" (assert) nil nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(lemma "connected_domain")
(("2"
(inst
-
"j!2"
"j!1+1+low!1"
"j!1+low!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide 2) (("3" (skosimp*) nil nil)) nil))
nil))
nil)
("3" (skosimp*) nil nil))
nil))
nil)
((sigma2 def-decl "real" sigma nil)
(sigma def-decl "real" sigma nil)
(T_high type-eq-decl nil sigma nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(T_low type-eq-decl nil sigma nil)
(<= const-decl "bool" reals nil)
(T formal-subtype-decl nil 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]" 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)
(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)
(connected_domain formula-decl nil sigma nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(integer nonempty-type-from-decl nil integers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(low!1 skolem-const-decl "T_low" sigma nil)
(high!1 skolem-const-decl "T_high" 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)
(pred type-eq-decl nil defined_types nil)
(nat_induction formula-decl nil naturalnumbers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil))
nil))
(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" sigma nil)
(nn!1 skolem-const-decl "nat" sigma nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(low!1 skolem-const-decl "T_low" sigma nil)
(T_low type-eq-decl nil sigma nil)
(<= const-decl "bool" reals nil)
(T formal-subtype-decl nil 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]" 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]" sigma nil)
(T formal-subtype-decl nil sigma nil)
(<= const-decl "bool" reals nil)
(T_low type-eq-decl nil 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) 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" sigma nil)
(nn!1 skolem-const-decl "nat" sigma nil)
(rng!2 skolem-const-decl "nat" sigma nil)
(low!1 skolem-const-decl "T_low" sigma nil)
(nn!1 skolem-const-decl "nat" sigma nil)
(rng!2 skolem-const-decl "nat" sigma nil)
(T_pred_lem formula-decl nil 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" sigma nil)
(T_high type-eq-decl nil 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]" sigma nil)
(T formal-subtype-decl nil sigma nil)
(<= const-decl "bool" reals nil)
(T_low type-eq-decl nil 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" 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]" sigma nil)
(T formal-subtype-decl nil sigma nil)
(<= const-decl "bool" reals nil)
(T_high type-eq-decl nil sigma nil)
(T_low type-eq-decl nil 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" 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]" sigma nil)
(T formal-subtype-decl nil sigma nil)
(<= const-decl "bool" reals nil)
(T_high type-eq-decl nil sigma nil)
(T_low type-eq-decl nil 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 sigma nil)
(T_high type-eq-decl nil sigma nil)
(<= const-decl "bool" reals nil)
(T formal-subtype-decl nil sigma nil)
(T_pred const-decl "[int -> boolean]" 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" sigma nil)
(sigma_spl formula-decl nil sigma nil)
(T_pred_lem formula-decl nil sigma nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(high!1 skolem-const-decl "T_high" sigma nil)
(low!1 skolem-const-decl "T_low" sigma nil)
(z!1 skolem-const-decl "int" 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 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 sigma nil)
(T_high type-eq-decl nil 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 sigma nil)
(T_pred const-decl "[int -> boolean]" 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 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 sigma nil)
(T_high type-eq-decl nil 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 sigma nil)
(T_pred const-decl "[int -> boolean]" 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" 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 sigma nil)
(T_low type-eq-decl nil sigma nil)
(<= const-decl "bool" reals nil)
(T formal-subtype-decl nil sigma nil)
(T_pred const-decl "[int -> boolean]" 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 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" 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]" sigma nil)
(T formal-subtype-decl nil sigma nil)
(<= const-decl "bool" reals nil)
(T_high type-eq-decl nil sigma nil)
(T_low type-eq-decl nil 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 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 sigma nil)
(T_low type-eq-decl nil sigma nil)
(T_high type-eq-decl nil 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 sigma nil)
(T_pred const-decl "[int -> boolean]" 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" 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]" sigma nil)
(T formal-subtype-decl nil sigma nil)
(<= const-decl "bool" reals nil)
(T_high type-eq-decl nil sigma nil)
(T_low type-eq-decl nil 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 sigma nil)
(T_high type-eq-decl nil sigma nil)
(<= const-decl "bool" reals nil)
(T formal-subtype-decl nil sigma nil)
(T_pred const-decl "[int -> boolean]" 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 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" 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]" sigma nil)
(T formal-subtype-decl nil sigma nil)
(<= const-decl "bool" reals nil)
(T_low type-eq-decl nil sigma nil)
(T_high type-eq-decl nil 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" 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]" sigma nil)
(T formal-subtype-decl nil sigma nil)
(<= const-decl "bool" reals nil)
(T_high type-eq-decl nil sigma nil)
(T_low type-eq-decl nil 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]" sigma nil)
(T formal-subtype-decl nil 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 sigma nil)
(sigma_rew formula-decl nil sigma nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sigma def-decl "real" 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 sigma nil)
(T_high type-eq-decl nil 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 sigma nil)
(T_pred const-decl "[int -> boolean]" 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 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]" sigma nil)
(T formal-subtype-decl nil sigma nil)
(<= const-decl "bool" reals nil)
(T_high type-eq-decl nil sigma nil)
(T_low type-eq-decl nil sigma nil)
(pred type-eq-decl nil defined_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(sigma def-decl "real" 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" sigma nil)
(high!1 skolem-const-decl "T_high" 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 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 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 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]" sigma nil)
(T formal-subtype-decl nil sigma nil)
(<= const-decl "bool" reals nil)
(T_high type-eq-decl nil sigma nil)
(T_low type-eq-decl nil 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")
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.62 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.
|
