| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/vectors/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 123 kB |
|
Quelle sigma_2D.prfSprache: Lisp |
|||||||||||||||
|
(sigma_2D (T_pred_lem 0 (T_pred_lem-1 nil 3352120046 ("" (skosimp* t) (("" (prop) (("1" (lemma "connected_domain") (("1" (inst - "low!1" "high!1" "z!1") (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "connected_domain") (("2" (inst - "j!1" "high!1" "z!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (lemma "connected_domain") (("3" (inst - "low!1" "j!1" "z!1") (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (lemma "connected_domain") (("4" (inst - "low!1" "j!2" "z!1") (("1" (assert) nil nil) ("2" (lemma "connected_domain") (("2" (inst - "j!1" "j!2" "low!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((low!1 skolem-const-decl "T_low" sigma_2D nil) (high!1 skolem-const-decl "T_high" sigma_2D nil) (integer nonempty-type-from-decl nil integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (connected_domain formula-decl nil sigma_2D nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil)) shostak)) (high_low_rewrite_TCC1 0 (high_low_rewrite_TCC1-1 nil 3352229091 ("" (skosimp*) (("" (inst + "high!1") (("1" (assert) nil nil) ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil)) nil)) nil) ((high!1 skolem-const-decl "T_high" sigma_2D nil) (T_high type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil sigma_2D nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (T_low type-eq-decl nil sigma_2D nil) (T_pred_lem formula-decl nil sigma_2D nil)) nil)) (high_low_rewrite 0 (high_low_rewrite-1 nil 3352228842 ("" (skosimp*) (("" (inst?) (("" (prop) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (high!1 skolem-const-decl "T_high" sigma_2D nil) (low!1 skolem-const-decl "T_low" sigma_2D nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (sigma_TCC1 0 (sigma_TCC1-2 nil 3403452046 ("" (skosimp* t) (("" (assert) (("" (skosimp*) (("" (typepred "j!1") (("" (lemma "connected_domain") (("" (inst - "low!1" "j!1" "high!1") (("1" (assert) nil nil) ("2" (prop) (("2" (skosimp*) (("2" (lemma "connected_domain") (("2" (assert) (("2" (inst - "j!2" "j!1" "low!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (low!1 skolem-const-decl "T_low" sigma_2D nil) (integer nonempty-type-from-decl nil integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (connected_domain formula-decl nil sigma_2D nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma_2D nil) (T_high type-eq-decl nil sigma_2D nil)) nil) (sigma_TCC1-1 nil 3255975799 ("" (skosimp*) (("" (use "T_pred_lem") (("" (assert) nil nil)) nil)) nil) nil nil)) (sigma_TCC2 0 (sigma_TCC2-2 nil 3403452083 ("" (skosimp*) (("" (typepred "high!1") (("" (assert) (("" (prop) (("1" (inst + "high!1") (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (typepred "j!1") (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T_high type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil sigma_2D nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (high!1 skolem-const-decl "T_high" sigma_2D nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil) (sigma_TCC2-1 nil 3255975799 ("" (skosimp* t) (("" (assert) (("" (skosimp*) (("" (typepred "j!1") (("" (lemma "connected_domain") (("" (inst - "low!1" "j!1" "high!1") (("1" (assert) nil nil) ("2" (prop) (("2" (skosimp*) (("2" (lemma "connected_domain") (("2" (assert) (("2" (inst - "j!2" "j!1" "low!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil nil)) (sigma_TCC3 0 (sigma_TCC3-1 nil 3255975799 ("" (skosimp*) (("" (grind) nil nil)) nil) ((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (minus_int_is_int application-judgement "int" integers nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (sigma_rew_TCC1 0 (sigma_rew_TCC1-1 nil 3411477956 ("" (skosimp*) (("" (assert) (("" (typepred "low!1") (("" (typepred "high!1") (("" (ground) (("" (skosimp*) (("" (assert) (("" (typepred "j!1") (("" (typepred "j!2") (("" (lemma "connected_domain") (("" (inst - "j!1" "j!2" "low!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (T_high type-eq-decl nil sigma_2D nil) (connected_domain formula-decl nil sigma_2D nil) (integer nonempty-type-from-decl nil integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma_2D nil)) nil)) (sigma_rew 0 (sigma_rew-1 nil 3352522445 ("" (skosimp*) (("" (lift-if) (("" (ground) (("1" (expand "sigma") (("1" (propax) nil nil)) nil) ("2" (expand "sigma") (("2" (expand "sigma") (("2" (assert) nil nil)) nil)) nil) ("3" (expand "sigma" 2 1) (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ((add_zero_right formula-decl nil vectors_2D nil) (sigma def-decl "Vector" sigma_2D nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) shostak)) (sigma_spl_TCC1 0 (sigma_spl_TCC1-1 nil 3255975799 ("" (skosimp*) (("" (inst + "low!1 + nn!1 + rng!1") (("" (assert) nil nil)) nil)) nil) nil nil)) (sigma_spl_TCC2 0 (sigma_spl_TCC2-1 nil 3255975799 ("" (skosimp*) (("" (inst + "low!1 + nn!1 + rng!1") (("" (assert) nil nil)) nil)) nil) ((int_plus_int_is_int application-judgement "int" integers nil) (rng!1 skolem-const-decl "nat" sigma_2D nil) (nn!1 skolem-const-decl "nat" sigma_2D nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (low!1 skolem-const-decl "T_low" sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil sigma_2D nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (sigma_spl_TCC3 0 (sigma_spl_TCC3-1 nil 3351939915 ("" (skosimp* t) (("" (prop) (("1" (assert) (("1" (inst + "low!1") (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma_2D nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) nil)) (sigma_spl 0 (sigma_spl-1 nil 3255975799 ("" (induct "rng") (("1" (skosimp*) (("1" (assert) (("1" (expand "sigma" 1 3) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" + (1 3)) (("2" (inst?) (("2" (assert) (("2" (lemma "T_pred_lem") (("2" (inst?) (("2" (inst - "1+j!1+low!1+nn!1" "low!1") (("2" (assert) (("2" (replace -2) (("2" (hide -2) (("2" (apply-extensionality 1 :hide? t) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (inst + "low!1") (("1" (assert) nil nil) ("2" (typepred "low!1") (("2" (assert) (("2" (skosimp*) (("2" (lemma "connected_domain") (("2" (inst - "j!1" "low!1 + nn!1 + rng!2" "low!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (inst + "low!1+nn!1+rng!2") (("4" (assert) nil nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp*) nil nil)) nil)) nil) ((low!1 skolem-const-decl "T_low" sigma_2D nil) (nn!1 skolem-const-decl "nat" sigma_2D nil) (rng!2 skolem-const-decl "nat" sigma_2D nil) (NOT const-decl "[bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (connected_domain formula-decl nil sigma_2D nil) (low!1 skolem-const-decl "T_low" sigma_2D nil) (T_pred_lem formula-decl nil sigma_2D nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (add_zero_right formula-decl nil vectors_2D nil) (nat_induction formula-decl nil naturalnumbers nil) (+ const-decl "Vector" vectors_2D nil) (sigma def-decl "Vector" sigma_2D nil) (T_high type-eq-decl nil sigma_2D nil) (= const-decl "[T, T -> boolean]" equalities nil) (Vector type-eq-decl nil vectors_2D nil) (pred type-eq-decl nil defined_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma_2D nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil)) (sigma_split_TCC1 0 (sigma_split_TCC1-1 nil 3255975799 ("" (skosimp* t) (("" (prop) (("1" (inst + "high!1") nil nil) ("2" (inst + "high!1") nil nil) ("3" (skosimp*) (("3" (inst + "j!1") (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (inst + "j!2") (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ((high!1 skolem-const-decl "T_high" sigma_2D nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil)) nil)) (sigma_split_TCC2 0 (sigma_split_TCC2-1 nil 3351939915 ("" (skosimp* t) (("" (assert) (("" (prop) (("1" (inst + "low!1") (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (inst + "low!1") (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (inst + "j!1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (low!1 skolem-const-decl "T_low" sigma_2D nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil)) nil)) (sigma_split 0 (sigma_split-1 nil 3255975799 ("" (skosimp*) (("" (case "high!1<low!1") (("1" (expand "sigma") (("1" (assert) nil nil)) nil) ("2" (case-replace "z!1=low!1-1") (("1" (assert) (("1" (expand "sigma") (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "sigma_spl") (("2" (inst - "F!1" "low!1" "z!1-low!1" "high!1-z!1") (("1" (assert) (("1" (hide-all-but (1 3)) (("1" (use "T_pred_lem") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((T_low type-eq-decl nil sigma_2D nil) (T_high type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil sigma_2D nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (add_zero_left formula-decl nil vectors_2D nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma def-decl "Vector" sigma_2D nil) (sigma_spl formula-decl nil sigma_2D nil) (T_pred_lem formula-decl nil sigma_2D nil) (Vector type-eq-decl nil vectors_2D nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (high!1 skolem-const-decl "T_high" sigma_2D nil) (low!1 skolem-const-decl "T_low" sigma_2D nil) (z!1 skolem-const-decl "int" sigma_2D nil) (>= const-decl "bool" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil)) nil)) (sigma_diff 0 (sigma_diff-1 nil 3255975799 ("" (skosimp*) (("" (lemma "sigma_split") (("" (inst?) (("" (inst -1 "z!1") (("" (assert) (("" (assert) (("" (replace -1) (("" (hide -1) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma_split formula-decl nil sigma_2D nil) (add_cancel formula-decl nil vectors_2D nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (T_low type-eq-decl nil sigma_2D nil) (T_high type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D nil) (T formal-subtype-decl nil sigma_2D nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil)) (sigma_diff_neg 0 (sigma_diff_neg-1 nil 3255975799 ("" (skosimp*) (("" (lemma "sigma_diff") (("" (inst -1 "F!1" "high!1" "low!1" "z!1") (("" (assert) (("" (replace -1 + rl) (("" (assert) (("" (expand "-") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma_diff formula-decl nil sigma_2D nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "Vector" vectors_2D nil) (- const-decl "Vector" vectors_2D nil) (real_minus_real_is_real application-judgement "real" reals nil) (T_low type-eq-decl nil sigma_2D nil) (T_high type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D nil) (T formal-subtype-decl nil sigma_2D nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil)) (sigma_eq_arg 0 (sigma_eq_arg-1 nil 3255975799 ("" (skosimp*) (("" (expand "sigma") (("" (expand "sigma") (("" (assert) nil nil)) nil)) nil)) nil) ((sigma def-decl "Vector" sigma_2D nil) (add_zero_right formula-decl nil vectors_2D nil)) nil)) (sigma_first_TCC1 0 (sigma_first_TCC1-1 nil 3255975799 ("" (skosimp*) (("" (use "T_pred_lem") (("" (assert) nil nil)) nil)) nil) ((T_pred_lem formula-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil sigma_2D nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (T_high type-eq-decl nil sigma_2D nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (sigma_first_TCC2 0 (sigma_first_TCC2-1 nil 3352113941 ("" (skosimp* t) (("" (prop) (("1" (inst + "low!1") (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil) ("3" (inst + "low!1") (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (inst + "j!1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (low!1 skolem-const-decl "T_low" sigma_2D nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil)) nil)) (sigma_first 0 (sigma_first-1 nil 3255975799 ("" (skosimp*) (("" (lemma "sigma_split") (("" (inst?) (("" (inst -1 "low!1") (("" (rewrite "sigma_eq_arg") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((sigma_split formula-decl nil sigma_2D nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_eq_arg formula-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil) (T_high type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D nil) (T formal-subtype-decl nil sigma_2D nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil)) (sigma_last_TCC1 0 (sigma_last_TCC1-2 nil 3351941334 ("" (skosimp* t) (("" (prop) (("1" (inst + "high!1") (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (inst + "high!1") (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (inst + "j!1") (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (inst + "j!2") (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (high!1 skolem-const-decl "T_high" sigma_2D nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil)) nil) (sigma_last_TCC1-1 nil 3255975799 ("" (skosimp*) (("" (typepred "high!1") (("" (skosimp*) (("" (inst + "j!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil) nil nil)) (sigma_last_TCC2 0 (sigma_last_TCC2-1 nil 3351939915 ("" (skosimp*) (("" (use "T_pred_lem") (("" (assert) nil nil)) nil)) nil) ((T_pred_lem formula-decl nil sigma_2D nil) (T_high type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil sigma_2D nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (T_low type-eq-decl nil sigma_2D nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (sigma_last 0 (sigma_last-1 nil 3255975799 ("" (skosimp*) (("" (rewrite "sigma") (("" (assert) (("" (expand "sigma") (("" (lift-if) (("" (ground) (("" (expand "+ ") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma def-decl "Vector" sigma_2D nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma_2D nil) (T_high type-eq-decl nil sigma_2D nil) (Vector type-eq-decl nil vectors_2D nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (add_zero_right formula-decl nil vectors_2D nil) (add_zero_left formula-decl nil vectors_2D nil) (+ const-decl "Vector" vectors_2D nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (sigma_middle_TCC1 0 (sigma_middle_TCC1-1 nil 3256039673 ("" (skosimp* t) (("" (prop) (("1" (inst + "high!1") (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (inst + "high!1") (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (inst + "j!1") (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (inst + "j!2") (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (high!1 skolem-const-decl "T_high" sigma_2D nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil)) shostak)) (sigma_middle_TCC2 0 (sigma_middle_TCC2-1 nil 3256039673 ("" (skosimp*) (("" (inst + "i!1") (("" (assert) nil nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (sigma_middle 0 (sigma_middle-1 nil 3256032001 ("" (skosimp*) (("" (lemma "sigma_split") (("" (inst?) (("" (inst -1 "i!1") (("" (assert) (("" (rewrite "sigma_rew" -) (("" (assert) (("" (replace -1) (("" (hide -1) (("" (expand "sigma" 1 1) (("" (ground) (("" (expand "sigma") (("" (expand "+ ") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma_split formula-decl nil sigma_2D nil) (sigma_rew formula-decl nil sigma_2D nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma def-decl "Vector" sigma_2D nil) (+ const-decl "Vector" vectors_2D nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (T_low type-eq-decl nil sigma_2D nil) (T_high type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D nil) (T formal-subtype-decl nil sigma_2D nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (sigma_const 0 (sigma_const-1 nil 3255975799 ("" (skolem 1 (_ _ x)) (("" (rewrite "high_low_rewrite") (("" (hide 2) (("" (skosimp*) (("" (prop) (("1" (expand "sigma") (("1" (assert) nil nil)) nil) ("2" (induct "n" 2) (("1" (rewrite "sigma_eq_arg") (("1" (assert) (("1" (expand "const_vec") (("1" (expand "*") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "sigma" +) (("2" (assert) (("2" (replace -2) (("2" (hide -2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 3) (("3" (skosimp*) (("3" (inst + "high!1") (("1" (assert) nil nil) ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_plus_int_is_int application-judgement "int" integers nil) (high_low_rewrite formula-decl nil sigma_2D nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil) (pred type-eq-decl nil defined_types nil) (Vector type-eq-decl nil vectors_2D nil) (= const-decl "[T, T -> boolean]" equalities nil) (sigma def-decl "Vector" sigma_2D nil) (const_vec const-decl "Vector" vectors_2D nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (>= const-decl "bool" reals nil) (* const-decl "Vector" vectors_2D nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (zero const-decl "Vector" vectors_2D nil) (int_minus_int_is_int application-judgement "int" integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (low!1 skolem-const-decl "T_low" sigma_2D nil) (high!1 skolem-const-decl "T_high" sigma_2D nil) (subrange type-eq-decl nil integers nil) (subrange_induction formula-decl nil subrange_inductions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (T_pred_lem formula-decl nil sigma_2D nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (scal_1 formula-decl nil vectors_2D nil) (sigma_eq_arg formula-decl nil sigma_2D nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (+ const-decl "Vector" vectors_2D nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (sigma_zero 0 (sigma_zero-1 nil 3255975799 ("" (skosimp*) (("" (lemma "sigma_const") (("" (inst - "high!1" "low!1" "0") (("" (assert) (("" (case-replace "const_vec(0) = zero") (("1" (assert) nil nil) ("2" (invoke (hide ($+n)) (? * "sigma")) (("2" (expand "const_vec") (("2" (expand "zero") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma_const formula-decl nil sigma_2D nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (scal_zero formula-decl nil vectors_2D nil) (int_plus_int_is_int application-judgement "int" integers nil) (Vector type-eq-decl nil vectors_2D nil) (= const-decl "[T, T -> boolean]" equalities nil) (const_vec const-decl "Vector" vectors_2D nil) (zero const-decl "Vector" vectors_2D nil) (T_low type-eq-decl nil sigma_2D nil) (T_high type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil sigma_2D nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil)) (sigma_scal 0 (sigma_scal-1 nil 3255975799 ("" (skolem 1 ("F" "a" _ _)) (("" (rewrite "high_low_rewrite") (("" (hide 2) (("" (skosimp*) (("" (prop) (("1" (expand "sigma") (("1" (assert) nil nil)) nil) ("2" (induct "n" 2) (("1" (rewrite "sigma_eq_arg") (("1" (rewrite "sigma_eq_arg") nil nil) ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "sigma" +) (("2" (assert) (("2" (replace -2 * lr) (("2" (hide -2) (("2" (apply-extensionality 1 :hide? t) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (inst + "high!1") (("1" (assert) nil nil) ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil)) nil)) nil) ("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((high_low_rewrite formula-decl nil sigma_2D nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil) (pred type-eq-decl nil defined_types nil) (Vector type-eq-decl nil vectors_2D nil) (= const-decl "[T, T -> boolean]" equalities nil) (sigma def-decl "Vector" sigma_2D nil) (* const-decl "Vector" vectors_2D nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (low!1 skolem-const-decl "T_low" sigma_2D nil) (high!1 skolem-const-decl "T_high" sigma_2D nil) (subrange type-eq-decl nil integers nil) (subrange_induction formula-decl nil subrange_inductions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (>= const-decl "bool" reals nil) (T_pred_lem formula-decl nil sigma_2D nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_eq_arg formula-decl nil sigma_2D nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "Vector" vectors_2D nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (scal_zero formula-decl nil vectors_2D nil)) nil)) (sigma_shift_T_TCC1 0 (sigma_shift_T_TCC1-1 nil 3255975799 ("" (skosimp* t) (("" (prop) (("1" (inst - "low!1") nil nil) ("2" (skosimp*) (("2" (inst + "j!1+z!1") (("1" (assert) nil nil) ("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ((low!1 skolem-const-decl "T_low" sigma_2D nil) (int_plus_int_is_int application-judgement "int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (j!1 skolem-const-decl "T" sigma_2D nil) (z!1 skolem-const-decl "int" sigma_2D nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma_2D nil)) nil)) (sigma_shift_T_TCC2 0 (sigma_shift_T_TCC2-1 nil 3351939915 ("" (skosimp* t) (("" (prop) (("1" (inst?) nil nil) ("2" (skosimp*) (("2" (inst + "z!1+j!1") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ((high!1 skolem-const-decl "T_high" sigma_2D nil) (int_plus_int_is_int application-judgement "int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (j!1 skolem-const-decl "T" sigma_2D nil) (z!1 skolem-const-decl "int" sigma_2D nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma_2D nil)) nil)) (sigma_shift_T_TCC3 0 (sigma_shift_T_TCC3-1 nil 3352113941 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil)) (sigma_shift_T 0 (sigma_shift_T-1 nil 3255975799 ("" (skolem 1 ("F" _ _ "z")) (("" (rewrite "high_low_rewrite") (("1" (hide 2) (("1" (skosimp*) (("1" (prop) (("1" (expand "sigma") (("1" (assert) nil nil)) nil) ("2" (induct "n" 2) (("1" (skosimp*) (("1" (rewrite "sigma_eq_arg") (("1" (rewrite "sigma_eq_arg") (("1" (hide -1 2) (("1" (use "T_pred_lem") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (inst?) (("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "sigma" +) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) nil nil) ("4" (hide-all-but 1) (("4" (skosimp* t) (("4" (typepred "high!1") (("4" (prop) (("1" (inst + "high!1") nil nil) ("2" (skosimp*) (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide -1 2 3) (("5" (skosimp* t) (("5" (typepred "high!1") (("5" (prop) (("1" (inst + "high!1+z") (("1" (assert) nil nil) ("2" (inst?) nil nil)) nil) ("2" (skosimp*) (("2" (inst + "j!1+z") (("1" (assert) nil nil) ("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (hide -1 2 3) (("6" (skosimp* t) (("6" (assert) (("6" (typepred "low!1") (("6" (prop) (("1" (inst?) nil nil) ("2" (skosimp*) (("2" (inst + "j!1+z") (("1" (assert) nil nil) ("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("7" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) nil nil) ("3" (hide 2) (("3" (skosimp* t) (("3" (hide -1 -4) (("3" (assert) (("3" (prop) (("1" (typepred "high!1") (("1" (prop) (("1" (assert) (("1" (inst?) nil nil)) nil) ("2" (skosimp*) (("2" (inst + "j!1+z") (("1" (assert) nil nil) ("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "high!1") (("2" (prop) (("1" (inst?) nil nil) ("2" (skosimp*) (("2" (inst + "j!2+z") (("1" (assert) nil nil) ("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp* t) (("4" (hide -1) (("4" (inst?) (("4" (assert) (("4" (skosimp*) (("4" (reveal -1) (("4" (inst + "j!1+z") (("1" (assert) nil nil) ("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_plus_int_is_int application-judgement "int" integers nil) (high_low_rewrite formula-decl nil sigma_2D nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (Vector type-eq-decl nil vectors_2D nil) (= const-decl "[T, T -> boolean]" equalities nil) (sigma def-decl "Vector" sigma_2D nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (low!1 skolem-const-decl "T_low" sigma_2D nil) (high!1 skolem-const-decl "T_high" sigma_2D nil) (subrange type-eq-decl nil integers nil) (z skolem-const-decl "int" sigma_2D 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) (sigma_eq_arg formula-decl nil sigma_2D nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (T_pred_lem formula-decl nil sigma_2D nil) (NOT const-decl "[bool -> bool]" booleans nil) (j!1 skolem-const-decl "T" sigma_2D nil) (j!1 skolem-const-decl "T" sigma_2D nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (high!1 skolem-const-decl "T_high" sigma_2D nil) (j!2 skolem-const-decl "T" sigma_2D nil) (j!1 skolem-const-decl "T" sigma_2D nil) (low!1 skolem-const-decl "T_low" sigma_2D nil) (j!1 skolem-const-decl "T" sigma_2D nil)) nil)) (sigma_shift_T2_TCC1 0 (sigma_shift_T2_TCC1-2 nil 3351941788 ("" (skosimp*) (("" (inst + "low!1+z!1") (("" (assert) nil nil)) nil)) nil) nil nil) (sigma_shift_T2_TCC1-1 nil 3351939915 ("" (skosimp*) (("" (typepred "high!1") (("" (skosimp*) (("" (inst + "z!1+high!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil) nil nil)) (sigma_shift_T2_TCC2 0 (sigma_shift_T2_TCC2-1 nil 3352113941 ("" (skosimp*) (("" (inst + "high!1+z!1") (("" (assert) nil nil)) nil)) nil) nil nil)) (sigma_shift_T2 0 (sigma_shift_T2-1 nil 3304414785 ("" (skolem 1 ("F" _ _ "z")) (("" (rewrite "high_low_rewrite") (("1" (hide 2) (("1" (skosimp*) (("1" (prop) (("1" (expand "sigma") (("1" (assert) nil nil)) nil) ("2" (induct "n" 2) (("1" (flatten) (("1" (rewrite "sigma_eq_arg") (("1" (rewrite "sigma_eq_arg") (("1" (assert) nil nil) ("2" (hide -1 -2 2) (("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "sigma" +) (("2" (assert) (("2" (prop) (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (invoke (hide ($+n)) (? * "sigma")) (("2" (lemma "connected_domain") (("2" (inst?) (("2" (inst - "low!1+z" "1+k!1+z") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp* t) (("3" (typepred "high!1") (("3" (inst + "high!1") (("3" (assert) (("3" (skosimp*) (("3" (assert) (("3" (use "T_pred_lem") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (skosimp*) nil nil)) nil) ("5" (hide-all-but 1) (("5" (skosimp*) nil nil)) nil) ("6" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) nil nil)) nil) ("3" (hide 2) (("3" (skosimp*) nil nil)) nil)) nil)) nil) ((int_plus_int_is_int application-judgement "int" integers nil) (high_low_rewrite formula-decl nil sigma_2D nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (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) (Vector type-eq-decl nil vectors_2D nil) (= const-decl "[T, T -> boolean]" equalities nil) (sigma def-decl "Vector" sigma_2D nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (zero const-decl "Vector" vectors_2D nil) (low!1 skolem-const-decl "T_low" sigma_2D nil) (high!1 skolem-const-decl "T_high" sigma_2D nil) (subrange type-eq-decl nil integers nil) (z skolem-const-decl "int" sigma_2D 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) (sigma_eq_arg formula-decl nil sigma_2D nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (T_pred_lem formula-decl nil sigma_2D nil) (integer nonempty-type-from-decl nil integers nil) (connected_domain formula-decl nil sigma_2D nil) (NOT const-decl "[bool -> bool]" booleans 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_sum 0 (sigma_sum-2 nil 3411479595 ("" (skolem 1 ("F" "G" _ _)) (("" (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") (("1" (rewrite "sigma_eq_arg") nil nil)) nil) ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "sigma" +) (("2" (replace -2 + rl) (("2" (hide -2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp* t) (("3" (typepred "high!1") (("3" (inst + "high!1") (("3" (assert) (("3" (skosimp*) (("3" (use "T_pred_lem") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((high_low_rewrite formula-decl nil sigma_2D nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil) (pred type-eq-decl nil defined_types nil) (Vector type-eq-decl nil vectors_2D nil) (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "Vector" vectors_2D nil) (sigma def-decl "Vector" sigma_2D nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (low!1 skolem-const-decl "T_low" sigma_2D nil) (high!1 skolem-const-decl "T_high" sigma_2D nil) (subrange type-eq-decl nil integers nil) (subrange_induction formula-decl nil subrange_inductions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (>= const-decl "bool" reals nil) (T_pred_lem formula-decl nil sigma_2D nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_eq_arg formula-decl nil sigma_2D nil) (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) (NOT const-decl "[bool -> bool]" booleans 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) (add_zero_left formula-decl nil vectors_2D nil)) nil) (sigma_sum-1 nil 3255975799 ("" (skolem 1 ("F" "G" _ _)) (("" (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") (("1" (rewrite "sigma_eq_arg") nil nil)) nil) ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "sigma" +) (("2" (replace -2 + rl) (("2" (hide -2) (("2" (apply-extensionality 1 :hide? t) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp* t) (("3" (typepred "high!1") (("3" (inst + "high!1") (("3" (assert) (("3" (skosimp*) (("3" (use "T_pred_lem") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) nil nil)) (sigma_minus 0 (sigma_minus-1 nil 3255975799 ("" (skolem 1 ("F" "G" _ _)) (("" (rewrite "high_low_rewrite") (("" (hide 2) (("" (skosimp*) (("" (prop) (("1" (expand "sigma") (("1" (assert) (("1" (expand "zero") (("1" (expand "-") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (induct "n" 2) (("1" (rewrite "sigma_eq_arg") (("1" (rewrite "sigma_eq_arg") (("1" (rewrite "sigma_eq_arg") nil nil)) nil) ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "sigma" +) (("2" (replace -2 + rl) (("2" (hide -2) (("2" (expand "+ ") (("2" (expand "-") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp* t) (("3" (typepred "high!1") (("3" (inst + "high!1") (("3" (assert) (("3" (skosimp*) (("3" (use "T_pred_lem") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((high_low_rewrite formula-decl nil sigma_2D nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil) (pred type-eq-decl nil defined_types nil) (Vector type-eq-decl nil vectors_2D nil) (= const-decl "[T, T -> boolean]" equalities nil) (- const-decl "Vector" vectors_2D nil) (sigma def-decl "Vector" sigma_2D nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (low!1 skolem-const-decl "T_low" sigma_2D nil) (high!1 skolem-const-decl "T_high" sigma_2D nil) (subrange type-eq-decl nil integers nil) (subrange_induction formula-decl nil subrange_inductions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (>= const-decl "bool" reals nil) (T_pred_lem formula-decl nil sigma_2D nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_eq_arg formula-decl nil sigma_2D nil) (+ const-decl "Vector" vectors_2D nil) (NOT const-decl "[bool -> bool]" booleans 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) (sub_zero_left formula-decl nil vectors_2D nil) (neg_zero formula-decl nil vectors_2D nil)) nil)) (sigma_restrict 0 (sigma_restrict-1 nil 3255975799 ("" (skolem 1 ("F" "h" _ "l" _)) (("" (rewrite "high_low_rewrite") (("1" (hide 2) (("1" (skosimp*) (("1" (prop) (("1" (expand "sigma") (("1" (assert) nil nil)) nil) ("2" (induct "n" 2) (("1" (rewrite "sigma_eq_arg") (("1" (rewrite "sigma_eq_arg") (("1" (expand "restrict") (("1" (flatten) (("1" (assert) nil nil)) 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" (rewrite "restrict") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (inst + "h") (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (inst + "l") (("4" (assert) nil nil)) nil)) nil) ("5" (hide-all-but 1) (("5" (skosimp* t) (("5" (hide -3 -4) (("5" (inst + "n!2") (("1" (assert) nil nil) ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("6" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (inst + "h") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (inst + "l") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((high_low_rewrite formula-decl nil sigma_2D nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (>= const-decl "bool" reals nil) (Vector type-eq-decl nil vectors_2D nil) (= const-decl "[T, T -> boolean]" equalities nil) (sigma def-decl "Vector" sigma_2D nil) (restrict const-decl "[T -> Vector]" sigma_2D nil) (low!1 skolem-const-decl "T_low" sigma_2D nil) (high!1 skolem-const-decl "T_high" sigma_2D nil) (subrange type-eq-decl nil integers nil) (l skolem-const-decl "T" sigma_2D nil) (h skolem-const-decl "T" sigma_2D nil) (subrange_induction formula-decl nil subrange_inductions nil) (T_pred_lem formula-decl nil sigma_2D nil) (sigma_eq_arg formula-decl nil sigma_2D nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (int_plus_int_is_int application-judgement "int" integers 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_ge_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)) nil)) (sigma_restrict_to 0 (sigma_restrict_to-1 nil 3255975799 ("" (skosimp*) (("" (case "high!1 < low!1") (("1" (expand "sigma") (("1" (assert) nil nil)) nil) ("2" (rewrite "sigma_restrict") (("1" (use "T_pred_lem") (("1" (assert) nil nil)) nil) ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((T_low type-eq-decl nil sigma_2D nil) (T_high type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil sigma_2D nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma def-decl "Vector" sigma_2D nil) (T_pred_lem formula-decl nil sigma_2D nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (Vector type-eq-decl nil vectors_2D nil) (sigma_restrict formula-decl nil sigma_2D nil)) nil)) (sigma_restrict_eq 0 (sigma_restrict_eq-1 nil 3255975799 ("" (skosimp*) (("" (case "high!1 < low!1") (("1" (expand "sigma") (("1" (assert) nil nil)) nil) ("2" (lemma "sigma_restrict") (("2" (inst?) (("2" (inst -1 "high!1" "low!1") (("1" (assert) (("1" (replace*) (("1" (hide -1 -2) (("1" (lemma "sigma_restrict") (("1" (inst -1 "G!1" "high!1" "high!1" "low!1" "low!1") (("1" (assert) nil nil) ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil) ("3" (use "T_pred_lem") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil) ("3" (use "T_pred_lem") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T_low type-eq-decl nil sigma_2D nil) (T_high type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil sigma_2D nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma def-decl "Vector" sigma_2D nil) (Vector type-eq-decl nil vectors_2D nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (T_pred_lem formula-decl nil sigma_2D nil) (low!1 skolem-const-decl "T_low" sigma_2D nil) (high!1 skolem-const-decl "T_high" sigma_2D nil) (sigma_restrict formula-decl nil sigma_2D nil)) nil)) (sigma_eq_TCC1 0 (sigma_eq_TCC1-1 nil 3411477956 ("" (skosimp*) (("" (typepred "n!1") (("" (typepred "low!1") (("" (typepred "high!1") (("" (lemma "connected_domain") (("" (ground) (("1" (inst - "low!1" "high!1" "n!1") (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (inst - "j!1" "high!1" "n!1") (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (inst - "low!1" "j!1" "n!1") (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (inst - "j!1" "j!2" "n!1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((subrange type-eq-decl nil integers nil) (T_high type-eq-decl nil sigma_2D nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (T_low type-eq-decl nil sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (<= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (integer nonempty-type-from-decl nil integers nil) (connected_domain formula-decl nil sigma_2D nil)) nil)) (sigma_eq 0 (sigma_eq-1 nil 3255975799 ("" (skosimp*) (("" (lemma "sigma_restrict_eq") (("" (inst?) (("" (assert) (("" (hide 2) (("" (expand "restrict") (("" (apply-extensionality 1 :hide? t) (("" (lift-if) (("" (ground) (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma_restrict_eq formula-decl nil sigma_2D nil) (restrict const-decl "[T -> Vector]" sigma_2D nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers 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_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (< const-decl "bool" reals nil) (> const-decl "bool" reals nil) (zero const-decl "Vector" vectors_2D nil) (T_low type-eq-decl nil sigma_2D nil) (T_high type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D nil) (T formal-subtype-decl nil sigma_2D nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil)) (sigma_with 0 (sigma_with-2 nil 3411479877 ("" (skosimp*) (("" (case "i!1 = low!1") (("1" (rewrite "sigma_first") (("1" (lemma "sigma_first") (("1" (inst -1 "G!1" "high!1" "low!1") (("1" (assert) (("1" (replace -1) (("1" (replace -5) (("1" (hide -1 -5) (("1" (assert) (("1" (replace -1) (("1" (assert) (("1" (lemma "sigma_eq") (("1" (inst?) (("1" (inst - "G!1") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (rewrite "add_comm") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "i!1 = high!1") (("1" (rewrite "sigma_last") (("1" (lemma "sigma_last") (("1" (inst -1 "G!1" "high!1" "low!1") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (replace -4) (("1" (assert) (("1" (lemma "sigma_eq") (("1" (inst?) (("1" (inst -1 "G!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sigma_split") (("2" (inst?) (("2" (inst -1 "i!1") (("2" (assert) (("2" (replace -1) (("2" (hide -1) (("2" (lemma "sigma_split") (("2" (inst -1 "G!1" "high!1" "low!1" "i!1") (("2" (assert) (("2" (replace -1) (("2" (hide -1) (("2" (lemma "sigma_last") (("2" (inst-cp -1 "F!1" "i!1" "low!1") (("2" (inst -1 "G!1" "i!1" "low!1") (("2" (assert) (("2" (replace -1) (("2" (hide -1) (("2" (replace -1) (("2" (hide -1) (("2" (replace -3) (("2" (hide -3) (("2" (ground) (("2" (case-replace "sigma(low!1, i!1 - 1, G!1 WITH [i!1 := v!1]) = sigma(low!1, i!1 - 1, G!1)") (("1" (hide -1) (("1" (case "sigma(1 + i!1, high!1, G!1 WITH [i!1 := v!1]) = sigma(1 + i!1, high!1, G!1 )") (("1" (replace -1) (("1" (hide -1) (("1" (expand "+ ") (("1" (assert) (("1" (expand "-") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (lemma "sigma_eq") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (lemma "sigma_eq") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T_low type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (T formal-subtype-decl nil sigma_2D nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (add_cancel formula-decl nil vectors_2D nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (add_comm formula-decl nil vectors_2D nil) (sigma def-decl "Vector" sigma_2D nil) (sigma_eq formula-decl nil sigma_2D nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (T_high type-eq-decl nil sigma_2D nil) (Vector type-eq-decl nil vectors_2D nil) (sigma_first formula-decl nil sigma_2D nil) (sigma_split formula-decl nil sigma_2D nil) (- const-decl "Vector" vectors_2D nil) (+ const-decl "Vector" vectors_2D nil) (real_plus_real_is_real application-judgement "real" reals nil) (sigma_last formula-decl nil sigma_2D nil) (int_minus_int_is_int application-judgement "int" integers nil) (add_cancel_neg2 formula-decl nil vectors_2D nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil)) nil) (sigma_with-1 nil 3255975799 ("" (skosimp*) (("" (case "i!1 = low!1") (("1" (rewrite "sigma_first") (("1" (lemma "sigma_first") (("1" (inst -1 "G!1" "high!1" "low!1") (("1" (assert) (("1" (split -1) (("1" (assert) (("1" (replace -1) (("1" (replace -5) (("1" (hide -1 -5) (("1" (assert) (("1" (replace -1) (("1" (assert) (("1" (rewrite "sigma_eq") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "sigma") (("2" (assert) (("2" (expand "sigma") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "sigma") (("2" (assert) (("2" (expand "sigma") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case-replace "i!1 = high!1") (("1" (rewrite "sigma_last") (("1" (lemma "sigma_last") (("1" (inst -1 "G!1" "high!1" "low!1") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (replace -4) (("1" (assert) (("1" (rewrite "sigma_eq") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sigma_split") (("2" (inst?) (("2" (inst -1 "i!1") (("2" (assert) (("2" (replace -1) (("2" (hide -1) (("2" (lemma "sigma_split") (("2" (inst -1 "G!1" "high!1" "low!1" "i!1") (("2" (assert) (("2" (replace -1) (("2" (hide -1) (("2" (lemma "sigma_last") (("2" (inst-cp -1 "F!1" "i!1" "low!1") (("2" (inst -1 "G!1" "i!1" "low!1") (("2" (assert) (("2" (replace -1) (("2" (hide -1) (("2" (replace -1) (("2" (hide -1) (("2" (replace -3) (("2" (hide -3) (("2" (ground) (("2" (case-replace "sigma(low!1, i!1 - 1, G!1 WITH [i!1 := a!1]) = sigma(low!1, i!1 - 1, G!1)") (("1" (hide -1) (("1" (assert) (("1" (rewrite "sigma_eq") nil nil)) nil)) nil) ("2" (hide 4) (("2" (rewrite "sigma_eq") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil nil)) (sum_it_def_TCC1 0 (sum_it_def_TCC1-1 nil 3255975799 ("" (skosimp*) (("" (inst + "low!1") (("1" (assert) nil nil) ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil)) nil)) nil) ((low!1 skolem-const-decl "T_low" sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil sigma_2D nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_gt_is_strict_total_order name-judgement "(strict_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) (T_high type-eq-decl nil sigma_2D nil) (T_pred_lem formula-decl nil sigma_2D nil)) nil)) (sum_it_def_TCC2 0 (sum_it_def_TCC2-1 nil 3255975799 ("" (skosimp*) (("" (use "T_pred_lem") (("" (assert) nil nil)) nil)) nil) ((T_pred_lem formula-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil sigma_2D nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (T_high type-eq-decl nil sigma_2D nil) (real_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)) (sum_it_def_TCC3 0 (sum_it_def_TCC3-1 nil 3352118808 ("" (subtype-tcc) nil nil) ((int_minus_int_is_int application-judgement "int" integers nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma_2D nil) (T_high type-eq-decl nil sigma_2D nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs 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)) nil)) (sum_it_prop_TCC1 0 (sum_it_prop_TCC1-1 nil 3352142246 ("" (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" (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) ((int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (low!1 skolem-const-decl "T_low" sigma_2D nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil)) nil)) (sum_it_prop 0 (sum_it_prop-1 nil 3255975799 ("" (skosimp*) (("" (case "high!1<low!1") (("1" (assert) (("1" (expand "sum_it_def") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (lemma "subrange_induction[low!1,high!1]") (("1" (inst -1 "lambda(lh:T| low!1 <= lh AND lh <= high!1): sum_it_def((high!1-lh)+low!1, high!1, F!1, sigma (("1" (expand "extend") (("1" (ground) (("1" (inst -1 "high!1-i!1+low!1-1") (("1" (ground) nil nil) ("2" (expand "sum_it_def") (("2" (expand "sigma") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (ground) (("2" (hide -2 -3 -4 3) (("2" (expand "sum_it_def") (("2" (expand "sum_it_def") (("2" (expand "sigma" + 2) (("2" (expand "+ ") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (ground) (("3" (expand "sigma") (("3" (assert) (("3" (hide -1 -2 3) (("3" (use "T_pred_lem") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide -1 -2 3) (("4" (skosimp*) (("4" (ground) (("1" (expand "sum_it_def" 1) (("1" (expand "sigma" -) (("1" (assert) (("1" (expand "sigma" 1 2) (("1" (rewrite "add_comm" -4) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (lemma "T_pred_lem") (("2" (inst?) (("2" (inst - "high!1" "low!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "high!1 -lh!1 +low!1") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (lemma "T_pred_lem") (("2" (inst - "high!1" "low!1" "high!1-lh!1+low!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (typepred "high!1") (("3" (typepred "low!1") (("3" (assert) (("3" (lemma "T_pred_lem") (("3" (inst - "high!1" "low!1" "(high!1 - lh!1) + low!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((T_low type-eq-decl nil sigma_2D nil) (T_high type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil sigma_2D nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sum_it_def def-decl "Vector" sigma_2D nil) (sigma def-decl "Vector" sigma_2D 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) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (high!1 skolem-const-decl "T_high" sigma_2D nil) (low!1 skolem-const-decl "T_low" sigma_2D nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (pred type-eq-decl nil defined_types nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (Vector type-eq-decl nil vectors_2D nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (i!1 skolem-const-decl "T" sigma_2D nil) (+ const-decl "Vector" vectors_2D nil) (T_pred_lem formula-decl nil sigma_2D nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (add_comm formula-decl nil vectors_2D nil) (lh!1 skolem-const-decl "{lh: T | low!1 <= lh AND lh <= high!1}" sigma_2D nil) (NOT const-decl "[bool -> bool]" booleans nil) (>= const-decl "bool" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (subrange_induction formula-decl nil subrange_inductions nil)) nil)) (sum_it_sigma 0 (sum_it_sigma-1 nil 3255975799 ("" (skolem 1 ("F" "high" "low")) (("" (case "low > high") (("1" (expand "sum_it") (("1" (expand "sum_it_def") (("1" (expand "sigma") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "sum_it") (("2" (expand "sum_it_def") (("2" (assert) (("2" (lemma "sum_it_prop") (("2" (inst -1 "F" "high" "low" "low") (("2" (assert) (("2" (rewrite "sigma_eq_arg") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T_high type-eq-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil sigma_2D nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (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) (sum_it_def def-decl "Vector" sigma_2D nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma def-decl "Vector" sigma_2D nil) (sum_it const-decl "Vector" sigma_2D nil) (sum_it_prop formula-decl nil sigma_2D nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_eq_arg formula-decl nil sigma_2D nil) (Vector type-eq-decl nil vectors_2D nil) (add_zero_left formula-decl nil vectors_2D nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil)))
¤ Dauer der Verarbeitung: 0.62 Sekunden (vorverarbeitet am 2026-04-26) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26