Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: relation_inverse_image.prf Sprache: Lisp

Original von: PVS^©

(relation_inverse_image
(equivClass_is_nonempty 0
  (equivClass_is_nonempty-1 nil 3570861010
   ("" (skolem!)
    (("" (flatten)
      (("" (expand "nonempty?")
        (("" (expand "empty?")
          (("" (inst?)
            (("" (expand "member")
              (("" (expand "equivClass")
                (("" (expand "equivalence?")
                  (("" (prop)
                    (("" (expand "reflexive?")
                      (("" (expand "equivClass")
                        (("" (expand "image_inverse")
                          (("" (inst?) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (equivalence? const-decl "bool" relations nil)
    (reflexive? const-decl "bool" relations nil)
    (image_inverse const-decl "pred[[T, T]]" relation_inverse_image
     nil)
    (U formal-nonempty-type-decl nil relation_inverse_image nil)
    (equivClass const-decl "pred[T]" relation_inverse_image nil)
    (equivClass const-decl "pred[T]" relation_inverse_image nil)
    (T formal-nonempty-type-decl nil relation_inverse_image nil)
    (nonempty? const-decl "bool" sets nil))
   shostak))
(equivClass_equal_is_nonempty 0
  (equivClass_equal_is_nonempty-1 nil 3570861063
   ("" (skolem!)
    (("" (expand "nonempty?")
      (("" (expand "empty?")
        (("" (inst?)
          (("" (expand "member")
            (("" (expand "equivClass")
              (("" (expand "equivClass")
                (("" (expand "image_inverse") (("" (propax) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nonempty? const-decl "bool" sets nil)
    (T formal-nonempty-type-decl nil relation_inverse_image nil)
    (equivClass const-decl "pred[T]" relation_inverse_image nil)
    (image_inverse const-decl "pred[[T, T]]" relation_inverse_image
     nil)
    (equivClass const-decl "pred[T]" relation_inverse_image nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil))
   shostak))
(inverse_image_of_equivalence 0
  (inverse_image_of_equivalence-1 nil 3570452661
   ("" (skolem!)
    (("" (prop)
      (("" (expand "equivalence?")
        (("" (prop)
          (("1" (expand "image_inverse")
            (("1" (expand "reflexive?")
              (("1" (skolem!) (("1" (inst?) nil nil)) nil)) nil))
            nil)
           ("2" (expand "symmetric?")
            (("2" (skolem!)
              (("2" (expand "image_inverse")
                (("2" (inst -2 "f!1(x!1)" "f!1(y!1)") nil nil)) nil))
              nil))
            nil)
           ("3" (expand "transitive?")
            (("3" (skolem!)
              (("3" (expand "image_inverse") (("3" (inst? -3) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((reflexive? const-decl "bool" relations nil)
    (U formal-nonempty-type-decl nil relation_inverse_image nil)
    (T formal-nonempty-type-decl nil relation_inverse_image nil)
    (image_inverse const-decl "pred[[T, T]]" relation_inverse_image
     nil)
    (symmetric? const-decl "bool" relations nil)
    (transitive? const-decl "bool" relations nil)
    (equivalence? const-decl "bool" relations nil))
   shostak))
(preserves_eqv_of_inv_image 0
  (preserves_eqv_of_inv_image-1 nil 3570657993
   ("" (skolem!)
    (("" (inst 1 "=")
      (("" (expand "equivalence?")
        (("" (prop)
          (("1" (expand "reflexive?")
            (("1" (skolem!)
              (("1" (expand "image_inverse") (("1" (propax) nil nil))
                nil))
              nil))
            nil)
           ("2" (expand "symmetric?")
            (("2" (skolem!)
              (("2" (flatten)
                (("2" (expand "image_inverse")
                  (("2" (replace -1 1 :dir rl) (("2" (propax) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("3" (expand "transitive?")
            (("3" (skolem!)
              (("3" (prop)
                (("3" (expand "image_inverse")
                  (("3" (replace -2 1 rl) (("3" (propax) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((U formal-nonempty-type-decl nil relation_inverse_image nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (image_inverse const-decl "pred[[T, T]]" relation_inverse_image
     nil)
    (reflexive? const-decl "bool" relations nil)
    (symmetric? const-decl "bool" relations nil)
    (transitive? const-decl "bool" relations nil)
    (equivalence? const-decl "bool" relations nil))
   shostak))
(inverse_image_of_equality 0
  (inverse_image_of_equality-1 nil 3570452710
   ("" (skolem!)
    (("" (expand "equivalence?")
      (("" (prop)
        (("1" (expand "reflexive?")
          (("1" (skolem!)
            (("1" (expand "image_inverse") (("1" (propax) nil nil))
              nil))
            nil))
          nil)
         ("2" (expand "symmetric?")
          (("2" (skolem!)
            (("2" (prop)
              (("2" (expand "image_inverse")
                (("2" (replace -1 1 :dir rl) (("2" (propax) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("3" (expand "transitive?")
          (("3" (skolem!)
            (("3" (prop)
              (("3" (expand "image_inverse")
                (("3" (replace -2 1 :dir rl) (("3" (propax) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((equivalence? const-decl "bool" relations nil)
    (transitive? const-decl "bool" relations nil)
    (symmetric? const-decl "bool" relations nil)
    (reflexive? const-decl "bool" relations nil)
    (image_inverse const-decl "pred[[T, T]]" relation_inverse_image
     nil))
   shostak))
(image_inverse_eq_is_eq_kernel 0
  (image_inverse_eq_is_eq_kernel-1 nil 3570525503
   ("" (skolem!)
    (("" (apply-extensionality :hide? t)
      (("" (iff)
        (("" (prop)
          (("1" (expand "EquivalenceKernel")
            (("1" (expand "image_inverse")
              (("1" (expand "image_inverse") (("1" (propax) nil nil))
                nil))
              nil))
            nil)
           ("2" (expand "image_inverse")
            (("2" (expand "EquivalenceKernel")
              (("2" (expand "image_inverse") (("2" (propax) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-nonempty-type-decl nil relation_inverse_image nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (image_inverse const-decl "pred[[T, T]]" relation_inverse_image
     nil)
    (pred type-eq-decl nil defined_types nil)
    (EquivalenceKernel const-decl "equivalence[X1]" KernelDefinition
     nil)
    (equivalence type-eq-decl nil relations nil)
    (equivalence? const-decl "bool" relations nil)
    (U formal-nonempty-type-decl nil relation_inverse_image nil)
    (image_inverse const-decl "pred[[T, T]]" relation_inverse_image
     nil))
   shostak))
(inv_img_surj_impl_codom_eq 0
  (inv_img_surj_impl_codom_eq-1 nil 3570458696
   ("" (skolem-typepred)
    (("" (skolem!)
      (("" (flatten)
        (("" (expand "surjective?")
          (("" (expand "equivalence?")
            (("" (prop)
              (("1" (expand "reflexive?")
                (("1" (skolem!)
                  (("1" (inst?)
                    (("1" (skolem!)
                      (("1" (inst?)
                        (("1" (expand "image_inverse")
                          (("1" (replace -1 1 rl)
                            (("1" (propax) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (expand "symmetric?")
                (("2" (skolem!)
                  (("2" (inst-cp -1 "x!1")
                    (("2" (inst -1 "y!1")
                      (("2" (skolem!)
                        (("2" (skolem!)
                          (("2" (replace -1 1 rl)
                            (("2" (replace -2 1 rl)
                              (("2"
                                (inst -4 "x!3" "x!2")
                                (("2"
                                  (expand "image_inverse")
                                  (("2" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("3" (expand "transitive?")
                (("3" (skolem!)
                  (("3" (inst-cp -1 "x!1")
                    (("3" (inst-cp -1 "y!1")
                      (("3" (inst -1 "z!1")
                        (("3" (skolem!)
                          (("3" (skolem!)
                            (("3" (skolem!)
                              (("3"
                                (replace -1 1 rl)
                                (("3"
                                  (replace -2 1 rl)
                                  (("3"
                                    (replace -3 1 rl)
                                    (("3"
                                      (inst -6 "x!4" "x!3" "x!2")
                                      (("3"
                                        (expand "image_inverse")
                                        (("3" (propax) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((equivalence? const-decl "bool" relations nil)
    (transitive? const-decl "bool" relations nil)
    (symmetric? const-decl "bool" relations nil)
    (reflexive? const-decl "bool" relations nil)
    (image_inverse const-decl "pred[[T, T]]" relation_inverse_image
     nil)
    (surjective? const-decl "bool" functions nil)
    (U formal-nonempty-type-decl nil relation_inverse_image nil)
    (T formal-nonempty-type-decl nil relation_inverse_image nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
(right_inv_inv_finv_image_impl_codom_eq 0
  (right_inv_inv_finv_image_impl_codom_eq-1 nil 3570899897
   ("" (skolem!)
    (("" (prop)
      (("" (expand "equivalence?")
        (("" (prop)
          (("1" (expand "reflexive?")
            (("1" (skolem!)
              (("1" (expand "right_inverse?")
                (("1" (inst?)
                  (("1" (expand "image_inverse")
                    (("1" (replace -1 1 rl) (("1" (inst?) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (expand "symmetric?")
            (("2" (skolem!)
              (("2" (expand "right_inverse?")
                (("2" (inst-cp -1 "x!1")
                  (("2" (inst -1 "y!1")
                    (("2" (replace -1 1 rl)
                      (("2" (replace -2 1 rl)
                        (("2" (expand "image_inverse")
                          (("2" (expand "inverse")
                            (("2"
                              (inst -4
                               "(epsilon! (x: T): f!1(x) = x!1)"
                               "(epsilon! (x: T): f!1(x) = y!1)")
                              nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("3" (expand "transitive?")
            (("3" (skolem!)
              (("3" (expand "right_inverse?")
                (("3" (inst-cp -1 "x!1")
                  (("3" (inst-cp -1 "y!1")
                    (("3" (inst -1 "z!1")
                      (("3" (replace -1 1 rl)
                        (("3" (replace -2 1 rl)
                          (("3" (replace -3 1 rl)
                            (("3" (expand "image_inverse")
                              (("3"
                                (expand "inverse")
                                (("3"
                                  (inst
                                   -6
                                   "(epsilon! (x: T): f!1(x) = x!1)"
                                   "(epsilon! (x: T): f!1(x) = y!1)"
                                   "(epsilon! (x: T): f!1(x) = z!1)")
                                  nil
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((U formal-nonempty-type-decl nil relation_inverse_image nil)
    (inverse const-decl "D" function_inverse nil)
    (T formal-nonempty-type-decl nil relation_inverse_image nil)
    (image_inverse const-decl "pred[[T, T]]" relation_inverse_image
     nil)
    (right_inverse? const-decl "bool" function_inverse_def nil)
    (reflexive? const-decl "bool" relations nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (epsilon const-decl "T" epsilons nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (symmetric? const-decl "bool" relations nil)
    (transitive? const-decl "bool" relations nil)
    (equivalence? const-decl "bool" relations nil))
   shostak))
(surjective_eqv_image_inv_rel_codomain 0
  (surjective_eqv_image_inv_rel_codomain-1 nil 3570659487
   ("" (skolem-typepred)
    (("" (iff)
      (("" (split)
        (("1" (use "inv_img_surj_impl_codom_eq")
          (("1" (prop)
            (("1" (expand "image_inverse")
              (("1" (expand "image_inverse") (("1" (propax) nil nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (use "inverse_image_of_equivalence")
          (("2" (prop)
            (("2" (expand "image_inverse")
              (("2" (expand "image_inverse") (("2" (propax) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((inverse_image_of_equivalence formula-decl nil
     relation_inverse_image nil)
    (inv_img_surj_impl_codom_eq formula-decl nil relation_inverse_image
     nil)
    (pred type-eq-decl nil defined_types nil)
    (image_inverse const-decl "pred[[T, T]]" relation_inverse_image
     nil)
    (image_inverse const-decl "pred[[T, T]]" relation_inverse_image
     nil)
    (surjective? const-decl "bool" functions nil)
    (U formal-nonempty-type-decl nil relation_inverse_image nil)
    (T formal-nonempty-type-decl nil relation_inverse_image nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
(right_inv_inv_finv_image_eq_codom_eq 0
  (right_inv_inv_finv_image_eq_codom_eq-1 nil 3570901557
   ("" (skolem!)
    (("" (flatten)
      (("" (iff)
        (("" (prop)
          (("1" (use " inv_img_surj_impl_codom_eq")
            (("1" (prop) nil nil)
             ("2" (expand "surjective?")
              (("2" (expand "right_inverse?")
                (("2" (skolem!)
                  (("2" (inst? -2)
                    (("2" (inst 1 "inverse(f!1)(y!1)") nil nil)) nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (expand "equivalence?")
            (("2" (prop)
              (("1" (expand "reflexive?")
                (("1" (skolem!)
                  (("1" (expand "image_inverse")
                    (("1" (inst?) nil nil)) nil))
                  nil))
                nil)
               ("2" (expand "symmetric?")
                (("2" (skolem!)
                  (("2" (expand "image_inverse")
                    (("2" (inst -2 "f!1(x!1)" "f!1(y!1)") nil nil))
                    nil))
                  nil))
                nil)
               ("3" (expand "transitive?")
                (("3" (skolem!)
                  (("3" (expand "image_inverse")
                    (("3" (inst -3 "f!1(x!1)" "f!1(y!1)" "f!1(z!1)")
                      nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((inverse const-decl "D" function_inverse nil)
    (right_inverse? const-decl "bool" function_inverse_def nil)
    (f!1 skolem-const-decl "[T -> U]" relation_inverse_image nil)
    (surjective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (U formal-nonempty-type-decl nil relation_inverse_image nil)
    (T formal-nonempty-type-decl nil relation_inverse_image nil)
    (pred type-eq-decl nil defined_types nil)
    (inv_img_surj_impl_codom_eq formula-decl nil relation_inverse_image
     nil)
    (image_inverse const-decl "pred[[T, T]]" relation_inverse_image
     nil)
    (reflexive? const-decl "bool" relations nil)
    (symmetric? const-decl "bool" relations nil)
    (transitive? const-decl "bool" relations nil)
    (equivalence? const-decl "bool" relations nil))
   shostak)))

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