mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
289 lines
13 KiB
Plaintext
289 lines
13 KiB
Plaintext
(PowerInt
|
|
(power_TCC1 0
|
|
(power_TCC1-1 nil 3552165738 ("" (subtype-tcc) nil nil)
|
|
((boolean nonempty-type-decl nil booleans nil)
|
|
(bool nonempty-type-eq-decl nil booleans nil)
|
|
(NOT const-decl "[bool -> bool]" booleans nil)
|
|
(number nonempty-type-decl nil numbers nil)
|
|
(number_field_pred const-decl "[number -> boolean]" number_fields
|
|
nil)
|
|
(number_field nonempty-type-from-decl nil number_fields nil)
|
|
(real_pred const-decl "[number_field -> boolean]" reals nil)
|
|
(real nonempty-type-from-decl nil reals nil)
|
|
(rational_pred const-decl "[real -> boolean]" rationals nil)
|
|
(rational nonempty-type-from-decl nil rationals nil)
|
|
(integer_pred const-decl "[rational -> boolean]" integers nil)
|
|
(int nonempty-type-eq-decl nil integers nil)
|
|
(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)
|
|
(/= const-decl "boolean" notequal nil))
|
|
nil))
|
|
(power_0_TCC1 0
|
|
(power_0_TCC1-1 nil 3552165738 ("" (subtype-tcc) nil nil)
|
|
((/= const-decl "boolean" notequal nil)) nil))
|
|
(power_0 0
|
|
(power_0-1 nil 3552165759 ("" (grind))
|
|
((expt def-decl "real" exponentiation nil)
|
|
(^ const-decl "real" exponentiation nil))
|
|
shostak))
|
|
(power_s_TCC1 0
|
|
(power_s_TCC1-1 nil 3552165738 ("" (subtype-tcc) nil nil)
|
|
((boolean nonempty-type-decl nil booleans nil)
|
|
(bool nonempty-type-eq-decl nil booleans nil)
|
|
(NOT const-decl "[bool -> bool]" booleans nil)
|
|
(number nonempty-type-decl nil numbers nil)
|
|
(number_field_pred const-decl "[number -> boolean]" number_fields
|
|
nil)
|
|
(number_field nonempty-type-from-decl nil number_fields nil)
|
|
(real_pred const-decl "[number_field -> boolean]" reals nil)
|
|
(real nonempty-type-from-decl nil reals nil)
|
|
(rational_pred const-decl "[real -> boolean]" rationals nil)
|
|
(rational nonempty-type-from-decl nil rationals nil)
|
|
(integer_pred const-decl "[rational -> boolean]" integers nil)
|
|
(int nonempty-type-eq-decl nil integers nil)
|
|
(int_minus_int_is_int application-judgement "int" integers nil)
|
|
(real_lt_is_strict_total_order name-judgement
|
|
"(strict_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)
|
|
(/= const-decl "boolean" notequal nil))
|
|
nil))
|
|
(power_s 0
|
|
(power_s-1 nil 3552165759 ("" (grind))
|
|
((boolean nonempty-type-decl nil booleans nil)
|
|
(bool nonempty-type-eq-decl nil booleans nil)
|
|
(NOT const-decl "[bool -> bool]" booleans nil)
|
|
(number nonempty-type-decl nil numbers nil)
|
|
(number_field_pred const-decl "[number -> boolean]" number_fields
|
|
nil)
|
|
(number_field nonempty-type-from-decl nil number_fields nil)
|
|
(real_pred const-decl "[number_field -> boolean]" reals nil)
|
|
(real nonempty-type-from-decl nil reals nil)
|
|
(rational_pred const-decl "[real -> boolean]" rationals nil)
|
|
(rational nonempty-type-from-decl nil rationals nil)
|
|
(integer_pred const-decl "[rational -> boolean]" integers nil)
|
|
(int nonempty-type-eq-decl nil integers nil)
|
|
(int_minus_int_is_int application-judgement "int" integers nil)
|
|
(real_times_real_is_real application-judgement "real" reals 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)
|
|
(expt def-decl "real" exponentiation nil)
|
|
(^ const-decl "real" exponentiation nil)
|
|
(int_plus_int_is_int application-judgement "int" integers nil)
|
|
(minus_int_is_int application-judgement "int" integers nil))
|
|
shostak))
|
|
(power_s_alt_TCC1 0
|
|
(power_s_alt_TCC1-1 nil 3575890745 ("" (subtype-tcc) nil nil)
|
|
((boolean nonempty-type-decl nil booleans nil)
|
|
(bool nonempty-type-eq-decl nil booleans nil)
|
|
(NOT const-decl "[bool -> bool]" booleans nil)
|
|
(number nonempty-type-decl nil numbers nil)
|
|
(number_field_pred const-decl "[number -> boolean]" number_fields
|
|
nil)
|
|
(number_field nonempty-type-from-decl nil number_fields nil)
|
|
(real_pred const-decl "[number_field -> boolean]" reals nil)
|
|
(real nonempty-type-from-decl nil reals nil)
|
|
(rational_pred const-decl "[real -> boolean]" rationals nil)
|
|
(rational nonempty-type-from-decl nil rationals nil)
|
|
(integer_pred const-decl "[rational -> boolean]" integers nil)
|
|
(int nonempty-type-eq-decl nil integers nil)
|
|
(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)
|
|
(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)
|
|
(/= const-decl "boolean" notequal nil))
|
|
nil))
|
|
(power_1_TCC1 0
|
|
(power_1_TCC1-1 nil 3552165738 ("" (subtype-tcc) nil nil)
|
|
((/= const-decl "boolean" notequal nil)) nil))
|
|
(power_1 0
|
|
(power_1-1 nil 3552165759 ("" (grind))
|
|
((expt def-decl "real" exponentiation nil)
|
|
(^ const-decl "real" exponentiation nil))
|
|
shostak))
|
|
(power_sum_TCC1 0
|
|
(power_sum_TCC1-1 nil 3552165738 ("" (subtype-tcc) nil nil)
|
|
((boolean nonempty-type-decl nil booleans nil)
|
|
(bool nonempty-type-eq-decl nil booleans nil)
|
|
(NOT const-decl "[bool -> bool]" booleans nil)
|
|
(number nonempty-type-decl nil numbers nil)
|
|
(number_field_pred const-decl "[number -> boolean]" number_fields
|
|
nil)
|
|
(number_field nonempty-type-from-decl nil number_fields nil)
|
|
(real_pred const-decl "[number_field -> boolean]" reals nil)
|
|
(real nonempty-type-from-decl nil reals nil)
|
|
(rational_pred const-decl "[real -> boolean]" rationals nil)
|
|
(rational nonempty-type-from-decl nil rationals nil)
|
|
(integer_pred const-decl "[rational -> boolean]" integers nil)
|
|
(int nonempty-type-eq-decl nil integers nil)
|
|
(real_lt_is_strict_total_order name-judgement
|
|
"(strict_total_order?[real])" real_props nil)
|
|
(int_plus_int_is_int application-judgement "int" integers nil)
|
|
(real_le_is_total_order name-judgement "(total_order?[real])"
|
|
real_props nil)
|
|
(real_ge_is_total_order name-judgement "(total_order?[real])"
|
|
real_props nil)
|
|
(/= const-decl "boolean" notequal nil))
|
|
nil))
|
|
(power_sum_TCC2 0
|
|
(power_sum_TCC2-1 nil 3552165738 ("" (subtype-tcc) nil nil)
|
|
((boolean nonempty-type-decl nil booleans nil)
|
|
(bool nonempty-type-eq-decl nil booleans nil)
|
|
(NOT const-decl "[bool -> bool]" booleans nil)
|
|
(number nonempty-type-decl nil numbers nil)
|
|
(number_field_pred const-decl "[number -> boolean]" number_fields
|
|
nil)
|
|
(number_field nonempty-type-from-decl nil number_fields nil)
|
|
(real_pred const-decl "[number_field -> boolean]" reals nil)
|
|
(real nonempty-type-from-decl nil reals nil)
|
|
(rational_pred const-decl "[real -> boolean]" rationals nil)
|
|
(rational nonempty-type-from-decl nil rationals nil)
|
|
(integer_pred const-decl "[rational -> boolean]" integers nil)
|
|
(int nonempty-type-eq-decl nil integers nil)
|
|
(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)
|
|
(/= const-decl "boolean" notequal nil))
|
|
nil))
|
|
(power_sum 0 (power_sum-1 nil 3552165759 ("" (grind)) nil shostak))
|
|
(power_mult_TCC1 0
|
|
(power_mult_TCC1-1 nil 3552165738 ("" (subtype-tcc) nil nil)
|
|
((boolean nonempty-type-decl nil booleans nil)
|
|
(bool nonempty-type-eq-decl nil booleans nil)
|
|
(NOT const-decl "[bool -> bool]" booleans nil)
|
|
(number nonempty-type-decl nil numbers nil)
|
|
(number_field_pred const-decl "[number -> boolean]" number_fields
|
|
nil)
|
|
(number_field nonempty-type-from-decl nil number_fields nil)
|
|
(real_pred const-decl "[number_field -> boolean]" reals nil)
|
|
(real nonempty-type-from-decl nil reals nil)
|
|
(rational_pred const-decl "[real -> boolean]" rationals nil)
|
|
(rational nonempty-type-from-decl nil rationals nil)
|
|
(integer_pred const-decl "[rational -> boolean]" integers nil)
|
|
(int nonempty-type-eq-decl nil integers nil)
|
|
(real_lt_is_strict_total_order name-judgement
|
|
"(strict_total_order?[real])" real_props nil)
|
|
(mult_divides1 application-judgement "(divides(n))" divides nil)
|
|
(mult_divides2 application-judgement "(divides(m))" divides 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)
|
|
(/= const-decl "boolean" notequal nil))
|
|
nil))
|
|
(power_mult_TCC2 0
|
|
(power_mult_TCC2-1 nil 3552165738 ("" (subtype-tcc) nil nil)
|
|
((boolean nonempty-type-decl nil booleans nil)
|
|
(bool nonempty-type-eq-decl nil booleans nil)
|
|
(NOT const-decl "[bool -> bool]" booleans nil)
|
|
(number nonempty-type-decl nil numbers nil)
|
|
(number_field_pred const-decl "[number -> boolean]" number_fields
|
|
nil)
|
|
(number_field nonempty-type-from-decl nil number_fields nil)
|
|
(real_pred const-decl "[number_field -> boolean]" reals nil)
|
|
(real nonempty-type-from-decl nil reals nil)
|
|
(rational_pred const-decl "[real -> boolean]" rationals nil)
|
|
(rational nonempty-type-from-decl nil rationals nil)
|
|
(integer_pred const-decl "[rational -> boolean]" integers nil)
|
|
(int nonempty-type-eq-decl nil integers nil)
|
|
(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)
|
|
(/= const-decl "boolean" notequal nil))
|
|
nil))
|
|
(power_mult 0
|
|
(power_mult-1 nil 3552165759
|
|
("" (auto-rewrite-theory "real_props")
|
|
(("" (grind)
|
|
(("" (auto-rewrite-theory "exponentiation")
|
|
(("" (use "expt_times_aux")
|
|
(("" (replace -1)
|
|
(("" (expand "expt") (("" (grind) nil nil)) nil)) nil))
|
|
nil))
|
|
nil))
|
|
nil))
|
|
nil)
|
|
((neg_times_lt formula-decl nil real_props nil)
|
|
(pos_times_ge formula-decl nil real_props nil)
|
|
(/= const-decl "boolean" notequal nil)
|
|
(zero_times3 formula-decl nil real_props nil)
|
|
(^ const-decl "real" exponentiation nil)
|
|
(expt def-decl "real" exponentiation nil)
|
|
(mult_divides1 application-judgement "(divides(n))" divides nil)
|
|
(mult_divides2 application-judgement "(divides(m))" divides nil)
|
|
(minus_int_is_int application-judgement "int" integers 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)
|
|
(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)
|
|
(expt_times_aux formula-decl nil exponentiation nil)
|
|
(x!1 skolem-const-decl "real" PowerInt nil)
|
|
(= const-decl "[T, T -> boolean]" equalities nil)
|
|
(>= const-decl "bool" reals nil)
|
|
(nat nonempty-type-eq-decl nil naturalnumbers nil)
|
|
(nzreal nonempty-type-eq-decl nil reals nil)
|
|
(zero_le_zero formula-decl nil real_props nil)
|
|
(expt_1n_aux formula-decl nil exponentiation nil)
|
|
(expt_minus_aux formula-decl nil exponentiation nil)
|
|
(int_minus_int_is_int application-judgement "int" integers nil)
|
|
(posnat_expt application-judgement "posnat" exponentiation nil)
|
|
(nat_expt application-judgement "nat" exponentiation nil)
|
|
(zero_times1 formula-decl nil real_props nil)
|
|
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
|
|
integers nil)
|
|
(even_times_int_is_even application-judgement "even_int" integers
|
|
nil))
|
|
shostak))
|
|
(power_mult2_TCC1 0
|
|
(power_mult2_TCC1-1 nil 3575890745 ("" (subtype-tcc) nil nil)
|
|
((boolean nonempty-type-decl nil booleans nil)
|
|
(bool nonempty-type-eq-decl nil booleans nil)
|
|
(NOT const-decl "[bool -> bool]" booleans nil)
|
|
(number nonempty-type-decl nil numbers nil)
|
|
(number_field_pred const-decl "[number -> boolean]" number_fields
|
|
nil)
|
|
(number_field nonempty-type-from-decl nil number_fields nil)
|
|
(real_pred const-decl "[number_field -> boolean]" reals nil)
|
|
(real nonempty-type-from-decl nil reals nil)
|
|
(rational_pred const-decl "[real -> boolean]" rationals nil)
|
|
(rational nonempty-type-from-decl nil rationals nil)
|
|
(integer_pred const-decl "[rational -> boolean]" integers nil)
|
|
(int nonempty-type-eq-decl nil integers nil)
|
|
(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_times_real_is_real application-judgement "real" reals nil)
|
|
(real_ge_is_total_order name-judgement "(total_order?[real])"
|
|
real_props nil)
|
|
(/= const-decl "boolean" notequal nil))
|
|
nil)))
|
|
|