|
(more_list_props
(length_parm 0
(length_parm-1 nil 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)
((list type-decl nil list_adt nil)
(every adt-def-decl "boolean" list_adt 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)
(PRED type-eq-decl nil defined_types 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)
(list_induction formula-decl nil list_adt nil)
(NOT const-decl "[bool -> bool]" booleans nil))
shostak))
(nth_parm_TCC1 0
(nth_parm_TCC1-1 nil 3500358260
("" (skosimp* :preds? t)
(("" (use "length_parm") (("" (assert) nil nil)) nil)) nil)
((length_parm formula-decl nil more_list_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(every adt-def-decl "boolean" 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)
(< 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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(length def-decl "nat" list_props nil)
(below type-eq-decl nil nat_types nil))
nil))
(nth_parm 0
(nth_parm-1 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)
((below type-eq-decl nil nat_types 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)
(PP skolem-const-decl "PRED[T]" more_list_props nil)
(every adt-def-decl "boolean" list_adt nil)
(list type-decl nil list_adt nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nth def-decl "T" list_props nil)
(PRED type-eq-decl nil defined_types 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)
(list_induction formula-decl nil list_adt 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)
(n!1 skolem-const-decl
"below[length(cons(cons1_var!1, cons2_var!1))]" more_list_props
nil)
(cons2_var!1 skolem-const-decl "list[(PP)]" more_list_props nil)
(cons1_var!1 skolem-const-decl "(PP)" more_list_props 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
(cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(length_parm formula-decl nil more_list_props nil))
shostak))
(every_parm 0
(every_parm-1 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)
((i!1 skolem-const-decl "below(length(pl!1))" more_list_props nil)
(every_nth formula-decl nil list_props nil)
(restrict const-decl "R" restrict nil)
(length_parm formula-decl nil more_list_props nil)
(below type-eq-decl nil nat_types nil)
(nth_parm formula-decl nil more_list_props nil)
(i!1 skolem-const-decl "below(length[T](pl!1))" more_list_props
nil)
(pl!1 skolem-const-decl "list[(P!1)]" more_list_props nil)
(P!1 skolem-const-decl "PRED[T]" more_list_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(length def-decl "nat" list_props nil)
(below type-eq-decl nil naturalnumbers 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)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(every adt-def-decl "boolean" list_adt nil))
shostak))
(append_parm 0
(append_parm-1 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)
((list type-decl nil list_adt nil)
(every adt-def-decl "boolean" list_adt nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(append def-decl "list[T]" list_props nil)
(PRED type-eq-decl nil defined_types 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)
(list_induction formula-decl nil list_adt nil))
shostak))
(append_append_cons 0
(append_append_cons-1 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)
((list_cons_extensionality formula-decl nil list_adt nil)
(list_induction formula-decl nil list_adt nil)
(T formal-type-decl nil more_list_props nil)
(null adt-constructor-decl "(null?)" list_adt nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
(cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(append def-decl "list[T]" list_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(list type-decl nil list_adt nil))
shostak))
(append_equal_null 0
(append_equal_null-1 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"
(case-replace
"append(cons2_var_1, cons(cons1_var, cons2_var)) =
append(append(cons2_var_1, cons(cons1_var, null)), cons2_var)" :hide?
t)
(("1" (hide -3)
(("1"
(inst -3
"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)
((cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil)
(car adt-accessor-decl "[(cons?) -> T]" list_adt nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(append_append_cons formula-decl nil more_list_props nil)
(cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
(cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(list_induction formula-decl nil list_adt nil)
(T formal-type-decl nil more_list_props nil)
(null adt-constructor-decl "(null?)" list_adt nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(append def-decl "list[T]" list_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(list type-decl nil list_adt nil))
shostak))
(nth_append_below_TCC1 0
(nth_append_below_TCC1-1 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)
((length_append formula-decl nil list_props 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)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(list_induction formula-decl nil list_adt nil)
(T formal-type-decl nil more_list_props nil)
(append def-decl "list[T]" list_props nil)
(length def-decl "nat" list_props nil)
(< const-decl "bool" reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans 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)
(boolean nonempty-type-decl nil booleans nil)
(list type-decl nil list_adt nil))
nil))
(nth_append_below 0
(nth_append_below-1 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)
((length_append formula-decl nil list_props nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(i!1 skolem-const-decl "nat" more_list_props 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)
(NOT const-decl "[bool -> bool]" booleans 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)
(= const-decl "[T, T -> boolean]" equalities 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)
(length def-decl "nat" list_props nil)
(append def-decl "list[T]" list_props nil))
shostak))
(nth_append_above_TCC1 0
(nth_append_above_TCC1-1 nil 3520951758
("" (skosimp)
(("" (rewrite "length_append") (("" (assert) nil nil)) nil)) 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)
(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)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(nth_append_above 0
(nth_append_above-1 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)
((nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(length_append formula-decl nil list_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)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(= const-decl "[T, T -> boolean]" equalities 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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(length def-decl "nat" list_props nil)
(< const-decl "bool" reals nil)
(append def-decl "list[T]" list_props 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))
shostak))
(tail?_TCC1 0
(tail?_TCC1-1 nil 3520133815 ("" (subtype-tcc) nil nil) nil nil))
(tail?_TCC2 0
(tail?_TCC2-1 nil 3520133815 ("" (termination-tcc) nil nil)
((<< adt-def-decl "(strict_well_founded?[list])" list_adt nil))
nil))
(tail_append 0
(tail_append-1 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)
((list_induction formula-decl nil list_adt nil)
(T formal-type-decl nil more_list_props nil)
(append def-decl "list[T]" list_props nil)
(tail? def-decl "bool" more_list_props nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(list type-decl nil list_adt nil))
shostak))
(ldiff_TCC1 0
(ldiff_TCC1-1 nil 3520133815
("" (skeep :preds? t)
(("" (expand "tail?") (("" (assert) nil nil)) nil)) nil)
((tail? def-decl "bool" more_list_props nil)) nil))
(ldiff_TCC2 0
(ldiff_TCC2-1 nil 3520133815
("" (skeep :preds? t)
(("" (expand "tail?" -) (("" (assert) nil nil)) nil)) nil)
((tail? def-decl "bool" more_list_props nil)) nil))
(ldiff_TCC3 0
(ldiff_TCC3-1 nil 3520133815
("" (skeep :preds? t)
(("" (assert)
(("" (expand "<<")
(("" (lift-if)
(("" (expand "tail?") (("" (prop) nil nil)) nil)) nil))
nil))
nil))
nil)
((tail? def-decl "bool" more_list_props nil)
(<< adt-def-decl "(strict_well_founded?[list])" list_adt nil))
nil))
(ldiff_append_TCC1 0
(ldiff_append_TCC1-1 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)
((list_induction formula-decl nil list_adt nil)
(T formal-type-decl nil more_list_props nil)
(append def-decl "list[T]" list_props nil)
(tail? def-decl "bool" more_list_props nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(list type-decl nil list_adt nil))
nil))
(ldiff_append 0
(ldiff_append-1 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)
((tail_append formula-decl nil more_list_props nil)
(list_cons_extensionality formula-decl nil list_adt nil)
(append_equal_null formula-decl nil more_list_props 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)
(ldiff def-decl "list[T]" more_list_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(list type-decl nil list_adt nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(tail? def-decl "bool" more_list_props nil)
(append def-decl "list[T]" list_props nil))
shostak)))
¤ Dauer der Verarbeitung: 0.16 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.
|
