| products/sources/formale Sprachen/C/Lyx/po/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: fr.po Sprache: Unknown
|
(rem (ml1 0
(ml1-1 nil 3249307029 ("" (skolem!) (("" (expand "div") (("" (expand "sgn") (("" (expand "abs") (("" (assert) (("" (lemma "both_sides_times_pos_lt1") (("" (inst - "m!1" "n!1/m!1" "floor(n!1/m!1)+1") (("" (flatten) (("" (ground) (("" (typepred "floor(n!1 / m!1)") (("" (propax) nil)))))))))))))))))))) nil) ((int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (div const-decl "integer" div nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil 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) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (nnint_plus_posint_is_posint application-judgement "posint" 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) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (sgn const-decl "int" real_defs nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil)) nil)) (ml3 0 (ml3-1 nil 3249307029 ("" (skosimp*) (("" (case "i!1 >= 0") (("1" (expand "abs") (("1" (lift-if) (("1" (split 1) (("1" (flatten) (("1" (lemma "div_smaller") (("1" (inst?) (("1" (assert) nil))))))) ("2" (flatten) (("2" (lemma "ml1") (("2" (inst?) nil))))))))))) ("2" (expand "abs") (("2" (lift-if) (("2" (lemma "div_neg") (("2" (inst?) (("2" (split 2) (("1" (flatten) (("1" (lemma "ml1") (("1" (inst -1 "m!1" "-i!1") (("1" (assert) nil) ("2" (assert) nil))))))) ("2" (flatten) (("2" (lemma "div_smaller") (("2" (inst -1 "m!1" "-i!1") (("1" (assert) nil) ("2" (assert) nil)))))))))))))))))))) 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) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (ml1 formula-decl nil rem nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (i!1 skolem-const-decl "int" rem nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (div_smaller formula-decl nil div nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (/= const-decl "boolean" notequal nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (minus_int_is_int application-judgement "int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (div_nat formula-decl nil div nil) (div_neg formula-decl nil div nil) (int_minus_int_is_int application-judgement "int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil)) nil)) (rem_TCC1 0 (rem_TCC1-1 nil 3249307029 ("" (skosimp*) (("" (lemma "ml3") (("" (case "j!1 >= 0") (("1" (inst?) (("1" (expand "abs" 1 2) (("1" (assert) nil))) ("2" (assert) nil))) ("2" (inst -1 "i!1" "-j!1") (("1" (lemma "div_neg_d") (("1" (inst?) (("1" (replace -1) (("1" (expand "abs" 2 2) (("1" (assert) nil))))))))) ("2" (assert) nil)))))))) nil) ((ml3 formula-decl nil rem nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (minus_int_is_int application-judgement "int" integers nil) (div_neg_d formula-decl nil div 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (j!1 skolem-const-decl "nonzero_integer" rem nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (abs_nat_rew formula-decl nil abs_rews 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" 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) (/= const-decl "boolean" notequal nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil)) nil)) (rem_neg 0 (rem_neg-1 nil 3249307029 ("" (skosimp*) (("" (expand "rem") (("" (rewrite "div_neg") (("" (assert) nil)))))) nil) ((mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (rem const-decl "{k | abs(k) < abs(j)}" rem nil) (minus_int_is_int application-judgement "int" 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (div_neg formula-decl nil div nil)) nil)) (rem_neg_d 0 (rem_neg_d-1 nil 3249307029 ("" (skosimp*) (("" (expand "rem") (("" (rewrite "div_neg_d") (("" (assert) nil)))))) nil) ((mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (rem const-decl "{k | abs(k) < abs(j)}" rem nil) (minus_int_is_int application-judgement "int" 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (div_neg_d formula-decl nil div nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil)) nil)) (rem_even 0 (rem_even-1 nil 3249307029 ("" (skosimp*) (("" (expand "rem") (("" (rewrite "div_even") nil)))) nil) ((mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (rem const-decl "{k | abs(k) < abs(j)}" rem nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (div_even formula-decl nil div nil)) nil)) (rem_eq_arg 0 (rem_eq_arg-1 nil 3249307029 ("" (skolem!) (("" (expand "rem") (("" (rewrite "div_eq_arg") (("" (assert) nil)))))) nil) ((mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (rem const-decl "{k | abs(k) < abs(j)}" rem nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (div_eq_arg formula-decl nil div nil)) nil)) (rem_zero 0 (rem_zero-1 nil 3249307029 ("" (skosimp*) (("" (expand "rem") (("" (rewrite "div_zero") (("" (assert) nil)))))) nil) ((rem const-decl "{k | abs(k) < abs(j)}" rem nil) (int_times_even_is_even application-judgement "even_int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (div_zero formula-decl nil div nil)) nil)) (rem_lt 0 (rem_lt-1 nil 3249307029 ("" (skosimp*) (("" (expand "rem") (("" (rewrite "div_lt") (("" (assert) nil)))))) nil) ((mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (rem const-decl "{k | abs(k) < abs(j)}" rem nil) (int_times_even_is_even application-judgement "even_int" integers nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (div_lt formula-decl nil div nil)) nil)) (rem_it_is 0 (rem_it_is-1 nil 3249307029 ("" (skosimp*) (("" (expand "rem") (("" (case "div(a!1,m!1) = c!1") (("1" (assert) nil) ("2" (hide 2) (("2" (expand "div") (("2" (expand "sgn") (("2" (expand "abs") (("2" (replace -1) (("2" (hide -1) (("2" (lemma "floor_plus_int") (("2" (case "(b!1 + m!1 * c!1) / m!1 = b!1 / m!1 + c!1") (("1" (replace -1) (("1" (hide -1) (("1" (inst -1 "c!1" "b!1/m!1") (("1" (replace -1) (("1" (hide -1) (("1" (lemma "floor_small") (("1" (inst?) (("1" (expand "abs") (("1" (assert) nil))))))))))))))))) ("2" (hide -1 -2 2) (("2" (assert) nil)))))))))))))))))))))))) nil) ((nil application-judgement "nat" div nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (rem const-decl "{k | abs(k) < abs(j)}" rem nil) (sgn const-decl "int" real_defs nil) (floor_plus_int formula-decl nil floor_ceil nil) (floor_small formula-decl nil floor_ceil nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nnrat_plus_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (div_nat formula-decl nil div nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers 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) (= const-decl "[T, T -> boolean]" equalities 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) (/= const-decl "boolean" notequal nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (integer nonempty-type-from-decl nil integers nil) (div const-decl "integer" div nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil)) nil)) (rem_eq_0 0 (rem_eq_0-1 nil 3249307029 ("" (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) (/= const-decl "boolean" notequal nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (real_ge_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) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (int_minus_int_is_int application-judgement "int" integers nil) (rem const-decl "{k | abs(k) < abs(j)}" rem nil) (div const-decl "integer" div nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)) nil)) (rem_one 0 (rem_one-1 nil 3249307029 ("" (skosimp*) (("" (lift-if) (("" (split 1) (("1" (flatten) (("1" (expand "abs") (("1" (lift-if) (("1" (split -1) (("1" (flatten) (("1" (lemma "rem_eq_arg") (("1" (inst -1 "1") (("1" (lemma "rem_neg_d") (("1" (inst -1 "1" "1") (("1" (assert) nil))))))))))) ("2" (flatten) (("2" (lemma "rem_eq_arg") (("2" (inst?) (("2" (assert) nil))))))))))))))) ("2" (flatten) (("2" (lemma "rem_lt") (("2" (inst?) (("2" (expand "abs") (("2" (lift-if) (("2" (ground) nil)))))))))))))))) nil) ((rem_lt formula-decl nil rem 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) (int nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (rem_neg_d formula-decl nil rem nil) (rem_eq_arg formula-decl nil rem nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil)) nil)) (rem_TCC2 0 (rem_TCC2-1 nil 3249307029 ("" (skosimp*) (("" (expand "rem") (("" (lemma "div_smaller") (("" (inst?) (("" (assert) (("" (lemma "ml1") (("" (inst - "m!1" "n!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nil application-judgement "nat" div nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (rem const-decl "{k | abs(k) < abs(j)}" rem 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) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (ml1 formula-decl nil rem nil) (div_nat formula-decl nil div 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) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (div_smaller formula-decl nil div nil)) nil))) [ zur Elbe Produktseite wechseln0.10Quellennavigators Analyse erneut starten ] |