Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: compiler.prf Sprache: Lisp

Original von: PVS^©

(compiler
(CA_TCC1 0
  (CA_TCC1-1 nil 3398403700 ("" (grind) nil nil)
   ((V formal-nonempty-type-decl nil compiler nil)
    (<< adt-def-decl "(strict_well_founded?[AExp])" AExp nil))
   nil))
(CA_TCC2 0
  (CA_TCC2-1 nil 3398403700 ("" (grind) nil nil)
   ((V formal-nonempty-type-decl nil compiler nil)
    (<< adt-def-decl "(strict_well_founded?[AExp])" AExp nil))
   nil))
(CA_TCC3 0
  (CA_TCC3-1 nil 3398403700 ("" (grind) nil nil)
   ((V formal-nonempty-type-decl nil compiler nil)
    (<< adt-def-decl "(strict_well_founded?[AExp])" AExp nil))
   nil))
(CA_TCC4 0
  (CA_TCC4-1 nil 3398403700 ("" (grind) nil nil)
   ((V formal-nonempty-type-decl nil compiler nil)
    (<< adt-def-decl "(strict_well_founded?[AExp])" AExp nil))
   nil))
(CA_TCC5 0
  (CA_TCC5-1 nil 3398403700 ("" (grind) nil nil)
   ((V formal-nonempty-type-decl nil compiler nil)
    (<< adt-def-decl "(strict_well_founded?[AExp])" AExp nil))
   nil))
(CA_TCC6 0
  (CA_TCC6-1 nil 3398403700 ("" (grind) nil nil)
   ((V formal-nonempty-type-decl nil compiler nil)
    (<< adt-def-decl "(strict_well_founded?[AExp])" AExp nil))
   nil))
(CB_TCC1 0
  (CB_TCC1-1 nil 3399357896 ("" (termination-tcc) nil nil)
   ((V formal-nonempty-type-decl nil compiler nil)
    (<< adt-def-decl "(strict_well_founded?[BExp])" BExp nil))
   nil))
(CB_TCC2 0
  (CB_TCC2-1 nil 3399357896 ("" (termination-tcc) nil nil)
   ((V formal-nonempty-type-decl nil compiler nil)
    (<< adt-def-decl "(strict_well_founded?[BExp])" BExp nil))
   nil))
(CB_TCC3 0
  (CB_TCC3-1 nil 3399357896 ("" (termination-tcc) nil nil)
   ((V formal-nonempty-type-decl nil compiler nil)
    (<< adt-def-decl "(strict_well_founded?[BExp])" BExp nil))
   nil))
(CS_TCC1 0
  (CS_TCC1-1 nil 3399357896 ("" (termination-tcc) nil nil)
   ((V formal-nonempty-type-decl nil compiler nil)
    (<< adt-def-decl "(strict_well_founded?[Stm])" Stm nil))
   nil))
(CS_TCC2 0
  (CS_TCC2-1 nil 3399357896 ("" (termination-tcc) nil nil)
   ((V formal-nonempty-type-decl nil compiler nil)
    (<< adt-def-decl "(strict_well_founded?[Stm])" Stm nil))
   nil))
(CS_TCC3 0
  (CS_TCC3-1 nil 3399357896 ("" (termination-tcc) nil nil)
   ((V formal-nonempty-type-decl nil compiler nil)
    (<< adt-def-decl "(strict_well_founded?[Stm])" Stm nil))
   nil))
(CS_TCC4 0
  (CS_TCC4-1 nil 3399357896 ("" (termination-tcc) nil nil)
   ((V formal-nonempty-type-decl nil compiler nil)
    (<< adt-def-decl "(strict_well_founded?[Stm])" Stm nil))
   nil))
(CS_TCC5 0
  (CS_TCC5-1 nil 3399357896 ("" (termination-tcc) nil nil)
   ((V formal-nonempty-type-decl nil compiler nil)
    (<< adt-def-decl "(strict_well_founded?[Stm])" Stm nil))
   nil))
(nonnull_CA 0
  (nonnull_CA-1 nil 3399363243
   ("" (induct "a")
    (("1" (expand "CA") (("1" (propax) nil nil)) nil)
     ("2" (expand "CA") (("2" (propax) nil nil)) nil)
     ("3" (skosimp*)
      (("3" (expand "CA" -1)
        (("3"
          (lemma "append_is_null"
           ("l1" "CA(Add2_var!1)" "l2" "append(CA(Add1_var!1),
                          cons(BINARY(LAMBDA (i, j:int): i + j), null[Instruction]))"))
          (("3" (assert) nil nil)) nil))
        nil))
      nil)
     ("4" (skosimp)
      (("4"
        (lemma "append_is_null"
         ("l1" "CA(Sub2_var!1)" "l2" "append(CA(Sub1_var!1),
                          cons(BINARY(LAMBDA (i, j:int): i - j), null[Instruction]))"))
        (("4" (expand "CA" -2) (("4" (assert) nil nil)) nil)) nil))
      nil)
     ("5" (skosimp*)
      (("5"
        (lemma "append_is_null"
         ("l1" "CA(Mul2_var!1)" "l2" "append(CA(Mul1_var!1),
                          cons(BINARY(LAMBDA (i, j:int): i * j), null[Instruction]))"))
        (("5" (expand "CA" -2) (("5" (assert) 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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (BINARY adt-constructor-decl "[[[int, int] -> int] -> (BINARY?)]"
     Instruction nil)
    (BINARY? adt-recognizer-decl "[Instruction -> boolean]" Instruction
     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)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (append def-decl "list[T]" list_props nil)
    (append_is_null formula-decl nil list_props_aux nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (AExp_induction formula-decl nil AExp nil)
    (V formal-nonempty-type-decl nil compiler nil)
    (CA def-decl "Code" compiler nil)
    (Code nonempty-type-eq-decl nil Instruction nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (list type-decl nil list_adt nil)
    (Instruction type-decl nil Instruction nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (AExp type-decl nil AExp nil))
   shostak))
(nonnull_CB 0
  (nonnull_CB-1 nil 3399363470
   ("" (induct "b")
    (("1" (expand "CB") (("1" (propax) nil nil)) nil)
     ("2" (expand "CB") (("2" (propax) nil nil)) nil)
     ("3" (skosimp*)
      (("3" (expand "CB")
        (("3" (lemma "nonnull_CA" ("a" "Eq2_var!1"))
          (("3"
            (lemma "append_is_null"
             ("l1" "CA(Eq2_var!1)" "l2" "append(CA(Eq1_var!1),
                          cons(BINARY(LAMBDA (i, j:int): b2n(i = j)), null[Instruction]))"))
            (("3" (assert) nil nil)) nil))
          nil))
        nil))
      nil)
     ("4" (skosimp*)
      (("4" (expand "CB")
        (("4"
          (lemma "append_is_null"
           ("l1" "CA(Le2_var!1)" "l2" "append(CA(Le1_var!1),
                          cons(BINARY(LAMBDA (i, j:int): b2n(i <= j)), null[Instruction]))"))
          (("4" (lemma "nonnull_CA" ("a" "Le2_var!1"))
            (("4" (assert) nil nil)) nil))
          nil))
        nil))
      nil)
     ("5" (skolem + "b!1")
      (("5" (flatten)
        (("5" (expand "CB" -1)
          (("5"
            (lemma "append_is_null"
             ("l1" "CB(b!1)" "l2"
              "cons(UNARY(LAMBDA (i:int): 1 - i), null[Instruction])"))
            (("5" (assert) nil nil)) nil))
          nil))
        nil))
      nil)
     ("6" (skolem + ("b!1" "b!2"))
      (("6" (flatten)
        (("6" (expand "CB" -1)
          (("6"
            (lemma "append_is_null"
             ("l1" "CB(b!2)" "l2"
              "append(CB(b!1), cons(BINARY(LAMBDA (i, j:int): i * j), null[Instruction]))"))
            (("6"
              (lemma "append_is_null"
               ("l1" "CB(b!1)" "l2"
                "cons(BINARY(LAMBDA (i, j:int): i * j), null[Instruction])"))
              (("6" (assert) 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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (UNARY? adt-recognizer-decl "[Instruction -> boolean]" Instruction
     nil)
    (UNARY adt-constructor-decl "[[int -> int] -> (UNARY?)]"
     Instruction nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (<= const-decl "bool" reals nil)
    (nonnull_CA formula-decl nil compiler nil)
    (AExp type-decl nil AExp nil)
    (append_is_null formula-decl nil list_props_aux nil)
    (CA def-decl "Code" compiler nil)
    (append def-decl "list[T]" list_props nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (BINARY? adt-recognizer-decl "[Instruction -> boolean]" Instruction
     nil)
    (BINARY adt-constructor-decl "[[[int, int] -> int] -> (BINARY?)]"
     Instruction nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil) (nbit type-eq-decl nil bit nil)
    (b2n const-decl "nbit" bit nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (BExp_induction formula-decl nil BExp nil)
    (V formal-nonempty-type-decl nil compiler nil)
    (CB def-decl "Code" compiler nil)
    (Code nonempty-type-eq-decl nil Instruction nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (list type-decl nil list_adt nil)
    (Instruction type-decl nil Instruction nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (BExp type-decl nil BExp nil))
   shostak))
(nonnull_CS 0
  (nonnull_CS-1 nil 3399357897
   ("" (induct "S")
    (("1" (expand "CS")
      (("1" (skolem + ("x!1" "a!1"))
        (("1"
          (lemma "append_is_null"
           ("l1" "CA(a!1)" "l2" "cons(STORE(x!1), null[Instruction])"))
          (("1" (assert) nil nil)) nil))
        nil))
      nil)
     ("2" (expand "CS") (("2" (propax) nil nil)) nil)
     ("3" (skolem + ("S!1" "S!2"))
      (("3" (flatten)
        (("3" (expand "CS" -1)
          (("3"
            (lemma "append_is_null" ("l1" "CS(S!1)" "l2" "CS(S!2)"))
            (("3" (assert) nil nil)) nil))
          nil))
        nil))
      nil)
     ("4" (skolem + ("b!1" "S!1" "S!2"))
      (("4" (flatten)
        (("4" (expand "CS" -1)
          (("4"
            (lemma "append_is_null"
             ("l1" "CB(b!1)" "l2"
              "cons(BRANCH(CS(S!1), CS(S!2)), null[Instruction])"))
            (("4" (assert) nil nil)) nil))
          nil))
        nil))
      nil)
     ("5" (skolem + ("b!1" "S!1"))
      (("5" (flatten)
        (("5" (expand "CS" -1) (("5" (propax) nil nil)) nil)) nil))
      nil))
    nil)
   ((BExp type-decl nil BExp nil) (CB def-decl "Code" compiler nil)
    (BRANCH? adt-recognizer-decl "[Instruction -> boolean]" Instruction
     nil)
    (BRANCH adt-constructor-decl
     "[[list[Instruction], list[Instruction]] -> (BRANCH?)]"
     Instruction nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (STORE adt-constructor-decl "[V -> (STORE?)]" Instruction nil)
    (STORE? adt-recognizer-decl "[Instruction -> boolean]" Instruction
     nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (CA def-decl "Code" compiler nil) (AExp type-decl nil AExp nil)
    (append_is_null formula-decl nil list_props_aux nil)
    (Stm_induction formula-decl nil Stm nil)
    (V formal-nonempty-type-decl nil compiler nil)
    (CS def-decl "Code" compiler nil)
    (Code nonempty-type-eq-decl nil Instruction nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (list type-decl nil list_adt nil)
    (Instruction type-decl nil Instruction nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Stm type-decl nil Stm nil))
   shostak)))

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