products/sources/formale Sprachen/C/Lyx/images image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: util.prf   Sprache: Unknown

(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" (assertnil nil)) nil)
         ("2" (inst - "relreal" "pr*x" "pr*y" "1/pr")
          (("2" (assertnil 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" (assertnil nil))
                    nil))
                  nil))
                nil)
               ("2" (replace -1)
                (("2" (assert)
                  (("2" (mult-by -2 "pr") (("2" (assertnil nil))
                    nil))
                  nil))
                nil)
               ("3" (replace -1)
                (("3" (assert)
                  (("3" (mult-by -2 "pr") (("3" (assertnil nil))
                    nil))
                  nil))
                nil)
               ("4" (replace -1)
                (("4" (assert)
                  (("4" (mult-by -2 "pr") (("4" (assertnil 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 nilnil
   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" (assertnil 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" (assertnil 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" (assertnil 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" (assertnil 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 nilnil 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" (assertnil nil)
                                 ("2"
                                  (hide 3)
                                  (("2"
                                    (replaces -6)
                                    (("2"
                                      (assert)
                                      (("2"
                                        (expand "length" -1)
                                        (("2" (assertnil 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" (assertnil 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 nilnil nil))
 (denormalize_listreal_TCC1 0
  (denormalize_listreal_TCC1-1 nil 3509627050
   ("" (subtype-tcc) nil nilnil 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) (("" (assertnil 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)))


[ Dauer der Verarbeitung: 0.18 Sekunden  (vorverarbeitet)  ]