Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei:   Sprache: Lisp

Original von: PVS©

(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" (assertnil nil)) nil))
              nil)
             ("2" (skosimp*)
              (("2" (lemma "connected_domain")
                (("2" (inst - "j!1" "high!1" "z!1")
                  (("2" (assertnil nil)) nil))
                nil))
              nil)
             ("3" (skosimp*)
              (("3" (lemma "connected_domain")
                (("3" (inst - "low!1" "j!1" "z!1")
                  (("3" (assertnil nil)) nil))
                nil))
              nil)
             ("4" (skosimp*)
              (("4" (lemma "connected_domain")
                (("4" (inst - "low!1" "j!2" "z!1")
                  (("1" (assertnil nil)
                   ("2" (lemma "connected_domain")
                    (("2" (inst - "j!1" "j!2" "low!1")
                      (("2" (assertnil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ((low!1 skolem-const-decl "T_low" sigma nil)
          (high!1 skolem-const-decl "T_high" 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 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]" sigma nil)
          (T formal-subtype-decl nil sigma nil)
          (<= const-decl "bool" reals nil)
          (T_high type-eq-decl nil sigma nil)
          (T_low type-eq-decl nil sigma nil))
         shostak))
       (high_low_rewrite_TCC1 0
        (high_low_rewrite_TCC1-1 nil 3352229091
         ("" (skosimp*)
          (("" (inst + "high!1")
            (("1" (assertnil nil)
             ("2" (use "T_pred_lem") (("2" (assertnil nil)) nil))
            nil))
          nil)
         ((high!1 skolem-const-decl "T_high" sigma nil)
          (T_high type-eq-decl nil sigma nil)
          (<= const-decl "bool" reals nil)
          (T formal-subtype-decl nil sigma nil)
          (OR const-decl "[bool, bool -> bool]" booleans nil)
          (bool nonempty-type-eq-decl nil booleans nil)
          (T_pred const-decl "[int -> boolean]" 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 sigma nil)
          (T_pred_lem formula-decl nil sigma nil))
         nil))
       (high_low_rewrite 0
        (high_low_rewrite-1 nil 3352228842
         ("" (skosimp*)
          (("" (inst?)
            (("" (prop) (("" (inst?) (("" (assertnil 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 nil)
          (T formal-subtype-decl nil sigma nil)
          (<= const-decl "bool" reals nil)
          (T_high type-eq-decl nil sigma nil)
          (T_low type-eq-decl nil 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" sigma nil)
          (low!1 skolem-const-decl "T_low" sigma 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" (assertnil nil)
                     ("2" (prop)
                      (("2" (skosimp*)
                        (("2" (lemma "connected_domain")
                          (("2" (assert)
                            (("2" (inst - "j!2" "j!1" "low!1")
                              (("2" (assertnil 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 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 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 nil)
          (T formal-subtype-decl nil sigma nil)
          (<= const-decl "bool" reals nil)
          (T_low type-eq-decl nil sigma nil)
          (T_high type-eq-decl nil sigma nil))
         nil)
        (sigma_TCC1-1 nil 3255975799
         ("" (skosimp*)
          (("" (use "T_pred_lem") (("" (assertnil nil)) nil)) nil)
         nil nil))
       (sigma_TCC2 0
        (sigma_TCC2-2 nil 3403452083
         ("" (skosimp*)
          (("" (typepred "high!1")
            (("" (assert)
              (("" (prop)
                (("1" (inst + "high!1") (("1" (assertnil nil)) nil)
                 ("2" (skosimp*)
                  (("2" (typepred "j!1")
                    (("2" (inst + "j!1") (("2" (assertnil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ((T_high type-eq-decl nil sigma nil)
          (<= const-decl "bool" reals nil)
          (T formal-subtype-decl nil sigma nil)
          (T_pred const-decl "[int -> boolean]" 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)
          (real_le_is_total_order name-judgement "(total_order?[real])"
           real_props nil)
          (high!1 skolem-const-decl "T_high" 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))
         nil)
        (sigma_TCC2-1 nil 3255975799
         ("" (skosimp* t)
          (("" (assert)
            (("" (skosimp*)
              (("" (typepred "j!1")
                (("" (lemma "connected_domain")
                  (("" (inst - "low!1" "j!1" "high!1")
                    (("1" (assertnil nil)
                     ("2" (prop)
                      (("2" (skosimp*)
                        (("2" (lemma "connected_domain")
                          (("2" (assert)
                            (("2" (inst - "j!2" "j!1" "low!1")
                              (("2" (assertnil 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))
       (sigma2_TCC1 0
        (sigma2_TCC1-1 nil 3403451849
         ("" (skosimp*)
          (("" (typepred "low!1")
            (("" (assert)
              (("" (skosimp*)
                (("" (replace -2)
                  (("" (typepred "j!1")
                    (("" (typepred "high!1")
                      (("" (assert)
                        (("" (skosimp*)
                          (("" (lemma "connected_domain")
                            (("" (inst - "j!1" "j!2" "low!1")
                              (("" (assertnil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ((T_low type-eq-decl nil sigma nil)
          (<= const-decl "bool" reals nil)
          (T formal-subtype-decl nil sigma nil)
          (T_pred const-decl "[int -> boolean]" 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)
          (real_le_is_total_order name-judgement "(total_order?[real])"
           real_props nil)
          (connected_domain formula-decl nil sigma nil)
          (integer nonempty-type-from-decl nil integers nil)
          (T_high type-eq-decl nil sigma nil)
          (real_gt_is_strict_total_order name-judgement
           "(strict_total_order?[real])" real_props 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" (assertnil nil)) nil))
                nil)
               ("3" (expand "sigma" 2 1) (("3" (propax) nil nil)) nil))
              nil))
            nil))
          nil)
         ((sigma def-decl "real" 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_plus_real_is_real application-judgement "real" reals
           nil))
         shostak))
       (sigma_rew2 0
        (sigma_rew2-1 nil 3403459500
         ("" (skosimp*)
          ((""
            (case "FORALL (rng: nat): T_pred(low!1+rng) IMPLIES
                              sigma(low!1, low!1+rng, F!1) = sigma2(low!1, low!1+rng, F!1)")
            (("1" (inst - "high!1-low!1")
              (("1" (assert)
                (("1" (typepred "high!1")
                  (("1" (assert)
                    (("1" (skosimp*)
                      (("1" (typepred "j!1")
                        (("1" (typepred "low!1")
                          (("1" (lemma "connected_domain")
                            (("1" (inst - "low!1" "j!1" "high!1")
                              (("1"
                                (assert)
                                (("1"
                                  (expand "sigma")
                                  (("1"
                                    (expand "sigma2")
                                    (("1" (propax) nil nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (assert)
                                (("2"
                                  (skosimp*)
                                  (("2"
                                    (lemma "connected_domain")
                                    (("2"
                                      (inst - "j!2" "j!1" "low!1")
                                      (("2"
                                        (assert)
                                        (("2"
                                          (expand "sigma")
                                          (("2"
                                            (expand "sigma2")
                                            (("2" (propax) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (expand "sigma")
                (("2" (expand "sigma2") (("2" (assertnil nil)) nil))
                nil))
              nil)
             ("2" (hide 2)
              (("2" (induct "rng")
                (("1" (assert)
                  (("1" (flatten)
                    (("1" (expand "sigma")
                      (("1" (expand "sigma")
                        (("1" (expand "sigma2")
                          (("1" (propax) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (skosimp*)
                  (("2" (assert)
                    (("2" (expand "sigma" 1)
                      (("2" (expand "sigma2" 1)
                        (("2" (assert)
                          (("2" (hide 2)
                            (("2" (typepred "low!1")
                              (("2"
                                (typepred "j!1")
                                (("2"
                                  (assert)
                                  (("2"
                                    (prop)
                                    (("1"
                                      (lemma "connected_domain")
                                      (("1"
                                        (inst
                                         -
                                         "low!1"
                                         "j!1+1+low!1"
                                         "j!1+low!1")
                                        (("1" (assertnil nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (skosimp*)
                                      (("2"
                                        (lemma "connected_domain")
                                        (("2"
                                          (inst
                                           -
                                           "j!2"
                                           "j!1+1+low!1"
                                           "j!1+low!1")
                                          (("2" (assertnil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("3" (hide 2) (("3" (skosimp*) nil nil)) nil))
                nil))
              nil)
             ("3" (skosimp*) nil nil))
            nil))
          nil)
         ((sigma2 def-decl "real" sigma nil)
          (sigma def-decl "real" sigma nil)
          (T_high type-eq-decl nil sigma nil)
          (= const-decl "[T, T -> boolean]" equalities nil)
          (T_low type-eq-decl nil sigma nil)
          (<= const-decl "bool" reals nil)
          (T formal-subtype-decl nil sigma nil)
          (OR const-decl "[bool, bool -> bool]" 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 nil)
          (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
          (nat nonempty-type-eq-decl nil naturalnumbers nil)
          (>= const-decl "bool" reals nil)
          (bool nonempty-type-eq-decl nil booleans nil)
          (int nonempty-type-eq-decl nil integers nil)
          (integer_pred const-decl "[rational -> boolean]" integers
                        nil)
          (rational nonempty-type-from-decl nil rationals nil)
          (rational_pred const-decl "[real -> boolean]" rationals nil)
          (real nonempty-type-from-decl nil reals nil)
          (real_pred const-decl "[number_field -> boolean]" reals nil)
          (number_field nonempty-type-from-decl nil number_fields nil)
          (number_field_pred const-decl "[number -> boolean]"
           number_fields nil)
          (boolean nonempty-type-decl nil booleans nil)
          (number nonempty-type-decl nil numbers nil)
          (int_plus_int_is_int application-judgement "int" integers
           nil)
          (real_gt_is_strict_total_order name-judgement
           "(strict_total_order?[real])" real_props nil)
          (connected_domain formula-decl nil sigma nil)
          (real_le_is_total_order name-judgement "(total_order?[real])"
           real_props nil)
          (integer nonempty-type-from-decl nil integers nil)
          (NOT const-decl "[bool -> bool]" booleans nil)
          (low!1 skolem-const-decl "T_low" sigma nil)
          (high!1 skolem-const-decl "T_high" sigma nil)
          (- const-decl "[numfield, numfield -> numfield]"
             number_fields nil)
          (int_minus_int_is_int application-judgement "int" integers
           nil)
          (real_ge_is_total_order name-judgement "(total_order?[real])"
           real_props nil)
          (pred type-eq-decl nil defined_types nil)
          (nat_induction formula-decl nil naturalnumbers nil)
          (posint_plus_nnint_is_posint application-judgement "posint"
           integers nil)
          (nnint_plus_posint_is_posint application-judgement "posint"
           integers nil))
         nil))
       (sigma_spl_TCC1 0
        (sigma_spl_TCC1-1 nil 3255975799
         ("" (skosimp*)
          (("" (inst + "low!1 + nn!1 + rng!1") (("" (assertnil nil))
            nil))
          nil)
         nil nil))
       (sigma_spl_TCC2 0
        (sigma_spl_TCC2-1 nil 3255975799
         ("" (skosimp*)
          (("" (inst + "low!1 + nn!1 + rng!1") (("" (assertnil nil))
            nil))
          nil)
         ((int_plus_int_is_int application-judgement "int" integers
           nil)
          (rng!1 skolem-const-decl "nat" sigma nil)
          (nn!1 skolem-const-decl "nat" sigma nil)
          (nat nonempty-type-eq-decl nil naturalnumbers nil)
          (>= const-decl "bool" reals nil)
          (low!1 skolem-const-decl "T_low" sigma nil)
          (T_low type-eq-decl nil sigma nil)
          (<= const-decl "bool" reals nil)
          (T formal-subtype-decl nil 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]" 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" (assertnil nil)) nil))
              nil)
             ("2" (skosimp*)
              (("2" (inst + "j!1") (("2" (assertnil 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 nil)
          (T formal-subtype-decl nil sigma nil)
          (<= const-decl "bool" reals nil)
          (T_low type-eq-decl nil 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" (assertnil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("3" (hide 2)
            (("3" (skosimp*)
              (("3" (inst + "low!1+nn!1")
                (("1" (assertnil nil)
                 ("2" (lemma "T_pred_lem")
                  (("2" (inst?)
                    (("2" (inst - "low!1+nn!1+rng!2" "low!1")
                      (("1" (assertnil nil) ("2" (assertnil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("4" (hide 2)
            (("4" (skosimp*)
              (("4" (inst + "low!1+nn!1+rng!2")
                (("4" (assertnil nil)) nil))
              nil))
            nil)
           ("5" (hide 2) (("5" (skosimp*) nil nil)) nil))
          nil)
         ((low!1 skolem-const-decl "T_low" sigma nil)
          (nn!1 skolem-const-decl "nat" sigma nil)
          (rng!2 skolem-const-decl "nat" sigma nil)
          (low!1 skolem-const-decl "T_low" sigma nil)
          (nn!1 skolem-const-decl "nat" sigma nil)
          (rng!2 skolem-const-decl "nat" sigma nil)
          (T_pred_lem formula-decl nil 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" sigma nil)
          (T_high type-eq-decl nil 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]" sigma nil)
          (T formal-subtype-decl nil sigma nil)
          (<= const-decl "bool" reals nil)
          (T_low type-eq-decl nil 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" (assertnil nil)) nil)) nil)
             ("4" (skosimp*)
              (("4" (inst + "j!2") (("4" (assertnil nil)) nil)) nil))
            nil))
          nil)
         ((high!1 skolem-const-decl "T_high" 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]" sigma nil)
          (T formal-subtype-decl nil sigma nil)
          (<= const-decl "bool" reals nil)
          (T_high type-eq-decl nil sigma nil)
          (T_low type-eq-decl nil sigma nil))
         nil))
       (sigma_split_TCC2 0
        (sigma_split_TCC2-1 nil 3351939915
         ("" (skosimp* t)
          (("" (assert)
            (("" (prop)
              (("1" (inst + "low!1") (("1" (assertnil nil)) nil)
               ("2" (skosimp*)
                (("2" (inst + "j!1") (("2" (assertnil nil)) nil))
                nil)
               ("3" (skosimp*)
                (("3" (inst + "low!1") (("3" (assertnil nil)) nil))
                nil)
               ("4" (skosimp*)
                (("4" (inst + "j!1") (("4" (assertnil 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 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 nil)
          (T formal-subtype-decl nil sigma nil)
          (<= const-decl "bool" reals nil)
          (T_high type-eq-decl nil sigma nil)
          (T_low type-eq-decl nil sigma nil))
         nil))
       (sigma_split 0
        (sigma_split-1 nil 3255975799
         ("" (skosimp*)
          (("" (case "high!1)
            (("1" (expand "sigma") (("1" (assertnil 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" (assertnil nil))
                        nil))
                      nil))
                    nil)
                   ("2" (assertnil nil) ("3" (assertnil nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ((T_low type-eq-decl nil sigma nil)
          (T_high type-eq-decl nil sigma nil)
          (<= const-decl "bool" reals nil)
          (T formal-subtype-decl nil sigma nil)
          (T_pred const-decl "[int -> boolean]" 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" sigma nil)
          (sigma_spl formula-decl nil sigma nil)
          (T_pred_lem formula-decl nil sigma nil)
          (nat nonempty-type-eq-decl nil naturalnumbers nil)
          (high!1 skolem-const-decl "T_high" sigma nil)
          (low!1 skolem-const-decl "T_low" sigma nil)
          (z!1 skolem-const-decl "int" 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") (("" (assertnil nil)) nil)) nil))
            nil))
          nil)
         ((sigma_split formula-decl nil 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 sigma nil)
          (T_high type-eq-decl nil 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 sigma nil)
          (T_pred const-decl "[int -> boolean]" 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")
              (("" (assertnil nil)) nil))
            nil))
          nil)
         ((sigma_diff formula-decl nil 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 sigma nil)
          (T_high type-eq-decl nil 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 sigma nil)
          (T_pred const-decl "[int -> boolean]" 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" sigma nil)) nil))
       (sigma_first_TCC1 0
        (sigma_first_TCC1-1 nil 3255975799
         ("" (skosimp*)
          (("" (use "T_pred_lem") (("" (assertnil nil)) nil)) nil)
         ((T_pred_lem formula-decl nil sigma nil)
          (T_low type-eq-decl nil sigma nil)
          (<= const-decl "bool" reals nil)
          (T formal-subtype-decl nil sigma nil)
          (T_pred const-decl "[int -> boolean]" 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 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" (assertnil nil)) nil)
             ("2" (skosimp*)
              (("2" (inst + "j!1") (("2" (assertnil nil)) nil)) nil)
             ("3" (inst + "low!1") (("3" (assertnil nil)) nil)
             ("4" (skosimp*)
              (("4" (inst + "j!1") (("4" (assertnil 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 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 nil)
          (T formal-subtype-decl nil sigma nil)
          (<= const-decl "bool" reals nil)
          (T_high type-eq-decl nil sigma nil)
          (T_low type-eq-decl nil sigma nil))
         nil))
       (sigma_first 0
        (sigma_first-1 nil 3255975799
         ("" (skosimp*)
          (("" (lemma "sigma_split")
            (("" (inst?)
              (("" (inst -1 "low!1")
                (("" (rewrite "sigma_eq_arg") (("" (assertnil nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ((sigma_split formula-decl nil 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 sigma nil)
          (T_low type-eq-decl nil sigma nil)
          (T_high type-eq-decl nil 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 sigma nil)
          (T_pred const-decl "[int -> boolean]" 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" (assertnil nil)) nil)
             ("2" (skosimp*)
              (("2" (inst + "high!1") (("2" (assertnil nil)) nil))
              nil)
             ("3" (skosimp*)
              (("3" (inst + "j!1") (("3" (assertnil nil)) nil)) nil)
             ("4" (skosimp*)
              (("4" (inst + "j!2") (("4" (assertnil 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 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 nil)
          (T formal-subtype-decl nil sigma nil)
          (<= const-decl "bool" reals nil)
          (T_high type-eq-decl nil sigma nil)
          (T_low type-eq-decl nil sigma nil))
         nil)
        (sigma_last_TCC1-1 nil 3255975799
         ("" (skosimp*)
          (("" (typepred "high!1")
            (("" (skosimp*)
              (("" (inst + "j!1") (("" (assertnil nil)) nil)) nil))
            nil))
          nil)
         nil nil))
       (sigma_last_TCC2 0
        (sigma_last_TCC2-1 nil 3351939915
         ("" (skosimp*)
          (("" (use "T_pred_lem") (("" (assertnil nil)) nil)) nil)
         ((T_pred_lem formula-decl nil sigma nil)
          (T_high type-eq-decl nil sigma nil)
          (<= const-decl "bool" reals nil)
          (T formal-subtype-decl nil sigma nil)
          (T_pred const-decl "[int -> boolean]" 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 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") (("" (assertnil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ((sigma def-decl "real" 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]" sigma nil)
          (T formal-subtype-decl nil sigma nil)
          (<= const-decl "bool" reals nil)
          (T_low type-eq-decl nil sigma nil)
          (T_high type-eq-decl nil 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" (assertnil nil)) nil)
             ("2" (skosimp*)
              (("2" (inst + "high!1") (("2" (assertnil nil)) nil))
              nil)
             ("3" (skosimp*)
              (("3" (inst + "j!1") (("3" (assertnil nil)) nil)) nil)
             ("4" (skosimp*)
              (("4" (inst + "j!2") (("4" (assertnil 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 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 nil)
          (T formal-subtype-decl nil sigma nil)
          (<= const-decl "bool" reals nil)
          (T_high type-eq-decl nil sigma nil)
          (T_low type-eq-decl nil sigma nil))
         shostak))
       (sigma_middle_TCC2 0
        (sigma_middle_TCC2-1 nil 3256039673
         ("" (skosimp*)
          (("" (inst + "i!1") (("" (assertnil 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 nil)
          (T formal-subtype-decl nil 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")
                                    (("" (assertnil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ((sigma_split formula-decl nil sigma nil)
          (sigma_rew formula-decl nil sigma nil)
          (real_gt_is_strict_total_order name-judgement
           "(strict_total_order?[real])" real_props nil)
          (sigma def-decl "real" 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 sigma nil)
          (T_high type-eq-decl nil 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 sigma nil)
          (T_pred const-decl "[int -> boolean]" 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" (assertnil nil)) nil)
                   ("2" (induct "n" 2)
                    (("1" (rewrite "sigma_eq_arg")
                      (("1" (assertnil nil)
                       ("2" (use "T_pred_lem") (("2" (assertnil nil))
                        nil))
                      nil)
                     ("2" (hide 2)
                      (("2" (skosimp*)
                        (("2" (expand "sigma" +)
                          (("2" (assertnil nil)) nil))
                        nil))
                      nil)
                     ("3" (hide 3)
                      (("3" (skosimp*)
                        (("3" (inst + "high!1")
                          (("1" (assertnil nil)
                           ("2" (use "T_pred_lem")
                            (("2" (assertnil nil)) nil))
                          nil))
                        nil))
                      nil)
                     ("4" (assertnil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ((high_low_rewrite formula-decl nil 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]" sigma nil)
          (T formal-subtype-decl nil sigma nil)
          (<= const-decl "bool" reals nil)
          (T_high type-eq-decl nil sigma nil)
          (T_low type-eq-decl nil sigma nil)
          (pred type-eq-decl nil defined_types nil)
          (= const-decl "[T, T -> boolean]" equalities nil)
          (sigma def-decl "real" 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" sigma nil)
          (high!1 skolem-const-decl "T_high" 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 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 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 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]" sigma nil)
          (T formal-subtype-decl nil sigma nil)
          (<= const-decl "bool" reals nil)
          (T_high type-eq-decl nil sigma nil)
          (T_low type-eq-decl nil 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" (assertnil nil)) nil)
                   ("2" (induct "n" 2)
                    (("1" (rewrite "sigma_eq_arg")
                      (("1" (rewrite "sigma_eq_arg"nil nil)
                       ("2" (use "T_pred_lem") (("2" (assertnil nil))
                        nil))
                      nil)
                     ("2" (hide 2)
                      (("2" (skosimp*)
                        (("2" (expand "sigma" +)
                          (("2" (assertnil nil)) nil))
                        nil))
                      nil)
                     ("3" (skosimp*)
                      (("3" (inst + "high!1")
                        (("1" (assertnil nil)
                         ("2" (use "T_pred_lem")
--> --------------------

--> maximum size reached

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

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


Bot Zugriff



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik