| products/sources/formale sprachen/PVS/complex/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Sprache: LispOriginal von: PVS© |
|
||||||
|
(complex_sets
(difference_TCC1 0 (difference_TCC1-1 nil 3385400933 ("" (skosimp) (("" (typepred "X!1") (("" (expand "nonempty?") (("" (expand "empty?") (("" (expand "member") (("" (skosimp) (("" (inst - "-x!1") (("" (rewrite "number_fields_negate_negate") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nonempty_set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets 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) (empty? const-decl "bool" sets nil) (number_fields_negate_negate formula-decl nil number_fields_bis nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (member const-decl "bool" sets nil) (minus_real_is_real application-judgement "real" reals nil) (minus_complex_is_complex application-judgement "complex" complex_types nil)) nil)) (plus_TCC1 0 (plus_TCC1-1 nil 3385400933 ("" (skosimp) (("" (typepred "X!1") (("" (typepred "Y!1") (("" (expand "nonempty?") (("" (expand "empty?") (("" (skosimp*) (("" (expand "member") (("" (inst - "x!2+x!1") (("" (inst + "x!2" "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nonempty_set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets 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) (real_plus_real_is_real application-judgement "real" reals nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (x!2 skolem-const-decl "real" complex_sets nil) (X!1 skolem-const-decl "nonempty_set[real]" complex_sets nil) (x!1 skolem-const-decl "real" complex_sets nil) (Y!1 skolem-const-decl "nonempty_set[real]" complex_sets nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil)) nil)) (difference_TCC2 0 (difference_TCC2-1 nil 3385400933 ("" (skosimp) (("" (typepred "X!1") (("" (typepred "Y!1") (("" (expand "nonempty?") (("" (expand "empty?") (("" (expand "member") (("" (skosimp*) (("" (inst - "x!2-x!1") (("" (inst + "x!2" "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nonempty_set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets 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) (member const-decl "bool" sets nil) (real_minus_real_is_real application-judgement "real" reals nil) (complex_minus_complex_is_complex application-judgement "complex" complex_types nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (x!2 skolem-const-decl "real" complex_sets nil) (X!1 skolem-const-decl "nonempty_set[real]" complex_sets nil) (x!1 skolem-const-decl "real" complex_sets nil) (Y!1 skolem-const-decl "nonempty_set[real]" complex_sets nil) (empty? const-decl "bool" sets nil)) nil)) (Arg_TCC1 0 (Arg_TCC1-1 nil 3295022236 ("" (skosimp) (("" (expand "nonempty?") (("" (expand "empty?") (("" (inst - "arg(n0z!1)") (("" (expand "member") (("" (inst + "0") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((complex_times_complex_is_complex application-judgement "complex" complex_types nil) (real_times_real_is_real application-judgement "real" reals nil) (nonempty? const-decl "bool" sets 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) (complex_pred const-decl "[number_field -> boolean]" complex_types nil) (complex nonempty-type-from-decl nil complex_types nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (pi_lb const-decl "posreal" trig_basic "trig/") (pi_ub const-decl "posreal" trig_basic "trig/") (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic "trig/") (<= const-decl "bool" reals nil) (argrng nonempty-type-eq-decl nil polar nil) (arg const-decl "argrng" polar nil) (/= const-decl "boolean" notequal nil) (nzcomplex nonempty-type-eq-decl nil complex_types 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) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil)) shostak)) (Arg_def 0 (Arg_def-1 nil 3386163620 ("" (skosimp) (("" (expand "Arg") (("" (apply-extensionality 1 :hide? t) (("" (case-replace "abs(n0z!1) * exp(x!1 * i) = n0z!1") (("1" (rewrite "exp_imag") (("1" (lemma "idempotent_polar" ("n0z" "n0z!1")) (("1" (expand "polar") (("1" (expand "from_polar") (("1" (assert) (("1" (name-replace "DRL100" "arg(n0z!1)") (("1" (lemma "eq_iff_periodic" ("a" "x!1" "b" "DRL100")) (("1" (replace -1 1 rl) (("1" (hide -1) (("1" (lemma "both_sides_times2" ("n0z" "abs(n0z!1)" "x" "sin(x!1)*i+cos(x!1)" "y" "sin(DRL100)*i+cos(DRL100)")) (("1" (assert) (("1" (hide -2 -3) (("1" (lemma "unique_characterization" ("x0" "cos(x!1)" "x1" "cos(DRL100)" "y0" "sin(x!1)" "y1" "sin(DRL100)")) (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "abs_nzcomplex" ("n0z" "n0z!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (skosimp) (("2" (replace -1) (("2" (hide -1) (("2" (lemma "exp_periodicity" ("x" "arg(n0z!1)*i" "j" "j!1")) (("2" (assert) (("2" (replace -1 1) (("2" (hide -1) (("2" (rewrite "exp_imag") (("2" (lemma "idempotent_polar" ("n0z" "n0z!1")) (("2" (expand "polar") (("2" (expand "from_polar") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((complex_times_complex_is_complex application-judgement "complex" complex_types nil) (real_times_real_is_real application-judgement "real" reals nil) (Arg const-decl "nonempty_set[real]" complex_sets nil) (idempotent_polar formula-decl nil polar nil) (from_polar const-decl "complex" polar 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) (both_sides_times2 formula-decl nil number_fields_bis nil) (nznum nonempty-type-eq-decl nil number_fields nil) (sin const-decl "real" trig_basic "trig/") (cos const-decl "real" trig_basic "trig/") (unique_characterization formula-decl nil complex_types nil) (abs_nzcomplex formula-decl nil polar nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (eq_iff_periodic formula-decl nil trig_aux nil) (polar const-decl "[nnreal, argrng]" polar nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (cos_range application-judgement "trig_range" trig_basic "trig/") (sin_range application-judgement "trig_range" trig_basic "trig/") (exp_imag formula-decl nil exp nil) (exp_periodicity formula-decl nil exp 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 "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (complex_pred const-decl "[number_field -> boolean]" complex_types nil) (complex nonempty-type-from-decl nil complex_types nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (pi_lb const-decl "posreal" trig_basic "trig/") (pi_ub const-decl "posreal" trig_basic "trig/") (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic "trig/") (<= const-decl "bool" reals nil) (argrng nonempty-type-eq-decl nil polar nil) (arg const-decl "argrng" polar nil) (/= const-decl "boolean" notequal nil) (nzcomplex nonempty-type-eq-decl nil complex_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnreal type-eq-decl nil real_types nil) (abs const-decl "nnreal" polar nil) (exp const-decl "nzcomplex" exp nil) (i const-decl "complex" complex_types 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)) shostak)) (Arg_mult 0 (Arg_mult-1 nil 3295023222 ("" (skolem 1 ("a" "b")) (("" (apply-extensionality :hide? t) (("" (expand "Arg") (("" (rewrite "arg_mult") (("" (case-replace "(EXISTS (x: (Arg(a)), y: (Arg(b))): x!1 = x + y)") (("1" (skosimp*) (("1" (typepred "x!2") (("1" (typepred "y!1") (("1" (expand "Arg") (("1" (skosimp*) (("1" (replace -1) (("1" (replace -2) (("1" (case-replace "arg(a)+arg(b)>pi") (("1" (inst + "j!1+j!2+1") (("1" (assert) nil nil)) nil) ("2" (case-replace "arg(a) + arg(b) <= -pi") (("1" (inst + "j!1+j!2-1") (("1" (assert) nil nil)) nil) ("2" (inst + "j!1+j!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (skosimp*) (("2" (case-replace "arg(a) + arg(b) > pi") (("1" (inst + "arg(a)" "arg(b)+2*(j!1-1)*pi") (("1" (assert) nil nil) ("2" (expand "Arg") (("2" (inst + "j!1-1") (("2" (assert) nil nil)) nil)) nil) ("3" (expand "Arg") (("3" (inst + "0") (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (case-replace "arg(a) + arg(b) <= -pi") (("1" (assert) (("1" (inst + "arg(a)" "arg(b)+2*(j!1+1)*pi") (("1" (assert) nil nil) ("2" (expand "Arg") (("2" (inst + "j!1+1") (("2" (assert) nil nil)) nil)) nil) ("3" (expand "Arg") (("3" (inst + "0") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst + "arg(a)" "arg(b)+2*j!1*pi") (("1" (assert) nil nil) ("2" (expand "Arg") (("2" (inst + "j!1") nil nil)) nil) ("3" (expand "Arg") (("3" (inst + "0") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (set type-eq-decl nil sets nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (Arg const-decl "nonempty_set[real]" complex_sets nil) (nonempty_set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (nzcomplex nonempty-type-eq-decl nil complex_types nil) (/= const-decl "boolean" notequal nil) (complex nonempty-type-from-decl nil complex_types nil) (complex_pred const-decl "[number_field -> boolean]" complex_types nil) (nzcomplex_times_nzcomplex_is_nzcomplex application-judgement "nzcomplex" complex_types nil) (arg_mult formula-decl nil polar nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (a skolem-const-decl "nzcomplex" complex_sets nil) (b skolem-const-decl "nzcomplex" complex_sets nil) (j!1 skolem-const-decl "int" complex_sets nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_nzcomplex_is_nzcomplex application-judgement "nzcomplex" complex_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" 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) (complex_minus_complex_is_complex application-judgement "complex" complex_types nil) (> const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (pi_lb const-decl "posreal" trig_basic "trig/") (pi_ub const-decl "posreal" trig_basic "trig/") (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic "trig/") (<= const-decl "bool" reals nil) (argrng nonempty-type-eq-decl nil polar nil) (arg const-decl "argrng" polar nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (complex_times_complex_is_complex application-judgement "complex" complex_types nil)) shostak)) (Arg_inv 0 (Arg_inv-1 nil 3295024532 ("" (skolem 1 ("a")) (("" (apply-extensionality :hide? t) (("" (expand "Arg") (("" (rewrite "arg_inv") (("" (case-replace "(EXISTS j: -x!1 = arg(a) + 2 * (j * pi))") (("1" (skosimp*) (("1" (case-replace "arg(a)=0") (("1" (inst + "-j!1") (("1" (assert) nil nil)) nil) ("2" (case-replace "arg(a) = pi") (("1" (inst + "-j!1-1") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (inst + "-j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (skosimp*) (("2" (case-replace "arg(a) = pi") (("1" (assert) (("1" (inst + "-j!1-1") (("1" (assert) nil nil)) nil)) nil) ("2" (inst + "-j!1") (("2" (case-replace "arg(a)=0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (set type-eq-decl nil sets nil) (- const-decl "[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) (Arg const-decl "nonempty_set[real]" complex_sets nil) (nonempty_set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (nzcomplex nonempty-type-eq-decl nil complex_types nil) (/= const-decl "boolean" notequal nil) (complex nonempty-type-from-decl nil complex_types nil) (complex_pred const-decl "[number_field -> boolean]" complex_types nil) (nzcomplex_div_nzcomplex_is_nzcomplex application-judgement "nzcomplex" complex_types nil) (minus_complex_is_complex application-judgement "complex" complex_types nil) (minus_real_is_real application-judgement "real" reals nil) (arg_inv formula-decl nil polar nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (complex_minus_complex_is_complex application-judgement "complex" complex_types nil) (int_minus_int_is_int application-judgement "int" integers nil) (minus_int_is_int application-judgement "int" integers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (arg const-decl "argrng" polar nil) (argrng nonempty-type-eq-decl nil polar nil) (<= const-decl "bool" reals nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic "trig/") (pi_ub const-decl "posreal" trig_basic "trig/") (pi_lb const-decl "posreal" trig_basic "trig/") (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) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities 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_plus_real_is_real application-judgement "real" reals nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (real_times_real_is_real application-judgement "real" reals nil) (complex_times_complex_is_complex application-judgement "complex" complex_types nil)) shostak)) (Arg_div 0 (Arg_div-1 nil 3295024788 ("" (skolem 1 ("a" "b")) (("" (rewrite "div_def") (("" (rewrite "Arg_mult") (("1" (apply-extensionality :hide? t) (("1" (case-replace "(EXISTS (x: (Arg(a)), y: (Arg(b))): x!1 = x - y)") (("1" (skosimp*) (("1" (typepred "x!2") (("1" (typepred "y!1") (("1" (inst + "x!2" "-y!1") (("1" (rewrite "minus_add") nil nil) ("2" (rewrite "Arg_inv") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (skosimp*) (("2" (typepred "x!2") (("2" (typepred "y!1") (("2" (rewrite "Arg_inv") (("2" (assert) (("2" (inst + "x!2" "-y!1") (("2" (rewrite "minus_add") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "real_is_complex" ("x" "1")) (("2" (rewrite "closed_divides") nil nil)) nil)) nil)) nil)) nil) ((div_def formula-decl nil number_fields 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) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (complex_pred const-decl "[number_field -> boolean]" complex_types nil) (complex nonempty-type-from-decl nil complex_types nil) (nzcomplex nonempty-type-eq-decl nil complex_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nzcomplex_div_nzcomplex_is_nzcomplex application-judgement "nzcomplex" complex_types nil) (nzcomplex_times_nzcomplex_is_nzcomplex application-judgement "nzcomplex" complex_types nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (Arg const-decl "nonempty_set[real]" complex_sets nil) (nonempty_set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (Arg_inv formula-decl nil complex_sets nil) (minus_nzcomplex_is_nzcomplex application-judgement "nzcomplex" complex_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (minus_add formula-decl nil number_fields nil) (y!1 skolem-const-decl "(Arg(b))" complex_sets nil) (- const-decl "[numfield -> numfield]" number_fields nil) (b skolem-const-decl "nzcomplex" complex_sets nil) (minus_complex_is_complex application-judgement "complex" complex_types nil) (minus_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (complex_minus_complex_is_complex application-judgement "complex" complex_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (Arg_mult formula-decl nil complex_sets nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)) shostak))) ¤ Dauer der Verarbeitung: 0.972 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.Bot Zugriff |
