| products/sources/formale sprachen/PVS/structures/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: more_list_props.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(more_list_props
(prefix?_TCC1 0 (prefix?_TCC1-1 nil 3286895430 ("" (termination-tcc) nil nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (length def-decl "nat" list_props nil)) shostak)) (suffix?_TCC1 0 (suffix?_TCC1-1 nil 3286897128 ("" (lemma "length_reverse[T]") (("" (grind) nil nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (length def-decl "nat" list_props nil) (list type-decl nil list_adt nil) (length_reverse formula-decl nil list_props nil) (T formal-type-decl nil more_list_props nil)) shostak)) (caret_TCC1 0 (caret_TCC1-1 nil 3287764724 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (caret_TCC2 0 (caret_TCC2-1 nil 3287764724 ("" (termination-tcc) nil nil) nil shostak)) (caret_TCC3 0 (caret_TCC3-1 nil 3287771390 ("" (subtype-tcc) nil nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (caret_TCC4 0 (caret_TCC4-1 nil 3287771390 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (caret_TCC5 0 (caret_TCC5-1 nil 3287771390 ("" (termination-tcc) (("" (postpone) 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) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (caret_TCC6 0 (caret_TCC6-1 nil 3287774349 ("" (termination-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) shostak)) (prefix_length 0 (prefix_length-1 nil 3287327236 ("" (skosimp*) (("" (expand "prefix?") (("" (assert) nil nil)) nil)) nil) ((prefix? def-decl "bool" more_list_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (suffix_length 0 (suffix_length-1 nil 3287327263 ("" (skosimp*) (("" (expand "suffix?") (("" (assert) nil nil)) nil)) nil) ((suffix? def-decl "bool" more_list_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (every_forall 0 (every_forall-1 nil 3286897625 ("" (skeep) (("" (rewrite "every_nth") nil nil)) nil) ((every_nth formula-decl nil list_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (T formal-type-decl nil more_list_props nil)) shostak)) (some_exists 0 (some_exists-1 nil 3287148696 ("" (induct "L") (("1" (grind) nil nil) ("2" (skosimp*) (("2" (inst?) (("2" (rewrite "some" +) (("2" (replace -1) (("2" (hide -1) (("2" (prop) (("1" (rewrite "nth") (("1" (inst?) (("1" (assert) nil nil) ("2" (assert) (("2" (rewrite "length") (("2" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst 1 "n!1+1") (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (inst + "n!1-1") (("1" (grind) (("1" (expand "nth") (("1" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (typepred "n!1") (("2" (rewrite "length" -) (("2" (assert) (("2" (hide -1) (("2" (rewrite "nth" -) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (n!1 skolem-const-decl "below(length(cons(cons1_var!1, cons2_var!1)))" more_list_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (n!1 skolem-const-decl "below(length(cons2_var!1))" more_list_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (cons2_var!1 skolem-const-decl "list[T]" more_list_props nil) (cons1_var!1 skolem-const-decl "T" more_list_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (list_induction formula-decl nil list_adt nil) (T formal-type-decl nil more_list_props nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (below type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (< const-decl "bool" reals 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) (some adt-def-decl "boolean" list_adt nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil)) shostak)) (list_extensionality_TCC1 0 (list_extensionality_TCC1-1 nil 3546992291 ("" (subtype-tcc) nil nil) ((below type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (list type-decl nil list_adt nil) (T formal-type-decl nil more_list_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) (< const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (list_extensionality 0 (list_extensionality-1 nil 3546992303 ("" (induct "l1") (("1" (grind) nil nil) ("2" (skeep) (("2" (skeep) (("2" (case "null?(l2)") (("1" (grind) nil nil) ("2" (lemma "list_cons_eta[T]") (("2" (inst -1 "l2") (("1" (replaces -1 :dir rl) (("1" (split) (("1" (flatten) (("1" (replaces -1) (("1" (skeep) nil nil)) nil)) nil) ("2" (flatten) (("2" (rewrite "list_cons_extensionality[T]") (("1" (inst -2 "0") (("1" (expand "nth") (("1" (propax) nil nil)) nil) ("2" (expand "length" 1) (("2" (assert) nil nil)) nil)) nil) ("2" (expand "length" -1) (("2" (inst -3 "cdr(l2)") (("2" (assert) (("2" (skeep 4) (("2" (inst -2 "n+1") (("1" (expand "nth" -2) (("1" (propax) nil nil)) nil) ("2" (expand "length" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ((cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (l2 skolem-const-decl "list[T]" more_list_props nil) (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (list_cons_extensionality formula-decl nil list_adt nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (cons2_var skolem-const-decl "list[T]" more_list_props nil) (cons1_var skolem-const-decl "T" more_list_props nil) (n skolem-const-decl "below(length(cons2_var))" more_list_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (list_cons_eta formula-decl nil list_adt nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (null adt-constructor-decl "(null?)" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (list_induction formula-decl nil list_adt nil) (T formal-type-decl nil more_list_props nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (= const-decl "[T, T -> boolean]" equalities 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) (length def-decl "nat" list_props nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil)) shostak)) (list_pigeonhole 0 (list_pigeonhole-1 nil 3287156645 ("" (measure-induct "card(A)" "A" 1) (("" (skosimp*) (("" (rewrite "length" -) (("" (lift-if) (("" (ground) (("" (inst - "remove(car(B!1), x!1)") (("" (rewrite "card_remove") (("" (rewrite "every") (("" (flatten) (("" (assert) (("" (inst - "cdr(B!1)") (("" (prop) (("1" (skosimp*) (("1" (inst + "n!1+1" "m!1+1") (("1" (expand "nth" +) (("1" (assert) nil nil)) nil) ("2" (typepred "m!1") (("2" (assert) (("2" (rewrite "length" +) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (typepred "n!1") (("3" (rewrite "length" +) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst + 0 _) (("1" (rewrite "nth" +) (("1" (expand "remove") (("1" (expand "member") (("1" (rewrite "every_forall") (("1" (rewrite "every_forall") (("1" (skosimp*) (("1" (inst 3 "n!1+1") (("1" (inst -3 "n!1") (("1" (assert) (("1" (rewrite "nth" 3) (("1" (assert) nil nil) ("2" (typepred "n!1") (("2" (rewrite "length" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "n!1") (("2" (rewrite "length" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "length" 1) (("2" (assert) nil nil)) nil)) nil) ("2" (rewrite "length" 1) (("2" (assert) nil nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((finite_remove application-judgement "finite_set" finite_sets nil) (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (remove const-decl "set" sets 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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (B!1 skolem-const-decl "list[T]" more_list_props nil) (n!1 skolem-const-decl "below[length(cdr(B!1))]" more_list_props nil) (m!1 skolem-const-decl "below[length(cdr(B!1))]" more_list_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (member const-decl "bool" sets nil) (below type-eq-decl nil naturalnumbers nil) (n!1 skolem-const-decl "below(length(cdr(B!1)))" more_list_props nil) (every_forall formula-decl nil more_list_props nil) (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) (int_minus_int_is_int application-judgement "int" integers nil) (card_remove formula-decl nil finite_sets nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nth def-decl "T" list_props nil) (/= const-decl "boolean" notequal nil) (below type-eq-decl nil nat_types nil) (length def-decl "nat" list_props nil) (> const-decl "bool" reals nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (list type-decl nil list_adt nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (= const-decl "[T, T -> boolean]" equalities 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_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil more_list_props 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)) (nth_append_TCC1 0 (nth_append_TCC1-1 nil 3577469759 ("" (skeep) (("" (rewrite "length_append") nil nil)) nil) ((nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (length_append formula-decl nil list_props nil) (list type-decl nil list_adt nil) (T formal-type-decl nil more_list_props nil)) nil)) (nth_append_TCC2 0 (nth_append_TCC2-1 nil 3577469759 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (nth_append 0 (nth_append-1 nil 3577469817 ("" (induct "l1") (("1" (grind) nil nil) ("2" (skolem 1 ("a" "l")) (("2" (flatten) (("2" (skeep) (("2" (case-replace "length(cons(a,l))=length(l)+1") (("1" (hide -1) (("1" (expand "append" 1) (("1" (lift-if) (("1" (case-replace "i < 1 + length(l)") (("1" (expand "nth" 1) (("1" (case-replace "i=0") (("1" (assert) (("1" (inst? -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "nth" 2 1) (("2" (inst? -) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "length" 1 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skeep) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (skeep) (("4" (rewrite "length_append") nil nil)) nil)) nil)) nil) ((length_append formula-decl nil list_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (list_induction formula-decl nil list_adt nil) (T formal-type-decl nil more_list_props nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (length def-decl "nat" list_props nil) (append def-decl "list[T]" list_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil)) shostak)) (length_null 0 (length_null-1 nil 3580049561 ("" (grind) nil nil) ((length def-decl "nat" list_props nil)) shostak)) (length_singleton 0 (length_singleton-1 nil 3580049452 ("" (grind) nil nil) ((length def-decl "nat" list_props nil)) shostak)) (length_null_list 0 (length_null_list-1 nil 3601030512 ("" (skeep) (("" (ground) (("1" (expand "length" -1) (("1" (assert) nil nil)) nil) ("2" (expand "length") (("2" (propax) nil nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (length def-decl "nat" list_props nil)) shostak)) (reverse_def_TCC1 0 (reverse_def_TCC1-1 nil 3601030498 ("" (skeep) (("" (rewrite "length_reverse") nil nil)) nil) ((length_reverse formula-decl nil list_props nil) (list type-decl nil list_adt nil) (T formal-type-decl nil more_list_props nil)) nil)) (reverse_def_TCC2 0 (reverse_def_TCC2-1 nil 3601030498 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (reverse_def 0 (reverse_def-1 nil 3601030538 ("" (case "NOT forall (lpr:list[T],j:nat,k:nat): k+1=length(lpr) AND j (("1" (hide 2) (("1" (induct "k") (("1" (skeep) (("1" (assert) (("1" (case "NOT j = 0") (("1" (assert) nil nil) ("2" (replaces -1) (("2" (assert) (("2" (copy -1) (("2" (hide -3) (("2" (replace -1 :dir rl) (("2" (assert) (("2" (expand "nth" +) (("2" (copy -1) (("2" (expand "length" -1) (("2" (expand "length" -1) (("2" (lift-if) (("2" (ground) (("2" (expand "reverse" +) (("2" (expand "reverse" +) (("2" (expand "append") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (expand "reverse" +) (("2" (lemma "length_null_list") (("2" (inst - "lpr!1") (("2" (assert) (("2" (rewrite "nth_append") (("1" (lift-if) (("1" (ground) (("1" (name "kk" "j!1") (("1" (replaces -1) (("1" (assert) (("1" (inst - "cdr(lpr!1)" "j!2-1") (("1" (assert) (("1" (split -) (("1" (case "length(cdr(lpr!1)) = length(lpr!1)-1") (("1" (replaces -1) (("1" (replaces -1 :dir rl) (("1" (expand "nth" + 1) (("1" (lift-if) (("1" (ground) (("1" (replaces -1) (("1" (assert) (("1" (rewrite "length_reverse") (("1" (expand "length" - 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "length" 1 2) (("2" (propax) nil nil)) nil)) nil) ("2" (expand "length" -2) (("2" (assert) nil nil)) nil) ("3" (expand "length" -3) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "NOT j!2 = 0") (("1" (assert) nil nil) ("2" (replaces -1) (("2" (rewrite "length_reverse") (("2" (expand "length" -1 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "length_reverse") (("2" (expand "length" 1 1) (("2" (assert) (("2" (case "NOT j!2 = 0") (("1" (assert) nil nil) ("2" (replaces -1) (("2" (assert) (("2" (expand "length" 2 1) (("2" (hide -) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "length_reverse") (("2" (expand "length" 1 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) (("3" (rewrite "length_reverse") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (inst - "L" "length(L)-1-j" "length(L)-1") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) (("3" (rewrite "length_reverse") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((int_plus_int_is_int application-judgement "int" integers nil) (j skolem-const-decl "nat" more_list_props nil) (L skolem-const-decl "list[T]" more_list_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (null adt-constructor-decl "(null?)" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (nth_append formula-decl nil more_list_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (length_singleton formula-decl nil more_list_props nil) (j!2 skolem-const-decl "nat" more_list_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (length_reverse formula-decl nil list_props nil) (length_null_list formula-decl nil more_list_props nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (append def-decl "list[T]" list_props nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers 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 more_list_props nil) (list type-decl nil list_adt 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (length def-decl "nat" list_props nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (reverse def-decl "list[T]" list_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil)) shostak)) (cons_append 0 (cons_append-1 nil 3613292587 ("" (skeep) (("" (rewrite "list_extensionality") (("" (split) (("1" (expand "length" 1 1) (("1" (rewrite "length_append") nil nil)) nil) ("2" (skeep) (("2" (rewrite "nth_append") (("1" (expand "nth" 1) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (expand "nth") (("1" (propax) nil nil)) nil) ("2" (expand "nth" + 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "n") (("2" (expand "length" -1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((list_extensionality formula-decl nil more_list_props nil) (T formal-type-decl nil more_list_props nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (append def-decl "list[T]" list_props nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (NOT const-decl "[bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (nth_append formula-decl nil more_list_props nil) (length def-decl "nat" list_props nil) (length_append formula-decl nil list_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (length_singleton formula-decl nil more_list_props nil)) shostak)) (expand_list_TCC1 0 (expand_list_TCC1-1 nil 3613298395 ("" (subtype-tcc) nil nil) nil nil)) (expand_list 0 (expand_list-1 nil 3613298397 ("" (skeep) (("" (lemma "list_extensionality") (("" (inst?) (("" (assert) (("" (hide 3) (("" (split) (("1" (expand "length") (("1" (propax) nil nil)) nil) ("2" (skeep) (("2" (expand "nth") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((list_extensionality formula-decl nil more_list_props nil) (length def-decl "nat" list_props nil) (nth def-decl "T" list_props nil) (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (T formal-type-decl nil more_list_props nil)) shostak)) (append_null_left 0 (append_null_left-1 nil 3613298991 ("" (grind) nil nil) ((append def-decl "list[T]" list_props nil)) shostak))) ¤ Dauer der Verarbeitung: 0.31 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 |
