Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: finite_sets_card_from.prf   Sprache: Lisp

Original von: PVS©

(continuity_interval
 (J_TCC1 0
  (J_TCC1-1 nil 3442580979
   ("" (inst 1 "a") (("" (assertnil nil)) nil)
   ((b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
    (a formal-const-decl "real" continuity_interval nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (bolz_weier 0
  (bolz_weier-1 nil 3442580979
   ("" (skolem!)
    (("" (lemma "bolzano_weierstrass4")
      (("" (inst -1 "a" "b" "u!1")
        (("" (prop)
          (("1" (skosimp) (("1" (inst?) (("1" (assertnil nil)) nil))
            nil)
           ("2" (delete 2) (("2" (grind) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((bolzano_weierstrass4 formula-decl nil convergence_sequences nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (c!1 skolem-const-decl "real" continuity_interval nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (J nonempty-type-eq-decl nil continuity_interval nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (sequence type-eq-decl nil sequences nil)
    (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)
    (b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
    (<= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (a formal-const-decl "real" continuity_interval 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))
   nil))
 (unbounded_sequence 0
  (unbounded_sequence-1 nil 3442580979
   ("" (skosimp)
    (("" (expand "bounded_above?")
      (("" (inst 2 "lambda (n : nat) : epsilon! (x : J) : f!1(x) > n")
        (("" (skosimp)
          (("" (assert)
            (("" (use "epsilon_ax[J]")
              (("" (ground)
                (("" (inst? 2)
                  (("" (delete 3)
                    (("" (skolem!)
                      (("" (inst?) (("" (assertnil nil)) nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((bounded_above? const-decl "bool" real_fun_preds "reals/")
    (epsilon_ax formula-decl nil epsilons nil)
    (real_le_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)
    (epsilon const-decl "T" epsilons nil)
    (pred type-eq-decl nil defined_types nil)
    (sequence type-eq-decl nil sequences nil)
    (J nonempty-type-eq-decl nil continuity_interval nil)
    (b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
    (a formal-const-decl "real" continuity_interval nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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))
   nil))
 (bounded_from_above 0
  (bounded_from_above-1 nil 3442580979
   ("" (skosimp)
    (("" (use "unbounded_sequence")
      (("" (assert)
        (("" (skolem!)
          (("" (use "bolz_weier")
            (("" (skolem!)
              (("" (expand "continuous?")
                (("" (inst? -3)
                  (("" (forward-chain "continuity_accumulation[J]")
                    (("" (delete -2 -4 1)
                      (("" (expand "accumulation")
                        (("" (expand "o")
                          ((""
                            (case "EXISTS (m : nat) : f!1(c!1) + 1 < m")
                            (("1" (skolem!)
                              (("1"
                                (inst -2 "1" "m!1")
                                (("1"
                                  (skosimp)
                                  (("1"
                                    (inst?)
                                    (("1" (grind) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (delete -)
                              (("2"
                                (use "axiom_of_archimedes")
                                (("2"
                                  (skolem!)
                                  (("2"
                                    (inst
                                     1
                                     "IF i!1 < 0 THEN 0 ELSE i!1 ENDIF")
                                    (("1"
                                      (lift-if)
                                      (("1" (assertnil nil))
                                      nil)
                                     ("2" (ground) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((unbounded_sequence formula-decl nil continuity_interval nil)
    (J nonempty-type-eq-decl nil continuity_interval nil)
    (b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
    (a formal-const-decl "real" continuity_interval nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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)
    (O const-decl "T3" function_props nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (i!1 skolem-const-decl "int" continuity_interval nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (axiom_of_archimedes formula-decl nil real_props 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_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)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (< const-decl "bool" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (accumulation const-decl "bool" convergence_sequences nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (continuity_accumulation formula-decl nil continuity_props nil)
    (continuous? const-decl "bool" continuous_functions 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 "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (sequence type-eq-decl nil sequences nil)
    (bolz_weier formula-decl nil continuity_interval nil))
   nil))
 (bounded_from_below 0
  (bounded_from_below-2 nil 3442582177
   ("" (skosimp)
    (("" (lemma "bounded_from_above" ("f" "-f!1"))
      (("" (rewrite "bounded_above_neg[J]")
        (("" (assert) (("" (rewrite "neg_fun_continuous [J]"nil nil))
          nil))
        nil))
      nil))
    nil)
   ((- const-decl "[T -> real]" real_fun_ops "reals/")
    (J nonempty-type-eq-decl nil continuity_interval nil)
    (b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
    (a formal-const-decl "real" continuity_interval nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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)
    (bounded_from_above formula-decl nil continuity_interval nil)
    (continuous_fun nonempty-type-eq-decl nil continuous_functions nil)
    (continuous? const-decl "bool" continuous_functions nil)
    (neg_fun_continuous judgement-tcc nil continuous_functions nil)
    (bounded_above_neg formula-decl nil real_fun_props "reals/"))
   nil)
  (bounded_from_below-1 nil 3442580979
   ("" (skosimp)
    (("" (lemma "bounded_from_above" ("f" "-f!1"))
      (("" (rewrite "bounded_above_opposite[J]")
        (("" (assert) (("" (rewrite "neg_fun_continuous [J]"nil nil))
          nil))
        nil))
      nil))
    nil)
   nil nil))
 (max_extraction_TCC1 0
  (max_extraction_TCC1-1 nil 3442580979
   ("" (lemma "bounded_from_above") (("" (propax) nil nil)) nil)
   ((bounded_from_above formula-decl nil continuity_interval nil))
   nil))
 (max_extraction 0
  (max_extraction-1 nil 3442580979
   ("" (skosimp)
    (("" (forward-chain "bounded_from_above")
      (("" (assert)
        ((""
          (inst 1
           "LAMBDA (n : nat) : epsilon! (x : J) : sup(f!1) - f!1(x) < 1 / (1 + n)")
          (("" (skolem!)
            ((""
              (lemma "epsilon_ax"
               ("p"
                "LAMBDA (x: J): sup(f!1) - f!1(x) < 1 / (1 + n!1)"))
              (("" (assert)
                (("" (delete 2)
                  ((""
                    (lemma "supfun_is_sup[J]"
                     ("g" "f!1" "epsilon" "1/(1+n!1)"))
                    (("" (skolem!)
                      (("" (inst?) (("" (assertnil nil)) nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((bounded_from_above formula-decl nil continuity_interval 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (a formal-const-decl "real" continuity_interval nil)
    (b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
    (J nonempty-type-eq-decl nil continuity_interval nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (real_minus_real_is_real application-judgement "real" 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 "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (sequence type-eq-decl nil sequences nil)
    (pred type-eq-decl nil defined_types nil)
    (epsilon const-decl "T" epsilons nil)
    (< const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (bounded_above? const-decl "bool" real_fun_preds "reals/")
    (sup const-decl "real" real_fun_supinf nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (epsilon_ax formula-decl nil epsilons 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)
    (supfun_is_sup formula-decl nil real_fun_supinf nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil))
   nil))
 (sup_is_reached 0
  (sup_is_reached-1 nil 3442580979
   ("" (skosimp)
    (("" (forward-chain "bounded_from_above")
      (("" (assert)
        (("" (forward-chain "max_extraction")
          (("" (skolem!)
            (("" (use "bolz_weier")
              (("" (skolem!)
                (("" (expand "continuous?")
                  (("" (inst? -4)
                    (("" (forward-chain "continuity_accumulation[J]")
                      (("" (delete -2 -4 -5)
                        (("" (inst? 1)
                          (("" (expand "accumulation")
                            (("" (expand "o")
                              ((""
                                (use "supfun_is_bound[J]")
                                ((""
                                  (name "eps" "sup(f!1) - f!1(c!1)")
                                  ((""
                                    (assert)
                                    ((""
                                      (use
                                       "archimedean2"
                                       ("x" "eps/2"))
                                      ((""
                                        (skolem!)
                                        ((""
                                          (inst -4 "eps/2" "a!1")
                                          ((""
                                            (skosimp)
                                            ((""
                                              (inst -6 "i!1")
                                              ((""
                                                (case
                                                 "1 / (1 + i!1) < 1 / a!1")
                                                (("1"
                                                  (expand "abs")
                                                  (("1"
                                                    (lift-if)
                                                    (("1"
                                                      (ground)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (rewrite
                                                   "both_sides_div_pos_lt2"
                                                   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)
   ((bounded_from_above formula-decl nil continuity_interval 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (a formal-const-decl "real" continuity_interval nil)
    (b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
    (J nonempty-type-eq-decl nil continuity_interval nil)
    (max_extraction formula-decl nil continuity_interval nil)
    (bolz_weier formula-decl nil continuity_interval nil)
    (sequence type-eq-decl nil sequences nil)
    (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)
    (continuous? const-decl "bool" continuous_functions nil)
    (continuity_accumulation formula-decl nil continuity_props nil)
    (O const-decl "T3" function_props 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)
    (sup const-decl "real" real_fun_supinf 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)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal 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)
    (archimedean2 formula-decl nil real_facts "reals/")
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (both_sides_div_pos_lt2 formula-decl nil real_props nil)
    (int_minus_int_is_int application-judgement "int" integers 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)
    (minus_real_is_real application-judgement "real" reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (< const-decl "bool" reals nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (bounded_above? const-decl "bool" real_fun_preds "reals/")
    (supfun_is_bound formula-decl nil real_fun_supinf nil)
    (accumulation const-decl "bool" convergence_sequences nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
 (maximum_exists 0
  (maximum_exists-1 nil 3442580979
   ("" (skosimp)
    (("" (forward-chain "sup_is_reached")
      (("" (skolem!)
        (("" (inst?)
          (("" (rewrite "max_upper_bound[J]")
            (("" (assert) (("" (rewrite "bounded_from_above"nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sup_is_reached formula-decl nil continuity_interval 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (a formal-const-decl "real" continuity_interval nil)
    (b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
    (J nonempty-type-eq-decl nil continuity_interval nil)
    (bounded_from_above formula-decl nil continuity_interval nil)
    (max_upper_bound formula-decl nil real_fun_supinf nil))
   nil))
 (max_pt_TCC1 0
  (max_pt_TCC1-1 nil 3442580979
   (""
    (inst +
     "(LAMBDA (f: {f | continuous?[J](f)}): choose({xj: J | is_maximum[J](xj, f)}))")
    (("" (skosimp*)
      (("" (lemma "maximum_exists")
        (("" (inst?)
          (("" (assert)
            (("" (skosimp*)
              (("" (expand "nonempty?")
                (("" (expand "empty?")
                  (("" (inst?)
                    (("" (expand "member") (("" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (maximum_exists formula-decl nil continuity_interval nil)
    (choose const-decl "(p)" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (is_maximum? const-decl "bool" real_fun_preds "reals/")
    (continuous? const-decl "bool" continuous_functions nil)
    (J nonempty-type-eq-decl nil continuity_interval nil)
    (b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
    (a formal-const-decl "real" continuity_interval nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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))
   nil))
 (inf_is_reached_TCC1 0
  (inf_is_reached_TCC1-1 nil 3442580979
   ("" (lemma "bounded_from_below") (("" (propax) nil nil)) nil)
   ((bounded_from_below formula-decl nil continuity_interval nil))
   nil))
 (inf_is_reached 0
  (inf_is_reached-1 nil 3442580979
   ("" (skosimp)
    (("" (use "sup_is_reached" ("f" "-f!1"))
      (("" (split)
        (("1" (skolem!)
          (("1" (rewrite "supfun_neg[J]")
            (("1" (expand "-")
              (("1" (inst?) (("1" (assertnil nil)) nil)) nil)
             ("2" (rewrite "bounded_from_below"nil nil))
            nil))
          nil)
         ("2" (rewrite "neg_fun_continuous [J]"nil nil))
        nil))
      nil))
    nil)
   ((sup_is_reached formula-decl nil continuity_interval 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (a formal-const-decl "real" continuity_interval nil)
    (b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
    (J nonempty-type-eq-decl nil continuity_interval nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (neg_fun_continuous judgement-tcc nil continuous_functions nil)
    (continuous? const-decl "bool" continuous_functions nil)
    (continuous_fun nonempty-type-eq-decl nil continuous_functions nil)
    (bounded_from_below formula-decl nil continuity_interval nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (bounded_below? const-decl "bool" real_fun_preds "reals/")
    (supfun_neg formula-decl nil real_fun_supinf nil))
   nil))
 (minimum_exists 0
  (minimum_exists-1 nil 3442580979
   ("" (skosimp)
    (("" (use "maximum_exists" ("f" "-f!1"))
      (("" (split)
        (("1" (skolem!)
          (("1" (rewrite "max_neg[J]") (("1" (inst?) nil nil)) nil))
          nil)
         ("2" (rewrite "neg_fun_continuous [J]"nil nil))
        nil))
      nil))
    nil)
   ((maximum_exists formula-decl nil continuity_interval 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (a formal-const-decl "real" continuity_interval nil)
    (b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
    (J nonempty-type-eq-decl nil continuity_interval nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (neg_fun_continuous judgement-tcc nil continuous_functions nil)
    (continuous? const-decl "bool" continuous_functions nil)
    (continuous_fun nonempty-type-eq-decl nil continuous_functions nil)
    (max_neg formula-decl nil real_fun_props "reals/"))
   nil))
 (min_pt_TCC1 0
  (min_pt_TCC1-2 nil 3445335662
   (""
    (inst +
     "(LAMBDA (f: {f | continuous?[J](f)}): choose({xj: J | is_minimum[J](xj, f)}))")
    (("" (skosimp*)
      (("" (lemma "minimum_exists")
        (("" (inst?)
          (("" (assert)
            (("" (skosimp*)
              (("" (expand "nonempty?")
                (("" (expand "empty?")
                  (("" (inst?)
                    (("" (expand "member") (("" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (minimum_exists formula-decl nil continuity_interval nil)
    (choose const-decl "(p)" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (is_minimum? const-decl "bool" real_fun_preds "reals/")
    (continuous? const-decl "bool" continuous_functions nil)
    (J nonempty-type-eq-decl nil continuity_interval nil)
    (b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
    (a formal-const-decl "real" continuity_interval nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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))
   nil)
  (min_pt_TCC1-1 nil 3442580979
   (""
    (inst +
     "(LAMBDA (f: {f | continuous[J](f)}): choose({xj: J | is_minimum[J](xj, f)}))")
    (("" (skosimp*)
      (("" (lemma "minimum_exists")
        (("" (inst?)
          (("" (assert)
            (("" (skosimp*)
              (("" (expand "nonempty?")
                (("" (expand "empty?")
                  (("" (inst?)
                    (("" (expand "member") (("" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((is_minimum? const-decl "bool" real_fun_preds "reals/")) nil))
 (intermediate_value1_TCC1 0
  (intermediate_value1_TCC1-1 nil 3442580979
   ("" (skosimp) (("" (assert) (("" (assertnil nil)) nil)) nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (intermediate_value1_TCC2 0
  (intermediate_value1_TCC2-1 nil 3442580979
   ("" (skosimp) (("" (assertnil nil)) 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))
   nil))
 (intermediate_value1 0
  (intermediate_value1-1 nil 3442580979
   ("" (skosimp)
    (("" (name "E" "{y:real| a <= y AND y <= b AND f!1(y) < x!1}")
      (("1" (case "nonempty?(E) AND bounded_above?(E)")
        (("1" (assert)
          (("1" (ground)
            (("1" (case "a <= lub(E) AND lub(E) <= b")
              (("1" (assert)
                (("1" (ground)
                  (("1" (hide -1 -2 -3 -4)
                    (("1" (expand "continuous?")
                      (("1" (inst - "lub(E)")
                        (("1" (inst + "lub(E)")
                          (("1"
                            (auto-rewrite "abs" "subset_fullset[real]")
                            (("1" (case "x!1 < f!1(lub(E))")
                              (("1"
                                (assert)
                                (("1"
                                  (expand "continuous?")
                                  (("1"
                                    (inst - "f!1(lub(E)) - x!1")
                                    (("1"
                                      (skolem!)
                                      (("1"
                                        (use
                                         "adherence_sup"
                                         ("epsilon" "delta!1"))
                                        (("1"
                                          (skolem-typepred)
                                          (("1"
                                            (replace -4 -1 rl)
                                            (("1"
                                              (assert)
                                              (("1"
                                                (use
                                                 "lub_is_bound"
                                                 ("U" "E" "x" "x!2"))
                                                (("1"
                                                  (ground)
                                                  (("1"
                                                    (inst - "x!2")
                                                    (("1"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (name
                                 "F"
                                 "{y:real | lub(E) < y AND y <= b}")
                                (("2"
                                  (rewrite "continuity_def[J]")
                                  (("2"
                                    (lemma
                                     "subset_convergence2[J]"
                                     ("E1" "F"))
                                    (("2"
                                      (inst
                                       -
                                       "fullset[real]"
                                       "f!1"
                                       "lub(E)"
                                       "f!1(lub(E))")
                                      (("1"
                                        (ground)
                                        (("1"
                                          (delete -4)
                                          (("1"
                                            (lemma
                                             "convergence_lower_bound[J]"
                                             ("b" "x!1"))
                                            (("1"
                                              (inst
                                               -
                                               "F"
                                               "f!1"
                                               "lub(E)"
                                               "f!1(lub(E))")
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (skosimp)
                                                  (("1"
                                                    (replace -3 -1 rl)
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (use
                                                         "lub_is_bound"
                                                         ("U"
                                                          "E"
                                                          "x"
                                                          "x!2"))
                                                        (("1"
                                                          (assert)
                                                          nil
                                                          nil)
                                                         ("2"
                                                          (replace
                                                           -4
                                                           +
                                                           rl)
                                                          (("2"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (hide -1 -2 -4 -5 2 3)
                                          (("2"
                                            (expand "convergence")
                                            (("2"
                                              (expand "convergence")
                                              (("2" (propax) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (replace -1 + rl)
                                        (("2"
                                          (expand "adh")
                                          (("2"
                                            (skosimp)
                                            (("2"
                                              (case "b < lub(E) + e!1")
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (inst + "b")
                                                  (("1"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (assert)
                                                (("2"
                                                  (inst
                                                   +
                                                   "lub(E) + e!1/2")
                                                  (("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (delete -1 -2 -4 -5 -6 2)
                (("2" (ground)
                  (("1" (rewrite "lub_is_bound")
                    (("1" (replace -1 + rl) (("1" (assertnil nil))
                      nil))
                    nil)
                   ("2" (rewrite "lub_is_lub")
                    (("2" (skolem-typepred)
                      (("2" (replace -2 - rl)
                        (("2" (assert) (("2" (assertnil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (replace -1 + rl)
          (("2" (delete -1 -2 2)
            (("2" (grind :if-match nil)
              (("1" (inst + "b")
                (("1" (skolem!) (("1" (assertnil nil)) nil)) nil)
               ("2" (inst - "a") (("2" (assertnil nil)) nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (skosimp) (("2" (assertnil nil)) nil))
      nil))
    nil)
   ((J nonempty-type-eq-decl nil continuity_interval nil)
    (< const-decl "bool" reals nil)
    (b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
    (a formal-const-decl "real" continuity_interval nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (upper_bound? const-decl "bool" bounded_real_defs nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (least_upper_bound? const-decl "bool" bounded_real_defs nil)
    (lub const-decl "{x | least_upper_bound?(x, SA)}" bounded_real_defs
     nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (continuous? const-decl "bool" continuous_functions nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (continuous? const-decl "bool" continuous_functions nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (lub_is_bound formula-decl nil real_facts "reals/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (adherence_sup formula-decl nil real_facts "reals/")
    (>= 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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields 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)
    (continuity_def formula-decl nil continuous_functions nil)
    (adh const-decl "setof[real]" convergence_functions nil)
    (F skolem-const-decl "[real -> boolean]" continuity_interval nil)
    (E skolem-const-decl "[real -> boolean]" continuity_interval nil)
    (fullset const-decl "set" sets nil)
    (convergence const-decl "bool" convergence_functions nil)
    (convergence const-decl "bool" lim_of_functions nil)
    (convergence_lower_bound formula-decl nil convergence_functions
     nil)
    (subset_fullset formula-decl nil sets_lemmas nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (setof type-eq-decl nil defined_types nil)
    (subset_convergence2 formula-decl nil convergence_functions nil)
    (lub_is_lub formula-decl nil real_facts "reals/")
    (bounded_above? const-decl "bool" bounded_real_defs nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil))
   nil))
 (intermediate_value2_TCC1 0
  (intermediate_value2_TCC1-1 nil 3442580979
   ("" (skosimp) (("" (assertnil nil)) nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (intermediate_value2 0
  (intermediate_value2-1 nil 3442580979
   ("" (skosimp)
    (("" (use "intermediate_value1")
      (("" (assert)
        (("" (split)
          (("1" (propax) nil nil)
           ("2" (inst 2 "a") (("2" (assertnil nil)) nil)
           ("3" (inst 2 "b") (("3" (assertnil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((intermediate_value1 formula-decl nil continuity_interval nil)
    (J nonempty-type-eq-decl nil continuity_interval nil)
    (b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
    (a formal-const-decl "real" continuity_interval nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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)
    (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))
   nil))
 (intermediate_value3_TCC1 0
  (intermediate_value3_TCC1-1 nil 3442580979
   ("" (skosimp) (("" (assertnil nil)) nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (intermediate_value3 0
  (intermediate_value3-1 nil 3442580979
   ("" (skosimp)
    (("" (lemma "intermediate_value1" ("f" "-f!1" "x" "-x!1"))
      (("" (auto-rewrite "neg_fun_continuous [J]" "-")
        (("" (assert)
          (("" (skolem!) (("" (inst?) (("" (assertnil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (J nonempty-type-eq-decl nil continuity_interval nil)
    (b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
    (a formal-const-decl "real" continuity_interval nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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)
    (intermediate_value1 formula-decl nil continuity_interval 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)
    (neg_fun_continuous judgement-tcc nil continuous_functions nil))
   nil))
 (intermediate_value4 0
  (intermediate_value4-1 nil 3442580979
   ("" (skosimp)
    (("" (use "intermediate_value3")
      (("" (assert)
        (("" (split)
          (("1" (propax) nil nil)
           ("2" (inst 2 "b") (("2" (assertnil nil)) nil)
           ("3" (inst 2 "a") (("3" (assertnil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((intermediate_value3 formula-decl nil continuity_interval nil)
    (J nonempty-type-eq-decl nil continuity_interval nil)
    (b formal-const-decl "{x: real | a <= x}" continuity_interval nil)
    (a formal-const-decl "real" continuity_interval nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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)
    (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))
   nil)))


¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.63Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤





Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik