Quelle  sigma_lemmas.prf

(sigma_lemmas (sigma_restrict_dom_TCC1 0 (sigma_restrict_dom_TCC1-1 nil 3544852161 ("" (subtype-tcc) nil nil) nil nil)) (sigma_restrict_dom_TCC2 0 (sigma_restrict_dom_TCC2-1 nil 3544852161 ("" (subtype-tcc) nil nil) nil nil)) (sigma_restrict_dom_TCC3 0 (sigma_restrict_dom_TCC3-1 nil 3544852161 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers 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_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (sigma_restrict_dom_TCC4 0 (sigma_restrict_dom_TCC4-1 nil 3544852161 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil 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) (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) (integer nonempty-type-from-decl nil integers nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil)) nil)) (sigma_restrict_dom_TCC5 0 (sigma_restrict_dom_TCC5-1 nil 3544852161 ("" (subtype-tcc) nil nil) nil nil)) (sigma_restrict_dom_TCC6 0 (sigma_restrict_dom_TCC6-1 nil 3544852663 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers 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_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (sigma_restrict_dom_TCC7 0 (sigma_restrict_dom_TCC7-1 nil 3544852663 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (integer nonempty-type-from-decl nil integers nil) (below type-eq-decl nil nat_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil)) nil)) (sigma_restrict_dom 0 (sigma_restrict_dom-1 nil 3544863886 ("" (induct "j") (("1" (case "j!1=0") (("1" (hide 1) (("1" (skosimp) (("1" (replace -1) (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (skosimp) (("3" (case "j!1=0") (("1" (hide -2 -3) (("1" (replace -1) (("1" (assert) (("1" (expand "sigma") (("1" (inst -2 "0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1>0") (("1" (assert) (("1" (hide -3 1) (("1" (expand "sigma" 1) (("1" (copy -3) (("1" (inst -1 "j!1") (("1" (replace -1 1) (("1" (assert) (("1" (hide -1) (("1" (inst -2 "m!1" "F!1" "G!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (skosimp) (("4" (assert) nil nil)) nil)) nil) ("5" (skosimp) (("5" (skosimp) (("5" (assert) nil nil)) nil)) nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma_0_neg formula-decl nil sigma_below "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_induction formula-decl nil naturalnumbers nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil)) shostak)) (sigma_restrict_dom2_TCC1 0 (sigma_restrict_dom2_TCC1-1 nil 3544852161 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil 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)) nil)) (sigma_restrict_dom2_TCC2 0 (sigma_restrict_dom2_TCC2-1 nil 3544852161 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil)) nil)) (sigma_restrict_dom2_TCC3 0 (sigma_restrict_dom2_TCC3-1 nil 3544852161 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil 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) (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) (integer nonempty-type-from-decl nil integers nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil)) nil)) (sigma_restrict_dom2_TCC4 0 (sigma_restrict_dom2_TCC4-1 nil 3544852161 ("" (subtype-tcc) nil nil) nil nil)) (sigma_restrict_dom2_TCC5 0 (sigma_restrict_dom2_TCC5-1 nil 3544852663 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (posint_plus_nnint_is_posint application-judgement "posint" 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)) nil)) (sigma_restrict_dom2_TCC6 0 (sigma_restrict_dom2_TCC6-1 nil 3544852663 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (integer nonempty-type-from-decl nil integers nil) (below type-eq-decl nil nat_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil)) nil)) (sigma_restrict_dom2 0 (sigma_restrict_dom2-1 nil 3544864211 ("" (induct "j") (("1" (skosimp) (("1" (case "j!1=0") (("1" (replace -1 2) (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (skosimp) (("3" (case "j!1=0") (("1" (replace -1 1) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (inst -4 "1") nil nil)) nil)) nil)) nil) ("2" (case "j!1>0") (("1" (assert) (("1" (hide -3) (("1" (inst -2 "m!1" "F!1" "G!1") (("1" (assert) (("1" (replace -3 -2) (("1" (lemma "sigma_last[below[j!1]]") (("1" (expand "sigma" 2) (("1" (hide -1) (("1" (inst -3 "1+j!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3 -4 2 3) (("2" (skosimp) (("2" (typepred "y!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (skosimp) (("4" (assert) nil nil)) nil)) nil) ("5" (skosimp) (("5" (skosimp) nil nil)) nil) ("6" (skosimp) (("6" (skosimp) (("6" (assert) nil nil)) nil)) nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (integer nonempty-type-from-decl nil integers nil) (sigma_last formula-decl nil sigma "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_induction formula-decl nil naturalnumbers nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) shostak)) (sigma_below_shift_TCC1 0 (sigma_below_shift_TCC1-1 nil 3544852161 ("" (subtype-tcc) nil nil) nil nil)) (sigma_below_shift_TCC2 0 (sigma_below_shift_TCC2-1 nil 3544852161 ("" (subtype-tcc) nil nil) nil nil)) (sigma_below_shift_TCC3 0 (sigma_below_shift_TCC3-1 nil 3544852161 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil nat_types nil) (integer nonempty-type-from-decl nil 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_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (sigma_below_shift_TCC4 0 (sigma_below_shift_TCC4-1 nil 3544852161 ("" (subtype-tcc) nil nil) nil nil)) (sigma_below_shift_TCC5 0 (sigma_below_shift_TCC5-1 nil 3544852161 ("" (subtype-tcc) nil nil) nil nil)) (sigma_below_shift_TCC6 0 (sigma_below_shift_TCC6-1 nil 3544852663 ("" (subtype-tcc) nil nil) nil nil)) (sigma_below_shift_TCC7 0 (sigma_below_shift_TCC7-1 nil 3544852663 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (integer nonempty-type-from-decl nil 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_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)) nil)) (sigma_below_shift 0 (sigma_below_shift-1 nil 3544864444 ("" (induct "m") (("1" (skosimp) (("1" (typepred "m!1") (("1" (propax) nil nil)) nil)) nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (skosimp) (("3" (case "j!1=0") (("1" (hide -2 -3) (("1" (replace -1) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("1" (lemma "sigma_last[below[2+j!1]]") (("1" (inst -1 " LAMBDA (i: below[2 + j!1]): F!1(i)" "1+j!1" "1") (("1" (assert) (("1" (replace -1 2) (("1" (hide -1) (("1" (lemma "sigma_last[below[1+j!1]]") (("1" (inst -1 " LAMBDA (i: below[1 + j!1]): F!1(1 + i)" "j!1" "0") (("1" (assert) (("1" (replace -1 2) (("1" (assert) (("1" (hide -1) (("1" (inst -1 " LAMBDA (i: below[1 + j!1]): F!1(i)") (("1" (lemma "sigma_restrict_dom") (("1" (inst -1 "j!1" "j!1" "LAMBDA (i_1: below[j!1]): F!1(1 + i_1)" "LAMBDA (i: below[1 + j!1]): F!1(1 + i)") (("1" (assert) (("1" (swap-rel -1) (("1" (replace -1 2) (("1" (hide -1) (("1" (lemma "sigma_restrict_dom2") (("1" (inst -1 "j!1" "1+j!1" " LAMBDA (i_1: below[1 + j!1]): F!1(i_1)" "LAMBDA (i: below[2 + j!1]): F!1(i)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "y!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (skosimp) (("4" (typepred "y!1") (("4" (assert) nil nil)) nil)) nil)) nil) ("5" (skosimp) (("5" (assert) nil nil)) nil) ("6" (skosimp) (("6" (assert) nil nil)) nil) ("7" (skosimp) (("7" (assert) nil nil)) nil)) nil) ((sigma_last formula-decl nil sigma "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_restrict_dom formula-decl nil sigma_lemmas nil) (sigma_restrict_dom2 formula-decl nil sigma_lemmas nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (real_plus_real_is_real application-judgement "real" reals 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (nat_induction formula-decl nil naturalnumbers nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (pred type-eq-decl nil defined_types nil) (integer nonempty-type-from-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil nat_types nil) (<= const-decl "bool" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) shostak)) (sigma_eq_index_TCC1 0 (sigma_eq_index_TCC1-1 nil 3539495453 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil)) nil)) (sigma_eq_index_TCC2 0 (sigma_eq_index_TCC2-1 nil 3539495453 ("" (subtype-tcc) nil nil) nil nil)) (sigma_eq_index_TCC3 0 (sigma_eq_index_TCC3-1 nil 3539495453 ("" (subtype-tcc) nil nil) nil nil)) (sigma_eq_index 0 (teo "fin" 3544864996 ("" (induct "m") (("1" (typepred "m!1") (("1" (propax) nil nil)) nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (typepred "j!1") (("3" (case "j!1=0") (("1" (hide -2 -3 -4) (("1" (skosimp) (("1" (replace -1) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (assert) (("1" (replace -2 1) (("1" (assert) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1>0") (("1" (hide -2 1) (("1" (hide -3) (("1" (assert) (("1" (skosimp) (("1" (swap-rel -3) (("1" (replace -3 1) (("1" (assert) (("1" (lemma "sigma_last[ Index[1 + j!1]]") (("1" (inst -1 " LAMBDA (i: Index[1 + j!1]): F!1(i)" "j!1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_last[Index[n!1]]") (("1" (inst -1 " LAMBDA (i: Index[n!1]): G!1(i)" "j!1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (copy -4) (("1" (inst -1 "j!1") (("1" (replace -1 1) (("1" (hide -1) (("1" (assert) (("1" (inst -2 "n!1-1" " LAMBDA (i: Index[j!1]): F!1(i)" "LAMBDA (i: Index[n!1-1]): G!1(i)") (("1" (assert) (("1" (case " (FORALL (i_1: below[j!1]): F!1(i_1) = G!1(i_1))") (("1" (replace -1 -3) (("1" (hide -1) (("1" (case " sigma(0, j!1 - 1, LAMBDA (i_1: Index[j!1]): F!1(i_1))= sigma(0, j!1 - 1, LAMBDA (i: Index[1 + j!1]): F!1(i))") (("1" (replace -1 -3) (("1" (hide -1) (("1" (case " sigma(0, n!1 - 2, LAMBDA (i_1: Index[n!1 - 1]): G!1(i_1))= sigma(0, n!1 - 2, LAMBDA (i_1: Index[n!1]): G!1(i_1))") (("1" (replace -1 -3) (("1" (hide -1) (("1" (replace -3 -2) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (assert) (("2" (lemma "sigma_restrict_dom") (("2" (inst -1 "n!1-1" "n!1-1" " LAMBDA (i_1: Index[n!1 - 1]): G!1(i_1)" "LAMBDA (i_1: Index[n!1]): G!1(i_1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide -2 -4 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (assert) (("2" (lemma "sigma_restrict_dom") (("2" (inst -1 "j!1" "j!1" "LAMBDA (i_1: Index[j!1]): F!1(i_1)" " LAMBDA (i: Index[1 + j!1]): F!1(i)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide -2 -4 2) (("3" (skosimp) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (skosimp) (("2" (inst -3 "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (hide 2) (("4" (skosimp) (("4" (grind) nil nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp) (("5" (grind) nil nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp) (("6" (grind) nil nil)) nil)) nil) ("7" (hide 2) (("7" (skosimp) (("7" (grind) nil nil)) nil)) nil)) nil) ((real_plus_real_is_real application-judgement "real" reals nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_restrict_dom formula-decl nil sigma_lemmas nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_last formula-decl nil sigma "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (nat_induction formula-decl nil naturalnumbers nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (pred type-eq-decl nil defined_types nil) (integer nonempty-type-from-decl nil integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (Index type-eq-decl nil vectors "vectors/") (<= const-decl "bool" reals 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (int_minus_int_is_int application-judgement "int" integers nil)) shostak) (thm "finished" 3539496088 ("" (induct "m") (("1" (typepred "m!1") (("1" (propax) nil nil)) nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (typepred "j!1") (("3" (case "j!1=0") (("1" (hide -2 -3 -4) (("1" (skosimp) (("1" (replace -1) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (assert) (("1" (replace -2 1) (("1" (assert) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1>0") (("1" (hide -2 1) (("1" (hide -3) (("1" (assert) (("1" (skosimp) (("1" (swap-rel -3) (("1" (replace -3 1) (("1" (assert) (("1" (lemma "sigma_last[ Index[1 + j!1]]") (("1" (inst -1 " LAMBDA (i: Index[1 + j!1]): F!1(i)" "j!1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_last[Index[n!1]]") (("1" (inst -1 " LAMBDA (i: Index[n!1]): G!1(i)" "j!1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (copy -4) (("1" (inst -1 "j!1") (("1" (replace -1 1) (("1" (hide -1) (("1" (assert) (("1" (inst -2 "n!1-1" " LAMBDA (i: Index[j!1]): F!1(i)" "LAMBDA (i: Index[n!1-1]): G!1(i)") (("1" (assert) (("1" (case " (FORALL (i_1: below[j!1]): F!1(i_1) = G!1(i_1))") (("1" (replace -1 -3) (("1" (hide -1) (("1" (case " sigma(0, j!1 - 1, LAMBDA (i_1: Index[j!1]): F!1(i_1))= sigma(0, j!1 - 1, LAMBDA (i: Index[1 + j!1]): F!1(i))") (("1" (replace -1 -3) (("1" (hide -1) (("1" (case " sigma(0, n!1 - 2, LAMBDA (i_1: Index[n!1 - 1]): G!1(i_1))= sigma(0, n!1 - 2, LAMBDA (i_1: Index[n!1]): G!1(i_1))") (("1" (replace -1 -3) (("1" (hide -1) (("1" (replace -3 -2) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (lemma "sigma_restrict_dom[1]") (("2" (inst -1 "n!1-1" "n!1-1" " LAMBDA (i_1: Index[n!1 - 1]): G!1(i_1)" "LAMBDA (i_1: Index[n!1]): G!1(i_1)") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (hide -2 -4 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (lemma "sigma_restrict_dom[1]") (("2" (inst -1 "j!1" "j!1" "LAMBDA (i_1: Index[j!1]): F!1(i_1)" " LAMBDA (i: Index[1 + j!1]): F!1(i)") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (hide -2 -4 2) (("3" (skosimp) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (skosimp) (("2" (inst -3 "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 -4 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 -4 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (hide 2) (("4" (skosimp) (("4" (grind) nil nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp) (("5" (grind) nil nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp) (("6" (grind) nil nil)) nil)) nil) ("7" (hide 2) (("7" (skosimp) (("7" (grind) nil nil)) nil)) nil) ("8" (hide 2) (("8" (skosimp) (("8" (grind) nil nil)) nil)) nil)) nil) ((Index type-eq-decl nil vectors "vectors/") (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (sigma_last formula-decl nil sigma "reals/")) shostak) (sigma_eq_index-1 nil 3539495453 ("" (induct "m") (("1" (typepred "m!1") (("1" (propax) nil nil)) nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (typepred "j!1") (("3" (case "j!1=0") (("1" (hide -2 -3 -4) (("1" (skosimp) (("1" (replace -1) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (assert) (("1" (replace -2 1) (("1" (assert) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1>0") (("1" (hide -2 1) (("1" (hide -3) (("1" (assert) (("1" (skosimp) (("1" (swap-rel -3) (("1" (replace -3 1) (("1" (assert) (("1" (lemma "sigma_last[ Index[1 + j!1]]") (("1" (inst -1 " LAMBDA (i: Index[1 + j!1]): F!1(i)" "j!1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_last[Index[n!1]]") (("1" (inst -1 " LAMBDA (i: Index[n!1]): G!1(i)" "j!1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (copy -4) (("1" (inst -1 "j!1") (("1" (replace -1 1) (("1" (hide -1) (("1" (assert) (("1" (inst -2 "n!1-1" " LAMBDA (i: Index[j!1]): F!1(i)" "LAMBDA (i: Index[n!1-1]): G!1(i)") (("1" (assert) (("1" (case " (FORALL (i_1: below[j!1]): F!1(i_1) = G!1(i_1))") (("1" (replace -1 -3) (("1" (hide -1) (("1" (case " sigma(0, j!1 - 1, LAMBDA (i_1: Index[j!1]): F!1(i_1))= sigma(0, j!1 - 1, LAMBDA (i: Index[1 + j!1]): F!1(i))") (("1" (replace -1 -3) (("1" (hide -1) (("1" (case " sigma(0, n!1 - 2, LAMBDA (i_1: Index[n!1 - 1]): G!1(i_1))= sigma(0, n!1 - 2, LAMBDA (i_1: Index[n!1]): G!1(i_1))") (("1" (replace -1 -3) (("1" (hide -1) (("1" (replace -3 -2) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (postpone) nil nil)) nil) ("3" (postpone) nil nil)) nil)) nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil) ("4" (postpone) nil nil) ("5" (postpone) nil nil) ("6" (postpone) nil nil) ("7" (postpone) nil nil) ("8" (postpone) nil nil)) nil) ((Index type-eq-decl nil vectors "vectors/") (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (sigma_last formula-decl nil sigma "reals/")) shostak)) (aux_sigma_TCC1 0 (aux_sigma_TCC1-1 nil 3539499370 ("" (subtype-tcc) nil nil) nil nil)) (aux_sigma_TCC2 0 (aux_sigma_TCC2-1 nil 3539499370 ("" (subtype-tcc) nil nil) nil nil)) (aux_sigma_TCC3 0 (aux_sigma_TCC3-1 nil 3539499370 ("" (subtype-tcc) nil nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (aux_sigma 0 (teo "fin" 3544865338 ("" (induct "m") (("1" (grind) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (case "j!1=0") (("1" (hide -2 -3) (("1" (skosimp) (("1" (replace -1) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (assert) (("1" (replace -2) (("1" (inst -3 "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1>0") (("1" (assert) (("1" (hide -3 1) (("1" (skosimp) (("1" (inst -2 "n!1" "Lambda(i: below[j!1]): F!1(i)" " LAMBDA (i: below[j!1 + n!1]): G!1(i)") (("1" (assert) (("1" (case " (FORALL (i_1: below[j!1]): F!1(i_1) = G!1(i_1)) ") (("1" (replace -1 -3) (("1" (hide -1) (("1" (lemma "sigma_last[below[1+j!1]]") (("1" (inst -1 "LAMBDA (i: below[1 + j!1]): F!1(i)" "j!1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_last[ below[1 + j!1 + n!1]]") (("1" (inst -1 " LAMBDA (i: below[1 + j!1 + n!1]): G!1(i)" "j!1+n!1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (copy -4) (("1" (inst -1 "j!1") (("1" (case "F!1(j!1)=G!1(j!1+n!1)") (("1" (replace -1 1) (("1" (assert) (("1" (hide -1 -2) (("1" (case " sigma(0, j!1 - 1, LAMBDA (i_1: below[j!1]): F!1(i_1)) =sigma(0, j!1 - 1, LAMBDA (i: below[1 + j!1]): F!1(i))") (("1" (replace -1 -3) (("1" (hide -1) (("1" (case " sigma(0, j!1 - 1 + n!1, LAMBDA (i_1: below[j!1 + n!1]): G!1(i_1))= sigma(0, j!1 - 1 + n!1, LAMBDA (i: below[1 + j!1 + n!1]): G!1(i))") (("1" (replace -1 -3) (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (hide -2) (("2" (assert) (("2" (lemma "sigma_restrict_dom") (("2" (inst -1 "j!1+n!1" "j!1+n!1" " LAMBDA (i_1: below[j!1 + n!1]): G!1(i_1)" " LAMBDA (i: below[1 + j!1 + n!1]): G!1(i)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (hide -4 -6 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (assert) (("2" (lemma "sigma_restrict_dom") (("2" (inst -1 "j!1" "j!1" " LAMBDA (i_1: below[j!1]): F!1(i_1)" " LAMBDA (i: below[1 + j!1]): F!1(i)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide -2 -4 2) (("3" (skosimp) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -4) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -4 "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (grind) nil nil)) nil) ("5" (hide 2) (("5" (grind) nil nil)) nil) ("6" (hide 2) (("6" (grind) nil nil)) nil) ("7" (hide 2) (("7" (grind) nil nil)) nil) ("8" (hide 2) (("8" (grind) nil nil)) nil) ("9" (hide 2) (("9" (grind) nil nil)) nil)) nil) ((odd_minus_even_is_odd application-judgement "odd_int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (sigma_restrict_dom formula-decl nil sigma_lemmas nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_last formula-decl nil sigma "reals/") (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) (int_plus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (nat_induction formula-decl nil naturalnumbers nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (pred type-eq-decl nil defined_types nil) (integer nonempty-type-from-decl nil integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) shostak) (thm "finished" 3539510712 ("" (induct "m") (("1" (grind) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (case "j!1=0") (("1" (hide -2 -3) (("1" (skosimp) (("1" (replace -1) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (assert) (("1" (replace -2) (("1" (inst -3 "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1>0") (("1" (assert) (("1" (hide -3 1) (("1" (skosimp) (("1" (inst -2 "n!1" "Lambda(i: below[j!1]): F!1(i)" " LAMBDA (i: below[j!1 + n!1]): G!1(i)") (("1" (assert) (("1" (case " (FORALL (i_1: below[j!1]): F!1(i_1) = G!1(i_1)) ") (("1" (replace -1 -3) (("1" (hide -1) (("1" (lemma "sigma_last[below[1+j!1]]") (("1" (inst -1 "LAMBDA (i: below[1 + j!1]): F!1(i)" "j!1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_last[ below[1 + j!1 + n!1]]") (("1" (inst -1 " LAMBDA (i: below[1 + j!1 + n!1]): G!1(i)" "j!1+n!1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (copy -4) (("1" (inst -1 "j!1") (("1" (case "F!1(j!1)=G!1(j!1+n!1)") (("1" (replace -1 1) (("1" (assert) (("1" (hide -1 -2) (("1" (case " sigma(0, j!1 - 1, LAMBDA (i_1: below[j!1]): F!1(i_1)) =sigma(0, j!1 - 1, LAMBDA (i: below[1 + j!1]): F!1(i))") (("1" (replace -1 -3) (("1" (hide -1) (("1" (case " sigma(0, j!1 - 1 + n!1, LAMBDA (i_1: below[j!1 + n!1]): G!1(i_1))= sigma(0, j!1 - 1 + n!1, LAMBDA (i: below[1 + j!1 + n!1]): G!1(i))") (("1" (replace -1 -3) (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (hide -2) (("2" (lemma "sigma_restrict_dom[1]") (("2" (inst -1 "j!1+n!1" "j!1+n!1" " LAMBDA (i_1: below[j!1 + n!1]): G!1(i_1)" " LAMBDA (i: below[1 + j!1 + n!1]): G!1(i)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (hide -4 -6 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (lemma "sigma_restrict_dom[1]") (("2" (inst -1 "j!1" "j!1" " LAMBDA (i_1: below[j!1]): F!1(i_1)" " LAMBDA (i: below[1 + j!1]): F!1(i)") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (hide -2 -4 2) (("3" (skosimp) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -4) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (hide -4 -6 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (hide -4 -6 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -4 "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (grind) nil nil)) nil) ("5" (hide 2) (("5" (grind) nil nil)) nil) ("6" (hide 2) (("6" (grind) nil nil)) nil) ("7" (hide 2) (("7" (grind) nil nil)) nil) ("8" (hide 2) (("8" (grind) nil nil)) nil) ("9" (hide 2) (("9" (grind) nil nil)) nil)) nil) ((T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (sigma_last formula-decl nil sigma "reals/")) shostak) (casi "casi" 3539510573 ("" (induct "m") (("1" (grind) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (case "j!1=0") (("1" (hide -2 -3) (("1" (skosimp) (("1" (replace -1) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (assert) (("1" (replace -2) (("1" (inst -3 "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1>0") (("1" (assert) (("1" (hide -3 1) (("1" (skosimp) (("1" (inst -2 "n!1" "Lambda(i: below[j!1]): F!1(i)" " LAMBDA (i: below[j!1 + n!1]): G!1(i)") (("1" (assert) (("1" (case " (FORALL (i_1: below[j!1]): F!1(i_1) = G!1(i_1)) ") (("1" (replace -1 -3) (("1" (hide -1) (("1" (lemma "sigma_last[below[1+j!1]]") (("1" (inst -1 "LAMBDA (i: below[1 + j!1]): F!1(i)" "j!1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_last[ below[1 + j!1 + n!1]]") (("1" (inst -1 " LAMBDA (i: below[1 + j!1 + n!1]): G!1(i)" "j!1+n!1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (copy -4) (("1" (inst -1 "j!1") (("1" (case "F!1(j!1)=G!1(j!1+n!1)") (("1" (replace -1 1) (("1" (assert) (("1" (hide -1 -2) (("1" (case " sigma(0, j!1 - 1, LAMBDA (i_1: below[j!1]): F!1(i_1)) =sigma(0, j!1 - 1, LAMBDA (i: below[1 + j!1]): F!1(i))") (("1" (replace -1 -3) (("1" (hide -1) (("1" (case " sigma(0, j!1 - 1 + n!1, LAMBDA (i_1: below[j!1 + n!1]): G!1(i_1))= sigma(0, j!1 - 1 + n!1, LAMBDA (i: below[1 + j!1 + n!1]): G!1(i))") (("1" (replace -1 -3) (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (hide -2) (("2" (postpone) nil nil)) nil)) nil) ("3" (skosimp) (("3" (hide -4 -6 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (postpone) nil nil)) nil) ("3" (hide -2 -4 2) (("3" (skosimp) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -4) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (hide -4 -6 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (hide -4 -6 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -4 "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (grind) nil nil)) nil) ("5" (hide 2) (("5" (grind) nil nil)) nil) ("6" (hide 2) (("6" (grind) nil nil)) nil) ("7" (hide 2) (("7" (grind) nil nil)) nil) ("8" (hide 2) (("8" (grind) nil nil)) nil) ("9" (hide 2) (("9" (grind) nil nil)) nil)) nil) ((T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (sigma_last formula-decl nil sigma "reals/")) shostak) (aux_sigma-1 nil 3539499430 ("" (induct "m") (("1" (grind) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (case "j!1=0") (("1" (hide -2 -3) (("1" (skosimp) (("1" (replace -1) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (assert) (("1" (replace -2) (("1" (inst -3 "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1>0") (("1" (assert) (("1" (hide -3 1) (("1" (skosimp) (("1" (inst -2 "n!1" "Lambda(i: below[j!1]): F!1(i)" " LAMBDA (i: below[j!1 + n!1]): G!1(i)") (("1" (assert) (("1" (case " (FORALL (i_1: below[j!1]): F!1(i_1) = G!1(i_1)) ") (("1" (replace -1 -3) (("1" (hide -1) (("1" (postpone) nil nil)) nil)) nil) ("2" (skosimp) (("2" (inst -4 "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (grind) nil nil)) nil) ("5" (hide 2) (("5" (grind) nil nil)) nil) ("6" (hide 2) (("6" (grind) nil nil)) nil) ("7" (hide 2) (("7" (grind) nil nil)) nil) ("8" (hide 2) (("8" (grind) nil nil)) nil) ("9" (hide 2) (("9" (grind) nil nil)) nil)) nil) nil shostak)) (aux_sigma2_TCC1 0 (aux_sigma2_TCC1-1 nil 3539673824 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers 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_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) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (aux_sigma2_TCC2 0 (aux_sigma2_TCC2-1 nil 3539673824 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers 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_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) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (aux_sigma2 0 (thm "finished" 3539675903 ("" (induct "j") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (case "j!1=0") (("1" (skosimp) (("1" (hide -2) (("1" (replace -1) (("1" (assert) (("1" (replace -3) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (inst -5 "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1>0") (("1" (assert) (("1" (hide -3 1) (("1" (skosimp) (("1" (lemma "sigma_last[below[m!1]]") (("1" (inst -1 " LAMBDA (i: below[m!1]): F!1(i)" "j!1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_last[below[m!1+n!1]]") (("1" (inst -1 " LAMBDA (i: below[m!1 + n!1]): G!1(i)" "j!1+n!1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (copy -5) (("1" (inst -1 "j!1") (("1" (replace -1 1) (("1" (hide -1) (("1" (case "G!1(j!1)=G!1(j!1+n!1)") (("1" (replace -1 1) (("1" (hide -1) (("1" (assert) (("1" (inst -2 "m!1" "n!1" " LAMBDA (i: below[m!1]): F!1(i)" " LAMBDA (i: below[m!1 + n!1]): G!1(i)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (replace -3 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (skosimp) (("2" (hide -6) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 -5 2) (("2" (skosimp) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp) (("4" (skosimp) (("4" (skosimp) (("4" (hide -4) (("4" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp) (("5" (skosimp) (("5" (hide -4) (("5" (grind) nil nil)) nil)) nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp) (("6" (skosimp) (("6" (skosimp) (("6" (hide -4) (("6" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("7" (hide 2) (("7" (skosimp) (("7" (skosimp) (("7" (hide -4) (("7" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((sigma_last formula-decl nil sigma "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (int_plus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma_0_neg formula-decl nil sigma_below "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_induction formula-decl nil naturalnumbers nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil)) shostak) (encamino "encamino" 3539675829 ("" (induct "j") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (case "j!1=0") (("1" (skosimp) (("1" (hide -2) (("1" (replace -1) (("1" (assert) (("1" (replace -3) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (inst -5 "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1>0") (("1" (assert) (("1" (hide -3 1) (("1" (skosimp) (("1" (lemma "sigma_last[below[m!1]]") (("1" (inst -1 " LAMBDA (i: below[m!1]): F!1(i)" "j!1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_last[below[m!1+n!1]]") (("1" (inst -1 " LAMBDA (i: below[m!1 + n!1]): G!1(i)" "j!1+n!1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (copy -5) (("1" (inst -1 "j!1") (("1" (replace -1 1) (("1" (hide -1) (("1" (case "G!1(j!1)=G!1(j!1+n!1)") (("1" (replace -1 1) (("1" (hide -1) (("1" (assert) (("1" (postpone) nil nil)) nil)) nil)) nil) ("2" (replace -3 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (skosimp) (("2" (hide -6) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 -5 2) (("2" (skosimp) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp) (("4" (skosimp) (("4" (skosimp) (("4" (hide -4) (("4" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp) (("5" (skosimp) (("5" (hide -4) (("5" (grind) nil nil)) nil)) nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp) (("6" (skosimp) (("6" (skosimp) (("6" (hide -4) (("6" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("7" (hide 2) (("7" (skosimp) (("7" (skosimp) (("7" (hide -4) (("7" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (sigma_0_neg formula-decl nil sigma_below "reals/") (sigma_last formula-decl nil sigma "reals/")) shostak) (aux_sigma2-1 nil 3539675235 ("" (induct "j") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (case "j!1=0") (("1" (skosimp) (("1" (hide -2) (("1" (replace -1) (("1" (assert) (("1" (replace -3) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (inst -5 "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1>0") (("1" (assert) (("1" (hide -3 1) (("1" (postpone) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp) (("4" (skosimp) (("4" (skosimp) (("4" (hide -4) (("4" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp) (("5" (skosimp) (("5" (hide -4) (("5" (grind) nil nil)) nil)) nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp) (("6" (skosimp) (("6" (skosimp) (("6" (hide -4) (("6" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("7" (hide 2) (("7" (skosimp) (("7" (skosimp) (("7" (hide -4) (("7" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (sigma_restrict_gen_TCC1 0 (sigma_restrict_gen_TCC1-1 nil 3539497928 ("" (subtype-tcc) nil nil) nil nil)) (sigma_restrict_gen_TCC2 0 (sigma_restrict_gen_TCC2-1 nil 3539497928 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers 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_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (sigma_restrict_gen_TCC3 0 (sigma_restrict_gen_TCC3-1 nil 3539497928 ("" (subtype-tcc) nil nil) nil nil)) (sigma_restrict_gen_TCC4 0 (sigma_restrict_gen_TCC4-1 nil 3539497928 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers 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_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (sigma_restrict_gen 0 (teo "fin" 3544866218 ("" (induct "n") (("1" (grind) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (skosimp) (("3" (typepred "j!1") (("3" (case "j!1=0") (("1" (replace -1) (("1" (hide -3 -4) (("1" (assert) (("1" (case " (FORALL (i: below[m!1]): F!1(i) = G!1(i))") (("1" (hide -1) (("1" (hide -3 -4) (("1" (hide -1) (("1" (lemma "sigma_eq[below[1+j!1+m!1]]") (("1" (inst -1 "G!1" "lambda(i:below[1+j!1+m!1]):G!1(i)" "j!2-1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_eq[below[1+m!1]]") (("1" (inst -1 "G!1" " LAMBDA (i: below[1 +m!1]): G!1(i)" "j!2-1" "0") (("1" (assert) (("1" (hide -1) (("1" (lemma "aux_sigma2") (("1" (inst -1 "m!1+1" "j!2" "j!1" "LAMBDA (i: below[1 + m!1]): G!1(i)" "LAMBDA (i: below[1 + j!1 + m!1]): G!1(i)") (("1" (assert) (("1" (lemma "sigma_restrict_dom") (("1" (inst -1 "j!2" "m!1" "F!1" "G!1") (("1" (assert) nil nil) ("2" (hide -1 2) (("2" (skosimp) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (case "j!1>0") (("1" (assert) (("1" (hide -2 1 -4) (("1" (inst -2 "j!2" "_" "_" "_") (("1" (inst -2 "m!1" "_" "_") (("1" (inst -2 "F!1" "_") (("1" (inst -2 "Lambda(i: below[j!1+m!1]): G!1(i)") (("1" (case " (FORALL (i_1: below[m!1]): F!1(i_1) = G!1(i_1))") (("1" (replace -1 -3) (("1" (hide -1) (("1" (assert) (("1" (replace -2 1) (("1" (hide -2) (("1" (assert) (("1" (hide -1) (("1" (lemma "sigma_eq[below[1 + j!1 + m!1]]") (("1" (inst -1 "LAMBDA (i: below[j!1 + m!1 + 1]): G!1(i)" "G!1" "j!2-1" "0") (("1" (assert) (("1" (lemma "sigma_restrict_dom") (("1" (inst -1 "j!2" "j!1+m!1" "LAMBDA (i: below[j!1 + m!1]): G!1(i)" "LAMBDA (i: below[j!1 + m!1+1]): G!1(i)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (grind) nil nil)) nil) ("5" (hide 2) (("5" (skosimp) (("5" (grind) nil nil)) nil)) nil)) nil) ((NOT const-decl "[bool -> bool]" booleans nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (aux_sigma2 formula-decl nil sigma_lemmas nil) (int_plus_int_is_int application-judgement "int" integers nil) (sigma_restrict_dom formula-decl nil sigma_lemmas nil) (m!1 skolem-const-decl "posnat" sigma_lemmas nil) (j!1 skolem-const-decl "nat" sigma_lemmas nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (sigma_eq formula-decl nil sigma "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_induction formula-decl nil naturalnumbers nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil)) shostak) (poc "poc" 3544866143 ("" (induct "n") (("1" (grind) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (skosimp) (("3" (typepred "j!1") (("3" (case "j!1=0") (("1" (replace -1) (("1" (hide -3 -4) (("1" (assert) (("1" (case " (FORALL (i: below[m!1]): F!1(i) = G!1(i))") (("1" (hide -1) (("1" (hide -3 -4) (("1" (hide -1) (("1" (lemma "sigma_eq[below[1+j!1+m!1]]") (("1" (inst -1 "G!1" "lambda(i:below[1+j!1+m!1]):G!1(i)" "j!2-1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_eq[below[1+m!1]]") (("1" (inst -1 "G!1" " LAMBDA (i: below[1 +m!1]): G!1(i)" "j!2-1" "0") (("1" (assert) (("1" (hide -1) (("1" (lemma "aux_sigma2") (("1" (inst -1 "m!1+1" "j!2" "j!1" "LAMBDA (i: below[1 + m!1]): G!1(i)" "LAMBDA (i: below[1 + j!1 + m!1]): G!1(i)") (("1" (assert) (("1" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (case "j!1>0") (("1" (assert) (("1" (hide -2 1 -4) (("1" (inst -2 "j!2" "_" "_" "_") (("1" (inst -2 "m!1" "_" "_") (("1" (inst -2 "F!1" "_") (("1" (inst -2 "Lambda(i: below[j!1+m!1]): G!1(i)") (("1" (case " (FORALL (i_1: below[m!1]): F!1(i_1) = G!1(i_1))") (("1" (replace -1 -3) (("1" (hide -1) (("1" (assert) (("1" (replace -2 1) (("1" (hide -2) (("1" (assert) (("1" (hide -1) (("1" (lemma "sigma_eq[below[1 + j!1 + m!1]]") (("1" (inst -1 "LAMBDA (i: below[j!1 + m!1 + 1]): G!1(i)" "G!1" "j!2-1" "0") (("1" (assert) (("1" (lemma "sigma_restrict_dom") (("1" (inst -1 "j!2" "j!1+m!1" "LAMBDA (i: below[j!1 + m!1]): G!1(i)" "LAMBDA (i: below[j!1 + m!1+1]): G!1(i)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (grind) nil nil)) nil) ("5" (hide 2) (("5" (skosimp) (("5" (grind) nil nil)) nil)) nil)) nil) ((T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (sigma_eq formula-decl nil sigma "reals/")) shostak) (thm "finished" 3539675926 ("" (induct "n") (("1" (grind) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (skosimp) (("3" (typepred "j!1") (("3" (case "j!1=0") (("1" (replace -1) (("1" (hide -3 -4) (("1" (assert) (("1" (lemma "sigma_restrict_dom[1]") (("1" (inst -1 "j!2" "m!1" "F!1" "G!1") (("1" (case " (FORALL (i: below[m!1]): F!1(i) = G!1(i))") (("1" (replace -1 -2) (("1" (hide -1) (("1" (assert) (("1" (hide -3 -4) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_eq[below[1+j!1+m!1]]") (("1" (inst -1 "G!1" "lambda(i:below[1+j!1+m!1]):G!1(i)" "j!2-1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_eq[below[1+m!1]]") (("1" (inst -1 "G!1" " LAMBDA (i: below[1 +m!1]): G!1(i)" "j!2-1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "aux_sigma2") (("1" (inst -1 "m!1+1" "j!2" "j!1" "LAMBDA (i: below[1 + m!1]): G!1(i)" "LAMBDA (i: below[1 + j!1 + m!1]): G!1(i)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (skosimp) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1>0") (("1" (assert) (("1" (hide -2 1 -4) (("1" (inst -2 "j!2" "_" "_" "_") (("1" (inst -2 "m!1" "_" "_") (("1" (inst -2 "F!1" "_") (("1" (inst -2 "Lambda(i: below[j!1+m!1]): G!1(i)") (("1" (case " (FORALL (i_1: below[m!1]): F!1(i_1) = G!1(i_1))") (("1" (replace -1 -3) (("1" (hide -1) (("1" (assert) (("1" (replace -2 1) (("1" (hide -2) (("1" (lemma "sigma_restrict_dom[1]") (("1" (inst -1 "j!2" "j!1+m!1" "LAMBDA (i: below[j!1 + m!1]): G!1(i)" "LAMBDA (i: below[j!1 + m!1+1]): G!1(i)") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_eq[below[1 + j!1 + m!1]]") (("1" (inst -1 "LAMBDA (i: below[j!1 + m!1 + 1]): G!1(i)" "G!1" "j!2-1" "0") (("1" (assert) nil nil)) nil) ("2" (hide -2 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (grind) nil nil)) nil) ("5" (hide 2) (("5" (skosimp) (("5" (grind) nil nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp) (("6" (grind) nil nil)) nil)) nil) ("7" (hide 2) (("7" (skosimp) (("7" (grind) nil nil)) nil)) nil)) nil) ((sigma_eq formula-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/")) shostak) (apunto "apunto" 3539675228 ("" (induct "n") (("1" (grind) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (skosimp) (("3" (typepred "j!1") (("3" (case "j!1=0") (("1" (replace -1) (("1" (hide -3 -4) (("1" (assert) (("1" (lemma "sigma_restrict_dom[1]") (("1" (inst -1 "j!2" "m!1" "F!1" "G!1") (("1" (case " (FORALL (i: below[m!1]): F!1(i) = G!1(i))") (("1" (replace -1 -2) (("1" (hide -1) (("1" (assert) (("1" (hide -3 -4) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_eq[below[1+j!1+m!1]]") (("1" (inst -1 "G!1" "lambda(i:below[1+j!1+m!1]):G!1(i)" "j!2-1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_eq[below[1+m!1]]") (("1" (inst -1 "G!1" " LAMBDA (i: below[1 +m!1]): G!1(i)" "j!2-1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "aux_sigma2") (("1" (inst -1 "m!1+1" "j!2" "j!1" "LAMBDA (i: below[1 + m!1]): G!1(i)" "LAMBDA (i: below[1 + j!1 + m!1]): G!1(i)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (skosimp) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1>0") (("1" (assert) (("1" (hide -2 1 -4) (("1" (inst -2 "j!2" "_" "_" "_") (("1" (inst -2 "m!1" "_" "_") (("1" (inst -2 "F!1" "_") (("1" (inst -2 "Lambda(i: below[j!1+m!1]): G!1(i)") (("1" (case " (FORALL (i_1: below[m!1]): F!1(i_1) = G!1(i_1))") (("1" (replace -1 -3) (("1" (hide -1) (("1" (assert) (("1" (replace -2 1) (("1" (hide -2) (("1" (lemma "sigma_restrict_dom[1]") (("1" (inst -1 "j!2" "j!1+m!1" "LAMBDA (i: below[j!1 + m!1]): G!1(i)" "LAMBDA (i: below[j!1 + m!1+1]): G!1(i)") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_eq[below[1 + j!1 + m!1]]") (("1" (inst -1 "LAMBDA (i: below[j!1 + m!1 + 1]): G!1(i)" "G!1" "j!2-1" "0") (("1" (assert) nil nil)) nil) ("2" (hide -2 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (grind) nil nil)) nil) ("5" (hide 2) (("5" (skosimp) (("5" (grind) nil nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp) (("6" (grind) nil nil)) nil)) nil) ("7" (hide 2) (("7" (skosimp) (("7" (grind) nil nil)) nil)) nil)) nil) ((T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (sigma_eq formula-decl nil sigma "reals/")) shostak) (faltauna "faltauna" 3539499031 ("" (induct "n") (("1" (grind) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (skosimp) (("3" (typepred "j!1") (("3" (case "j!1=0") (("1" (replace -1) (("1" (hide -3 -4) (("1" (assert) (("1" (lemma "sigma_restrict_dom[1]") (("1" (inst -1 "j!2" "m!1" "F!1" "G!1") (("1" (case " (FORALL (i: below[m!1]): F!1(i) = G!1(i))") (("1" (replace -1 -2) (("1" (hide -1) (("1" (assert) (("1" (hide -3 -4) (("1" (replace -1 1) (("1" (hide -1) (("1" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (skosimp) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1>0") (("1" (assert) (("1" (hide -2 1 -4) (("1" (inst -2 "j!2" "_" "_" "_") (("1" (inst -2 "m!1" "_" "_") (("1" (inst -2 "F!1" "_") (("1" (inst -2 "Lambda(i: below[j!1+m!1]): G!1(i)") (("1" (case " (FORALL (i_1: below[m!1]): F!1(i_1) = G!1(i_1))") (("1" (replace -1 -3) (("1" (hide -1) (("1" (assert) (("1" (replace -2 1) (("1" (hide -2) (("1" (lemma "sigma_restrict_dom[1]") (("1" (inst -1 "j!2" "j!1+m!1" "LAMBDA (i: below[j!1 + m!1]): G!1(i)" "LAMBDA (i: below[j!1 + m!1+1]): G!1(i)") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_eq[below[1 + j!1 + m!1]]") (("1" (inst -1 "LAMBDA (i: below[j!1 + m!1 + 1]): G!1(i)" "G!1" "j!2-1" "0") (("1" (assert) nil nil)) nil) ("2" (hide -2 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (grind) nil nil)) nil) ("5" (hide 2) (("5" (skosimp) (("5" (grind) nil nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp) (("6" (grind) nil nil)) nil)) nil) ("7" (hide 2) (("7" (skosimp) (("7" (grind) nil nil)) nil)) nil)) nil) nil shostak) (faltapoco "faltapoco" 3539498812 ("" (induct "n") (("1" (grind) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (skosimp) (("3" (typepred "j!1") (("3" (case "j!1=0") (("1" (replace -1) (("1" (hide -3 -4) (("1" (assert) (("1" (lemma "sigma_restrict_dom[1]") (("1" (inst -1 "j!2" "m!1" "F!1" "G!1") (("1" (case " (FORALL (i: below[m!1]): F!1(i) = G!1(i))") (("1" (replace -1 -2) (("1" (hide -1) (("1" (assert) (("1" (hide -3 -4) (("1" (replace -1 1) (("1" (hide -1) (("1" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (skosimp) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1>0") (("1" (assert) (("1" (hide -2 1 -4) (("1" (inst -2 "j!2" "_" "_" "_") (("1" (inst -2 "m!1" "_" "_") (("1" (inst -2 "F!1" "_") (("1" (inst -2 "Lambda(i: below[j!1+m!1]): G!1(i)") (("1" (case " (FORALL (i_1: below[m!1]): F!1(i_1) = G!1(i_1))") (("1" (replace -1 -3) (("1" (hide -1) (("1" (assert) (("1" (replace -2 1) (("1" (hide -2) (("1" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (grind) nil nil)) nil) ("5" (hide 2) (("5" (skosimp) (("5" (grind) nil nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp) (("6" (grind) nil nil)) nil)) nil) ("7" (hide 2) (("7" (skosimp) (("7" (grind) nil nil)) nil)) nil)) nil) nil shostak) (dos "dos" 3539498484 ("" (induct "n") (("1" (grind) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (skosimp) (("3" (typepred "j!1") (("3" (case "j!1=0") (("1" (replace -1) (("1" (hide -3 -4) (("1" (assert) (("1" (lemma "sigma_restrict_dom[1]") (("1" (inst -1 "j!2" "m!1" "F!1" "G!1") (("1" (case " (FORALL (i: below[m!1]): F!1(i) = G!1(i))") (("1" (replace -1 -2) (("1" (hide -1) (("1" (assert) (("1" (hide -3 -4) (("1" (replace -1 1) (("1" (hide -1) (("1" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (skosimp) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1>0") (("1" (assert) (("1" (hide -2 1 -4) (("1" (postpone) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (grind) nil nil)) nil) ("5" (hide 2) (("5" (skosimp) (("5" (grind) nil nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp) (("6" (grind) nil nil)) nil)) nil) ("7" (hide 2) (("7" (skosimp) (("7" (grind) nil nil)) nil)) nil)) nil) nil shostak) (sigma_restrict_gen-1 nil 3539497951 ("" (induct "n") (("1" (grind) nil nil) ("2" (assert) nil nil) ("3" (postpone) nil nil) ("4" (skosimp) (("4" (grind) nil nil)) nil) ("5" (hide 2) (("5" (skosimp) (("5" (grind) nil nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp) (("6" (grind) nil nil)) nil)) nil) ("7" (hide 2) (("7" (skosimp) (("7" (grind) nil nil)) nil)) nil)) nil) nil shostak)) (sigma_eq_index2_TCC1 0 (sigma_eq_index2_TCC1-1 nil 3540046271 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil 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) (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)) nil)) (sigma_eq_index2_TCC2 0 (sigma_eq_index2_TCC2-1 nil 3540046271 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil 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) (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)) nil)) (sigma_eq_index2 0 (thm "finished" 3540050426 ("" (induct "j") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (case "j!1=0") (("1" (hide -2) (("1" (hide -2) (("1" (skosimp) (("1" (replace -1) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (inst -4 "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1>0") (("1" (hide 1) (("1" (assert) (("1" (hide -3) (("1" (skosimp) (("1" (inst -2 "m!1+1" "n!1+1" "_" "_") (("1" (assert) (("1" (inst -2 " LAMBDA (i: Index[m!1+1]): IF i<m!1 THEN F!1(i) ELSE 0 ENDIF" "_") (("1" (inst -2 " LAMBDA (i: Index[n!1+1]): IF i<n!1 THEN G!1(i) ELSE 0 ENDIF") (("1" (case " (FORALL (i_1: below[1 + m!1]):
         IF i_1 < m!1 THEN F!1(i_1) ELSE 0 ENDIF =
          IF i_1 < n!1 THEN G!1(i_1) ELSE 0 ENDIF)") (("1" (replace -1 -3) (("1" (hide -1) (("1" (lemma "sigma_last[below[m!1]]") (("1" (inst -1 "LAMBDA (i: Index[m!1]): F!1(i)" "j!1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_last[below[n!1]]") (("1" (inst -1 " LAMBDA (i: Index[n!1]): G!1(i)" "j!1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (copy -5) (("1" (inst -1 "j!1") (("1" (replace -1 1) (("1" (hide -1) (("1" (assert) (("1" (lemma "sigma_restrict_gen") (("1" (inst -1 "j!1" "m!1" "1" " LAMBDA (i: Index[m!1]): F!1(i)" " LAMBDA (i_1: Index[1 + m!1]):
              IF i_1 < m!1 THEN F!1(i_1) ELSE 0 ENDIF") (("1" (assert) (("1" (swap-rel -1) (("1" (replace -1 -3) (("1" (hide -1) (("1" (lemma "sigma_restrict_gen") (("1" (inst -1 "j!1" "n!1" "1" " LAMBDA (i: Index[n!1]): G!1(i)" " LAMBDA (i_1: Index[1 + n!1]):
               IF i_1 < n!1 THEN G!1(i_1) ELSE 0 ENDIF") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (skosimp) (("2" (lift-if) (("2" (case "i!1<m!1") (("1" (assert) (("1" (inst -5 "i!1") nil nil)) nil) ("2" (case "i!1>=m!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (skosimp) (("4" (skosimp) (("4" (assert) nil nil)) nil)) nil)) nil) ("5" (skosimp) (("5" (skosimp) (("5" (assert) nil nil)) nil)) nil) ("6" (skosimp) (("6" (skosimp) (("6" (skosimp) (("6" (assert) nil nil)) nil)) nil)) nil) ("7" (skosimp) (("7" (skosimp) (("7" (assert) nil nil)) nil)) nil) ("8" (skosimp) (("8" (skosimp) (("8" (skosimp) (("8" (assert) nil nil)) nil)) nil)) nil)) 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) (sigma_last formula-decl nil sigma "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (sigma_restrict_gen formula-decl nil sigma_lemmas nil) (real_plus_real_is_real application-judgement "real" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (sigma_0_neg formula-decl nil sigma_below "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_induction formula-decl nil naturalnumbers nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (pred type-eq-decl nil defined_types 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) (Index type-eq-decl nil vectors "vectors/") (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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (int_minus_int_is_int application-judgement "int" integers nil)) shostak) (problema "problema" 3540048708 ("" (induct "m") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (skosimp) (("3" (case "j!1=0") (("1" (hide -2 -3) (("1" (replace -1) (("1" (assert) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (inst -4 "j!2-1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1>0") (("1" (assert) (("1" (hide -3 1) (("1" (inst -2 "j!1" "_" "_" "_") (("1" (case "j!2=1") (("1" (replace -1) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (inst -6 "0") nil nil)) nil)) nil)) nil) ("2" (case "j!2>1") (("1" (inst -3 "j!2-1" "_" "_") (("1" (hide 1) (("1" (inst -3 " LAMBDA (i: Index[j!1]): F!1(i)" " LAMBDA (i: Index[j!1]): G!1(i)") (("1" (assert) (("1" (case " (FORALL (i_1: below[j!1]): F!1(i_1) = G!1(i_1))") (("1" (replace -1 -4) (("1" (hide -1) (("1" (lemma "sigma_last[below[1+j!1]]") (("1" (inst -1 " LAMBDA (i: Index[1 + j!1]): F!1(i)" "j!2-1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_last[below[n!1]]") (("1" (inst -1 "LAMBDA (i: Index[n!1]): G!1(i)" "j!2-1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (copy -6) (("1" (inst -1 "j!2-1") (("1" (replace -1 1) (("1" (hide -1) (("1" (assert) (("1" (lemma "sigma_restrict_gen") (("1" (inst -1 "j!2-1" "j!1" "1" " LAMBDA (i: Index[j!1]): F!1(i)" " LAMBDA (i: Index[1 + j!1]): F!1(i)") (("1" (assert) (("1" (replace -1 -4) (("1" (replace -4 1) (("1" (hide -1) (("1" (hide -3) (("1" (lemma "sigma_restrict_gen") (("1" (inst -1 "j!2-1" "j!1" "1" "LAMBDA (i_1: Index[j!1]): G!1(i_1)" "LAMBDA (i_1: Index[n!1]): G!1(i_1)") (("1" (assert) (("1" (replace -1 1) (("1" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -6 "i!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (skosimp) (("4" (skosimp) (("4" (assert) nil nil)) nil)) nil)) nil) ("5" (skosimp) (("5" (skosimp) (("5" (assert) nil nil)) nil)) nil) ("6" (skosimp) (("6" (skosimp) (("6" (skosimp) (("6" (assert) nil nil)) nil)) nil)) nil) ("7" (skosimp) (("7" (skosimp) (("7" (assert) nil nil)) nil)) nil) ("8" (skosimp) (("8" (skosimp) (("8" (assert) nil nil)) nil)) nil) ("9" (skosimp) (("9" (skosimp) (("9" (skosimp) (("9" (assert) nil nil)) nil)) nil)) nil)) nil) ((sigma_last formula-decl nil sigma "reals/") (sigma_0_neg formula-decl nil sigma_below "reals/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (Index type-eq-decl nil vectors "vectors/")) shostak) (casi "casi" 3540047548 ("" (induct "m") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (skosimp) (("3" (case "j!1=0") (("1" (hide -2 -3) (("1" (replace -1) (("1" (assert) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (inst -4 "j!2-1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1>0") (("1" (assert) (("1" (hide -3 1) (("1" (inst -2 "j!1" "_" "_" "_") (("1" (case "j!2=1") (("1" (replace -1) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (inst -6 "0") nil nil)) nil)) nil)) nil) ("2" (case "j!2>1") (("1" (inst -3 "j!2-1" "_" "_") (("1" (hide 1) (("1" (inst -3 " LAMBDA (i: Index[j!1]): F!1(i)" " LAMBDA (i: Index[j!1]): G!1(i)") (("1" (assert) (("1" (case " (FORALL (i_1: below[j!1]): F!1(i_1) = G!1(i_1))") (("1" (replace -1 -4) (("1" (hide -1) (("1" (lemma "sigma_last[below[1+j!1]]") (("1" (inst -1 " LAMBDA (i: Index[1 + j!1]): F!1(i)" "j!2-1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_last[below[n!1]]") (("1" (inst -1 "LAMBDA (i: Index[n!1]): G!1(i)" "j!2-1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (copy -6) (("1" (inst -1 "j!2-1") (("1" (replace -1 1) (("1" (hide -1) (("1" (assert) (("1" (lemma "sigma_restrict_gen") (("1" (inst -1 "j!2-1" "j!1" "1" " LAMBDA (i: Index[j!1]): F!1(i)" " LAMBDA (i: Index[1 + j!1]): F!1(i)") (("1" (assert) (("1" (replace -1 -4) (("1" (replace -4 1) (("1" (hide -1) (("1" (hide -3) (("1" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -6 "i!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (skosimp) (("4" (skosimp) (("4" (assert) nil nil)) nil)) nil)) nil) ("5" (skosimp) (("5" (skosimp) (("5" (assert) nil nil)) nil)) nil) ("6" (skosimp) (("6" (skosimp) (("6" (skosimp) (("6" (assert) nil nil)) nil)) nil)) nil) ("7" (skosimp) (("7" (skosimp) (("7" (assert) nil nil)) nil)) nil) ("8" (skosimp) (("8" (skosimp) (("8" (assert) nil nil)) nil)) nil) ("9" (skosimp) (("9" (skosimp) (("9" (skosimp) (("9" (assert) nil nil)) nil)) nil)) nil)) nil) nil shostak) (sigma_eq_index2-1 nil 3540046594 ("" (induct "m") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (skosimp) (("3" (case "j!1=0") (("1" (hide -2 -3) (("1" (replace -1) (("1" (assert) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (inst -4 "j!2-1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1>0") (("1" (assert) (("1" (hide -3 1) (("1" (inst -2 "j!1" "_" "_" "_") (("1" (case "j!2=1") (("1" (replace -1) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (inst -6 "0") nil nil)) nil)) nil)) nil) ("2" (case "j!2>1") (("1" (inst -3 "j!2-1" "_" "_") (("1" (hide 1) (("1" (inst -3 " LAMBDA (i: Index[j!1]): F!1(i)" " LAMBDA (i: Index[j!1]): G!1(i)") (("1" (assert) (("1" (case " (FORALL (i_1: below[j!1]): F!1(i_1) = G!1(i_1))") (("1" (replace -1 -4) (("1" (hide -1) (("1" (lemma "sigma_last[below[1+j!1]]") (("1" (inst -1 " LAMBDA (i: Index[1 + j!1]): F!1(i)" "j!2-1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_last[below[n!1]]") (("1" (inst -1 "LAMBDA (i: Index[n!1]): G!1(i)" "j!2-1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (copy -6) (("1" (inst -1 "j!2-1") (("1" (replace -1 1) (("1" (hide -1) (("1" (assert) (("1" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -6 "i!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (skosimp) (("4" (skosimp) (("4" (assert) nil nil)) nil)) nil)) nil) ("5" (skosimp) (("5" (skosimp) (("5" (assert) nil nil)) nil)) nil) ("6" (skosimp) (("6" (skosimp) (("6" (skosimp) (("6" (assert) nil nil)) nil)) nil)) nil) ("7" (skosimp) (("7" (skosimp) (("7" (assert) nil nil)) nil)) nil) ("8" (skosimp) (("8" (skosimp) (("8" (assert) nil nil)) nil)) nil) ("9" (skosimp) (("9" (skosimp) (("9" (skosimp) (("9" (assert) nil nil)) nil)) nil)) nil)) nil) nil shostak)) (sigma_restrict_gen2_TCC1 0 (sigma_restrict_gen2_TCC1-1 nil 3539929747 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (sigma_restrict_gen2_TCC2 0 (sigma_restrict_gen2_TCC2-1 nil 3539929747 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (sigma_restrict_gen2 0 (sigma_restrict_gen2-1 nil 3539929747 ("" (skosimp) (("" (lemma "sigma_split[below[m!1]]") (("1" (inst -1 "F!1" "j!1-1" "0" "k!1-1") (("1" (assert) (("1" (lemma "sigma_split[below[m!1+n!1]]") (("1" (inst -1 "G!1" "j!1-1" "0" "k!1-1") (("1" (assert) (("1" (lemma "both_sides_plus2") (("1" (lemma "sigma_restrict_gen") (("1" (inst -1 "j!1" "m!1" "n!1" "F!1" "G!1") (("1" (replace -5 -1) (("1" (assert) (("1" (replace -1 -4) (("1" (hide -1) (("1" (lemma "sigma_restrict_gen") (("1" (inst -1 "k!1" "m!1" "n!1" "F!1" "G!1") (("1" (replace -5 -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (hide -3 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (hide -3 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((below type-eq-decl nil nat_types nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals 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_split formula-decl nil sigma "reals/") (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (both_sides_plus2 formula-decl nil real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma_restrict_gen formula-decl nil sigma_lemmas nil) (real_plus_real_is_real application-judgement "real" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (T_low type-eq-decl nil sigma "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (T_high type-eq-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_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)) shostak)) (sigma_eq_index3_TCC1 0 (sigma_eq_index3_TCC1-1 nil 3540063060 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (sigma_eq_index3_TCC2 0 (sigma_eq_index3_TCC2-1 nil 3540063060 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (sigma_eq_index3 0 (sigma_eq_index3-1 nil 3540063060 ("" (skosimp) (("" (lemma "sigma_eq_index2") (("" (inst -1 "m!1" "n!1" "j!1" " LAMBDA (i: Index[m!1]): F!1(i)" "LAMBDA (i: Index[n!1]): G!1(i)") (("" (assert) (("" (case " (FORALL (i_1: below[m!1]): F!1(i_1) = G!1(i_1))") (("1" (replace -1 -2) (("1" (hide -1) (("1" (lemma "sigma_split[below[m!1]]") (("1" (inst -1 " LAMBDA (i_1: Index[m!1]): F!1(i_1)" "j!1-1" "0" "k!1-1") (("1" (assert) (("1" (replace -1 -2) (("1" (hide -1) (("1" (lemma "sigma_split[below[n!1]]") (("1" (inst -1 " LAMBDA (i_1: Index[n!1]): G!1(i_1)" "j!1-1" "0" "k!1-1") (("1" (assert) (("1" (replace -1 -2) (("1" (hide -1) (("1" (case " sigma(0, k!1 - 1, LAMBDA (i_1: Index[m!1]): F!1(i_1))= sigma(0, k!1 - 1, LAMBDA (i_1: Index[n!1]): G!1(i_1))") (("1" (assert) nil nil) ("2" (hide -1 2) (("2" (lemma "sigma_eq_index2") (("2" (inst -1 "m!1" "n!1" "k!1" " LAMBDA (i_1: Index[m!1]): F!1(i_1)" "LAMBDA (i_1: Index[n!1]): G!1(i_1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((sigma_eq_index2 formula-decl nil sigma_lemmas 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_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_split formula-decl nil sigma "reals/") (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma def-decl "real" sigma "reals/") (real_plus_real_is_real application-judgement "real" reals nil) (T_low type-eq-decl nil sigma "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (T_high type-eq-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (Index type-eq-decl nil vectors "vectors/") (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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)) shostak)) (sigma_shift_gen_TCC1 0 (sigma_shift_gen_TCC1-1 nil 3539921332 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers 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_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (sigma_shift_gen_TCC2 0 (sigma_shift_gen_TCC2-1 nil 3539921332 ("" (subtype-tcc) nil nil) nil nil)) (sigma_shift_gen_TCC3 0 (sigma_shift_gen_TCC3-1 nil 3539921332 ("" (subtype-tcc) nil nil) nil nil)) (sigma_shift_gen_TCC4 0 (sigma_shift_gen_TCC4-1 nil 3539921332 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers 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_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (sigma_shift_gen 0 (thm "finished" 3539930173 ("" (induct "m") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (skosimp) (("3" (case "j!1=0") (("1" (hide -2 -3) (("1" (typepred "j!2") (("1" (case "j!2=1") (("1" (hide -2) (("1" (replace -1) (("1" (assert) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case "j!1>0") (("1" (assert) (("1" (hide -3 1) (("1" (typepred "j!2") (("1" (case "j!2=1") (("1" (replace -1) (("1" (assert) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (case "j!2>1") (("1" (hide 1) (("1" (hide -2) (("1" (inst -3 "j!2-1" "n!1" "LAMBDA (i: below[j!1 + n!1]): F!1(i)") (("1" (assert) (("1" (lemma "sigma_last[below[1+j!1]]") (("1" (inst -1 " LAMBDA (i: below[1 + j!1]): F!1(i + n!1)" "j!2-1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_last[below[1+j!1+n!1]]") (("1" (inst -1 " LAMBDA (i: below[1 + j!1 + n!1]): F!1(i)" "j!2-1+n!1" "n!1") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (assert) (("1" (lemma "sigma_restrict_gen") (("1" (inst -1 "j!2-1" "j!1" "1" "LAMBDA (i_1: below[j!1]): F!1(i_1 + n!1)" " LAMBDA (i: below[1 + j!1]): F!1(i + n!1)") (("1" (assert) (("1" (replace -1 -4) (("1" (hide -1) (("1" (case " sigma[below[j!1 + n!1]]
           (n!1, j!2 - 2 + n!1, LAMBDA (i_1: below[j!1 + n!1]): F!1(i_1))= sigma(n!1, j!2 - 2 + n!1, LAMBDA (i: below[1 + j!1 + n!1]): F!1(i))") (("1" (replace -1 -4) (("1" (propax) nil nil)) nil) ("2" (hide -3 2) (("2" (lemma "sigma_restrict_gen2") (("2" (inst -1 "j!2-1+n!1" "n!1" "j!1+n!1" "1" " LAMBDA (i_1: below[j!1 + n!1]): F!1(i_1)" " LAMBDA (i: below[1 + j!1 + n!1]): F!1(i)") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (hide -3 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (hide -5 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -3 2) (("2" (skosimp) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp) (("4" (skosimp) (("4" (skosimp) (("4" (grind) nil nil)) nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp) (("5" (skosimp) (("5" (grind) nil nil)) nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp) (("6" (skosimp) (("6" (grind) nil nil)) nil)) nil)) nil) ("7" (hide 2) (("7" (skosimp) (("7" (skosimp) (("7" (skosimp) (("7" (grind) nil nil)) nil)) nil)) nil)) nil) ("8" (hide 2) (("8" (skosimp) (("8" (skosimp) (("8" (grind) nil nil)) nil)) nil)) nil) ("9" (hide 2) (("9" (skosimp) (("9" (skosimp) (("9" (grind) nil nil)) nil)) nil)) nil)) nil) ((NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (odd_minus_odd_is_even application-judgement "even_int" integers 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_gen formula-decl nil sigma_lemmas nil) (sigma_restrict_gen2 formula-decl nil sigma_lemmas nil) (sigma_last formula-decl nil sigma "reals/") (j!2 skolem-const-decl "posnat" sigma_lemmas nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_induction formula-decl nil naturalnumbers nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (pred type-eq-decl nil defined_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (integer nonempty-type-from-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) shostak) (ultima "ultima" 3539929319 ("" (induct "m") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (skosimp) (("3" (case "j!1=0") (("1" (hide -2 -3) (("1" (typepred "j!2") (("1" (case "j!2=1") (("1" (hide -2) (("1" (replace -1) (("1" (assert) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case "j!1>0") (("1" (assert) (("1" (hide -3 1) (("1" (typepred "j!2") (("1" (case "j!2=1") (("1" (replace -1) (("1" (assert) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (case "j!2>1") (("1" (hide 1) (("1" (hide -2) (("1" (inst -3 "j!2-1" "n!1" "LAMBDA (i: below[j!1 + n!1]): F!1(i)") (("1" (assert) (("1" (lemma "sigma_last[below[1+j!1]]") (("1" (inst -1 " LAMBDA (i: below[1 + j!1]): F!1(i + n!1)" "j!2-1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_last[below[1+j!1+n!1]]") (("1" (inst -1 " LAMBDA (i: below[1 + j!1 + n!1]): F!1(i)" "j!2-1+n!1" "n!1") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (assert) (("1" (lemma "sigma_restrict_gen") (("1" (inst -1 "j!2-1" "j!1" "1" "LAMBDA (i_1: below[j!1]): F!1(i_1 + n!1)" " LAMBDA (i: below[1 + j!1]): F!1(i + n!1)") (("1" (assert) (("1" (replace -1 -4) (("1" (hide -1) (("1" (case " sigma[below[j!1 + n!1]]
           (n!1, j!2 - 2 + n!1, LAMBDA (i_1: below[j!1 + n!1]): F!1(i_1))= sigma(n!1, j!2 - 2 + n!1, LAMBDA (i: below[1 + j!1 + n!1]): F!1(i))") (("1" (replace -1 -4) (("1" (propax) nil nil)) nil) ("2" (hide -3 2) (("2" (postpone) nil nil)) nil) ("3" (skosimp) (("3" (hide -3 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (hide -5 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -3 2) (("2" (skosimp) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp) (("4" (skosimp) (("4" (skosimp) (("4" (grind) nil nil)) nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp) (("5" (skosimp) (("5" (grind) nil nil)) nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp) (("6" (skosimp) (("6" (grind) nil nil)) nil)) nil)) nil) ("7" (hide 2) (("7" (skosimp) (("7" (skosimp) (("7" (skosimp) (("7" (grind) nil nil)) nil)) nil)) nil)) nil) ("8" (hide 2) (("8" (skosimp) (("8" (skosimp) (("8" (grind) nil nil)) nil)) nil)) nil) ("9" (hide 2) (("9" (skosimp) (("9" (skosimp) (("9" (grind) nil nil)) nil)) nil)) nil)) nil) ((T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (sigma_last formula-decl nil sigma "reals/")) shostak) (unaaa "unaa" 3539924104 ("" (induct "m") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (skosimp) (("3" (case "j!1=0") (("1" (hide -2 -3) (("1" (typepred "j!2") (("1" (case "j!2=1") (("1" (hide -2) (("1" (replace -1) (("1" (assert) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case "j!1>0") (("1" (assert) (("1" (hide -3 1) (("1" (typepred "j!2") (("1" (case "j!2=1") (("1" (replace -1) (("1" (assert) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (case "j!2>1") (("1" (hide 1) (("1" (hide -2) (("1" (inst -3 "j!2-1" "n!1" "LAMBDA (i: below[j!1 + n!1]): F!1(i)") (("1" (assert) (("1" (lemma "sigma_last[below[1+j!1]]") (("1" (inst -1 " LAMBDA (i: below[1 + j!1]): F!1(i + n!1)" "j!2-1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_last[below[1+j!1+n!1]]") (("1" (inst -1 " LAMBDA (i: below[1 + j!1 + n!1]): F!1(i)" "j!2-1+n!1" "n!1") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (assert) (("1" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (hide -5 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -3 2) (("2" (skosimp) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp) (("4" (skosimp) (("4" (skosimp) (("4" (grind) nil nil)) nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp) (("5" (skosimp) (("5" (grind) nil nil)) nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp) (("6" (skosimp) (("6" (grind) nil nil)) nil)) nil)) nil) ("7" (hide 2) (("7" (skosimp) (("7" (skosimp) (("7" (skosimp) (("7" (grind) nil nil)) nil)) nil)) nil)) nil) ("8" (hide 2) (("8" (skosimp) (("8" (skosimp) (("8" (grind) nil nil)) nil)) nil)) nil) ("9" (hide 2) (("9" (skosimp) (("9" (skosimp) (("9" (grind) nil nil)) nil)) nil)) nil)) nil) nil shostak) (dos "dos" 3539923655 ("" (induct "m") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (skosimp) (("3" (case "j!1=0") (("1" (hide -2 -3) (("1" (postpone) nil nil)) nil) ("2" (case "j!1>0") (("1" (assert) (("1" (hide -3 1) (("1" (typepred "j!2") (("1" (case "j!2=1") (("1" (replace -1) (("1" (assert) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (case "j!2>1") (("1" (hide 1) (("1" (hide -2) (("1" (inst -3 "j!2-1" "n!1" "LAMBDA (i: below[j!1 + n!1]): F!1(i)") (("1" (assert) (("1" (lemma "sigma_last[below[1+j!1]]") (("1" (inst -1 " LAMBDA (i: below[1 + j!1]): F!1(i + n!1)" "j!2-1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_last[below[1+j!1+n!1]]") (("1" (inst -1 " LAMBDA (i: below[1 + j!1 + n!1]): F!1(i)" "j!2-1+n!1" "n!1") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (assert) (("1" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (hide -5 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -3 2) (("2" (skosimp) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp) (("4" (skosimp) (("4" (skosimp) (("4" (grind) nil nil)) nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp) (("5" (skosimp) (("5" (grind) nil nil)) nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp) (("6" (skosimp) (("6" (grind) nil nil)) nil)) nil)) nil) ("7" (hide 2) (("7" (skosimp) (("7" (skosimp) (("7" (skosimp) (("7" (grind) nil nil)) nil)) nil)) nil)) nil) ("8" (hide 2) (("8" (skosimp) (("8" (skosimp) (("8" (grind) nil nil)) nil)) nil)) nil) ("9" (hide 2) (("9" (skosimp) (("9" (skosimp) (("9" (grind) nil nil)) nil)) nil)) nil)) nil) nil shostak) (tres "tres" 3539923478 ("" (induct "m") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (skosimp) (("3" (case "j!1=0") (("1" (hide -2 -3) (("1" (postpone) nil nil)) nil) ("2" (case "j!1>0") (("1" (assert) (("1" (hide -3 1) (("1" (typepred "j!2") (("1" (case "j!2=1") (("1" (postpone) nil nil) ("2" (case "j!2>1") (("1" (hide 1) (("1" (hide -2) (("1" (inst -3 "j!2-1" "n!1" "LAMBDA (i: below[j!1 + n!1]): F!1(i)") (("1" (assert) (("1" (lemma "sigma_last[below[1+j!1]]") (("1" (inst -1 " LAMBDA (i: below[1 + j!1]): F!1(i + n!1)" "j!2-1" "0") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_last[below[1+j!1+n!1]]") (("1" (inst -1 " LAMBDA (i: below[1 + j!1 + n!1]): F!1(i)" "j!2-1+n!1" "n!1") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (assert) (("1" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (hide -5 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -3 2) (("2" (skosimp) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp) (("4" (skosimp) (("4" (skosimp) (("4" (grind) nil nil)) nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp) (("5" (skosimp) (("5" (grind) nil nil)) nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp) (("6" (skosimp) (("6" (grind) nil nil)) nil)) nil)) nil) ("7" (hide 2) (("7" (skosimp) (("7" (skosimp) (("7" (skosimp) (("7" (grind) nil nil)) nil)) nil)) nil)) nil) ("8" (hide 2) (("8" (skosimp) (("8" (skosimp) (("8" (grind) nil nil)) nil)) nil)) nil) ("9" (hide 2) (("9" (skosimp) (("9" (skosimp) (("9" (grind) nil nil)) nil)) nil)) nil)) nil) nil shostak) (problema "problema" 3539922566 ("" (induct "n") (("1" (postpone) nil nil) ("2" (postpone) nil nil) ("3" (skosimp) (("3" (case "j!1=0") (("1" (postpone) nil nil) ("2" (case "j!1>0") (("1" (assert) (("1" (hide -3 1) (("1" (skosimp) (("1" (inst -2 "j!2" "m!1" " LAMBDA (i: below[j!1 + m!1]): F!1(i)") (("1" (assert) (("1" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil) ("4" (postpone) nil nil) ("5" (postpone) nil nil) ("6" (postpone) nil nil) ("7" (postpone) nil nil)) nil) nil shostak) (sigma_shift_gen-1 nil 3539921507 ("" (induct "n") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (case "j!1=0") (("1" (skosimp) (("1" (hide -2 -3) (("1" (replace -1) (("1" (assert) (("1" (postpone) nil nil)) nil)) nil)) nil)) nil) ("2" (case "j!1>0") (("1" (assert) (("1" (hide -3 1) (("1" (skosimp) (("1" (inst -2 "j!1" "m!1" " LAMBDA (i: below[j!1 + m!1]): F!1(i)") (("1" (typepred "j!1") (("1" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp) (("4" (skosimp) (("4" (skosimp) (("4" (grind) nil nil)) nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp) (("5" (skosimp) (("5" (grind) nil nil)) nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp) (("6" (skosimp) (("6" (skosimp) (("6" (grind) nil nil)) nil)) nil)) nil)) nil) ("7" (hide 2) (("7" (skosimp) (("7" (skosimp) (("7" (grind) nil nil)) nil)) nil)) nil)) nil) nil shostak)))