products/sources/formale sprachen/PVS/while/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: OSSearchServlet.java   Sprache: Lisp

Original von: PVS©
(natural
 (depth_TCC1 0
  (depth_TCC1-1 nil 3400243711 ("" (termination-tcc) nil nil)
   ((<< adt-def-decl "(strict_well_founded?[tree])" natural nil)) nil))
 (depth_TCC2 0
  (depth_TCC2-1 nil 3400243711 ("" (termination-tcc) nil nil)
   ((<< adt-def-decl "(strict_well_founded?[tree])" natural nil)) nil))
 (depth_TCC3 0
  (depth_TCC3-1 nil 3400243711 ("" (termination-tcc) nil nil)
   ((<< adt-def-decl "(strict_well_founded?[tree])" natural nil)) nil))
 (derivation_tree?_TCC1 0
  (derivation_tree?_TCC1-1 nil 3400238483 ("" (subtype-tcc) nil nil)
   ((S const-decl "Stm" natural nil)
    (s1 const-decl "State" natural nil)
    (s0 const-decl "State" natural nil)
    (V formal-nonempty-type-decl nil natural nil)
    (assign const-decl "State" State nil))
   nil))
 (derivation_tree?_TCC2 0
  (derivation_tree?_TCC2-1 nil 3400238483
   ("" (termination-tcc) nil nil) ((S const-decl "Stm" natural nil))
   nil))
 (derivation_tree?_TCC3 0
  (derivation_tree?_TCC3-1 nil 3400238483
   ("" (termination-tcc) nil nil)
   ((S const-decl "Stm" natural nil) (S const-decl "Stm" natural nil))
   nil))
 (derivation_tree?_TCC4 0
  (derivation_tree?_TCC4-1 nil 3400238483 ("" (subtype-tcc) nil nil)
   ((S const-decl "Stm" natural nil) (S const-decl "Stm" natural nil)
    (s0 const-decl "State" natural nil)
    (s0 const-decl "State" natural nil)
    (s1 const-decl "State" natural nil)
    (s1 const-decl "State" natural nil))
   nil))
 (derivation_tree?_TCC5 0
  (derivation_tree?_TCC5-1 nil 3400238483 ("" (subtype-tcc) nil nil)
   ((s1 const-decl "State" natural nil)
    (s1 const-decl "State" natural nil)
    (s0 const-decl "State" natural nil)
    (s0 const-decl "State" natural nil)
    (S const-decl "Stm" natural nil))
   nil))
 (derivation_tree?_TCC6 0
  (derivation_tree?_TCC6-1 nil 3400238483 ("" (subtype-tcc) nil nil)
   ((S const-decl "Stm" natural nil)
    (s0 const-decl "State" natural nil)
    (S const-decl "Stm" natural nil)
    (s1 const-decl "State" natural nil)
    (s1 const-decl "State" natural nil)
    (s0 const-decl "State" natural nil))
   nil))
 (derivation_tree_TCC1 0
  (derivation_tree_TCC1-1 nil 3400238483
   ("" (expand "derivation_tree?")
    (("" (expand "S")
      (("" (expand "s1")
        (("" (expand "s0") (("" (propax) nil nil)) nil)) nil))
      nil))
    nil)
   ((S const-decl "Stm" natural nil)
    (s0 const-decl "State" natural nil)
    (s1 const-decl "State" natural nil)
    (derivation_tree? def-decl "bool" natural nil))
   nil))
 (dt_eq 0
  (dt_eq-1 nil 3400238504
   (""
    (case "FORALL (d1, d2: derivation_tree,n:nat): depth(d1)<=n&depth(d2)<=n&
        S(d1) = S(d2) AND s0(d1) = s0(d2) => d1 = d2")
    (("1" (skosimp)
      (("1" (inst - "d1!1" "d2!1" "max(depth(d1!1),depth(d2!1))")
        (("1" (expand "max")
          (("1" (case-replace "depth(d1!1) < depth(d2!1)")
            (("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil)
     ("2" (hide 2)
      (("2" (induct "n")
        (("1" (skosimp)
          (("1" (case "leaf?(d1!1)")
            (("1" (case "leaf?(d2!1)")
              (("1" (hide -3 -4)
                (("1" (typepred "d1!1")
                  (("1" (typepred "d2!1")
                    (("1" (expand "derivation_tree?")
                      (("1" (assert)
                        (("1" (expand "S")
                          (("1" (expand "S")
                            (("1" (expand "s0")
                              (("1"
                                (expand "s0")
                                (("1"
                                  (expand "s1")
                                  (("1"
                                    (case
                                     "d1!1=leaf((d(d1!1)`1,d(d1!1)`2,d(d1!1)`3))")
                                    (("1"
                                      (replace -1 1)
                                      (("1"
                                        (case
                                         "d2!1=leaf((d(d2!1)`1,d(d2!1)`2,d(d2!1)`3))")
                                        (("1"
                                          (replace -1 1)
                                          (("1"
                                            (hide -1 -2)
                                            (("1"
                                              (case-replace
                                               "Assign?(d(d2!1)`1)")
                                              (("1" (assert) nil nil)
                                               ("2"
                                                (assert)
                                                (("2"
                                                  (case-replace
                                                   "Skip?(d(d2!1)`1)")
                                                  (("1"
                                                    (assert)
                                                    nil
                                                    nil)
                                                   ("2"
                                                    (assert)
                                                    (("2"
                                                      (flatten)
                                                      (("2"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (hide-all-but (-4 1))
                                          (("2"
                                            (decompose-equality)
                                            (("2"
                                              (decompose-equality)
                                              nil
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (hide-all-but (-4 1))
                                      (("2"
                                        (decompose-equality)
                                        (("2"
                                          (decompose-equality)
                                          nil
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (hide -2 -3 2)
                (("2" (typepred "d1!1")
                  (("2" (typepred "d2!1")
                    (("2" (expand "derivation_tree?")
                      (("2" (assert)
                        (("2" (split -2)
                          (("1" (flatten)
                            (("1" (assert)
                              (("1"
                                (expand "S")
                                (("1"
                                  (expand "S")
                                  (("1"
                                    (expand "s0")
                                    (("1"
                                      (expand "s0")
                                      (("1"
                                        (assert)
                                        (("1"
                                          (lift-if)
                                          (("1" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (flatten)
                            (("2" (expand "S")
                              (("2"
                                (expand "S")
                                (("2"
                                  (expand "s0")
                                  (("2"
                                    (expand "s0")
                                    (("2"
                                      (lift-if)
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("3" (flatten)
                            (("3" (expand "S")
                              (("3"
                                (expand "S")
                                (("3"
                                  (expand "s0")
                                  (("3"
                                    (expand "s0")
                                    (("3"
                                      (lift-if)
                                      (("3" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (hide-all-but (-1 1))
              (("2" (expand "depth")
                (("2" (lift-if)
                  (("2" (assert)
                    (("2" (typepred "depth(t1(d1!1))")
                      (("1" (typepred "depth(t2(d1!1))")
                        (("1" (assert)
                          (("1" (expand "max")
                            (("1"
                              (case-replace
                               "depth(t1(d1!1)) < depth(t2(d1!1))")
                              (("1" (assert) nil nil)
                               ("2" (assert) nil nil))
                              nil))
                            nil))
                          nil)
                         ("2" (assert) nil nil))
                        nil)
                       ("2" (flatten) (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (skolem + ("n!1"))
          (("2" (skosimp*)
            (("2" (expand "S")
              (("2" (expand "S")
                (("2" (expand "s0")
                  (("2" (expand "s0")
                    (("2" (case "branch1?(d1!1)")
                      (("1" (case "branch1?(d2!1)")
                        (("1" (typepred "d1!1")
                          (("1" (typepred "d2!1")
                            (("1" (expand "derivation_tree?")
                              (("1"
                                (assert)
                                (("1"
                                  (flatten)
                                  (("1"
                                    (expand "s0")
                                    (("1"
                                      (expand "s0")
                                      (("1"
                                        (expand "s1")
                                        (("1"
                                          (expand "s1")
                                          (("1"
                                            (expand "S")
                                            (("1"
                                              (expand "S")
                                              (("1"
                                                (case-replace
                                                 "B(b(d(d1!1)`1))(d(d1!1)`2)")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (inst
                                                     -
                                                     "t1(d1!1)"
                                                     "t1(d2!1)")
                                                    (("1"
                                                      (expand
                                                       "depth"
                                                       (-15 -16))
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (case
                                                           "d1!1=branch1((d(d1!1)`1,d(d1!1)`2,d(d1!1)`3),t1(d1!1))")
                                                          (("1"
                                                            (replace
                                                             -1
                                                             1)
                                                            (("1"
                                                              (case
                                                               "d2!1=branch1((d(d2!1)`1,d(d2!1)`2,d(d2!1)`3),t1(d2!1))")
                                                              (("1"
                                                                (replace
                                                                 -1
                                                                 1)
                                                                (("1"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (hide-all-but
                                                                 (-13
                                                                  1))
                                                                (("2"
                                                                  (decompose-equality)
                                                                  (("2"
                                                                    (decompose-equality)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (hide-all-but
                                                             (-12 1))
                                                            (("2"
                                                              (decompose-equality)
                                                              (("2"
                                                                (decompose-equality)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (assert)
                                                  (("2"
                                                    (inst
                                                     -
                                                     "t1(d1!1)"
                                                     "t1(d2!1)")
                                                    (("2"
                                                      (expand
                                                       "depth"
                                                       (-14 -15))
                                                      (("2"
                                                        (assert)
                                                        (("2"
                                                          (case
                                                           "d1!1=branch1((d(d1!1)`1,d(d1!1)`2,d(d1!1)`3),t1(d1!1))")
                                                          (("1"
                                                            (replace
                                                             -1
                                                             2)
                                                            (("1"
                                                              (case
                                                               "d2!1=branch1((d(d2!1)`1,d(d2!1)`2,d(d2!1)`3),t1(d2!1))")
                                                              (("1"
                                                                (replace
                                                                 -1
                                                                 2)
                                                                (("1"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (hide-all-but
                                                                 (-13
                                                                  1))
                                                                (("2"
                                                                  (decompose-equality)
                                                                  (("2"
                                                                    (decompose-equality)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (hide-all-but
                                                             (-11 1))
                                                            (("2"
                                                              (decompose-equality)
                                                              (("2"
                                                                (decompose-equality)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("3"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (hide-all-but (-1 -5 -6 1))
                          (("2" (typepred "d1!1")
                            (("2" (typepred "d2!1")
                              (("2"
                                (expand "derivation_tree?")
                                (("2"
                                  (assert)
                                  (("2"
                                    (flatten)
                                    (("2"
                                      (assert)
                                      (("2"
                                        (expand "S")
                                        (("2"
                                          (expand "s1")
                                          (("2"
                                            (expand "s0")
                                            (("2"
                                              (expand "s1")
                                              (("2"
                                                (expand "s0")
                                                (("2"
                                                  (expand "S")
                                                  (("2"
                                                    (assert)
                                                    (("2"
                                                      (lift-if)
                                                      (("2"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (case "leaf?(d1!1)")
                        (("1" (inst - "d1!1" "d2!1")
                          (("1" (assert)
                            (("1" (expand "depth")
                              (("1"
                                (assert)
                                (("1"
                                  (case-replace "leaf?(d2!1)")
                                  (("1" (assert) nil nil)
                                   ("2"
                                    (case-replace "branch1?(d2!1)")
                                    (("1"
                                      (assert)
                                      (("1"
                                        (typepred "d1!1")
                                        (("1"
                                          (typepred "d2!1")
                                          (("1"
                                            (expand "derivation_tree?")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (flatten)
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (expand "s0")
                                                    (("1"
                                                      (expand "s0")
                                                      (("1"
                                                        (expand "s1")
                                                        (("1"
                                                          (expand "s1")
                                                          (("1"
                                                            (expand
                                                             "S")
                                                            (("1"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (assert)
                                      (("2"
                                        (typepred "d1!1")
                                        (("2"
                                          (typepred "d2!1")
                                          (("2"
                                            (expand "derivation_tree?")
                                            (("2"
                                              (assert)
                                              (("2"
                                                (expand "S")
                                                (("2"
                                                  (expand "s1")
                                                  (("2"
                                                    (expand "s1")
                                                    (("2"
                                                      (expand "s0")
                                                      (("2"
                                                        (expand "s0")
                                                        (("2"
                                                          (split -2)
                                                          (("1"
                                                            (flatten)
                                                            (("1"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (flatten)
                                                            (("2"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil)
                                                           ("3"
                                                            (flatten)
                                                            (("3"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (case "branch2?(d1!1)")
                          (("1" (hide 1 2)
                            (("1" (case "branch2?(d2!1)")
                              (("1"
                                (case
                                 "d1!1=branch2((d(d1!1)`1,d(d1!1)`2,d(d1!1)`3),t1(d1!1),t2(d1!1))")
                                (("1"
                                  (replace -1 1)
                                  (("1"
                                    (hide -1)
                                    (("1"
                                      (case
                                       "d2!1=branch2((d(d2!1)`1,d(d2!1)`2,d(d2!1)`3),t1(d2!1),t2(d2!1))")
                                      (("1"
                                        (replace -1 1)
                                        (("1"
                                          (hide -1)
                                          (("1"
                                            (typepred "d1!1")
                                            (("1"
                                              (typepred "d2!1")
                                              (("1"
                                                (expand
                                                 "derivation_tree?")
                                                (("1"
                                                  (lift-if)
                                                  (("1"
                                                    (assert)
                                                    (("1"
                                                      (expand "S")
                                                      (("1"
                                                        (expand "S")
                                                        (("1"
                                                          (expand "s0")
                                                          (("1"
                                                            (expand
                                                             "s0")
                                                            (("1"
                                                              (expand
                                                               "s1")
                                                              (("1"
                                                                (expand
                                                                 "s1")
                                                                (("1"
                                                                  (case-replace
                                                                   " Sequence?(d(d1!1)`1)")
                                                                  (("1"
                                                                    (assert)
                                                                    (("1"
                                                                      (flatten)
                                                                      (("1"
                                                                        (inst-cp
                                                                         -
                                                                         "t1(d1!1)"
                                                                         "t1(d2!1)")
                                                                        (("1"
                                                                          (inst
                                                                           -
                                                                           "t2(d1!1)"
                                                                           "t2(d2!1)")
                                                                          (("1"
                                                                            (expand
                                                                             "depth"
                                                                             (-20
                                                                              -21))
                                                                            (("1"
                                                                              (assert)
                                                                              (("1"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (assert)
                                                                    (("2"
                                                                      (flatten)
                                                                      (("2"
                                                                        (inst-cp
                                                                         -
                                                                         "t1(d1!1)"
                                                                         "t1(d2!1)")
                                                                        (("2"
                                                                          (inst
                                                                           -
                                                                           "t2(d1!1)"
                                                                           "t2(d2!1)")
                                                                          (("2"
                                                                            (expand
                                                                             "depth"
                                                                             (-23
                                                                              -24))
                                                                            (("2"
                                                                              (assert)
                                                                              (("2"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (hide-all-but (-1 1))
                                        (("2"
                                          (decompose-equality)
                                          (("2"
                                            (decompose-equality)
                                            nil
                                            nil))
                                          nil))
                                        nil)
                                       ("3" (propax) nil nil)
                                       ("4" (flatten) nil nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (hide-all-but (-2 1))
                                  (("2"
                                    (decompose-equality)
                                    (("2"
                                      (decompose-equality)
                                      nil
                                      nil))
                                    nil))
                                  nil)
                                 ("3" (propax) nil nil)
                                 ("4" (assert) nil nil))
                                nil)
                               ("2"
                                (typepred "d1!1")
                                (("2"
                                  (typepred "d2!1")
                                  (("2"
                                    (expand "derivation_tree?")
                                    (("2"
                                      (assert)
                                      (("2"
                                        (expand "S")
                                        (("2"
                                          (expand "S")
                                          (("2"
                                            (expand "s1")
                                            (("2"
                                              (expand "s1")
                                              (("2"
                                                (expand "s0")
                                                (("2"
                                                  (expand "s0")
                                                  (("2"
                                                    (assert)
                                                    (("2"
                                                      (flatten)
                                                      (("2"
                                                        (assert)
                                                        (("2"
                                                          (lift-if)
                                                          (("2"
                                                            (assert)
                                                            (("2"
                                                              (case-replace
                                                               "Sequence?(d(d1!1)`1)")
                                                              (("1"
                                                                (assert)
                                                                nil
                                                                nil)
                                                               ("2"
                                                                (assert)
                                                                (("2"
                                                                  (flatten)
                                                                  (("2"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (assert) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((branch1 adt-constructor-decl
     "[[[Stm[V], State[V], State[V]], tree] -> (branch1?)]" natural
     nil)
    (tree_branch1_extensionality formula-decl nil natural nil)
    (BExp type-decl nil BExp nil)
    (B def-decl "[State -> bool]" BExp nil)
    (Conditional? adt-recognizer-decl "[Stm -> boolean]" Stm nil)
    (While? adt-recognizer-decl "[Stm -> boolean]" Stm nil)
    (b shared-adt-accessor-decl
     "[{x: Stm | Conditional?(x) OR While?(x)} -> BExp[V]]" Stm nil)
    (s1 const-decl "State" natural nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (Sequence? adt-recognizer-decl "[Stm -> boolean]" Stm nil)
    (d2!1 skolem-const-decl "derivation_tree" natural nil)
    (d1!1 skolem-const-decl "derivation_tree" natural nil)
    (tree_branch2_extensionality formula-decl nil natural nil)
    (branch2 adt-constructor-decl
     "[[[Stm[V], State[V], State[V]], tree, tree] -> (branch2?)]"
     natural nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (branch1? adt-recognizer-decl "[tree -> boolean]" natural nil)
    (branch2? adt-recognizer-decl "[tree -> boolean]" natural nil)
    (t1 shared-adt-accessor-decl
     "[{x: tree | branch1?(x) OR branch2?(x)} -> tree]" natural nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (t2 adt-accessor-decl "[(branch2?) -> tree]" natural nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (S const-decl "Stm" natural nil)
    (s0 const-decl "State" natural nil)
    (s1 const-decl "State" natural nil)
    (tree_leaf_extensionality formula-decl nil natural nil)
    (Assign? adt-recognizer-decl "[Stm -> boolean]" Stm nil)
    (Skip? adt-recognizer-decl "[Stm -> boolean]" Stm nil)
    (d shared-adt-accessor-decl
     "[tree -> [Stm[V], State[V], State[V]]]" natural nil)
    (leaf adt-constructor-decl
     "[[Stm[V], State[V], State[V]] -> (leaf?)]" natural nil)
    (leaf? adt-recognizer-decl "[tree -> boolean]" natural nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (pred type-eq-decl nil defined_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (< const-decl "bool" reals nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (nat_max application-judgement "{k: nat | i <= k AND j <= k}"
     real_defs nil)
    (nonneg_rat_max application-judgement
     "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil)
    (tree type-decl nil natural nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (derivation_tree? def-decl "bool" natural nil)
    (derivation_tree nonempty-type-eq-decl nil natural 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)
    (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)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil) (depth def-decl "nat" natural nil)
    (V formal-nonempty-type-decl nil natural nil)
    (Stm type-decl nil Stm nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (S const-decl "Stm" natural nil)
    (State nonempty-type-eq-decl nil State nil)
    (s0 const-decl "State" natural nil))
   shostak))
 (SS_TCC1 0
  (SS_TCC1-1 nil 3400238483
   ("" (skosimp*)
    (("" (expand "nonempty?")
      (("" (expand "empty?")
        (("" (expand "member")
          (("" (inst - "s1(d!1)")
            (("" (inst + "d!1") (("" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((nonempty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (derivation_tree nonempty-type-eq-decl nil natural nil)
    (derivation_tree? def-decl "bool" natural nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (s1 const-decl "State" natural nil)
    (tree type-decl nil natural nil)
    (State nonempty-type-eq-decl nil State 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (V formal-nonempty-type-decl nil natural nil)
    (empty? const-decl "bool" sets nil))
   nil))
 (SS_deterministic 0
  (SS_deterministic-1 nil 3400293675
   ("" (skolem + ("S!1" "s0!1" "s1!1"))
    (("" (expand "SS")
      (("" (lift-if)
        (("" (assert)
          (("" (case-replace "EXISTS d: S(d) = S!1 AND s0(d) = s0!1")
            (("1"
              (case "nonempty?({s1 |
                    EXISTS (d_1: derivation_tree):
                      S(d_1) = S!1 AND s0(d_1) = s0!1 AND s1(d_1) = s1})")
              (("1"
                (lemma "choose_member"
                 ("a" "{s1 |
                    EXISTS (d_1: derivation_tree):
                      S(d_1) = S!1 AND s0(d_1) = s0!1 AND s1(d_1) = s1}"))
                (("1" (split -1)
                  (("1"
                    (name-replace "CC" "choose({s1 |
                       EXISTS (d_1: derivation_tree):
                         S(d_1) = S!1 AND
                          s0(d_1) = s0!1 AND s1(d_1) = s1})")
                    (("1" (expand "member")
                      (("1" (hide -2 -3)
                        (("1" (skosimp)
                          (("1" (split)
                            (("1" (skosimp*)
                              (("1"
                                (lemma "dt_eq" ("d1" "d!1" "d2" "d!2"))
                                (("1" (assert) nil nil))
                                nil))
                              nil)
                             ("2" (flatten)
                              (("2"
                                (inst + "d!1")
                                (("2"
                                  (rewrite "up_equal")
                                  (("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (expand "nonempty?") (("2" (propax) nil nil))
                    nil))
                  nil))
                nil)
               ("2" (hide 2)
                (("2" (skosimp)
                  (("2" (expand "nonempty?")
                    (("2" (expand "empty?")
                      (("2" (expand "member")
                        (("2" (inst - "s1(d!1)")
                          (("2" (inst + "d!1") (("2" (assert) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (replace 1 2)
              (("2" (skosimp)
                (("2" (inst + "d!1") (("2" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((SS const-decl "Cont" natural nil)
    (s1 const-decl "State" natural nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil) (member const-decl "bool" sets nil)
    (up_equal formula-decl nil lift_props "orders/")
    (dt_eq formula-decl nil natural nil)
    (choose const-decl "(p)" sets nil)
    (choose_member formula-decl nil sets_lemmas nil)
    (empty? const-decl "bool" sets nil)
    (s0 const-decl "State" natural nil)
    (State nonempty-type-eq-decl nil State 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)
    (S const-decl "Stm" natural nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Stm type-decl nil Stm nil)
    (V formal-nonempty-type-decl nil natural nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (derivation_tree nonempty-type-eq-decl nil natural nil)
    (derivation_tree? def-decl "bool" natural nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (tree type-decl nil natural nil))
   shostak))
 (natural_le_sos 0
  (natural_le_sos-1 nil 3400294622
   ("" (expand "sq_le")
    ((""
      (case "forall (S:Stm,s1,s2:State,n:nat): (EXISTS d: depth(d) <= n &S(d) = S AND s0(d) = s1 AND s1(d) = s2)=>sos.SS(S)(s1) = up(s2)")
      (("1" (skosimp*)
        (("1" (rewrite "SS_deterministic" * :dir rl)
          (("1" (skosimp)
            (("1" (inst - "S!1" "s1!1" "s2!1" "depth(d!1)")
              (("1" (split -1)
                (("1" (propax) nil nil)
                 ("2" (inst + "d!1") (("2" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide 2)
        (("2" (induct "n")
          (("1" (skosimp*)
            (("1" (expand "depth")
              (("1" (lift-if)
                (("1" (assert)
                  (("1" (prop)
                    (("1" (typepred "d!1")
                      (("1" (expand "derivation_tree?")
                        (("1" (assert)
                          (("1" (split)
                            (("1" (expand "S")
                              (("1"
                                (expand "s1")
                                (("1"
                                  (expand "s0")
                                  (("1"
                                    (expand "S")
                                    (("1"
                                      (expand "s0")
                                      (("1"
                                        (expand "s1")
                                        (("1"
                                          (replace -3)
                                          (("1"
                                            (replace -4)
                                            (("1"
                                              (replace -5)
                                              (("1"
                                                (flatten)
                                                (("1"
                                                  (rewrite
                                                   "sos.SS_deterministic"
                                                   1
                                                   :dir
                                                   rl)
                                                  (("1"
                                                    (inst + "1")
                                                    (("1"
                                                      (expand "tr")
                                                      (("1"
                                                        (expand "step")
                                                        (("1"
                                                          (assert)
                                                          (("1"
                                                            (expand
                                                             "tr")
                                                            (("1"
                                                              (replace
                                                               -2
                                                               1)
                                                              (("1"
                                                                (propax)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (expand "s0")
                              (("2"
                                (expand "S")
                                (("2"
                                  (expand "S")
                                  (("2"
                                    (expand "s0")
                                    (("2"
                                      (expand "s1")
                                      (("2"
                                        (expand "s1")
                                        (("2"
                                          (replace -3)
                                          (("2"
                                            (replace -4)
                                            (("2"
                                              (replace -5)
                                              (("2"
                                                (flatten)
                                                (("2"
                                                  (rewrite
                                                   "sos.SS_deterministic"
                                                   1
                                                   :dir
                                                   rl)
                                                  (("2"
                                                    (inst + "1")
                                                    (("2"
                                                      (expand "tr")
                                                      (("2"
                                                        (expand "step")
                                                        (("2"
                                                          (expand "tr")
                                                          (("2"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("3" (expand "S")
                              (("3"
                                (expand "S")
                                (("3"
                                  (expand "s0")
                                  (("3"
                                    (expand "s0")
                                    (("3"
                                      (expand "s1")
                                      (("3"
                                        (expand "s1")
                                        (("3"
                                          (replace -3)
                                          (("3"
                                            (replace -4)
                                            (("3"
                                              (replace -5)
                                              (("3"
                                                (flatten)
                                                (("3"
                                                  (rewrite
                                                   "sos.SS_deterministic"
                                                   +
                                                   :dir
                                                   rl)
                                                  (("3"
                                                    (expand "tr")
                                                    (("3"
                                                      (expand "step")
                                                      (("3"
                                                        (assert)
                                                        (("3"
                                                          (expand "tr")
                                                          (("3"
                                                            (expand
                                                             "step")
                                                            (("3"
                                                              (expand
                                                               "tr")
                                                              (("3"
                                                                (expand
                                                                 "step")
                                                                (("3"
                                                                  (expand
                                                                   "tr")
                                                                  (("3"
                                                                    (inst
                                                                     +
                                                                     "3")
                                                                    (("3"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.57 Sekunden  (vorverarbeitet)  ¤



Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




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.


Bot Zugriff