mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
98 lines
4.1 KiB
Plaintext
98 lines
4.1 KiB
Plaintext
(ExpLog
|
|
(exp_zero 0
|
|
(exp_zero-1 nil 3552165298 ("" (default-strategy))
|
|
((exp_0 formula-decl nil ln_exp "lnexp/")) shostak))
|
|
(exp_sum 0
|
|
(exp_sum-1 nil 3552165298 ("" (grind) (("" (postpone) nil nil)) nil)
|
|
nil shostak))
|
|
(log_TCC1 0
|
|
(log_TCC1-1 nil 3552164963 ("" (grind) 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)
|
|
(real_ge_is_total_order name-judgement "(total_order?[real])"
|
|
real_props nil)
|
|
(real_gt_is_strict_total_order name-judgement
|
|
"(strict_total_order?[real])" real_props nil))
|
|
nil))
|
|
(log_one 0
|
|
(log_one-1 nil 3552165298 ("" (default-strategy))
|
|
((real_gt_is_strict_total_order name-judgement
|
|
"(strict_total_order?[real])" real_props nil)
|
|
(ln_1 formula-decl nil ln_exp "lnexp/"))
|
|
shostak))
|
|
(log_mul_TCC1 0
|
|
(log_mul_TCC1-1 nil 3552164963 ("" (grind) 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)
|
|
(real_ge_is_total_order name-judgement "(total_order?[real])"
|
|
real_props 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))
|
|
nil))
|
|
(log_mul_TCC2 0
|
|
(log_mul_TCC2-1 nil 3552164963 ("" (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)
|
|
(real_ge_is_total_order name-judgement "(total_order?[real])"
|
|
real_props nil)
|
|
(real_gt_is_strict_total_order name-judgement
|
|
"(strict_total_order?[real])" real_props nil))
|
|
nil))
|
|
(log_mul 0
|
|
(log_mul-1 nil 3552165298 ("" (default-strategy)) nil shostak))
|
|
(log_exp_TCC1 0
|
|
(log_exp_TCC1-1 nil 3552164963 ("" (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)
|
|
(real_ge_is_total_order name-judgement "(total_order?[real])"
|
|
real_props nil)
|
|
(real_gt_is_strict_total_order name-judgement
|
|
"(strict_total_order?[real])" real_props nil))
|
|
nil))
|
|
(log_exp 0
|
|
(log_exp-1 nil 3552165298 ("" (default-strategy))
|
|
((real_gt_is_strict_total_order name-judgement
|
|
"(strict_total_order?[real])" real_props 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))
|
|
shostak))
|
|
(exp_log 0
|
|
(exp_log-1 nil 3552165298 ("" (default-strategy)) nil shostak)))
|
|
|