| products/sources/formale sprachen/PVS/vectors/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: sigma_2D.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(sigma_2D
(T_pred_lem 0 (T_pred_lem-1 nil 3352120046 ("" (skosimp* t) (("" (prop) (("1" (lemma "connected_domain") (("1" (inst - "low!1" "high!1" "z!1") (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "connected_domain") (("2" (inst - "j!1" "high!1" "z!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (lemma "connected_domain") (("3" (inst - "low!1" "j!1" "z!1") (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (lemma "connected_domain") (("4" (inst - "low!1" "j!2" "z!1") (("1" (assert) nil nil) ("2" (lemma "connected_domain") (("2" (inst - "j!1" "j!2" "low!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((low!1 skolem-const-decl "T_low" sigma_2D nil) (high!1 skolem-const-decl "T_high" sigma_2D nil) (integer nonempty-type-from-decl nil integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (connected_domain formula-decl nil sigma_2D nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil)) shostak)) (high_low_rewrite_TCC1 0 (high_low_rewrite_TCC1-1 nil 3352229091 ("" (skosimp*) (("" (inst + "high!1") (("1" (assert) nil nil) ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil)) nil)) nil) ((high!1 skolem-const-decl "T_high" sigma_2D nil) (T_high type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil sigma_2D nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (T_low type-eq-decl nil sigma_2D nil) (T_pred_lem formula-decl nil sigma_2D nil)) nil)) (high_low_rewrite 0 (high_low_rewrite-1 nil 3352228842 ("" (skosimp*) (("" (inst?) (("" (prop) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (high!1 skolem-const-decl "T_high" sigma_2D nil) (low!1 skolem-const-decl "T_low" sigma_2D nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (sigma_TCC1 0 (sigma_TCC1-2 nil 3403452046 ("" (skosimp* t) (("" (assert) (("" (skosimp*) (("" (typepred "j!1") (("" (lemma "connected_domain") (("" (inst - "low!1" "j!1" "high!1") (("1" (assert) nil nil) ("2" (prop) (("2" (skosimp*) (("2" (lemma "connected_domain") (("2" (assert) (("2" (inst - "j!2" "j!1" "low!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (low!1 skolem-const-decl "T_low" sigma_2D nil) (integer nonempty-type-from-decl nil integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (connected_domain formula-decl nil sigma_2D nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma_2D nil) (T_high type-eq-decl nil sigma_2D nil)) nil) (sigma_TCC1-1 nil 3255975799 ("" (skosimp*) (("" (use "T_pred_lem") (("" (assert) nil nil)) nil)) nil) nil nil)) (sigma_TCC2 0 (sigma_TCC2-2 nil 3403452083 ("" (skosimp*) (("" (typepred "high!1") (("" (assert) (("" (prop) (("1" (inst + "high!1") (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (typepred "j!1") (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T_high type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil sigma_2D nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (high!1 skolem-const-decl "T_high" sigma_2D nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil) (sigma_TCC2-1 nil 3255975799 ("" (skosimp* t) (("" (assert) (("" (skosimp*) (("" (typepred "j!1") (("" (lemma "connected_domain") (("" (inst - "low!1" "j!1" "high!1") (("1" (assert) nil nil) ("2" (prop) (("2" (skosimp*) (("2" (lemma "connected_domain") (("2" (assert) (("2" (inst - "j!2" "j!1" "low!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil nil)) (sigma_TCC3 0 (sigma_TCC3-1 nil 3255975799 ("" (skosimp*) (("" (grind) nil nil)) nil) ((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (minus_int_is_int application-judgement "int" integers nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (sigma_rew_TCC1 0 (sigma_rew_TCC1-1 nil 3411477956 ("" (skosimp*) (("" (assert) (("" (typepred "low!1") (("" (typepred "high!1") (("" (ground) (("" (skosimp*) (("" (assert) (("" (typepred "j!1") (("" (typepred "j!2") (("" (lemma "connected_domain") (("" (inst - "j!1" "j!2" "low!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (T_high type-eq-decl nil sigma_2D nil) (connected_domain formula-decl nil sigma_2D nil) (integer nonempty-type-from-decl nil integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma_2D nil)) nil)) (sigma_rew 0 (sigma_rew-1 nil 3352522445 ("" (skosimp*) (("" (lift-if) (("" (ground) (("1" (expand "sigma") (("1" (propax) nil nil)) nil) ("2" (expand "sigma") (("2" (expand "sigma") (("2" (assert) nil nil)) nil)) nil) ("3" (expand "sigma" 2 1) (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ((add_zero_right formula-decl nil vectors_2D nil) (sigma def-decl "Vector" sigma_2D nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) shostak)) (sigma_spl_TCC1 0 (sigma_spl_TCC1-1 nil 3255975799 ("" (skosimp*) (("" (inst + "low!1 + nn!1 + rng!1") (("" (assert) nil nil)) nil)) nil) nil nil)) (sigma_spl_TCC2 0 (sigma_spl_TCC2-1 nil 3255975799 ("" (skosimp*) (("" (inst + "low!1 + nn!1 + rng!1") (("" (assert) nil nil)) nil)) nil) ((int_plus_int_is_int application-judgement "int" integers nil) (rng!1 skolem-const-decl "nat" sigma_2D nil) (nn!1 skolem-const-decl "nat" sigma_2D nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (low!1 skolem-const-decl "T_low" sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil sigma_2D nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (sigma_spl_TCC3 0 (sigma_spl_TCC3-1 nil 3351939915 ("" (skosimp* t) (("" (prop) (("1" (assert) (("1" (inst + "low!1") (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma_2D nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) nil)) (sigma_spl 0 (sigma_spl-1 nil 3255975799 ("" (induct "rng") (("1" (skosimp*) (("1" (assert) (("1" (expand "sigma" 1 3) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" + (1 3)) (("2" (inst?) (("2" (assert) (("2" (lemma "T_pred_lem") (("2" (inst?) (("2" (inst - "1+j!1+low!1+nn!1" "low!1") (("2" (assert) (("2" (replace -2) (("2" (hide -2) (("2" (apply-extensionality 1 :hide? t) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (inst + "low!1") (("1" (assert) nil nil) ("2" (typepred "low!1") (("2" (assert) (("2" (skosimp*) (("2" (lemma "connected_domain") (("2" (inst - "j!1" "low!1 + nn!1 + rng!2" "low!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (inst + "low!1+nn!1+rng!2") (("4" (assert) nil nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp*) nil nil)) nil)) nil) ((low!1 skolem-const-decl "T_low" sigma_2D nil) (nn!1 skolem-const-decl "nat" sigma_2D nil) (rng!2 skolem-const-decl "nat" sigma_2D nil) (NOT const-decl "[bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (connected_domain formula-decl nil sigma_2D nil) (low!1 skolem-const-decl "T_low" sigma_2D nil) (T_pred_lem formula-decl nil sigma_2D nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (add_zero_right formula-decl nil vectors_2D nil) (nat_induction formula-decl nil naturalnumbers nil) (+ const-decl "Vector" vectors_2D nil) (sigma def-decl "Vector" sigma_2D nil) (T_high type-eq-decl nil sigma_2D nil) (= const-decl "[T, T -> boolean]" equalities nil) (Vector type-eq-decl nil vectors_2D nil) (pred type-eq-decl nil defined_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma_2D nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil)) (sigma_split_TCC1 0 (sigma_split_TCC1-1 nil 3255975799 ("" (skosimp* t) (("" (prop) (("1" (inst + "high!1") nil nil) ("2" (inst + "high!1") nil nil) ("3" (skosimp*) (("3" (inst + "j!1") (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (inst + "j!2") (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ((high!1 skolem-const-decl "T_high" sigma_2D nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil)) nil)) (sigma_split_TCC2 0 (sigma_split_TCC2-1 nil 3351939915 ("" (skosimp* t) (("" (assert) (("" (prop) (("1" (inst + "low!1") (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (inst + "low!1") (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (inst + "j!1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (low!1 skolem-const-decl "T_low" sigma_2D nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil)) nil)) (sigma_split 0 (sigma_split-1 nil 3255975799 ("" (skosimp*) (("" (case "high!1 (("1" (expand "sigma") (("1" (assert) nil nil)) nil) ("2" (case-replace "z!1=low!1-1") (("1" (assert) (("1" (expand "sigma") (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "sigma_spl") (("2" (inst - "F!1" "low!1" "z!1-low!1" "high!1-z!1") (("1" (assert) (("1" (hide-all-but (1 3)) (("1" (use "T_pred_lem") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((T_low type-eq-decl nil sigma_2D nil) (T_high type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil sigma_2D nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (add_zero_left formula-decl nil vectors_2D nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma def-decl "Vector" sigma_2D nil) (sigma_spl formula-decl nil sigma_2D nil) (T_pred_lem formula-decl nil sigma_2D nil) (Vector type-eq-decl nil vectors_2D nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (high!1 skolem-const-decl "T_high" sigma_2D nil) (low!1 skolem-const-decl "T_low" sigma_2D nil) (z!1 skolem-const-decl "int" sigma_2D nil) (>= const-decl "bool" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil)) nil)) (sigma_diff 0 (sigma_diff-1 nil 3255975799 ("" (skosimp*) (("" (lemma "sigma_split") (("" (inst?) (("" (inst -1 "z!1") (("" (assert) (("" (assert) (("" (replace -1) (("" (hide -1) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma_split formula-decl nil sigma_2D nil) (add_cancel formula-decl nil vectors_2D nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (T_low type-eq-decl nil sigma_2D nil) (T_high type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D nil) (T formal-subtype-decl nil sigma_2D nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil)) (sigma_diff_neg 0 (sigma_diff_neg-1 nil 3255975799 ("" (skosimp*) (("" (lemma "sigma_diff") (("" (inst -1 "F!1" "high!1" "low!1" "z!1") (("" (assert) (("" (replace -1 + rl) (("" (assert) (("" (expand "-") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma_diff formula-decl nil sigma_2D nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "Vector" vectors_2D nil) (- const-decl "Vector" vectors_2D nil) (real_minus_real_is_real application-judgement "real" reals nil) (T_low type-eq-decl nil sigma_2D nil) (T_high type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D nil) (T formal-subtype-decl nil sigma_2D nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil)) (sigma_eq_arg 0 (sigma_eq_arg-1 nil 3255975799 ("" (skosimp*) (("" (expand "sigma") (("" (expand "sigma") (("" (assert) nil nil)) nil)) nil)) nil) ((sigma def-decl "Vector" sigma_2D nil) (add_zero_right formula-decl nil vectors_2D nil)) nil)) (sigma_first_TCC1 0 (sigma_first_TCC1-1 nil 3255975799 ("" (skosimp*) (("" (use "T_pred_lem") (("" (assert) nil nil)) nil)) nil) ((T_pred_lem formula-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil sigma_2D nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (T_high type-eq-decl nil sigma_2D nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (sigma_first_TCC2 0 (sigma_first_TCC2-1 nil 3352113941 ("" (skosimp* t) (("" (prop) (("1" (inst + "low!1") (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil) ("3" (inst + "low!1") (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (inst + "j!1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (low!1 skolem-const-decl "T_low" sigma_2D nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil)) nil)) (sigma_first 0 (sigma_first-1 nil 3255975799 ("" (skosimp*) (("" (lemma "sigma_split") (("" (inst?) (("" (inst -1 "low!1") (("" (rewrite "sigma_eq_arg") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((sigma_split formula-decl nil sigma_2D nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_eq_arg formula-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil) (T_high type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D nil) (T formal-subtype-decl nil sigma_2D nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil)) (sigma_last_TCC1 0 (sigma_last_TCC1-2 nil 3351941334 ("" (skosimp* t) (("" (prop) (("1" (inst + "high!1") (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (inst + "high!1") (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (inst + "j!1") (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (inst + "j!2") (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (high!1 skolem-const-decl "T_high" sigma_2D nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil)) nil) (sigma_last_TCC1-1 nil 3255975799 ("" (skosimp*) (("" (typepred "high!1") (("" (skosimp*) (("" (inst + "j!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil) nil nil)) (sigma_last_TCC2 0 (sigma_last_TCC2-1 nil 3351939915 ("" (skosimp*) (("" (use "T_pred_lem") (("" (assert) nil nil)) nil)) nil) ((T_pred_lem formula-decl nil sigma_2D nil) (T_high type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil sigma_2D nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (T_low type-eq-decl nil sigma_2D nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (sigma_last 0 (sigma_last-1 nil 3255975799 ("" (skosimp*) (("" (rewrite "sigma") (("" (assert) (("" (expand "sigma") (("" (lift-if) (("" (ground) (("" (expand "+ ") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma def-decl "Vector" sigma_2D nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma_2D nil) (T_high type-eq-decl nil sigma_2D nil) (Vector type-eq-decl nil vectors_2D nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (add_zero_right formula-decl nil vectors_2D nil) (add_zero_left formula-decl nil vectors_2D nil) (+ const-decl "Vector" vectors_2D nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (sigma_middle_TCC1 0 (sigma_middle_TCC1-1 nil 3256039673 ("" (skosimp* t) (("" (prop) (("1" (inst + "high!1") (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (inst + "high!1") (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (inst + "j!1") (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (inst + "j!2") (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (high!1 skolem-const-decl "T_high" sigma_2D nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil)) shostak)) (sigma_middle_TCC2 0 (sigma_middle_TCC2-1 nil 3256039673 ("" (skosimp*) (("" (inst + "i!1") (("" (assert) nil nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (sigma_middle 0 (sigma_middle-1 nil 3256032001 ("" (skosimp*) (("" (lemma "sigma_split") (("" (inst?) (("" (inst -1 "i!1") (("" (assert) (("" (rewrite "sigma_rew" -) (("" (assert) (("" (replace -1) (("" (hide -1) (("" (expand "sigma" 1 1) (("" (ground) (("" (expand "sigma") (("" (expand "+ ") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma_split formula-decl nil sigma_2D nil) (sigma_rew formula-decl nil sigma_2D nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma def-decl "Vector" sigma_2D nil) (+ const-decl "Vector" vectors_2D nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (T_low type-eq-decl nil sigma_2D nil) (T_high type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D nil) (T formal-subtype-decl nil sigma_2D nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (sigma_const 0 (sigma_const-1 nil 3255975799 ("" (skolem 1 (_ _ x)) (("" (rewrite "high_low_rewrite") (("" (hide 2) (("" (skosimp*) (("" (prop) (("1" (expand "sigma") (("1" (assert) nil nil)) nil) ("2" (induct "n" 2) (("1" (rewrite "sigma_eq_arg") (("1" (assert) (("1" (expand "const_vec") (("1" (expand "*") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "sigma" +) (("2" (assert) (("2" (replace -2) (("2" (hide -2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 3) (("3" (skosimp*) (("3" (inst + "high!1") (("1" (assert) nil nil) ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_plus_int_is_int application-judgement "int" integers nil) (high_low_rewrite formula-decl nil sigma_2D nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil) (pred type-eq-decl nil defined_types nil) (Vector type-eq-decl nil vectors_2D nil) (= const-decl "[T, T -> boolean]" equalities nil) (sigma def-decl "Vector" sigma_2D nil) (const_vec const-decl "Vector" vectors_2D nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (>= const-decl "bool" reals nil) (* const-decl "Vector" vectors_2D nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (zero const-decl "Vector" vectors_2D nil) (int_minus_int_is_int application-judgement "int" integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (low!1 skolem-const-decl "T_low" sigma_2D nil) (high!1 skolem-const-decl "T_high" sigma_2D nil) (subrange type-eq-decl nil integers nil) (subrange_induction formula-decl nil subrange_inductions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (T_pred_lem formula-decl nil sigma_2D nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (scal_1 formula-decl nil vectors_2D nil) (sigma_eq_arg formula-decl nil sigma_2D nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (+ const-decl "Vector" vectors_2D nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (sigma_zero 0 (sigma_zero-1 nil 3255975799 ("" (skosimp*) (("" (lemma "sigma_const") (("" (inst - "high!1" "low!1" "0") (("" (assert) (("" (case-replace "const_vec(0) = zero") (("1" (assert) nil nil) ("2" (invoke (hide ($+n)) (? * "sigma")) (("2" (expand "const_vec") (("2" (expand "zero") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma_const formula-decl nil sigma_2D nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (scal_zero formula-decl nil vectors_2D nil) (int_plus_int_is_int application-judgement "int" integers nil) (Vector type-eq-decl nil vectors_2D nil) (= const-decl "[T, T -> boolean]" equalities nil) (const_vec const-decl "Vector" vectors_2D nil) (zero const-decl "Vector" vectors_2D nil) (T_low type-eq-decl nil sigma_2D nil) (T_high type-eq-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil sigma_2D nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil)) (sigma_scal 0 (sigma_scal-1 nil 3255975799 ("" (skolem 1 ("F" "a" _ _)) (("" (rewrite "high_low_rewrite") (("" (hide 2) (("" (skosimp*) (("" (prop) (("1" (expand "sigma") (("1" (assert) nil nil)) nil) ("2" (induct "n" 2) (("1" (rewrite "sigma_eq_arg") (("1" (rewrite "sigma_eq_arg") nil nil) ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "sigma" +) (("2" (assert) (("2" (replace -2 * lr) (("2" (hide -2) (("2" (apply-extensionality 1 :hide? t) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (inst + "high!1") (("1" (assert) nil nil) ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil)) nil)) nil) ("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((high_low_rewrite formula-decl nil sigma_2D nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil) (pred type-eq-decl nil defined_types nil) (Vector type-eq-decl nil vectors_2D nil) (= const-decl "[T, T -> boolean]" equalities nil) (sigma def-decl "Vector" sigma_2D nil) (* const-decl "Vector" vectors_2D nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (low!1 skolem-const-decl "T_low" sigma_2D nil) (high!1 skolem-const-decl "T_high" sigma_2D nil) (subrange type-eq-decl nil integers nil) (subrange_induction formula-decl nil subrange_inductions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (>= const-decl "bool" reals nil) (T_pred_lem formula-decl nil sigma_2D nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_eq_arg formula-decl nil sigma_2D nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "Vector" vectors_2D nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (scal_zero formula-decl nil vectors_2D nil)) nil)) (sigma_shift_T_TCC1 0 (sigma_shift_T_TCC1-1 nil 3255975799 ("" (skosimp* t) (("" (prop) (("1" (inst - "low!1") nil nil) ("2" (skosimp*) (("2" (inst + "j!1+z!1") (("1" (assert) nil nil) ("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ((low!1 skolem-const-decl "T_low" sigma_2D nil) (int_plus_int_is_int application-judgement "int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (j!1 skolem-const-decl "T" sigma_2D nil) (z!1 skolem-const-decl "int" sigma_2D nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma_2D nil)) nil)) (sigma_shift_T_TCC2 0 (sigma_shift_T_TCC2-1 nil 3351939915 ("" (skosimp* t) (("" (prop) (("1" (inst?) nil nil) ("2" (skosimp*) (("2" (inst + "z!1+j!1") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ((high!1 skolem-const-decl "T_high" sigma_2D nil) (int_plus_int_is_int application-judgement "int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (j!1 skolem-const-decl "T" sigma_2D nil) (z!1 skolem-const-decl "int" sigma_2D nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma_2D nil)) nil)) (sigma_shift_T_TCC3 0 (sigma_shift_T_TCC3-1 nil 3352113941 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil)) (sigma_shift_T 0 (sigma_shift_T-1 nil 3255975799 ("" (skolem 1 ("F" _ _ "z")) (("" (rewrite "high_low_rewrite") (("1" (hide 2) (("1" (skosimp*) (("1" (prop) (("1" (expand "sigma") (("1" (assert) nil nil)) nil) ("2" (induct "n" 2) (("1" (skosimp*) (("1" (rewrite "sigma_eq_arg") (("1" (rewrite "sigma_eq_arg") (("1" (hide -1 2) (("1" (use "T_pred_lem") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (inst?) (("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "sigma" +) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) nil nil) ("4" (hide-all-but 1) (("4" (skosimp* t) (("4" (typepred "high!1") (("4" (prop) (("1" (inst + "high!1") nil nil) ("2" (skosimp*) (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide -1 2 3) (("5" (skosimp* t) (("5" (typepred "high!1") (("5" (prop) (("1" (inst + "high!1+z") (("1" (assert) nil nil) ("2" (inst?) nil nil)) nil) ("2" (skosimp*) (("2" (inst + "j!1+z") (("1" (assert) nil nil) ("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (hide -1 2 3) (("6" (skosimp* t) (("6" (assert) (("6" (typepred "low!1") (("6" (prop) (("1" (inst?) nil nil) ("2" (skosimp*) (("2" (inst + "j!1+z") (("1" (assert) nil nil) ("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("7" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) nil nil) ("3" (hide 2) (("3" (skosimp* t) (("3" (hide -1 -4) (("3" (assert) (("3" (prop) (("1" (typepred "high!1") (("1" (prop) (("1" (assert) (("1" (inst?) nil nil)) nil) ("2" (skosimp*) (("2" (inst + "j!1+z") (("1" (assert) nil nil) ("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "high!1") (("2" (prop) (("1" (inst?) nil nil) ("2" (skosimp*) (("2" (inst + "j!2+z") (("1" (assert) nil nil) ("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp* t) (("4" (hide -1) (("4" (inst?) (("4" (assert) (("4" (skosimp*) (("4" (reveal -1) (("4" (inst + "j!1+z") (("1" (assert) nil nil) ("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_plus_int_is_int application-judgement "int" integers nil) (high_low_rewrite formula-decl nil sigma_2D nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" sigma_2D nil) (T formal-subtype-decl nil sigma_2D nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma_2D nil) (T_low type-eq-decl nil sigma_2D nil) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (Vector type-eq-decl nil vectors_2D nil) (= const-decl "[T, T -> boolean]" equalities nil) (sigma def-decl "Vector" sigma_2D nil) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.68 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
