Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: bisimulation.prf Sprache: Lisp

Original von: PVS^©

(bisimulation
(correct_AExp 0
  (correct_AExp-1 nil 3398501093
   ("" (induct "a")
    (("1" (skolem + "n!1")
      (("1" (skosimp)
        (("1" (expand "CA")
          (("1" (expand "am.tr")
            (("1" (expand "step")
              (("1" (expand "push")
                (("1" (expand "A")
                  (("1" (inst + "1")
                    (("1" (assert)
                      (("1" (expand "am.tr") (("1" (propax) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (skolem + ("x!1"))
      (("2" (skosimp)
        (("2" (inst + "1")
          (("2" (expand "CA")
            (("2" (expand "A")
              (("2" (expand "am.tr")
                (("2" (expand "step")
                  (("2" (expand "am.tr")
                    (("2" (expand "push") (("2" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("3" (skolem + ("a!1" "a!2"))
      (("3" (skosimp*)
        (("3" (expand "A" 1)
          (("3" (expand "CA" 1)
            (("3" (inst -2 "e!1" "s!1")
              (("3" (skosimp)
                (("3" (inst - "cons(A(a!2)(s!1), e!1)" "s!1")
                  (("3" (skosimp)
                    (("3" (inst + "n!1+n!2+1")
                      (("3" (name-replace "C1" "CA(a!1)")
                        (("3" (name-replace "C2" "CA(a!2)")
                          (("3" (name-replace "N1" "A(a!1)(s!1)")
                            (("3" (name-replace "N2" "A(a!2)(s!1)")
                              (("3"
                                (case
                                 "am.tr(1)((cons(BINARY(LAMBDA (i, j:int): i + j), null[Instruction]),cons(N1, cons(N2, e!1)), s!1),(null, cons(N1 + N2, e!1), s!1))")
                                (("1"
                                  (name-replace
                                   "C3"
                                   "cons(BINARY(LAMBDA (i, j: int): i + j), null[Instruction])")
                                  (("1"
                                    (case
                                     "am.tr
          (n!2+1)((append(C1, C3),cons(N2, e!1), s!1), (null, cons(N1 + N2, e!1), s!1))")
                                    (("1"
                                      (hide -2 -3)
                                      (("1"
                                        (lemma
                                         "code_partial"
                                         ("k"
                                          "n!1"
                                          "c0"
                                          "C2"
                                          "e0"
                                          "e!1"
                                          "s0"
                                          "s!1"
                                          "c1"
                                          "null[Instruction]"
                                          "e1"
                                          "cons(N2, e!1)"
                                          "s1"
                                          "s!1"
                                          "c2"
                                          "append(C1, C3)"
                                          "e2"
                                          "null[int]"))
                                        (("1"
                                          (replace -3)
                                          (("1"
                                            (rewrite "append_null")
                                            (("1"
                                              (rewrite "append_null")
                                              (("1"
                                                (expand "append" -1 3)
                                                (("1"
                                                  (lemma
                                                   "am.tr_add"
                                                   ("k1"
                                                    "n!1"
                                                    "k2"
                                                    "n!2+1"
                                                    "cf0"
                                                    "(append(C2, append(C1, C3)), e!1, s!1)"
                                                    "cf2"
                                                    "(null[Instruction], cons(N1 + N2, e!1), s!1)"))
                                                  (("1"
                                                    (replace -1 1)
                                                    (("1"
                                                      (inst
                                                       +
                                                       "(append(C1, C3), cons(N2, e!1), s!1)")
                                                      (("1"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (hide -3 2)
                                      (("2"
                                        (lemma
                                         "code_partial"
                                         ("k"
                                          "n!2"
                                          "c0"
                                          "C1"
                                          "e0"
                                          "cons(N2, e!1)"
                                          "s0"
                                          "s!1"
                                          "c1"
                                          "null[Instruction]"
                                          "e1"
                                          "cons(N1, cons(N2, e!1))"
                                          "s1"
                                          "s!1"
                                          "c2"
                                          "C3"
                                          "e2"
                                          "null[int]"))
                                        (("2"
                                          (replace -3)
                                          (("2"
                                            (rewrite "append_null")
                                            (("2"
                                              (rewrite "append_null")
                                              (("2"
                                                (expand "append" -1 2)
                                                (("2"
                                                  (hide -3)
                                                  (("2"
                                                    (lemma
                                                     "am.tr_add"
                                                     ("k1"
                                                      "n!2"
                                                      "k2"
                                                      "1"
                                                      "cf0"
                                                      "(append(C1, C3), cons(N2, e!1), s!1)"
                                                      "cf2"
                                                      "(null[Instruction], cons(N1 + N2, e!1), s!1)"))
                                                    (("2"
                                                      (replace -1 1)
                                                      (("2"
                                                        (hide -1)
                                                        (("2"
                                                          (inst
                                                           +
                                                           "(C3, cons(N1, cons(N2, e!1)), s!1)")
                                                          (("2"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (hide-all-but 1)
                                  (("2" (grind) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("4" (skolem + ("a!1" "a!2"))
      (("4" (skosimp*)
        (("4" (expand "A" 1)
          (("4" (expand "CA" 1)
            (("4" (inst - "cons(A(a!2)(s!1),e!1)" "s!1")
              (("4" (inst - "e!1" "s!1")
                (("4" (skosimp*)
                  (("4" (inst + "n!1+n!2+1")
                    (("4" (name-replace "N1" "A(a!1)(s!1)")
                      (("4" (name-replace "N2" "A(a!2)(s!1)")
                        (("4" (name-replace "C1" "CA(a!1)")
                          (("4" (name-replace "C2" "CA(a!2)")
                            (("4"
                              (case "am.tr(1)((cons(BINARY(LAMBDA (i, j:int): i - j), null[Instruction]),cons(N1, cons(N2, e!1)), s!1),(null, cons(N1 - N2, e!1), s!1))")
                              (("1"
                                (name-replace
                                 "C3"
                                 "cons(BINARY(LAMBDA (i, j: int): i - j), null[Instruction])")
                                (("1"
                                  (lemma
                                   "code_partial"
                                   ("k"
                                    "n!1"
                                    "c0"
                                    "C1"
                                    "c1"
                                    "null[Instruction]"
                                    "c2"
                                    "C3"
                                    "e0"
                                    "cons(N2, e!1)"
                                    "e1"
                                    "cons(N1, cons(N2, e!1))"
                                    "e2"
                                    "null[int]"
                                    "s0"
                                    "s!1"
                                    "s1"
                                    "s!1"))
                                  (("1"
                                    (replace -3)
                                    (("1"
                                      (rewrite "append_null")
                                      (("1"
                                        (rewrite "append_null")
                                        (("1"
                                          (expand "append" -1 2)
                                          (("1"
                                            (lemma
                                             "am.tr_add"
                                             ("k1"
                                              "n!1"
                                              "k2"
                                              "1"
                                              "cf0"
                                              "(append(C1, C3), cons(N2, e!1), s!1)"
                                              "cf2"
                                              "(null[Instruction], cons(N1 - N2, e!1), s!1)"))
                                            (("1"
                                              (flatten)
                                              (("1"
                                                (hide -1)
                                                (("1"
                                                  (split -1)
                                                  (("1"
                                                    (hide -2 -3 -4)
                                                    (("1"
                                                      (lemma
                                                       "code_partial"
                                                       ("k"
                                                        "n!2"
                                                        "c0"
                                                        "C2"
                                                        "c1"
                                                        "null[Instruction]"
                                                        "c2"
                                                        "append(C1, C3)"
                                                        "e0"
                                                        "e!1"
                                                        "e1"
                                                        "cons(N2, e!1)"
                                                        "e2"
                                                        "null[int]"
                                                        "s0"
                                                        "s!1"
                                                        "s1"
                                                        "s!1"))
                                                      (("1"
                                                        (replace -3)
                                                        (("1"
                                                          (rewrite
                                                           "append_null")
                                                          (("1"
                                                            (rewrite
                                                             "append_null")
                                                            (("1"
                                                              (expand
                                                               "append"
                                                               -1
                                                               3)
                                                              (("1"
                                                                (hide
                                                                 -3)
                                                                (("1"
                                                                  (lemma
                                                                   "am.tr_add"
                                                                   ("k1"
                                                                    "n!2"
                                                                    "k2"
                                                                    "n!1+1"
                                                                    "cf0"
                                                                    "(append(C2, append(C1, C3)), e!1, s!1)"
                                                                    "cf2"
                                                                    "(null[Instruction], cons(N1 - N2, e!1), s!1)"))
                                                                  (("1"
                                                                    (replace
                                                                     -1)
                                                                    (("1"
                                                                      (hide
                                                                       -1)
                                                                      (("1"
                                                                        (inst
                                                                         +
                                                                         "(append(C1, C3), cons(N2, e!1), s!1)")
                                                                        (("1"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (inst
                                                     +
                                                     "(C3, cons(N1, cons(N2, e!1)), s!1)")
                                                    (("2"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2" (grind) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("5" (skolem + ("a!1" "a!2"))
      (("5" (skosimp*)
        (("5" (inst - "cons(A(a!2)(s!1),e!1)" "s!1")
          (("5" (inst - "e!1" "s!1")
            (("5" (skosimp*)
              (("5" (inst + "n!1+n!2+1")
                (("5" (expand "CA" 1)
                  (("5" (expand "A" 1)
                    (("5" (name-replace "C1" "CA(a!1)")
                      (("5" (name-replace "C2" "CA(a!2)")
                        (("5" (name-replace "N1" "A(a!1)(s!1)")
                          (("5" (name-replace "N2" "A(a!2)(s!1)")
                            (("5"
                              (case "am.tr(1)((cons(BINARY(LAMBDA (i, j:int): i * j), null[Instruction]),cons(N1, cons(N2, e!1)), s!1),(null, cons(N1 * N2, e!1), s!1))")
                              (("1"
                                (name-replace
                                 "C3"
                                 "cons(BINARY(LAMBDA (i, j: int): i * j), null[Instruction])")
                                (("1"
                                  (lemma
                                   "am.tr_add"
                                   ("k1"
                                    "n!2"
                                    "k2"
                                    "n!1+1"
                                    "cf0"
                                    "(append(C2, append(C1, C3)), e!1, s!1)"
                                    "cf2"
                                    "(null[Instruction], cons(N1 * N2, e!1), s!1)"))
                                  (("1"
                                    (replace -1)
                                    (("1"
                                      (inst
                                       +
                                       "(append(C1, C3),cons(N2, e!1), s!1)")
                                      (("1"
                                        (hide -1)
                                        (("1"
                                          (split)
                                          (("1"
                                            (lemma
                                             "code_partial"
                                             ("k"
                                              "n!2"
                                              "c0"
                                              "C2"
                                              "e0"
                                              "e!1"
                                              "s0"
                                              "s!1"
                                              "c1"
                                              "null[Instruction]"
                                              "e1"
                                              "cons(N2, e!1)"
                                              "s1"
                                              "s!1"
                                              "c2"
                                              "append(C1, C3)"
                                              "e2"
                                              "null[int]"))
                                            (("1"
                                              (rewrite "append_null")
                                              (("1"
                                                (rewrite "append_null")
                                                (("1"
                                                  (expand
                                                   "append"
                                                   -1
                                                   3)
                                                  (("1"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (hide -3)
                                            (("2"
                                              (lemma
                                               "code_partial"
                                               ("k"
                                                "n!1"
                                                "c0"
                                                "C1"
                                                "e0"
                                                "cons(N2, e!1)"
                                                "s0"
                                                "s!1"
                                                "c1"
                                                "null[Instruction]"
                                                "e1"
                                                "cons(N1, cons(N2, e!1))"
                                                "s1"
                                                "s!1"
                                                "c2"
                                                "C3"
                                                "e2"
                                                "null[int]"))
                                              (("2"
                                                (rewrite "append_null")
                                                (("2"
                                                  (rewrite
                                                   "append_null")
                                                  (("2"
                                                    (expand
                                                     "append"
                                                     -1
                                                     2)
                                                    (("2"
                                                      (assert)
                                                      (("2"
                                                        (hide -3)
                                                        (("2"
                                                          (lemma
                                                           "am.tr_add"
                                                           ("k1"
                                                            "n!1"
                                                            "k2"
                                                            "1"
                                                            "cf0"
                                                            "(append(C1, C3), cons(N2, e!1), s!1)"
                                                            "cf2"
                                                            "(null[Instruction], cons(N1 * N2, e!1), s!1)"))
                                                          (("2"
                                                            (replace
                                                             -1)
                                                            (("2"
                                                              (inst
                                                               +
                                                               "(C3, cons(N1, cons(N2, e!1)), s!1)")
                                                              (("2"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (hide-all-but 1)
                                (("2"
                                  (expand "am.tr")
                                  (("2"
                                    (expand "step")
                                    (("2"
                                      (expand "am.tr")
                                      (("2"
                                        (assert)
                                        (("2"
                                          (expand "check2")
                                          (("2"
                                            (expand "top")
                                            (("2"
                                              (expand "pop")
                                              (("2"
                                                (expand "push")
                                                (("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))
    nil)
   ((mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (even_minus_odd_is_odd application-judgement "odd_int" integers
     nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (pop const-decl "Stack" am nil) (top const-decl "int" am nil)
    (check2 const-decl "bool" am nil) (tr_add formula-decl nil am nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (append_null formula-decl nil list_props nil)
    (code_partial formula-decl nil am nil)
    (append def-decl "list[T]" list_props nil)
    (BINARY adt-constructor-decl "[[[int, int] -> int] -> (BINARY?)]"
     Instruction nil)
    (BINARY? adt-recognizer-decl "[Instruction -> boolean]" Instruction
     nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (step const-decl "Config" am nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (push const-decl "Stack" am nil)
    (AExp_induction formula-decl nil AExp nil)
    (V formal-nonempty-type-decl nil bisimulation nil)
    (A def-decl "[State -> int]" AExp nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (CA def-decl "Code" compiler nil) (tr def-decl "bool" am nil)
    (Config nonempty-type-eq-decl nil am nil)
    (Stack nonempty-type-eq-decl nil am nil)
    (Code nonempty-type-eq-decl nil Instruction nil)
    (Instruction type-decl nil Instruction nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (every adt-def-decl "boolean" list_adt nil)
    (PRED type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (list type-decl nil list_adt nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (AExp type-decl nil AExp nil))
   shostak))
(correct_BExp 0
  (correct_BExp-1 nil 3399055662
   ("" (induct "b")
    (("1" (skosimp)
      (("1" (inst + "1")
        (("1" (expand "tr")
          (("1" (expand "CB")
            (("1" (expand "tr")
              (("1" (expand "step")
                (("1" (expand "push")
                  (("1" (expand "B") (("1" (propax) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (skosimp)
      (("2" (inst + "1")
        (("2" (expand "tr")
          (("2" (expand "tr")
            (("2" (expand "CB")
              (("2" (expand "B")
                (("2" (expand "step")
                  (("2" (expand "push") (("2" (propax) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("3" (skolem + ("a!1" "a!2"))
      (("3" (skosimp)
        (("3" (expand "CB")
          (("3" (lemma "correct_AExp" ("a" "a!2" "e" "e!1" "s" "s!1"))
            (("3" (skosimp)
              (("3"
                (lemma "correct_AExp"
                 ("a" "a!1" "e" "cons(A(a!2)(s!1), e!1)" "s" "s!1"))
                (("3" (skosimp)
                  (("3" (expand "B" 1)
                    (("3" (inst + "n!1+n!2+1")
                      (("3"
                        (lemma "code_partial"
                         ("k" "n!2" "c0" "CA(a!1)" "e0"
                          "cons(A(a!2)(s!1), e!1)" "s0" "s!1" "c1"
                          "null[Instruction]" "e1"
                          "cons(A(a!1)(s!1), cons(A(a!2)(s!1), e!1))"
                          "s1" "s!1" "c2"
                          "cons(BINARY(LAMBDA (i, j:int): b2n(i = j)), null)"
                          "e2" "null[int]"))
                        (("3" (replace -2)
                          (("3" (rewrite "append_null")
                            (("3" (rewrite "append_null")
                              (("3"
                                (expand "append" -1 2)
                                (("3"
                                  (name-replace
                                   "C2"
                                   "append(CA(a!1),
                 cons(BINARY(LAMBDA (i, j: int): b2n(i = j)), null))")
                                  (("3"
                                    (hide -2)
                                    (("3"
                                      (case
                                       "tr(n!2+1)((C2, cons(A(a!2)(s!1), e!1), s!1),(null[Instruction],cons(b2n(A(a!1)(s!1) = A(a!2)(s!1)), e!1), s!1))")
                                      (("1"
                                        (hide -2)
                                        (("1"
                                          (lemma
                                           "code_partial"
                                           ("k"
                                            "n!1"
                                            "c0"
                                            "CA(a!2)"
                                            "e0"
                                            "e!1"
                                            "s0"
                                            "s!1"
                                            "c1"
                                            "null[Instruction]"
                                            "e1"
                                            "cons(A(a!2)(s!1), e!1)"
                                            "s1"
                                            "s!1"
                                            "c2"
                                            "C2"
                                            "e2"
                                            "null[int]"))
                                          (("1"
                                            (assert)
                                            (("1"
                                              (rewrite "append_null")
                                              (("1"
                                                (rewrite "append_null")
                                                (("1"
                                                  (expand
                                                   "append"
                                                   -1
                                                   2)
                                                  (("1"
                                                    (lemma
                                                     "am.tr_add"
                                                     ("k1"
                                                      "n!1"
                                                      "k2"
                                                      "n!2+1"
                                                      "cf0"
                                                      "(append(CA(a!2), C2), e!1, s!1)"
                                                      "cf2"
                                                      "(null[Instruction], cons(b2n(A(a!1)(s!1) = A(a!2)(s!1)), e!1), s!1)"))
                                                    (("1"
                                                      (replace -1 1)
                                                      (("1"
                                                        (inst
                                                         +
                                                         "(C2, cons(A(a!2)(s!1), e!1), s!1)")
                                                        (("1"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (hide -2 2)
                                        (("2"
                                          (lemma
                                           "tr_add"
                                           ("k1"
                                            "n!2"
                                            "k2"
                                            "1"
                                            "cf0"
                                            "(C2, cons(A(a!2)(s!1), e!1), s!1)"
                                            "cf2"
                                            "(null[Instruction], cons(b2n(A(a!1)(s!1) = A(a!2)(s!1)), e!1),
          s!1)"))
                                          (("2"
                                            (replace -1)
                                            (("2"
                                              (inst
                                               +
                                               "(cons(BINARY(LAMBDA (i_1, j_1: int): b2n(i_1 = j_1)), null[Instruction]),
          cons(A(a!1)(s!1), cons(A(a!2)(s!1), e!1)), s!1)")
                                              (("2"
                                                (assert)
                                                (("2"
                                                  (hide-all-but 1)
                                                  (("2"
                                                    (expand "tr")
                                                    (("2"
                                                      (expand "tr")
                                                      (("2"
                                                        (expand "step")
                                                        (("2"
                                                          (expand
                                                           "check2")
                                                          (("2"
                                                            (expand
                                                             "top")
                                                            (("2"
                                                              (expand
                                                               "pop")
                                                              (("2"
                                                                (expand
                                                                 "push")
                                                                (("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))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("4" (skolem + ("a!1" "a!2"))
      (("4" (skosimp)
        (("4" (expand "CB")
          (("4" (expand "B")
            (("4"
              (lemma "correct_AExp" ("a" "a!2" "e" "e!1" "s" "s!1"))
              (("4"
                (lemma "correct_AExp"
                 ("a" "a!1" "e" "cons(A(a!2)(s!1),e!1)" "s" "s!1"))
                (("4" (skosimp*)
                  (("4" (inst + "n!1+n!2+1")
                    (("4"
                      (case "am.tr
          (n!1+1)((append(CA(a!1),
                          cons(BINARY(LAMBDA (i, j:int): b2n(i <= j)), null)),cons(A(a!2)(s!1), e!1), s!1),(null, cons(b2n(A(a!1)(s!1) <= A(a!2)(s!1)), e!1), s!1))")
                      (("1" (hide -2)
                        (("1"
                          (name-replace "C2" "append(CA(a!1),
                   cons(BINARY(LAMBDA (i, j: int): b2n(i <= j)), null))")
                          (("1"
                            (name-replace "CF2"
                             "(null[Instruction], cons(b2n(A(a!1)(s!1) <= A(a!2)(s!1)), e!1), s!1)")
                            (("1"
                              (lemma "code_partial"
                               ("k"
                                "n!2"
                                "c0"
                                "CA(a!2)"
                                "e0"
                                "e!1"
                                "s0"
                                "s!1"
                                "c1"
                                "null[Instruction]"
                                "e1"
                                "cons(A(a!2)(s!1), e!1)"
                                "s1"
                                "s!1"
                                "c2"
                                "C2"
                                "e2"
                                "null[int]"))
                              (("1"
                                (assert)
                                (("1"
                                  (rewrite "append_null")
                                  (("1"
                                    (rewrite "append_null")
                                    (("1"
                                      (expand "append" -1 2)
                                      (("1"
                                        (assert)
                                        (("1"
                                          (lemma
                                           "am.tr_add"
                                           ("k1"
                                            "n!2"
                                            "k2"
                                            "n!1+1"
                                            "cf0"
                                            "(append(CA(a!2), C2), e!1, s!1)"
                                            "cf2"
                                            "CF2"))
                                          (("1"
                                            (replace -1)
                                            (("1"
                                              (hide -1)
                                              (("1"
                                                (inst
                                                 +
                                                 "(C2, cons(A(a!2)(s!1), e!1), s!1)")
                                                (("1"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (hide -2 2)
                        (("2"
                          (lemma "code_partial"
                           ("k" "n!1" "c0" "CA(a!1)" "e0"
                            "cons(A(a!2)(s!1),e!1)" "s0" "s!1" "c1"
                            "null[Instruction]" "e1"
                            "cons(A(a!1)(s!1), cons(A(a!2)(s!1), e!1))"
                            "s1" "s!1" "c2"
                            "cons(BINARY(LAMBDA (i, j: int): b2n(i <= j)), null[Instruction])"
                            "e2" "null[int]"))
                          (("2" (assert)
                            (("2" (rewrite "append_null")
                              (("2"
                                (rewrite "append_null")
                                (("2"
                                  (expand "append" -1 2)
                                  (("2"
                                    (lemma
                                     "am.tr_add"
                                     ("k1"
                                      "n!1"
                                      "k2"
                                      "1"
                                      "cf0"
                                      "(append(CA(a!1),
                   cons(BINARY(LAMBDA (i, j: int): b2n(i <= j)), null)),
            cons(A(a!2)(s!1), e!1), s!1)"
                                      "cf2"
                                      "(null[Instruction], cons(b2n(A(a!1)(s!1) <= A(a!2)(s!1)), e!1), s!1)"))
                                    (("2"
                                      (replace -1)
                                      (("2"
                                        (inst
                                         +
                                         "(cons(BINARY(LAMBDA (i_1, j_1: int): b2n(i_1 <= j_1)),
               null[Instruction]),
          cons(A(a!1)(s!1), cons(A(a!2)(s!1), e!1)), s!1)")
                                        (("2"
                                          (assert)
                                          (("2"
                                            (hide-all-but 2)
                                            (("2"
                                              (expand "tr")
                                              (("2"
                                                (expand "tr")
                                                (("2"
                                                  (expand "step")
                                                  (("2"
                                                    (expand "check2")
                                                    (("2"
                                                      (expand "top")
                                                      (("2"
                                                        (expand "pop")
                                                        (("2"
                                                          (expand
                                                           "push")
                                                          (("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))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("5" (skolem + ("b!1"))
      (("5" (skosimp*)
        (("5" (inst - "e!1" "s!1")
          (("5" (skosimp)
            (("5" (inst + "n!1+1")
              (("5" (expand "CB" 1)
                (("5" (expand "B" 1)
                  (("5" (expand "b2n" 1)
                    (("5" (assert)
                      (("5"
                        (lemma "code_partial"
                         ("k" "n!1" "c0" "CB(b!1)" "e0" "e!1" "s0"
                          "s!1" "c1" "null[Instruction]" "e1"
                          "cons(b2n(B(b!1)(s!1)), e!1)" "s1" "s!1" "c2"
                          "cons(UNARY(LAMBDA (i:int): 1 - i), null[Instruction])"
                          "e2" "null[int]"))
                        (("5" (assert)
                          (("5" (rewrite "append_null")
                            (("5" (rewrite "append_null")
                              (("5"
                                (expand "append" -1 2)
                                (("5"
                                  (name
                                   "CF0"
                                   "(append(CB(b!1), cons(UNARY(LAMBDA (i:int): 1 - i), null[Instruction])), e!1, s!1)")
                                  (("5"
                                    (replace -1)
                                    (("5"
                                      (hide -1)
                                      (("5"
                                        (lemma
                                         "am.tr_add"
                                         ("k1"
                                          "n!1"
                                          "k2"
                                          "1"
                                          "cf0"
                                          "CF0"
                                          "cf2"
                                          "(null[Instruction], cons(IF NOT (B(b!1)(s!1)) THEN 1 ELSE 0 ENDIF, e!1), s!1)"))
                                        (("5"
                                          (replace -1 1)
                                          (("5"
                                            (hide -1)
                                            (("5"
                                              (inst
                                               +
                                               "(cons(UNARY(LAMBDA (i_1: int): 1 - i_1), null[Instruction]),
          cons(b2n(B(b!1)(s!1)), e!1), s!1)")
                                              (("5"
                                                (assert)
                                                (("5"
                                                  (hide -1 -2)
                                                  (("5"
                                                    (expand "tr")
                                                    (("5"
                                                      (expand "tr")
                                                      (("5"
                                                        (expand "step")
                                                        (("5"
                                                          (expand
                                                           "check1")
                                                          (("5"
                                                            (expand
                                                             "top")
                                                            (("5"
                                                              (expand
                                                               "push")
                                                              (("5"
                                                                (expand
                                                                 "pop")
                                                                (("5"
                                                                  (assert)
                                                                  (("5"
                                                                    (expand
                                                                     "b2n")
                                                                    (("5"
                                                                      (assert)
                                                                      (("5"
                                                                        (lift-if)
                                                                        (("5"
                                                                          (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))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("6" (skolem + ("b!1" "b!2"))
      (("6" (skosimp*)
        (("6" (expand "CB" 1)
          (("6" (expand "B" 1)
            (("6" (inst - "cons(b2n(B(b!2)(s!1)),e!1)" "s!1")
              (("6" (skosimp)
                (("6" (inst - "e!1" "s!1")
                  (("6" (skosimp)
                    (("6" (expand "b2n" 1)
                      (("6" (name-replace "B1" "B(b!1)(s!1)")
                        (("6" (name-replace "B2" "B(b!2)(s!1)")
                          (("6"
                            (case "am.tr
          (n!1+1)
          ((append(CB(b!1),
                            cons(BINARY(LAMBDA (i, j:int): i * j), null[Instruction])), cons(b2n(B2), e!1), s!1),(null[Instruction], cons(IF B1 AND B2 THEN 1 ELSE 0 ENDIF, e!1), s!1))")
                            (("1" (hide -2)
                              (("1"
                                (name-replace
                                 "C2"
                                 "append(CB(b!1),
                   cons(BINARY(LAMBDA (i, j: int): i * j),
                        null[Instruction]))")
                                (("1"
                                  (name-replace
                                   "CF2"
                                   "(null[Instruction], cons(IF B1 AND B2 THEN 1 ELSE 0 ENDIF, e!1),
            s!1)")
                                  (("1"
                                    (lemma
                                     "code_partial"
                                     ("k"
                                      "n!2"
                                      "c0"
                                      "CB(b!2)"
                                      "e0"
                                      "e!1"
                                      "s0"
                                      "s!1"
                                      "c1"
                                      "null[Instruction]"
                                      "e1"
                                      "cons(b2n(B2), e!1)"
                                      "s1"
                                      "s!1"
                                      "c2"
                                      "C2"
                                      "e2"
                                      "null[int]"))
                                    (("1"
                                      (assert)
                                      (("1"
                                        (rewrite "append_null")
                                        (("1"
                                          (rewrite "append_null")
                                          (("1"
                                            (expand "append" -1 2)
                                            (("1"
                                              (inst + "n!2+n!1+1")
                                              (("1"
                                                (lemma
                                                 "am.tr_add"
                                                 ("k1"
                                                  "n!2"
                                                  "k2"
                                                  "1+n!1"
                                                  "cf0"
                                                  "(append(CB(b!2), C2), e!1, s!1)"
                                                  "cf2"
                                                  "CF2"))
                                                (("1"
                                                  (replace -1)
                                                  (("1"
                                                    (inst
                                                     +
                                                     "(C2, cons(b2n(B2), e!1), s!1)")
                                                    (("1"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (hide -2 2)
                              (("2"
                                (lemma
                                 "code_partial"
                                 ("k"
                                  "n!1"
                                  "c0"
                                  "CB(b!1)"
                                  "e0"
                                  "cons(b2n(B2), e!1)"
                                  "s0"
                                  "s!1"
                                  "c1"
                                  "null[Instruction]"
                                  "e1"
                                  "cons(b2n(B1), cons(b2n(B2), e!1))"
                                  "s1"
                                  "s!1"
                                  "c2"
                                  "cons(BINARY(LAMBDA (i, j: int): i * j),
                        null[Instruction])"
                                  "e2"
                                  "null[int]"))
                                (("2"
                                  (assert)
                                  (("2"
                                    (rewrite "append_null")
                                    (("2"
                                      (rewrite "append_null")
                                      (("2"
                                        (expand "append" -1 2)
                                        (("2"
                                          (name-replace
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 1.134 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.