Quellcodebibliothek

^© Kompilation durch diese Firma

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

Verzeichnis trig_basic.prf Sprache: Lisp

Original von: PVS^©

(old_sigma
(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" old_sigma nil)
    (high!1 skolem-const-decl "T_high" old_sigma 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 old_sigma 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]" old_sigma nil)
    (T formal-subtype-decl nil old_sigma nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil old_sigma nil)
    (T_low type-eq-decl nil old_sigma 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" old_sigma nil)
    (T_high type-eq-decl nil old_sigma nil)
    (<= const-decl "bool" reals nil)
    (T formal-subtype-decl nil old_sigma nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T_pred const-decl "[int -> boolean]" old_sigma 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 old_sigma nil)
    (T_pred_lem formula-decl nil old_sigma 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]" old_sigma nil)
    (T formal-subtype-decl nil old_sigma nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil old_sigma nil)
    (T_low type-eq-decl nil old_sigma 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" old_sigma nil)
    (low!1 skolem-const-decl "T_low" old_sigma nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   shostak))
(sigma_TCC1 0
  (sigma_TCC1-1 nil 3255975799
   ("" (skosimp*) (("" (use "T_pred_lem") (("" (assert) nil nil)) nil))
    nil)
   ((T_pred_lem formula-decl nil old_sigma nil)
    (T_low type-eq-decl nil old_sigma nil)
    (<= const-decl "bool" reals nil)
    (T formal-subtype-decl nil old_sigma nil)
    (T_pred const-decl "[int -> boolean]" old_sigma 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 old_sigma 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))
   nil))
(sigma_TCC2 0
  (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)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (low!1 skolem-const-decl "T_low" old_sigma 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 old_sigma 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]" old_sigma nil)
    (T formal-subtype-decl nil old_sigma nil)
    (<= const-decl "bool" reals nil)
    (T_low type-eq-decl nil old_sigma nil)
    (T_high type-eq-decl nil old_sigma nil))
   nil))
(sigma_TCC3 0
  (sigma_TCC3-1 nil 3255975799
   ("" (skosimp*)
    (("" (assert)
      (("" (typepred "high!1")
        (("" (prop)
          (("1" (inst 4 "high!1") (("1" (assert) nil nil)) nil)
           ("2" (skosimp*)
            (("2" (inst 4 "j!1") (("2" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    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)
    (high!1 skolem-const-decl "T_high" old_sigma 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]" old_sigma nil)
    (T formal-subtype-decl nil old_sigma nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil old_sigma nil))
   nil))
(sigma_TCC4 0
  (sigma_TCC4-2 nil 3351941985
   ("" (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_TCC4-1 nil 3255975799
   ("" (skosimp*) (("" (assert) nil nil)) nil) nil nil))
(sigma_rew_TCC1 0
  (sigma_rew_TCC1-1 nil 3352522153
   ("" (skosimp*)
    (("" (assert)
      (("" (lemma "T_pred_lem")
        (("" (inst - "high!1" "low!1" "high!1") (("" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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]" old_sigma nil)
    (T formal-subtype-decl nil old_sigma nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil old_sigma nil)
    (T_low type-eq-decl nil old_sigma nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (T_pred_lem formula-decl nil old_sigma nil))
   nil))
(sigma_rew_TCC2 0
  (sigma_rew_TCC2-1 nil 3352522153
   ("" (skosimp*)
    (("" (typepred "high!1")
      (("" (prop)
        (("1" (inst + "high!1") (("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 old_sigma nil)
    (<= const-decl "bool" reals nil)
    (T formal-subtype-decl nil old_sigma nil)
    (T_pred const-decl "[int -> boolean]" old_sigma 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!1 skolem-const-decl "T_high" old_sigma 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))
   nil))
(sigma_rew 0
  (sigma_rew-1 nil 3352522445
   ("" (skosimp*) (("" (grind) nil nil)) nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sigma def-decl "real" old_sigma 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" old_sigma nil)
    (nn!1 skolem-const-decl "nat" old_sigma nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (low!1 skolem-const-decl "T_low" old_sigma nil)
    (T_low type-eq-decl nil old_sigma nil)
    (<= const-decl "bool" reals nil)
    (T formal-subtype-decl nil old_sigma 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]" old_sigma 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]" old_sigma nil)
    (T formal-subtype-decl nil old_sigma nil)
    (<= const-decl "bool" reals nil)
    (T_low type-eq-decl nil old_sigma 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" (assert)
      (("1" (expand "sigma") (("1" (propax) 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" (lift-if) (("2" (ground) nil nil)) 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" old_sigma nil)
    (nn!1 skolem-const-decl "nat" old_sigma nil)
    (rng!2 skolem-const-decl "nat" old_sigma nil)
    (low!1 skolem-const-decl "T_low" old_sigma nil)
    (nn!1 skolem-const-decl "nat" old_sigma nil)
    (rng!2 skolem-const-decl "nat" old_sigma nil)
    (T_pred_lem formula-decl nil old_sigma nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (sigma def-decl "real" old_sigma nil)
    (T_high type-eq-decl nil old_sigma 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]" old_sigma nil)
    (T formal-subtype-decl nil old_sigma nil)
    (<= const-decl "bool" reals nil)
    (T_low type-eq-decl nil old_sigma 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" old_sigma 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]" old_sigma nil)
    (T formal-subtype-decl nil old_sigma nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil old_sigma nil)
    (T_low type-eq-decl nil old_sigma 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" old_sigma 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]" old_sigma nil)
    (T formal-subtype-decl nil old_sigma nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil old_sigma nil)
    (T_low type-eq-decl nil old_sigma 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" (propax) 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 old_sigma nil)
    (T_high type-eq-decl nil old_sigma nil)
    (<= const-decl "bool" reals nil)
    (T formal-subtype-decl nil old_sigma nil)
    (T_pred const-decl "[int -> boolean]" old_sigma 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_plus_real_is_real application-judgement "real" reals 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 "real" old_sigma nil)
    (sigma_spl formula-decl nil old_sigma nil)
    (T_pred_lem formula-decl nil old_sigma nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (high!1 skolem-const-decl "T_high" old_sigma nil)
    (low!1 skolem-const-decl "T_low" old_sigma nil)
    (z!1 skolem-const-decl "int" old_sigma 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) nil nil)) nil))
        nil))
      nil))
    nil)
   ((sigma_split formula-decl nil old_sigma 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_minus_real_is_real application-judgement "real" reals nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (T_low type-eq-decl nil old_sigma nil)
    (T_high type-eq-decl nil old_sigma 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 old_sigma nil)
    (T_pred const-decl "[int -> boolean]" old_sigma 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) nil nil)) nil))
      nil))
    nil)
   ((sigma_diff formula-decl nil old_sigma nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (int_minus_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 old_sigma nil)
    (T_high type-eq-decl nil old_sigma 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 old_sigma nil)
    (T_pred const-decl "[int -> boolean]" old_sigma 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") (("" (propax) nil nil)) nil)) nil))
    nil)
   ((sigma def-decl "real" old_sigma 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 old_sigma nil)
    (T_low type-eq-decl nil old_sigma nil)
    (<= const-decl "bool" reals nil)
    (T formal-subtype-decl nil old_sigma nil)
    (T_pred const-decl "[int -> boolean]" old_sigma 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 old_sigma 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" old_sigma 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]" old_sigma nil)
    (T formal-subtype-decl nil old_sigma nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil old_sigma nil)
    (T_low type-eq-decl nil old_sigma 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 old_sigma 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_plus_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sigma_eq_arg formula-decl nil old_sigma nil)
    (T_low type-eq-decl nil old_sigma nil)
    (T_high type-eq-decl nil old_sigma 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 old_sigma nil)
    (T_pred const-decl "[int -> boolean]" old_sigma 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" old_sigma 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]" old_sigma nil)
    (T formal-subtype-decl nil old_sigma nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil old_sigma nil)
    (T_low type-eq-decl nil old_sigma 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 old_sigma nil)
    (T_high type-eq-decl nil old_sigma nil)
    (<= const-decl "bool" reals nil)
    (T formal-subtype-decl nil old_sigma nil)
    (T_pred const-decl "[int -> boolean]" old_sigma 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 old_sigma 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)
        (("" (lift-if)
          (("" (ground)
            (("" (expand "sigma") (("" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((sigma def-decl "real" old_sigma 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]" old_sigma nil)
    (T formal-subtype-decl nil old_sigma nil)
    (<= const-decl "bool" reals nil)
    (T_low type-eq-decl nil old_sigma nil)
    (T_high type-eq-decl nil old_sigma nil)
    (real_gt_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)
    (real_plus_real_is_real application-judgement "real" reals 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" old_sigma 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]" old_sigma nil)
    (T formal-subtype-decl nil old_sigma nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil old_sigma nil)
    (T_low type-eq-decl nil old_sigma 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]" old_sigma nil)
    (T formal-subtype-decl nil old_sigma 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)
                    (("" (assert)
                      (("" (expand "sigma" 1 1)
                        (("" (lift-if)
                          (("" (ground)
                            (("" (expand "sigma")
                              (("" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sigma_split formula-decl nil old_sigma nil)
    (sigma_rew formula-decl nil old_sigma nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sigma def-decl "real" old_sigma nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_plus_real_is_real application-judgement "real" reals 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 old_sigma nil)
    (T_high type-eq-decl nil old_sigma 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 old_sigma nil)
    (T_pred const-decl "[int -> boolean]" old_sigma 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) nil nil)
                 ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil))
                nil)
               ("2" (hide 2)
                (("2" (skosimp*)
                  (("2" (expand "sigma" +) (("2" (assert) 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)
   ((high_low_rewrite formula-decl nil old_sigma 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]" old_sigma nil)
    (T formal-subtype-decl nil old_sigma nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil old_sigma nil)
    (T_low type-eq-decl nil old_sigma nil)
    (pred type-eq-decl nil defined_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sigma def-decl "real" old_sigma nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (>= const-decl "bool" reals nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (low!1 skolem-const-decl "T_low" old_sigma nil)
    (high!1 skolem-const-decl "T_high" old_sigma 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 old_sigma nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (sigma_eq_arg formula-decl nil old_sigma 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*) (("" (rewrite "sigma_const") nil nil)) nil)
   ((mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (int_times_even_is_even application-judgement "even_int" integers
     nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sigma_const formula-decl nil old_sigma 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]" old_sigma nil)
    (T formal-subtype-decl nil old_sigma nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil old_sigma nil)
    (T_low type-eq-decl nil old_sigma 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) 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)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (high_low_rewrite formula-decl nil old_sigma 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]" old_sigma nil)
    (T formal-subtype-decl nil old_sigma nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil old_sigma nil)
    (T_low type-eq-decl nil old_sigma nil)
    (pred type-eq-decl nil defined_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sigma def-decl "real" old_sigma nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (low!1 skolem-const-decl "T_low" old_sigma nil)
    (high!1 skolem-const-decl "T_high" old_sigma 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 old_sigma nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sigma_eq_arg formula-decl nil old_sigma nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_plus_real_is_real application-judgement "real" reals 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_bound 0
  (sigma_bound-1 nil 3255975799
   ("" (skolem 1 ("B" "F" _ _))
    (("" (rewrite "high_low_rewrite")
      (("" (hide 2)
        (("" (skosimp*)
          (("" (prop)
            (("1" (expand "sigma") (("1" (assert) nil nil)) nil)
             ("2" (induct "n" 2)
              (("1" (skosimp*)
                (("1" (rewrite "sigma_eq_arg")
                  (("1" (inst?) (("1" (assert) nil 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 "sigma" +)
                    (("2" (prop)
                      (("1" (inst?) (("1" (assert) nil nil)) nil)
                       ("2" (skosimp*)
                        (("2" (inst?) (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("3" (skosimp*)
                (("3" (hide-all-but (1 2))
                  (("3" (typepred "n!2")
                    (("3" (assert)
                      (("3" (typepred "high!1")
                        (("3" (prop)
                          (("1" (inst + "high!1") nil nil)
                           ("2" (skosimp*)
                            (("2" (inst + "j!1")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("4" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((int_minus_int_is_int application-judgement "int" integers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (high_low_rewrite formula-decl nil old_sigma 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]" old_sigma nil)
    (T formal-subtype-decl nil old_sigma nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil old_sigma nil)
    (T_low type-eq-decl nil old_sigma 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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (>= const-decl "bool" reals nil)
    (sigma def-decl "real" old_sigma nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (low!1 skolem-const-decl "T_low" old_sigma nil)
    (high!1 skolem-const-decl "T_high" old_sigma nil)
    (subrange type-eq-decl nil integers nil)
    (F skolem-const-decl "[T -> real]" old_sigma nil)
    (B skolem-const-decl "real" old_sigma nil)
    (subrange_induction formula-decl nil subrange_inductions nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sigma_eq_arg formula-decl nil old_sigma nil)
    (T_pred_lem formula-decl nil old_sigma nil)
    (int_plus_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_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
(sigma_abs 0
  (sigma_abs-1 nil 3255975799
   ("" (skolem 1 ("F" _ _))
    (("" (rewrite "high_low_rewrite")
      (("" (hide 2)
        (("" (skosimp*)
          (("" (prop)
            (("1" (expand "sigma")
              (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil)
             ("2" (induct "n" 2)
              (("1" (rewrite "sigma_eq_arg")
                (("1" (rewrite "sigma_eq_arg") (("1" (assert) nil nil))
                  nil)
                 ("2" (hide 2)
                  (("2" (use "T_pred_lem") (("2" (assert) nil nil))
                    nil))
                  nil))
                nil)
               ("2" (hide 2)
                (("2" (skosimp*)
                  (("2" (expand "sigma" +)
                    (("2" (lemma "triangle")
                      (("2" (inst?) (("2" (assert) 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)
   ((high_low_rewrite formula-decl nil old_sigma 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]" old_sigma nil)
    (T formal-subtype-decl nil old_sigma nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil old_sigma nil)
    (T_low type-eq-decl nil old_sigma nil)
    (pred type-eq-decl nil defined_types nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (sigma def-decl "real" old_sigma nil)
    (low!1 skolem-const-decl "T_low" old_sigma nil)
    (high!1 skolem-const-decl "T_high" old_sigma 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 old_sigma nil)
    (sigma_eq_arg formula-decl nil old_sigma nil)
    (triangle formula-decl nil real_props nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_plus_real_is_real application-judgement "real" reals 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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
(sigma_ge_0_TCC1 0
  (sigma_ge_0_TCC1-1 nil 3255975799
   ("" (skosimp* t)
    (("" (prop)
      (("1" (use "T_pred_lem") (("1" (assert) nil nil)) nil)
       ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil)
       ("3" (use "T_pred_lem") (("3" (assert) nil nil)) nil)
       ("4" (use "T_pred_lem") (("4" (assert) nil nil)) nil))
      nil))
    nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (T_pred_lem formula-decl nil old_sigma 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]" old_sigma nil)
    (T formal-subtype-decl nil old_sigma nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil old_sigma nil)
    (T_low type-eq-decl nil old_sigma nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (subrange type-eq-decl nil integers nil))
   nil))
(sigma_ge_0 0
  (sigma_ge_0-1 nil 3255975799
   ("" (skolem 1 ("F" _ _))
    (("" (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" (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 "sigma" +)
                    (("2" (prop)
                      (("1" (inst?) (("1" (assert) 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 old_sigma 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)
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.70 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.