Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: ln_series.pvs Sprache: Lisp

Original von: PVS^©

(axiomatic
(inference_tree?_TCC1 0
  (inference_tree?_TCC1-1 nil 3399608346 ("" (termination-tcc) nil nil)
   ((S const-decl "Stm" axiomatic nil)) nil))
(inference_tree?_TCC2 0
  (inference_tree?_TCC2-1 nil 3399608346 ("" (subtype-tcc) nil nil)
   ((S const-decl "Stm" axiomatic nil)) nil))
(inference_tree?_TCC3 0
  (inference_tree?_TCC3-1 nil 3399608346 ("" (termination-tcc) nil nil)
   ((<< adt-def-decl "(strict_well_founded?[tree])" axiomatic nil)
    (S const-decl "Stm" axiomatic nil))
   nil))
(inference_tree?_TCC4 0
  (inference_tree?_TCC4-1 nil 3399608883 ("" (termination-tcc) nil nil)
   ((<< adt-def-decl "(strict_well_founded?[tree])" axiomatic nil)
    (S const-decl "Stm" axiomatic nil))
   nil))
(inference_tree?_TCC5 0
  (inference_tree?_TCC5-1 nil 3399608883 ("" (subtype-tcc) nil nil)
   ((S const-decl "Stm" axiomatic nil)) nil))
(inference_tree?_TCC6 0
  (inference_tree?_TCC6-1 nil 3399608883 ("" (subtype-tcc) nil nil)
   ((S const-decl "Stm" axiomatic nil)) nil))
(inference_tree?_TCC7 0
  (inference_tree?_TCC7-1 nil 3399608883 ("" (termination-tcc) nil nil)
   ((<< adt-def-decl "(strict_well_founded?[tree])" axiomatic nil)
    (S const-decl "Stm" axiomatic nil))
   nil))
(inference_tree?_TCC8 0
  (inference_tree?_TCC8-1 nil 3399608883 ("" (termination-tcc) nil nil)
   ((<< adt-def-decl "(strict_well_founded?[tree])" axiomatic nil)
    (S const-decl "Stm" axiomatic nil))
   nil))
(inference_tree?_TCC9 0
  (inference_tree?_TCC9-1 nil 3399608883 ("" (subtype-tcc) nil nil)
   ((S const-decl "Stm" axiomatic nil)) nil))
(inference_tree?_TCC10 0
  (inference_tree?_TCC10-1 nil 3399608883
   ("" (termination-tcc) nil nil)
   ((<< adt-def-decl "(strict_well_founded?[tree])" axiomatic nil)
    (S const-decl "Stm" axiomatic nil))
   nil))
(inference_tree?_TCC11 0
  (inference_tree?_TCC11-1 nil 3399608883 ("" (subtype-tcc) nil nil)
   ((S const-decl "Stm" axiomatic nil)) nil))
(inference_tree?_TCC12 0
  (inference_tree?_TCC12-1 nil 3399608883
   ("" (termination-tcc) nil nil)
   ((<< adt-def-decl "(strict_well_founded?[tree])" axiomatic nil))
   nil))
(inference_tree_TCC1 0
  (inference_tree_TCC1-1 nil 3399608346
   ("" (expand "inference_tree?")
    (("" (expand "S")
      (("" (expand "P") (("" (expand "Q") (("" (propax) nil nil)) nil))
        nil))
      nil))
    nil)
   ((S const-decl "Stm" axiomatic nil)
    (Q const-decl "Predicate" axiomatic nil)
    (P const-decl "Predicate" axiomatic nil)
    (inference_tree? def-decl "bool" axiomatic nil))
   nil))
(wlp_is_precondition 0
  (wlp_is_precondition-1 nil 3399619747
   ("" (skosimp)
    (("" (expand "wlp")
      (("" (expand "|=")
        (("" (skosimp*)
          (("" (inst - "s1!1") (("" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((wlp const-decl "bool" axiomatic 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 axiomatic nil)
    (\|= const-decl "bool" axiomatic nil))
   shostak))
(wlp_is_weakest 0
  (wlp_is_weakest-1 nil 3399619791
   ("" (skosimp*)
    (("" (expand "|>")
      (("" (skosimp)
        (("" (expand "|=")
          (("" (expand "wlp")
            (("" (skosimp)
              (("" (inst - "s!1" "s1!1") (("" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((\|> const-decl "bool" axiomatic nil)
    (\|= const-decl "bool" axiomatic 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 axiomatic nil)
    (wlp const-decl "bool" axiomatic nil))
   shostak))
(soundness 0
  (soundness-1 nil 3399608945
   ("" (expand "|-")
    (("" (case "forall (t:inference_tree): |=(H(t))")
      (("1" (skosimp)
        (("1" (skosimp)
          (("1" (inst - "t!1")
            (("1" (replace -2) (("1" (propax) nil nil)) nil)) nil))
          nil))
        nil)
       ("2" (hide 2)
        (("2" (induct "t")
          (("1" (typepred "t!1") (("1" (propax) nil nil)) nil)
           ("2" (skolem + ("HH"))
            (("2" (flatten)
              (("2" (expand "|=")
                (("2" (skosimp)
                  (("2" (expand "H")
                    (("2" (expand "inference_tree?")
                      (("2" (flatten)
                        (("2" (expand "assign")
                          (("2" (expand "Q")
                            (("2" (expand "P")
                              (("2"
                                (expand "S")
                                (("2"
                                  (replace -2 -3 rl)
                                  (("2"
                                    (assert)
                                    (("2"
                                      (hide -2)
                                      (("2"
                                        (rewrite
                                         "SS_deterministic"
                                         *
                                         :dir
                                         rl)
                                        (("2"
                                          (skosimp)
                                          (("2"
                                            (expand "tr")
                                            (("2"
                                              (expand "step")
                                              (("2"
                                                (expand "tr")
                                                (("2"
                                                  (prop)
                                                  (("2"
                                                    (decompose-equality)
                                                    (("2"
                                                      (replace -1)
                                                      (("2"
                                                        (propax)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("3" (skolem + ("HH"))
            (("3" (flatten)
              (("3" (expand "|=")
                (("3" (skosimp)
                  (("3" (expand "inference_tree?")
                    (("3" (flatten)
                      (("3" (expand "H")
                        (("3" (expand "Q")
                          (("3" (expand "P")
                            (("3"
                              (rewrite "SS_deterministic" -4 :dir rl)
                              (("3"
                                (skosimp)
                                (("3"
                                  (expand "tr")
                                  (("3"
                                    (expand "step")
                                    (("3"
                                      (assert)
                                      (("3"
                                        (expand "S")
                                        (("3"
                                          (assert)
                                          (("3"
                                            (expand "tr")
                                            (("3"
                                              (prop)
                                              (("3"
                                                (decompose-equality)
                                                (("3"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("4" (skolem + ("HH" "T1" "T2"))
            (("4" (flatten)
              (("4" (expand "inference_tree?" -3)
                (("4" (flatten)
                  (("4" (expand "H" 1)
                    (("4" (expand "|=")
                      (("4" (skosimp)
                        (("4" (replace -6)
                          (("4" (replace -7)
                            (("4" (hide -6 -7)
                              (("4"
                                (expand "S" (-4 -5))
                                (("4"
                                  (expand "P")
                                  (("4"
                                    (expand "Q")
                                    (("4"
                                      (replace -6)
                                      (("4"
                                        (rewrite
                                         "SS_deterministic"
                                         *
                                         :dir
                                         rl)
                                        (("4"
                                          (skosimp)
                                          (("4"
                                            (expand "S")
                                            (("4"
                                              (lemma
                                               "tr_split"
                                               ("k"
                                                "n!1"
                                                "S1"
                                                "S1(HH`2)"
                                                "S2"
                                                "S2(HH`2)"
                                                "s0"
                                                "s!1"
                                                "s2"
                                                "s1!1"))
                                              (("4"
                                                (case-replace
                                                 "Sequence(S1(HH`2), S2(HH`2))=HH`2")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (skosimp)
                                                    (("1"
                                                      (replace -8)
                                                      (("1"
                                                        (replace -9)
                                                        (("1"
                                                          (replace -11)
                                                          (("1"
                                                            (replace
                                                             -12)
                                                            (("1"
                                                              (hide
                                                               -7
                                                               -8
                                                               -9
                                                               -10
                                                               -11
                                                               -12
                                                               -1)
                                                              (("1"
                                                                (inst
                                                                 -
                                                                 "s!1"
                                                                 "s1!2")
                                                                (("1"
                                                                  (replace
                                                                   -6)
                                                                  (("1"
                                                                    (split
                                                                     -4)
                                                                    (("1"
                                                                      (inst
                                                                       -
                                                                       "s1!2"
                                                                       "s1!1")
                                                                      (("1"
                                                                        (replace
                                                                         -1)
                                                                        (("1"
                                                                          (split
                                                                           -5)
                                                                          (("1"
                                                                            (propax)
                                                                            nil
                                                                            nil)
                                                                           ("2"
                                                                            (rewrite
                                                                             "SS_deterministic"
                                                                             *
                                                                             :dir
                                                                             rl)
                                                                            (("2"
                                                                              (inst
                                                                               +
                                                                               "k2!1")
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (rewrite
                                                                       "SS_deterministic"
                                                                       *
                                                                       :dir
                                                                       rl)
                                                                      (("2"
                                                                        (inst
                                                                         +
                                                                         "k1!1")
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (decompose-equality)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("5" (skolem + ("HH" "T1" "T2"))
            (("5" (flatten)
              (("5" (expand "inference_tree?" -3)
                (("5" (flatten)
                  (("5" (assert)
                    (("5" (expand "S")
                      (("5" (expand "P")
                        (("5" (expand "Q")
                          (("5" (expand "|=")
                            (("5" (expand "H" 1)
                              (("5"
                                (skosimp)
                                (("5"
                                  (rewrite
                                   "SS_deterministic"
                                   *
                                   :dir
                                   rl)
                                  (("5"
                                    (skosimp)
                                    (("5"
                                      (replace -8)
                                      (("5"
                                        (replace -9)
                                        (("5"
                                          (replace -10)
                                          (("5"
                                            (replace -11)
                                            (("5"
                                              (hide
                                               -6
                                               -7
                                               -8
                                               -9
                                               -10
                                               -11)
                                              (("5"
                                                (inst - "s!1" "s1!1")
                                                (("5"
                                                  (inst - "s!1" "s1!1")
                                                  (("5"
                                                    (expand "&")
                                                    (("5"
                                                      (replace -6)
                                                      (("5"
                                                        (expand "~")
                                                        (("5"
                                                          (case-replace
                                                           "B(b(HH`2))(s!1)")
                                                          (("1"
                                                            (split -2)
                                                            (("1"
                                                              (propax)
                                                              nil
                                                              nil)
                                                             ("2"
                                                              (rewrite
                                                               "SS_deterministic"
                                                               *
                                                               :dir
                                                               rl)
                                                              (("2"
                                                                (inst
                                                                 +
                                                                 "n!1-1")
                                                                (("1"
                                                                  (expand
                                                                   "tr"
                                                                   -6)
                                                                  (("1"
                                                                    (expand
                                                                     "step")
                                                                    (("1"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (assert)
                                                                  (("2"
                                                                    (expand
                                                                     "tr")
                                                                    (("2"
                                                                      (propax)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (replace 1)
                                                            (("2"
                                                              (split
                                                               -1)
                                                              (("1"
                                                                (propax)
                                                                nil
                                                                nil)
                                                               ("2"
                                                                (rewrite
                                                                 "SS_deterministic"
                                                                 *
                                                                 :dir
                                                                 rl)
                                                                (("2"
                                                                  (inst
                                                                   +
                                                                   "n!1-1")
                                                                  (("1"
                                                                    (expand
                                                                     "tr"
                                                                     -5)
                                                                    (("1"
                                                                      (expand
                                                                       "step")
                                                                      (("1"
                                                                        (assert)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (expand
                                                                     "tr")
                                                                    (("2"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("3"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("6" (assert)
            (("6" (skolem + ("HH" "T1"))
              (("6" (flatten)
                (("6" (copy -2)
                  (("6" (expand "inference_tree?" -1)
                    (("6" (flatten)
                      (("6" (assert)
                        (("6" (expand "H" 1)
                          (("6" (expand "|=")
                            (("6" (skosimp)
                              (("6"
                                (expand "S")
                                (("6"
                                  (expand "P")
                                  (("6"
                                    (expand "Q")
                                    (("6"
                                      (rewrite
                                       "SS_deterministic"
                                       *
                                       :dir
                                       rl)
                                      (("6"
                                        (skosimp)
                                        (("6"
                                          (replace -3)
                                          (("6"
                                            (replace -4)
                                            (("6"
                                              (replace -5)
                                              (("6"
                                                (hide -3 -4 -5)
                                                (("6"
                                                  (expand "&")
                                                  (("6"
                                                    (expand "~")
                                                    (("6"
                                                      (lemma
                                                       "NAT_induction"
                                                       ("p"
                                                        "lambda (k: nat): FORALL (x, y: State):
        HH`1(x) AND tr(k)(I(HH`2, x), T(y)) => NOT B(b(HH`2))(y) AND HH`1(y)"))
                                                      (("1"
                                                        (split -1)
                                                        (("1"
                                                          (inst
                                                           -
                                                           "n!1")
                                                          (("1"
                                                            (inst
                                                             -
                                                             "s!1"
                                                             "s1!1")
                                                            (("1"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (hide
                                                           -2
                                                           -5
                                                           -6
                                                           -7
                                                           2)
                                                          (("2"
                                                            (skosimp*)
                                                            (("2"
                                                              (expand
                                                               "tr"
                                                               -3)
                                                              (("2"
                                                                (expand
                                                                 "step"
                                                                 -3)
                                                                (("2"
                                                                  (assert)
                                                                  (("2"
                                                                    (case-replace
                                                                     "j!1=0")
                                                                    (("2"
                                                                      (assert)
                                                                      (("2"
                                                                        (expand
                                                                         "tr"
                                                                         -3)
                                                                        (("2"
                                                                          (expand
                                                                           "step"
                                                                           -3)
                                                                          (("2"
                                                                            (case-replace
                                                                             "j!1 - 1 = 0")
                                                                            (("2"
                                                                              (assert)
                                                                              (("2"
                                                                                (case-replace
                                                                                 "B(b(HH`2))(x!1)")
                                                                                (("1"
                                                                                  (lemma
                                                                                   "tr_split"
                                                                                   ("k"
                                                                                    "j!1-2"
                                                                                    "S1"
                                                                                    "S1(HH`2)"
                                                                                    "S2"
                                                                                    "HH`2"
                                                                                    "s0"
                                                                                    "x!1"
                                                                                    "s2"
                                                                                    "y!1"))
                                                                                  (("1"
                                                                                    (assert)
                                                                                    (("1"
                                                                                      (skosimp)
                                                                                      (("1"
                                                                                        (inst
                                                                                         -
                                                                                         "k2!1")
                                                                                        (("1"
                                                                                          (assert)
                                                                                          (("1"
                                                                                            (inst
                                                                                             -
                                                                                             "s1!2"
                                                                                             "y!1")
                                                                                            (("1"
                                                                                              (replace
                                                                                               -2)
                                                                                              (("1"
                                                                                                (inst
                                                                                                 -
                                                                                                 "x!1"
                                                                                                 "s1!2")
                                                                                                (("1"
                                                                                                  (replace
                                                                                                   -4)
                                                                                                  (("1"
                                                                                                    (replace
                                                                                                     -6)
                                                                                                    (("1"
                                                                                                      (split
                                                                                                       -10)
                                                                                                      (("1"
                                                                                                        (replace
                                                                                                         -1)
                                                                                                        (("1"
                                                                                                          (propax)
                                                                                                          nil
                                                                                                          nil))
                                                                                                        nil)
                                                                                                       ("2"
                                                                                                        (rewrite
                                                                                                         "SS_deterministic"
                                                                                                         *
                                                                                                         :dir
                                                                                                         rl)
                                                                                                        (("2"
                                                                                                          (inst
                                                                                                           +
                                                                                                           "k1!1")
                                                                                                          (("2"
                                                                                                            (replace
                                                                                                             -9)
                                                                                                            (("2"
                                                                                                              (propax)
                                                                                                              nil
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("2"
                                                                                  (assert)
                                                                                  (("2"
                                                                                    (expand
                                                                                     "tr"
                                                                                     -3)
                                                                                    (("2"
                                                                                      (expand
                                                                                       "step"
                                                                                       -3)
                                                                                      (("2"
                                                                                        (expand
                                                                                         "tr"
                                                                                         -3)
                                                                                        (("2"
                                                                                          (prop)
                                                                                          (("1"
                                                                                            (copy
                                                                                             -3)
                                                                                            (("1"
                                                                                              (decompose-equality)
                                                                                              (("1"
                                                                                                (assert)
                                                                                                nil
                                                                                                nil))
                                                                                              nil))
                                                                                            nil)
                                                                                           ("2"
                                                                                            (decompose-equality)
                                                                                            (("2"
                                                                                              (assert)
                                                                                              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))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("7" (skolem + ("HH" "T1"))
            (("7" (flatten)
              (("7" (expand "|=")
                (("7" (skosimp)
                  (("7" (expand "H" -3)
                    (("7" (expand "H" -4)
                      (("7" (expand "H" 1)
                        (("7" (expand "inference_tree?" -2)
                          (("7" (flatten)
                            (("7" (replace -2)
                              (("7"
                                (inst - "s!1" "s1!1")
                                (("7"
                                  (expand "S")
                                  (("7"
                                    (replace -3 * rl)
                                    (("7"
                                      (expand "P")
                                      (("7"
                                        (expand "Q")
                                        (("7"
                                          (assert)
                                          (("7"
                                            (expand "|>")
                                            (("7"
                                              (inst - "s!1")
                                              (("7"
                                                (assert)
                                                (("7"
                                                  (assert)
                                                  (("7"
                                                    (inst - "s1!1")
                                                    (("7"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((H def-decl "Hoare" axiomatic nil)
    (Hoare nonempty-type-eq-decl nil axiomatic nil)
    (\|= const-decl "bool" axiomatic nil) (Stm type-decl nil Stm nil)
    (Predicate nonempty-type-eq-decl nil axiomatic 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)
    (V formal-nonempty-type-decl nil axiomatic nil)
    (inference_tree nonempty-type-eq-decl nil axiomatic nil)
    (inference_tree? def-decl "bool" axiomatic nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (tree type-decl nil axiomatic nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (tree_induction formula-decl nil axiomatic nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (assign const-decl "bool" axiomatic nil)
    (P const-decl "Predicate" axiomatic nil)
    (step def-decl "[Config]" sos nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Config type-decl nil sos nil)
    (T? adt-recognizer-decl "[Config -> boolean]" sos nil)
    (s1 adt-accessor-decl "[(T?) -> State[V]]" sos nil)
    (T adt-constructor-decl "[State[V] -> (T?)]" sos nil)
    (assign const-decl "State" State nil)
    (Assign? adt-recognizer-decl "[Stm -> boolean]" Stm nil)
    (x adt-accessor-decl "[(Assign?) -> V]" Stm nil)
    (AExp type-decl nil AExp nil)
    (A def-decl "[State -> int]" AExp nil)
    (a adt-accessor-decl "[(Assign?) -> AExp[V]]" Stm nil)
    (tr def-decl "bool" sos nil)
    (SS_deterministic formula-decl nil sos nil)
    (S const-decl "Stm" axiomatic nil)
    (Q const-decl "Predicate" axiomatic nil)
    (tr_split formula-decl nil sos nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (Sequence? adt-recognizer-decl "[Stm -> boolean]" Stm nil)
    (Conditional? adt-recognizer-decl "[Stm -> boolean]" Stm nil)
    (While? adt-recognizer-decl "[Stm -> boolean]" Stm nil)
    (S1 shared-adt-accessor-decl
     "[{x: Stm | Sequence?(x) OR Conditional?(x) OR While?(x)} -> Stm]"
     Stm nil)
    (S2 shared-adt-accessor-decl
     "[{x: Stm | Sequence?(x) OR Conditional?(x)} -> Stm]" Stm nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (Stm_Sequence_extensionality formula-decl nil Stm nil)
    (HH skolem-const-decl "Hoare" axiomatic nil)
    (Sequence adt-constructor-decl "[[Stm, Stm] -> (Sequence?)]" Stm
     nil)
    (b shared-adt-accessor-decl
     "[{x: Stm | Conditional?(x) OR While?(x)} -> BExp[V]]" Stm nil)
    (B def-decl "[State -> bool]" BExp nil)
    (BExp type-decl nil BExp nil)
    (n!1 skolem-const-decl "nat" axiomatic nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (~ const-decl "bool" axiomatic nil)
    (& const-decl "bool" axiomatic nil)
    (I adt-constructor-decl "[[Stm[V], State[V]] -> (I?)]" sos nil)
    (I? adt-recognizer-decl "[Config -> boolean]" sos nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (NAT_induction formula-decl nil naturalnumbers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (\|> const-decl "bool" axiomatic nil)
    (\|- const-decl "bool" axiomatic nil))
   shostak))
(completeness 0
  (completeness-1 nil 3399619607
   ("" (case "FORALL (Q: Predicate, S: Stm): |-(wlp(S,Q), S, Q)")
    (("1" (skosimp)
      (("1" (inst - "Q!1" "S!1")
        (("1" (lemma "wlp_is_weakest" ("P" "P!1" "S" "S!1" "Q" "Q!1"))
          (("1" (assert)
            (("1" (hide -3)
              (("1" (expand "|-")
                (("1" (skosimp)
                  (("1" (inst + "cons((P!1, S!1, Q!1),t!1)")
                    (("1" (expand "H" 1) (("1" (propax) nil nil)) nil)
                     ("2" (typepred "t!1")
                      (("2" (expand "inference_tree?" 1)
                        (("2" (replace -3)
                          (("2" (expand "S")
                            (("2" (expand "P")
                              (("2"
                                (expand "Q")
                                (("2"
                                  (expand "|>")
                                  (("2" (skosimp) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (hide 2)
      (("2" (induct "S")
        (("1" (skolem + ("x!1" "a!1"))
          (("1" (skosimp)
            (("1" (expand "|-")
              (("1"
                (inst +
                 "ass((wlp(Assign(x!1, a!1), Q!1), Assign(x!1, a!1), Q!1))")
                (("1" (expand "H") (("1" (propax) nil nil)) nil)
                 ("2" (expand "inference_tree?")
                  (("2" (assert)
                    (("2" (expand "S")
                      (("2" (expand "Q")
                        (("2" (expand "P")
                          (("2" (expand "wlp")
                            (("2" (apply-extensionality :hide? t)
                              (("2"
                                (case-replace
                                 "assign(x!1, a!1)(Q!1)(x!2)")
                                (("1"
                                  (skosimp)
                                  (("1"
                                    (rewrite
                                     "SS_deterministic"
                                     *
                                     :dir
                                     rl)
                                    (("1"
                                      (skosimp)
                                      (("1"
                                        (expand "tr")
                                        (("1"
                                          (expand "step")
                                          (("1"
                                            (expand "tr")
                                            (("1"
                                              (prop)
                                              (("1"
                                                (decompose-equality)
                                                (("1"
                                                  (expand "assign" -3)
                                                  (("1"
                                                    (replace -1)
                                                    (("1"
                                                      (propax)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (replace 1)
                                  (("2"
                                    (assert)
                                    (("2"
                                      (expand "assign" 1)
                                      (("2"
                                        (inst
                                         -
                                         "assign(x!1, A(a!1))(x!2)")
                                        (("2"
                                          (assert)
                                          (("2"
                                            (rewrite
                                             "SS_deterministic"
                                             *
                                             :dir
                                             rl)
                                            (("2"
                                              (inst + "1")
                                              (("2"
                                                (expand "tr")
                                                (("2"
                                                  (expand "step")
                                                  (("2"
                                                    (expand "tr")
                                                    (("2"
                                                      (propax)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (skosimp)
          (("2" (expand "|-")
            (("2" (inst + "skip((wlp(Skip, Q!1), Skip, Q!1))")
              (("1" (expand "H") (("1" (propax) nil nil)) nil)
               ("2" (expand "inference_tree?")
                (("2" (expand "S")
                  (("2" (expand "P")
                    (("2" (expand "Q")
                      (("2" (expand "wlp")
                        (("2" (apply-extensionality :hide? t)
                          (("2" (case-replace "Q!1(x!1)")
                            (("1" (skosimp)
                              (("1"
                                (rewrite "SS_deterministic" * :dir rl)
                                (("1"
                                  (skosimp)
                                  (("1"
                                    (expand "tr")
                                    (("1"
                                      (expand "step")
                                      (("1"
                                        (expand "tr")
                                        (("1"
                                          (prop)
                                          (("1"
                                            (decompose-equality)
                                            (("1" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (assert)
                              (("2"
                                (inst - "x!1")
                                (("2"
                                  (split)
                                  (("1" (propax) nil nil)
                                   ("2"
                                    (rewrite
                                     "SS_deterministic"
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.196 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht 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.