(more_list_propsnil 3500358324"" (skolem 1 ("PP" _))"" (induct "pl" )"1" (grind) nil nil )"2" (skosimp* :preds? t)"2" (expand "length" +) (("2" (propax) nil nil )) nil )) nil ))nil ))nil )nil list_adt nil )"boolean" list_adt nil )nil numbers nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"nat" list_props nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil more_list_props nil )nil list_adt nil )NOT const-decl "[bool -> bool]" booleans nil ))nil 3500358260"" (skosimp* :preds? t)"" (use "length_parm" ) (("" (assert ) nil nil )) nil )) nil )nil more_list_props nil )"(strict_total_order?[real])" real_props nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil more_list_props nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"nat" list_props nil )nil nat_types nil ))nil ))nil 3500358406"" (skolem 1 ("PP" _ _))"" (induct "pl" )"1" (grind) nil nil )"2" (skosimp* :preds? t)"2" (expand "nth" +)"2" (lift-if)"2" (prop) (("2" (inst?) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (grind)"3" (hide-all-but (-3 1))"3" (use "length_parm" ) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )nil nat_types nil )"nat" list_props nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"PRED[T]" more_list_props nil )"boolean" list_adt nil )nil list_adt nil )"[T, T -> boolean]" equalities nil )"T" list_props nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil more_list_props nil )nil list_adt nil )"(null?)" list_adt nil )"[list -> boolean]" list_adt nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"below[length(cons(cons1_var!1, cons2_var!1))]" more_list_propsnil )"list[(PP)]" more_list_props nil )"(PP)" more_list_props nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"(total_order?[real])" nil )"[[T, list] -> (cons?)]" list_adt nil )"[list -> boolean]" list_adt nil )nil more_list_props nil ))nil 3500357635"" (skosimp* :preds? t)"" (iff)"" (prop)"1" (rewrite "every_nth" )"1" (rewrite "every_nth" )"1" (rewrite "every_nth" )"1" (skosimp* :preds? t)"1" (expand "restrict" )"1" (inst?)"1" (inst?)"1" (assert )"1" (hide -1 -3)"1" (lemma "nth_parm" )"1" (inst -1 "P!1" "pl!1" "i!1" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (use "length_parm" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "every_nth" )"2" (rewrite "every_nth" )"2" (rewrite "every_nth" )"2" (skosimp* :preds? t)"2" (expand "restrict" )"2" (inst?)"1" (inst?)"1" (assert )"1" (hide -1 -3)"1" (lemma "nth_parm" )"1" (inst -1 "P!1" "pl!1" "i!1" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (use "length_parm" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"below(length(pl!1))" more_list_props nil )nil list_props nil )"R" restrict nil )nil more_list_props nil )nil nat_types nil )nil more_list_props nil )"below(length[T](pl!1))" more_list_propsnil )"list[(P!1)]" more_list_props nil )"PRED[T]" more_list_props nil )"(strict_total_order?[real])" real_props nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"nat" list_props nil )nil naturalnumbers nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil more_list_props nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil ))nil 3520967096"" (skolem 1 ("P" "_" "_" ))"" (induct "l1" )"1" (grind) nil nil )"2" (skosimp)"2" (skosimp)"2" (expand "append" +)"2" (inst -1 "l2!1" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil list_adt nil )"boolean" list_adt nil )"[T, T -> boolean]" equalities nil )"list[T]" list_props nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil more_list_props nil )nil list_adt nil ))nil 3520141411"" (induct "l1" )"1" (grind) nil nil )"2" (skeep :preds? t)"2" (skeep :preds? t)"2" (expand "append" 1 1)"2" (expand "append" 1 3)"2" (expand "append" 1 2)"2" (decompose-equality 1) (("2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil list_adt nil )nil list_adt nil )nil more_list_props nil )"(null?)" list_adt nil )"[list -> boolean]" list_adt nil )"[[T, list] -> (cons?)]" list_adt nil )"[list -> boolean]" list_adt nil )"list[T]" list_props nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil list_adt nil ))nil 3520140894"" (induct "l2" )"1" (induct "l1" )"1" (skeep :preds? t)"1" (expand "append" -2) (("1" (propax) nil nil )) nil )) nil ))nil )"2" (skeep :preds? t)"2" (induct "l1" )"2" (skeep :preds? t)"2" (expand "append" -2)"2" (decompose-equality -2)"2" "append(cons2_var_1, cons(cons1_var, cons2_var)) = " :hide? "1" (hide -3)"1" "append(cons2_var_1, cons(cons1_var, null))" )"1" (assert )"1" (expand "append" -3)"1" (lift-if) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (use "append_append_cons" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[(cons?) -> list]" list_adt nil )"[(cons?) -> T]" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil more_list_props nil )"[[T, list] -> (cons?)]" list_adt nil )"[list -> boolean]" list_adt nil )nil list_adt nil )nil more_list_props nil )"(null?)" list_adt nil )"[list -> boolean]" list_adt nil )"list[T]" list_props nil )"[T, T -> boolean]" equalities nil )"[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil list_adt nil ))nil 3520951758"" (induct "l1" )"1" (grind) nil nil )"2" (skosimp)"2" (skosimp)"2" (expand "append" +)"2" (expand "length" +)"2" (expand "length" -2)"2" (inst?)"2" (inst?)"2" (assert )"2" (rewrite "length_append" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil list_props nil )"nonneg_int" nil )"(strict_total_order?[real])" real_props nil )"posint" nil )nil list_adt nil )nil more_list_props nil )"list[T]" list_props nil )"nat" list_props nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil booleans nil )nil list_adt nil ))nil ))nil 3520951770"" (induct "l1" )"1" (grind) nil nil )"2" (skosimp :preds? t)"2" (skosimp :preds? t)"2" (expand "append" 1 1)"2" (expand "nth" +)"2" (lift-if)"2" (prop)"2" (inst?)"1" (assert )"1" (expand "length" -2) (("1" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skosimp :preds? t)"3" (rewrite "length_append" ) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil )nil list_props nil )"nonneg_int" nil )"(total_order?[real])" nil )"int" integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" more_list_props nil )"posint" nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil list_adt nil )nil more_list_props nil )"T" list_props nil )nil nat_types nil )"[T, T -> boolean]" equalities nil )nil list_adt nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"nat" list_props nil )"list[T]" list_props nil ))nil 3520951758"" (skosimp)"" (rewrite "length_append" ) (("" (assert ) nil nil )) nil )) nil )nil list_props nil )nil list_adt nil )nil more_list_props nil )"nonneg_int" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil ))nil ))nil 3520952014"" (induct "l1" )"1" (grind) nil nil )"2" (skosimp :preds? t)"2" (skosimp :preds? t)"2" (expand "append" +)"2" (expand "length" +)"2" (expand "nth" 1 1)"2" (lift-if)"2" (expand "length" -3)"2" (assert )"2" (inst -2 "i!1 - 1" "l2!1" )"2" (assert )"2" (expand "append" -3)"2" (expand "length" -3)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp :preds? t)"3" (assert )"3" (assert )"3" (rewrite "length_append" ) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"nonneg_int" nil )nil list_props nil )"(total_order?[real])" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )NOT const-decl "[bool -> bool]" booleans nil )nil list_adt nil )nil more_list_props nil )"T" list_props nil )nil nat_types nil )"[T, T -> boolean]" equalities nil )nil list_adt nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"nat" list_props nil )"bool" reals nil )"list[T]" list_props nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil ))nil 3520133815 ("" (subtype-tcc) nil nil ) nil nil ))nil 3520133815 ("" (termination-tcc) nil nil )"(strict_well_founded?[list])" list_adt nil ))nil ))nil 3520141563"" (induct "l1" )"1" (grind) (("1" (expand "tail?" ) (("1" (propax) nil nil )) nil ))nil )"2" (skeep :preds? t)"2" (expand "append" +)"2" (expand "tail?" +)"2" (skeep :preds? t) (("2" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil )nil list_adt nil )nil more_list_props nil )"list[T]" list_props nil )"bool" more_list_props nil )nil booleans nil )nil booleans nil )nil list_adt nil ))nil 3520133815"" (skeep :preds? t)"" (expand "tail?" ) (("" (assert ) nil nil )) nil )) nil )"bool" more_list_props nil )) nil ))nil 3520133815"" (skeep :preds? t)"" (expand "tail?" -) (("" (assert ) nil nil )) nil )) nil )"bool" more_list_props nil )) nil ))nil 3520133815"" (skeep :preds? t)"" (assert )"" (expand "<<" )"" (lift-if)"" (expand "tail?" ) (("" (prop) nil nil )) nil )) nil ))nil ))nil ))nil )"bool" more_list_props nil )"(strict_well_founded?[list])" list_adt nil ))nil ))nil 3520133815"" (induct "l1" )"1" (grind) (("1" (expand "tail?" ) (("1" (propax) nil nil )) nil ))nil )"2" (skeep :preds? t)"2" (expand "append" +)"2" (expand "tail?" +)"2" (skeep :preds? t)"2" (hide 1) (("2" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil list_adt nil )nil more_list_props nil )"list[T]" list_props nil )"bool" more_list_props nil )nil booleans nil )nil booleans nil )nil list_adt nil ))nil ))nil 3520132082"" (induct "l1" )"1" (grind) nil nil )"2" (skeep :preds? t)"2" (skeep :preds? t)"2" (expand "append" +)"2" (expand "ldiff" +)"2" (lift-if)"2" (prop)"1" (lemma "append_equal_null" )"1" (inst -1 "cons(cons1_var, cons2_var)" "l2" )"1" (expand "append" -1 1)"1" (propax) nil nil )) nil ))nil ))nil )"2" (hide 1)"2" (apply-extensionality :hide? t)"2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skeep :preds? t) (("3" (use "tail_append" ) nil nil )) nil ))nil )nil more_list_props nil )nil list_adt nil )nil more_list_props nil )"[list -> boolean]" list_adt nil )"[[T, list] -> (cons?)]" list_adt nil )nil list_adt nil )nil more_list_props nil )"list[T]" more_list_props nil )"[T, T -> boolean]" equalities nil )nil list_adt nil )nil booleans nil )nil booleans nil )"bool" more_list_props nil )"list[T]" list_props nil ))quality 100%
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
