|
(product
(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" product nil)
(high!1 skolem-const-decl "T_high" product 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 product 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]" product nil)
(T formal-subtype-decl nil product nil)
(<= const-decl "bool" reals nil)
(T_high type-eq-decl nil product nil)
(T_low type-eq-decl nil product 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" product nil)
(T_high type-eq-decl nil product nil)
(<= const-decl "bool" reals nil)
(T formal-subtype-decl nil product nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T_pred const-decl "[int -> boolean]" product 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 product nil)
(T_pred_lem formula-decl nil product 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]" product nil)
(T formal-subtype-decl nil product nil)
(<= const-decl "bool" reals nil)
(T_high type-eq-decl nil product nil)
(T_low type-eq-decl nil product 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" product nil)
(low!1 skolem-const-decl "T_low" product nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(product_TCC1 0
(product_TCC1-1 nil 3410094710
("" (skosimp*)
(("" (typepred "low!1")
(("" (typepred "high!1")
(("" (assert)
(("" (skosimp*)
(("" (typepred "j!1")
(("" (lemma "connected_domain")
(("" (inst - "low!1" "j!1" "high!1")
(("1" (assert) nil nil)
("2" (assert)
(("2" (skosimp*)
(("2" (lemma "connected_domain")
(("2" (inst - "j!2" "j!1" "low!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T_low type-eq-decl nil product nil)
(<= const-decl "bool" reals nil)
(T formal-subtype-decl nil product nil)
(T_pred const-decl "[int -> boolean]" product 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_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(low!1 skolem-const-decl "T_low" product 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 product nil)
(T_high type-eq-decl nil product nil))
nil))
(product_TCC2 0
(product_TCC2-1 nil 3410094710
("" (skeep)
(("" (typepred "high")
(("" (typepred "low")
(("" (assert)
(("" (ground)
(("1" (inst + "high") (("1" (assert) nil nil)) nil)
("2" (skosimp*)
(("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil)
("3" (skosimp*)
(("3" (inst + "high") (("3" (assert) nil nil)) nil)) nil)
("4" (skosimp*)
(("4" (inst + "j!1") (("4" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((T_high type-eq-decl nil product nil)
(<= const-decl "bool" reals nil)
(T formal-subtype-decl nil product nil)
(T_pred const-decl "[int -> boolean]" product 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)
(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)
(T_low type-eq-decl nil product nil))
nil))
(product_TCC3 0
(product_TCC3-1 nil 3410094710 ("" (termination-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(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]" product nil)
(T formal-subtype-decl nil product nil)
(<= const-decl "bool" reals nil)
(T_low type-eq-decl nil product nil)
(T_high type-eq-decl nil product nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(minus_int_is_int application-judgement "int" integers nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(int_plus_int_is_int application-judgement "int" integers nil))
nil))
(product_spl_TCC1 0
(product_spl_TCC1-1 nil 3410103726 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(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]" product nil)
(T formal-subtype-decl nil product nil)
(<= const-decl "bool" reals nil)
(T_low type-eq-decl nil product nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int_plus_int_is_int application-judgement "int" integers nil))
nil))
(product_spl_TCC2 0
(product_spl_TCC2-1 nil 3410103726
("" (skeep)
(("" (inst + "low + nn + rng") (("" (assert) nil nil)) nil)) nil)
((int_plus_int_is_int application-judgement "int" integers nil)
(rng skolem-const-decl "nat" product nil)
(nn skolem-const-decl "nat" product nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(low skolem-const-decl "T_low" product nil)
(T_low type-eq-decl nil product nil)
(<= const-decl "bool" reals nil)
(T formal-subtype-decl nil product 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]" product 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))
(product_spl_TCC3 0
(product_spl_TCC3-1 nil 3410103726
("" (skeep)
(("" (typepred "low")
(("" (split -1)
(("1" (inst + "low") (("1" (assert) nil nil)) nil)
("2" (skosimp*)
(("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((T_low type-eq-decl nil product nil)
(<= const-decl "bool" reals nil)
(T formal-subtype-decl nil product nil)
(T_pred const-decl "[int -> boolean]" product 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)
(low skolem-const-decl "T_low" product nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(product_spl 0
(product_spl-1 nil 3410103740
("" (induct "rng")
(("1" (assert)
(("1" (expand "product") (("1" (propax) nil nil)) nil)) nil)
("2" (skosimp*)
(("2" (expand "product" + (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" product nil)
(nn!1 skolem-const-decl "nat" product nil)
(rng!2 skolem-const-decl "nat" product nil)
(low!1 skolem-const-decl "T_low" product nil)
(nn!1 skolem-const-decl "nat" product nil)
(rng!2 skolem-const-decl "nat" product nil)
(T_pred_lem formula-decl nil product 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_times_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)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(product def-decl "real" product nil)
(T_high type-eq-decl nil product 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]" product nil)
(T formal-subtype-decl nil product nil)
(<= const-decl "bool" reals nil)
(T_low type-eq-decl nil product 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))
(product_split_TCC1 0
(product_split_TCC1-1 nil 3410103726
("" (skeep)
(("" (typepred "high")
(("" (assert)
(("" (split -1)
(("1" (inst + "high") nil nil)
("2" (skosimp*)
(("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((T_high type-eq-decl nil product nil)
(<= const-decl "bool" reals nil)
(T formal-subtype-decl nil product nil)
(T_pred const-decl "[int -> boolean]" product 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 skolem-const-decl "T_high" product nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(product_split_TCC2 0
(product_split_TCC2-1 nil 3410103726
("" (skeep)
(("" (typepred "low")
(("" (split -1)
(("1" (inst + "low") (("1" (assert) nil nil)) nil)
("2" (skosimp*)
(("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((T_low type-eq-decl nil product nil)
(<= const-decl "bool" reals nil)
(T formal-subtype-decl nil product nil)
(T_pred const-decl "[int -> boolean]" product 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)
(low skolem-const-decl "T_low" product nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(int_plus_int_is_int application-judgement "int" integers nil))
nil))
(product_split 0
(product_split-1 nil 3410103810
("" (skosimp*)
(("" (case "high!1)
(("1" (expand "product") (("1" (assert) nil nil)) nil)
("2" (case-replace "z!1=low!1-1")
(("1" (assert)
(("1" (expand "product") (("1" (assert) nil nil)) nil)) nil)
("2" (lemma "product_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 product nil)
(T_high type-eq-decl nil product nil)
(<= const-decl "bool" reals nil)
(T formal-subtype-decl nil product nil)
(T_pred const-decl "[int -> boolean]" product 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_times_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)
(product def-decl "real" product nil)
(product_spl formula-decl nil product nil)
(T_pred_lem formula-decl nil product nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(high!1 skolem-const-decl "T_high" product nil)
(low!1 skolem-const-decl "T_low" product nil)
(z!1 skolem-const-decl "int" product 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))
(product_div 0
(product_div-1 nil 3410104326
("" (skeep)
(("" (cross-mult 2)
(("" (lemma "product_split")
(("" (inst - "F" "high" "low" "z") (("" (assert) nil nil))
nil))
nil))
nil))
nil)
((real_div_nzreal_is_real application-judgement "real" reals nil)
(div_cancel3 formula-decl nil real_props nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(product def-decl "real" product nil)
(T_high type-eq-decl nil product nil)
(T_low type-eq-decl nil product nil)
(<= const-decl "bool" reals nil)
(T formal-subtype-decl nil product nil)
(T_pred const-decl "[int -> boolean]" product 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)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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_times_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(product_split formula-decl nil product nil))
shostak))
(product_div_neg 0
(product_div_neg-1 nil 3410104551
("" (skeep)
(("" (cross-mult 2)
(("" (lemma "product_split")
(("" (inst - "F" "high" "low" "z") (("" (assert) nil nil))
nil))
nil))
nil))
nil)
((int_plus_int_is_int application-judgement "int" integers 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]" product nil)
(T formal-subtype-decl nil product nil)
(bool nonempty-type-eq-decl nil booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(T_high type-eq-decl nil product nil)
(T_low type-eq-decl nil product 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_div_nzreal_is_real application-judgement "real" reals nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(product_split formula-decl nil product nil))
shostak))
(product_eq_arg 0
(product_eq_arg-1 nil 3410104588
("" (skosimp*)
(("" (expand "product")
(("" (expand "product") (("" (propax) nil nil)) nil)) nil))
nil)
((product def-decl "real" product nil)) shostak))
(product_first_TCC1 0
(product_first_TCC1-1 nil 3410104637
("" (skeep)
(("" (typepred "low")
(("" (assert)
(("" (skosimp*)
(("" (typepred "high")
(("" (assert)
(("" (split -1)
(("1" (lemma "connected_domain")
(("1" (assert)
(("1" (inst - "j!1" "high" "low")
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (skosimp*)
(("2" (lemma "connected_domain")
(("2" (inst - "j!1" "j!2" "low")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T_low type-eq-decl nil product nil)
(<= const-decl "bool" reals nil)
(T formal-subtype-decl nil product nil)
(T_pred const-decl "[int -> boolean]" product 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 product nil)
(integer nonempty-type-from-decl nil integers nil)
(T_high type-eq-decl nil product nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(product_first_TCC2 0
(product_first_TCC2-1 nil 3410104637
("" (skeep)
(("" (typepred "low")
(("" (assert)
(("" (split -1)
(("1" (inst + "low") (("1" (assert) nil nil)) nil)
("2" (skosimp*)
(("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((T_low type-eq-decl nil product nil)
(<= const-decl "bool" reals nil)
(T formal-subtype-decl nil product nil)
(T_pred const-decl "[int -> boolean]" product 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)
(low skolem-const-decl "T_low" product nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_plus_int_is_int application-judgement "int" integers nil))
nil))
(product_first 0
(product_first-1 nil 3410104659
("" (skosimp*)
(("" (lemma "product_split")
(("" (inst?)
(("" (inst -1 "low!1")
(("" (rewrite "product_eq_arg") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((product_split formula-decl nil product 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_times_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(product_eq_arg formula-decl nil product nil)
(T_low type-eq-decl nil product nil)
(T_high type-eq-decl nil product 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 product nil)
(T_pred const-decl "[int -> boolean]" product 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))
(product_last_TCC1 0
(product_last_TCC1-1 nil 3410104637
("" (skeep)
(("" (typepred "high")
(("" (split -1)
(("1" (inst + "high") (("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 product nil)
(<= const-decl "bool" reals nil)
(T formal-subtype-decl nil product nil)
(T_pred const-decl "[int -> boolean]" product 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 skolem-const-decl "T_high" product nil)
(real_ge_is_total_order name-judgement "(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))
(product_last_TCC2 0
(product_last_TCC2-1 nil 3410104637
("" (skeep)
(("" (typepred "high")
(("" (assert)
(("" (skosimp*)
(("" (lemma "connected_domain")
(("" (inst - "low" "j!1" "high")
(("1" (assert) nil nil)
("2" (typepred "low")
(("2" (assert)
(("2" (skosimp*)
(("2" (lemma "connected_domain")
(("2" (assert)
(("2" (inst - "j!2" "j!1" "low")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T_high type-eq-decl nil product nil)
(<= const-decl "bool" reals nil)
(T formal-subtype-decl nil product nil)
(T_pred const-decl "[int -> boolean]" product 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)
(T_low type-eq-decl nil product nil)
(low skolem-const-decl "T_low" product 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 product nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(product_last 0
(product_last-1 nil 3410104722
("" (skosimp*)
(("" (rewrite "product") (("" (assert) nil nil)) nil)) nil)
((product def-decl "real" product 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]" product nil)
(T formal-subtype-decl nil product nil)
(<= const-decl "bool" reals nil)
(T_low type-eq-decl nil product nil)
(T_high type-eq-decl nil product 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_times_real_is_real application-judgement "real" reals nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(product_middle_TCC1 0
(product_middle_TCC1-1 nil 3410104812
("" (skeep)
(("" (typepred "i") (("" (inst + "i") (("" (assert) nil nil)) nil))
nil))
nil)
((T formal-subtype-decl nil product nil)
(T_pred const-decl "[int -> boolean]" product 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)
(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)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(product_middle_TCC2 0
(product_middle_TCC2-1 nil 3410104812
("" (skeep)
(("" (typepred "i") (("" (inst + "i") (("" (assert) nil nil)) nil))
nil))
nil)
((T formal-subtype-decl nil product nil)
(T_pred const-decl "[int -> boolean]" product 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)
(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)
(int_plus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(product_middle 0
(product_middle-1 nil 3410104844
("" (skosimp*)
(("" (lemma "product_split")
(("" (inst?)
(("" (inst -1 "i!1")
(("" (assert)
(("" (assert)
(("" (replace -1)
(("" (hide -1)
(("" (expand "product" 1 1) (("" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((product_split formula-decl nil product nil)
(product def-decl "real" product nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_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 product nil)
(T_high type-eq-decl nil product 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 product nil)
(T_pred const-decl "[int -> boolean]" product 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))
(product_const_TCC1 0
(product_const_TCC1-1 nil 3410104812 ("" (subtype-tcc) nil nil)
((int_plus_int_is_int application-judgement "int" integers nil))
nil))
(product_const 0
(product_const-2 nil 3410105217
("" (skolem 1 (_ _ nzr))
(("" (rewrite "high_low_rewrite")
(("" (hide 2)
(("" (skosimp*)
(("" (prop)
(("1" (expand "product") (("1" (assert) nil nil)) nil)
("2" (induct "n" 2)
(("1" (rewrite "product_eq_arg")
(("1" (assert)
(("1" (expand "^")
(("1" (expand "expt")
(("1" (expand "expt") (("1" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil))
nil)
("2" (hide 2)
(("2" (skosimp*)
(("2" (expand "product" +)
(("2" (assert)
(("2" (lemma "expt_plus")
(("2" (inst - "(1 - low!1 + k!1)" "1" "nzr")
(("2" (replace -1)
(("2" (hide -1)
(("2"
(rewrite "expt_x1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide 3)
(("3" (skosimp*)
(("3" (inst + "high!1")
(("1" (assert) nil nil)
("2" (use "T_pred_lem") (("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("4" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(high_low_rewrite formula-decl nil product 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]" product nil)
(T formal-subtype-decl nil product nil)
(<= const-decl "bool" reals nil)
(T_high type-eq-decl nil product nil)
(T_low type-eq-decl nil product nil)
(pred type-eq-decl nil defined_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(product def-decl "real" product nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(>= const-decl "bool" reals nil)
(^ const-decl "real" exponentiation nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(low!1 skolem-const-decl "T_low" product nil)
(high!1 skolem-const-decl "T_high" product 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 product nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(expt def-decl "real" exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(product_eq_arg formula-decl nil product nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(expt_x1 formula-decl nil exponentiation nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(expt_plus formula-decl nil exponentiation 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)
(product_const-1 nil 3410104877
("" (skolem 1 (_ _ x))
(("" (rewrite "high_low_rewrite")
(("1" (hide 2)
(("1" (skosimp*)
(("1" (prop)
(("1" (expand "product") (("1" (assert) nil nil)) nil)
("2" (induct "n" 2)
(("1" (rewrite "product_eq_arg")
(("1" (assert)
(("1" (expand "^")
(("1" (expand "expt")
(("1" (expand "expt") (("1" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil))
nil)
("2" (hide 2)
(("2" (skosimp*)
(("2" (expand "product" +)
(("2" (assert)
(("2" (lemma "expt_plus")
(("2" (inst - "(1 - low!1 + k!1)" "1" "x")
(("1" (replace -1)
(("1" (hide -1)
(("1"
(rewrite "expt_x1")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2" (flatten) (("2" (postpone) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide 3)
(("3" (skosimp*)
(("3" (inst + "high!1")
(("1" (assert) nil nil)
("2" (use "T_pred_lem") (("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("4" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (postpone) nil nil))
nil))
nil)
nil nil))
(product_zero 0
(product_zero-1 nil 3410105243
("" (skosimp*)
(("" (rewrite "product_first") (("" (assert) nil nil)) nil)) nil)
((product_first formula-decl nil product 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]" product nil)
(T formal-subtype-decl nil product nil)
(bool nonempty-type-eq-decl nil booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(T_high type-eq-decl nil product nil)
(T_low type-eq-decl nil product nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(real_times_real_is_real application-judgement "real" reals 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))
shostak))
(product_scal_TCC1 0
(product_scal_TCC1-1 nil 3410105938 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(OR const-decl "[bool, bool -> bool]" booleans 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]" product nil)
(T formal-subtype-decl nil product nil)
(<= const-decl "bool" reals nil)
(T_high type-eq-decl nil product nil)
(T_low type-eq-decl nil product nil)
(/= const-decl "boolean" notequal nil)
(int_plus_int_is_int application-judgement "int" integers nil))
nil))
(product_scal 0
(product_scal-1 nil 3410105347
("" (skolem 1 ("F" "a" _ _))
(("" (rewrite "high_low_rewrite")
(("1" (hide 2)
(("1" (skosimp*)
(("1" (ground)
(("1" (induct "n" 2)
(("1" (rewrite "product_eq_arg")
(("1" (rewrite "product_eq_arg")
(("1" (assert) (("1" (rewrite "expt_x1") nil nil))
nil))
nil)
("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil))
nil)
("2" (hide 2)
(("2" (skosimp*)
(("2" (expand "product" +)
(("2" (assert)
(("2" (replace -2)
(("2" (hide -2)
(("2" (lemma "expt_plus")
(("2" (inst - "(1 - low!1 + k!1)" "1" "a")
(("2"
(assert)
(("2"
(replace -1)
(("2"
(hide -1)
(("2"
(rewrite "expt_x1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (skosimp*)
(("3" (inst + "high!1")
(("1" (assert) nil nil)
("2" (use "T_pred_lem") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2) (("2" (skosimp*) nil nil)) nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(high_low_rewrite formula-decl nil product 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]" product nil)
(T formal-subtype-decl nil product nil)
(<= const-decl "bool" reals nil)
(T_high type-eq-decl nil product nil)
(T_low type-eq-decl nil product nil)
(pred type-eq-decl nil defined_types nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(product def-decl "real" product nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(>= const-decl "bool" reals nil)
(^ const-decl "real" exponentiation nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(low!1 skolem-const-decl "T_low" product nil)
(high!1 skolem-const-decl "T_high" product nil)
(subrange type-eq-decl nil integers nil)
(a skolem-const-decl "real" product 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 product nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(expt_x1 formula-decl nil exponentiation nil)
(product_eq_arg formula-decl nil product nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(expt_plus formula-decl nil exponentiation nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(product_eq_0_TCC1 0
(product_eq_0_TCC1-1 nil 3412957398
("" (skeep)
(("" (skosimp*)
(("" (typepred "n!1")
(("" (lemma "T_pred_lem")
(("" (inst - "high" "low" "n!1") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((T_pred_lem formula-decl nil product nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(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)
(<= const-decl "bool" 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)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(T_pred const-decl "[int -> boolean]" product nil)
(T formal-subtype-decl nil product nil)
(T_low type-eq-decl nil product nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(T_high type-eq-decl nil product nil)
(subrange type-eq-decl nil integers nil))
nil))
(product_eq_0 0
(product_eq_0-1 nil 3412957679
("" (skolem 1 ("F" _ _))
(("" (rewrite "high_low_rewrite")
(("1" (hide 2)
(("1" (skosimp*)
(("1" (prop)
(("1" (expand "product") (("1" (assert) nil nil)) nil)
("2" (induct "n" 2)
(("1" (skosimp*)
(("1" (rewrite "product_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 "product" -3)
(("2" (mult-cases -3)
(("1" (inst?) nil nil)
("2" (skosimp*)
(("2" (typepred "n!1") (("2" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (skosimp*)
(("3" (hide 3)
(("3" (typepred "n!2")
(("3" (typepred "n!1")
(("3" (lemma "T_pred_lem")
(("3" (assert)
(("3" (inst - "high!1" "low!1" "n!2")
(("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (skosimp*)
(("4" (typepred "n!1")
(("4" (lemma "T_pred_lem")
(("4" (inst - "high!1" "low!1" "n!1")
(("4" (assert) nil nil)) nil))
nil))
nil))
nil)
("5" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (typepred "n!1")
(("2" (lemma "T_pred_lem")
(("2" (inst - "high!1" "low!1" "n!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((high_low_rewrite formula-decl nil product 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]" product nil)
(T formal-subtype-decl nil product nil)
(<= const-decl "bool" reals nil)
(T_high type-eq-decl nil product nil)
(T_low type-eq-decl nil product nil)
(pred type-eq-decl nil defined_types nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(product def-decl "real" product nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(subrange type-eq-decl nil integers nil)
(low!1 skolem-const-decl "T_low" product nil)
(high!1 skolem-const-decl "T_high" product nil)
(F skolem-const-decl "[T -> real]" product 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)
(product_eq_arg formula-decl nil product nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(T_pred_lem formula-decl nil product nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(zero_times3 formula-decl nil real_props nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(product_eq_zero_TCC1 0
(product_eq_zero_TCC1-1 nil 3618849229
("" (skeep)
(("" (typepred "low")
(("" (typepred "high")
(("" (typepred "n")
(("" (lemma "connected_domain")
(("" (ground)
(("1" (inst - "low" "high" "n") (("1" (assert) nil nil))
nil)
("2" (skosimp*)
(("2" (inst - "j!1" "high" "n")
(("2" (assert) nil nil)) nil))
nil)
("3" (skosimp*)
(("3" (inst - "low" "j!1" "n") (("3" (assert) nil nil))
nil))
nil)
("4" (skosimp*)
(("4" (inst - "j!1" "j!2" "n") (("4" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T_low type-eq-decl nil product nil)
(<= const-decl "bool" reals nil)
(T formal-subtype-decl nil product nil)
(T_pred const-decl "[int -> boolean]" product 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)
(subrange type-eq-decl nil integers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(integer nonempty-type-from-decl nil integers nil)
(connected_domain formula-decl nil product nil)
(T_high type-eq-decl nil product nil))
nil))
(product_eq_zero 0
(product_eq_zero-1 nil 3618849033
("" (skeep)
(("" (lemma "product_eq_0")
(("" (inst?)
(("" (split 1)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 1.834 Sekunden
(vorverarbeitet)
¤
|
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchen
Die farbliche Syntaxdarstellung ist noch experimentell.
|
