Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: coqdep_boot.ml Sprache: Lisp

Original von: PVS^©

(Cont
(sq_le_def 0
  (sq_le_def-1 nil 3353048819
   ("" (skosimp)
    (("" (expand "sq_le")
      (("" (expand "subset?")
        (("" (expand "member")
          (("" (split)
            (("1" (skosimp*)
              (("1" (expand "graph")
                (("1" (expand "extend")
                  (("1" (expand "LPartFun_to_SPartFun")
                    (("1" (expand "graph")
                      (("1" (prop)
                        (("1" (inst - "x!1`1" "x!1`2")
                          (("1" (lemma "up_down" ("y" "c1!1(x!1`1)"))
                            (("1" (lemma "up_down" ("y" "c2!1(x!1`1)"))
                              (("1" (assert) nil nil)) nil))
                            nil))
                          nil)
                         ("2" (inst - "x!1`1" "x!1`2")
                          (("2" (lemma "up_down" ("y" "c1!1(x!1`1)"))
                            (("2" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (skosimp*)
              (("2" (inst - "(s1!1,s2!1)")
                (("2" (expand "graph")
                  (("2" (expand "extend")
                    (("2" (expand "LPartFun_to_SPartFun")
                      (("2" (assert)
                        (("2" (expand "graph")
                          (("2" (replace -2)
                            (("2" (rewrite "down_up")
                              (("2"
                                (prop)
                                (("2"
                                  (replace -2 1 rl)
                                  (("2"
                                    (lemma
                                     "up_down"
                                     ("y" "c2!1(s1!1)"))
                                    (("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sq_le const-decl "bool" Cont nil)
    (member const-decl "bool" sets nil)
    (down_up formula-decl nil lift_props "orders/")
    (extend const-decl "R" extend nil)
    (graph const-decl "bool" functions nil)
    (V formal-nonempty-type-decl nil Cont nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans 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)
    (State nonempty-type-eq-decl nil State nil)
    (Cont nonempty-type-eq-decl nil Cont nil)
    (lift type-decl nil lift_adt nil)
    (up_down formula-decl nil lift_props "orders/")
    (LPartFun_to_SPartFun const-decl "SubsetPartialFunction"
     PartialFunctionDefinitions nil)
    (graph const-decl "set[[X, Y]]" partial_function_props "scott/")
    (subset? const-decl "bool" sets nil))
   shostak))
(partial_order_sq_le 0
  (partial_order_sq_le-1 nil 3353051459
   ("" (expand "partial_order?")
    (("" (expand "preorder?")
      (("" (split)
        (("1" (expand "reflexive?")
          (("1" (skosimp)
            (("1" (rewrite "sq_le_def")
              (("1" (rewrite "subset_reflexive") nil nil)) nil))
            nil))
          nil)
         ("2" (expand "transitive?")
          (("2" (skosimp)
            (("2" (rewrite "sq_le_def")
              (("2" (rewrite "sq_le_def")
                (("2" (rewrite "sq_le_def")
                  (("2" (expand "subset?")
                    (("2" (expand "member")
                      (("2" (skosimp)
                        (("2" (inst - "x!2")
                          (("2" (inst - "x!2") (("2" (assert) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("3" (expand "antisymmetric?")
          (("3" (skosimp)
            (("3" (rewrite "sq_le_def")
              (("3" (rewrite "sq_le_def")
                (("3" (lemma "subset_antisymmetric[[State,State]]")
                  (("3" (inst - "graph(x!1)" "graph(y!1)")
                    (("3" (assert)
                      (("3" (lemma "graph_eq")
                        (("3" (inst - "x!1" "y!1")
                          (("3" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((preorder? const-decl "bool" orders nil)
    (antisymmetric? const-decl "bool" relations nil)
    (subset_antisymmetric formula-decl nil sets_lemmas nil)
    (graph_eq formula-decl nil partial_function_props "scott/")
    (transitive? const-decl "bool" relations nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (reflexive? const-decl "bool" relations nil)
    (sq_le_def formula-decl nil Cont nil)
    (V formal-nonempty-type-decl nil Cont nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans 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)
    (State nonempty-type-eq-decl nil State nil)
    (lift type-decl nil lift_adt nil)
    (Cont nonempty-type-eq-decl nil Cont nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (graph const-decl "set[[X, Y]]" partial_function_props "scott/")
    (LiftPartialFunction type-eq-decl nil PartialFunctionDefinitions
     nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (subset_reflexive formula-decl nil sets_lemmas nil)
    (partial_order? const-decl "bool" orders nil))
   shostak))
(lub_graph_TCC1 0
  (lub_graph_TCC1-1 nil 3353058858 ("" (subtype-tcc) nil nil)
   ((member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (nonempty? const-decl "bool" sets nil))
   nil))
(lub_graph_TCC2 0
  (lub_graph_TCC2-1 nil 3353058858
   ("" (skosimp)
    (("" (split -1)
      (("1" (rewrite "emptyset_is_empty?")
        (("1" (replace -1)
          (("1" (expand "image")
            (("1" (expand "graph?")
              (("1" (skosimp)
                (("1" (expand "Union")
                  (("1" (skosimp)
                    (("1" (skosimp)
                      (("1" (typepred "a!1")
                        (("1" (typepred "a!2")
                          (("1" (skosimp)
                            (("1" (typepred "x!2")
                              (("1"
                                (expand "emptyset")
                                (("1" (propax) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand "graph?")
        (("2" (skosimp)
          (("2" (expand "Union")
            (("2" (skosimp*)
              (("2" (typepred "a!1")
                (("2" (typepred "a!2")
                  (("2" (expand "image")
                    (("2" (skosimp*)
                      (("2" (typepred "x!2")
                        (("2" (typepred "x!3")
                          (("2" (replace -3)
                            (("2" (replace -4)
                              (("2"
                                (hide -3 -4)
                                (("2"
                                  (expand "graph")
                                  (("2"
                                    (expand "extend")
                                    (("2"
                                      (expand "LPartFun_to_SPartFun")
                                      (("2"
                                        (expand "graph")
                                        (("2"
                                          (prop)
                                          (("2"
                                            (expand "directed?")
                                            (("2"
                                              (inst - "x!2" "x!3")
                                              (("2"
                                                (assert)
                                                (("2"
                                                  (skosimp)
                                                  (("2"
                                                    (typepred "z!1")
                                                    (("2"
                                                      (expand "sq_le")
                                                      (("2"
                                                        (inst
                                                         -
                                                         "x!1"
                                                         "y2!1")
                                                        (("2"
                                                          (inst
                                                           -
                                                           "x!1"
                                                           "y1!1")
                                                          (("2"
                                                            (lemma
                                                             "up_down"
                                                             ("y"
                                                              "x!2(x!1)"))
                                                            (("2"
                                                              (lemma
                                                               "up_down"
                                                               ("y"
                                                                "x!3(x!1)"))
                                                              (("2"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((graph? const-decl "bool" partial_function_props "scott/")
    (Union const-decl "set" sets nil)
    (graph const-decl "set[[X, Y]]" partial_function_props "scott/")
    (LiftPartialFunction type-eq-decl nil PartialFunctionDefinitions
     nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (emptyset const-decl "set" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (image const-decl "set[R]" function_image nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (finite_emptyset name-judgement "finite_set[Cont]" Cont nil)
    (Cont nonempty-type-eq-decl nil Cont nil)
    (lift type-decl nil lift_adt nil)
    (State nonempty-type-eq-decl nil State nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (V formal-nonempty-type-decl nil Cont nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (emptyset_is_empty? formula-decl nil sets_lemmas nil)
    (LPartFun_to_SPartFun const-decl "SubsetPartialFunction"
     PartialFunctionDefinitions nil)
    (sq_le const-decl "bool" Cont nil)
    (up_down formula-decl nil lift_props "orders/")
    (directed? const-decl "bool" directed_orders "orders/")
    (graph const-decl "bool" functions nil)
    (extend const-decl "R" extend nil))
   nil))
(lub_graph 0
  (lub_graph-1 nil 3353730711
   ("" (skosimp)
    (("" (case-replace "nonempty?(D!1)")
      (("1" (split -2)
        (("1" (expand "nonempty?") (("1" (propax) nil nil)) nil)
         ("2" (expand "least_upper_bound?")
          (("2" (split)
            (("1" (expand "upper_bound?")
              (("1" (skosimp)
                (("1" (expand "sq_le")
                  (("1" (skosimp)
                    (("1" (expand "from_graph")
                      (("1" (lift-if)
                        (("1" (assert)
                          (("1" (prop)
                            (("1"
                              (case-replace
                               "{y: State | Union(image(graph, D!1))(s1!1, y)} = singleton(s2!1)")
                              (("1"
                                (rewrite "choose_singleton")
                                nil
                                nil)
                               ("2"
                                (hide 2)
                                (("2"
                                  (apply-extensionality 1 :hide? t)
                                  (("2"
                                    (expand "singleton")
                                    (("2"
                                      (case-replace "x!1=s2!1")
                                      (("1"
                                        (typepred "r!1")
                                        (("1"
                                          (expand "Union")
                                          (("1"
                                            (inst + "graph(r!1)")
                                            (("1"
                                              (expand "graph")
                                              (("1"
                                                (expand "extend")
                                                (("1"
                                                  (expand
                                                   "LPartFun_to_SPartFun")
                                                  (("1"
                                                    (expand "graph")
                                                    (("1"
                                                      (replace -4)
                                                      (("1"
                                                        (rewrite
                                                         "down_up")
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (expand "image")
                                              (("2"
                                                (inst + "r!1")
                                                nil
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (assert)
                                        (("2"
                                          (expand "Union")
                                          (("2"
                                            (skosimp)
                                            (("2"
                                              (typepred "a!1")
                                              (("2"
                                                (expand "image")
                                                (("2"
                                                  (skosimp)
                                                  (("2"
                                                    (typepred "x!2")
                                                    (("2"
                                                      (replace -2)
                                                      (("2"
                                                        (hide -2)
                                                        (("2"
                                                          (typepred
                                                           "r!1")
                                                          (("2"
                                                            (expand
                                                             "directed?")
                                                            (("2"
                                                              (inst
                                                               -
                                                               "x!2"
                                                               "r!1")
                                                              (("2"
                                                                (assert)
                                                                (("2"
                                                                  (skosimp)
                                                                  (("2"
                                                                    (expand
                                                                     "graph")
                                                                    (("2"
                                                                      (expand
                                                                       "extend")
                                                                      (("2"
                                                                        (prop)
                                                                        (("2"
                                                                          (expand
                                                                           "graph")
                                                                          (("2"
                                                                            (expand
                                                                             "LPartFun_to_SPartFun")
                                                                            (("2"
                                                                              (replace
                                                                               -2
                                                                               *
                                                                               rl)
                                                                              (("2"
                                                                                (inst
                                                                                 -
                                                                                 "s1!1"
                                                                                 "x!1")
                                                                                (("2"
                                                                                  (inst
                                                                                   -
                                                                                   "s1!1"
                                                                                   "s2!1")
                                                                                  (("2"
                                                                                    (assert)
                                                                                    (("2"
                                                                                      (split
                                                                                       -7)
                                                                                      (("1"
                                                                                        (lemma
                                                                                         "down_equal"
                                                                                         ("y1"
                                                                                          "up(x!1)"
                                                                                          "y2"
                                                                                          "up(s2!1)"))
                                                                                        (("1"
                                                                                          (assert)
                                                                                          nil
                                                                                          nil))
                                                                                        nil)
                                                                                       ("2"
                                                                                        (replace
                                                                                         -2
                                                                                         1
                                                                                         rl)
                                                                                        (("2"
                                                                                          (lemma
                                                                                           "up_down"
                                                                                           ("y"
                                                                                            "x!2(s1!1)"))
                                                                                          (("2"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (expand "nonempty?")
                              (("2"
                                (expand "empty?")
                                (("2"
                                  (skosimp)
                                  (("2"
                                    (expand "member")
                                    (("2"
                                      (inst - "s2!1")
                                      (("2"
                                        (expand "Union")
                                        (("2"
                                          (inst + "graph(r!1)")
                                          (("1"
                                            (expand "graph")
                                            (("1"
                                              (expand "extend")
                                              (("1"
                                                (expand
                                                 "LPartFun_to_SPartFun")
                                                (("1"
                                                  (expand "graph")
                                                  (("1"
                                                    (replace -1)
                                                    (("1"
                                                      (rewrite
                                                       "down_up")
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (expand "image")
                                            (("2"
                                              (inst + "r!1")
                                              nil
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (expand "sq_le")
              (("2" (expand "upper_bound?")
                (("2" (skosimp*)
                  (("2" (expand "from_graph")
                    (("2" (lift-if -2)
                      (("2" (assert)
                        (("2" (prop)
                          (("2" (copy -1)
                            (("2" (expand "nonempty?" -1)
                              (("2"
                                (expand "empty?")
                                (("2"
                                  (expand "member")
                                  (("2"
                                    (skosimp*)
                                    (("2"
                                      (expand "Union" -1)
                                      (("2"
                                        (skosimp)
                                        (("2"
                                          (typepred "a!1")
                                          (("2"
                                            (expand "image" -1)
                                            (("2"
                                              (skosimp)
                                              (("2"
                                                (replace -1)
                                                (("2"
                                                  (typepred "x!2")
                                                  (("2"
                                                    (hide -2)
                                                    (("2"
                                                      (inst -5 "x!2")
                                                      (("2"
                                                        (inst
                                                         -5
                                                         "s1!1"
                                                         "x!1")
                                                        (("2"
                                                          (expand
                                                           "graph"
                                                           -2)
                                                          (("2"
                                                            (expand
                                                             "extend")
                                                            (("2"
                                                              (expand
                                                               "LPartFun_to_SPartFun")
                                                              (("2"
                                                                (prop)
                                                                (("1"
                                                                  (expand
                                                                   "graph"
                                                                   -3)
                                                                  (("1"
                                                                    (case-replace
                                                                     "{y:State|Union(image(graph,D!1))(s1!1,y)} =singleton(x!1)")
                                                                    (("1"
                                                                      (rewrite
                                                                       "choose_singleton")
                                                                      (("1"
                                                                        (assert)
                                                                        nil
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (hide
                                                                       2)
                                                                      (("2"
                                                                        (apply-extensionality
                                                                         1
                                                                         :hide?
                                                                         t)
                                                                        (("2"
                                                                          (expand
                                                                           "singleton")
                                                                          (("2"
                                                                            (case-replace
                                                                             "x!3 = x!1")
                                                                            (("1"
                                                                              (expand
                                                                               "Union")
                                                                              (("1"
                                                                                (inst
                                                                                 +
                                                                                 "graph(x!2)")
                                                                                (("1"
                                                                                  (expand
                                                                                   "graph")
                                                                                  (("1"
                                                                                    (expand
                                                                                     "extend")
                                                                                    (("1"
                                                                                      (expand
                                                                                       "LPartFun_to_SPartFun")
                                                                                      (("1"
                                                                                        (expand
                                                                                         "graph")
                                                                                        (("1"
                                                                                          (propax)
                                                                                          nil
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("2"
                                                                                  (expand
                                                                                   "image")
                                                                                  (("2"
                                                                                    (inst
                                                                                     +
                                                                                     "x!2")
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil)
                                                                             ("2"
                                                                              (assert)
                                                                              (("2"
                                                                                (expand
                                                                                 "Union")
                                                                                (("2"
                                                                                  (skosimp)
                                                                                  (("2"
                                                                                    (typepred
                                                                                     "a!2")
                                                                                    (("2"
                                                                                      (expand
                                                                                       "image")
                                                                                      (("2"
                                                                                        (skosimp)
                                                                                        (("2"
                                                                                          (typepred
                                                                                           "x!4")
                                                                                          (("2"
                                                                                            (replace
                                                                                             -2)
                                                                                            (("2"
                                                                                              (hide
                                                                                               -2)
                                                                                              (("2"
                                                                                                (expand
                                                                                                 "graph")
                                                                                                (("2"
                                                                                                  (expand
                                                                                                   "extend")
                                                                                                  (("2"
                                                                                                    (expand
                                                                                                     "LPartFun_to_SPartFun")
                                                                                                    (("2"
                                                                                                      (expand
                                                                                                       "graph")
                                                                                                      (("2"
                                                                                                        (prop)
                                                                                                        (("2"
                                                                                                          (hide-all-but
                                                                                                           (-1
                                                                                                            -2
                                                                                                            -3
                                                                                                            -5
                                                                                                            -6
                                                                                                            -7
                                                                                                            -10
                                                                                                            1))
                                                                                                          (("2"
                                                                                                            (expand
                                                                                                             "directed?")
                                                                                                            (("2"
                                                                                                              (inst
                                                                                                               -
                                                                                                               "x!2"
                                                                                                               "x!4")
                                                                                                              (("2"
                                                                                                                (assert)
                                                                                                                (("2"
                                                                                                                  (skosimp)
                                                                                                                  (("2"
                                                                                                                    (inst
                                                                                                                     -
                                                                                                                     "s1!1"
                                                                                                                     "x!1")
                                                                                                                    (("2"
                                                                                                                      (inst
                                                                                                                       -
                                                                                                                       "s1!1"
                                                                                                                       "x!3")
                                                                                                                      (("2"
                                                                                                                        (lemma
                                                                                                                         "up_down"
                                                                                                                         ("y"
                                                                                                                          "x!4(s1!1)"))
                                                                                                                        (("2"
                                                                                                                          (lemma
                                                                                                                           "up_down"
                                                                                                                           ("y"
                                                                                                                            "x!2(s1!1)"))
                                                                                                                          (("2"
                                                                                                                            (assert)
                                                                                                                            nil
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (expand
                                                                   "graph")
                                                                  (("2"
                                                                    (lemma
                                                                     "up_down"
                                                                     ("y"
                                                                      "x!2(s1!1)"))
                                                                    (("2"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand "nonempty?")
        (("2" (hide -2)
          (("2"
            (case-replace
             "from_graph(Union(image(graph, D!1))) = lambda (s:State): bottom")
            (("1" (rewrite "emptyset_is_empty?")
              (("1" (replace -2)
                (("1" (hide -1 -2)
                  (("1" (expand "least_upper_bound?")
                    (("1" (expand "upper_bound?")
                      (("1" (expand "sq_le")
                        (("1" (skosimp)
                          (("1" (typepred "r!1")
                            (("1" (expand "emptyset")
                              (("1" (propax) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (hide 2)
              (("2" (apply-extensionality 1 :hide? t)
                (("2" (expand "image")
                  (("2" (expand "Union")
                    (("2" (expand "from_graph")
                      (("2" (lift-if)
                        (("2" (expand "nonempty?")
                          (("2" (expand "empty?")
                            (("2" (prop)
                              (("2"
                                (skosimp)
                                (("2"
                                  (expand "member")
                                  (("2"
                                    (skosimp)
                                    (("2"
                                      (typepred "a!1")
                                      (("2"
                                        (skosimp)
                                        (("2"
                                          (typepred "x!3")
                                          (("2"
                                            (inst - "x!3")
                                            nil
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((V formal-nonempty-type-decl nil Cont nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans 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)
    (State nonempty-type-eq-decl nil State nil)
    (lift type-decl nil lift_adt nil)
    (Cont nonempty-type-eq-decl nil Cont nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (nonempty? const-decl "bool" sets nil)
    (least_upper_bound? const-decl "bool" bounded_orders "orders/")
    (x!2 skolem-const-decl "(D!1)" Cont nil)
    (upper_bound? const-decl "bool" bounded_orders "orders/")
    (sq_le const-decl "bool" Cont nil)
    (from_graph const-decl "LiftPartialFunction" partial_function_props
     "scott/")
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (Union const-decl "set" sets nil)
    (LiftPartialFunction type-eq-decl nil PartialFunctionDefinitions
     nil)
    (image const-decl "set[R]" function_image nil)
    (graph const-decl "set[[X, Y]]" partial_function_props "scott/")
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (choose_singleton formula-decl nil sets_lemmas nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (LPartFun_to_SPartFun const-decl "SubsetPartialFunction"
     PartialFunctionDefinitions nil)
    (down_up formula-decl nil lift_props "orders/")
    (graph const-decl "bool" functions nil)
    (extend const-decl "R" extend nil)
    (r!1 skolem-const-decl "(D!1)" Cont nil)
    (D!1 skolem-const-decl "set[Cont]" Cont nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (up adt-constructor-decl "[T -> (up?)]" lift_adt nil)
    (up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
    (down_equal formula-decl nil lift_props "orders/")
    (up_down formula-decl nil lift_props "orders/")
    (directed? const-decl "bool" directed_orders "orders/")
    (emptyset_is_empty? formula-decl nil sets_lemmas nil)
    (finite_emptyset name-judgement "finite_set[Cont]" Cont nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (emptyset const-decl "set" sets nil)
    (bottom adt-constructor-decl "(bottom?)" lift_adt nil)
    (bottom? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
    (graph? const-decl "bool" partial_function_props "scott/"))
   shostak))
(sq_le_dcpo 0
  (sq_le_dcpo-1 nil 3353053412
   ("" (expand "directed_complete_partial_order?")
    (("" (lemma "partial_order_sq_le")
      (("" (assert)
        (("" (expand "directed_complete?")
          (("" (skosimp)
            (("" (expand "least_bounded_above?")
              (("" (name "G" "Union(image(graph,D!1))")
                (("" (case "graph?(G)")
                  (("1" (inst + "from_graph(G)")
                    (("1" (expand "least_upper_bound?")
                      (("1" (expand "upper_bound?")
                        (("1" (expand "sq_le")
                          (("1" (expand "G")
                            (("1" (expand "from_graph")
                              (("1"
                                (split)
                                (("1"
                                  (skosimp)
                                  (("1"
                                    (skosimp)
                                    (("1"
                                      (lift-if 1)
                                      (("1"
                                        (assert)
                                        (("1"
                                          (prop)
                                          (("1"
                                            (typepred "r!1")
                                            (("1"
                                              (lemma
                                               "down_equal"
                                               ("y1"
                                                "up(choose({y: State | Union(image(graph, D!1))(s1!1, y)}))"
                                                "y2"
                                                "up(s2!1)"))
                                              (("1"
                                                (split -1)
                                                (("1"
                                                  (flatten -1)
                                                  (("1"
                                                    (hide -2)
                                                    (("1"
                                                      (rewrite
                                                       "down_up"
                                                       -1)
                                                      (("1"
                                                        (rewrite
                                                         "down_up"
                                                         -1)
                                                        (("1"
                                                          (split -1)
                                                          (("1"
                                                            (propax)
                                                            nil
                                                            nil)
                                                           ("2"
                                                            (hide 2)
                                                            (("2"
                                                              (lemma
                                                               "choose_singleton"
                                                               ("x"
                                                                "s2!1"))
                                                              (("2"
                                                                (expand
                                                                 "singleton")
                                                                (("2"
                                                                  (case-replace
                                                                   "{y: State | Union(image(graph, D!1))(s1!1, y)} = {y: State | y = s2!1}")
                                                                  (("2"
                                                                    (hide
                                                                     -1
                                                                     2)
                                                                    (("2"
                                                                      (apply-extensionality
                                                                       1
                                                                       :hide?
                                                                       t)
                                                                      (("2"
                                                                        (case-replace
                                                                         "x!1=s2!1")
                                                                        (("1"
                                                                          (expand
                                                                           "Union")
                                                                          (("1"
                                                                            (inst
                                                                             +
                                                                             "graph(r!1)")
                                                                            (("1"
                                                                              (expand
                                                                               "graph")
                                                                              (("1"
                                                                                (expand
                                                                                 "extend")
                                                                                (("1"
                                                                                  (expand
                                                                                   "LPartFun_to_SPartFun")
                                                                                  (("1"
                                                                                    (expand
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.74 Sekunden (vorverarbeitet) ¤

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