| products/Sources/formale Sprachen/PVS/co_structures/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: numerical_bandb.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(csequence_extract
(caret_TCC1 0 (caret_TCC1-1 nil 3513606610 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (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)) (caret_TCC2 0 (caret_TCC2-1 nil 3513606610 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (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) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (caret_TCC3 0 (caret_TCC3-1 nil 3513606610 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (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) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (caret_TCC4 0 (caret_TCC4-1 nil 3513606610 ("" (termination-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (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) (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)) (caret_TCC5 0 (caret_TCC5-1 nil 3513606610 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (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)) (caret_TCC6 0 (caret_TCC6-1 nil 3513606610 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (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) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (caret_TCC7 0 (caret_TCC7-1 nil 3513606610 ("" (termination-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (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) (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)) (caret_TCC8 0 (caret_TCC8-1 nil 3513606610 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (add_finite application-judgement "nonempty_finite_csequence[T]" csequence_extract 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)) nil)) (extract_empty 0 (extract_empty-1 nil 3513606633 ("" (measure-induct+ "range`2" ("range")) (("" (skolem!) (("" (expand "^" +) (("" (expand "is_finite" +) (("" (expand "index?" +) (("" (reduce) nil nil)) nil)) nil)) nil)) nil)) nil) ((even_minus_odd_is_odd application-judgement "odd_int" integers nil) (add_finite application-judgement "nonempty_finite_csequence[T]" csequence_extract nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (cseq!1 skolem-const-decl "csequence[T]" csequence_extract nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (x!1 skolem-const-decl "[nat, nat]" csequence_extract nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (int_minus_int_is_int application-judgement "int" integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (index? def-decl "bool" csequence_nth nil) (NOT const-decl "[bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (^ def-decl "finite_csequence" csequence_extract nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (is_finite inductive-decl "bool" csequence_props nil) (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_extract nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (naturalnumber type-eq-decl nil naturalnumbers 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) (measure_induction formula-decl nil measure_induction nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) shostak)) (extract_nonempty 0 (extract_nonempty-1 nil 3513606721 ("" (skolem!) (("" (use "extract_empty") (("" (ground) nil nil)) nil)) nil) ((extract_empty formula-decl nil csequence_extract 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) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_extract 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)) shostak)) (extract_length 0 (extract_length-1 nil 3513606732 ("" (measure-induct+ "range`2" ("range")) (("" (skolem!) (("" (smash) (("1" (use "length_empty?_rew") (("1" (expand "^") (("1" (flatten) nil nil)) nil)) nil) ("2" (use "extract_empty") (("2" (assert) (("2" (rewrite "index?_prop") (("2" (assert) (("2" (rewrite "length_empty?_rew") nil nil)) nil)) nil)) nil)) nil) ("3" (expand "^" +) (("3" (expand "length" 3 1) (("3" (expand "length" 3 2) (("3" (expand "length" 3 3) (("3" (expand "length" (-3 2)) (("3" (expand "is_finite" -2) (("3" (lift-if) (("3" (ground) (("1" (inst - "(x!1`1 - 1, x!1`2 - 1)") (("1" (inst - "rest(cseq!1)") (("1" (assert) nil nil)) nil)) nil) ("2" (inst - "(x!1`1, x!1`2 - 1)") (("2" (inst - "rest(cseq!1)") (("2" (assert) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "^" +) (("4" (expand "length" 4 1) (("4" (expand "length" 4 2) (("4" (expand "length" 4 2) (("4" (expand "length" (2 3)) (("4" (lift-if) (("4" (ground) (("1" (inst - "(x!1`1 - 1, x!1`2 - 1)") (("1" (inst - "rest(cseq!1)") (("1" (assert) nil nil)) nil)) nil) ("2" (inst - "(x!1`1, x!1`2 - 1)") (("2" (inst - "rest(cseq!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (expand "^" +) (("5" (expand "length" 3 1) (("5" (expand "length" 3 2) (("5" (expand "length" 3 2) (("5" (expand "is_finite" +) (("5" (lift-if) (("5" (ground) (("1" (inst - "(x!1`1 - 1, x!1`2 - 1)") (("1" (inst - "rest(cseq!1)") (("1" (assert) nil nil)) nil)) nil) ("2" (inst - "(x!1`1, x!1`2 - 1)") (("2" (inst - "rest(cseq!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((odd_plus_even_is_odd application-judgement "odd_int" integers nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (extract_empty formula-decl nil csequence_extract nil) (index?_prop formula-decl nil csequence_nth nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (length_empty?_rew formula-decl nil csequence_length nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (numfield nonempty-type-eq-decl nil number_fields nil) (^ def-decl "finite_csequence" csequence_extract nil) (length def-decl "{n | has_length(fseq, n)}" csequence_length nil) (has_length def-decl "bool" csequence_props nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (is_finite inductive-decl "bool" csequence_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_extract nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (naturalnumber type-eq-decl nil naturalnumbers 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) (measure_induction formula-decl nil measure_induction nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) shostak)) (extract_def 0 (extract_def-1 nil 3513607023 ("" (induct "nfseq" :name "is_finite_induction") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil) ("4" (skosimp*) (("4" (expand "^" +) (("4" (expand "length" -4) (("4" (use "length_empty?_rew") (("4" (lift-if) (("4" (ground) (("1" (decompose-equality) (("1" (lemma "length_empty?_rew" ("cseq" "rest(cseq!1)")) (("1" (assert) nil nil)) nil)) nil) ("2" (decompose-equality 2) (("2" (inst - "n!1 - 1") (("2" (assert) nil nil)) nil)) nil) ("3" (decompose-equality) nil nil) ("4" (decompose-equality 2) (("4" (expand "^") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((empty_cseq adt-constructor-decl "(empty?)" csequence_codt nil) (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil) (add adt-constructor-decl "[[T, csequence] -> (nonempty?)]" csequence_codt nil) (csequence_add_extensionality formula-decl nil csequence_codt nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (add_finite application-judgement "nonempty_finite_csequence[T]" csequence_extract nil) (length_empty?_rew formula-decl nil csequence_length nil) (nonempty_finite_csequence type-eq-decl nil csequence_props nil) (is_finite_induction formula-decl nil csequence_props nil) (T formal-type-decl nil csequence_extract nil) (^ def-decl "finite_csequence" csequence_extract nil) (= const-decl "[T, T -> boolean]" equalities nil) (length def-decl "{n | has_length(fseq, n)}" csequence_length nil) (has_length def-decl "bool" csequence_props nil) (finite_csequence nonempty-type-eq-decl nil csequence_props 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) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (is_finite inductive-decl "bool" csequence_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (csequence type-decl nil csequence_codt nil) (int_minus_int_is_int application-judgement "int" integers nil)) shostak)) (extract_rest_TCC1 0 (extract_rest_TCC1-1 nil 3513606610 ("" (skolem-typepred) (("" (rewrite "length_nonempty?_rew") (("" (assert) nil nil)) nil)) nil) ((length_nonempty?_rew formula-decl nil csequence_length nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (nonempty_finite_csequence type-eq-decl nil csequence_props nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (is_finite inductive-decl "bool" csequence_props nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_extract nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (extract_rest 0 (extract_rest-1 nil 3513607165 ("" (skolem!) (("" (use "extract_rest_TCC1") (("" (use "extract_def" ("n" "length(nfseq!1) - 1")) (("" (assert) (("" (expand "^") (("" (lift-if) (("" (ground) (("1" (decompose-equality -) nil nil) ("2" (decompose-equality -) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((extract_rest_TCC1 subtype-tcc nil csequence_extract nil) (nonempty_finite_csequence type-eq-decl nil csequence_props nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (is_finite inductive-decl "bool" csequence_props nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_extract nil) (int_minus_int_is_int application-judgement "int" integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (empty_cseq adt-constructor-decl "(empty?)" csequence_codt nil) (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (add adt-constructor-decl "[[T, csequence] -> (nonempty?)]" csequence_codt nil) (first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (add_finite application-judgement "nonempty_finite_csequence[T]" csequence_extract nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (^ def-decl "finite_csequence" csequence_extract nil) (length def-decl "{n | has_length(fseq, n)}" csequence_length nil) (has_length def-decl "bool" csequence_props 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) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (extract_def formula-decl nil csequence_extract nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (extract_rest2 0 (extract_rest2-1 nil 3513607229 ("" (induct "n") (("1" (expand "^") (("1" (reduce) nil nil)) nil) ("2" (skosimp*) (("2" (expand "^" (-2 +)) (("2" (smash) (("1" (inst - "rest(cseq!1)" "m!1 - 1") (("1" (assert) (("1" (replace -1) (("1" (expand "^" +) (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (inst - "rest(cseq!1)" "m!1 - 1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (add_finite application-judgement "nonempty_finite_csequence[T]" csequence_extract nil) (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (NOT const-decl "[bool -> bool]" booleans nil) (nat_induction formula-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (= const-decl "[T, T -> boolean]" equalities nil) (^ def-decl "finite_csequence" csequence_extract nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (is_finite inductive-decl "bool" csequence_props nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_extract nil) (pred type-eq-decl nil defined_types 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) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) shostak)) (extract_extract 0 (extract_extract-1 nil 3513607305 ("" (measure-induct+ "range`2" ("range")) (("" (skolem!) (("" (expand "^" 1 1) (("" (lift-if) (("" (ground) (("1" (expand "^") (("1" (propax) nil nil)) nil) ("2" (expand "^") (("2" (propax) nil nil)) nil) ("3" (inst - "(x!1`1 - 1, x!1`2 - 1)") (("3" (inst - "rest(cseq!1)" "range2!1") (("3" (assert) (("3" (replace -2) (("3" (hide -2) (("3" (expand "^" 1 2) (("3" (expand* "^" "min") (("3" (reduce) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide -2) (("4" (expand "^" 1 2) (("4" (expand* "^" "^" "min") (("4" (reduce) nil nil)) nil)) nil)) nil) ("5" (expand "^" 2 2) (("5" (lift-if) (("5" (ground) (("1" (expand* "^" "min") nil nil) ("2" (inst - "(x!1`1, x!1`2 - 1)") (("2" (inst - "rest(cseq!1)" "(range2!1`1 - 1, range2!1`2 - 1)") (("2" (assert) (("2" (replace -2) (("2" (hide -2) (("2" (expand "^" 1 2) (("2" (expand* "^" "min") (("2" (reduce) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand* "^" "min") nil nil) ("4" (inst - "(x!1`1, x!1`2 - 1)") (("4" (inst - "rest(cseq!1)" "(range2!1`1, range2!1`2 - 1)") (("4" (assert) (("4" (replace -1) (("4" (hide -1) (("4" (expand "^" 2 2) (("4" (expand "min") (("4" (reduce) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (add_finite application-judgement "nonempty_finite_csequence[T]" csequence_extract nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (^ def-decl "finite_csequence" csequence_extract nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (is_finite inductive-decl "bool" csequence_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_extract nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (naturalnumber type-eq-decl nil naturalnumbers 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) (measure_induction formula-decl nil measure_induction nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) shostak)) (extract_index 0 (extract_index-1 nil 3513607514 ("" (skolem!) (("" (rewrite "index?_prop") (("" (rewrite "index?_prop") (("" (use "extract_length") (("" (lift-if) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ((index?_prop formula-decl nil csequence_nth nil) (csequence type-decl nil csequence_codt 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) (is_finite inductive-decl "bool" csequence_props nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (^ def-decl "finite_csequence" csequence_extract nil) (T formal-type-decl nil csequence_extract nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (extract_length formula-decl nil csequence_extract nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (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) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)) shostak)) (extract_first_TCC1 0 (extract_first_TCC1-1 nil 3513606610 ("" (skosimp) (("" (use "extract_index") (("" (assert) (("" (expand "index?" 1) (("" (propax) nil nil)) nil)) nil)) nil)) nil) ((extract_index formula-decl nil csequence_extract 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) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_extract nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (index? def-decl "bool" csequence_nth nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (extract_first 0 (extract_first-1 nil 3513607566 ("" (induct "m") (("1" (skosimp) (("1" (expand* "^" "nth") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "^" (-2 +)) (("2" (expand "nth" +) (("2" (lift-if) (("2" (ground) (("2" (inst - "rest(cseq!1)" "n!1 - 1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (forward-chain "extract_first_TCC1") nil nil)) nil)) nil) ((extract_first_TCC1 subtype-tcc nil csequence_extract 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) (int_minus_int_is_int application-judgement "int" integers nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nat_induction formula-decl nil naturalnumbers nil) (nth def-decl "T" csequence_nth nil) (indexes type-eq-decl nil csequence_nth nil) (first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil) (= const-decl "[T, T -> boolean]" equalities nil) (pred type-eq-decl nil defined_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T formal-type-decl nil csequence_extract nil) (csequence type-decl nil csequence_codt nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (is_finite inductive-decl "bool" csequence_props nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (^ def-decl "finite_csequence" csequence_extract nil) (index? def-decl "bool" csequence_nth nil)) shostak)) (extract_nth_TCC1 0 (extract_nth_TCC1-1 nil 3513606610 ("" (skolem-typepred) (("" (rewrite "extract_index") (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil) ((extract_index formula-decl nil csequence_extract nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (^ def-decl "finite_csequence" csequence_extract nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (is_finite inductive-decl "bool" csequence_props nil) (indexes type-eq-decl nil csequence_nth nil) (index? def-decl "bool" csequence_nth nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_extract nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (extract_nth 0 (extract_nth-1 nil 3513607662 ("" (measure-induct+ "m + n" ("cseq" "m" "n")) (("1" (skolem-typepred) (("1" (rewrite "extract_index") (("1" (flatten) (("1" (expand "^" +) (("1" (expand "nth" +) (("1" (smash) (("1" (expand "index?") (("1" (propax) nil nil)) nil) ("2" (inst - "rest(x!1)" "x!2 - 1" "x!3 - 1") (("1" (inst - 0) (("1" (expand "nth" -3 1) (("1" (propax) nil nil)) nil) ("2" (rewrite "extract_index") (("2" (expand "index?" -) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "index?" -) (("2" (assert) nil nil)) nil)) nil) ("3" (expand "index?") (("3" (propax) nil nil)) nil) ("4" (rewrite "extract_rest2") (("1" (inst - "rest(x!1)" "x!2" "x!3 - 1") (("1" (inst - "i!1 - 1") (("1" (assert) nil nil)) nil) ("2" (expand "index?" -) (("2" (use "index?_lt" ("cseq" "rest(x!1)" "i" "i!1 - 1 + x!2")) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (rewrite "index?_0") (("2" (rewrite "extract_index") (("2" (expand "index?" -) (("2" (lemma "index?_lt" ("cseq" "rest(x!1)" "i" "i!1 - 1 + x!2" "n" "x!2 - 1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("5" (inst - "rest(x!1)" "x!2" "x!3 - 1") (("1" (inst - "i!1 - 1") (("1" (assert) nil nil)) nil) ("2" (expand "index?" -) (("2" (use "index?_lt" ("cseq" "rest(x!1)" "i" "i!1 - 1 + x!2")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "extract_nth_TCC1") (("2" (assert) nil nil)) nil) ("3" (skolem!) (("3" (use "extract_nth_TCC1") (("3" (assert) nil nil)) nil)) nil) ("4" (skolem!) (("4" (use "extract_nth_TCC1") (("4" (assert) nil nil)) nil)) nil) ("5" (use "extract_nth_TCC1") (("5" (assert) nil nil)) nil) ("6" (skolem!) (("6" (use "extract_nth_TCC1") (("6" (assert) nil nil)) nil)) nil) ("7" (use "extract_nth_TCC1") (("7" (assert) nil nil)) nil)) nil) ((extract_nth_TCC1 subtype-tcc nil csequence_extract nil) (NOT const-decl "[bool -> bool]" booleans nil) (extract_rest2 formula-decl nil csequence_extract nil) (index?_lt formula-decl nil csequence_nth nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (index?_0 formula-decl nil csequence_nth nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (x!1 skolem-const-decl "csequence[T]" csequence_extract nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (x!2 skolem-const-decl "indexes[T](x!1)" csequence_extract nil) (x!3 skolem-const-decl "nat" csequence_extract nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (extract_index formula-decl nil csequence_extract nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" csequence_nth nil) (= const-decl "[T, T -> boolean]" equalities nil) (^ def-decl "finite_csequence" csequence_extract nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (is_finite inductive-decl "bool" csequence_props nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (indexes type-eq-decl nil csequence_nth nil) (index? def-decl "bool" csequence_nth 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) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_extract nil) (measure_induction formula-decl nil measure_induction nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) shostak)) (extract_add_TCC1 0 (extract_add_TCC1-1 nil 3513606610 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_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)) nil)) (extract_add_TCC2 0 (extract_add_TCC2-1 nil 3513606610 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (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) (rat_max application-judgement "{s: rat | s >= q AND s >= r}" real_defs nil) (int_max application-judgement "{k: int | i <= k AND j <= k}" real_defs 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)) nil)) (extract_add_TCC3 0 (extract_add_TCC3-1 nil 3513606610 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_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)) nil)) (extract_add 0 (extract_add-1 nil 3513608880 ("" (expand "^" 1 1) (("" (expand "max") (("" (reduce) nil nil)) nil)) nil) ((max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (^ def-decl "finite_csequence" csequence_extract nil)) shostak)) (extract_last_TCC1 0 (extract_last_TCC1-1 nil 3513606610 ("" (skosimp) (("" (rewrite "index?_prop") (("" (expand "^") (("" (ground) nil nil)) nil)) nil)) nil) ((index?_prop formula-decl nil csequence_nth nil) (csequence type-decl nil csequence_codt 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) (T formal-type-decl nil csequence_extract 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) (^ def-decl "finite_csequence" csequence_extract nil)) nil)) (extract_last 0 (extract_last-1 nil 3513608941 ("" (induct "n") (("1" (skosimp) (("1" (expand* "^" "last" "index?") (("1" (expand "length" 1 1) (("1" (expand "length" 1 1) (("1" (expand "length" 1 1) (("1" (expand "nth" 1 2) (("1" (expand "nth" 1 2) (("1" (reduce) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "^" (-2 +)) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (ground) (("1" (inst - "rest(cseq!1)" "m!1 - 1") (("1" (expand "index?" -1) (("1" (expand "nth" +) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (inst - "rest(cseq!1)" "m!1 - 1") (("2" (expand "index?" +) (("2" (use "last_rest") (("2" (assert) (("2" (expand "^" -4) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "index?" -1) (("3" (use "add_last") (("3" (lift-if) (("3" (prop) (("1" (rewrite "extract_empty") (("1" (flatten) (("1" (lemma "index?_lt") (("1" (inst - "rest(cseq!1)" "j!1" "m!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst - "rest(cseq!1)" "m!1") (("2" (expand "nth" +) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "index?" +) (("4" (use "add_last") (("4" (lift-if) (("4" (prop) (("1" (rewrite "extract_empty") (("1" (flatten) (("1" (expand "index?" 1) (("1" (rewrite "length_nonempty?_rew") (("1" (flatten) (("1" (assert) (("1" (replace -3) (("1" (hide -3) (("1" (expand "last" +) (("1" (expand "length" 3) (("1" (expand "nth") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (hide -1) (("2" (inst - "rest(cseq!1)" "m!1") (("2" (assert) (("2" (use "last_rest") (("2" (expand "^" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (forward-chain "extract_last_TCC1") nil nil)) nil)) nil) ((extract_last_TCC1 subtype-tcc nil csequence_extract nil) (add_finite application-judgement "nonempty_finite_csequence[T]" csequence_extract nil) (int_minus_int_is_int application-judgement "int" integers nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (last_rest formula-decl nil csequence_nth nil) (add_last formula-decl nil csequence_add nil) (first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil) (cseq!1 skolem-const-decl "csequence[T]" csequence_extract nil) (j!1 skolem-const-decl "nat" csequence_extract nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (index?_lt formula-decl nil csequence_nth nil) (extract_empty formula-decl nil csequence_extract nil) (length_nonempty?_rew formula-decl nil csequence_length nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (length def-decl "{n | has_length(fseq, n)}" csequence_length nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nat_induction formula-decl nil naturalnumbers nil) (nth def-decl "T" csequence_nth nil) (indexes type-eq-decl nil csequence_nth nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (last const-decl "T" csequence_nth nil) (nonempty_finite_csequence type-eq-decl nil csequence_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (pred type-eq-decl nil defined_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T formal-type-decl nil csequence_extract nil) (csequence type-decl nil csequence_codt nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (index? def-decl "bool" csequence_nth nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (is_finite inductive-decl "bool" csequence_props nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (^ def-decl "finite_csequence" csequence_extract nil)) shostak)) (extract_extensionality 0 (extract_extensionality-1 nil 3513609793 ("" (skosimp) (("" (use "nth_extensionality") (("" (assert) (("" (case "index?(cseq1!1) = index?(cseq2!1)") (("1" (assert) (("1" (skolem-typepred) (("1" (assert) (("1" (inst - "(0, n!1)") (("1" (lemma "extract_index") (("1" (inst - "cseq1!1" 0 "n!1" "n!1") (("1" (assert) (("1" (lemma "extract_nth") (("1" (inst-cp - "cseq2!1" 0 "n!1" "n!1") (("1" (inst - "cseq1!1" 0 "n!1" "n!1") (("1" (assert) nil nil) ("2" (use "index?_lt") (("2" (assert) nil nil)) nil)) nil) ("2" (use "index?_lt") (("2" (assert) nil nil)) nil)) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.66 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
