Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
floor_div_lems.prf
Sprache: Unknown
|
(floor_div_lems
(floor_small_nat 0
(floor_small_nat-1 nil 3507028513
("" (skosimp*)
(("" (assert)
(("" (lemma "floor_small")
(("" (inst?) (("" (expand "abs") (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
((nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(integer nonempty-type-from-decl nil 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)
(/= const-decl "boolean" notequal nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(floor_small formula-decl nil floor_ceil nil))
nil))
(is_multiple 0
(is_multiple-1 nil 3507028513
("" (skosimp*)
(("" (iff 1)
(("" (split 1)
(("1" (flatten)
(("1" (inst 1 "i!1/j!1") (("1" (assert) nil)))))
("2" (flatten) (("2" (skosimp*) (("2" (assert) nil))))))))))
nil)
((mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(rat_times_rat_is_rat application-judgement "rat" rationals 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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(int nonempty-type-eq-decl nil integers nil)
(i!1 skolem-const-decl "int" floor_div_lems nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(j!1 skolem-const-decl "nonzero_integer" floor_div_lems nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil))
nil)))
[ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
]
|
|
