| products/sources/formale sprachen/PVS/co_structures/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: csequence_split.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(csequence_split
(split_left_struct_TCC1 0 (split_left_struct_TCC1-1 nil 3513700428 ("" (subtype-tcc) nil nil) nil nil)) (split_left_struct_TCC2 0 (split_left_struct_TCC2-1 nil 3513700428 ("" (subtype-tcc) nil nil) nil nil)) (split_empty_left 0 (split_empty_left-1 nil 3513700452 ("" (expand* "split" "split_left_struct" "coreduce") (("" (reduce) nil nil)) nil) ((split const-decl "[csequence, csequence]" csequence_split 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) (split_left_struct const-decl "csequence_struct" csequence_split nil)) shostak)) (split_empty_right 0 (split_empty_right-1 nil 3513700467 ("" (expand* "split" "split_right_struct" "coreduce") (("" (reduce) nil nil)) nil) ((split const-decl "[csequence, csequence]" csequence_split 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) (split_right_struct const-decl "csequence_struct" csequence_split nil)) shostak)) (split_nonempty_left 0 (split_nonempty_left-1 nil 3513700483 ("" (expand* "split" "split_left_struct" "coreduce") (("" (reduce) nil nil)) nil) ((split const-decl "[csequence, csequence]" csequence_split 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) (split_left_struct const-decl "csequence_struct" csequence_split nil)) shostak)) (split_nonempty_right 0 (split_nonempty_right-1 nil 3513700496 ("" (expand* "split" "split_right_struct" "coreduce") (("" (reduce) nil nil)) nil) ((split const-decl "[csequence, csequence]" csequence_split 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) (split_right_struct const-decl "csequence_struct" csequence_split nil)) shostak)) (split_first_left_TCC1 0 (split_first_left_TCC1-1 nil 3513700428 ("" (skolem!) (("" (rewrite "split_nonempty_left") nil nil)) nil) ((split_nonempty_left formula-decl nil csequence_split nil) (T formal-type-decl nil csequence_split nil) (csequence type-decl nil csequence_codt nil) (boolean nonempty-type-decl nil booleans nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (nonempty_csequence type-eq-decl nil csequence_props nil)) nil)) (split_first_left 0 (split_first_left-1 nil 3513700545 ("" (expand* "split" "split_left_struct" "coreduce") 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) (split_left_struct const-decl "csequence_struct" csequence_split nil) (split const-decl "[csequence, csequence]" csequence_split nil)) shostak)) (split_first_right_TCC1 0 (split_first_right_TCC1-1 nil 3513700428 ("" (skosimp) (("" (rewrite "split_nonempty_right") nil nil)) nil) ((split_nonempty_right formula-decl nil csequence_split nil) (T formal-type-decl nil csequence_split nil) (csequence type-decl nil csequence_codt nil) (boolean nonempty-type-decl nil booleans nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (nonempty_csequence type-eq-decl nil csequence_props nil)) nil)) (split_first_right 0 (split_first_right-1 nil 3513700556 ("" (expand* "split" "split_right_struct" "coreduce") (("" (reduce) nil nil)) 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_split nil) (csequence type-decl nil csequence_codt nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (nonempty_csequence type-eq-decl nil csequence_props nil) (split const-decl "[csequence, csequence]" csequence_split 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) (split_right_struct const-decl "csequence_struct" csequence_split nil)) shostak)) (split_rest_left_TCC1 0 (split_rest_left_TCC1-1 nil 3513700428 ("" (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) (T formal-type-decl nil csequence_split nil) (csequence type-decl nil csequence_codt nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (nonempty_csequence type-eq-decl nil csequence_props nil)) nil)) (split_rest_left 0 (split_rest_left-1 nil 3513700579 ("" (expand* "split" "split_left_struct") (("" (expand "coreduce" 1 1) (("" (reduce) 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) (nonempty_csequence type-eq-decl nil csequence_props nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_split nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (split const-decl "[csequence, csequence]" csequence_split nil) (split_left_struct const-decl "csequence_struct" csequence_split nil)) shostak)) (split_rest_right 0 (split_rest_right-1 nil 3513700604 ("" (expand* "split" "split_right_struct") (("" (expand "coreduce" 1 1) (("" (reduce) 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) (nonempty_csequence type-eq-decl nil csequence_props nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_split nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (split const-decl "[csequence, csequence]" csequence_split nil) (split_right_struct const-decl "csequence_struct" csequence_split nil)) shostak)) (split_rest_swap_left 0 (split_rest_swap_left-1 nil 3513700627 ("" (skolem!) (("" (lemma "coinduction") (("" (inst - "LAMBDA (cseq1, cseq2: csequence): (empty?(cseq1) AND empty?(cseq2)) OR (EXISTS "split(rest(nseq!1))`1" "split(nseq!1)`2") (("1" (ground) (("1" (inst + "nseq!1") nil nil) ("2" (inst + "nseq!1") nil nil)) nil) ("2" (delete 2) (("2" (expand "bisimulation?") (("2" (skosimp) (("2" (smash) (("1" (skosimp) (("1" (expand* "split" "split_left_struct" "split_right_struct" "coreduce") (("1" (reduce) nil nil)) nil)) nil) ("2" (skosimp) (("2" (expand* "split" "split_left_struct" "split_right_struct" "coreduce") (("2" (reduce) nil nil)) nil)) nil) ("3" (skosimp) (("3" (replace*) (("3" (hide -2 -3) (("3" (use "split_nonempty_left") (("3" (assert) (("3" (lemma "split_nonempty_right" ("cseq" "rest(rest(nseq!2))")) (("3" (use "split_rest_right") (("3" (use "split_rest_left") (("3" (lift-if) (("3" (ground) (("3" (inst + "rest(rest(nseq!2))") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (replace*) (("4" (hide -2 -3) (("4" (use "split_nonempty_left") (("4" (assert) (("4" (lemma "split_rest_left" ("nseq" "rest(nseq!2)")) (("4" (lift-if) (("4" (ground) (("4" (inst + "rest(rest(nseq!2))") (("4" (assert) (("4" (use "split_rest_right") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (skosimp) (("5" (replace*) (("5" (hide -2 -3) (("5" (use "split_nonempty_left") (("5" (assert) (("5" (rewrite "split_first_right") (("5" (rewrite "split_first_left") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil csequence_split nil) (coinduction formula-decl nil csequence_codt nil) (split_first_left formula-decl nil csequence_split nil) (split_first_right formula-decl nil csequence_split nil) (split_rest_right formula-decl nil csequence_split nil) (split_rest_left formula-decl nil csequence_split nil) (split_nonempty_right formula-decl nil csequence_split nil) (split_nonempty_left formula-decl nil csequence_split nil) (split_right_struct const-decl "csequence_struct" csequence_split 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) (split_left_struct const-decl "csequence_struct" csequence_split nil) (csequence type-decl nil csequence_codt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (bisimulation? adt-def-decl "boolean" csequence_codt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (nonempty_csequence type-eq-decl nil csequence_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (split const-decl "[csequence, csequence]" csequence_split nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil)) shostak)) (split_rest_swap_right 0 (split_rest_swap_right-1 nil 3513700832 ("" (skolem!) (("" (lemma "coinduction") (("" (inst - "LAMBDA (cseq1, cseq2: csequence): (empty?(cseq1) AND empty?(cseq2)) OR (EXISTS "split(rest(nseq!1))`2" "rest(split(nseq!1)`1)") (("1" (ground) (("1" (inst + "nseq!1") nil nil) ("2" (inst + "nseq!1") nil nil)) nil) ("2" (delete 2) (("2" (expand "bisimulation?") (("2" (skosimp) (("2" (smash) (("1" (skosimp) (("1" (expand* "split" "split_left_struct" "split_right_struct" "coreduce" "coreduce") (("1" (reduce) nil nil)) nil)) nil) ("2" (skosimp) (("2" (expand* "split" "split_left_struct" "split_right_struct" "coreduce" "coreduce") (("2" (reduce) nil nil)) nil)) nil) ("3" (skosimp) (("3" (replace*) (("3" (hide -2 -3) (("3" (use "split_nonempty_right") (("3" (ground) (("3" (use "split_rest_right") (("3" (assert) (("3" (inst + "rest(rest(nseq!2))") (("3" (assert) (("3" (use "split_rest_left") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (replace*) (("4" (hide -2 -3) (("4" (use "split_nonempty_right") (("4" (ground) (("4" (use "split_rest_right") (("4" (assert) (("4" (inst + "rest(rest(nseq!2))") (("4" (assert) (("4" (use "split_rest_left") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (skosimp) (("5" (replace*) (("5" (hide -2 -3) (("5" (use "split_nonempty_right") (("5" (ground) (("5" (rewrite "split_first_right") (("5" (use "split_rest_left") (("5" (assert) (("5" (replace -1) (("5" (rewrite "split_first_left") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (rewrite "split_nonempty_left") nil nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil csequence_split nil) (coinduction formula-decl nil csequence_codt nil) (split_nonempty_left formula-decl nil csequence_split nil) (split_first_left formula-decl nil csequence_split nil) (split_first_right formula-decl nil csequence_split nil) (split_rest_left formula-decl nil csequence_split nil) (split_rest_right formula-decl nil csequence_split nil) (split_nonempty_right formula-decl nil csequence_split nil) (split_right_struct const-decl "csequence_struct" csequence_split 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) (split_left_struct const-decl "csequence_struct" csequence_split nil) (PRED type-eq-decl nil defined_types nil) (bisimulation? adt-def-decl "boolean" csequence_codt nil) (OR const-decl "[bool, bool -> bool]" booleans 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) (NOT const-decl "[bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (nonempty_csequence type-eq-decl nil csequence_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (split const-decl "[csequence, csequence]" csequence_split nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil)) shostak)) (split_finite 0 (split_finite-1 nil 3513700428 ("" (measure-induct+ "length(fseq)" ("fseq") :skolem-typepreds? t) (("" (expand "is_finite" +) (("" (ground) (("1" (use "split_empty_right") (("1" (prop) (("1" (use "split_rest_right") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (inst - "rest(rest(x!1))") (("1" (expand "length" -2 2) (("1" (expand "length" 6 2) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "is_finite" -) (("2" (expand "is_finite" -) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "split_empty_left") (("2" (assert) (("2" (lemma "split_rest_left" ("nseq" "x!1")) (("2" (lift-if) (("2" (expand "is_finite" +) (("2" (ground) (("2" (replace -1) (("2" (hide -1) (("2" (inst - "rest(rest(x!1))") (("1" (expand "length" -2 2) (("1" (expand "length" 6 2) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "is_finite" -) (("2" (expand "is_finite" -) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((split_empty_left formula-decl nil csequence_split nil) (split_rest_left formula-decl nil csequence_split nil) (split_empty_right formula-decl nil csequence_split nil) (split_rest_right formula-decl nil csequence_split nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (nonempty_csequence type-eq-decl nil csequence_props nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (x!1 skolem-const-decl "finite_csequence[T]" csequence_split nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (split const-decl "[csequence, csequence]" csequence_split nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals 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) (naturalnumber 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) (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_split nil) (measure_induction formula-decl nil measure_induction nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) nil)) (split_infinite 0 (split_infinite-1 nil 3513700428 ("" (skolem-typepred) (("" (prop) (("1" (generalize-skolem-constants) (("1" (measure-induct+ "IF is_finite(split(iseq_1)`2) THEN length(split(iseq_1)`2) ELSE 0 ENDIF" ("iseq_1")) (("1" (expand "is_finite" (-2 +)) (("1" (ground) (("1" (rewrite "split_empty_right") (("1" (expand "is_finite" +) (("1" (assert) nil nil)) nil)) nil) ("2" (use "split_rest_right") (("2" (expand "is_finite" +) (("2" (ground) (("2" (inst - "rest(rest(x!1))") (("2" (assert) (("2" (expand "is_finite" 1) (("2" (expand "length" 1 2) (("2" (lift-if) (("2" (ground) (("2" (rewrite "split_empty_right") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (generalize-skolem-constants) (("2" (measure-induct+ "IF is_finite(split(iseq_1)`1) THEN length(split(iseq_1)`1) ELSE 0 ENDIF" ("iseq_1")) (("2" (expand "is_finite" (-2 +)) (("2" (rewrite "split_empty_left") (("2" (ground) (("2" (use "split_rest_left") (("2" (expand "is_finite" +) (("2" (lift-if -1) (("2" (ground) (("2" (replace -1) (("2" (inst - "rest(rest(x!1))") (("2" (assert) (("2" (expand "is_finite" 2) (("2" (expand "length" 2 2) (("2" (lift-if) (("2" (ground) (("2" (rewrite "split_empty_left") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((pred type-eq-decl nil defined_types nil) (well_founded? const-decl "bool" orders nil) (measure_induction formula-decl nil measure_induction 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) (naturalnumber type-eq-decl nil naturalnumbers nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (finite_csequence nonempty-type-eq-decl nil csequence_props 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) (< const-decl "bool" reals nil) (wf_nat formula-decl nil naturalnumbers nil) (split_empty_right formula-decl nil csequence_split nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonempty_csequence type-eq-decl nil csequence_props nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (split_rest_right formula-decl nil csequence_split nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (split const-decl "[csequence, csequence]" csequence_split nil) (split_empty_left formula-decl nil csequence_split nil) (split_rest_left formula-decl nil csequence_split 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_split nil)) nil)) (split_length_left 0 (split_length_left-1 nil 3513710930 ("" (measure-induct+ "length(fseq)" ("fseq") :skolem-typepreds? t) (("" (expand "length" +) (("" (lift-if) (("" (rewrite "split_empty_left") (("" (lift-if) (("" (ground) (("" (use "split_rest_left") (("" (lift-if) (("" (ground) (("1" (expand "length" +) (("1" (typepred "ceiling(1 / 2)") (("1" (assert) nil nil)) nil)) nil) ("2" (replace -1) (("2" (hide -1) (("2" (inst - "rest(rest(x!1))") (("1" (expand "length" -2 2) (("1" (expand "length" -2 2) (("1" (expand "length" 3 2) (("1" (typepred "ceiling((2 + length(rest(rest(x!1)))) / 2)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "is_finite" -) (("2" (expand "is_finite" -) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((split_empty_left formula-decl nil csequence_split nil) (nonneg_ceiling_is_nat application-judgement "nat" floor_ceil nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (x!1 skolem-const-decl "finite_csequence[T]" csequence_split nil) (posrat_plus_nnrat_is_posrat application-judgement "posrat" rationals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (nonempty_csequence type-eq-decl nil csequence_props nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (split_rest_left formula-decl nil csequence_split nil) (NOT const-decl "[bool -> bool]" booleans nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (ceiling const-decl "{i | x <= i & i < x + 1}" floor_ceil nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (split const-decl "[csequence, csequence]" csequence_split nil) (= const-decl "[T, T -> boolean]" equalities nil) (split_finite application-judgement "[finite_csequence, finite_csequence]" csequence_split nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals 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) (naturalnumber 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) (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_split 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)) (split_length_right 0 (split_length_right-1 nil 3513711060 ("" (measure-induct+ "length(fseq)" ("fseq") :skolem-typepreds? t) (("" (expand "length" +) (("" (lift-if) (("" (rewrite "split_empty_right") (("" (lift-if) (("" (ground) (("1" (expand "length" +) (("1" (typepred "floor(1 / 2)") (("1" (assert) nil nil)) nil)) nil) ("2" (use "split_rest_right") (("2" (assert) (("2" (replace -1) (("2" (hide -1) (("2" (inst - "rest(rest(x!1))") (("1" (expand "length" -2 2) (("1" (expand "length" -2 2) (("1" (expand "length" 3 2) (("1" (typepred "floor((2 + length(rest(rest(x!1)))) / 2)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "is_finite" -) (("2" (expand "is_finite" -) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((split_empty_right formula-decl nil csequence_split nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (x!1 skolem-const-decl "finite_csequence[T]" csequence_split nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (nonempty_csequence type-eq-decl nil csequence_props nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (split_rest_right formula-decl nil csequence_split nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (split const-decl "[csequence, csequence]" csequence_split nil) (= const-decl "[T, T -> boolean]" equalities nil) (split_finite application-judgement "[finite_csequence, finite_csequence]" csequence_split nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals 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) (naturalnumber 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) (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_split 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)) (split_length 0 (split_length-1 nil 3513711151 ("" (skolem!) (("" (use "split_length_left") (("" (use "split_length_right") (("" (use "floor_split") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((split_length_left formula-decl nil csequence_split 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_split nil) (split_finite application-judgement "[finite_csequence, finite_csequence]" csequence_split nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (floor_split formula-decl nil floor_ceil 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 nonempty-type-from-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) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (nonneg_ceiling_is_nat application-judgement "nat" floor_ceil nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (split_length_right formula-decl nil csequence_split nil)) shostak)) (split_index_left 0 (split_index_left-1 nil 3513711191 ("" (skolem!) (("" (rewrite "index?_prop") (("" (rewrite "index?_prop") (("" (rewrite "split_length_left") (("" (use "split_finite") (("" (ground) (("" (use "split_infinite") (("" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((index?_prop formula-decl nil csequence_nth nil) (csequence type-decl nil csequence_codt nil) (split const-decl "[csequence, csequence]" csequence_split 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_split nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (is_finite inductive-decl "bool" csequence_props nil) (split_length_left formula-decl nil csequence_split nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (nonneg_ceiling_is_nat application-judgement "nat" floor_ceil nil) (infinite_csequence type-eq-decl nil csequence_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (split_infinite judgement-tcc nil csequence_split nil) (split_finite judgement-tcc nil csequence_split nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil)) shostak)) (split_index_right 0 (split_index_right-1 nil 3513711230 ("" (skolem!) (("" (rewrite "index?_prop") (("" (rewrite "index?_prop") (("" (rewrite "split_length_right") (("" (use "split_finite") (("" (ground) (("" (use "split_infinite") (("" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((index?_prop formula-decl nil csequence_nth nil) (csequence type-decl nil csequence_codt nil) (split const-decl "[csequence, csequence]" csequence_split 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_split nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (is_finite inductive-decl "bool" csequence_props nil) (split_length_right formula-decl nil csequence_split nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (infinite_csequence type-eq-decl nil csequence_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (split_infinite judgement-tcc nil csequence_split nil) (split_finite judgement-tcc nil csequence_split nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (even_plus_odd_is_odd application-judgement "odd_int" integers 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)) shostak)) (split_nth_left_TCC1 0 (split_nth_left_TCC1-1 nil 3513700428 ("" (skolem-typepred) (("" (rewrite "split_index_left") nil nil)) nil) ((nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (split_index_left formula-decl nil csequence_split nil) (indexes type-eq-decl nil csequence_nth nil) (split const-decl "[csequence, csequence]" csequence_split 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_split nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (split_nth_left 0 (split_nth_left-1 nil 3513711290 ("" (measure-induct+ "n" ("cseq" "n") :skolem-typepreds? t) (("1" (expand "nth" +) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (ground) (("1" (rewrite "split_first_left") nil nil) ("2" (use "split_rest_left") (("2" (lift-if) (("2" (ground) (("1" (rewrite "split_index_left") (("1" (expand* "index?" "index?") nil nil)) nil) ("2" (replace -1) (("2" (hide -1) (("2" (expand "nth" 3 2) (("2" (inst - "rest(rest(x!1))" "x!2 - 1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "split_index_left" ("cseq" "y!1")) (("2" (assert) nil nil)) nil) ("3" (use "split_index_left") (("3" (assert) nil nil)) nil) ("4" (use "split_index_left") (("4" (assert) nil nil)) nil) ("5" (use "split_index_left") (("5" (assert) nil nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (split_first_left formula-decl nil csequence_split nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (nonempty_csequence type-eq-decl nil csequence_props 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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (split_index_left formula-decl nil csequence_split nil) (even_minus_even_is_even application-judgement "even_int" integers nil) (split_rest_left formula-decl nil csequence_split nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (nth def-decl "T" csequence_nth nil) (NOT const-decl "[bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides 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) (split const-decl "[csequence, csequence]" csequence_split 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_split 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)) (split_nth_right_TCC1 0 (split_nth_right_TCC1-1 nil 3513700428 ("" (skolem-typepred) (("" (rewrite "split_index_right") (("" (assert) nil nil)) nil)) nil) ((split_index_right formula-decl nil csequence_split nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (indexes type-eq-decl nil csequence_nth nil) (split const-decl "[csequence, csequence]" csequence_split 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_split nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (split_nth_right 0 (split_nth_right-1 nil 3513711496 ("" (measure-induct+ "n" ("cseq" "n") :skolem-typepreds? t) (("1" (expand "nth" +) (("1" (lift-if) (("1" (ground) (("1" (expand "nth" +) (("1" (rewrite "split_first_right") (("1" (rewrite "split_index_right") (("1" (expand* "index?" "index?") nil nil)) nil)) nil)) nil) ("2" (use "split_rest_right") (("2" (expand "nth" 2 2) (("2" (split) (("1" (replace -1) (("1" (hide -1) (("1" (inst - "rest(rest(x!1))" "x!2 - 1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (rewrite "split_index_right") (("2" (expand* "index?" "index?") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "split_index_right" ("cseq" "y!1")) (("2" (assert) nil nil)) nil) ("3" (use "split_index_right") (("3" (assert) nil nil)) nil) ("4" (use "split_index_right") (("4" (assert) nil nil)) nil) ("5" (use "split_index_right") (("5" (assert) nil nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (nonempty_csequence type-eq-decl nil csequence_props nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (split_first_right formula-decl nil csequence_split nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (split_index_right formula-decl nil csequence_split nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (split_rest_right formula-decl nil csequence_split nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (nth def-decl "T" csequence_nth nil) (NOT const-decl "[bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (odd_plus_even_is_odd application-judgement "odd_int" integers 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) (split const-decl "[csequence, csequence]" csequence_split 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_split 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)) (split_add 0 (split_add-1 nil 3513711631 ("" (skolem!) (("" (decompose-equality) (("1" (lemma "coinduction") (("1" (inst - "LAMBDA (cseq1, cseq2: csequence): (empty?(cseq1) AND empty?(cseq2)) OR (EXISTS "split(add(t!1, cseq!1))`1" "add(t!1, split(cseq!1)`2)") (("1" (ground) (("1" (inst + "cseq!1" "t!1") nil nil) ("2" (inst + "cseq!1" "t!1") nil nil)) nil) ("2" (delete 2) (("2" (expand "bisimulation?") (("2" (skosimp) (("2" (smash) (("1" (skosimp) (("1" (expand* "split" "split_left_struct" "coreduce") nil nil)) nil) ("2" (skosimp) (("2" (replace*) (("2" (hide -2 -3) (("2" (assert) (("2" (use "split_rest_left") (("2" (lift-if) (("2" (rewrite "split_empty_right") (("2" (ground) (("2" (inst + "rest(rest(cseq!2))" "first(rest(cseq!2))") (("2" (lemma "csequence_add_eta") (("2" (inst - "rest(cseq!2)") (("2" (assert) (("2" (hide-all-but 4) (("2" (expand* "split" "split_right_struct") (("2" (expand "coreduce" 1 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (replace*) (("3" (hide -2 -3) (("3" (use "split_rest_left") (("3" (lift-if) (("3" (ground) (("3" (case "empty?(rest(cseq!2))") (("1" (hide 3) (("1" (expand* "split" "split_left_struct" "coreduce") (("1" (reduce) nil nil)) nil)) nil) ("2" (assert) (("2" (inst + "rest(rest(cseq!2))" "first(rest(cseq!2))") (("2" (rewrite "csequence_add_eta") (("2" (assert) (("2" (decompose-equality 4) (("1" (rewrite "split_first_right") nil nil) ("2" (rewrite "split_rest_right") nil nil) ("3" (rewrite "split_nonempty_right") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (replace*) (("4" (hide -2 -3) (("4" (assert) (("4" (rewrite "split_first_left") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "coinduction") (("2" (inst - "LAMBDA (cseq1, cseq2: csequence): (empty?(cseq1) AND empty?(cseq2)) OR (EXISTS "split(add(t!1, cseq!1))`2" "split(cseq!1)`1") (("1" (ground) (("1" (inst + "cseq!1" "t!1") nil nil) ("2" (inst + "cseq!1" "t!1") nil nil)) nil) ("2" (delete 2) (("2" (expand "bisimulation?") (("2" (skosimp) (("2" (smash) (("1" (skosimp) (("1" (expand* "split" "split_left_struct" "split_right_struct" "coreduce") (("1" (reduce) nil nil)) nil)) nil) ("2" (skosimp) (("2" (expand* "split" "split_left_struct" "split_right_struct" "coreduce") (("2" (reduce) nil nil)) nil)) nil) ("3" (skosimp) (("3" (replace*) (("3" (hide -2 -3) (("3" (assert) (("3" (use "split_nonempty_right") (("3" (assert) (("3" (use "split_rest_right") (("3" --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.46 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 |
