|
(list_props_aux
(length_is_0 0
(length_is_0-1 nil 3399030887
("" (skosimp)
(("" (split)
(("1" (flatten)
(("1" (expand "length") (("1" (assert) nil nil)) nil)) nil)
("2" (flatten)
(("2" (expand "length") (("2" (assert) nil nil)) nil)) nil))
nil))
nil)
((length def-decl "nat" list_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil))
shostak))
(append_is_null 0
(append_is_null-1 nil 3398752737
("" (skosimp)
(("" (split)
(("1" (flatten)
(("1" (case-replace "l1!1=null")
(("1" (expand "append") (("1" (assert) nil nil)) nil)
("2" (assert)
(("2" (expand "append") (("2" (propax) nil nil)) nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (expand "append") (("2" (assert) nil nil)) nil)) nil))
nil))
nil)
((T formal-type-decl nil list_props_aux nil)
(list type-decl nil list_adt nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(null adt-constructor-decl "(null?)" list_adt nil)
(append def-decl "list[T]" list_props nil))
shostak))
(append_eq1 0
(append_eq1-1 nil 3398752918
("" (induct "l1")
(("1" (expand "append") (("1" (propax) nil nil)) nil)
("2" (skolem + ("x!1" "l!1"))
(("2" (skosimp*)
(("2" (inst - "l2!1" "l3!1")
(("2" (expand "append" 1)
(("2" (replace -1 * rl)
(("2" (hide -1)
(("2" (name-replace "L2" "append(l!1, l2!1)")
(("2" (name-replace "L3" "append(l!1, l3!1)")
(("2" (split)
(("1" (flatten)
(("1" (decompose-equality) nil nil)) nil)
("2" (flatten) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((AND const-decl "[bool, bool -> bool]" booleans nil)
(cons? 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)
(list_induction formula-decl nil list_adt nil)
(T formal-type-decl nil list_props_aux nil)
(append def-decl "list[T]" list_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IFF 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))
(append_eq2 0
(append_eq2-1 nil 3398753160
(""
(case "FORALL (n:nat,l1, l2, l3: list[T]): length(l2)=n & append(l2, l1) = append(l3, l1) => l2=l3")
(("1" (skosimp)
(("1" (split)
(("1" (flatten)
(("1" (inst - "length(l2!1)" "l1!1" "l2!1" "l3!1")
(("1" (assert) nil nil)) nil))
nil)
("2" (flatten) (("2" (assert) nil nil)) nil))
nil))
nil)
("2" (hide 2)
(("2" (induct "n")
(("1" (skosimp)
(("1" (rewrite "length_is_0")
(("1" (replace -1)
(("1" (expand "append" -2 1)
(("1" (lemma "length_append" ("l1" "l3!1" "l2" "l1!1"))
(("1" (replace -3 -1 rl)
(("1" (lemma "length_is_0" ("l" "l3!1"))
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "length" -2)
(("2" (case-replace "l2!1=null")
(("1" (assert) nil nil)
("2" (case-replace "l3!1=null")
(("1" (assert)
(("1" (expand "append" -4 2)
(("1"
(lemma "length_append" ("l1" "l2!1" "l2" "l1!1"))
(("1" (replace -5)
(("1" (lemma "length_is_0" ("l" "l2!1"))
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (case "cons?(l2!1)")
(("1" (case "cons?(l3!1)")
(("1" (hide 1 2)
(("1" (inst - "l1!1" "cdr(l2!1)" "cdr(l3!1)")
(("1" (replace -4)
(("1" (hide -4)
(("1"
(expand "append" -4)
(("1"
(name-replace
"TAIL2"
"append(cdr(l2!1), l1!1)")
(("1"
(name-replace
"TAIL3"
"append(cdr(l3!1), l1!1)")
(("1"
(copy -4)
(("1"
(hide -5)
(("1"
(decompose-equality)
(("1"
(assert)
(("1"
(hide -2)
(("1"
(case
"forall l: cons?(l) => l=cons(car(l),cdr(l))")
(("1"
(inst-cp - "l2!1")
(("1"
(inst - "l3!1")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(skosimp)
(("2"
(decompose-equality)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((null adt-constructor-decl "(null?)" list_adt nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil)
(cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
(car adt-accessor-decl "[(cons?) -> T]" list_adt nil)
(list_cons_extensionality formula-decl nil list_adt nil)
(cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(length_append formula-decl nil list_props nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(length_is_0 formula-decl nil list_props_aux nil)
(nat_induction formula-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types 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)
(T formal-type-decl nil list_props_aux nil)
(list type-decl nil list_adt nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(length def-decl "nat" list_props nil)
(append def-decl "list[T]" list_props nil))
shostak)))
¤ Dauer der Verarbeitung: 0.35 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.
|
