|
(arithmetic_ops
(apply_TCC1 0
(apply_TCC1-1 nil 3507032124
("" (skolem-typepred) (("" (tcc) nil)) nil)
((rat_times_rat_is_rat application-judgement "rat" rationals nil)
(rat_plus_rat_is_rat application-judgement "rat" rationals nil)
(Sum def-decl "real" sum_hack nil)
(value_digit const-decl "nonneg_real" IEEE_854_values nil)
(value const-decl "real" IEEE_854_values nil)
(^ const-decl "real" exponentiation nil)
(expt def-decl "real" exponentiation nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(int_exp application-judgement "int" exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nzreal_expt application-judgement "nzreal" exponentiation nil)
(int_expt application-judgement "int" exponentiation nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_int_is_int application-judgement "int" integers nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(posnat_expt application-judgement "posnat" exponentiation nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(nzint_times_nzint_is_nzint application-judgement "nzint" integers
nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(zero? const-decl "bool" IEEE_854_values nil)
(div? adt-recognizer-decl "[fp_ops -> boolean]"
enumerated_type_defs nil)
(fp_ops type-decl nil enumerated_type_defs nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
nil)
(fp_num type-decl nil IEEE_854_values nil)
(E_min formal-const-decl "{i: integer | E_max > i}" arithmetic_ops
nil)
(E_max formal-const-decl "integer" arithmetic_ops nil)
(integer nonempty-type-from-decl nil integers nil)
(p formal-const-decl "above(1)" arithmetic_ops nil)
(b formal-const-decl "above(1)" arithmetic_ops nil)
(above nonempty-type-eq-decl nil integers 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)
(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))
nil)))
¤ Dauer der Verarbeitung: 0.24 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.
|
