Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: continuous_lambda.prf Sprache: PVS

Original von: PVS^©

(multi_polynomial
(IMP_sigma_bijection_TCC1 0
  (IMP_sigma_bijection_TCC1-1 nil 3510937745
   ("" (assuming-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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (integer nonempty-type-from-decl nil integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
(polyproduct_eval_TCC1 0
  (polyproduct_eval_TCC1-1 nil 3498403670 ("" (subtype-tcc) nil nil)
   nil nil))
(multipoly_translate_denormalize_TCC1 0
  (multipoly_translate_denormalize_TCC1-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)
    (ge_realorder name-judgement "RealOrder" util nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (gt_realorder name-judgement "RealOrder" util nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (/= const-decl "boolean" notequal nil)
    (bounded_points_exclusive? const-decl "bool" util nil)
    (lt_below? const-decl "bool" util nil))
   nil))
(multipoly_translate_denormalize 0
  (multipoly_translate_denormalize-1 nil 3500329151
   ("" (skeep)
    (("" (label "boundedpointsexclusive" -2)
      (("" (hide "boundedpointsexclusive")
        (("" (skoletin 1)
          (("1" (label "pconstname" -1)
            (("1" (hide "pconstname")
              (("1" (label "altb" -1)
                (("1" (hide "altb")
                  (("1" (assert)
                    (("1" (expand "multipoly_eval")
                      (("1" (rewrite "sigma_scal" :dir rl)
                        (("1" (rewrite "sigma_restrict_eq")
                          (("1" (hide 2)
                            (("1" (decompose-equality)
                              (("1"
                                (expand "restrict")
                                (("1"
                                  (lift-if)
                                  (("1"
                                    (ground)
                                    (("1"
                                      (name "ii" "x!1")
                                      (("1"
                                        (replace -1)
                                        (("1"
                                          (case
                                           "polyproduct_eval(multipoly_translate(mpoly,
                                                                                    polydegmono,
                                                                                    nvars,
                                                                                    boundedpts)
                                                                                   (Avars, Bvars)
                                                                                   (ii),
                                                                polydegmono, nvars)
                                                               (X)
                                               =
                                               pconst *
                                                  polyproduct_eval(mpoly(ii), polydegmono, nvars)
                                                                  (denormalize_lambda(nvars,
                                                                                      X,
                                                                                      boundedpts)
                                                                                     (Avars, Bvars))")
                                          (("1" (assert) nil nil)
                                           ("2"
                                            (hide 3)
                                            (("2"
                                              (expand
                                               "polyproduct_eval")
                                              (("2"
                                                (expand "pconst")
                                                (("2"
                                                  (rewrite
                                                   "product_prod")
                                                  (("1"
                                                    (rewrite
                                                     "product_restrict_eq")
                                                    (("1"
                                                      (hide 2)
                                                      (("1"
                                                        (decompose-equality)
                                                        (("1"
                                                          (name
                                                           "pj"
                                                           "x!2")
                                                          (("1"
                                                            (replace
                                                             -1)
                                                            (("1"
                                                              (expand
                                                               "restrict")
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (lift-if)
                                                                  (("1"
                                                                    (split
                                                                     +)
                                                                    (("1"
                                                                      (propax)
                                                                      nil
                                                                      nil)
                                                                     ("2"
                                                                      (flatten)
                                                                      (("2"
                                                                        (assert)
                                                                        (("2"
                                                                          (lift-if)
                                                                          (("2"
                                                                            (split
                                                                             +)
                                                                            (("1"
                                                                              (flatten)
                                                                              (("1"
                                                                                (case
                                                                                 "boundedpts(pj)`1 AND NOT boundedpts(pj)`2")
                                                                                (("1"
                                                                                  (flatten)
                                                                                  (("1"
                                                                                    (hide
                                                                                     2)
                                                                                    (("1"
                                                                                      (expand
                                                                                       "denormalize_lambda")
                                                                                      (("1"
                                                                                        (assert)
                                                                                        (("1"
                                                                                          (inst
                                                                                           -
                                                                                           "pj")
                                                                                          (("1"
                                                                                            (assert)
                                                                                            (("1"
                                                                                              (assert)
                                                                                              (("1"
                                                                                                (expand
                                                                                                 "multipoly_translate")
                                                                                                (("1"
                                                                                                  (expand
                                                                                                   "polyprod_translate")
                                                                                                  (("1"
                                                                                                    (lemma
                                                                                                     "poly_translate_inf_pos_def")
                                                                                                    (("1"
                                                                                                      (inst?)
                                                                                                      (("1"
                                                                                                        (assert)
                                                                                                        nil
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("2"
                                                                                  (case
                                                                                   "boundedpts(pj)`2 AND NOT boundedpts(pj)`1")
                                                                                  (("1"
                                                                                    (hide
                                                                                     1)
                                                                                    (("1"
                                                                                      (hide
                                                                                       1)
                                                                                      (("1"
                                                                                        (flatten)
                                                                                        (("1"
                                                                                          (inst
                                                                                           -
                                                                                           "pj")
                                                                                          (("1"
                                                                                            (assert)
                                                                                            (("1"
                                                                                              (expand
                                                                                               "denormalize_lambda")
                                                                                              (("1"
                                                                                                (expand
                                                                                                 "multipoly_translate")
                                                                                                (("1"
                                                                                                  (expand
                                                                                                   "polyprod_translate")
                                                                                                  (("1"
                                                                                                    (lemma
                                                                                                     "poly_translate_inf_neg_def")
                                                                                                    (("1"
                                                                                                      (inst?)
                                                                                                      (("1"
                                                                                                        (assert)
                                                                                                        nil
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil)
                                                                                   ("2"
                                                                                    (reveal
                                                                                     "boundedpointsexclusive")
                                                                                    (("2"
                                                                                      (expand
                                                                                       "bounded_points_exclusive?")
                                                                                      (("2"
                                                                                        (inst
                                                                                         -
                                                                                         "pj")
                                                                                        (("2"
                                                                                          (ground)
                                                                                          nil
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil)
                                                                             ("2"
                                                                              (flatten)
                                                                              (("2"
                                                                                (assert)
                                                                                (("2"
                                                                                  (expand
                                                                                   "denormalize_lambda")
                                                                                  (("2"
                                                                                    (expand
                                                                                     "multipoly_translate")
                                                                                    (("2"
                                                                                      (expand
                                                                                       "polyprod_translate")
                                                                                      (("2"
                                                                                        (lemma
                                                                                         "poly_translate_id")
                                                                                        (("2"
                                                                                          (inst?)
                                                                                          (("1"
                                                                                            (inst
                                                                                             -
                                                                                             "Avars(pj) + Bvars(pj) * X(pj) - Avars(pj) * X(pj)")
                                                                                            (("1"
                                                                                              (assert)
                                                                                              (("1"
                                                                                                (case
                                                                                                 "((Bvars(pj) * X(pj) - Avars(pj) * X(pj)) /
                                          (Bvars(pj) - Avars(pj))) = X(pj)")
                                                                                                (("1"
                                                                                                  (assert)
                                                                                                  nil
                                                                                                  nil)
                                                                                                 ("2"
                                                                                                  (cross-mult
                                                                                                   1)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil)
                                                                                           ("2"
                                                                                            (reveal
                                                                                             "altb")
                                                                                            (("2"
                                                                                              (expand
                                                                                               "lt_below?")
                                                                                              (("2"
                                                                                                (inst
                                                                                                 -
                                                                                                 "pj")
                                                                                                (("2"
                                                                                                  (assert)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (skosimp*)
                                                          (("2"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (hide 2)
                                                      (("2"
                                                        (skosimp*)
                                                        (("2"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (hide 2)
                                                    (("2"
                                                      (skosimp*)
                                                      (("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)
           ("2" (hide 2)
            (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((<= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (>= const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (DegreeMono type-eq-decl nil util nil)
    (Vars type-eq-decl nil util nil)
    (/= const-decl "boolean" notequal nil)
    (IntervalEndpoints type-eq-decl nil util nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (ge_realorder name-judgement "RealOrder" util nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" util nil)
    (real_le_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 "[T, T -> boolean]" equalities nil)
    (T_low type-eq-decl nil product "reals/")
    (T_high type-eq-decl nil product "reals/")
    (product def-decl "real" product "reals/")
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (^ const-decl "real" exponentiation nil)
    (Polynomial type-eq-decl nil util nil)
    (Polyproduct type-eq-decl nil util nil)
    (MultiPolynomial type-eq-decl nil util nil)
    (Coeff type-eq-decl nil util nil)
    (multipoly_eval const-decl "real" multi_polynomial nil)
    (multipoly_translate const-decl "Polyproduct" multi_polynomial nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (denormalize_lambda const-decl "Vars" util nil)
    (sigma_restrict_eq formula-decl nil sigma "reals/")
    (restrict const-decl "[T -> real]" sigma "reals/")
    (polynomial const-decl "[real -> real]" polynomials "reals/")
    (sequence type-eq-decl nil sequences nil)
    (product_prod formula-decl nil product "reals/")
    (Avars skolem-const-decl "Vars" multi_polynomial nil)
    (pj skolem-const-decl "nat" multi_polynomial nil)
    (Bvars skolem-const-decl "Vars" multi_polynomial nil)
    (div_cancel3 formula-decl nil real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (lt_below? const-decl "bool" util nil)
    (poly_translate_id formula-decl nil polynomials "reals/")
    (poly_translate_inf_neg_def formula-decl nil polynomials "reals/")
    (bounded_points_exclusive? const-decl "bool" util nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (polyprod_translate const-decl "Polynomial" multi_polynomial nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (poly_translate_inf_pos_def formula-decl nil polynomials "reals/")
    (restrict const-decl "[T -> real]" product "reals/")
    (polydegmono skolem-const-decl "DegreeMono" multi_polynomial nil)
    (X skolem-const-decl "Vars" multi_polynomial nil)
    (boundedpts skolem-const-decl "IntervalEndpoints" multi_polynomial
     nil)
    (product_restrict_eq formula-decl nil product "reals/")
    (pconst skolem-const-decl "real" multi_polynomial nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" util nil)
    (sigma_scal formula-decl nil sigma "reals/")
    (polyproduct_eval const-decl "real" multi_polynomial nil)
    (T_high type-eq-decl nil sigma "reals/")
    (T_low type-eq-decl nil sigma "reals/"))
   nil))
(multipoly_translate_normalize_TCC1 0
  (multipoly_translate_normalize_TCC1-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)
    (ge_realorder name-judgement "RealOrder" util nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (gt_realorder name-judgement "RealOrder" util nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (bounded_points_exclusive? const-decl "bool" util nil)
    (/= const-decl "boolean" notequal nil)
    (lt_below? const-decl "bool" util nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
(multipoly_translate_normalize_TCC2 0
  (multipoly_translate_normalize_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)
    (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)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (bounded_points_exclusive? const-decl "bool" util nil)
    (/= const-decl "boolean" notequal nil)
    (lt_below? const-decl "bool" util nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
(multipoly_translate_normalize 0
  (multipoly_translate_normalize-3 nil 3503399943
   ("" (skeep)
    (("" (label "altb" -1)
      (("" (label "boundedpointsexclusive" -3)
        (("" (hide "boundedpointsexclusive")
          (("" (skoletin 1)
            (("1" (label "pconstname" -1)
              (("1" (hide "pconstname")
                (("1" (expand "multipoly_eval")
                  (("1" (rewrite "sigma_scal" :dir rl)
                    (("1" (rewrite "sigma_restrict_eq")
                      (("1" (hide 2)
                        (("1" (decompose-equality)
                          (("1" (expand "restrict")
                            (("1" (lift-if)
                              (("1"
                                (ground)
                                (("1"
                                  (name "ii" "x!1")
                                  (("1"
                                    (replace -1)
                                    (("1"
                                      (case
                                       "pconst *
                                                      polyproduct_eval(multipoly_translate(mpoly,
                                                                                           polydegmono,
                                                                                           nvars,
                                                                                           boundedpts)
                                                                                          (Avars, Bvars)
                                                                                          (ii),
                                                                       polydegmono, nvars)
                                                                      (normalize_lambda(nvars, X, boundedpts)
                                                                                       (Avars, Bvars))
                                                    = polyproduct_eval(mpoly(ii), polydegmono, nvars)(X)")
                                      (("1" (assert) nil nil)
                                       ("2"
                                        (hide 3)
                                        (("2"
                                          (expand "polyproduct_eval")
                                          (("2"
                                            (expand "pconst")
                                            (("2"
                                              (rewrite "product_prod")
                                              (("1"
                                                (rewrite
                                                 "product_restrict_eq")
                                                (("1"
                                                  (hide 2)
                                                  (("1"
                                                    (decompose-equality)
                                                    (("1"
                                                      (name "pj" "x!2")
                                                      (("1"
                                                        (replace -1)
                                                        (("1"
                                                          (expand
                                                           "restrict")
                                                          (("1"
                                                            (assert)
                                                            (("1"
                                                              (lift-if)
                                                              (("1"
                                                                (split
                                                                 +)
                                                                (("1"
                                                                  (propax)
                                                                  nil
                                                                  nil)
                                                                 ("2"
                                                                  (flatten)
                                                                  (("2"
                                                                    (assert)
                                                                    (("2"
                                                                      (split
                                                                       +)
                                                                      (("1"
                                                                        (flatten)
                                                                        (("1"
                                                                          (expand
                                                                           "normalize_lambda")
                                                                          (("1"
                                                                            (assert)
                                                                            (("1"
                                                                              (inst
                                                                               -
                                                                               "pj")
                                                                              (("1"
                                                                                (flatten)
                                                                                (("1"
                                                                                  (assert)
                                                                                  (("1"
                                                                                    (assert)
                                                                                    (("1"
                                                                                      (expand
                                                                                       "multipoly_translate")
                                                                                      (("1"
                                                                                        (expand
                                                                                         "polyprod_translate")
                                                                                        (("1"
                                                                                          (lemma
                                                                                           "poly_translate_inf_pos_def_rev")
                                                                                          (("1"
                                                                                            (inst?)
                                                                                            (("1"
                                                                                              (assert)
                                                                                              nil
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (flatten)
                                                                        (("2"
                                                                          (split
                                                                           2)
                                                                          (("1"
                                                                            (flatten)
                                                                            (("1"
                                                                              (inst
                                                                               -
                                                                               "pj")
                                                                              (("1"
                                                                                (flatten)
                                                                                (("1"
                                                                                  (assert)
                                                                                  (("1"
                                                                                    (expand
                                                                                     "normalize_lambda")
                                                                                    (("1"
                                                                                      (expand
                                                                                       "multipoly_translate")
                                                                                      (("1"
                                                                                        (expand
                                                                                         "polyprod_translate")
                                                                                        (("1"
                                                                                          (lemma
                                                                                           "poly_translate_inf_neg_def_rev")
                                                                                          (("1"
                                                                                            (inst?)
                                                                                            (("1"
                                                                                              (assert)
                                                                                              nil
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (flatten)
                                                                            (("2"
                                                                              (case
                                                                               "boundedpts(pj)`1 AND boundedpts(pj)`2")
                                                                              (("1"
                                                                                (flatten)
                                                                                (("1"
                                                                                  (assert)
                                                                                  (("1"
                                                                                    (hide
                                                                                     1)
                                                                                    (("1"
                                                                                      (hide
                                                                                       2)
                                                                                      (("1"
                                                                                        (expand
                                                                                         "normalize_lambda")
                                                                                        (("1"
                                                                                          (inst
                                                                                           -
                                                                                           "pj")
                                                                                          (("1"
                                                                                            (flatten)
                                                                                            (("1"
                                                                                              (assert)
                                                                                              (("1"
                                                                                                (assert)
                                                                                                (("1"
                                                                                                  (expand
                                                                                                   "multipoly_translate")
                                                                                                  (("1"
                                                                                                    (expand
                                                                                                     "polyprod_translate")
                                                                                                    (("1"
                                                                                                      (lemma
                                                                                                       "poly_translate_id")
                                                                                                      (("1"
                                                                                                        (inst?)
                                                                                                        (("1"
                                                                                                          (assert)
                                                                                                          nil
                                                                                                          nil)
                                                                                                         ("2"
                                                                                                          (expand
                                                                                                           "lt_below?")
                                                                                                          (("2"
                                                                                                            (inst
                                                                                                             -
                                                                                                             "pj")
                                                                                                            (("2"
                                                                                                              (assert)
                                                                                                              nil
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (reveal
                                                                                 "boundedpointsexclusive")
                                                                                (("2"
                                                                                  (expand
                                                                                   "bounded_points_exclusive?")
                                                                                  (("2"
                                                                                    (inst
                                                                                     -
                                                                                     "pj")
                                                                                    (("2"
                                                                                      (ground)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (skosimp*)
                                                      (("2"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil)
                                                     ("3"
                                                      (skosimp*)
                                                      (("3"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (skosimp*)
                                                  (("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil)
                                                 ("3"
                                                  (skosimp*)
                                                  (("3"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (skosimp*)
                                                (("2"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil)
                                               ("3"
                                                (skosimp*)
                                                (("3"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (skosimp*) (("2" (assert) nil nil)) nil)
             ("3" (skosimp*) (("3" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sigma_restrict_eq formula-decl nil sigma "reals/")
    (restrict const-decl "[T -> real]" sigma "reals/")
    (polynomial const-decl "[real -> real]" polynomials "reals/")
    (sequence type-eq-decl nil sequences nil)
    (product_prod formula-decl nil product "reals/")
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (poly_translate_inf_pos_def_rev formula-decl nil polynomials
     "reals/")
    (polyprod_translate const-decl "Polynomial" multi_polynomial nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (poly_translate_inf_neg_def_rev formula-decl nil polynomials
     "reals/")
    (poly_translate_id formula-decl nil polynomials "reals/")
    (pj skolem-const-decl "nat" multi_polynomial nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (bounded_points_exclusive? const-decl "bool" util nil)
    (restrict const-decl "[T -> real]" product "reals/")
    (Bvars skolem-const-decl "Vars" multi_polynomial nil)
    (polydegmono skolem-const-decl "DegreeMono" multi_polynomial nil)
    (Avars skolem-const-decl "Vars" multi_polynomial nil)
    (X skolem-const-decl "Vars" multi_polynomial nil)
    (boundedpts skolem-const-decl "IntervalEndpoints" multi_polynomial
     nil)
    (product_restrict_eq formula-decl nil product "reals/")
    (pconst skolem-const-decl "real" multi_polynomial nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" util nil)
    (sigma_scal formula-decl nil sigma "reals/")
    (polyproduct_eval const-decl "real" multi_polynomial nil)
    (T_high type-eq-decl nil sigma "reals/")
    (T_low type-eq-decl nil sigma "reals/")
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.47 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.