| products/Sources/formale Sprachen/PVS/reals/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: product.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(product
(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" product nil) (high!1 skolem-const-decl "T_high" product 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 product 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]" product nil) (T formal-subtype-decl nil product nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil product nil) (T_low type-eq-decl nil product 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" product nil) (T_high type-eq-decl nil product nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil product nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (T_pred const-decl "[int -> boolean]" product 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 product nil) (T_pred_lem formula-decl nil product 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]" product nil) (T formal-subtype-decl nil product nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil product nil) (T_low type-eq-decl nil product 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" product nil) (low!1 skolem-const-decl "T_low" product nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (product_TCC1 0 (product_TCC1-1 nil 3410094710 ("" (skosimp*) (("" (typepred "low!1") (("" (typepred "high!1") (("" (assert) (("" (skosimp*) (("" (typepred "j!1") (("" (lemma "connected_domain") (("" (inst - "low!1" "j!1" "high!1") (("1" (assert) nil nil) ("2" (assert) (("2" (skosimp*) (("2" (lemma "connected_domain") (("2" (inst - "j!2" "j!1" "low!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T_low type-eq-decl nil product nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil product nil) (T_pred const-decl "[int -> boolean]" product 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_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (low!1 skolem-const-decl "T_low" product 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 product nil) (T_high type-eq-decl nil product nil)) nil)) (product_TCC2 0 (product_TCC2-1 nil 3410094710 ("" (skeep) (("" (typepred "high") (("" (typepred "low") (("" (assert) (("" (ground) (("1" (inst + "high") (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (inst + "high") (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (inst + "j!1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T_high type-eq-decl nil product nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil product nil) (T_pred const-decl "[int -> boolean]" product 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) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (T_low type-eq-decl nil product nil)) nil)) (product_TCC3 0 (product_TCC3-1 nil 3410094710 ("" (termination-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) (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]" product nil) (T formal-subtype-decl nil product nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil product nil) (T_high type-eq-decl nil product 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) (int_minus_int_is_int application-judgement "int" integers nil) (minus_int_is_int application-judgement "int" integers nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil)) (product_spl_TCC1 0 (product_spl_TCC1-1 nil 3410103726 ("" (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) (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]" product nil) (T formal-subtype-decl nil product nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil product nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil)) (product_spl_TCC2 0 (product_spl_TCC2-1 nil 3410103726 ("" (skeep) (("" (inst + "low + nn + rng") (("" (assert) nil nil)) nil)) nil) ((int_plus_int_is_int application-judgement "int" integers nil) (rng skolem-const-decl "nat" product nil) (nn skolem-const-decl "nat" product nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (low skolem-const-decl "T_low" product nil) (T_low type-eq-decl nil product nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil product 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]" product 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)) (product_spl_TCC3 0 (product_spl_TCC3-1 nil 3410103726 ("" (skeep) (("" (typepred "low") (("" (split -1) (("1" (inst + "low") (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((T_low type-eq-decl nil product nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil product nil) (T_pred const-decl "[int -> boolean]" product 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) (low skolem-const-decl "T_low" product nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (product_spl 0 (product_spl-1 nil 3410103740 ("" (induct "rng") (("1" (assert) (("1" (expand "product") (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "product" + (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) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (inst + "low!1+nn!1") (("1" (assert) nil nil) ("2" (lemma "T_pred_lem") (("2" (inst?) (("2" (inst - "low!1+nn!1+rng!2" "low!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (inst + "low!1+nn!1+rng!2") (("4" (assert) nil nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp*) nil nil)) nil)) nil) ((low!1 skolem-const-decl "T_low" product nil) (nn!1 skolem-const-decl "nat" product nil) (rng!2 skolem-const-decl "nat" product nil) (low!1 skolem-const-decl "T_low" product nil) (nn!1 skolem-const-decl "nat" product nil) (rng!2 skolem-const-decl "nat" product nil) (T_pred_lem formula-decl nil product nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nat_induction formula-decl nil naturalnumbers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (product def-decl "real" product nil) (T_high type-eq-decl nil product nil) (= const-decl "[T, T -> boolean]" equalities nil) (pred type-eq-decl nil defined_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" product nil) (T formal-subtype-decl nil product nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil product 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)) (product_split_TCC1 0 (product_split_TCC1-1 nil 3410103726 ("" (skeep) (("" (typepred "high") (("" (assert) (("" (split -1) (("1" (inst + "high") nil nil) ("2" (skosimp*) (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T_high type-eq-decl nil product nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil product nil) (T_pred const-decl "[int -> boolean]" product nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (high skolem-const-decl "T_high" product nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (product_split_TCC2 0 (product_split_TCC2-1 nil 3410103726 ("" (skeep) (("" (typepred "low") (("" (split -1) (("1" (inst + "low") (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((T_low type-eq-decl nil product nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil product nil) (T_pred const-decl "[int -> boolean]" product 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) (low skolem-const-decl "T_low" product 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)) nil)) (product_split 0 (product_split-1 nil 3410103810 ("" (skosimp*) (("" (case "high!1 (("1" (expand "product") (("1" (assert) nil nil)) nil) ("2" (case-replace "z!1=low!1-1") (("1" (assert) (("1" (expand "product") (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "product_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 product nil) (T_high type-eq-decl nil product nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil product nil) (T_pred const-decl "[int -> boolean]" product nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (product def-decl "real" product nil) (product_spl formula-decl nil product nil) (T_pred_lem formula-decl nil product nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (high!1 skolem-const-decl "T_high" product nil) (low!1 skolem-const-decl "T_low" product nil) (z!1 skolem-const-decl "int" product 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)) (product_div 0 (product_div-1 nil 3410104326 ("" (skeep) (("" (cross-mult 2) (("" (lemma "product_split") (("" (inst - "F" "high" "low" "z") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((real_div_nzreal_is_real application-judgement "real" reals nil) (div_cancel3 formula-decl nil real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (product def-decl "real" product nil) (T_high type-eq-decl nil product nil) (T_low type-eq-decl nil product nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil product nil) (T_pred const-decl "[int -> boolean]" product 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) (nonzero_real nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (product_split formula-decl nil product nil)) shostak)) (product_div_neg 0 (product_div_neg-1 nil 3410104551 ("" (skeep) (("" (cross-mult 2) (("" (lemma "product_split") (("" (inst - "F" "high" "low" "z") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((int_plus_int_is_int application-judgement "int" integers 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]" product nil) (T formal-subtype-decl nil product nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil product nil) (T_low type-eq-decl nil product 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_div_nzreal_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (product_split formula-decl nil product nil)) shostak)) (product_eq_arg 0 (product_eq_arg-1 nil 3410104588 ("" (skosimp*) (("" (expand "product") (("" (expand "product") (("" (propax) nil nil)) nil)) nil)) nil) ((product def-decl "real" product nil)) shostak)) (product_first_TCC1 0 (product_first_TCC1-1 nil 3410104637 ("" (skeep) (("" (typepred "low") (("" (assert) (("" (skosimp*) (("" (typepred "high") (("" (assert) (("" (split -1) (("1" (lemma "connected_domain") (("1" (assert) (("1" (inst - "j!1" "high" "low") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "connected_domain") (("2" (inst - "j!1" "j!2" "low") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T_low type-eq-decl nil product nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil product nil) (T_pred const-decl "[int -> boolean]" product nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (connected_domain formula-decl nil product nil) (integer nonempty-type-from-decl nil integers nil) (T_high type-eq-decl nil product nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (product_first_TCC2 0 (product_first_TCC2-1 nil 3410104637 ("" (skeep) (("" (typepred "low") (("" (assert) (("" (split -1) (("1" (inst + "low") (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T_low type-eq-decl nil product nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil product nil) (T_pred const-decl "[int -> boolean]" product 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) (low skolem-const-decl "T_low" product nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil)) (product_first 0 (product_first-1 nil 3410104659 ("" (skosimp*) (("" (lemma "product_split") (("" (inst?) (("" (inst -1 "low!1") (("" (rewrite "product_eq_arg") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((product_split formula-decl nil product 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_times_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (product_eq_arg formula-decl nil product nil) (T_low type-eq-decl nil product nil) (T_high type-eq-decl nil product 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 product nil) (T_pred const-decl "[int -> boolean]" product 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)) (product_last_TCC1 0 (product_last_TCC1-1 nil 3410104637 ("" (skeep) (("" (typepred "high") (("" (split -1) (("1" (inst + "high") (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((T_high type-eq-decl nil product nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil product nil) (T_pred const-decl "[int -> boolean]" product nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (high skolem-const-decl "T_high" product nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (product_last_TCC2 0 (product_last_TCC2-1 nil 3410104637 ("" (skeep) (("" (typepred "high") (("" (assert) (("" (skosimp*) (("" (lemma "connected_domain") (("" (inst - "low" "j!1" "high") (("1" (assert) nil nil) ("2" (typepred "low") (("2" (assert) (("2" (skosimp*) (("2" (lemma "connected_domain") (("2" (assert) (("2" (inst - "j!2" "j!1" "low") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T_high type-eq-decl nil product nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil product nil) (T_pred const-decl "[int -> boolean]" product 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) (T_low type-eq-decl nil product nil) (low skolem-const-decl "T_low" product 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 product nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (product_last 0 (product_last-1 nil 3410104722 ("" (skosimp*) (("" (rewrite "product") (("" (assert) nil nil)) nil)) nil) ((product def-decl "real" product 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]" product nil) (T formal-subtype-decl nil product nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil product nil) (T_high type-eq-decl nil product nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (product_middle_TCC1 0 (product_middle_TCC1-1 nil 3410104812 ("" (skeep) (("" (typepred "i") (("" (inst + "i") (("" (assert) nil nil)) nil)) nil)) nil) ((T formal-subtype-decl nil product nil) (T_pred const-decl "[int -> boolean]" product 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) (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) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (product_middle_TCC2 0 (product_middle_TCC2-1 nil 3410104812 ("" (skeep) (("" (typepred "i") (("" (inst + "i") (("" (assert) nil nil)) nil)) nil)) nil) ((T formal-subtype-decl nil product nil) (T_pred const-decl "[int -> boolean]" product 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) (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) (int_plus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (product_middle 0 (product_middle-1 nil 3410104844 ("" (skosimp*) (("" (lemma "product_split") (("" (inst?) (("" (inst -1 "i!1") (("" (assert) (("" (assert) (("" (replace -1) (("" (hide -1) (("" (expand "product" 1 1) (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((product_split formula-decl nil product nil) (product def-decl "real" product nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (T_low type-eq-decl nil product nil) (T_high type-eq-decl nil product 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 product nil) (T_pred const-decl "[int -> boolean]" product 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)) (product_const_TCC1 0 (product_const_TCC1-1 nil 3410104812 ("" (subtype-tcc) nil nil) ((int_plus_int_is_int application-judgement "int" integers nil)) nil)) (product_const 0 (product_const-2 nil 3410105217 ("" (skolem 1 (_ _ nzr)) (("" (rewrite "high_low_rewrite") (("" (hide 2) (("" (skosimp*) (("" (prop) (("1" (expand "product") (("1" (assert) nil nil)) nil) ("2" (induct "n" 2) (("1" (rewrite "product_eq_arg") (("1" (assert) (("1" (expand "^") (("1" (expand "expt") (("1" (expand "expt") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "product" +) (("2" (assert) (("2" (lemma "expt_plus") (("2" (inst - "(1 - low!1 + k!1)" "1" "nzr") (("2" (replace -1) (("2" (hide -1) (("2" (rewrite "expt_x1") (("2" (assert) nil nil)) nil)) 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) ((IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (int_plus_int_is_int application-judgement "int" integers nil) (high_low_rewrite formula-decl nil product 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]" product nil) (T formal-subtype-decl nil product nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil product nil) (T_low type-eq-decl nil product nil) (pred type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (product def-decl "real" product nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (>= const-decl "bool" reals nil) (^ const-decl "real" exponentiation 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) (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" product nil) (high!1 skolem-const-decl "T_high" product 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 product nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (expt def-decl "real" exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (product_eq_arg formula-decl nil product nil) (real_times_real_is_real application-judgement "real" reals nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (expt_x1 formula-decl nil exponentiation nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (expt_plus formula-decl nil exponentiation 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) (product_const-1 nil 3410104877 ("" (skolem 1 (_ _ x)) (("" (rewrite "high_low_rewrite") (("1" (hide 2) (("1" (skosimp*) (("1" (prop) (("1" (expand "product") (("1" (assert) nil nil)) nil) ("2" (induct "n" 2) (("1" (rewrite "product_eq_arg") (("1" (assert) (("1" (expand "^") (("1" (expand "expt") (("1" (expand "expt") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "product" +) (("2" (assert) (("2" (lemma "expt_plus") (("2" (inst - "(1 - low!1 + k!1)" "1" "x") (("1" (replace -1) (("1" (hide -1) (("1" (rewrite "expt_x1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (postpone) nil 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) ("2" (postpone) nil nil)) nil)) nil) nil nil)) (product_zero 0 (product_zero-1 nil 3410105243 ("" (skosimp*) (("" (rewrite "product_first") (("" (assert) nil nil)) nil)) nil) ((product_first formula-decl nil product 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]" product nil) (T formal-subtype-decl nil product nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil product nil) (T_low type-eq-decl nil product nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals 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)) shostak)) (product_scal_TCC1 0 (product_scal_TCC1-1 nil 3410105938 ("" (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) (OR const-decl "[bool, bool -> bool]" booleans 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]" product nil) (T formal-subtype-decl nil product nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil product nil) (T_low type-eq-decl nil product nil) (/= const-decl "boolean" notequal nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil)) (product_scal 0 (product_scal-1 nil 3410105347 ("" (skolem 1 ("F" "a" _ _)) (("" (rewrite "high_low_rewrite") (("1" (hide 2) (("1" (skosimp*) (("1" (ground) (("1" (induct "n" 2) (("1" (rewrite "product_eq_arg") (("1" (rewrite "product_eq_arg") (("1" (assert) (("1" (rewrite "expt_x1") nil nil)) nil)) nil) ("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "product" +) (("2" (assert) (("2" (replace -2) (("2" (hide -2) (("2" (lemma "expt_plus") (("2" (inst - "(1 - low!1 + k!1)" "1" "a") (("2" (assert) (("2" (replace -1) (("2" (hide -1) (("2" (rewrite "expt_x1") (("2" (assert) nil nil)) nil)) nil)) nil)) 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)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) nil nil)) nil)) nil)) nil) ((real_times_real_is_real application-judgement "real" reals nil) (int_plus_int_is_int application-judgement "int" integers nil) (high_low_rewrite formula-decl nil product 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]" product nil) (T formal-subtype-decl nil product nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil product nil) (T_low type-eq-decl nil product 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 "boolean" notequal nil) (= const-decl "[T, T -> boolean]" equalities nil) (product def-decl "real" product nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (>= const-decl "bool" reals nil) (^ const-decl "real" exponentiation nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (low!1 skolem-const-decl "T_low" product nil) (high!1 skolem-const-decl "T_high" product nil) (subrange type-eq-decl nil integers nil) (a skolem-const-decl "real" product 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 product nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (expt_x1 formula-decl nil exponentiation nil) (product_eq_arg formula-decl nil product nil) (nzreal nonempty-type-eq-decl nil reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (expt_plus formula-decl nil exponentiation nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (product_eq_0_TCC1 0 (product_eq_0_TCC1-1 nil 3412957398 ("" (skeep) (("" (skosimp*) (("" (typepred "n!1") (("" (lemma "T_pred_lem") (("" (inst - "high" "low" "n!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((T_pred_lem formula-decl nil product 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) (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) (<= const-decl "bool" 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) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[int -> boolean]" product nil) (T formal-subtype-decl nil product nil) (T_low type-eq-decl nil product nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (T_high type-eq-decl nil product nil) (subrange type-eq-decl nil integers nil)) nil)) (product_eq_0 0 (product_eq_0-1 nil 3412957679 ("" (skolem 1 ("F" _ _)) (("" (rewrite "high_low_rewrite") (("1" (hide 2) (("1" (skosimp*) (("1" (prop) (("1" (expand "product") (("1" (assert) nil nil)) nil) ("2" (induct "n" 2) (("1" (skosimp*) (("1" (rewrite "product_eq_arg") (("1" (inst?) nil nil) ("2" (hide -1 2) (("2" (use "T_pred_lem") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "product" -3) (("2" (mult-cases -3) (("1" (inst?) nil nil) ("2" (skosimp*) (("2" (typepred "n!1") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (hide 3) (("3" (typepred "n!2") (("3" (typepred "n!1") (("3" (lemma "T_pred_lem") (("3" (assert) (("3" (inst - "high!1" "low!1" "n!2") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (typepred "n!1") (("4" (lemma "T_pred_lem") (("4" (inst - "high!1" "low!1" "n!1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ("5" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "n!1") (("2" (lemma "T_pred_lem") (("2" (inst - "high!1" "low!1" "n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((high_low_rewrite formula-decl nil product 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]" product nil) (T formal-subtype-decl nil product nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil product nil) (T_low type-eq-decl nil product nil) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (product def-decl "real" product nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (low!1 skolem-const-decl "T_low" product nil) (high!1 skolem-const-decl "T_high" product nil) (F skolem-const-decl "[T -> real]" product 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) (product_eq_arg formula-decl nil product nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (T_pred_lem formula-decl nil product nil) (int_plus_int_is_int application-judgement "int" integers nil) (zero_times3 formula-decl nil real_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (NOT const-decl "[bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers 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)) shostak)) (product_eq_zero_TCC1 0 (product_eq_zero_TCC1-1 nil 3618849229 ("" (skeep) (("" (typepred "low") (("" (typepred "high") (("" (typepred "n") (("" (lemma "connected_domain") (("" (ground) (("1" (inst - "low" "high" "n") (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (inst - "j!1" "high" "n") (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (inst - "low" "j!1" "n") (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (inst - "j!1" "j!2" "n") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T_low type-eq-decl nil product nil) (<= const-decl "bool" reals nil) (T formal-subtype-decl nil product nil) (T_pred const-decl "[int -> boolean]" product 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) (subrange type-eq-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" 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 product nil) (T_high type-eq-decl nil product nil)) nil)) (product_eq_zero 0 (product_eq_zero-1 nil 3618849033 ("" (skeep) (("" (lemma "product_eq_0") (("" (inst?) (("" (split 1) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.73 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 |
