Quelle sigma_2D.prf Sprache: Lisp

(sigma_2D
(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" sigma_2D nil)
    (high!1 skolem-const-decl "T_high" sigma_2D 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 sigma_2D 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]" sigma_2D nil)
    (T formal-subtype-decl nil sigma_2D nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma_2D nil)
    (T_low type-eq-decl nil sigma_2D 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" sigma_2D nil)
    (T_high type-eq-decl nil sigma_2D nil)
    (<= const-decl "bool" reals nil)
    (T formal-subtype-decl nil sigma_2D nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T_pred const-decl "[int -> boolean]" sigma_2D 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 sigma_2D nil)
    (T_pred_lem formula-decl nil sigma_2D 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]" sigma_2D nil)
    (T formal-subtype-decl nil sigma_2D nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma_2D nil)
    (T_low type-eq-decl nil sigma_2D 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" sigma_2D nil)
    (low!1 skolem-const-decl "T_low" sigma_2D nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   shostak))
(sigma_TCC1 0
  (sigma_TCC1-2 nil 3403452046
   ("" (skosimp* t)
    (("" (assert)
      (("" (skosimp*)
        (("" (typepred "j!1")
          (("" (lemma "connected_domain")
            (("" (inst - "low!1" "j!1" "high!1")
              (("1" (assert) nil nil)
               ("2" (prop)
                (("2" (skosimp*)
                  (("2" (lemma "connected_domain")
                    (("2" (assert)
                      (("2" (inst - "j!2" "j!1" "low!1")
                        (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (low!1 skolem-const-decl "T_low" sigma_2D 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 sigma_2D 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]" sigma_2D nil)
    (T formal-subtype-decl nil sigma_2D nil)
    (<= const-decl "bool" reals nil)
    (T_low type-eq-decl nil sigma_2D nil)
    (T_high type-eq-decl nil sigma_2D nil))
   nil)
  (sigma_TCC1-1 nil 3255975799
   ("" (skosimp*) (("" (use "T_pred_lem") (("" (assert) nil nil)) nil))
    nil)
   nil nil))
(sigma_TCC2 0
  (sigma_TCC2-2 nil 3403452083
   ("" (skosimp*)
    (("" (typepred "high!1")
      (("" (assert)
        (("" (prop)
          (("1" (inst + "high!1") (("1" (assert) nil nil)) nil)
           ("2" (skosimp*)
            (("2" (typepred "j!1")
              (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T_high type-eq-decl nil sigma_2D nil)
    (<= const-decl "bool" reals nil)
    (T formal-subtype-decl nil sigma_2D nil)
    (T_pred const-decl "[int -> boolean]" sigma_2D 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)
    (high!1 skolem-const-decl "T_high" sigma_2D nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil)
  (sigma_TCC2-1 nil 3255975799
   ("" (skosimp* t)
    (("" (assert)
      (("" (skosimp*)
        (("" (typepred "j!1")
          (("" (lemma "connected_domain")
            (("" (inst - "low!1" "j!1" "high!1")
              (("1" (assert) nil nil)
               ("2" (prop)
                (("2" (skosimp*)
                  (("2" (lemma "connected_domain")
                    (("2" (assert)
                      (("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))
(sigma_TCC3 0
  (sigma_TCC3-1 nil 3255975799
   ("" (skosimp*) (("" (grind) nil nil)) nil)
   ((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
     real_defs nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil))
(sigma_rew_TCC1 0
  (sigma_rew_TCC1-1 nil 3411477956
   ("" (skosimp*)
    (("" (assert)
      (("" (typepred "low!1")
        (("" (typepred "high!1")
          (("" (ground)
            (("" (skosimp*)
              (("" (assert)
                (("" (typepred "j!1")
                  (("" (typepred "j!2")
                    (("" (lemma "connected_domain")
                      (("" (inst - "j!1" "j!2" "low!1")
                        (("" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (T_high type-eq-decl nil sigma_2D nil)
    (connected_domain formula-decl nil sigma_2D nil)
    (integer nonempty-type-from-decl nil integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props 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]" sigma_2D nil)
    (T formal-subtype-decl nil sigma_2D nil)
    (<= const-decl "bool" reals nil)
    (T_low type-eq-decl nil sigma_2D nil))
   nil))
(sigma_rew 0
  (sigma_rew-1 nil 3352522445
   ("" (skosimp*)
    (("" (lift-if)
      (("" (ground)
        (("1" (expand "sigma") (("1" (propax) nil nil)) nil)
         ("2" (expand "sigma")
          (("2" (expand "sigma") (("2" (assert) nil nil)) nil)) nil)
         ("3" (expand "sigma" 2 1) (("3" (propax) nil nil)) nil))
        nil))
      nil))
    nil)
   ((add_zero_right formula-decl nil vectors_2D nil)
    (sigma def-decl "Vector" sigma_2D nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   shostak))
(sigma_spl_TCC1 0
  (sigma_spl_TCC1-1 nil 3255975799
   ("" (skosimp*)
    (("" (inst + "low!1 + nn!1 + rng!1") (("" (assert) nil nil)) nil))
    nil)
   nil nil))
(sigma_spl_TCC2 0
  (sigma_spl_TCC2-1 nil 3255975799
   ("" (skosimp*)
    (("" (inst + "low!1 + nn!1 + rng!1") (("" (assert) nil nil)) nil))
    nil)
   ((int_plus_int_is_int application-judgement "int" integers nil)
    (rng!1 skolem-const-decl "nat" sigma_2D nil)
    (nn!1 skolem-const-decl "nat" sigma_2D nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (low!1 skolem-const-decl "T_low" sigma_2D nil)
    (T_low type-eq-decl nil sigma_2D nil)
    (<= const-decl "bool" reals nil)
    (T formal-subtype-decl nil sigma_2D 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]" sigma_2D 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))
(sigma_spl_TCC3 0
  (sigma_spl_TCC3-1 nil 3351939915
   ("" (skosimp* t)
    (("" (prop)
      (("1" (assert)
        (("1" (inst + "low!1") (("1" (assert) nil nil)) nil)) nil)
       ("2" (skosimp*)
        (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil))
      nil))
    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)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (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]" sigma_2D nil)
    (T formal-subtype-decl nil sigma_2D nil)
    (<= const-decl "bool" reals nil)
    (T_low type-eq-decl nil sigma_2D nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil))
   nil))
(sigma_spl 0
  (sigma_spl-1 nil 3255975799
   ("" (induct "rng")
    (("1" (skosimp*)
      (("1" (assert)
        (("1" (expand "sigma" 1 3) (("1" (assert) nil nil)) nil)) nil))
      nil)
     ("2" (skosimp*)
      (("2" (expand "sigma" + (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)
                    (("2" (replace -2)
                      (("2" (hide -2)
                        (("2" (apply-extensionality 1 :hide? t)
                          (("1" (grind) nil nil) ("2" (grind) nil nil)
                           ("3" (grind) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("3" (skosimp*)
      (("3" (inst + "low!1")
        (("1" (assert) nil nil)
         ("2" (typepred "low!1")
          (("2" (assert)
            (("2" (skosimp*)
              (("2" (lemma "connected_domain")
                (("2" (inst - "j!1" "low!1 + nn!1 + rng!2" "low!1")
                  (("2" (assert) nil 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" sigma_2D nil)
    (nn!1 skolem-const-decl "nat" sigma_2D nil)
    (rng!2 skolem-const-decl "nat" sigma_2D nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (integer nonempty-type-from-decl nil integers nil)
    (connected_domain formula-decl nil sigma_2D nil)
    (low!1 skolem-const-decl "T_low" sigma_2D nil)
    (T_pred_lem formula-decl nil sigma_2D nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (add_zero_right formula-decl nil vectors_2D nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (+ const-decl "Vector" vectors_2D nil)
    (sigma def-decl "Vector" sigma_2D nil)
    (T_high type-eq-decl nil sigma_2D nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vector type-eq-decl nil vectors_2D 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]" sigma_2D nil)
    (T formal-subtype-decl nil sigma_2D nil)
    (<= const-decl "bool" reals nil)
    (T_low type-eq-decl nil sigma_2D 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))
(sigma_split_TCC1 0
  (sigma_split_TCC1-1 nil 3255975799
   ("" (skosimp* t)
    (("" (prop)
      (("1" (inst + "high!1") nil nil) ("2" (inst + "high!1") nil nil)
       ("3" (skosimp*)
        (("3" (inst + "j!1") (("3" (assert) nil nil)) nil)) nil)
       ("4" (skosimp*)
        (("4" (inst + "j!2") (("4" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((high!1 skolem-const-decl "T_high" sigma_2D nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (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]" sigma_2D nil)
    (T formal-subtype-decl nil sigma_2D nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma_2D nil)
    (T_low type-eq-decl nil sigma_2D nil))
   nil))
(sigma_split_TCC2 0
  (sigma_split_TCC2-1 nil 3351939915
   ("" (skosimp* t)
    (("" (assert)
      (("" (prop)
        (("1" (inst + "low!1") (("1" (assert) nil nil)) nil)
         ("2" (skosimp*)
          (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil)
         ("3" (skosimp*)
          (("3" (inst + "low!1") (("3" (assert) nil nil)) nil)) nil)
         ("4" (skosimp*)
          (("4" (inst + "j!1") (("4" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((int_plus_int_is_int application-judgement "int" integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (low!1 skolem-const-decl "T_low" sigma_2D 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]" sigma_2D nil)
    (T formal-subtype-decl nil sigma_2D nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma_2D nil)
    (T_low type-eq-decl nil sigma_2D nil))
   nil))
(sigma_split 0
  (sigma_split-1 nil 3255975799
   ("" (skosimp*)
    (("" (case "high!1)
      (("1" (expand "sigma") (("1" (assert) nil nil)) nil)
       ("2" (case-replace "z!1=low!1-1")
        (("1" (assert)
          (("1" (expand "sigma") (("1" (assert) nil nil)) nil)) nil)
         ("2" (lemma "sigma_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 sigma_2D nil)
    (T_high type-eq-decl nil sigma_2D nil)
    (<= const-decl "bool" reals nil)
    (T formal-subtype-decl nil sigma_2D nil)
    (T_pred const-decl "[int -> boolean]" sigma_2D 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)
    (add_zero_left formula-decl nil vectors_2D 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)
    (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)
    (sigma def-decl "Vector" sigma_2D nil)
    (sigma_spl formula-decl nil sigma_2D nil)
    (T_pred_lem formula-decl nil sigma_2D nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (high!1 skolem-const-decl "T_high" sigma_2D nil)
    (low!1 skolem-const-decl "T_low" sigma_2D nil)
    (z!1 skolem-const-decl "int" sigma_2D 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))
(sigma_diff 0
  (sigma_diff-1 nil 3255975799
   ("" (skosimp*)
    (("" (lemma "sigma_split")
      (("" (inst?)
        (("" (inst -1 "z!1")
          (("" (assert)
            (("" (assert)
              (("" (replace -1)
                (("" (hide -1) (("" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sigma_split formula-decl nil sigma_2D nil)
    (add_cancel formula-decl nil vectors_2D 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)
    (T_low type-eq-decl nil sigma_2D nil)
    (T_high type-eq-decl nil sigma_2D nil)
    (<= const-decl "bool" reals nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (T formal-subtype-decl nil sigma_2D nil)
    (T_pred const-decl "[int -> boolean]" sigma_2D 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))
(sigma_diff_neg 0
  (sigma_diff_neg-1 nil 3255975799
   ("" (skosimp*)
    (("" (lemma "sigma_diff")
      (("" (inst -1 "F!1" "high!1" "low!1" "z!1")
        (("" (assert)
          (("" (replace -1 + rl)
            (("" (assert)
              (("" (expand "-") (("" (propax) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sigma_diff formula-decl nil sigma_2D nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (- const-decl "Vector" vectors_2D nil)
    (- const-decl "Vector" vectors_2D nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (T_low type-eq-decl nil sigma_2D nil)
    (T_high type-eq-decl nil sigma_2D nil)
    (<= const-decl "bool" reals nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (T formal-subtype-decl nil sigma_2D nil)
    (T_pred const-decl "[int -> boolean]" sigma_2D 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))
(sigma_eq_arg 0
  (sigma_eq_arg-1 nil 3255975799
   ("" (skosimp*)
    (("" (expand "sigma")
      (("" (expand "sigma") (("" (assert) nil nil)) nil)) nil))
    nil)
   ((sigma def-decl "Vector" sigma_2D nil)
    (add_zero_right formula-decl nil vectors_2D nil))
   nil))
(sigma_first_TCC1 0
  (sigma_first_TCC1-1 nil 3255975799
   ("" (skosimp*) (("" (use "T_pred_lem") (("" (assert) nil nil)) nil))
    nil)
   ((T_pred_lem formula-decl nil sigma_2D nil)
    (T_low type-eq-decl nil sigma_2D nil)
    (<= const-decl "bool" reals nil)
    (T formal-subtype-decl nil sigma_2D nil)
    (T_pred const-decl "[int -> boolean]" sigma_2D 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)
    (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)
    (T_high type-eq-decl nil sigma_2D nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
(sigma_first_TCC2 0
  (sigma_first_TCC2-1 nil 3352113941
   ("" (skosimp* t)
    (("" (prop)
      (("1" (inst + "low!1") (("1" (assert) nil nil)) nil)
       ("2" (skosimp*)
        (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil)
       ("3" (inst + "low!1") (("3" (assert) nil nil)) nil)
       ("4" (skosimp*)
        (("4" (inst + "j!1") (("4" (assert) nil nil)) nil)) nil))
      nil))
    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)
    (low!1 skolem-const-decl "T_low" sigma_2D 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]" sigma_2D nil)
    (T formal-subtype-decl nil sigma_2D nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma_2D nil)
    (T_low type-eq-decl nil sigma_2D nil))
   nil))
(sigma_first 0
  (sigma_first-1 nil 3255975799
   ("" (skosimp*)
    (("" (lemma "sigma_split")
      (("" (inst?)
        (("" (inst -1 "low!1")
          (("" (rewrite "sigma_eq_arg") (("" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((sigma_split formula-decl nil sigma_2D 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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sigma_eq_arg formula-decl nil sigma_2D nil)
    (T_low type-eq-decl nil sigma_2D nil)
    (T_high type-eq-decl nil sigma_2D nil)
    (<= const-decl "bool" reals nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (T formal-subtype-decl nil sigma_2D nil)
    (T_pred const-decl "[int -> boolean]" sigma_2D 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))
(sigma_last_TCC1 0
  (sigma_last_TCC1-2 nil 3351941334
   ("" (skosimp* t)
    (("" (prop)
      (("1" (inst + "high!1") (("1" (assert) nil nil)) nil)
       ("2" (skosimp*)
        (("2" (inst + "high!1") (("2" (assert) nil nil)) nil)) nil)
       ("3" (skosimp*)
        (("3" (inst + "j!1") (("3" (assert) nil nil)) nil)) nil)
       ("4" (skosimp*)
        (("4" (inst + "j!2") (("4" (assert) nil nil)) nil)) nil))
      nil))
    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)
    (high!1 skolem-const-decl "T_high" sigma_2D 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]" sigma_2D nil)
    (T formal-subtype-decl nil sigma_2D nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma_2D nil)
    (T_low type-eq-decl nil sigma_2D nil))
   nil)
  (sigma_last_TCC1-1 nil 3255975799
   ("" (skosimp*)
    (("" (typepred "high!1")
      (("" (skosimp*) (("" (inst + "j!1") (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   nil nil))
(sigma_last_TCC2 0
  (sigma_last_TCC2-1 nil 3351939915
   ("" (skosimp*) (("" (use "T_pred_lem") (("" (assert) nil nil)) nil))
    nil)
   ((T_pred_lem formula-decl nil sigma_2D nil)
    (T_high type-eq-decl nil sigma_2D nil)
    (<= const-decl "bool" reals nil)
    (T formal-subtype-decl nil sigma_2D nil)
    (T_pred const-decl "[int -> boolean]" sigma_2D 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)
    (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)
    (T_low type-eq-decl nil sigma_2D nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
(sigma_last 0
  (sigma_last-1 nil 3255975799
   ("" (skosimp*)
    (("" (rewrite "sigma")
      (("" (assert)
        (("" (expand "sigma")
          (("" (lift-if)
            (("" (ground)
              (("" (expand "+ ") (("" (propax) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sigma def-decl "Vector" sigma_2D 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]" sigma_2D nil)
    (T formal-subtype-decl nil sigma_2D nil)
    (<= const-decl "bool" reals nil)
    (T_low type-eq-decl nil sigma_2D nil)
    (T_high type-eq-decl nil sigma_2D nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (add_zero_right formula-decl nil vectors_2D nil)
    (add_zero_left formula-decl nil vectors_2D nil)
    (+ const-decl "Vector" vectors_2D 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))
(sigma_middle_TCC1 0
  (sigma_middle_TCC1-1 nil 3256039673
   ("" (skosimp* t)
    (("" (prop)
      (("1" (inst + "high!1") (("1" (assert) nil nil)) nil)
       ("2" (skosimp*)
        (("2" (inst + "high!1") (("2" (assert) nil nil)) nil)) nil)
       ("3" (skosimp*)
        (("3" (inst + "j!1") (("3" (assert) nil nil)) nil)) nil)
       ("4" (skosimp*)
        (("4" (inst + "j!2") (("4" (assert) nil nil)) nil)) nil))
      nil))
    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)
    (high!1 skolem-const-decl "T_high" sigma_2D 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]" sigma_2D nil)
    (T formal-subtype-decl nil sigma_2D nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma_2D nil)
    (T_low type-eq-decl nil sigma_2D nil))
   shostak))
(sigma_middle_TCC2 0
  (sigma_middle_TCC2-1 nil 3256039673
   ("" (skosimp*) (("" (inst + "i!1") (("" (assert) 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)
    (T_pred const-decl "[int -> boolean]" sigma_2D nil)
    (T formal-subtype-decl nil sigma_2D nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   shostak))
(sigma_middle 0
  (sigma_middle-1 nil 3256032001
   ("" (skosimp*)
    (("" (lemma "sigma_split")
      (("" (inst?)
        (("" (inst -1 "i!1")
          (("" (assert)
            (("" (rewrite "sigma_rew" -)
              (("" (assert)
                (("" (replace -1)
                  (("" (hide -1)
                    (("" (expand "sigma" 1 1)
                      (("" (ground)
                        (("" (expand "sigma")
                          ((""
                            (expand "+
")
                            (("" (propax) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sigma_split formula-decl nil sigma_2D nil)
    (sigma_rew formula-decl nil sigma_2D nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sigma def-decl "Vector" sigma_2D nil)
    (+ const-decl "Vector" vectors_2D nil)
    (real_ge_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)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (T_low type-eq-decl nil sigma_2D nil)
    (T_high type-eq-decl nil sigma_2D nil)
    (<= const-decl "bool" reals nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (T formal-subtype-decl nil sigma_2D nil)
    (T_pred const-decl "[int -> boolean]" sigma_2D 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))
   shostak))
(sigma_const 0
  (sigma_const-1 nil 3255975799
   ("" (skolem 1 (_ _ x))
    (("" (rewrite "high_low_rewrite")
      (("" (hide 2)
        (("" (skosimp*)
          (("" (prop)
            (("1" (expand "sigma") (("1" (assert) nil nil)) nil)
             ("2" (induct "n" 2)
              (("1" (rewrite "sigma_eq_arg")
                (("1" (assert)
                  (("1" (expand "const_vec")
                    (("1" (expand "*") (("1" (propax) nil nil)) nil))
                    nil))
                  nil)
                 ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil))
                nil)
               ("2" (hide 2)
                (("2" (skosimp*)
                  (("2" (expand "sigma" +)
                    (("2" (assert)
                      (("2" (replace -2)
                        (("2" (hide -2) (("2" (grind) 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)
   ((int_plus_int_is_int application-judgement "int" integers nil)
    (high_low_rewrite formula-decl nil sigma_2D 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]" sigma_2D nil)
    (T formal-subtype-decl nil sigma_2D nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma_2D nil)
    (T_low type-eq-decl nil sigma_2D nil)
    (pred type-eq-decl nil defined_types nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sigma def-decl "Vector" sigma_2D nil)
    (const_vec const-decl "Vector" vectors_2D nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (>= const-decl "bool" reals nil)
    (* const-decl "Vector" vectors_2D 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)
    (zero const-decl "Vector" vectors_2D 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" sigma_2D nil)
    (high!1 skolem-const-decl "T_high" sigma_2D 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 sigma_2D nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (scal_1 formula-decl nil vectors_2D nil)
    (sigma_eq_arg formula-decl nil sigma_2D nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (+ const-decl "Vector" vectors_2D nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
(sigma_zero 0
  (sigma_zero-1 nil 3255975799
   ("" (skosimp*)
    (("" (lemma "sigma_const")
      (("" (inst - "high!1" "low!1" "0")
        (("" (assert)
          (("" (case-replace "const_vec(0) = zero")
            (("1" (assert) nil nil)
             ("2" (invoke (hide ($+n)) (? * "sigma"))
              (("2" (expand "const_vec")
                (("2" (expand "zero") (("2" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sigma_const formula-decl nil sigma_2D nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (scal_zero formula-decl nil vectors_2D nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (const_vec const-decl "Vector" vectors_2D nil)
    (zero const-decl "Vector" vectors_2D nil)
    (T_low type-eq-decl nil sigma_2D nil)
    (T_high type-eq-decl nil sigma_2D nil)
    (<= const-decl "bool" reals nil)
    (T formal-subtype-decl nil sigma_2D nil)
    (T_pred const-decl "[int -> boolean]" sigma_2D 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)
    (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))
(sigma_scal 0
  (sigma_scal-1 nil 3255975799
   ("" (skolem 1 ("F" "a" _ _))
    (("" (rewrite "high_low_rewrite")
      (("" (hide 2)
        (("" (skosimp*)
          (("" (prop)
            (("1" (expand "sigma") (("1" (assert) nil nil)) nil)
             ("2" (induct "n" 2)
              (("1" (rewrite "sigma_eq_arg")
                (("1" (rewrite "sigma_eq_arg") nil nil)
                 ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil))
                nil)
               ("2" (hide 2)
                (("2" (skosimp*)
                  (("2" (expand "sigma" +)
                    (("2" (assert)
                      (("2" (replace -2 * lr)
                        (("2" (hide -2)
                          (("2" (apply-extensionality 1 :hide? t)
                            (("1" (grind) nil nil)
                             ("2" (grind) nil nil)
                             ("3" (grind) 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)
               ("4" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((high_low_rewrite formula-decl nil sigma_2D 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]" sigma_2D nil)
    (T formal-subtype-decl nil sigma_2D nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma_2D nil)
    (T_low type-eq-decl nil sigma_2D nil)
    (pred type-eq-decl nil defined_types nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sigma def-decl "Vector" sigma_2D nil)
    (* const-decl "Vector" vectors_2D nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (low!1 skolem-const-decl "T_low" sigma_2D nil)
    (high!1 skolem-const-decl "T_high" sigma_2D 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)
    (>= const-decl "bool" reals nil)
    (T_pred_lem formula-decl nil sigma_2D nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sigma_eq_arg formula-decl nil sigma_2D nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "Vector" vectors_2D nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (scal_zero formula-decl nil vectors_2D nil))
   nil))
(sigma_shift_T_TCC1 0
  (sigma_shift_T_TCC1-1 nil 3255975799
   ("" (skosimp* t)
    (("" (prop)
      (("1" (inst - "low!1") nil nil)
       ("2" (skosimp*)
        (("2" (inst + "j!1+z!1")
          (("1" (assert) nil nil) ("2" (inst?) nil nil)) nil))
        nil))
      nil))
    nil)
   ((low!1 skolem-const-decl "T_low" sigma_2D nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (j!1 skolem-const-decl "T" sigma_2D nil)
    (z!1 skolem-const-decl "int" sigma_2D nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props 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]" sigma_2D nil)
    (T formal-subtype-decl nil sigma_2D nil)
    (<= const-decl "bool" reals nil)
    (T_low type-eq-decl nil sigma_2D nil))
   nil))
(sigma_shift_T_TCC2 0
  (sigma_shift_T_TCC2-1 nil 3351939915
   ("" (skosimp* t)
    (("" (prop)
      (("1" (inst?) nil nil)
       ("2" (skosimp*)
        (("2" (inst + "z!1+j!1")
          (("1" (inst?) (("1" (assert) nil nil)) nil)
           ("2" (inst?) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((high!1 skolem-const-decl "T_high" sigma_2D nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (j!1 skolem-const-decl "T" sigma_2D nil)
    (z!1 skolem-const-decl "int" sigma_2D nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props 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]" sigma_2D nil)
    (T formal-subtype-decl nil sigma_2D nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma_2D nil))
   nil))
(sigma_shift_T_TCC3 0
  (sigma_shift_T_TCC3-1 nil 3352113941 ("" (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)
    (int_plus_int_is_int application-judgement "int" integers nil))
   nil))
(sigma_shift_T 0
  (sigma_shift_T-1 nil 3255975799
   ("" (skolem 1 ("F" _ _ "z"))
    (("" (rewrite "high_low_rewrite")
      (("1" (hide 2)
        (("1" (skosimp*)
          (("1" (prop)
            (("1" (expand "sigma") (("1" (assert) nil nil)) nil)
             ("2" (induct "n" 2)
              (("1" (skosimp*)
                (("1" (rewrite "sigma_eq_arg")
                  (("1" (rewrite "sigma_eq_arg")
                    (("1" (hide -1 2)
                      (("1" (use "T_pred_lem") (("1" (assert) nil nil))
                        nil))
                      nil))
                    nil)
                   ("2" (hide 2)
                    (("2" (inst?)
                      (("2" (use "T_pred_lem") (("2" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (hide 2)
                (("2" (skosimp*)
                  (("2" (expand "sigma" +) (("2" (assert) nil nil))
                    nil))
                  nil))
                nil)
               ("3" (skosimp*) nil nil)
               ("4" (hide-all-but 1)
                (("4" (skosimp* t)
                  (("4" (typepred "high!1")
                    (("4" (prop)
                      (("1" (inst + "high!1") nil nil)
                       ("2" (skosimp*)
                        (("2" (inst + "j!1") (("2" (assert) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("5" (hide -1 2 3)
                (("5" (skosimp* t)
                  (("5" (typepred "high!1")
                    (("5" (prop)
                      (("1" (inst + "high!1+z")
                        (("1" (assert) nil nil) ("2" (inst?) nil nil))
                        nil)
                       ("2" (skosimp*)
                        (("2" (inst + "j!1+z")
                          (("1" (assert) nil nil)
                           ("2" (inst?) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("6" (hide -1 2 3)
                (("6" (skosimp* t)
                  (("6" (assert)
                    (("6" (typepred "low!1")
                      (("6" (prop)
                        (("1" (inst?) nil nil)
                         ("2" (skosimp*)
                          (("2" (inst + "j!1+z")
                            (("1" (assert) nil nil)
                             ("2" (inst?) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("7" (assert) nil nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (skosimp*) nil nil)
       ("3" (hide 2)
        (("3" (skosimp* t)
          (("3" (hide -1 -4)
            (("3" (assert)
              (("3" (prop)
                (("1" (typepred "high!1")
                  (("1" (prop)
                    (("1" (assert) (("1" (inst?) nil nil)) nil)
                     ("2" (skosimp*)
                      (("2" (inst + "j!1+z")
                        (("1" (assert) nil nil) ("2" (inst?) nil nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (skosimp*)
                  (("2" (typepred "high!1")
                    (("2" (prop)
                      (("1" (inst?) nil nil)
                       ("2" (skosimp*)
                        (("2" (inst + "j!2+z")
                          (("1" (assert) nil nil)
                           ("2" (inst?) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("4" (hide 2)
        (("4" (skosimp* t)
          (("4" (hide -1)
            (("4" (inst?)
              (("4" (assert)
                (("4" (skosimp*)
                  (("4" (reveal -1)
                    (("4" (inst + "j!1+z")
                      (("1" (assert) nil nil) ("2" (inst?) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((int_plus_int_is_int application-judgement "int" integers nil)
    (high_low_rewrite formula-decl nil sigma_2D 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]" sigma_2D nil)
    (T formal-subtype-decl nil sigma_2D nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma_2D nil)
    (T_low type-eq-decl nil sigma_2D nil)
    (pred type-eq-decl nil defined_types nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sigma def-decl "Vector" sigma_2D nil)
--> --------------------

--> maximum size reached

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

quality97%

¤ Dauer der Verarbeitung: 0.33 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.