| products/Sources/formale Sprachen/PVS/co_structures/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Sprache: LispOriginal von: PVS© |
|
||||||
|
(csequence_reverse
(reverse_TCC1 0 (reverse_TCC1-1 nil 3513691554 ("" (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_reverse nil) (csequence type-decl nil csequence_codt nil) (is_finite inductive-decl "bool" csequence_props nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil)) nil)) (reverse_TCC2 0 (reverse_TCC2-1 nil 3513691554 ("" (skosimp :preds? t) (("" (expand "is_finite" -) (("" (assert) nil 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_reverse nil) (csequence type-decl nil csequence_codt nil) (is_finite inductive-decl "bool" csequence_props nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil)) nil)) (reverse_TCC3 0 (reverse_TCC3-1 nil 3513691554 ("" (termination-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil csequence_reverse nil) (csequence type-decl nil csequence_codt nil) (is_finite inductive-decl "bool" csequence_props nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (length def-decl "{n | has_length(fseq, n)}" csequence_length nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (reverse_empty 0 (reverse_empty-1 nil 3513691724 ("" (expand "reverse") (("" (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_reverse nil) (csequence type-decl nil csequence_codt nil) (is_finite inductive-decl "bool" csequence_props nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (append_finite application-judgement "nonempty_finite_csequence" csequence_reverse nil) (reverse def-decl "finite_csequence" csequence_reverse nil)) shostak)) (reverse_nonempty 0 (reverse_nonempty-1 nil 3513691738 ("" (expand "reverse") (("" (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_reverse nil) (csequence type-decl nil csequence_codt nil) (is_finite inductive-decl "bool" csequence_props nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (append_finite application-judgement "nonempty_finite_csequence" csequence_reverse nil) (reverse def-decl "finite_csequence" csequence_reverse nil)) shostak)) (reverse_first_TCC1 0 (reverse_first_TCC1-1 nil 3513691554 ("" (skolem!) (("" (rewrite "reverse_nonempty") nil nil)) nil) ((reverse_nonempty formula-decl nil csequence_reverse nil) (T formal-type-decl nil csequence_reverse 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) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (nonempty_finite_csequence type-eq-decl nil csequence_props nil)) nil)) (reverse_first 0 (reverse_first-1 nil 3513691767 ("" (measure-induct+ "length(nfseq)" ("nfseq")) (("1" (expand "reverse" +) (("1" (expand* "append" "append_struct" "coreduce") (("1" (smash) (("1" (hide -1) (("1" (rewrite "reverse_empty") (("1" (use "length_empty?_rew") (("1" (assert) (("1" (expand* "last" "length" "nth") nil nil)) nil)) nil)) nil)) nil) ("2" (expand "reverse" 1) (("2" (lift-if) (("2" (ground) (("2" (inst - "rest(x!1)") (("2" (expand "length" -1 2) (("2" (use "last_rest") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "reverse_first_TCC1") nil nil)) nil) ((reverse_first_TCC1 subtype-tcc nil csequence_reverse nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (reverse_empty formula-decl nil csequence_reverse nil) (nth def-decl "T" csequence_nth nil) (length_empty?_rew formula-decl nil csequence_length nil) (last_rest formula-decl nil csequence_nth nil) (append_finite application-judgement "nonempty_finite_csequence" csequence_reverse nil) (append const-decl "nonempty_csequence" csequence_append 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) (append_struct const-decl "csequence_struct" csequence_append nil) (= const-decl "[T, T -> boolean]" equalities nil) (first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil) (last const-decl "T" csequence_nth nil) (reverse def-decl "finite_csequence" csequence_reverse 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) (nonempty_finite_csequence type-eq-decl nil csequence_props nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (is_finite inductive-decl "bool" csequence_props nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_reverse 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)) (reverse_last 0 (reverse_last-1 nil 3513691875 ("" (skolem!) (("" (expand "reverse") (("" (rewrite "append_last") nil nil)) nil)) nil) ((reverse def-decl "finite_csequence" csequence_reverse nil) (T formal-type-decl nil csequence_reverse nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (nonempty_finite_csequence type-eq-decl nil csequence_props 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) (first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (boolean nonempty-type-decl nil booleans nil) (csequence type-decl nil csequence_codt nil) (append_last formula-decl nil csequence_append nil)) shostak)) (reverse_length 0 (reverse_length-1 nil 3513691896 ("" (induct "fseq" :name "is_finite_induction") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (expand "reverse" +) (("3" (expand "length" 1 3) (("3" (use "length_empty?_rew") (("3" (lift-if) (("3" (ground) (("3" (rewrite "append_length") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (append_length formula-decl nil csequence_append nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (append_finite application-judgement "nonempty_finite_csequence" csequence_reverse nil) (length_empty?_rew formula-decl nil csequence_length nil) (is_finite_induction formula-decl nil csequence_props nil) (T formal-type-decl nil csequence_reverse nil) (reverse def-decl "finite_csequence" csequence_reverse 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) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers 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)) shostak)) (reverse_index 0 (reverse_index-1 nil 3513691943 ("" (skolem!) (("" (decompose-equality) (("" (rewrite "index?_finite") (("" (rewrite "index?_finite") (("" (rewrite "reverse_length") nil nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil csequence_reverse nil) (csequence type-decl nil csequence_codt nil) (index? def-decl "bool" csequence_nth nil) (is_finite inductive-decl "bool" csequence_props nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (reverse def-decl "finite_csequence" csequence_reverse 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) (reverse_length formula-decl nil csequence_reverse nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (index?_finite formula-decl nil csequence_nth nil)) shostak)) (reverse_nth_TCC1 0 (reverse_nth_TCC1-1 nil 3513691554 ("" (skolem-typepred) (("" (rewrite "reverse_index") (("" (rewrite "index?_finite") (("" (rewrite "index?_finite") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((reverse_index formula-decl nil csequence_reverse nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (has_length def-decl "bool" csequence_props nil) (length def-decl "{n | has_length(fseq, n)}" csequence_length 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) (index?_finite formula-decl nil csequence_nth nil) (indexes type-eq-decl nil csequence_nth nil) (reverse def-decl "finite_csequence" csequence_reverse 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) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (is_finite inductive-decl "bool" csequence_props nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_reverse nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (reverse_nth 0 (reverse_nth-1 nil 3513692003 ("" (measure-induct+ "length(fseq)" ("fseq")) (("1" (skolem-typepred) (("1" (expand "reverse" (-1 1)) (("1" (ground) (("1" (use "index?_nonempty") (("1" (assert) nil nil)) nil) ("2" (rewrite "append_index") (("2" (split) (("1" (use "append_last") (("1" (expand "last") (("1" (rewrite "append_length") (("1" (rewrite "reverse_length") (("1" (expand "length" +) (("1" (expand "nth" 2 2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "append_nth") (("2" (expand "length" +) (("2" (inst - "rest(x!1)") (("2" (expand "length" -2 2) (("2" (inst - "n!1") (("2" (expand "nth" 2 2) (("2" (lift-if) (("2" (ground) (("2" (rewrite "reverse_index") (("2" (rewrite "index?_finite") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "reverse_nth_TCC1") (("2" (ground) nil nil)) nil) ("3" (use "reverse_nth_TCC1") (("3" (ground) nil nil)) nil) ("4" (use "reverse_nth_TCC1") (("4" (assert) nil nil)) nil)) nil) ((reverse_nth_TCC1 subtype-tcc nil csequence_reverse nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (append_finite application-judgement "nonempty_finite_csequence" csequence_reverse nil) (index?_nonempty formula-decl nil csequence_nth nil) (last const-decl "T" csequence_nth nil) (reverse_length formula-decl nil csequence_reverse nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (append_length formula-decl nil csequence_append nil) (append_last formula-decl nil csequence_append nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (index?_finite formula-decl nil csequence_nth nil) (reverse_index formula-decl nil csequence_reverse nil) (append_nth formula-decl nil csequence_append nil) (append_index formula-decl nil csequence_append nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" csequence_nth nil) (= const-decl "[T, T -> boolean]" equalities nil) (index? def-decl "bool" csequence_nth nil) (reverse def-decl "finite_csequence" csequence_reverse nil) (indexes type-eq-decl nil csequence_nth nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers 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_reverse 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)) (reverse_add1 0 (reverse_add1-1 nil 3513692174 ("" (induct "fseq" :name "is_finite_induction") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp*) (("3" (auto-rewrite "append_first") (("3" (expand "reverse" +) (("3" (smash) (("1" (expand "append" 2 2) (("1" (expand* "append_struct" "coreduce" "coreduce" "reverse" "append" "append_struct" "coreduce" "coreduce") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "append" 1 2) (("2" (expand* "append_struct" "coreduce" "coreduce" "reverse" "append" "append_struct" "coreduce" "coreduce") (("2" (assert) nil nil)) nil)) nil) ("3" (auto-rewrite "append_rest") (("3" (assert) (("3" (inst - "t!1") (("3" (replace -2 :dir rl) (("3" (hide -2) (("3" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (use "append_finite" ("fseq" "fseq!2")) nil nil)) nil)) nil) ((append_finite judgement-tcc nil csequence_append nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil) (csequence_add_extensionality formula-decl nil csequence_codt nil) (append_rest formula-decl nil csequence_append nil) (append_struct const-decl "csequence_struct" csequence_append 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) (append_finite application-judgement "nonempty_finite_csequence" csequence_reverse nil) (append_first formula-decl nil csequence_append nil) (is_finite_induction formula-decl nil csequence_props nil) (T formal-type-decl nil csequence_reverse nil) (reverse def-decl "finite_csequence" csequence_reverse nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (add adt-constructor-decl "[[T, csequence] -> (nonempty?)]" csequence_codt nil) (= const-decl "[T, T -> boolean]" equalities 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) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (nonempty_csequence type-eq-decl nil csequence_props nil) (append const-decl "nonempty_csequence" csequence_append nil)) shostak)) (reverse_add2_TCC1 0 (reverse_add2_TCC1-1 nil 3513691554 ("" (expand "is_finite") (("" (propax) nil nil)) nil) ((is_finite inductive-decl "bool" csequence_props nil)) nil)) (reverse_add2 0 (reverse_add2-1 nil 3513692718 ("" (expand "reverse" 1 1) (("" (propax) nil nil)) nil) ((reverse def-decl "finite_csequence" csequence_reverse nil)) shostak)) (reverse_reverse 0 (reverse_reverse-1 nil 3513692734 ("" (skolem!) (("" (use "nth_extensionality") (("" (assert) (("" (hide 2) (("" (split) (("1" (decompose-equality) (("1" (rewrite "reverse_index") (("1" (rewrite "reverse_index") nil nil)) nil)) nil) ("2" (skolem-typepred) (("2" (rewrite "reverse_nth") (("2" (rewrite "reverse_nth") (("1" (rewrite "reverse_length") (("1" (assert) nil nil)) nil) ("2" (rewrite "index?_finite") (("2" (rewrite "reverse_length") (("2" (rewrite "reverse_length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nth_extensionality formula-decl nil csequence_nth nil) (T formal-type-decl nil csequence_reverse nil) (reverse def-decl "finite_csequence" csequence_reverse 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) (NOT const-decl "[bool -> bool]" booleans nil) (indexes type-eq-decl nil csequence_nth nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (has_length def-decl "bool" csequence_props nil) (length def-decl "{n | has_length(fseq, n)}" csequence_length nil) (int_plus_int_is_int application-judgement "int" integers nil) (reverse_length formula-decl nil csequence_reverse nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (index?_finite formula-decl nil csequence_nth nil) (int_minus_int_is_int application-judgement "int" integers nil) (reverse_nth formula-decl nil csequence_reverse 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) (reverse_index formula-decl nil csequence_reverse nil)) shostak)) (reverse_extensionality 0 (reverse_extensionality-1 nil 3513692804 ("" (skosimp) (("" (lemma "nth_extensionality") (("" (inst - "fseq1!1" "fseq2!1") (("" (assert) (("" (case "index?(fseq1!1) = index?(fseq2!1)") (("1" (assert) (("1" (skolem-typepred) (("1" (copy -1) (("1" (replace -3 -2) (("1" (rewrite "index?_finite") (("1" (rewrite "index?_finite") (("1" (assert) (("1" (lemma "reverse_length") (("1" (inst-cp - "fseq2!1") (("1" (inst - "fseq1!1") (("1" (lemma "reverse_nth") (("1" (inst-cp - "fseq2!1" "length(fseq2!1) - n!1 - 1") (("1" (inst - "fseq1!1" "length(fseq1!1) - n!1 - 1") (("1" (assert) nil nil) ("2" (rewrite "index?_finite") (("2" (assert) nil nil)) nil)) nil) ("2" (rewrite "index?_finite") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete 2) (("2" (rewrite "reverse_index" :dir rl) (("2" (rewrite "reverse_index" :dir rl :subst ("fseq" "fseq2!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil csequence_reverse nil) (nth_extensionality formula-decl nil csequence_nth nil) (reverse_index formula-decl nil csequence_reverse nil) (index?_finite formula-decl nil csequence_nth nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (reverse_nth formula-decl nil csequence_reverse nil) (n!1 skolem-const-decl "indexes[T](fseq1!1)" csequence_reverse nil) (fseq1!1 skolem-const-decl "finite_csequence[T]" csequence_reverse nil) (length def-decl "{n | has_length(fseq, n)}" csequence_length nil) (has_length def-decl "bool" csequence_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (fseq2!1 skolem-const-decl "finite_csequence[T]" csequence_reverse nil) (reverse def-decl "finite_csequence" csequence_reverse nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (reverse_length formula-decl nil csequence_reverse nil) (indexes type-eq-decl nil csequence_nth nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (index? def-decl "bool" csequence_nth 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)) shostak)) (reverse_some 0 (reverse_some-1 nil 3513692952 ("" (skolem!) (("" (lemma "nth_some") (("" (inst-cp - "fseq!1" "p!1") (("" (inst - "reverse(fseq!1)" "p!1") (("" (prop) (("1" (skolem!) (("1" (rewrite "reverse_nth") (("1" (inst + "length(fseq!1) - 1 - i!1") (("1" (use "reverse_nth_TCC1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skolem-typepred) (("2" (rewrite "reverse_index" :dir rl) (("2" (assert) (("2" (use "reverse_nth_TCC1" ("fseq" "fseq!1")) (("2" (ground) (("2" (lemma "reverse_nth") (("2" (inst - "fseq!1" "length(fseq!1) - i!1 - 1") (("1" (assert) (("1" (inst + "length(fseq!1) - 1 - i!1") (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "reverse_index") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil csequence_reverse nil) (nth_some formula-decl nil csequence_nth nil) (reverse def-decl "finite_csequence" csequence_reverse nil) (NOT const-decl "[bool -> bool]" booleans nil) (i!1 skolem-const-decl "indexes[T](fseq!1)" csequence_reverse nil) (reverse_index formula-decl nil csequence_reverse nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (length def-decl "{n | has_length(fseq, n)}" csequence_length nil) (has_length def-decl "bool" csequence_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (i!1 skolem-const-decl "indexes[T](reverse(fseq!1))" csequence_reverse nil) (fseq!1 skolem-const-decl "finite_csequence[T]" csequence_reverse nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (reverse_nth_TCC1 subtype-tcc nil csequence_reverse nil) (int_minus_int_is_int application-judgement "int" integers nil) (indexes type-eq-decl nil csequence_nth nil) (index? def-decl "bool" csequence_nth nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (reverse_nth formula-decl nil csequence_reverse nil) (pred type-eq-decl nil defined_types 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)) shostak)) (reverse_every 0 (reverse_every-1 nil 3513693064 ("" (skolem!) (("" (lemma "every_some_rew") (("" (inst-cp - "p!1" "reverse(fseq!1)") (("" (inst - "p!1" "fseq!1") (("" (use "reverse_some") (("" (prop) nil nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil csequence_reverse nil) (every_some_rew formula-decl nil csequence_props nil) (pred_NOT const-decl "bool" csequence_props nil) (reverse_some formula-decl nil csequence_reverse nil) (reverse def-decl "finite_csequence" csequence_reverse nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (is_finite inductive-decl "bool" csequence_props nil) (csequence type-decl nil csequence_codt nil) (pred type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak))) ¤ Dauer der Verarbeitung: 0.42 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 |
