Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: symbols_as_interval.pvs Sprache: Lisp

Original von: PVS^©

(csequence_merge_split
(merge_split_eta 0
  (merge_split_eta-1 nil 3513713060
   ("" (skolem!)
    (("" (lemma "coinduction")
      ((""
        (inst - "LAMBDA cseq1, cseq2: cseq1 = merge(split(cseq2))"
         "merge(split(cseq!1))" "cseq!1")
        (("" (delete 2)
          (("" (expand "bisimulation?")
            (("" (skosimp)
              (("" (replace -1)
                (("" (hide -1)
                  (("" (smash)
                    (("1" (lemma "merge_empty")
                      (("1" (inst - "split(y!1)`1" "split(y!1)`2")
                        (("1" (ground)
                          (("1" (rewrite "split_empty_left") nil nil))
                          nil))
                        nil))
                      nil)
                     ("2" (use "split_empty_right")
                      (("2" (use "split_empty_left")
                        (("2" (assert)
                          (("2" (lemma "merge_nonempty")
                            (("2"
                              (inst - "split(y!1)`1" "split(y!1)`2")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("3" (lemma "merge_rest")
                      (("3" (inst - "split(y!1)`1" "split(y!1)`2")
                        (("3" (assert)
                          (("3" (lift-if)
                            (("3" (ground)
                              (("1"
                                (use "split_rest_swap_left")
                                (("1"
                                  (use "split_rest_swap_right")
                                  (("1" (assert) nil nil))
                                  nil))
                                nil)
                               ("2"
                                (use "split_empty_left")
                                (("2"
                                  (assert)
                                  (("2"
                                    (use "split_empty_right")
                                    (("2"
                                      (assert)
                                      (("2"
                                        (use "merge_nonempty")
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("4" (lemma "merge_first")
                      (("4" (inst - "split(y!1)`1" "split(y!1)`2")
                        (("4" (assert)
                          (("4" (lift-if)
                            (("4" (ground)
                              (("1"
                                (rewrite "split_first_left")
                                (("1" (assert) nil nil))
                                nil)
                               ("2"
                                (use "split_empty_left")
                                (("2"
                                  (assert)
                                  (("2"
                                    (use "split_empty_right")
                                    (("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil csequence_merge_split nil)
    (coinduction formula-decl nil csequence_codt nil)
    (merge_first formula-decl nil csequence_merge nil)
    (split_first_left formula-decl nil csequence_split nil)
    (merge_rest formula-decl nil csequence_merge nil)
    (split_rest_swap_right formula-decl nil csequence_split nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (split_rest_swap_left formula-decl nil csequence_split nil)
    (split_empty_right formula-decl nil csequence_split nil)
    (merge_nonempty formula-decl nil csequence_merge nil)
    (merge_empty formula-decl nil csequence_merge nil)
    (split_empty_left formula-decl nil csequence_split nil)
    (split const-decl "[csequence, csequence]" csequence_split nil)
    (merge const-decl "csequence" csequence_merge 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))
(split_merge_eta 0
  (split_merge_eta-1 nil 3513713264
   ("" (skosimp)
    (("" (decompose-equality)
      (("1" (lemma "coinduction")
        (("1"
          (inst -
           "LAMBDA cseq, cseq1: EXISTS cseq2: length_eq(cseq1, cseq2) AND cseq = split(merge(cseq1, cseq2))`1"
           "split(merge(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 -2)
                  (("2" (hide -2)
                    (("2" (smash)
                      (("1" (rewrite "split_empty_left")
                        (("1" (rewrite "merge_empty") nil nil)) nil)
                       ("2" (rewrite "split_nonempty_left")
                        (("2" (rewrite "merge_nonempty")
                          (("2" (rewrite "length_nonempty?_rew")
                            (("2" (rewrite "length_empty?_rew")
                              (("2"
                                (expand "length_eq")
                                (("2" (ground) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("3" (inst + "rest(cseq2!2)")
                        (("1" (expand "length_eq")
                          (("1" (expand "is_finite" -)
                            (("1" (expand "length" -)
                              (("1"
                                (smash)
                                (("1"
                                  (rewrite "split_nonempty_left")
                                  (("1"
                                    (rewrite "merge_nonempty")
                                    nil
                                    nil))
                                  nil)
                                 ("2"
                                  (rewrite "split_nonempty_left")
                                  (("2"
                                    (rewrite "merge_nonempty")
                                    nil
                                    nil))
                                  nil)
                                 ("3"
                                  (case
                                   "nonempty?(merge(y!1, cseq2!2))")
                                  (("1"
                                    (rewrite "split_rest_left")
                                    (("1"
                                      (lift-if)
                                      (("1"
                                        (ground)
                                        (("1"
                                          (expand*
                                           "merge"
                                           "merge_struct"
                                           "coreduce"
                                           "coreduce")
                                          nil
                                          nil)
                                         ("2"
                                          (lemma "merge_rest")
                                          (("2"
                                            (inst-cp - "y!1" "cseq2!2")
                                            (("2"
                                              (assert)
                                              (("2"
                                                (inst
                                                 -
                                                 "cseq2!2"
                                                 "rest(y!1)")
                                                (("2"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (rewrite "split_nonempty_left")
                                    nil
                                    nil))
                                  nil)
                                 ("4"
                                  (use "split_nonempty_left")
                                  (("4"
                                    (assert)
                                    (("4"
                                      (rewrite "split_rest_left")
                                      (("4"
                                        (lift-if)
                                        (("4"
                                          (ground)
                                          (("1"
                                            (expand*
                                             "merge"
                                             "merge_struct"
                                             "coreduce"
                                             "coreduce")
                                            nil
                                            nil)
                                           ("2"
                                            (lemma "merge_rest")
                                            (("2"
                                              (inst-cp
                                               -
                                               "y!1"
                                               "cseq2!2")
                                              (("2"
                                                (assert)
                                                (("2"
                                                  (inst
                                                   -
                                                   "cseq2!2"
                                                   "rest(y!1)")
                                                  (("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (rewrite "split_nonempty_left")
                          (("2" (rewrite "merge_nonempty")
                            (("2" (assert)
                              (("2"
                                (rewrite "length_nonempty?_rew")
                                (("2"
                                  (rewrite "length_nonempty?_rew")
                                  (("2"
                                    (expand "length_eq")
                                    (("2" (ground) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("4" (rewrite "split_nonempty_left")
                        (("4" (rewrite "split_first_left")
                          (("4" (rewrite "merge_first")
                            (("4" (lift-if)
                              (("4"
                                (ground)
                                (("4"
                                  (expand "length_eq")
                                  (("4"
                                    (ground)
                                    (("1"
                                      (use
                                       "infinite_csequence_is_nonempty")
                                      nil
                                      nil)
                                     ("2"
                                      (expand "length")
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (lemma "coinduction")
        (("2"
          (inst -
           "LAMBDA cseq, cseq2: EXISTS cseq1: length_eq(cseq1, cseq2) AND cseq = split(merge(cseq1, cseq2))`2"
           "split(merge(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 -2)
                  (("2" (hide -2)
                    (("2" (smash)
                      (("1" (rewrite "split_empty_right")
                        (("1" (rewrite "merge_empty")
                          (("1"
                            (expand* "merge" "merge_struct" "coreduce"
                             "coreduce")
                            (("1" (reduce)
                              (("1"
                                (rewrite "length_empty?_rew")
                                (("1"
                                  (rewrite "length_empty?_rew")
                                  (("1"
                                    (rewrite "length_nonempty?_rew")
                                    (("1"
                                      (expand "length_eq")
                                      (("1" (ground) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (rewrite "split_nonempty_right")
                        (("2" (flatten)
                          (("2" (rewrite "merge_nonempty")
                            (("2" (hide -3)
                              (("2"
                                (rewrite "length_nonempty?_rew")
                                (("2"
                                  (rewrite "length_empty?_rew")
                                  (("2"
                                    (expand "length_eq")
                                    (("2" (ground) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("3" (rewrite "split_nonempty_right")
                        (("3" (flatten)
                          (("3" (inst + "rest(cseq1!2)")
                            (("1" (split)
                              (("1"
                                (expand "length_eq")
                                (("1"
                                  (expand "is_finite" -)
                                  (("1"
                                    (expand "length" -)
                                    (("1" (reduce) nil nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (rewrite "split_rest_right")
                                (("2"
                                  (lemma "merge_rest")
                                  (("2"
                                    (inst-cp - "cseq1!2" "y!1")
                                    (("2"
                                      (assert)
                                      (("2"
                                        (lift-if)
                                        (("2"
                                          (ground)
                                          (("1"
                                            (replace -2)
                                            (("1"
                                              (inst
                                               -
                                               "y!1"
                                               "rest(cseq1!2)")
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (lift-if)
                                                  (("1"
                                                    (ground)
                                                    (("1"
                                                      (hide
                                                       -1
                                                       -3
                                                       -5
                                                       -6
                                                       2)
                                                      (("1"
                                                        (rewrite
                                                         "length_nonempty?_rew")
                                                        (("1"
                                                          (rewrite
                                                           "length_nonempty?_rew")
                                                          (("1"
                                                            (expand
                                                             "length_eq")
                                                            (("1"
                                                              (ground)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (rewrite
                                             "merge_empty_left"
                                             -5)
                                            (("2"
                                              (hide -1 -4 2)
                                              (("2"
                                                (rewrite
                                                 "length_nonempty?_rew")
                                                (("2"
                                                  (rewrite
                                                   "length_nonempty?_rew")
                                                  (("2"
                                                    (expand
                                                     "length_eq")
                                                    (("2"
                                                      (ground)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (rewrite "merge_nonempty")
                              (("2"
                                (assert)
                                (("2"
                                  (hide -3)
                                  (("2"
                                    (rewrite "length_nonempty?_rew")
                                    (("2"
                                      (rewrite "length_nonempty?_rew")
                                      (("2"
                                        (expand "length_eq")
                                        (("2" (ground) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("4" (rewrite "split_nonempty_right")
                        (("4" (flatten)
                          (("4" (rewrite "split_first_right")
                            (("4" (assert)
                              (("4"
                                (rewrite "merge_rest")
                                (("4"
                                  (rewrite "merge_nonempty")
                                  (("4"
                                    (lift-if)
                                    (("4"
                                      (ground)
                                      (("1"
                                        (rewrite "merge_first")
                                        (("1"
                                          (lift-if)
                                          (("1"
                                            (ground)
                                            (("1"
                                              (hide -2 -3 -4 2)
                                              (("1"
                                                (rewrite
                                                 "length_nonempty?_rew")
                                                (("1"
                                                  (rewrite
                                                   "length_nonempty?_rew")
                                                  (("1"
                                                    (expand
                                                     "length_eq")
                                                    (("1"
                                                      (ground)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (rewrite "merge_first")
                                        nil
                                        nil)
                                       ("3"
                                        (hide -1 2 3)
                                        (("3"
                                          (rewrite
                                           "length_nonempty?_rew")
                                          (("3"
                                            (rewrite
                                             "length_nonempty?_rew")
                                            (("3"
                                              (expand "length_eq")
                                              (("3" (ground) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((split const-decl "[csequence, csequence]" csequence_split nil)
    (merge const-decl "csequence" csequence_merge nil)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_merge_split nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (length_eq const-decl "bool" csequence_length_comp 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)
    (merge_empty formula-decl nil csequence_merge nil)
    (split_empty_left formula-decl nil csequence_split nil)
    (merge_nonempty formula-decl nil csequence_merge nil)
    (length_empty?_rew formula-decl nil csequence_length nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (length_nonempty?_rew formula-decl nil csequence_length nil)
    (split_nonempty_left formula-decl nil csequence_split nil)
    (length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
    (merge_rest formula-decl nil csequence_merge nil)
    (merge_struct const-decl "csequence_struct" csequence_merge 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)
    (split_rest_left formula-decl nil csequence_split nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (cseq2!2 skolem-const-decl "csequence[T]" csequence_merge_split
     nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (split_first_left formula-decl nil csequence_split nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (infinite_csequence type-eq-decl nil csequence_props nil)
    (infinite_csequence_is_nonempty judgement-tcc nil csequence_props
     nil)
    (merge_first formula-decl nil csequence_merge nil)
    (coinduction formula-decl nil csequence_codt nil)
    (split_empty_right formula-decl nil csequence_split nil)
    (split_nonempty_right formula-decl nil csequence_split nil)
    (merge_empty_left formula-decl nil csequence_merge nil)
    (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
     nil)
    (empty_csequence nonempty-type-eq-decl nil csequence_props nil)
    (split_rest_right formula-decl nil csequence_split nil)
    (cseq1!2 skolem-const-decl "csequence[T]" csequence_merge_split
     nil)
    (split_first_right formula-decl nil csequence_split nil))
   shostak)))

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.