|
(sigma_below_sub
(sigma_diff_eq_TCC1 0
(sigma_diff_eq_TCC1-1 nil 3282393213 ("" (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)
(>= 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_ge_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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(sigma_diff_eq_TCC2 0
(sigma_diff_eq_TCC2-1 nil 3282393213 ("" (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)
(>= 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_ge_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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(sigma_diff_eq_TCC3 0
(sigma_diff_eq_TCC3-1 nil 3282393213 ("" (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)
(>= 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(sigma_diff_eq_TCC4 0
(sigma_diff_eq_TCC4-1 nil 3282393213 ("" (assuming-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)
(>= 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil))
shostak))
(sigma_diff_eq_TCC5 0
(sigma_diff_eq_TCC5-1 nil 3282393214 ("" (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)
(>= 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(integer nonempty-type-from-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(N1 formal-const-decl "nat" sigma_below_sub nil)
(< const-decl "bool" reals nil))
shostak))
(sigma_diff_eq_TCC6 0
(sigma_diff_eq_TCC6-1 nil 3282393214 ("" (assuming-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)
(>= 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(sigma_diff_eq_TCC7 0
(sigma_diff_eq_TCC7-1 nil 3352459362 ("" (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)
(>= 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil))
nil))
(sigma_diff_eq_TCC8 0
(sigma_diff_eq_TCC8-1 nil 3352459362 ("" (assuming-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)
(>= 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(integer nonempty-type-from-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(N2 formal-const-decl "nat" sigma_below_sub nil)
(< const-decl "bool" reals nil))
nil))
(sigma_diff_eq 0
(sigma_diff_eq-3 nil 3403453952
("" (induct "n")
(("1" (skosimp*)
(("1" (expand "sigma")
(("1" (lift-if)
(("1" (ground)
(("1" (inst?)
(("1" (assert)
(("1" (expand "sigma") (("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "sigma" 1)
(("2" (assert)
(("2" (inst?)
(("2" (inst?)
(("2" (prop)
(("1" (inst -5 "1+j!1") (("1" (assert) nil nil)) nil)
("2" (assert)
(("2" (inst -4 "1+j!1")
(("2" (assert)
(("2" (assert)
(("2" (expand "sigma") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("3" (skosimp*)
(("3" (inst?) (("3" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)
("4" (hide 2) (("4" (skosimp*) nil nil)) nil)
("5" (assert)
(("5" (hide 2) (("5" (skosimp*) (("5" (assert) nil nil)) nil))
nil))
nil)
("6" (hide 2) (("6" (skosimp*) (("6" (assert) nil nil)) nil)) nil)
("7" (hide 2) (("7" (skosimp*) nil nil)) nil)
("8" (assert)
(("8" (hide 2) (("8" (skosimp*) (("8" (assert) nil nil)) nil))
nil))
nil)
("9" (hide 2) (("9" (skosimp*) (("9" (assert) nil nil)) nil)) nil)
("10" (hide 2) (("10" (skosimp*) (("10" (assert) nil nil)) nil))
nil))
nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(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)
(nat_induction formula-decl nil naturalnumbers nil)
(sigma def-decl "real" sigma 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)
(integer nonempty-type-from-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans 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)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
(N2 formal-const-decl "nat" sigma_below_sub nil)
(N1 formal-const-decl "nat" sigma_below_sub nil))
nil)
(sigma_diff_eq-2 nil 3282386439
("" (induct "n")
(("1" (skosimp*)
(("1" (expand "sigma")
(("1" (lift-if)
(("1" (ground) (("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "sigma" 1)
(("2" (assert)
(("2" (inst?)
(("2" (inst?)
(("2" (prop)
(("1" (inst -5 "1+j!1")
(("1" (assert)
(("1" (lift-if) (("1" (ground) nil nil)) nil))
nil))
nil)
("2" (assert)
(("2" (inst -4 "1+j!1") (("2" (assert) nil nil))
nil))
nil)
("3" (skosimp*)
(("3" (assert)
(("3" (inst?) (("3" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)
("4" (hide 2) (("4" (skosimp*) nil nil)) nil)
("5" (hide 2)
(("5" (skosimp*)
(("5" (inst + "0")
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
nil))
nil)
("6" (hide 2) (("6" (skosimp*) (("6" (assert) nil nil)) nil)) nil)
("7" (hide 2) (("7" (skosimp*) nil nil)) nil)
("8" (hide 2) (("8" (skosimp*) (("8" (assert) nil nil)) nil)) nil)
("9" (hide 2) (("9" (skosimp*) (("9" (assert) nil nil)) nil)) nil)
("10" (hide 2) (("10" (skosimp*) (("10" (assert) nil nil)) nil))
nil))
nil)
((T_low type-eq-decl nil sigma nil)
(T_high type-eq-decl nil sigma nil)
(sigma def-decl "real" sigma nil))
nil)
(sigma_diff_eq-1 nil 3282385980
("" (induct "n")
(("1" (skosimp*)
(("1" (expand "sigma")
(("1" (lift-if) (("1" (ground) nil nil)) nil)) nil))
nil)
("2" (skosimp*)
(("2" (expand "sigma" 1)
(("2" (assert)
(("2" (lift-if)
(("2" (ground)
(("1" (inst -6 "n0!1") nil nil)
("2" (inst -5 "1+j!1")
(("2" (assert)
(("2" (assert)
(("2" (replace -5)
(("2" (assert)
(("2" (inst?)
(("2" (assert) (("2" (postpone) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)
("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)
("5" (hide 2) (("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil)
("6" (hide 2) (("6" (skosimp*) (("6" (assert) nil nil)) nil)) nil)
("7" (postpone) nil nil) ("8" (postpone) nil nil))
nil)
nil shostak))
(sigma_diff_shift_TCC1 0
(sigma_diff_shift_TCC1-1 nil 3282393214 ("" (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)
(>= 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_ge_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)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(sigma_diff_shift_TCC2 0
(sigma_diff_shift_TCC2-1 nil 3282393214 ("" (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)
(>= 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_ge_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)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(sigma_diff_shift_TCC3 0
(sigma_diff_shift_TCC3-1 nil 3282393215 ("" (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)
(>= 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(sigma_diff_shift_TCC4 0
(sigma_diff_shift_TCC4-1 nil 3282393215 ("" (assuming-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)
(>= 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil))
shostak))
(sigma_diff_shift_TCC5 0
(sigma_diff_shift_TCC5-1 nil 3282393215 ("" (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)
(>= 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(integer nonempty-type-from-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(N1 formal-const-decl "nat" sigma_below_sub nil)
(< const-decl "bool" reals nil))
shostak))
(sigma_diff_shift_TCC6 0
(sigma_diff_shift_TCC6-1 nil 3282393216 ("" (assuming-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)
(>= 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(sigma_diff_shift_TCC7 0
(sigma_diff_shift_TCC7-1 nil 3352459362
("" (skosimp*)
(("" (inst + "n!1 + m!1")
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(N2 formal-const-decl "nat" sigma_below_sub nil)
(n!1 skolem-const-decl "nat" sigma_below_sub nil)
(m!1 skolem-const-decl "nat" sigma_below_sub nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals 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 "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(below type-eq-decl nil naturalnumbers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(sigma_diff_shift_TCC8 0
(sigma_diff_shift_TCC8-1 nil 3352459362 ("" (assuming-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)
(>= 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(integer nonempty-type-from-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(N2 formal-const-decl "nat" sigma_below_sub nil)
(< const-decl "bool" reals nil))
nil))
(sigma_diff_shift 0
(sigma_diff_shift-2 nil 3403453975
("" (induct "n")
(("1" (skosimp*)
(("1" (expand "sigma")
(("1" (lift-if)
(("1" (ground)
(("1" (inst?)
(("1" (assert)
(("1" (expand "sigma") (("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "sigma" 1)
(("2" (assert)
(("2" (inst?)
(("2" (inst?)
(("2" (assert)
(("2" (prop)
(("1" (inst -5 "1+j!1") (("1" (assert) nil nil)) nil)
("2" (ground)
(("2" (expand "sigma")
(("2" (assert)
(("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil)
("3" (skosimp*)
(("3" (inst?) (("3" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)
("4" (hide 2) (("4" (skosimp*) nil nil)) nil)
("5" (hide 2) (("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil)
("6" (hide 2) (("6" (skosimp*) (("6" (assert) nil nil)) nil)) nil)
("7" (hide 2) (("7" (skosimp*) nil nil)) nil)
("8" (hide 2) (("8" (skosimp*) (("8" (assert) nil nil)) nil)) nil)
("9" (hide 2) (("9" (skosimp*) (("9" (assert) nil nil)) nil)) nil)
("10" (hide 2) (("10" (skosimp*) (("10" (assert) nil nil)) nil))
nil))
nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_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)
(nat_induction formula-decl nil naturalnumbers nil)
(sigma def-decl "real" sigma 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)
(integer nonempty-type-from-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans 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)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(N2 formal-const-decl "nat" sigma_below_sub nil)
(N1 formal-const-decl "nat" sigma_below_sub nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil))
nil)
(sigma_diff_shift-1 nil 3282392564
("" (induct "n")
(("1" (skosimp*)
(("1" (expand "sigma")
(("1" (lift-if)
(("1" (ground) (("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "sigma" 1)
(("2" (assert)
(("2" (inst?)
(("2" (inst?)
(("2" (assert)
(("2" (prop)
(("1" (inst -5 "1+j!1")
(("1" (assert)
(("1" (lift-if) (("1" (ground) nil nil)) nil))
nil))
nil)
("2" (inst -4 "1+j!1") (("2" (assert) nil nil)) nil)
("3" (hide 2)
(("3" (skosimp*)
(("3" (assert)
(("3" (inst?) (("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)
("4" (hide 2) (("4" (skosimp*) nil nil)) nil)
("5" (hide 2) (("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil)
("6" (hide 2) (("6" (skosimp*) (("6" (assert) nil nil)) nil)) nil)
("7" (hide 2) (("7" (skosimp*) nil nil)) nil)
("8" (hide 2) (("8" (skosimp*) (("8" (assert) nil nil)) nil)) nil)
("9" (hide 2) (("9" (skosimp*) (("9" (assert) nil nil)) nil)) nil)
("10" (hide 2) (("10" (skosimp*) (("10" (assert) nil nil)) nil))
nil))
nil)
((T_low type-eq-decl nil sigma nil)
(T_high type-eq-decl nil sigma nil)
(sigma def-decl "real" sigma nil))
shostak)))
¤ Dauer der Verarbeitung: 0.40 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.
|
