| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/reals/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 165 kB |
|
Quelle sigma_nat.prf Sprache: Lisp |
|||||||||
|
(sigma_nat
(IMP_sigma_TCC1 0 (IMP_sigma_TCC1-1 nil 3620720752 ("" (assuming-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) (>= 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (integer nonempty-type-from-decl nil integers 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)) nil)) (int_is_T_high 0 (int_is_T_high-1 nil 3352138082 ("" (skosimp*) (("" (inst-cp + 0) (("" (inst + "x!1") (("1" (assert) nil nil) ("2" (assert) 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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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)) (nat_is_T_low 0 (nat_is_T_low-1 nil 3352138082 ("" (judgement-tcc) nil nil) nil nil)) (sigma_shift_TCC1 0 (sigma_shift_TCC1-1 nil 3403006081 ("" (skosimp*) (("" (assert) nil nil)) 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)) (sigma_shift 0 (sigma_shift-1 nil 3308675684 ("" (skosimp*) (("" (rewrite "sigma_shift_T") nil nil)) nil) ((nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (sigma_shift_T formula-decl nil sigma nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma nil) (T_low type-eq-decl nil sigma nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) nil)) (sigma_shift_neg_TCC1 0 (sigma_shift_neg_TCC1-1 nil 3308675684 ("" (skosimp*) (("" (inst + 0) (("" (assert) nil nil)) nil)) nil) nil nil)) (sigma_shift_neg_TCC2 0 (sigma_shift_neg_TCC2-1 nil 3352138082 ("" (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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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)) (sigma_shift_neg_TCC3 0 (sigma_shift_neg_TCC3-1 nil 3403006081 ("" (skosimp*) (("" (assert) nil nil)) 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (sigma_shift_neg 0 (sigma_shift_neg-1 nil 3308675684 ("" (skosimp*) (("" (lemma "sigma_shift_T2") (("" (inst?) (("" (inst - "high!1" "low!1" "0 - m!1") (("" (assert) (("" (prop) (("1" (replace -1 :hide? t) (("1" (rewrite "sigma_eq") (("1" (skosimp*) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (case "high!1 (("1" (expand "sigma") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sigma_shift_T2 formula-decl nil sigma nil) (int_minus_int_is_int application-judgement "int" integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma nil) (T_low type-eq-decl nil sigma nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (sigma_eq formula-decl nil sigma nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma def-decl "real" sigma nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil)) (sigma_shift_ng2 0 (sigma_shift_ng2-1 nil 3308675684 ("" (skosimp*) (("" (lemma "sigma_shift_T2") (("" (inst?) (("" (inst - "high!1" "low!1" "0-m!1") (("" (assert) (("" (prop) (("1" (replace -1 :hide? t) (("1" (rewrite "sigma_eq") (("1" (expand "~") (("1" (assert) (("1" (skosimp*) (("1" (assert) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "high!1 (("1" (expand "sigma") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sigma_shift_T2 formula-decl nil sigma nil) (int_minus_int_is_int application-judgement "int" integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma nil) (T_low type-eq-decl nil sigma nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (~ const-decl "nat" naturalnumbers nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (sigma_eq formula-decl nil sigma nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma def-decl "real" sigma nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (< const-decl "bool" reals 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)) (sigma_shift_i_TCC1 0 (sigma_shift_i_TCC1-1 nil 3410183793 ("" (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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_plus_int_is_int application-judgement "int" integers 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)) nil)) (sigma_shift_i_TCC2 0 (sigma_shift_i_TCC2-1 nil 3410183793 ("" (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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_plus_int_is_int application-judgement "int" integers 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)) nil)) (sigma_shift_i_TCC3 0 (sigma_shift_i_TCC3-1 nil 3410183793 ("" (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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (sigma_shift_i 0 (sigma_shift_i-1 nil 3410183811 ("" (skosimp*) (("" (rewrite "sigma_shift_T2") (("1" (rewrite "sigma_restrict_eq") (("1" (hide 2) (("1" (expand "restrict") (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("2" (case "low!1 <= high!1") (("1" (assert) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil) ((sigma_shift_T2 formula-decl nil sigma nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma nil) (T_low type-eq-decl nil sigma nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_plus_int_is_int application-judgement "int" integers 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (restrict const-decl "[T -> real]" sigma nil) (< const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (sigma_restrict_eq formula-decl nil sigma nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (sigma def-decl "real" sigma nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (sigma_shift_to_zero_TCC1 0 (sigma_shift_to_zero_TCC1-1 nil 3594380184 ("" (subtype-tcc) nil nil) nil nil)) (sigma_shift_to_zero_TCC2 0 (sigma_shift_to_zero_TCC2-1 nil 3594380184 ("" (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) (>= 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) (nat nonempty-type-eq-decl nil naturalnumbers 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_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (sigma_shift_to_zero 0 (sigma_shift_to_zero-1 nil 3594380186 ("" (induct "n") (("1" (skeep) (("1" (assert) (("1" (rewrite "sigma_restrict_eq") (("1" (decompose-equality 1) (("1" (expand "restrict") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (induct "m") (("1" (assert) nil nil) ("2" (skolem 1 "kk") (("2" (flatten) (("2" (assert) (("2" (skeep) (("2" (assert) (("2" (inst - "F") (("2" (case "NOT 1+j <=kk") (("1" (case "NOT kk=j") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) (("2" (expand "sigma" +) (("2" (expand "sigma" +) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "sigma" 1 1) (("2" (replace -2 +) (("2" (assert) (("2" (expand "sigma" 1 2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (int_plus_int_is_int application-judgement "int" integers nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (j skolem-const-decl "nat" sigma_nat nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (sigma_restrict_eq formula-decl nil sigma nil) (restrict const-decl "[T -> real]" sigma nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nat_induction formula-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma def-decl "real" sigma nil) (T_high type-eq-decl nil sigma nil) (T_low type-eq-decl nil sigma nil) (= const-decl "[T, T -> boolean]" equalities nil) (pred type-eq-decl nil defined_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (OR 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_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil)) shostak)) (sigma_first_ge 0 (sigma_first_ge-1 nil 3308675684 ("" (skosimp*) (("" (rewrite "sigma_first") nil nil)) nil) ((sigma_first formula-decl nil sigma nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma nil) (T_low type-eq-decl nil sigma nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) nil)) (sigma_split_ge_TCC1 0 (sigma_split_ge_TCC1-1 nil 3352162210 ("" (skosimp*) (("" (inst + 0) (("" (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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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)) (sigma_split_ge_TCC2 0 (sigma_split_ge_TCC2-1 nil 3403006081 ("" (skosimp*) (("" (assert) nil nil)) nil) ((int_plus_int_is_int application-judgement "int" integers 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)) (sigma_split_ge 0 (sigma_split_ge-1 nil 3308675684 ("" (skosimp*) (("" (rewrite "sigma_split") nil nil)) nil) ((sigma_split formula-decl nil sigma nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma nil) (T_low type-eq-decl nil sigma nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) nil)) (sigma_reverse_TCC1 0 (sigma_reverse_TCC1-1 nil 3481027293 ("" (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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil)) (sigma_reverse 0 (sigma_reverse-1 nil 3481027293 ("" (case "FORALL (F: [nat -> real], k: nat, low: nat): sigma(low, low+k, F) = sigma(low, low+k, LAMBDA (n: nat): IF n > k + 2*low THEN 0 ELSE F(2*low+k - n) ENDIF)") (("1" (skeep) (("1" (case "high < low") (("1" (expand "sigma" +) (("1" (assert) nil nil)) nil) ("2" (inst - "F" "high-low" "low") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "k") (("1" (skeep) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (skeep) (("2" (skeep) (("2" (inst - "F" "low") (("2" (expand "sigma" 1 1) (("2" (lemma "sigma_split") (("2" (inst - "LAMBDA (n: nat): IF n > 1 + j + 2 * low THEN 0 ELSE F(1 - n + j + 2 * low) ENDIF" "1+j+low" "low" "low") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (expand "sigma" + 3) (("1" (expand "sigma" + 3) (("1" (lemma "sigma_shift") (("1" (inst - "LAMBDA (n: nat): IF n > 1 + j + 2 * low THEN 0 ELSE F(1 - n + j + 2 * low) ENDIF" "low+j" "low" "1") (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (rewrite "sigma_restrict_eq") (("1" (hide 2) (("1" (decompose-equality) (("1" (expand "restrict") (("1" (propax) nil nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ((sigma_split formula-decl nil sigma nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (sigma_restrict_eq formula-decl nil sigma nil) (restrict const-decl "[T -> real]" sigma nil) (sigma_shift formula-decl nil sigma_nat nil) (low skolem-const-decl "nat" sigma_nat nil) (j skolem-const-decl "nat" sigma_nat nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (high skolem-const-decl "int" sigma_nat nil) (low skolem-const-decl "nat" sigma_nat nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_minus_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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma nil) (T_high type-eq-decl nil sigma nil) (sigma def-decl "real" sigma nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (> const-decl "bool" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil)) shostak)) (sigma_product_TCC1 0 (sigma_product_TCC1-1 nil 3541327761 ("" (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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (sigma_product_TCC2 0 (sigma_product_TCC2-1 nil 3541327761 ("" (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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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_lt_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)) nil)) (sigma_product 0 (sigma_product-1 nil 3541327793 ("" (case "FORALL (F, G: [nat -> real], high1, high2: int, low1, low2,rn: nat): rn = high1-low1 IMPLIES sigma(low1, high1, F) * sigma(low2, high2, G) = sigma(low1 + low2, high1 + high2, LAMBDA (k: nat): sigma(low1, high1, LAMBDA (i: nat): IF (i < k - high2 OR i > k - low2) THEN 0 ELSE F(i) * G(k - i) ENDIF))") (("1" (skeep) (("1" (case "high1 >= low1") (("1" (inst?) (("1" (inst - "high1-low1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide -) (("2" (expand "sigma" + 1) (("2" (assert) (("2" (assert) (("2" (case "FORALL (eg1:real): 0*eg1 = 0") (("1" (rewrite -1) (("1" (hide -1) (("1" (rewrite "sigma_restrict_eq_0") (("1" (hide 3) (("1" (skosimp*) (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (grind) nil nil)) nil) ("3" (hide 3) (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "rn") (("1" (skeep) (("1" (case "high1 = low1") (("1" (replace -1) (("1" (assert) (("1" (expand "sigma" + 1) (("1" (expand "sigma" + 2) (("1" (rewrite "sigma_scal" :dir rl) (("1" (expand "sigma" + 3) (("1" (expand "sigma" + 3) (("1" (assert) (("1" (lemma "sigma_shift") (("1" (invoke (inst - "%1" _ _ _) (! 1 2 3)) (("1" (inst - "high2" "low2" "low1") (("1" (replace -1) (("1" (hide -1) (("1" (rewrite "sigma_eq") nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (skeep) (("2" (skeep) (("2" (case "high1 >= low1 AND high2 >= low2") (("1" (flatten) (("1" (inst - "F" "G" "high1-1" "high2" "low1" "low2") (("1" (assert) (("1" (expand "sigma" + 1) (("1" (replace -3) (("1" (hide -3) (("1" (expand "sigma" + 5) (("1" (lemma "sigma_sum") (("1" (inst - "LAMBDA (k: nat): IF (high1 < k - high2 OR high1 > k - low2) THEN 0 ELSE F(high1) * G(k - high1) ENDIF" "LAMBDA (k: nat): sigma(low1, high1 - 1, LAMBDA (i: nat): IF (i < k - high2 OR i > k - low2) THEN 0 ELSE F(i) * G(k - i) ENDIF)" "high1+high2" "low1+low2") (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (case "FORALL (a1,a2,b1,b2:real): a1=b1 AND a2=b2 IMPLIES a1+a2=b2+b1") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (split +) (("1" (expand "sigma" + 3) (("1" (lemma "sigma_restrict_eq_0") (("1" (inst?) (("1" (assert) nil nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "sigma_split") (("2" (inst - "LAMBDA (k: nat): IF (high1 < k - high2 OR high1 > k - low2) THEN 0 ELSE F(high1) * G(k - high1) ENDIF" "high1+high2" "low1+low2" "high1+low2-1") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (case "NOT sigma(low1 + low2, high1 - 1 + low2, LAMBDA (k: nat): IF (high1 < k - high2 OR high1 > k - low2) THEN 0 ELSE F(high1) * G(k - high1) ENDIF) = 0") (("1" (hide 2) (("1" (rewrite "sigma_restrict_eq_0") nil nil)) nil) ("2" (replaces -1) (("2" (assert) (("2" (lemma "sigma_shift") (("2" (inst - "LAMBDA (k: nat): IF (high1 < k - high2 OR high1 > k - low2) THEN 0 ELSE F(high1) * G(k - high1) ENDIF" "high2" "low2" "high1") (("1" (replace -1) (("1" (hide -1) (("1" (rewrite "sigma_scal" :dir rl) (("1" (rewrite "sigma_eq") nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (ground) (("2" (expand "sigma" + 2) (("2" (rewrite "sigma_restrict_eq_0") (("1" (hide 3) (("1" (skosimp*) (("1" (rewrite "sigma_restrict_eq_0") (("1" (hide 2) (("1" (skosimp*) (("1" (assert) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp*) (("6" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp*) (("6" (assert) nil nil)) nil)) nil)) nil) ((sigma_sum formula-decl nil sigma nil) (real_plus_real_is_real application-judgement "real" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_split formula-decl nil sigma nil) (low2 skolem-const-decl "nat" sigma_nat nil) (high2 skolem-const-decl "int" sigma_nat nil) (high1 skolem-const-decl "int" sigma_nat nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (subrange type-eq-decl nil integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma_scal formula-decl nil sigma nil) (sigma_shift formula-decl nil sigma_nat nil) (sigma_eq formula-decl nil sigma nil) (low1 skolem-const-decl "nat" sigma_nat nil) (high2 skolem-const-decl "int" sigma_nat nil) (low2 skolem-const-decl "nat" sigma_nat nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma_restrict_eq_0 formula-decl nil sigma nil) (low1 skolem-const-decl "nat" sigma_nat nil) (high1 skolem-const-decl "int" sigma_nat nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities 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) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma nil) (T_high type-eq-decl nil sigma nil) (sigma def-decl "real" sigma nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (< const-decl "bool" reals nil) (> const-decl "bool" reals nil)) shostak)) (sigma_tolambda 0 (sigma_tolambda-1 nil 3620720753 ("" (skeep) (("" (rewrite "sigma_eq") nil nil)) nil) ((sigma_eq formula-decl nil sigma nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma nil) (T_low type-eq-decl nil sigma nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) shostak)) (sigma_bij_TCC1 0 (sigma_bij_TCC1-1 nil 3620667440 ("" (subtype-tcc) nil nil) nil nil)) (sigma_bij_TCC2 0 (sigma_bij_TCC2-1 nil 3620667440 ("" (subtype-tcc) nil nil) nil nil)) (sigma_bij 0 (sigma_bij-1 nil 3620667441 ("" (skeep) (("" (label "ontoz" -2) (("" (label "rangez" -1) (("" (label "injz" -3) (("" (case "NOT low<=high") (("1" (expand "sigma" +) (("1" (assert) nil nil)) nil) ("2" (name "FF" "LAMBDA (k:nat): (LAMBDA (i:nat): IF low<=i AND i<=low+k THEN F(i) ELSE 0 ENDIF)") (("2" (case "FORALL (k:nat): low+k<=high IMPLIES sigma(low,high, FF(k)) = sigma(low,high,FF(k) o sig)") (("1" (inst - "high-low") (("1" (assert) (("1" (case "sigma(low, high, FF(high - low)) = sigma(low, high,F) AND sigma(low, high (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (split 1) (("1" (rewrite "sigma_eq" 1) (("1" (skosimp*) (("1" (typepred "n!1") (("1" (expand "FF" 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite "sigma_eq" 1) (("2" (expand "o") (("2" (skosimp*) (("2" (expand "FF" 1) (("2" (lift-if) (("2" (inst - "n!1") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (hide 2) (("2" (induct "k") (("1" (assert) (("1" (inst -4 "low") (("1" (skosimp*) (("1" (lemma "sigma_eq_one_arg") (("1" (inst?) (("1" (inst - "low") (("1" (assert) (("1" (split -) (("1" (replaces -1) (("1" (lemma "sigma_eq_one_arg") (("1" (inst?) (("1" (inst - "j!1") (("1" (assert) (("1" (split -) (("1" (replaces -1) (("1" (expand "o") (("1" (assert) nil nil)) nil)) nil) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.36 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28