products/sources/formale Sprachen/PVS/Bernstein/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: Rings.thy   Sprache: Lisp

Untersuchung PVS©
(util
 (le_realorder 0
  (le_realorder-1 nil 3499875743 ("" (judgement-tcc) nil nil)
   ((realorder? const-decl "bool" util nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (lt_realorder 0
  (lt_realorder-1 nil 3499875743 ("" (judgement-tcc) nil nil)
   ((realorder? const-decl "bool" util nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (ge_realorder 0
  (ge_realorder-1 nil 3499875743 ("" (judgement-tcc) nil nil)
   ((realorder? const-decl "bool" util nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (gt_realorder 0
  (gt_realorder-1 nil 3499875743 ("" (judgement-tcc) nil nil)
   ((realorder? const-decl "bool" util nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (relreal_scal 0
  (relreal_scal-1 nil 3503403768
   (""
    (case "FORALL (relreal: RealOrder, x, y: real, pr: posreal):
        relreal(x, y) IMPLIES relreal(pr * x, pr * y)")
    (("1" (skeep)
      (("1" (ground)
        (("1" (inst?) (("1" (assert) nil nil)) nil)
         ("2" (inst - "relreal" "pr*x" "pr*y" "1/pr")
          (("2" (assert) nil nil)) nil))
        nil))
      nil)
     ("2" (hide 2)
      (("2" (skeep)
        (("2" (typepred "relreal")
          (("2" (expand "realorder?")
            (("2" (split -)
              (("1" (replace -1)
                (("1" (assert)
                  (("1" (mult-by -2 "pr") (("1" (assert) nil nil))
                    nil))
                  nil))
                nil)
               ("2" (replace -1)
                (("2" (assert)
                  (("2" (mult-by -2 "pr") (("2" (assert) nil nil))
                    nil))
                  nil))
                nil)
               ("3" (replace -1)
                (("3" (assert)
                  (("3" (mult-by -2 "pr") (("3" (assert) nil nil))
                    nil))
                  nil))
                nil)
               ("4" (replace -1)
                (("4" (assert)
                  (("4" (mult-by -2 "pr") (("4" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((NOT const-decl "[bool -> bool]" booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" util nil)
    (both_sides_times_pos_le1_imp formula-decl nil extra_real_props
     nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" util nil)
    (both_sides_times_pos_lt1 formula-decl nil real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" util nil)
    (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
     nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" util nil)
    (both_sides_times_pos_gt1 formula-decl nil real_props nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     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)
    (real_times_real_is_real application-judgement "real" reals 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)
    (realorder? const-decl "bool" util nil)
    (RealOrder type-eq-decl nil util nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields
       nil))
   shostak))
 (edge_point?_TCC1 0
  (edge_point?_TCC1-1 nil 3509968302 ("" (subtype-tcc) nil nil) nil
   nil))
 (normalize_lambda_TCC1 0
  (normalize_lambda_TCC1-1 nil 3500326686 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (Vars type-eq-decl nil util nil)
    (lt_below? const-decl "bool" util nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (gt_realorder name-judgement "RealOrder" util nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (ge_realorder name-judgement "RealOrder" util nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (lt_realorder name-judgement "RealOrder" util nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (/= const-decl "boolean" notequal nil))
   nil))
 (normalize_lambda_TCC2 0
  (normalize_lambda_TCC2-1 nil 3503397081 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (Vars type-eq-decl nil util nil)
    (lt_below? const-decl "bool" util nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (gt_realorder name-judgement "RealOrder" util nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (ge_realorder name-judgement "RealOrder" util nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (lt_realorder name-judgement "RealOrder" util nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (/= const-decl "boolean" notequal nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
 (normalize_lambda_TCC3 0
  (normalize_lambda_TCC3-1 nil 3503397081 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (Vars type-eq-decl nil util nil)
    (lt_below? const-decl "bool" util nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (gt_realorder name-judgement "RealOrder" util nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (ge_realorder name-judgement "RealOrder" util nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (lt_realorder name-judgement "RealOrder" util nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (/= const-decl "boolean" notequal nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
 (normalize_lambda_unitbox 0
  (normalize_lambda_unitbox-2 nil 3509875526
   ("" (skeep)
    (("" (hide -2)
      (("" (expand "normalize_lambda")
        (("" (expand "unitbox?")
          (("" (expand "boxbetween?")
            (("" (expand "interval_between?")
              (("" (skeep)
                (("" (inst - "j")
                  (("" (flatten)
                    (("" (case "boundedpts(j)`1 AND boundedpts(j)`2")
                      (("1" (flatten)
                        (("1" (assert)
                          (("1"
                            (case "Avars(j)<=X(j) AND X(j)<=Bvars(j)")
                            (("1" (flatten)
                              (("1"
                                (assert)
                                (("1"
                                  (split +)
                                  (("1" (cross-mult 1) nil nil)
                                   ("2" (cross-mult 1) nil nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (hide 2) (("2" (ground) nil nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (case "boundedpts(j)`1")
                        (("1" (assert)
                          (("1" (case "Avars(j)<=X(j)")
                            (("1" (assert)
                              (("1"
                                (split +)
                                (("1" (cross-mult 1) nil nil)
                                 ("2" (cross-mult 1) nil nil))
                                nil))
                              nil)
                             ("2" (assert) nil nil))
                            nil))
                          nil)
                         ("2" (assert)
                          (("2" (case "X(j)<=Bvars(j)")
                            (("1" (assert)
                              (("1"
                                (hide 2)
                                (("1"
                                  (split +)
                                  (("1" (cross-mult 1) nil nil)
                                   ("2" (cross-mult 1) nil nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (assert) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((unitbox? const-decl "bool" util nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" util nil)
    (lt_realorder name-judgement "RealOrder" util nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (interval_between? const-decl "bool" util 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)
    (< const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (below type-eq-decl nil naturalnumbers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IntervalEndpoints type-eq-decl nil util nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" util nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" util nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (div_mult_pos_le2 formula-decl nil real_props nil)
    (div_mult_pos_le1 formula-decl nil real_props nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (Vars type-eq-decl nil util nil) (<= const-decl "bool" reals nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (boxbetween? const-decl "bool" util nil)
    (normalize_lambda const-decl "Vars" util nil))
   nil)
  (normalize_lambda_unitbox-1 nil 3509354299
   ("" (skeep)
    (("" (hide -2)
      (("" (expand "normalize_lambda")
        (("" (expand "unitbox?")
          (("" (expand "boxbetween?")
            (("" (skeep)
              (("" (inst - "j")
                (("" (flatten)
                  (("" (case "boundedpts(j)`1 AND boundedpts(j)`2")
                    (("1" (flatten)
                      (("1" (assert)
                        (("1"
                          (case "Avars(j)<=X(j) AND X(j)<=Bvars(j)")
                          (("1" (flatten)
                            (("1" (assert)
                              (("1"
                                (split +)
                                (("1" (cross-mult 1) nil nil)
                                 ("2" (cross-mult 1) nil nil))
                                nil))
                              nil))
                            nil)
                           ("2" (hide 2) (("2" (ground) nil nil)) nil))
                          nil))
                        nil))
                      nil)
                     ("2" (case "boundedpts(j)`1")
                      (("1" (assert)
                        (("1" (case "Avars(j)<=X(j)")
                          (("1" (assert)
                            (("1" (split +)
                              (("1" (cross-mult 1) nil nil)
                               ("2" (cross-mult 1) nil nil))
                              nil))
                            nil)
                           ("2" (assert) nil nil))
                          nil))
                        nil)
                       ("2" (assert)
                        (("2" (case "X(j)<=Bvars(j)")
                          (("1" (assert)
                            (("1" (hide 2)
                              (("1"
                                (split +)
                                (("1" (cross-mult 1) nil nil)
                                 ("2" (cross-mult 1) nil nil))
                                nil))
                              nil))
                            nil)
                           ("2" (assert) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil shostak))
 (denormalize_listreal_rec_TCC1 0
  (denormalize_listreal_rec_TCC1-1 nil 3509627050
   ("" (subtype-tcc) nil nil) nil nil))
 (denormalize_listreal_rec_TCC2 0
  (denormalize_listreal_rec_TCC2-1 nil 3509627050
   ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (PRED type-eq-decl nil defined_types nil)
    (list type-decl nil list_adt nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" 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)
    (>= const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (length def-decl "nat" list_props nil)
    (upfrom nonempty-type-eq-decl nil integers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (listn type-eq-decl nil listn "structures/")
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (ge_realorder name-judgement "RealOrder" util nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (lt_realorder name-judgement "RealOrder" util nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_plus_int_is_int application-judgement "int" integers nil))
   nil))
 (denormalize_listreal_rec_TCC3 0
  (denormalize_listreal_rec_TCC3-1 nil 3509627050 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (PRED type-eq-decl nil defined_types nil)
    (list type-decl nil list_adt nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" 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)
    (>= const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (upfrom nonempty-type-eq-decl nil integers nil)
    (lt_realorder name-judgement "RealOrder" util nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (ge_realorder name-judgement "RealOrder" util nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (/= const-decl "boolean" notequal nil)
    (length def-decl "nat" list_props nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil))
   nil))
 (denormalize_listreal_rec_TCC4 0
  (denormalize_listreal_rec_TCC4-1 nil 3509627050
   ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (PRED type-eq-decl nil defined_types nil)
    (list type-decl nil list_adt nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" 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)
    (>= const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (length def-decl "nat" list_props nil)
    (upfrom nonempty-type-eq-decl nil integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" util nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" util nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil))
   nil))
 (denormalize_listreal_rec_TCC5 0
  (denormalize_listreal_rec_TCC5-1 nil 3509627050
   ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (PRED type-eq-decl nil defined_types nil)
    (list type-decl nil list_adt nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" 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))
   nil))
 (denormalize_listreal_rec_TCC6 0
  (denormalize_listreal_rec_TCC6-1 nil 3509627050 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (PRED type-eq-decl nil defined_types nil)
    (list type-decl nil list_adt nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" 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)
    (>= const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (length def-decl "nat" list_props nil)
    (upfrom nonempty-type-eq-decl nil integers nil)
    (ge_realorder name-judgement "RealOrder" util nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil))
   nil))
 (denormalize_listreal_rec_TCC7 0
  (denormalize_listreal_rec_TCC7-1 nil 3509627050
   ("" (termination-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (PRED type-eq-decl nil defined_types nil)
    (list type-decl nil list_adt nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" 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)
    (<< adt-def-decl "(strict_well_founded?[list])" list_adt nil))
   nil))
 (denormalize_listreal_rec_TCC8 0
  (denormalize_listreal_rec_TCC8-2 nil 3509627195
   ("" (skosimp* :preds? t)
    ((""
      (name-replace "V47__"
       "v!1(cdr[real](l!1), nnvars!1, Avars!1, Bvars!1,boundedpts!1)"
       :hide? t)
      (("1" (typepred "V47__")
        (("1" (assert)
          (("1" (hide (-1 -4))
            (("1" (expand "length" 1 1)
              (("1" (replace -6)
                (("1" (assert)
                  (("1" (expand "length" 1 2)
                    (("1" (skosimp* :preds? t)
                      (("1" (case-replace "i!1=0")
                        (("1" (expand "nth" 1)
                          (("1" (lift-if) (("1" (ground) nil nil))
                            nil))
                          nil)
                         ("2" (expand "nth" 2)
                          (("2" (assert)
                            (("2" (expand "length" 2)
                              (("2"
                                (inst -3 "i!1-1")
                                (("1" (assert) nil nil)
                                 ("2"
                                  (hide 3)
                                  (("2"
                                    (replaces -6)
                                    (("2"
                                      (assert)
                                      (("2"
                                        (expand "length" -1)
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (assert)
        (("2" (hide (-1 -3 2)) (("2" (grind) nil nil)) nil)) nil)
       ("3" (assert)
        (("3" (hide (-1 -4 2)) (("3" (grind) nil nil)) nil)) nil)
       ("4" (assert) nil nil))
      nil))
    nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" util nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vars type-eq-decl nil util nil)
    (IntervalEndpoints type-eq-decl nil util nil)
    (pred type-eq-decl nil defined_types nil)
    (strict_well_founded? const-decl "bool" orders nil)
    (<< adt-def-decl "(strict_well_founded?[list])" list_adt nil)
    (listn type-eq-decl nil listn "structures/")
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (nth def-decl "T" list_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" util nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (i!1 skolem-const-decl "below(length(l!1))" util nil)
    (l!1 skolem-const-decl "list[real]" util nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (PRED type-eq-decl nil defined_types nil)
    (list type-decl nil list_adt nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" 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)
    (>= const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (length def-decl "nat" list_props nil)
    (upfrom nonempty-type-eq-decl nil integers nil))
   nil)
  (denormalize_listreal_rec_TCC8-1 nil 3509627050
   ("" (subtype-tcc) nil nil) nil nil))
 (denormalize_listreal_TCC1 0
  (denormalize_listreal_TCC1-1 nil 3509627050
   ("" (subtype-tcc) nil nil) nil nil))
 (translist_polylist_id 0
  (translist_polylist_id-1 nil 3509627120
   ("" (skosimp* :preds? t)
    (("" (expand "translist")
      (("" (expand "polylist")
        (("" (rewrite "array2list_inv")
          (("" (rewrite "array2list_inv")
            (("" (rewrite "array2list_inv") nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((translist const-decl "real" util nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (array2list_inv formula-decl nil array2list "structures/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (length def-decl "nat" list_props nil)
    (listn type-eq-decl nil listn "structures/")
    (below type-eq-decl nil nat_types nil)
    (nth def-decl "T" list_props nil)
    (array2list const-decl
     "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}"
     array2list "structures/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (Polynomial type-eq-decl nil util nil)
    (Polyproduct type-eq-decl nil util nil)
    (MultiPolynomial type-eq-decl nil util nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (list type-decl nil list_adt nil)
    (PRED type-eq-decl nil defined_types nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" util nil)
    (polylist const-decl "PolyList" util nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil naturalnumbers nil)
    (<= const-decl "bool" reals nil)
    (DegreeMono type-eq-decl nil util nil)
    (upto nonempty-type-eq-decl nil naturalnumbers nil))
   nil))
 (corner_to_point_TCC1 0
  (corner_to_point_TCC1-1 nil 3499445915
   ("" (skeep)
    (("" (expand "unitbox?")
      (("" (skeep :preds? t)
        (("" (lemma "array2list_inv[real]")
          (("" (inst?)
            (("" (replaces -1)
              (("" (lift-if) (("" (assert) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((unitbox? const-decl "bool" util 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)
    (array2list_inv formula-decl nil array2list "structures/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" util nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (CoeffMono type-eq-decl nil util nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IF const-decl "[boolean, T, T -> T]" if_def 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))
   nil)))


¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.47Angebot  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