| products/sources/formale sprachen/PVS/co_structures/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: interval_bexpr.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(csequence_merge
(merge_struct_TCC1 0 (merge_struct_TCC1-1 nil 3513693179 ("" (subtype-tcc) nil nil) nil nil)) (merge_struct_TCC2 0 (merge_struct_TCC2-1 nil 3513693179 ("" (subtype-tcc) nil nil) nil nil)) (merge_empty 0 (merge_empty-1 nil 3513693197 ("" (expand* "merge" "merge_struct" "coreduce") (("" (reduce) nil nil)) nil) ((merge const-decl "csequence" csequence_merge nil) (coreduce adt-def-decl "{c: csequence[T] | inj_empty?(op(x)) AND empty?(c) OR inj_nonempty?(op(x)) AND nonempty?(c)}" csequence_codt_coreduce nil) (merge_struct const-decl "csequence_struct" csequence_merge nil)) shostak)) (merge_nonempty 0 (merge_nonempty-1 nil 3513693216 ("" (expand* "merge" "merge_struct" "coreduce") (("" (reduce) nil nil)) nil) ((merge const-decl "csequence" csequence_merge nil) (coreduce adt-def-decl "{c: csequence[T] | inj_empty?(op(x)) AND empty?(c) OR inj_nonempty?(op(x)) AND nonempty?(c)}" csequence_codt_coreduce nil) (merge_struct const-decl "csequence_struct" csequence_merge nil)) shostak)) (merge_empty_left 0 (merge_empty_left-1 nil 3513693224 ("" (skolem!) (("" (lemma "coinduction") (("" (inst - "LAMBDA cseq1, cseq2: cseq1 = merge(cseq2, eseq!1) OR cseq1 = merge(eseq!1, cseq "merge(eseq!1, cseq!1)" "cseq!1") (("" (delete 2) (("" (expand "bisimulation?") (("" (skosimp) (("" (smash) (("1" (expand* "merge" "merge_struct" "coreduce") nil nil) ("2" (expand* "merge" "merge_struct" "coreduce") nil nil) ("3" (replace -1) (("3" (hide -1) (("3" (expand* "merge" "merge_struct") (("3" (expand "coreduce" 1 1) (("3" (expand "coreduce" 2 1) (("3" (expand "coreduce" -) (("3" (reduce) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand* "merge" "merge_struct" "coreduce") (("4" (reduce) nil nil)) nil) ("5" (expand* "merge" "merge_struct" "coreduce") nil nil) ("6" (expand* "merge" "merge_struct" "coreduce") nil nil) ("7" (replace -1) (("7" (hide -1) (("7" (expand* "merge" "merge_struct") (("7" (expand "coreduce" 1 1) (("7" (expand "coreduce" 2 1) (("7" (expand "coreduce" -) (("7" (reduce) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("8" (expand* "merge" "merge_struct" "coreduce") (("8" (reduce) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil csequence_merge nil) (coinduction formula-decl nil csequence_codt nil) (merge_struct const-decl "csequence_struct" csequence_merge nil) (coreduce adt-def-decl "{c: csequence[T] | inj_empty?(op(x)) AND empty?(c) OR inj_nonempty?(op(x)) AND nonempty?(c)}" csequence_codt_coreduce nil) (eseq!1 skolem-const-decl "empty_csequence[T]" csequence_merge nil) (empty_csequence nonempty-type-eq-decl nil csequence_props nil) (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (merge const-decl "csequence" csequence_merge nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bisimulation? adt-def-decl "boolean" csequence_codt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (csequence type-decl nil csequence_codt nil)) shostak)) (merge_empty_right 0 (merge_empty_right-1 nil 3513693378 ("" (skolem!) (("" (lemma "coinduction") (("" (inst - "LAMBDA cseq1, cseq2: cseq1 = merge(cseq2, eseq!1) OR cseq1 = merge(eseq!1, cseq "merge(cseq!1, eseq!1)" "cseq!1") (("" (delete 2) (("" (expand "bisimulation?") (("" (skosimp) (("" (smash) (("1" (expand* "merge" "merge_struct" "coreduce") nil nil) ("2" (expand* "merge" "merge_struct" "coreduce") nil nil) ("3" (replace -1) (("3" (hide -1) (("3" (expand* "merge" "merge_struct") (("3" (expand "coreduce" 1 1) (("3" (expand "coreduce" 2 1) (("3" (expand "coreduce" -) (("3" (reduce) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand* "merge" "merge_struct" "coreduce") (("4" (reduce) nil nil)) nil) ("5" (expand* "merge" "merge_struct" "coreduce") nil nil) ("6" (expand* "merge" "merge_struct" "coreduce") nil nil) ("7" (replace -1) (("7" (hide -1) (("7" (expand* "merge" "merge_struct") (("7" (expand "coreduce" 1 1) (("7" (expand "coreduce" 2 1) (("7" (expand "coreduce" -) (("7" (reduce) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("8" (expand* "merge" "merge_struct" "coreduce") (("8" (reduce) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil csequence_merge nil) (coinduction formula-decl nil csequence_codt nil) (merge_struct const-decl "csequence_struct" csequence_merge nil) (coreduce adt-def-decl "{c: csequence[T] | inj_empty?(op(x)) AND empty?(c) OR inj_nonempty?(op(x)) AND nonempty?(c)}" csequence_codt_coreduce nil) (eseq!1 skolem-const-decl "empty_csequence[T]" csequence_merge nil) (empty_csequence nonempty-type-eq-decl nil csequence_props nil) (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (merge const-decl "csequence" csequence_merge nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bisimulation? adt-def-decl "boolean" csequence_codt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (csequence type-decl nil csequence_codt nil)) shostak)) (merge_first_TCC1 0 (merge_first_TCC1-1 nil 3513693179 ("" (skosimp) (("" (rewrite "merge_nonempty") (("" (assert) nil nil)) nil)) nil) ((merge_nonempty formula-decl nil csequence_merge nil) (T formal-type-decl nil csequence_merge nil) (csequence type-decl nil csequence_codt nil)) nil)) (merge_first 0 (merge_first-1 nil 3513693556 ("" (expand* "merge" "merge_struct" "coreduce") (("" (reduce) nil nil)) nil) ((merge const-decl "csequence" csequence_merge nil) (coreduce adt-def-decl "{c: csequence[T] | inj_empty?(op(x)) AND empty?(c) OR inj_nonempty?(op(x)) AND nonempty?(c)}" csequence_codt_coreduce nil) (merge_struct const-decl "csequence_struct" csequence_merge nil)) shostak)) (merge_rest 0 (merge_rest-1 nil 3513693567 ("" (skosimp) (("" (lift-if) (("" (prop) (("1" (expand* "merge" "merge_struct") (("1" (expand "coreduce" 1 1) (("1" (reduce) nil nil)) nil)) nil) ("2" (rewrite "merge_empty_left") nil nil)) nil)) nil)) nil) ((merge_empty_left formula-decl nil csequence_merge nil) (T formal-type-decl nil csequence_merge nil) (csequence type-decl nil csequence_codt nil) (boolean nonempty-type-decl nil booleans nil) (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (empty_csequence nonempty-type-eq-decl nil csequence_props nil) (merge_struct const-decl "csequence_struct" csequence_merge nil) (merge const-decl "csequence" csequence_merge nil) (coreduce adt-def-decl "{c: csequence[T] | inj_empty?(op(x)) AND empty?(c) OR inj_nonempty?(op(x)) AND nonempty?(c)}" csequence_codt_coreduce nil)) shostak)) (merge_finite 0 (merge_finite-1 nil 3513693179 ("" (induct "fseq1" :name "is_finite_induction") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (case "empty?(cseq!1)") (("1" (skolem!) (("1" (rewrite "merge_empty_left") (("1" (assert) nil nil)) nil)) nil) ("2" (ground) (("2" (skolem-typepred) (("2" (case "empty?(fseq2!1)") (("1" (rewrite "merge_empty_right") nil nil) ("2" (assert) (("2" (expand* "merge" "merge_struct") (("2" (expand "coreduce" +) (("2" (expand "is_finite" +) (("2" (expand "coreduce" +) (("2" (expand "is_finite" +) (("2" (inst - "rest(fseq2!1)") (("2" (expand "is_finite" -1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((merge_empty_right formula-decl nil csequence_merge nil) (merge_struct const-decl "csequence_struct" csequence_merge nil) (fseq2!1 skolem-const-decl "finite_csequence[T]" csequence_merge nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (coreduce adt-def-decl "{c: csequence[T] | inj_empty?(op(x)) AND empty?(c) OR inj_nonempty?(op(x)) AND nonempty?(c)}" csequence_codt_coreduce nil) (NOT const-decl "[bool -> bool]" booleans nil) (merge_empty_left formula-decl nil csequence_merge nil) (empty_csequence nonempty-type-eq-decl nil csequence_props nil) (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (is_finite_induction formula-decl nil csequence_props nil) (T formal-type-decl nil csequence_merge nil) (merge const-decl "csequence" csequence_merge nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (is_finite inductive-decl "bool" csequence_props 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)) nil)) (merge_finiteness 0 (merge_finiteness-1 nil 3513696751 ("" (skosimp) (("" (lemma "is_finite_induction") (("" (inst - "LAMBDA cseq: FORALL cseq1, cseq2: cseq = merge(cseq1, cseq2) IMPLIES is_finite( (("" (split) (("1" (inst - "merge(cseq1!1, cseq2!1)") (("1" (assert) (("1" (inst - "cseq1!1" "cseq2!1") nil nil)) nil)) nil) ("2" (delete -1 2) (("2" (skosimp*) (("2" (replace -2) (("2" (hide -2) (("2" (split) (("1" (rewrite "merge_empty") (("1" (expand "is_finite") (("1" (ground) nil nil)) nil)) nil) ("2" (flatten) (("2" (case "empty?(cseq1!2)") (("1" (rewrite "merge_empty_left") (("1" (expand "is_finite" +) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (inst - "cseq2!2" "rest(cseq1!2)") (("2" (expand "is_finite" 2 1) (("2" (expand* "merge" "merge_struct") (("2" (expand "coreduce" -2 1) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil csequence_merge nil) (is_finite_induction formula-decl nil csequence_props nil) (coreduce adt-def-decl "{c: csequence[T] | inj_empty?(op(x)) AND empty?(c) OR inj_nonempty?(op(x)) AND nonempty?(c)}" csequence_codt_coreduce nil) (merge_struct const-decl "csequence_struct" csequence_merge nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (empty_csequence nonempty-type-eq-decl nil csequence_props nil) (merge_empty_left formula-decl nil csequence_merge nil) (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (merge_empty formula-decl nil csequence_merge nil) (is_finite inductive-decl "bool" csequence_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (merge const-decl "csequence" csequence_merge nil) (= const-decl "[T, T -> boolean]" equalities 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)) shostak)) (merge_infinite1 0 (merge_infinite1-1 nil 3513693179 ("" (skolem-typepred) (("" (forward-chain "merge_finiteness") nil nil)) nil) ((merge_finiteness formula-decl nil csequence_merge nil) (infinite_csequence type-eq-decl nil csequence_props nil) (NOT const-decl "[bool -> bool]" booleans 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_merge nil)) nil)) (merge_infinite2 0 (merge_infinite2-1 nil 3513693179 ("" (skolem-typepred) (("" (forward-chain "merge_finiteness") nil nil)) nil) ((merge_finiteness formula-decl nil csequence_merge nil) (infinite_csequence type-eq-decl nil csequence_props nil) (NOT const-decl "[bool -> bool]" booleans 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_merge nil)) nil)) (merge_length 0 (merge_length-1 nil 3513696918 ("" (induct "fseq1" :name "is_finite_induction") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp*) (("3" (case "empty?(cseq!1)") (("1" (rewrite "merge_empty_left") (("1" (rewrite "length_empty?_rew") (("1" (ground) nil nil)) nil)) nil) ("2" (ground) (("2" (case "empty?(fseq2!1)") (("1" (rewrite "merge_empty_right") (("1" (rewrite "length_empty?_rew") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (expand* "merge" "merge_struct") (("2" (expand "coreduce" +) (("2" (expand "length" 3 1) (("2" (expand "coreduce" +) (("2" (expand "length" +) (("2" (inst - "rest(fseq2!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (lemma "merge_finite" ("fseq1" "fseq1!2" "fseq2" "fseq2!1")) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil) ((merge_finite judgement-tcc nil csequence_merge nil) (coreduce adt-def-decl "{c: csequence[T] | inj_empty?(op(x)) AND empty?(c) OR inj_nonempty?(op(x)) AND nonempty?(c)}" csequence_codt_coreduce nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (merge_struct const-decl "csequence_struct" csequence_merge nil) (merge_empty_right formula-decl nil csequence_merge nil) (empty_csequence nonempty-type-eq-decl nil csequence_props nil) (merge_empty_left formula-decl nil csequence_merge nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (length_empty?_rew formula-decl nil csequence_length nil) (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (is_finite_induction formula-decl nil csequence_props nil) (T formal-type-decl nil csequence_merge nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (length def-decl "{n | has_length(fseq, n)}" csequence_length nil) (has_length def-decl "bool" csequence_props 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) (= const-decl "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers nil) (csequence type-decl nil csequence_codt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (is_finite inductive-decl "bool" csequence_props nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (merge const-decl "csequence" csequence_merge nil)) shostak)) (merge_index_TCC1 0 (merge_index_TCC1-1 nil 3513693179 ("" (skosimp) (("" (rewrite "index?_finite") (("" (assert) nil nil)) nil)) nil) ((index?_finite formula-decl nil csequence_nth nil) (csequence type-decl nil csequence_codt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (is_finite inductive-decl "bool" csequence_props nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T formal-type-decl nil csequence_merge 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) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (merge_index 0 (merge_index-1 nil 3513697065 ("" (auto-rewrite "merge_length") (("" (auto-rewrite "index?_prop") (("" (skolem!) (("" (smash) (("1" (use "merge_finite") nil nil) ("2" (use "merge_infinite2") (("2" (assert) nil nil)) nil) ("3" (use "merge_infinite1") nil nil) ("4" (use "merge_infinite2") (("4" (assert) nil nil)) nil) ("5" (use "merge_infinite1") nil nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil csequence_merge nil) (index?_prop formula-decl nil csequence_nth nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (merge_length formula-decl nil csequence_merge nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (merge_finite judgement-tcc nil csequence_merge 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) (infinite_csequence type-eq-decl nil csequence_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (cseq2!1 skolem-const-decl "csequence[T]" csequence_merge nil) (merge_infinite2 judgement-tcc nil csequence_merge nil) (merge_infinite1 judgement-tcc nil csequence_merge nil)) shostak)) (merge_nth_TCC1 0 (merge_nth_TCC1-1 nil 3513693179 ("" (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) (csequence type-decl nil csequence_codt nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (index? def-decl "bool" csequence_nth nil) (merge const-decl "csequence" csequence_merge nil) (indexes type-eq-decl nil csequence_nth nil) (T formal-type-decl nil csequence_merge nil) (length_lt const-decl "bool" csequence_length_comp nil)) nil)) (merge_nth_TCC2 0 (merge_nth_TCC2-1 nil 3513693179 ("" (skosimp :preds? t) (("" (assert) (("" (rewrite "merge_index") (("" (expand "length_lt") (("" (auto-rewrite "index?_finite") (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (int_times_even_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (length_lt const-decl "bool" csequence_length_comp nil) (index?_finite formula-decl nil csequence_nth nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (merge_index formula-decl nil csequence_merge nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil csequence_merge nil) (csequence type-decl nil csequence_codt nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (index? def-decl "bool" csequence_nth nil) (merge const-decl "csequence" csequence_merge nil) (indexes type-eq-decl nil csequence_nth nil)) nil)) (merge_nth_TCC3 0 (merge_nth_TCC3-1 nil 3513693179 ("" (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) (csequence type-decl nil csequence_codt nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (index? def-decl "bool" csequence_nth nil) (merge const-decl "csequence" csequence_merge nil) (indexes type-eq-decl nil csequence_nth nil) (T formal-type-decl nil csequence_merge nil) (length_lt const-decl "bool" csequence_length_comp nil)) nil)) (merge_nth_TCC4 0 (merge_nth_TCC4-1 nil 3513693179 ("" (skosimp :preds? t) (("" (rewrite "merge_index") (("" (expand "length_lt") (("" (auto-rewrite "index?_finite") (("" (auto-rewrite "index?_infinite") (("" (reduce) nil nil)) nil)) nil)) nil)) nil)) nil) ((merge_index formula-decl nil csequence_merge nil) (int_minus_int_is_int application-judgement "int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (index?_finite formula-decl nil csequence_nth nil) (index?_infinite formula-decl nil csequence_nth nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_times_even_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (length_lt const-decl "bool" csequence_length_comp nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil csequence_merge nil) (csequence type-decl nil csequence_codt nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (index? def-decl "bool" csequence_nth nil) (merge const-decl "csequence" csequence_merge nil) (indexes type-eq-decl nil csequence_nth nil)) nil)) (merge_nth_TCC5 0 (merge_nth_TCC5-1 nil 3513693179 ("" (skosimp :preds? t) (("" (expand "even?") (("" (skolem!) (("" (assert) (("" (expand "length_lt") (("" (rewrite "index?_prop") (("" (rewrite "index?_prop") (("" (lemma "merge_finite") (("" (lemma "merge_length") (("" (reduce) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((even? const-decl "bool" integers nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (index?_prop formula-decl nil csequence_nth nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (merge_finite judgement-tcc nil csequence_merge nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (is_finite inductive-decl "bool" csequence_props nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (cseq2!1 skolem-const-decl "csequence[T]" csequence_merge nil) (merge_finite application-judgement "finite_csequence" csequence_merge nil) (merge_length formula-decl nil csequence_merge nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (length_lt const-decl "bool" csequence_length_comp nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil csequence_merge nil) (csequence type-decl nil csequence_codt nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (index? def-decl "bool" csequence_nth nil) (merge const-decl "csequence" csequence_merge nil) (indexes type-eq-decl nil csequence_nth nil)) nil)) (merge_nth_TCC6 0 (merge_nth_TCC6-1 nil 3513693179 ("" (skosimp :preds? t) (("" (use "even_or_odd") (("" (assert) (("" (expand* "odd?" "length_lt") (("" (rewrite "merge_index") (("" (auto-rewrite "index?_prop") (("" (reduce) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((even_or_odd formula-decl nil naturalnumbers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_times_even_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (int_minus_int_is_int application-judgement "int" integers nil) (length_lt const-decl "bool" csequence_length_comp nil) (even_times_int_is_even application-judgement "even_int" integers nil) (odd? const-decl "bool" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (index?_prop formula-decl nil csequence_nth nil) (int_plus_int_is_int application-judgement "int" integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (merge_index formula-decl nil csequence_merge nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil csequence_merge nil) (csequence type-decl nil csequence_codt nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (index? def-decl "bool" csequence_nth nil) (merge const-decl "csequence" csequence_merge nil) (indexes type-eq-decl nil csequence_nth nil)) nil)) (merge_nth 0 (merge_nth-1 nil 3513697436 ("" (measure-induct+ "n" ("cseq1" "cseq2" "n") :skolem-typepreds? t) (("1" (case-replace "x!3 = 0") (("1" (hide -3) (("1" (expand* "index?" "nth" "length_lt") (("1" (rewrite "merge_first") (("1" (rewrite "merge_nonempty") (("1" (lemma "length_nonempty?_rew") (("1" (inst-cp - "x!2") (("1" (inst - "x!1") (("1" (smash) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "index?") (("2" (flatten) (("2" (lemma "merge_index_TCC1" ("cseq1" "x!1" "n" "x!3")) (("2" (use "merge_index") (("2" (case "is_finite(x!1)") (("1" (assert) (("1" (case "empty?(x!1)") (("1" (use "length_empty?_rew") (("1" (assert) (("1" (rewrite "merge_empty_left") (("1" (expand "length_lt") (("1" (use "length_nonempty?_rew") (("1" (expand "index?" -5 1) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nth" 3 1) (("2" (forward-chain "merge_rest") (("2" (assert) (("2" (replace -1) (("2" (inst - "x!2" "rest(x!1)" "x!3 - 1") (("2" (use "length_empty?_rew") (("2" (assert) (("2" (expand "length_lt") (("2" (expand "is_finite" -2) (("2" (case-replace "length(x!1) = length(rest(x!1)) + 1") (("1" (expand "nth" 4 3) (("1" (expand "nth" 4 4) (("1" (use "even_plus1") (("1" (lemma "index?_prop") (("1" (inst - "x!1" "x!3") (("1" (expand "is_finite" -1) (("1" (expand "length" -1) (("1" (auto-rewrite "index?_finite") (("1" (smash) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "length" 1 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2) (("2" (expand "length_lt") (("2" (assert) (("2" (expand "nth" 3 1) (("2" (forward-chain "merge_rest") (("2" (use "infinite_csequence_is_nonempty") (("2" (assert) (("2" (replace -2) (("2" (inst - "x!2" "rest(x!1)" "x!3 - 1") (("2" (expand "is_finite" 1) (("2" (assert) (("2" (expand "nth" 3 2) (("2" (expand "nth" 3 3) (("2" (use "even_plus1") (("2" (reduce) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "merge_nth_TCC6") (("2" (ground) nil nil)) nil) ("3" (use "merge_nth_TCC5") (("3" (ground) nil nil)) nil) ("4" (use "merge_nth_TCC4") (("4" (ground) nil nil)) nil) ("5" (forward-chain "merge_nth_TCC3") (("5" (assert) nil nil)) nil) ("6" (forward-chain "merge_nth_TCC3") (("6" (assert) nil nil)) nil) ("7" (forward-chain "merge_nth_TCC2") (("7" (assert) nil nil)) nil) ("8" (use "merge_nth_TCC1") (("8" (assert) nil nil)) nil) ("9" (use "merge_nth_TCC1") (("9" (assert) nil nil)) nil) ("10" (use "merge_nth_TCC6") (("10" (ground) nil nil)) nil) ("11" (use "merge_nth_TCC5") (("11" (ground) nil nil)) nil) ("12" (use "merge_nth_TCC4") (("12" (ground) nil nil)) nil) ("13" (forward-chain "merge_nth_TCC3") (("13" (assert) nil nil)) nil) ("14" (forward-chain "merge_nth_TCC3") (("14" (assert) nil nil)) nil) ("15" (forward-chain "merge_nth_TCC2") (("15" (assert) nil nil)) nil) ("16" (use "merge_nth_TCC1") (("16" (assert) nil nil)) nil) ("17" (use "merge_nth_TCC1") (("17" (assert) nil nil)) nil) ("18" (use "merge_nth_TCC6") (("18" (ground) nil nil)) nil) ("19" (use "merge_nth_TCC5") (("19" (ground) nil nil)) nil) ("20" (use "merge_nth_TCC4") (("20" (ground) nil nil)) nil) ("21" (forward-chain "merge_nth_TCC3") (("21" (assert) nil nil)) nil) ("22" (forward-chain "merge_nth_TCC3") (("22" (assert) nil nil)) nil) ("23" (forward-chain "merge_nth_TCC2") (("23" (assert) nil nil)) nil) ("24" (use "merge_nth_TCC1") (("24" (assert) nil nil)) nil) ("25" (use "merge_nth_TCC1") (("25" (assert) nil nil)) nil) ("26" (use "merge_nth_TCC6") (("26" (ground) nil nil)) nil) ("27" (use "merge_nth_TCC5") (("27" (ground) nil nil)) nil) ("28" (use "merge_nth_TCC4") (("28" (ground) nil nil)) nil) ("29" (forward-chain "merge_nth_TCC3") (("29" (assert) nil nil)) nil) ("30" (forward-chain "merge_nth_TCC3") (("30" (assert) nil nil)) nil) ("31" (forward-chain "merge_nth_TCC2") (("31" (assert) nil nil)) nil) ("32" (use "merge_nth_TCC1") (("32" (assert) nil nil)) nil) ("33" (use "merge_nth_TCC1") (("33" (assert) nil nil)) nil)) nil) ((merge_nth_TCC1 subtype-tcc nil csequence_merge nil) (merge_nth_TCC2 subtype-tcc nil csequence_merge nil) (merge_nth_TCC3 subtype-tcc nil csequence_merge nil) (merge_nth_TCC4 subtype-tcc nil csequence_merge nil) (merge_nth_TCC5 subtype-tcc nil csequence_merge nil) (merge_nth_TCC6 subtype-tcc nil csequence_merge nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (merge_nonempty formula-decl nil csequence_merge 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (even_times_int_is_even application-judgement "even_int" integers nil) (length_nonempty?_rew formula-decl nil csequence_length nil) (merge_first formula-decl nil csequence_merge nil) (merge_index_TCC1 subtype-tcc nil csequence_merge nil) (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (merge_empty_left formula-decl nil csequence_merge nil) (empty_csequence nonempty-type-eq-decl nil csequence_props nil) (length_empty?_rew formula-decl nil csequence_length nil) (merge_rest formula-decl nil csequence_merge nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (index?_prop formula-decl nil csequence_nth nil) (index?_finite formula-decl nil csequence_nth nil) (even_plus_even_is_even application-judgement "even_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (rat_minus_rat_is_rat application-judgement "rat" rationals nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (even_plus1 formula-decl nil naturalnumbers nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (infinite_csequence_is_nonempty judgement-tcc nil csequence_props nil) (infinite_csequence type-eq-decl nil csequence_props nil) (merge_index formula-decl nil csequence_merge nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (nth def-decl "T" csequence_nth nil) (= const-decl "[T, T -> boolean]" equalities nil) (even? const-decl "bool" integers nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (is_finite inductive-decl "bool" csequence_props nil) (length_lt const-decl "bool" csequence_length_comp nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_times_even_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (indexes type-eq-decl nil csequence_nth nil) (merge const-decl "csequence" csequence_merge 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_merge 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)) (merge_add 0 (merge_add-1 nil 3513698074 ("" (expand* "merge" "merge_struct") (("" (expand "coreduce" 1 2) (("" (propax) nil nil)) nil)) nil) ((coreduce adt-def-decl "{c: csequence[T] | inj_empty?(op(x)) AND empty?(c) OR inj_nonempty?(op(x)) AND nonempty?(c)}" csequence_codt_coreduce nil) (merge const-decl "csequence" csequence_merge nil) (merge_struct const-decl "csequence_struct" csequence_merge nil)) shostak)) (merge_last_TCC1 0 (merge_last_TCC1-1 nil 3513693179 ("" (skosimp) (("" (rewrite "merge_nonempty") (("" (assert) (("" (lemma "length_nonempty?_rew") (("" (inst-cp - "fseq2!1") (("" (inst - "fseq1!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((merge_nonempty formula-decl nil csequence_merge nil) (T formal-type-decl nil csequence_merge nil) (csequence type-decl nil csequence_codt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (is_finite inductive-decl "bool" csequence_props nil) (finite_csequence nonempty-type-eq-decl nil csequence_props 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_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (merge_last_TCC2 0 (merge_last_TCC2-1 nil 3513693179 ("" (skosimp) (("" (rewrite "merge_nonempty") (("" (assert) (("" (lemma "length_nonempty?_rew") (("" (inst-cp - "fseq2!1") (("" (inst - "fseq1!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((merge_nonempty formula-decl nil csequence_merge nil) (T formal-type-decl nil csequence_merge nil) (csequence type-decl nil csequence_codt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (is_finite inductive-decl "bool" csequence_props nil) (finite_csequence nonempty-type-eq-decl nil csequence_props 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_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (merge_last 0 (merge_last-1 nil 3513698166 ("" (skosimp) (("" (expand "last") (("" (rewrite "merge_length") (("" (use "merge_nth") (("1" (expand* "length_lt" "even?") (("1" (reduce) nil nil)) nil) ("2" (rewrite "merge_nonempty") (("2" (lemma "length_nonempty?_rew") (("2" (inst-cp - "fseq2!1") (("2" (inst - "fseq1!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((last const-decl "T" csequence_nth nil) (merge_nth formula-decl nil csequence_merge nil) (indexes type-eq-decl nil csequence_nth nil) (merge const-decl "csequence" csequence_merge nil) (index? def-decl "bool" csequence_nth 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (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) (has_length def-decl "bool" csequence_props nil) (length def-decl "{n | has_length(fseq, n)}" csequence_length nil) (fseq1!1 skolem-const-decl "finite_csequence[T]" csequence_merge nil) (fseq2!1 skolem-const-decl "finite_csequence[T]" csequence_merge nil) (int_minus_int_is_int application-judgement "int" integers nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_times_even_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (merge_finite application-judgement "finite_csequence" csequence_merge nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (even_times_int_is_even application-judgement "even_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (length_lt const-decl "bool" csequence_length_comp nil) (even? const-decl "bool" integers 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) (merge_nonempty formula-decl nil csequence_merge nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers 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_merge nil) (merge_length formula-decl nil csequence_merge nil)) shostak)) (merge_extensionality 0 (merge_extensionality-1 nil 3513698243 ("" (skosimp) (("" (split) (("1" (lemma "coinduction") (("1" (inst - "LAMBDA cseq1, cseq3: EXISTS cseq2, cseq4: length_eq(cseq1, cseq2) AND length_eq "cseq1!1" "cseq3!1") (("1" (assert) (("1" (inst + "cseq2!1" "cseq4!1") (("1" (assert) nil nil)) nil)) nil) ("2" (delete -1 -2 -3 2) (("2" (expand "bisimulation?") (("2" (skosimp*) (("2" (lemma "length_eq_empty") (("2" (inst-cp - "y!1" "cseq4!2") (("2" (inst - "x!1" "cseq2!2") (("2" (smash) (("1" (rewrite "merge_empty_left") (("1" (use "merge_empty") (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "merge_empty_left" :subst ("eseq" "y!1")) (("2" (use "merge_empty") (("2" (assert) nil nil)) nil)) nil) ("3" (inst + "rest(cseq2!2)" "rest(cseq4!2)") (("3" (lemma "length_eq_rest") (("3" (inst-cp - "y!1" "cseq4!2") (("3" (inst - "x!1" "cseq2!2") (("3" (assert) (("3" (expand* "merge" "merge_struct") (("3" (expand "coreduce" -) (("3" (expand "coreduce" -) (("3" (smash) (("3" (decompose-equality) (("3" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand* "merge" "merge_struct" "coreduce") (("4" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "coinduction") (("2" (inst - "LAMBDA cseq2, cseq4: EXISTS cseq1, cseq3: length_eq(cseq1, cseq2) AND length_eq "cseq2!1" "cseq4!1") (("1" (assert) (("1" (inst + "cseq1!1" "cseq3!1") (("1" (assert) nil nil)) nil)) nil) ("2" (delete -1 -2 -3 2) (("2" (expand "bisimulation?") (("2" (skosimp*) (("2" (lemma "length_eq_empty") (("2" (inst-cp - "cseq3!2" "y!1") (("2" (inst - "cseq1!2" "x!1") (("2" (smash) (("1" (rewrite "merge_empty_right") (("1" (use "merge_empty") (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "merge_empty_right" :subst ("eseq" "y!1")) (("2" (use "merge_empty") (("2" (assert) nil nil)) nil)) nil) ("3" (inst + "rest(cseq1!2)" "rest(cseq3!2)") (("3" (lemma "length_eq_rest") (("3" (inst-cp - "cseq3!2" "y!1") (("3" (inst - "cseq1!2" "x!1") (("3" (assert) (("3" (expand* "merge" "merge_struct") (("3" (expand "coreduce" -) (("3" (expand "coreduce" -) (("3" (smash) (("3" (decompose-equality) (("3" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand* "merge" "merge_struct" "coreduce" "coreduce") (("4" (decompose-equality) (("4" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((merge const-decl "csequence" csequence_merge nil) (= const-decl "[T, T -> boolean]" equalities nil) (length_eq const-decl "bool" csequence_length_comp nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bisimulation? adt-def-decl "boolean" csequence_codt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (csequence type-decl nil csequence_codt nil) (length_eq_empty formula-decl nil csequence_length_comp nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (nonempty_csequence type-eq-decl nil csequence_props nil) (coreduce adt-def-decl "{c: csequence[T] | inj_empty?(op(x)) AND empty?(c) OR inj_nonempty?(op(x)) AND nonempty?(c)}" csequence_codt_coreduce nil) (inj_add adt-constructor-decl "[[T, domain] -> (inj_nonempty?)]" csequence_codt_coreduce nil) (inj_empty_cseq adt-constructor-decl "(inj_empty?)" csequence_codt_coreduce nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (inj_nonempty? adt-recognizer-decl "[csequence_struct -> boolean]" csequence_codt_coreduce nil) (inj_empty? adt-recognizer-decl "[csequence_struct -> boolean]" csequence_codt_coreduce nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (csequence_struct type-decl nil csequence_codt_coreduce nil) (add adt-constructor-decl "[[T, csequence] -> (nonempty?)]" csequence_codt nil) (first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (merge_struct const-decl "csequence_struct" csequence_merge nil) (length_eq_rest formula-decl nil csequence_length_comp nil) (empty_csequence nonempty-type-eq-decl nil csequence_props nil) (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (merge_empty_left formula-decl nil csequence_merge nil) (merge_empty formula-decl nil csequence_merge nil) (coinduction formula-decl nil csequence_codt nil) (T formal-type-decl nil csequence_merge nil) (merge_empty_right formula-decl nil csequence_merge nil)) shostak)) (merge_some 0 (merge_some-1 nil 3513698604 ("" (skolem!) (("" (prop) (("1" (lemma "some_induction") (("1" (inst - "p!1" "LAMBDA cseq: FORALL cseq1, cseq2: cseq = merge(cseq1, cseq2) IMPLIES some(p!1)( (("1" (split) (("1" (inst - "merge(cseq1!1, cseq2!1)") (("1" (assert) (("1" (inst - "cseq1!1" "cseq2!1") --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.63 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 |
