Quelle product.prf Sprache: Lisp

(product
(T_pred_lem 0
  (T_pred_lem-1 nil 3352120046
   ("" (skosimp* t)
    (("" (prop)
      (("1" (lemma "connected_domain")
        (("1" (inst - "low!1" "high!1" "z!1") (("1" (assert) nil nil))
          nil))
        nil)
       ("2" (skosimp*)
        (("2" (lemma "connected_domain")
          (("2" (inst - "j!1" "high!1" "z!1") (("2" (assert) nil nil))
            nil))
          nil))
        nil)
       ("3" (skosimp*)
        (("3" (lemma "connected_domain")
          (("3" (inst - "low!1" "j!1" "z!1") (("3" (assert) nil nil))
            nil))
          nil))
        nil)
       ("4" (skosimp*)
        (("4" (lemma "connected_domain")
          (("4" (inst - "low!1" "j!2" "z!1")
            (("1" (assert) nil nil)
             ("2" (lemma "connected_domain")
              (("2" (inst - "j!1" "j!2" "low!1")
                (("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((low!1 skolem-const-decl "T_low" product nil)
    (high!1 skolem-const-decl "T_high" product nil)
    (integer nonempty-type-from-decl nil integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (connected_domain formula-decl nil product nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (OR const-decl "[bool, 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)
    (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)
    (T_pred const-decl "[int -> boolean]" product nil)
    (T formal-subtype-decl nil product nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil product nil)
    (T_low type-eq-decl nil product nil))
   shostak))
(high_low_rewrite_TCC1 0
  (high_low_rewrite_TCC1-1 nil 3352229091
   ("" (skosimp*)
    (("" (inst + "high!1")
      (("1" (assert) nil nil)
       ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil))
      nil))
    nil)
   ((high!1 skolem-const-decl "T_high" product nil)
    (T_high type-eq-decl nil product nil)
    (<= const-decl "bool" reals nil)
    (T formal-subtype-decl nil product nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T_pred const-decl "[int -> boolean]" product nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (T_low type-eq-decl nil product nil)
    (T_pred_lem formula-decl nil product nil))
   nil))
(high_low_rewrite 0
  (high_low_rewrite-1 nil 3352228842
   ("" (skosimp*)
    (("" (inst?)
      (("" (prop) (("" (inst?) (("" (assert) nil nil)) nil)) nil))
      nil))
    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)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (T_pred const-decl "[int -> boolean]" product nil)
    (T formal-subtype-decl nil product nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil product nil)
    (T_low type-eq-decl nil product nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (subrange type-eq-decl nil integers nil)
    (high!1 skolem-const-decl "T_high" product nil)
    (low!1 skolem-const-decl "T_low" product nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   shostak))
(product_TCC1 0
  (product_TCC1-1 nil 3410094710
   ("" (skosimp*)
    (("" (typepred "low!1")
      (("" (typepred "high!1")
        (("" (assert)
          (("" (skosimp*)
            (("" (typepred "j!1")
              (("" (lemma "connected_domain")
                (("" (inst - "low!1" "j!1" "high!1")
                  (("1" (assert) nil nil)
                   ("2" (assert)
                    (("2" (skosimp*)
                      (("2" (lemma "connected_domain")
                        (("2" (inst - "j!2" "j!1" "low!1")
                          (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T_low type-eq-decl nil product nil)
    (<= const-decl "bool" reals nil)
    (T formal-subtype-decl nil product nil)
    (T_pred const-decl "[int -> boolean]" product nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (low!1 skolem-const-decl "T_low" product nil)
    (integer nonempty-type-from-decl nil integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (connected_domain formula-decl nil product nil)
    (T_high type-eq-decl nil product nil))
   nil))
(product_TCC2 0
  (product_TCC2-1 nil 3410094710
   ("" (skeep)
    (("" (typepred "high")
      (("" (typepred "low")
        (("" (assert)
          (("" (ground)
            (("1" (inst + "high") (("1" (assert) nil nil)) nil)
             ("2" (skosimp*)
              (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil)
             ("3" (skosimp*)
              (("3" (inst + "high") (("3" (assert) nil nil)) nil)) nil)
             ("4" (skosimp*)
              (("4" (inst + "j!1") (("4" (assert) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T_high type-eq-decl nil product nil)
    (<= const-decl "bool" reals nil)
    (T formal-subtype-decl nil product nil)
    (T_pred const-decl "[int -> boolean]" product nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (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_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (T_low type-eq-decl nil product nil))
   nil))
(product_TCC3 0
  (product_TCC3-1 nil 3410094710 ("" (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)
    (OR const-decl "[bool, 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)
    (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)
    (T_pred const-decl "[int -> boolean]" product nil)
    (T formal-subtype-decl nil product nil)
    (<= const-decl "bool" reals nil)
    (T_low type-eq-decl nil product nil)
    (T_high type-eq-decl nil product nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (int_plus_int_is_int application-judgement "int" integers nil))
   nil))
(product_spl_TCC1 0
  (product_spl_TCC1-1 nil 3410103726 ("" (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)
    (OR const-decl "[bool, 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)
    (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)
    (T_pred const-decl "[int -> boolean]" product nil)
    (T formal-subtype-decl nil product nil)
    (<= const-decl "bool" reals nil)
    (T_low type-eq-decl nil product nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (int_plus_int_is_int application-judgement "int" integers nil))
   nil))
(product_spl_TCC2 0
  (product_spl_TCC2-1 nil 3410103726
   ("" (skeep)
    (("" (inst + "low + nn + rng") (("" (assert) nil nil)) nil)) nil)
   ((int_plus_int_is_int application-judgement "int" integers nil)
    (rng skolem-const-decl "nat" product nil)
    (nn skolem-const-decl "nat" product nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (low skolem-const-decl "T_low" product nil)
    (T_low type-eq-decl nil product nil)
    (<= const-decl "bool" reals nil)
    (T formal-subtype-decl nil product nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (T_pred const-decl "[int -> boolean]" product nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
(product_spl_TCC3 0
  (product_spl_TCC3-1 nil 3410103726
   ("" (skeep)
    (("" (typepred "low")
      (("" (split -1)
        (("1" (inst + "low") (("1" (assert) nil nil)) nil)
         ("2" (skosimp*)
          (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((T_low type-eq-decl nil product nil)
    (<= const-decl "bool" reals nil)
    (T formal-subtype-decl nil product nil)
    (T_pred const-decl "[int -> boolean]" product nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (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)
    (low skolem-const-decl "T_low" product nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
(product_spl 0
  (product_spl-1 nil 3410103740
   ("" (induct "rng")
    (("1" (assert)
      (("1" (expand "product") (("1" (propax) nil nil)) nil)) nil)
     ("2" (skosimp*)
      (("2" (expand "product" + (1 3))
        (("2" (inst?)
          (("2" (assert)
            (("2" (lemma "T_pred_lem")
              (("2" (inst?)
                (("2" (inst - "1+j!1+low!1+nn!1" "low!1")
                  (("2" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("3" (hide 2)
      (("3" (skosimp*)
        (("3" (inst + "low!1+nn!1")
          (("1" (assert) nil nil)
           ("2" (lemma "T_pred_lem")
            (("2" (inst?)
              (("2" (inst - "low!1+nn!1+rng!2" "low!1")
                (("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("4" (hide 2)
      (("4" (skosimp*)
        (("4" (inst + "low!1+nn!1+rng!2") (("4" (assert) nil nil))
          nil))
        nil))
      nil)
     ("5" (hide 2) (("5" (skosimp*) nil nil)) nil))
    nil)
   ((low!1 skolem-const-decl "T_low" product nil)
    (nn!1 skolem-const-decl "nat" product nil)
    (rng!2 skolem-const-decl "nat" product nil)
    (low!1 skolem-const-decl "T_low" product nil)
    (nn!1 skolem-const-decl "nat" product nil)
    (rng!2 skolem-const-decl "nat" product nil)
    (T_pred_lem formula-decl nil product nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (product def-decl "int" product nil)
    (T_high type-eq-decl nil product nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (pred type-eq-decl nil defined_types 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)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (T_pred const-decl "[int -> boolean]" product nil)
    (T formal-subtype-decl nil product nil)
    (<= const-decl "bool" reals nil)
    (T_low type-eq-decl nil product 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)
    (int_plus_int_is_int application-judgement "int" integers nil))
   nil))
(product_split_TCC1 0
  (product_split_TCC1-1 nil 3410103726
   ("" (skeep)
    (("" (typepred "high")
      (("" (assert)
        (("" (split -1)
          (("1" (inst + "high") nil nil)
           ("2" (skosimp*)
            (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((T_high type-eq-decl nil product nil)
    (<= const-decl "bool" reals nil)
    (T formal-subtype-decl nil product nil)
    (T_pred const-decl "[int -> boolean]" product nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (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)
    (high skolem-const-decl "T_high" product nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil))
(product_split_TCC2 0
  (product_split_TCC2-1 nil 3410103726
   ("" (skeep)
    (("" (typepred "low")
      (("" (split -1)
        (("1" (inst + "low") (("1" (assert) nil nil)) nil)
         ("2" (skosimp*)
          (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((T_low type-eq-decl nil product nil)
    (<= const-decl "bool" reals nil)
    (T formal-subtype-decl nil product nil)
    (T_pred const-decl "[int -> boolean]" product nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (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)
    (low skolem-const-decl "T_low" product nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (int_plus_int_is_int application-judgement "int" integers nil))
   nil))
(product_split 0
  (product_split-1 nil 3410103810
   ("" (skosimp*)
    (("" (case "high!1)
      (("1" (expand "product") (("1" (assert) nil nil)) nil)
       ("2" (case-replace "z!1=low!1-1")
        (("1" (assert)
          (("1" (expand "product") (("1" (assert) nil nil)) nil)) nil)
         ("2" (lemma "product_spl")
          (("2" (inst - "F!1" "low!1" "z!1-low!1" "high!1-z!1")
            (("1" (assert)
              (("1" (hide-all-but (1 3))
                (("1" (use "T_pred_lem") (("1" (assert) nil nil)) nil))
                nil))
              nil)
             ("2" (assert) nil nil) ("3" (assert) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T_low type-eq-decl nil product nil)
    (T_high type-eq-decl nil product nil)
    (<= const-decl "bool" reals nil)
    (T formal-subtype-decl nil product nil)
    (T_pred const-decl "[int -> boolean]" product nil)
    (OR const-decl "[bool, bool -> bool]" 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)
    (< const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (product def-decl "int" product nil)
    (product_spl formula-decl nil product nil)
    (T_pred_lem formula-decl nil product nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (high!1 skolem-const-decl "T_high" product nil)
    (low!1 skolem-const-decl "T_low" product nil)
    (z!1 skolem-const-decl "int" product nil)
    (>= const-decl "bool" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil))
   nil))
(product_div 0
  (product_div-1 nil 3410104326
   ("" (skeep)
    (("" (cross-mult 2)
      (("" (lemma "product_split")
        (("" (inst - "F" "high" "low" "z") (("" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (div_cancel3 formula-decl nil real_props nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (product def-decl "int" product nil)
    (T_high type-eq-decl nil product nil)
    (T_low type-eq-decl nil product nil)
    (<= const-decl "bool" reals nil)
    (T formal-subtype-decl nil product nil)
    (T_pred const-decl "[int -> boolean]" product nil)
    (OR const-decl "[bool, bool -> bool]" booleans 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)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal 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)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (product_split formula-decl nil product nil))
   shostak))
(product_div_neg 0
  (product_div_neg-1 nil 3410104551
   ("" (skeep)
    (("" (cross-mult 2)
      (("" (lemma "product_split")
        (("" (inst - "F" "high" "low" "z") (("" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((int_plus_int_is_int application-judgement "int" integers 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)
    (T_pred const-decl "[int -> boolean]" product nil)
    (T formal-subtype-decl nil product nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil product nil)
    (T_low type-eq-decl nil product nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (product_split formula-decl nil product nil))
   shostak))
(product_eq_arg 0
  (product_eq_arg-1 nil 3410104588
   ("" (skosimp*)
    (("" (expand "product")
      (("" (expand "product") (("" (propax) nil nil)) nil)) nil))
    nil)
   ((product def-decl "int" product nil)) shostak))
(product_first_TCC1 0
  (product_first_TCC1-1 nil 3410104637
   ("" (skeep)
    (("" (typepred "low")
      (("" (assert)
        (("" (skosimp*)
          (("" (typepred "high")
            (("" (assert)
              (("" (split -1)
                (("1" (lemma "connected_domain")
                  (("1" (assert)
                    (("1" (inst - "j!1" "high" "low")
                      (("1" (assert) nil nil)) nil))
                    nil))
                  nil)
                 ("2" (skosimp*)
                  (("2" (lemma "connected_domain")
                    (("2" (inst - "j!1" "j!2" "low")
                      (("2" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T_low type-eq-decl nil product nil)
    (<= const-decl "bool" reals nil)
    (T formal-subtype-decl nil product nil)
    (T_pred const-decl "[int -> boolean]" product nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (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)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (connected_domain formula-decl nil product nil)
    (integer nonempty-type-from-decl nil integers nil)
    (T_high type-eq-decl nil product nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
(product_first_TCC2 0
  (product_first_TCC2-1 nil 3410104637
   ("" (skeep)
    (("" (typepred "low")
      (("" (assert)
        (("" (split -1)
          (("1" (inst + "low") (("1" (assert) nil nil)) nil)
           ("2" (skosimp*)
            (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((T_low type-eq-decl nil product nil)
    (<= const-decl "bool" reals nil)
    (T formal-subtype-decl nil product nil)
    (T_pred const-decl "[int -> boolean]" product nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (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)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (low skolem-const-decl "T_low" product nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_plus_int_is_int application-judgement "int" integers nil))
   nil))
(product_first 0
  (product_first-1 nil 3410104659
   ("" (skosimp*)
    (("" (lemma "product_split")
      (("" (inst?)
        (("" (inst -1 "low!1")
          (("" (rewrite "product_eq_arg") (("" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((product_split formula-decl nil product nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (product_eq_arg formula-decl nil product nil)
    (T_low type-eq-decl nil product nil)
    (T_high type-eq-decl nil product nil)
    (<= const-decl "bool" reals nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T formal-subtype-decl nil product nil)
    (T_pred const-decl "[int -> boolean]" product nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   nil))
(product_last_TCC1 0
  (product_last_TCC1-1 nil 3410104637
   ("" (skeep)
    (("" (typepred "high")
      (("" (split -1)
        (("1" (inst + "high") (("1" (assert) nil nil)) nil)
         ("2" (skosimp*)
          (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((T_high type-eq-decl nil product nil)
    (<= const-decl "bool" reals nil)
    (T formal-subtype-decl nil product nil)
    (T_pred const-decl "[int -> boolean]" product nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (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)
    (high skolem-const-decl "T_high" product nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
(product_last_TCC2 0
  (product_last_TCC2-1 nil 3410104637
   ("" (skeep)
    (("" (typepred "high")
      (("" (assert)
        (("" (skosimp*)
          (("" (lemma "connected_domain")
            (("" (inst - "low" "j!1" "high")
              (("1" (assert) nil nil)
               ("2" (typepred "low")
                (("2" (assert)
                  (("2" (skosimp*)
                    (("2" (lemma "connected_domain")
                      (("2" (assert)
                        (("2" (inst - "j!2" "j!1" "low")
                          (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T_high type-eq-decl nil product nil)
    (<= const-decl "bool" reals nil)
    (T formal-subtype-decl nil product nil)
    (T_pred const-decl "[int -> boolean]" product nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (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)
    (T_low type-eq-decl nil product nil)
    (low skolem-const-decl "T_low" product nil)
    (integer nonempty-type-from-decl nil integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (connected_domain formula-decl nil product nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
(product_last 0
  (product_last-1 nil 3410104722
   ("" (skosimp*)
    (("" (rewrite "product") (("" (assert) nil nil)) nil)) nil)
   ((product def-decl "int" product 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)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (T_pred const-decl "[int -> boolean]" product nil)
    (T formal-subtype-decl nil product nil)
    (<= const-decl "bool" reals nil)
    (T_low type-eq-decl nil product nil)
    (T_high type-eq-decl nil product nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil))
(product_middle_TCC1 0
  (product_middle_TCC1-1 nil 3410104812
   ("" (skeep)
    (("" (typepred "i") (("" (inst + "i") (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((T formal-subtype-decl nil product nil)
    (T_pred const-decl "[int -> boolean]" product nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
(product_middle_TCC2 0
  (product_middle_TCC2-1 nil 3410104812
   ("" (skeep)
    (("" (typepred "i") (("" (inst + "i") (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((T formal-subtype-decl nil product nil)
    (T_pred const-decl "[int -> boolean]" product nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
(product_middle 0
  (product_middle-1 nil 3410104844
   ("" (skosimp*)
    (("" (lemma "product_split")
      (("" (inst?)
        (("" (inst -1 "i!1")
          (("" (assert)
            (("" (assert)
              (("" (replace -1)
                (("" (hide -1)
                  (("" (expand "product" 1 1) (("" (propax) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((product_split formula-decl nil product nil)
    (product def-decl "int" product nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (T_low type-eq-decl nil product nil)
    (T_high type-eq-decl nil product nil)
    (<= const-decl "bool" reals nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T formal-subtype-decl nil product nil)
    (T_pred const-decl "[int -> boolean]" product nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   nil))
(product_const_TCC1 0
  (product_const_TCC1-1 nil 3410104812 ("" (subtype-tcc) nil nil)
   ((int_plus_int_is_int application-judgement "int" integers nil))
   nil))
(product_const 0
  (product_const-2 nil 3410105217
   ("" (skolem 1 (_ _ nzr))
    (("" (rewrite "high_low_rewrite")
      (("" (hide 2)
        (("" (skosimp*)
          (("" (prop)
            (("1" (expand "product") (("1" (assert) nil nil)) nil)
             ("2" (induct "n" 2)
              (("1" (rewrite "product_eq_arg")
                (("1" (assert)
                  (("1" (expand "^")
                    (("1" (expand "expt")
                      (("1" (expand "expt") (("1" (propax) nil nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil))
                nil)
               ("2" (hide 2)
                (("2" (skosimp*)
                  (("2" (expand "product" +)
                    (("2" (assert)
                      (("2" (lemma "expt_plus")
                        (("2" (inst - "(1 - low!1 + k!1)" "1" "nzr")
                          (("2" (replace -1)
                            (("2" (hide -1)
                              (("2"
                                (rewrite "expt_x1")
                                (("2" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("3" (hide 3)
                (("3" (skosimp*)
                  (("3" (inst + "high!1")
                    (("1" (assert) nil nil)
                     ("2" (use "T_pred_lem") (("2" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("4" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (high_low_rewrite formula-decl nil product 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)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (T_pred const-decl "[int -> boolean]" product nil)
    (T formal-subtype-decl nil product nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil product nil)
    (T_low type-eq-decl nil product nil)
    (pred type-eq-decl nil defined_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (product def-decl "int" product nil)
    (/= const-decl "boolean" notequal nil)
    (nzint nonempty-type-eq-decl nil integers nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (>= const-decl "bool" reals nil)
    (^ const-decl "real" exponentiation nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (low!1 skolem-const-decl "T_low" product nil)
    (high!1 skolem-const-decl "T_high" product nil)
    (subrange type-eq-decl nil integers nil)
    (subrange_induction formula-decl nil subrange_inductions nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (T_pred_lem formula-decl nil product nil)
    (int_exp application-judgement "int" exponentiation nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (expt def-decl "real" exponentiation nil)
    (nzreal_exp application-judgement "nzreal" exponentiation nil)
    (rat_exp application-judgement "rat" exponentiation nil)
    (product_eq_arg formula-decl nil product nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (expt_x1 formula-decl nil exponentiation nil)
    (even_minus_odd_is_odd application-judgement "odd_int" integers
     nil)
    (expt_plus formula-decl nil exponentiation nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil)
  (product_const-1 nil 3410104877
   ("" (skolem 1 (_ _ x))
    (("" (rewrite "high_low_rewrite")
      (("1" (hide 2)
        (("1" (skosimp*)
          (("1" (prop)
            (("1" (expand "product") (("1" (assert) nil nil)) nil)
             ("2" (induct "n" 2)
              (("1" (rewrite "product_eq_arg")
                (("1" (assert)
                  (("1" (expand "^")
                    (("1" (expand "expt")
                      (("1" (expand "expt") (("1" (propax) nil nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil))
                nil)
               ("2" (hide 2)
                (("2" (skosimp*)
                  (("2" (expand "product" +)
                    (("2" (assert)
                      (("2" (lemma "expt_plus")
                        (("2" (inst - "(1 - low!1 + k!1)" "1" "x")
                          (("1" (replace -1)
                            (("1" (hide -1)
                              (("1"
                                (rewrite "expt_x1")
                                (("1" (assert) nil nil))
                                nil))
                              nil))
                            nil)
                           ("2" (flatten) (("2" (postpone) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("3" (hide 3)
                (("3" (skosimp*)
                  (("3" (inst + "high!1")
                    (("1" (assert) nil nil)
                     ("2" (use "T_pred_lem") (("2" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("4" (assert) nil nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (postpone) nil nil))
      nil))
    nil)
   nil nil))
(product_zero 0
  (product_zero-1 nil 3410105243
   ("" (skosimp*)
    (("" (rewrite "product_first") (("" (assert) nil nil)) nil)) nil)
   ((product_first formula-decl nil product 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)
    (T_pred const-decl "[int -> boolean]" product nil)
    (T formal-subtype-decl nil product nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil product nil)
    (T_low type-eq-decl nil product nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (even_times_int_is_even application-judgement "even_int" 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))
   shostak))
(product_scal_TCC1 0
  (product_scal_TCC1-1 nil 3410105938 ("" (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)
    (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)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (T_pred const-decl "[int -> boolean]" product nil)
    (T formal-subtype-decl nil product nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil product nil)
    (T_low type-eq-decl nil product nil)
    (/= const-decl "boolean" notequal nil)
    (int_plus_int_is_int application-judgement "int" integers nil))
   nil))
(product_scal 0
  (product_scal-1 nil 3410105347
   ("" (skolem 1 ("F" "a" _ _))
    (("" (rewrite "high_low_rewrite")
      (("1" (hide 2)
        (("1" (skosimp*)
          (("1" (ground)
            (("1" (induct "n" 2)
              (("1" (rewrite "product_eq_arg")
                (("1" (rewrite "product_eq_arg")
                  (("1" (assert) (("1" (rewrite "expt_x1") nil nil))
                    nil))
                  nil)
                 ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil))
                nil)
               ("2" (hide 2)
                (("2" (skosimp*)
                  (("2" (expand "product" +)
                    (("2" (assert)
                      (("2" (replace -2)
                        (("2" (hide -2)
                          (("2" (lemma "expt_plus")
                            (("2" (inst - "(1 - low!1 + k!1)" "1" "a")
                              (("2"
                                (assert)
                                (("2"
                                  (replace -1)
                                  (("2"
                                    (hide -1)
                                    (("2"
                                      (rewrite "expt_x1")
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("3" (skosimp*)
                (("3" (inst + "high!1")
                  (("1" (assert) nil nil)
                   ("2" (use "T_pred_lem") (("2" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide 2) (("2" (skosimp*) nil nil)) nil))
      nil))
    nil)
   ((mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (high_low_rewrite formula-decl nil product 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)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (T_pred const-decl "[int -> boolean]" product nil)
    (T formal-subtype-decl nil product nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil product nil)
    (T_low type-eq-decl nil product nil)
    (pred type-eq-decl nil defined_types nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (product def-decl "int" product nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (>= const-decl "bool" reals nil)
    (^ const-decl "real" exponentiation nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (rat_exp application-judgement "rat" exponentiation nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (low!1 skolem-const-decl "T_low" product nil)
    (high!1 skolem-const-decl "T_high" product nil)
    (subrange type-eq-decl nil integers nil)
    (a skolem-const-decl "int" product nil)
    (subrange_induction formula-decl nil subrange_inductions nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (T_pred_lem formula-decl nil product nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (expt_x1 formula-decl nil exponentiation nil)
    (int_exp application-judgement "int" exponentiation nil)
    (product_eq_arg formula-decl nil product nil)
    (rat_times_rat_is_rat application-judgement "rat" rationals nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (expt_plus formula-decl nil exponentiation nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
(product_ge_0_TCC1 0
  (product_ge_0_TCC1-1 nil 3410107098
   ("" (skosimp*)
    (("" (typepred "n!1")
      (("" (typepred "low!1")
        (("" (assert)
          (("" (typepred "high!1")
            (("" (lemma "connected_domain")
              (("" (split -2)
                (("1" (split -3)
                  (("1" (inst - "low!1" "high!1" "n!1")
                    (("1" (assert) nil nil)) nil)
                   ("2" (skosimp*)
                    (("2" (inst - "j!1" "high!1" "n!1")
                      (("2" (assert) nil nil)) nil))
                    nil))
                  nil)
                 ("2" (skosimp*)
                  (("2" (inst - "low!1" "j!1" "n!1")
                    (("1" (assert) nil nil)
                     ("2" (assert)
                      (("2" (skosimp*)
                        (("2" (lemma "connected_domain")
                          (("2" (inst - "j!2" "j!1" "low!1")
                            (("2" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((subrange type-eq-decl nil integers nil)
    (T_high type-eq-decl nil product nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (T_low type-eq-decl nil product nil)
    (T formal-subtype-decl nil product nil)
    (T_pred const-decl "[int -> boolean]" product nil)
    (OR const-decl "[bool, bool -> bool]" 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)
    (<= 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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (connected_domain formula-decl nil product nil)
    (integer nonempty-type-from-decl nil integers nil)
    (high!1 skolem-const-decl "T_high" product nil)
    (low!1 skolem-const-decl "T_low" product nil))
   nil))
(product_ge_0 0
  (product_ge_0-1 nil 3410107124
   ("" (skolem 1 ("F" _ _))
    (("" (rewrite "high_low_rewrite")
      (("1" (hide 2)
        (("1" (skosimp*)
          (("1" (prop)
            (("1" (expand "product") (("1" (assert) nil nil)) nil)
             ("2" (induct "n" 2)
              (("1" (skosimp*)
                (("1" (rewrite "product_eq_arg")
                  (("1" (inst?) nil nil)
                   ("2" (hide -1 2)
                    (("2" (use "T_pred_lem") (("2" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (hide 2)
                (("2" (skosimp*)
                  (("2" (expand "product" +)
                    (("2" (prop)
                      (("1" (inst?)
                        (("1" (assert) (("1" (grind-reals) nil nil))
                          nil))
                        nil)
                       ("2" (skosimp*) (("2" (inst?) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("3" (hide 3)
                (("3" (skosimp*)
                  (("3" (inst + "high!1")
                    (("1" (assert) nil nil)
                     ("2" (hide -1)
                      (("2" (use "T_pred_lem") (("2" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("4" (hide-all-but 1)
                (("4" (skosimp* t)
                  (("4" (hide -1)
                    (("4" (use "T_pred_lem") (("4" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("5" (assert) nil nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide 2)
        (("2" (skosimp* t)
          (("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((high_low_rewrite formula-decl nil product 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)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (T_pred const-decl "[int -> boolean]" product nil)
    (T formal-subtype-decl nil product nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil product nil)
    (T_low type-eq-decl nil product nil)
    (pred type-eq-decl nil defined_types nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (subrange type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (product def-decl "int" product nil)
    (low!1 skolem-const-decl "T_low" product nil)
    (high!1 skolem-const-decl "T_high" product nil)
    (F skolem-const-decl "[T -> int]" product nil)
    (subrange_induction formula-decl nil subrange_inductions nil)
    (product_eq_arg formula-decl nil product nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (T_pred_lem formula-decl nil product nil)
    (pos_times_ge formula-decl nil real_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
(product_gt_0 0
  (product_gt_0-1 nil 3410107170
   ("" (skolem 1 ("F" _ _))
    (("" (rewrite "high_low_rewrite")
      (("1" (hide 2)
        (("1" (skosimp*)
          (("1" (prop)
            (("1" (expand "product") (("1" (assert) nil nil)) nil)
             ("2" (induct "n" 2)
              (("1" (skosimp*)
--> --------------------

--> maximum size reached

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

quality100%

¤ Dauer der Verarbeitung: 0.41 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.