Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: partial_function_props.prf Sprache: Lisp

Original von: PVS^©

(partial_function_props
(member_dom 0
  (member_dom-1 nil 3353045247 ("" (grind) nil nil)
   ((LPartFun_to_SPartFun const-decl "SubsetPartialFunction"
     PartialFunctionDefinitions nil)
    (dom const-decl "set[X]" partial_function_props nil)
    (/= const-decl "boolean" notequal nil))
   shostak))
(member_graph 0
  (member_graph-1 nil 3353048129
   ("" (skosimp)
    (("" (split)
      (("1" (skosimp*)
        (("1" (expand "graph")
          (("1" (expand "extend")
            (("1" (expand "LPartFun_to_SPartFun")
              (("1" (assert) nil nil)) nil))
            nil))
          nil))
        nil)
       ("2" (skosimp*)
        (("2" (inst + "down(f!1(x!1))")
          (("1" (expand "graph")
            (("1" (expand "extend")
              (("1" (expand "LPartFun_to_SPartFun")
                (("1" (assert)
                  (("1" (expand "graph") (("1" (propax) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((graph const-decl "set[[X, Y]]" partial_function_props nil)
    (LPartFun_to_SPartFun const-decl "SubsetPartialFunction"
     PartialFunctionDefinitions nil)
    (extend const-decl "R" extend nil)
    (x!1 skolem-const-decl "X" partial_function_props nil)
    (f!1 skolem-const-decl "LiftPartialFunction[X, Y]"
     partial_function_props nil)
    (LiftPartialFunction type-eq-decl nil PartialFunctionDefinitions
     nil)
    (X formal-type-decl nil partial_function_props nil)
    (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (lift type-decl nil lift_adt nil)
    (Y formal-type-decl nil partial_function_props nil)
    (down adt-accessor-decl "[(up?) -> T]" lift_adt nil)
    (graph const-decl "bool" functions nil))
   shostak))
(graph_eq 0
  (graph_eq-1 nil 3353051873
   ("" (skosimp)
    (("" (split)
      (("1" (flatten)
        (("1" (apply-extensionality :hide? t)
          (("1" (expand "graph")
            (("1" (expand "extend")
              (("1" (expand "LPartFun_to_SPartFun")
                (("1" (rewrite "extensionality_postulate" -1 :dir rl)
                  (("1" (case-replace "f1!1(x!1)=bottom")
                    (("1" (lemma "member_graph" ("f" "f2!1" "x" "x!1"))
                      (("1" (assert)
                        (("1" (skosimp)
                          (("1" (inst - "(x!1,y!1)")
                            (("1" (assert)
                              (("1"
                                (expand "graph")
                                (("1"
                                  (expand "extend")
                                  (("1"
                                    (expand "LPartFun_to_SPartFun")
                                    (("1" (propax) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (lemma "member_graph" ("f" "f1!1" "x" "x!1"))
                      (("2" (assert)
                        (("2" (skosimp)
                          (("2" (inst - "(x!1,y!1)")
                            (("2" (assert)
                              (("2"
                                (expand "graph")
                                (("2"
                                  (expand "extend")
                                  (("2"
                                    (expand "LPartFun_to_SPartFun")
                                    (("2"
                                      (expand "graph")
                                      (("2"
                                        (assert)
                                        (("2"
                                          (prop)
                                          (("2"
                                            (assert)
                                            (("2"
                                              (lemma
                                               "down_equal"
                                               ("y1"
                                                "f1!1(x!1)"
                                                "y2"
                                                "f2!1(x!1)"))
                                              (("2" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (skosimp)
                    (("2" (skosimp)
                      (("2" (expand "LPartFun_to_SPartFun")
                        (("2" (propax) nil nil)) nil))
                      nil))
                    nil)
                   ("3" (skosimp)
                    (("3" (expand "LPartFun_to_SPartFun")
                      (("3" (propax) nil nil)) nil))
                    nil)
                   ("4" (skosimp)
                    (("4" (skosimp)
                      (("4" (expand "LPartFun_to_SPartFun")
                        (("4" (propax) nil nil)) nil))
                      nil))
                    nil)
                   ("5" (skosimp)
                    (("5" (expand "LPartFun_to_SPartFun")
                      (("5" (propax) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (skosimp) (("2" (replace -1) (("2" (propax) nil nil)) nil))
        nil))
      nil))
    nil)
   ((X formal-type-decl nil partial_function_props nil)
    (Y formal-type-decl nil partial_function_props nil)
    (lift type-decl nil lift_adt nil)
    (LiftPartialFunction type-eq-decl nil PartialFunctionDefinitions
     nil)
    (extend const-decl "R" extend nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (extensionality_postulate formula-decl nil functions nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
    (PRED type-eq-decl nil defined_types nil)
    (SubsetPartialFunction type-eq-decl nil PartialFunctionDefinitions
     nil)
    (graph const-decl "bool" functions nil)
    (down adt-accessor-decl "[(up?) -> T]" lift_adt nil)
    (FALSE const-decl "bool" booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (down_equal formula-decl nil lift_props "orders/")
    (member_graph formula-decl nil partial_function_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bottom? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
    (bottom adt-constructor-decl "(bottom?)" lift_adt nil)
    (LPartFun_to_SPartFun const-decl "SubsetPartialFunction"
     PartialFunctionDefinitions nil)
    (graph const-decl "set[[X, Y]]" partial_function_props nil))
   shostak))
(graph_is_graph? 0
  (graph_is_graph?-1 nil 3353058450
   ("" (skosimp)
    (("" (expand "graph?")
      (("" (skosimp)
        (("" (expand "graph")
          (("" (expand "extend")
            (("" (prop)
              (("" (expand "LPartFun_to_SPartFun")
                (("" (expand "graph")
                  ((""
                    (lemma "down_equal"
                     ("y1" "up(y1!1)" "y2" "up(y2!1)"))
                    (("" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((graph? const-decl "bool" partial_function_props nil)
    (graph const-decl "set[[X, Y]]" partial_function_props nil)
    (graph const-decl "bool" functions nil)
    (down_equal formula-decl nil lift_props "orders/")
    (lift type-decl nil lift_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
    (up adt-constructor-decl "[T -> (up?)]" lift_adt nil)
    (Y formal-type-decl nil partial_function_props nil)
    (LPartFun_to_SPartFun const-decl "SubsetPartialFunction"
     PartialFunctionDefinitions nil)
    (extend const-decl "R" extend nil))
   shostak))
(graph_from_graph 0
  (graph_from_graph-1 nil 3353050512
   ("" (skosimp)
    (("" (typepred "g!1")
      (("" (expand "graph?")
        (("" (expand "from_graph")
          (("" (expand "graph")
            (("" (expand "extend")
              (("" (expand "LPartFun_to_SPartFun")
                (("" (expand "graph")
                  (("" (apply-extensionality 1 :hide? t)
                    (("1" (case-replace "g!1(x!1, x!2)")
                      (("1"
                        (case-replace
                         "{y | g!1(x!1, y)} = singleton(x!2)")
                        (("1" (assert)
                          (("1" (rewrite "choose_singleton")
                            (("1" (rewrite "nonempty_singleton")
                              (("1" (assert) nil nil)) nil))
                            nil))
                          nil)
                         ("2" (hide 2)
                          (("2" (apply-extensionality 1 :hide? t)
                            (("2" (expand "singleton")
                              (("2"
                                (case-replace "x!3=x!2")
                                (("2"
                                  (assert)
                                  (("2"
                                    (inst - "x!1" "x!2" "x!3")
                                    (("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (assert)
                        (("2" (prop)
                          (("2" (lift-if -1)
                            (("2" (assert)
                              (("2"
                                (prop)
                                (("2" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (skosimp)
                      (("2" (lift-if -1) (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((graph? const-decl "bool" partial_function_props nil)
    (set type-eq-decl nil sets nil)
    (Y formal-type-decl nil partial_function_props nil)
    (X formal-type-decl nil partial_function_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (from_graph const-decl "LiftPartialFunction" partial_function_props
     nil)
    (extend const-decl "R" extend nil)
    (graph const-decl "bool" functions nil)
    (nonempty_singleton judgement-tcc nil sets nil)
    (choose_singleton formula-decl nil sets_lemmas nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (bottom adt-constructor-decl "(bottom?)" lift_adt nil)
    (bottom? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
    (choose const-decl "(p)" sets nil)
    (up adt-constructor-decl "[T -> (up?)]" lift_adt nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (every adt-def-decl "boolean" lift_adt nil)
    (PRED type-eq-decl nil defined_types nil)
    (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
    (lift type-decl nil lift_adt nil)
    (g!1 skolem-const-decl "(graph?)" partial_function_props nil)
    (nonempty? const-decl "bool" sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (down adt-accessor-decl "[(up?) -> T]" lift_adt nil)
    (FALSE const-decl "bool" booleans nil)
    (LPartFun_to_SPartFun const-decl "SubsetPartialFunction"
     PartialFunctionDefinitions nil)
    (graph const-decl "set[[X, Y]]" partial_function_props nil))
   shostak))
(from_graph_graph_TCC1 0
  (from_graph_graph_TCC1-1 nil 3353050474
   ("" (skosimp) (("" (rewrite "graph_is_graph?") nil nil)) nil)
   ((graph_is_graph? formula-decl nil partial_function_props nil)
    (X formal-type-decl nil partial_function_props nil)
    (Y formal-type-decl nil partial_function_props nil)
    (lift type-decl nil lift_adt nil)
    (LiftPartialFunction type-eq-decl nil PartialFunctionDefinitions
     nil))
   nil))
(from_graph_graph 0
  (from_graph_graph-1 nil 3353050831
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("" (expand "graph")
        (("" (expand "from_graph")
          (("" (expand "extend")
            (("" (expand "LPartFun_to_SPartFun")
              (("" (expand "graph")
                (("" (lift-if)
                  (("" (case-replace "up?(f!1(x!1))")
                    (("1" (lift-if)
                      (("1" (assert)
                        (("1" (prop)
                          (("1"
                            (lemma "choose_member"
                             ("a" "{y | (down(f!1(x!1)) = y)}"))
                            (("1" (split -1)
                              (("1"
                                (name-replace
                                 "AA"
                                 "choose({y | (down(f!1(x!1)) = y)})")
                                (("1"
                                  (expand "member")
                                  (("1"
                                    (replace -1 1 rl)
                                    (("1" (rewrite "up_down") nil nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (expand "nonempty?")
                                (("2" (propax) nil nil))
                                nil))
                              nil))
                            nil)
                           ("2" (expand "nonempty?")
                            (("2" (expand "empty?")
                              (("2"
                                (expand "member")
                                (("2"
                                  (inst - "down(f!1(x!1))")
                                  nil
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (assert)
                      (("2" (lift-if)
                        (("2" (assert)
                          (("2" (prop)
                            (("2" (expand "nonempty?")
                              (("2"
                                (expand "empty?")
                                (("2"
                                  (skosimp)
                                  (("2"
                                    (expand "member")
                                    (("2" (propax) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((X formal-type-decl nil partial_function_props nil)
    (Y formal-type-decl nil partial_function_props nil)
    (lift type-decl nil lift_adt nil)
    (graph const-decl "set[[X, Y]]" partial_function_props nil)
    (from_graph const-decl "LiftPartialFunction" partial_function_props
     nil)
    (LiftPartialFunction type-eq-decl nil PartialFunctionDefinitions
     nil)
    (graph? const-decl "bool" partial_function_props nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (LPartFun_to_SPartFun const-decl "SubsetPartialFunction"
     PartialFunctionDefinitions nil)
    (empty? const-decl "bool" sets nil)
    (choose_member formula-decl nil sets_lemmas nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (down adt-accessor-decl "[(up?) -> T]" lift_adt nil)
    (choose const-decl "(p)" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (up_down formula-decl nil lift_props "orders/")
    (member const-decl "bool" sets nil)
    (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
    (graph const-decl "bool" functions nil)
    (extend const-decl "R" extend nil))
   shostak)))

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