| products/Sources/formale Sprachen/PVS/Sturm/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Sprache: LispOriginal von: PVS© |
|
||||||
|
(polylist
(eval_polylist_TCC1 0 (eval_polylist_TCC1-1 nil 3601220513 ("" (subtype-tcc) nil nil) ((listn_0 name-judgement "listn[rat](0)" polylist 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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist nil) (>= const-decl "bool" reals 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (upfrom nonempty-type-eq-decl nil integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil)) (eval_polylist_TCC2 0 (eval_polylist_TCC2-1 nil 3601220513 ("" (subtype-tcc) nil nil) ((listn_0 name-judgement "listn[rat](0)" polylist 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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist nil) (>= const-decl "bool" reals 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (upfrom nonempty-type-eq-decl nil integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil)) (eval_polylist_TCC3 0 (eval_polylist_TCC3-1 nil 3601220513 ("" (termination-tcc) nil nil) ((listn_0 name-judgement "listn[rat](0)" polylist 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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist nil) (>= const-decl "bool" reals 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (upfrom nonempty-type-eq-decl nil integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (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)) nil)) (eval_polylist_TCC4 0 (eval_polylist_TCC4-1 nil 3601220513 ("" (subtype-tcc) nil nil) ((listn_0 name-judgement "listn[rat](0)" polylist 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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist nil) (>= const-decl "bool" reals 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (upfrom nonempty-type-eq-decl nil integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil)) (eval_polylist_TCC5 0 (eval_polylist_TCC5-1 nil 3601224651 ("" (termination-tcc) nil nil) ((listn_0 name-judgement "listn[rat](0)" polylist 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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist nil) (>= const-decl "bool" reals 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (upfrom nonempty-type-eq-decl nil integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers 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) (length def-decl "nat" list_props nil)) nil)) (eval_polylist_times_x_TCC1 0 (eval_polylist_times_x_TCC1-1 nil 3601231397 ("" (subtype-tcc) nil nil) nil nil)) (eval_polylist_times_x_TCC2 0 (eval_polylist_times_x_TCC2-1 nil 3601231397 ("" (subtype-tcc) nil nil) nil nil)) (eval_polylist_times_x 0 (eval_polylist_times_x-1 nil 3601231398 ("" (induct "pl") (("1" (grind) nil nil) ("2" (ground) nil nil) ("3" (ground) (("3" (skeep) (("3" (skeep) (("3" (assert) (("3" (expand "eval_polylist" +) (("3" (lift-if) (("3" (split +) (("1" (grind) nil nil) ("2" (flatten) (("2" (assert) (("2" (inst?) (("1" (assert) (("1" (lemma "expt_plus") (("1" (inst - "(deg - length(cons(cons1_var, cons2_var)))" "1" "x") (("1" (expand "^" -1 3) (("1" (expand "expt" -1) (("1" (expand "expt" -1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replaces -1) (("2" (assert) (("2" (expand "^" 2) (("2" (expand "expt" 2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (typepred "deg") (("2" (expand "length" -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_plus_int_is_int application-judgement "int" integers nil) (minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (expt def-decl "real" exponentiation nil) (^ const-decl "real" exponentiation nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (x skolem-const-decl "real" polylist nil) (nzreal nonempty-type-eq-decl nil reals nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (nat_exp application-judgement "nat" exponentiation nil) (expt_plus formula-decl nil exponentiation nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (deg skolem-const-decl "upfrom(length(cons(cons1_var, cons2_var)))" polylist nil) (cons2_var skolem-const-decl "list[rat]" polylist nil) (cons1_var skolem-const-decl "rat" polylist nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (list_induction formula-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) (rat nonempty-type-eq-decl nil rationals nil) (eval_polylist def-decl "real" polylist nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (Polylist type-eq-decl nil polylist nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (upfrom nonempty-type-eq-decl nil integers nil) (length def-decl "nat" 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) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (list type-decl nil list_adt nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (eval_polylist_remove_acc 0 (eval_polylist_remove_acc-1 nil 3601307736 ("" (induct "pl") (("1" (grind) nil nil) ("2" (assert) nil nil) ("3" (skeep) (("3" (assert) (("3" (skeep) (("3" (expand "eval_polylist" +) (("3" (lift-if) (("3" (split +) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (assert) (("2" (copy -1) (("2" (inst?) (("2" (replaces -1) (("2" (invoke (name "AA" "%1") (! 2 1)) (("2" (replace -1) (("2" (hide -1) (("2" (inst?) (("2" (replace -1) (("2" (expand "AA") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((AA skolem-const-decl "real" polylist nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (list_induction formula-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) (rat nonempty-type-eq-decl nil rationals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (eval_polylist def-decl "real" polylist nil) (Polylist type-eq-decl nil polylist nil) (= const-decl "[T, T -> boolean]" equalities nil) (upfrom nonempty-type-eq-decl nil integers nil) (length def-decl "nat" list_props nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (list type-decl nil list_adt nil)) shostak)) (eval_polylist_test_TCC1 0 (eval_polylist_test_TCC1-1 nil 3601225669 ("" (grind) nil nil) ((every adt-def-decl "boolean" list_adt nil) (listn_0 name-judgement "listn[rat](0)" polylist nil)) nil)) (eval_polylist_test_TCC2 0 (eval_polylist_test_TCC2-1 nil 3601225669 ("" (grind) nil nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (length def-decl "nat" list_props nil)) nil)) (eval_polylist_test_TCC3 0 (eval_polylist_test_TCC3-1 nil 3601225669 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (eval_polylist_test_TCC4 0 (eval_polylist_test_TCC4-1 nil 3601728884 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (eval_polylist_test 0 (eval_polylist_test-1 nil 3601225671 ("" (grind) nil nil) ((length def-decl "nat" list_props nil) (expt def-decl "real" exponentiation nil) (^ const-decl "real" exponentiation nil) (eval_polylist def-decl "real" polylist nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (polylist_TCC1 0 (polylist_TCC1-1 nil 3601220513 ("" (subtype-tcc) nil nil) nil nil)) (pmonom_TCC1 0 (pmonom_TCC1-1 nil 3601224651 ("" (grind) nil nil) ((length def-decl "nat" list_props nil) (/= const-decl "boolean" notequal nil)) nil)) (pmonom_TCC2 0 (pmonom_TCC2-1 nil 3601313859 ("" (skeep) (("" (split) (("1" (replaces -1) (("1" (grind) nil nil)) nil) ("2" (replaces -1) (("2" (grind) nil nil)) nil)) nil)) nil) ((pconst const-decl "Polylist" polylist nil) (length def-decl "nat" list_props nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (polylist const-decl "real" polylist nil) (eval_polylist def-decl "real" polylist nil) (^ const-decl "real" exponentiation nil) (expt def-decl "real" exponentiation nil)) nil)) (pmonom_TCC3 0 (pmonom_TCC3-1 nil 3601313859 ("" (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)) nil)) (pmonom_TCC4 0 (pmonom_TCC4-1 nil 3601313859 ("" (termination-tcc) nil nil) nil nil)) (pmonom_TCC5 0 (pmonom_TCC5-1 nil 3601313859 ("" (skeep) (("" (invoke (case "NOT %1") (! 2 1)) (("1" (hide 3) (("1" (expand "length" +) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (skeep) (("2" (typepred "v(c,deg-1)") (("2" (inst - "x") (("2" (expand "^") (("2" (expand "expt" +) (("2" (mult-by -4 "x") (("2" (replace -1 :dir rl) (("2" (expand "polylist" +) (("2" (expand "eval_polylist" + 1) (("2" (expand "length" 2 1) (("2" (rewrite "eval_polylist_times_x") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) 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) (posint_plus_nnint_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) (number nonempty-type-decl nil numbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (rat nonempty-type-eq-decl nil 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) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (< const-decl "bool" reals nil) (Polylist type-eq-decl nil polylist nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polylist const-decl "real" polylist nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (listn_0 name-judgement "listn[rat](0)" polylist nil) (expt def-decl "real" exponentiation nil) (eval_polylist def-decl "real" polylist nil) (upfrom nonempty-type-eq-decl nil integers nil) (eval_polylist_times_x formula-decl nil polylist nil) (real_times_real_is_real application-judgement "real" reals nil) (both_sides_times1_imp formula-decl nil extra_real_props nil)) nil)) (psum_TCC1 0 (psum_TCC1-1 nil 3601220513 ("" (skeep*) (("" (expand "polylist" + 2) (("" (expand "length" +) (("" (expand "length" +) (("" (assert) (("" (expand "eval_polylist") (("" (expand "length" +) (("" (expand "length" +) (("" (expand "^" +) (("" (expand "expt") (("" (expand "polylist" +) (("" (expand "length" + 1) (("" (expand "eval_polylist" +) (("" (lift-if) (("" (lift-if) (("" (lift-if) (("" (assert) (("" (ground) (("1" (grind) nil nil) ("2" (replace -5 :dir rl) (("2" (expand "length" + 3) (("2" (expand "length" + 3) (("2" (case "x^0=1") (("1" (assert) (("1" (replaces -1) (("1" (rewrite "eval_polylist_remove_acc" +) (("1" (invoke (name "AA" "%1") (! 2 1)) (("1" (replace -1) (("1" (hide -1) (("1" (rewrite "eval_polylist_remove_acc" +) (("1" (expand "AA") (("1" (assert) (("1" (expand "length" + 2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((polylist const-decl "real" polylist nil) (eval_polylist def-decl "real" polylist nil) (expt def-decl "real" exponentiation nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (>= const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans 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_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) (real nonempty-type-from-decl nil reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (AA skolem-const-decl "real" polylist nil) (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) (upfrom nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (Polylist type-eq-decl nil polylist nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (rat nonempty-type-eq-decl nil rationals 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) (eval_polylist_remove_acc formula-decl nil polylist nil) (real_times_real_is_real application-judgement "real" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (^ const-decl "real" exponentiation nil) (rat_plus_rat_is_rat application-judgement "rat" rationals nil) (real_plus_real_is_real application-judgement "real" reals nil) (length def-decl "nat" list_props nil) (listn_0 name-judgement "listn[rat](0)" polylist nil)) nil)) (psum_TCC2 0 (psum_TCC2-2 nil 3601315963 ("" (skeep*) (("" (expand "polylist" + 3) (("" (expand "length" +) (("" (expand "length" +) (("" (assert) (("" (expand "eval_polylist") (("" (expand "length" +) (("" (expand "length" +) (("" (expand "^" +) (("" (expand "expt") (("" (expand "polylist" +) (("" (expand "length" + 1) (("" (expand "eval_polylist" +) (("" (assert) (("" (expand "length" + 3) (("" (expand "length" + 3) (("" (case "x^0=1") (("1" (assert) (("1" (replaces -1) (("1" (rewrite "eval_polylist_remove_acc" +) (("1" (invoke (name "AA" "%1") (! 2 1)) (("1" (replace -1) (("1" (hide -1) (("1" (rewrite "eval_polylist_remove_acc" +) (("1" (expand "AA") (("1" (assert) (("1" (expand "length" + 2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((polylist const-decl "real" polylist nil) (eval_polylist def-decl "real" polylist nil) (expt def-decl "real" exponentiation nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (eval_polylist_remove_acc formula-decl nil polylist 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) (rat nonempty-type-eq-decl nil rationals nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (upfrom nonempty-type-eq-decl nil integers nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) (AA skolem-const-decl "real" polylist nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (real nonempty-type-from-decl nil reals 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) (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) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (>= const-decl "bool" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (^ const-decl "real" exponentiation nil) (rat_plus_rat_is_rat application-judgement "rat" rationals nil) (real_plus_real_is_real application-judgement "real" reals nil) (length def-decl "nat" list_props nil) (listn_0 name-judgement "listn[rat](0)" polylist nil)) nil) (psum_TCC2-1 nil 3601220513 ("" (termination-tcc) nil nil) ((list type-decl nil list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)) nil)) (psum_TCC3 0 (psum_TCC3-1 nil 3601225382 ("" (termination-tcc) nil nil) ((listn_0 name-judgement "listn[rat](0)" polylist 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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist nil)) nil)) (psum_TCC4 0 (psum_TCC4-1 nil 3601315195 ("" (subtype-tcc) nil nil) ((listn_0 name-judgement "listn[rat](0)" polylist 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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist nil)) nil)) (psum_TCC5 0 (psum_TCC5-1 nil 3601315195 ("" (termination-tcc) nil nil) ((length def-decl "nat" list_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (psum_TCC6 0 (psum_TCC6-1 nil 3601315195 ("" (skeep*) (("" (expand "polylist" +) (("" (expand "length" + 1) (("" (expand "eval_polylist" +) (("" (assert) (("" (lift-if) (("" (ground) (("" (expand "length" + 3) (("" (expand "length" + 3) (("" (case "x^0=1") (("1" (replaces -1) (("1" (assert) (("1" (rewrite "eval_polylist_remove_acc" +) (("1" (invoke (name "AA" "%1") (! 2 1)) (("1" (replaces -1) (("1" (rewrite "eval_polylist_remove_acc" +) (("1" (invoke (name "BB" "%1") (! 2 2 1)) (("1" (replaces -1) (("1" (rewrite "eval_polylist_remove_acc" +) (("1" (expand "AA") (("1" (expand "BB") (("1" (assert) (("1" (typepred "v(cdr[rat](pl), cdr[rat](ql))") (("1" (inst - "x") (("1" (expand "polylist" -) (("1" (lemma "eval_polylist_times_x") (("1" (case "0 = 0*x") (("1" (replaces -1 +) (("1" (rewrite -1 + :dir rl) (("1" (invoke (name "AAA" "%1") (! 2 1)) (("1" (replaces -1) (("1" (rewrite -1 + :dir rl) (("1" (invoke (name "BBB" "%1") (! 2 2 1)) (("1" (replaces -1) (("1" (rewrite -1 + :dir rl) (("1" (expand "AAA") (("1" (expand "BBB") (("1" (expand "length" 2 2) (("1" (expand "length" 2 3) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "length" 1 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "length" 1 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((polylist const-decl "real" polylist nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (eval_polylist def-decl "real" polylist nil) (^ const-decl "real" exponentiation nil) (>= const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans 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_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) (real nonempty-type-from-decl nil reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (AA skolem-const-decl "real" polylist nil) (eval_polylist_times_x formula-decl nil polylist nil) (pl skolem-const-decl "Polylist" polylist nil) (AAA skolem-const-decl "real" polylist nil) (BBB skolem-const-decl "real" polylist nil) (ql skolem-const-decl "Polylist" polylist nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (NOT const-decl "[bool -> bool]" booleans nil) (BB skolem-const-decl "real" polylist nil) (upfrom nonempty-type-eq-decl nil integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (Polylist type-eq-decl nil polylist nil) (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (rat nonempty-type-eq-decl nil rationals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (eval_polylist_remove_acc formula-decl nil polylist nil) (expt def-decl "real" exponentiation nil) (rat_plus_rat_is_rat application-judgement "rat" rationals nil) (real_plus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (length def-decl "nat" list_props nil) (listn_0 name-judgement "listn[rat](0)" polylist nil)) nil)) (pscal_TCC1 0 (pscal_TCC1-1 nil 3601227496 ("" (skeep) (("" (grind) nil nil)) nil) ((length def-decl "nat" list_props nil) (expt def-decl "real" exponentiation nil) (^ const-decl "real" exponentiation nil) (eval_polylist def-decl "real" polylist nil) (polylist const-decl "real" polylist nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (listn_0 name-judgement "listn[rat](0)" polylist nil)) nil)) (pscal_TCC2 0 (pscal_TCC2-1 nil 3601747475 ("" (termination-tcc) nil nil) ((listn_0 name-judgement "listn[rat](0)" polylist 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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (rat nonempty-type-eq-decl nil rationals nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Polylist type-eq-decl nil polylist nil)) nil)) (pscal_TCC3 0 (pscal_TCC3-1 nil 3601747631 ("" (termination-tcc) nil nil) ((length def-decl "nat" list_props nil)) nil)) (pscal_TCC4 0 (pscal_TCC4-1 nil 3601747631 ("" (skeep) (("" (split) (("1" (expand "length" + 1) (("1" (assert) (("1" (typepred "v(c,cdr[rat](pl))") (("1" (replace -3) (("1" (expand "length" + 2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (expand "polylist" +) (("2" (expand "length" + 1) (("2" (typepred "v(c,cdr[rat](pl))") (("1" (expand "polylist") (("1" (expand "eval_polylist" +) (("1" (lift-if) (("1" (split) (("1" (flatten) (("1" (grind) nil nil)) nil) ("2" (flatten) (("2" (assert) (("2" (expand "length" + 3) (("2" (case "x^0=1") (("1" (replaces -1) (("1" (assert) (("1" (rewrite "eval_polylist_remove_acc" +) (("1" (invoke (name "AA" "%1") (! 2 1)) (("1" (replace -1) (("1" (rewrite "eval_polylist_remove_acc" +) (("1" (hide -1) (("1" (expand "AA") (("1" (assert) (("1" (inst - "x") (("1" (mult-by -4 "x") (("1" (rewrite "eval_polylist_times_x") (("1" (name "BBC" "eval_polylist(cdr[rat](pl), length(cdr[rat](pl)) - 1, 0)(x) * x") (("1" (rewrite "eval_polylist_times_x" -1) (("1" (expand "BBC" -1) (("1" (mult-by -1 "c") (("1" (replace -1 :dir rl) (("1" (assert) (("1" (expand "length" 2 2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers 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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.48 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 |
