| products/sources/formale sprachen/PVS/co_structures/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: csequence_zip_unzip.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(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 = unz "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.7 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
