|
(csequence_zip_unzip
(zip_unzip_eta 0
(zip_unzip_eta-1 nil 3513781677
("" (skolem!)
(("" (lemma "coinduction[[T1, T2]]")
((""
(inst -
"LAMBDA (cseq1, cseq2: csequence[[T1, T2]]): cseq1 = zip(unzip(cseq2))"
"zip(unzip(cseq!1))" "cseq!1")
(("" (delete 2)
(("" (expand "bisimulation?")
(("" (skosimp)
(("" (replace -1)
(("" (hide -1)
(("" (smash)
(("1" (use "unzip_nonempty")
(("1" (flatten)
(("1" (use "zip_nonempty")
(("1" (assert) nil nil)) nil))
nil))
nil)
("2"
(expand* "unzip" "unzip_left_struct"
"unzip_right_struct" "coreduce" "zip"
"zip_struct" "coreduce")
nil nil)
("3" (use "unzip_nonempty")
(("3" (flatten)
(("3" (lemma "zip_rest")
(("3" (inst - "unzip(y!1)`1" "unzip(y!1)`2")
(("3" (lemma "unzip_rest_left")
(("3"
(inst - "y!1")
(("3"
(lemma "unzip_rest_right")
(("3"
(inst - "y!1")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4"
(expand* "unzip" "unzip_left_struct"
"unzip_right_struct" "coreduce" "zip"
"zip_struct" "coreduce")
(("4" (smash) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T2 formal-type-decl nil csequence_zip_unzip nil)
(T1 formal-type-decl nil csequence_zip_unzip nil)
(coinduction formula-decl nil csequence_codt nil)
(zip_rest formula-decl nil csequence_zip nil)
(unzip_rest_left formula-decl nil csequence_unzip nil)
(unzip_rest_right formula-decl nil csequence_unzip nil)
(unzip_left_struct const-decl
"csequence_struct[T1, csequence[[T1, T2]]]" csequence_unzip nil)
(unzip_right_struct const-decl
"csequence_struct[T2, csequence[[T1, T2]]]" csequence_unzip nil)
(coreduce adt-def-decl "{c: csequence[T] |
inj_empty?(op(x)) AND empty?(c) OR
inj_nonempty?(op(x)) AND nonempty?(c)}"
csequence_codt_coreduce nil)
(zip_struct const-decl
"csequence_struct[[T1, T2], [csequence[T1], csequence[T2]]]"
csequence_zip nil)
(unzip_nonempty judgement-tcc nil csequence_unzip nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(nonempty_csequence type-eq-decl nil csequence_props nil)
(zip_nonempty judgement-tcc nil csequence_zip nil)
(y!1 skolem-const-decl "csequence[[T1, T2]]" csequence_zip_unzip
nil)
(unzip const-decl "[csequence[T1], csequence[T2]]" csequence_unzip
nil)
(zip const-decl "csequence[[T1, T2]]" csequence_zip nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(bisimulation? adt-def-decl "boolean" csequence_codt nil)
(PRED type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(csequence type-decl nil csequence_codt nil))
shostak))
(unzip_zip_eta 0
(unzip_zip_eta-1 nil 3513784473
("" (skosimp)
(("" (decompose-equality)
(("1" (lemma "coinduction[T1]")
(("1"
(inst -
"LAMBDA (cseq1, cseq2: csequence[T1]): EXISTS (cseq: csequence[T2]):
cseq1 = unzip(zip(cseq2, cseq))`1 AND length_eq(cseq2, cseq)"
"unzip(zip(cseq1!1, cseq2!1))`1" "cseq1!1")
(("1" (assert) (("1" (inst + "cseq2!1") nil nil)) nil)
("2" (delete -1 2)
(("2" (expand "bisimulation?")
(("2" (skosimp*)
(("2" (replace -1)
(("2" (hide -1)
(("2" (smash)
(("1" (rewrite "unzip_empty_left")
(("1" (rewrite "zip_empty")
(("1" (use "length_eq_empty")
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (use "unzip_empty_left")
(("2" (assert)
(("2" (rewrite "zip_empty") nil nil)) nil))
nil)
("3" (use "unzip_empty_left")
(("3" (assert)
(("3" (rewrite "zip_empty")
(("3" (ground)
(("3"
(inst + "rest(cseq!1)")
(("3"
(use "length_eq_rest")
(("3"
(assert)
(("3"
(rewrite "unzip_rest_left")
(("3"
(rewrite "zip_rest")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (use "unzip_empty_left")
(("4" (assert)
(("4" (rewrite "zip_empty")
(("4" (ground)
(("4"
(rewrite "unzip_first_left")
(("4"
(rewrite "zip_first")
(("4" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "coinduction[T2]")
(("2"
(inst -
"LAMBDA (cseq1, cseq2: csequence[T2]): EXISTS (cseq: csequence[T1]): cseq1 = unzip(zip(cseq, cseq2))`2 AND length_eq(cseq, cseq2)"
"unzip(zip(cseq1!1, cseq2!1))`2" "cseq2!1")
(("1" (assert) (("1" (inst + "cseq1!1") nil nil)) nil)
("2" (delete -1 2)
(("2" (expand "bisimulation?")
(("2" (skosimp*)
(("2" (replace -1)
(("2" (hide -1)
(("2" (smash)
(("1" (rewrite "unzip_empty_right")
(("1" (rewrite "zip_empty")
(("1" (use "length_eq_empty")
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (use "unzip_empty_right")
(("2" (assert)
(("2" (rewrite "zip_empty") nil nil)) nil))
nil)
("3" (use "unzip_empty_right")
(("3" (assert)
(("3" (rewrite "zip_empty")
(("3" (ground)
(("3"
(inst + "rest(cseq!1)")
(("3"
(use "length_eq_rest")
(("3"
(assert)
(("3"
(rewrite "unzip_rest_right")
(("3"
(rewrite "zip_rest")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (use "unzip_empty_right")
(("4" (assert)
(("4" (rewrite "zip_empty")
(("4" (ground)
(("4"
(rewrite "unzip_first_right")
(("4"
(rewrite "zip_first")
(("4" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((unzip const-decl "[csequence[T1], csequence[T2]]" csequence_unzip
nil)
(zip const-decl "csequence[[T1, T2]]" csequence_zip nil)
(T2 formal-type-decl nil csequence_zip_unzip nil)
(csequence type-decl nil csequence_codt nil)
(T1 formal-type-decl nil csequence_zip_unzip nil)
(length_eq const-decl "bool" csequence_length_comp nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bisimulation? adt-def-decl "boolean" csequence_codt nil)
(PRED type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(zip_empty formula-decl nil csequence_zip nil)
(length_eq_empty formula-decl nil csequence_length_comp nil)
(unzip_empty_left formula-decl nil csequence_unzip nil)
(length_eq_rest formula-decl nil csequence_length_comp nil)
(nonempty_csequence type-eq-decl nil csequence_props nil)
(unzip_rest_left formula-decl nil csequence_unzip nil)
(zip_rest formula-decl nil csequence_zip nil)
(nonempty? adt-recognizer-decl "[csequence -> boolean]"
csequence_codt nil)
(rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
nil)
(zip_first formula-decl nil csequence_zip nil)
(unzip_first_left formula-decl nil csequence_unzip nil)
(coinduction formula-decl nil csequence_codt nil)
(unzip_empty_right formula-decl nil csequence_unzip nil)
(unzip_rest_right formula-decl nil csequence_unzip nil)
(unzip_first_right formula-decl nil csequence_unzip nil))
shostak)))
¤ Dauer der Verarbeitung: 0.23 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.
|
