|
(convergence_aux
(IMP_metric_space_TCC1 0
(IMP_metric_space_TCC1-1 nil 3391875462
("" (expand "metric?")
(("" (expand "metric_zero?")
(("" (expand "metric_symmetric?")
(("" (expand "metric_triangle?") (("" (grind) nil nil)) nil))
nil))
nil))
nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(metric_zero? const-decl "bool" metric_def nil)
(metric_triangle? const-decl "bool" metric_def 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)
(minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(metric_symmetric? const-decl "bool" metric_def nil)
(metric? const-decl "bool" metric_def nil))
nil))
(bounded_seq_def 0
(bounded_seq_def-1 nil 3391990104
("" (skosimp)
(("" (expand "bounded_above?")
(("" (expand "bounded_seq?")
(("" (expand "fullset")
(("" (expand "image")
(("" (expand "bounded?")
(("" (expand "subset?")
(("" (expand "member")
(("" (expand "bounded_below?")
(("" (expand "ball")
(("" (split)
(("1" (flatten)
(("1" (skosimp)
(("1" (split)
(("1"
(inst + "x!1+r!1")
(("1"
(skolem + ("n!1"))
(("1"
(inst - "u!1(n!1)")
(("1"
(split -1)
(("1" (grind) nil nil)
("2"
(hide 2)
(("2" (inst + "n!1") nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst + "x!1-r!1")
(("2"
(skolem + ("n!1"))
(("2"
(inst - "u!1(n!1)")
(("2"
(split)
(("1" (grind) nil nil)
("2" (inst + "n!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (inst + "(a!2+a!1)/2" "a!1-a!2+1")
(("1" (skosimp)
(("1"
(skolem - ("n!1"))
(("1"
(inst - "n!1")
(("1"
(inst - "n!1")
(("1" (grind) nil nil))
nil))
nil))
nil))
nil)
("2" (inst - "0")
(("2"
(inst - "0")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((bounded_above? const-decl "bool" real_fun_preds "reals/")
(fullset const-decl "set" sets nil)
(bounded? const-decl "bool" metric_space_def nil)
(member const-decl "bool" sets nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(ball const-decl "set[T]" metric_space_def nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(a!2 skolem-const-decl "real" convergence_aux nil)
(a!1 skolem-const-decl "real" convergence_aux nil)
(real_div_nzreal_is_real application-judgement "real" reals 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)
(minus_real_is_real application-judgement "real" reals nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(TRUE const-decl "bool" booleans 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(sequence type-eq-decl nil sequences 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)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(real_plus_real_is_real application-judgement "real" reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(bounded_below? const-decl "bool" real_fun_preds "reals/")
(subset? const-decl "bool" sets nil)
(image const-decl "set[R]" function_image nil)
(bounded_seq? const-decl "bool" convergence_aux nil))
shostak))
(upper_bound?_TCC1 0
(upper_bound?_TCC1-1 nil 3425705935
("" (skosimp)
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (inst - "u!1(0)")
(("" (expand "fullset")
(("" (expand "image")
(("" (expand "member") (("" (inst + "0") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
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)
(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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(sequence type-eq-decl nil sequences nil)
(image const-decl "set[R]" function_image nil)
(TRUE const-decl "bool" booleans nil)
(member const-decl "bool" sets nil)
(fullset const-decl "set" sets nil)
(empty? const-decl "bool" sets nil))
nil))
(lub_TCC1 0
(lub_TCC1-1 nil 3391918402
("" (skosimp)
(("" (typepred "ua!1")
(("" (split)
(("1" (expand "nonempty?")
(("1" (expand "empty?")
(("1" (inst - "ua!1(0)")
(("1" (expand "fullset")
(("1" (expand "image")
(("1" (expand "member") (("1" (inst + "0") nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "bounded_above?")
(("2" (expand "fullset")
(("2" (expand "image")
(("2" (expand "upper_bound?")
(("2" (skosimp)
(("2" (inst + "a!1")
(("2" (skosimp)
(("2" (typepred "s!1")
(("2" (skosimp)
(("2" (inst - "x!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((bounded_above? const-decl "bool" real_fun_preds "reals/")
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(bounded_above? const-decl "bool" bounded_real_defs nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(upper_bound? const-decl "bool" bounded_real_defs nil)
(nonempty? const-decl "bool" sets nil)
(image const-decl "set[R]" function_image nil)
(TRUE const-decl "bool" booleans nil)
(member const-decl "bool" sets nil)
(fullset const-decl "set" sets nil)
(empty? const-decl "bool" sets nil))
nil))
(glb_TCC1 0
(glb_TCC1-1 nil 3391918402
("" (skosimp)
(("" (typepred "ub!1")
(("" (split)
(("1" (expand "nonempty?")
(("1" (expand "empty?")
(("1" (inst - "ub!1(0)")
(("1" (expand "image")
(("1" (expand "member")
(("1" (inst + "0")
(("1" (expand "fullset") (("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "fullset")
(("2" (expand "image")
(("2" (expand "bounded_below?")
(("2" (expand "lower_bound?")
(("2" (skosimp)
(("2" (inst + "a!1")
(("2" (skosimp)
(("2" (typepred "s!1")
(("2" (skosimp)
(("2" (inst - "x!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((bounded_below? const-decl "bool" real_fun_preds "reals/")
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(bounded_below? const-decl "bool" bounded_real_defs nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(TRUE const-decl "bool" booleans nil)
(lower_bound? const-decl "bool" bounded_real_defs nil)
(nonempty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil) (set type-eq-decl nil sets nil)
(fullset const-decl "set" sets nil)
(image const-decl "set[R]" function_image nil)
(empty? const-decl "bool" sets nil))
nil))
(converges_upto_bounded_above 0
(converges_upto_bounded_above-1 nil 3391917155
("" (skosimp)
(("" (expand "converges_upto?")
(("" (flatten)
(("" (expand "bounded_above?")
(("" (inst + "x!1")
(("" (skolem + ("n!1"))
(("" (rewrite "metric_convergence_def")
(("" (expand "metric_converges_to")
(("" (inst - "u!1(n!1)-x!1")
(("1" (skosimp)
(("1" (expand "member")
(("1" (expand "ball")
(("1" (inst - "n!1+n!2")
(("1" (assert)
(("1"
(expand "increasing?")
(("1"
(inst - "n!1" "n!1+n!2")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((converges_upto? const-decl "bool" convergence_aux nil)
(bounded_above? const-decl "bool" real_fun_preds "reals/")
(metric_converges_to const-decl "bool" metric_space_def nil)
(ball const-decl "set[T]" metric_space_def 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)
(increasing? const-decl "bool" real_fun_preds "reals/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(member const-decl "bool" sets nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(x!1 skolem-const-decl "real" convergence_aux nil)
(n!1 skolem-const-decl "nat" convergence_aux nil)
(u!1 skolem-const-decl "sequence[real]" convergence_aux nil)
(real_minus_real_is_real application-judgement "real" reals 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)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(sequence type-eq-decl nil sequences nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(metric_convergence_def formula-decl nil metric_space 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))
(converges_upto_le 0
(converges_upto_le-1 nil 3391878287
("" (skosimp)
(("" (skosimp)
(("" (expand "converges_upto?")
(("" (flatten)
(("" (rewrite "metric_convergence_def" -1)
(("" (expand "metric_converges_to")
(("" (case "u!1(n!1)>x!1")
(("1" (hide 1)
(("1" (inst - " u!1(n!1) - x!1")
(("1" (skosimp)
(("1" (inst - "max(n!1,n!2)")
(("1" (expand "increasing?")
(("1" (inst - "n!1" "max(n!1,n!2)")
(("1" (grind) nil nil)) nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((metric_converges_to const-decl "bool" metric_space_def nil)
(increasing? const-decl "bool" real_fun_preds "reals/")
(minus_real_is_real application-judgement "real" reals nil)
(member const-decl "bool" sets nil)
(ball const-decl "set[T]" metric_space_def nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(ball_is_metric_open application-judgement "metric_open"
convergence_aux nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(nat_max application-judgement "{k: nat | i <= k AND j <= k}"
real_defs nil)
(nonneg_rat_max application-judgement
"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(x!1 skolem-const-decl "real" convergence_aux nil)
(n!1 skolem-const-decl "nat" convergence_aux nil)
(u!1 skolem-const-decl "sequence[real]" convergence_aux nil)
(real_minus_real_is_real application-judgement "real" reals 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)
(> const-decl "bool" reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(sequence type-eq-decl nil sequences nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(metric_convergence_def formula-decl nil metric_space nil)
(converges_upto? const-decl "bool" convergence_aux nil))
shostak))
(converges_upto_def 0
(converges_upto_def-1 nil 3391875736
("" (skosimp*)
(("" (expand "converges_upto?")
(("" (case-replace "increasing?(u!1)")
(("1" (assert)
(("1" (split)
(("1" (flatten)
(("1" (lemma "converges_upto_le" ("u" "u!1" "x" "x!1"))
(("1" (split -1)
(("1" (replace -1)
(("1" (rewrite "metric_convergence_def" *)
(("1" (skosimp)
(("1" (expand "metric_converges_to")
(("1" (expand "ball")
(("1" (expand "member")
(("1"
(inst -2 "r!1")
(("1"
(skosimp)
(("1"
(inst + "n!1")
(("1"
(skosimp)
(("1"
(inst - "i!1")
(("1"
(inst - "i!1")
(("1"
(assert)
(("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "converges_upto?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (rewrite "metric_convergence_def" *)
(("2" (expand "metric_converges_to")
(("2" (skosimp)
(("2" (inst -2 "r!1")
(("2" (skosimp)
(("2" (inst + "n!1")
(("2" (skosimp)
(("2" (expand "ball")
(("2"
(expand "member")
(("2"
(inst - "i!1")
(("2"
(inst - "i!1")
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
((converges_upto? const-decl "bool" convergence_aux nil)
(metric_convergence_def formula-decl nil metric_space nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(metric_converges_to const-decl "bool" metric_space_def nil)
(member const-decl "bool" sets nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(ball const-decl "set[T]" metric_space_def nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(converges_upto_le formula-decl nil convergence_aux nil)
(sequence type-eq-decl nil sequences nil)
(increasing? const-decl "bool" real_fun_preds "reals/")
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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))
shostak))
(converges_upto_is_lub 0
(converges_upto_is_lub-1 nil 3391878113
("" (skosimp)
(("" (split)
(("1" (flatten)
(("1"
(lemma "converges_upto_bounded_above" ("u" "u!1" "x" "x!1"))
(("1" (assert)
(("1" (lemma "converges_upto_le" ("u" "u!1" "x" "x!1"))
(("1" (assert)
(("1" (expand "least_upper_bound?")
(("1" (split)
(("1" (expand "converges_upto?")
(("1" (flatten) nil nil)) nil)
("2" (expand "fullset")
(("2" (expand "image")
(("2" (expand "upper_bound?")
(("2" (skosimp)
(("2" (typepred "s!1")
(("2"
(skosimp)
(("2"
(inst - "x!2")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (skosimp)
(("3" (expand "fullset")
(("3" (expand "image")
(("3" (expand "upper_bound?")
(("3" (expand "converges_upto?")
(("3"
(flatten)
(("3"
(rewrite "metric_convergence_def" -4)
(("3"
(expand "metric_converges_to")
(("3"
(case "x!1>y!1")
(("1"
(inst -5 "x!1-y!1")
(("1"
(hide 1)
(("1"
(skosimp)
(("1"
(expand "ball")
(("1"
(expand "member")
(("1"
(inst - "u!1(n!1)")
(("1"
(inst - "n!1")
(("1"
(inst - "n!1")
(("1"
(assert)
(("1"
(expand
"abs")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(inst + "n!1")
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (expand "converges_upto?")
(("2" (assert)
(("2" (rewrite "metric_convergence_def" 1)
(("2" (expand "metric_converges_to")
(("2" (skosimp)
(("2" (expand "ball")
(("2" (expand "member")
(("2" (expand "fullset")
(("2" (expand "image")
(("2" (expand "least_upper_bound?")
(("2" (flatten)
(("2"
(expand "upper_bound?")
(("2"
(case
"exists n: FORALL i: i >= n IMPLIES x!1 - u!1(i) < r!1")
(("1"
(skosimp)
(("1"
(inst + "n!1")
(("1"
(skosimp)
(("1"
(inst - "i!1")
(("1"
(inst - "u!1(i!1)")
(("1"
(assert)
(("1"
(hide-all-but
(-1 -4 1))
(("1" (grind) nil nil))
nil))
nil)
("2"
(inst + "i!1")
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(inst -4 "x!1-r!1")
(("2"
(assert)
(("2"
(skosimp)
(("2"
(typepred "s!1")
(("2"
(skosimp)
(("2"
(inst + "x!2")
(("2"
(skosimp)
(("2"
(expand
"increasing?")
(("2"
(inst
-
"x!2"
"i!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sequence type-eq-decl nil sequences nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(converges_upto_bounded_above formula-decl nil convergence_aux nil)
(converges_upto_le formula-decl nil convergence_aux nil)
(least_upper_bound? const-decl "bool" bounded_real_defs nil)
(metric_convergence_def formula-decl nil metric_space nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(> const-decl "bool" reals nil)
(ball const-decl "set[T]" metric_space_def nil)
(u!1 skolem-const-decl "sequence[real]" convergence_aux nil)
(n!1 skolem-const-decl "nat" convergence_aux nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(member const-decl "bool" sets nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(y!1 skolem-const-decl "real" convergence_aux nil)
(x!1 skolem-const-decl "real" convergence_aux nil)
(real_minus_real_is_real application-judgement "real" reals 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)
(metric_converges_to const-decl "bool" metric_space_def nil)
(fullset const-decl "set" sets nil)
(upper_bound? const-decl "bool" bounded_real_defs nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(TRUE const-decl "bool" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(image const-decl "set[R]" function_image nil)
(converges_upto? const-decl "bool" convergence_aux nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(< const-decl "bool" reals nil)
(i!1 skolem-const-decl "nat" convergence_aux nil)
(increasing? const-decl "bool" real_fun_preds "reals/"))
shostak))
(bounded_above_is_convergent 0
(bounded_above_is_convergent-1 nil 3391920142
("" (skosimp)
(("" (expand "convergent_upto?")
(("" (inst + "lub(u!1)")
(("" (rewrite "converges_upto_is_lub")
(("" (assert)
(("" (expand "lub")
((""
(typepred "lub(image[nat, real](u!1, fullset[nat]))")
(("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((convergent_upto? const-decl "bool" convergence_aux nil)
(converges_upto_is_lub formula-decl nil convergence_aux nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(least_upper_bound? const-decl "bool" bounded_real_defs nil)
(bounded_above? const-decl "bool" bounded_real_defs nil)
(lub const-decl "{x | least_upper_bound?(x, SA)}" bounded_real_defs
nil)
(image const-decl "set[R]" function_image nil)
(fullset const-decl "set" sets nil)
(lub const-decl "real" convergence_aux 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(bounded_above? const-decl "bool" real_fun_preds "reals/")
(sequence type-eq-decl nil sequences nil)
(u!1 skolem-const-decl "sequence[real]" convergence_aux nil))
shostak))
(converges_upto_add 0
(converges_upto_add-1 nil 3391920589
("" (skosimp)
(("" (expand "converges_upto?")
(("" (flatten)
(("" (split)
(("1" (hide -2 -4)
(("1" (rewrite "metric_convergence_def" *)
(("1" (rewrite "metric_convergence_def" *)
(("1" (rewrite "metric_convergence_def" *)
(("1" (expand "metric_converges_to")
(("1" (skosimp)
(("1" (inst - "r!1/2")
(("1" (inst - "r!1/2")
(("1" (skosimp*)
(("1" (inst + "max(n!1,n!2)")
(("1"
(skosimp)
(("1"
(inst - "i!1")
(("1"
(inst - "i!1")
(("1"
(assert)
(("1"
(expand "ball")
(("1"
(expand "+")
(("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1 -3)
(("2" (expand "increasing?")
(("2" (skosimp*)
(("2" (inst - "x!2" "y!2")
(("2" (inst - "x!2" "y!2")
(("2" (assert)
(("2" (expand "+") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((converges_upto? const-decl "bool" convergence_aux nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(metric_convergence_def formula-decl nil metric_space 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(sequence type-eq-decl nil sequences nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(+ const-decl "[numfield, numfield -> numfield]" 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)
(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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nonneg_rat_max application-judgement
"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil)
(nat_max application-judgement "{k: nat | i <= k AND j <= k}"
real_defs nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(ball_is_metric_open application-judgement "metric_open"
convergence_aux nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(member const-decl "bool" sets nil)
(real_times_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(ball const-decl "set[T]" metric_space_def nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(metric_converges_to const-decl "bool" metric_space_def nil)
(increasing? const-decl "bool" real_fun_preds "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(converges_upto_scal 0
(converges_upto_scal-1 nil 3391927669
("" (skosimp)
(("" (expand "converges_upto?")
(("" (flatten)
(("" (split)
(("1" (hide -2)
(("1" (rewrite "metric_convergence_def" *)
(("1" (rewrite "metric_convergence_def" *)
(("1" (expand "metric_converges_to")
(("1" (skosimp)
(("1" (typepred "nnc!1")
(("1" (expand ">=" -1)
(("1" (expand "<=" -1)
(("1" (split -1)
(("1" (inst - "r!1/nnc!1")
(("1"
(skosimp)
(("1"
(inst + "n!1")
(("1"
(skosimp)
(("1"
(inst - "i!1")
(("1"
(expand "*")
(("1"
(expand "ball")
(("1"
(expand "member")
(("1"
(assert)
(("1"
(lemma
"abs_mult"
("x"
"nnc!1"
"y"
"x!1 - u!1(i!1)"))
(("1"
(expand "abs" -1 2)
(("1"
(replace -1 1)
(("1"
(rewrite
"div_mult_pos_lt2"
-4)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"posreal_div_posreal_is_posreal"
("px" "r!1" "py" "nnc!1"))
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil)
("3" (assert) nil nil))
nil)
("2" (replace -1 * rl)
(("2"
(hide -1)
(("2"
(expand "*")
(("2"
(expand "ball")
(("2"
(expand "member")
(("2"
(expand "abs")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1)
(("2" (expand "increasing?")
(("2" (expand "*")
(("2" (skosimp)
(("2" (inst - "x!2" "y!1")
(("2" (assert)
(("2" (case-replace "nnc!1=0")
(("1" (assert) nil nil)
("2"
(lemma "both_sides_times_pos_le1"
("pz" "nnc!1" "x" "u!1(x!2)" "y"
"u!1(y!1)"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((converges_upto? const-decl "bool" convergence_aux nil)
(real_times_real_is_real application-judgement "real" reals nil)
(metric_convergence_def formula-decl nil metric_space 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(sequence type-eq-decl nil sequences nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(nnreal type-eq-decl nil real_types nil)
(* const-decl "[numfield, numfield -> numfield]" 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)
(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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(metric_converges_to const-decl "bool" metric_space_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(<= const-decl "bool" reals 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)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(/= const-decl "boolean" notequal nil)
(nnc!1 skolem-const-decl "nnreal" convergence_aux nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(r!1 skolem-const-decl "posreal" convergence_aux nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(ball const-decl "set[T]" metric_space_def nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(div_mult_pos_lt2 formula-decl nil real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(abs_mult formula-decl nil real_props nil)
(member const-decl "bool" sets nil)
(posreal_div_posreal_is_posreal judgement-tcc nil real_types nil)
(increasing? const-decl "bool" real_fun_preds "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(both_sides_times_pos_le1 formula-decl nil real_props nil)
(= const-decl "[T, T -> boolean]" equalities nil))
shostak))
(converges_downto_bounded_below 0
(converges_downto_bounded_below-1 nil 3391952260
("" (skosimp)
(("" (expand "bounded_below?")
(("" (expand "converges_downto?")
(("" (flatten)
(("" (rewrite "metric_convergence_def" *)
(("" (expand "metric_converges_to")
(("" (expand "ball")
(("" (expand "member")
(("" (inst + "x!1")
(("" (skosimp)
(("" (expand "decreasing?")
(("" (inst - "x!1-u!1(x!2)")
(("1" (skosimp)
(("1" (inst - "n!1+x!2")
(("1"
(assert)
(("1"
(inst - "x!2" "n!1+x!2")
(("1" (grind) nil nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((bounded_below? const-decl "bool" real_fun_preds "reals/")
(metric_converges_to const-decl "bool" metric_space_def nil)
(member const-decl "bool" sets 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)
(x!1 skolem-const-decl "real" convergence_aux nil)
(u!1 skolem-const-decl "sequence[real]" convergence_aux nil)
(x!2 skolem-const-decl "nat" convergence_aux nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(decreasing? const-decl "bool" real_fun_preds "reals/")
(ball const-decl "set[T]" metric_space_def nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(sequence type-eq-decl nil sequences nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(metric_convergence_def formula-decl nil metric_space nil)
(converges_downto? const-decl "bool" convergence_aux nil))
shostak))
(converges_downto_ge 0
(converges_downto_ge-1 nil 3391953168
("" (skosimp*)
(("" (expand "converges_downto?")
(("" (flatten)
(("" (rewrite "metric_convergence_def" -1)
(("" (expand "metric_converges_to")
(("" (case "u!1(n!1))
(("1" (hide 1)
(("1" (inst - "x!1-u!1(n!1)")
(("1" (skosimp*)
(("1" (inst - "max(n!1,n!2)")
(("1" (expand "decreasing?")
(("1" (inst - "n!1" "max(n!1,n!2)")
(("1" (grind) nil nil)) nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((converges_downto? const-decl "bool" convergence_aux nil)
(metric_convergence_def formula-decl nil metric_space 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(sequence type-eq-decl nil sequences 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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(< const-decl "bool" reals 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)
(real_minus_real_is_real application-judgement "real" reals nil)
(x!1 skolem-const-decl "real" convergence_aux nil)
(u!1 skolem-const-decl "sequence[real]" convergence_aux nil)
(n!1 skolem-const-decl "nat" convergence_aux nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_rat_max application-judgement
"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil)
(nat_max application-judgement "{k: nat | i <= k AND j <= k}"
real_defs nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ball_is_metric_open application-judgement "metric_open"
convergence_aux nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(ball const-decl "set[T]" metric_space_def nil)
(member const-decl "bool" sets nil)
(decreasing? const-decl "bool" real_fun_preds "reals/")
(metric_converges_to const-decl "bool" metric_space_def nil))
shostak))
(converges_downto_def 0
(converges_downto_def-1 nil 3391957389
("" (skosimp)
(("" (expand "converges_downto?")
(("" (case-replace "decreasing?(u!1)")
(("1" (split)
(("1" (flatten)
(("1" (lemma "converges_downto_ge" ("u" "u!1" "x" "x!1"))
(("1" (split -1)
(("1" (assert)
(("1" (replace -1 1)
(("1" (rewrite "metric_convergence_def" *)
(("1" (expand "metric_converges_to")
(("1" (skosimp)
(("1" (inst -2 "r!1")
(("1" (skosimp)
(("1"
(inst + "n!1")
(("1"
(skosimp)
(("1"
(inst -2 "i!1")
(("1"
(assert)
(("1"
(expand "ball")
(("1"
(inst - "i!1")
(("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "converges_downto?")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (rewrite "metric_convergence_def")
(("2" (expand "metric_converges_to")
(("2" (skosimp)
(("2" (inst -2 "r!1")
(("2" (skosimp)
(("2" (inst + "n!1")
(("2" (skosimp)
(("2" (inst -2 "i!1")
(("2" (assert)
(("2"
(inst - "i!1")
(("2"
(expand "ball")
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
((converges_downto? const-decl "bool" convergence_aux nil)
(converges_downto_ge formula-decl nil convergence_aux nil)
(metric_convergence_def formula-decl nil metric_space nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.99Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
