Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
round.prf
Sprache: Unknown
|
(round (round_to_even0 0
(round_to_even0-1 nil 3507032123 ("" (grind) nil nil)
((round_to_even const-decl "integer" round nil)
(nonneg_ceiling_is_nat application-judgement "nat" floor_ceil
nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil
nil)
(nnint_times_nnint_is_nnint application-judgement
"nonneg_int" integers nil)
(even_times_int_is_even application-judgement "even_int"
integers nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(mult_divides2 application-judgement "(divides(m))" divides
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))
nil))
(round_to_even1 0
(round_to_even1-1 nil 3507032123
("" (skosimp*)
(("" (expand "abs")
(("" (lift-if)
(("" (prop)
(("1" (expand "round_to_even")
(("1" (lift-if) (("1" (ground) nil)))))
("2" (expand "round_to_even")
(("2" (lift-if) (("2" (ground) nil))))))))))))
nil)
((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil)
(minus_real_is_real application-judgement "real" reals 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)
(rat_div_nzrat_is_rat application-judgement "rat" rationals
nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(even_times_int_is_even application-judgement "even_int"
integers nil)
(round_to_even const-decl "integer" round nil)
(real_minus_real_is_real application-judgement "real" reals
nil))
nil))
(round_to_even2 0
(round_to_even2-1 nil 3507032123
("" (skosimp*)
(("" (expand "abs")
(("" (lift-if)
(("" (prop)
(("1" (expand "round_to_even")
(("1" (lift-if)
(("1" (ground)
(("1" (expand "integer?")
(("1" (propax) nil)))))))))
("2" (expand "round_to_even")
(("2" (lift-if)
(("2" (ground)
(("2" (expand "integer?")
(("2" (propax) nil))))))))))))))))
nil)
((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil)
(integer? const-decl "bool" integers nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(even_times_int_is_even application-judgement "even_int"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(round_to_even const-decl "integer" round nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals
nil)
(real_minus_real_is_real application-judgement "real" reals
nil))
nil))
(round1 0
(round1-1 nil 3507032123
("" (skosimp*)
(("" (expand "round")
(("" (lift-if)
(("" (prop)
(("1" (lemma "round_to_even1")
(("1" (inst?) (("1" (assert) nil)))))
("2" (grind) nil) ("3" (grind) nil)
("4" (grind) nil))))))))
nil)
((nonneg_floor_is_nat application-judgement "nat" floor_ceil
nil)
(round const-decl "integer" round 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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(round_to_even1 formula-decl nil round nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(sgn const-decl "int" real_defs nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil)
(real_plus_real_is_real application-judgement "real" reals
nil)
(minus_real_is_real application-judgement "real" reals nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(real_minus_real_is_real application-judgement "real" reals
nil))
nil))
(round_int 0
(round_int-1 nil 3507032123
("" (skosimp*)
(("" (expand "round")
(("" (lift-if)
(("" (ground)
(("1" (expand "round_to_even")
(("1" (lift-if) (("1" (ground) nil)))))
("2" (expand "abs")
(("2" (lift-if)
(("2" (expand "sgn")
(("2" (ground) nil))))))))))))))
nil)
((round const-decl "integer" round nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil
nil)
(int_abs_is_nonneg application-judgement
"{j: nonneg_int | j >= i}" real_defs 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)
(round_to_even const-decl "integer" round nil)
(minus_int_is_int application-judgement "int" integers nil)
(sgn const-decl "int" real_defs nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil))
nil)))
[ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
]
|
