products/sources/formale sprachen/PVS/sigma_set/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: Extraction.v   Sprache: PVS

Original von: PVS©
(function_props_aux
 (inverse_image_composition 0
  (inverse_image_composition-1 nil 3449912055
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("" (expand "inverse_image")
        (("" (expand "o ")
          (("" (expand "member") (("" (propax) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((T1 formal-type-decl nil function_props_aux nil)
    (boolean nonempty-type-decl nil booleans nil)
    (O const-decl "T3" function_props nil)
    (T3 formal-type-decl nil function_props_aux nil)
    (inverse_image const-decl "set[D]" function_image nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T2 formal-type-decl nil function_props_aux nil)
    (member const-decl "bool" sets nil))
   shostak))
 (composition_inverse_alt_TCC1 0
  (composition_inverse_alt_TCC1-1 nil 3301539767
   ("" (skosimp)
    (("" (typepred "f1!1")
      (("" (typepred "f2!1")
        (("" (expand "bijective?")
          (("" (flatten)
            (("" (expand "surjective?")
              (("" (skosimp*)
                (("" (inst - "r!1")
                  (("" (skosimp)
                    (("" (inst - "x!1")
                      (("" (skosimp) (("" (inst + "x!2") nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((bijective? const-decl "bool" functions nil)
    (T2 formal-type-decl nil function_props_aux nil)
    (T1 formal-type-decl nil function_props_aux nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (surjective? const-decl "bool" functions nil)
    (T3 formal-type-decl nil function_props_aux nil))
   shostak))
 (composition_inverse_alt_TCC2 0
  (composition_inverse_alt_TCC2-1 nil 3301539767
   ("" (skosimp*)
    (("" (typepred "f1!1")
      (("" (expand "bijective?")
        (("" (expand "surjective?")
          (("" (flatten)
            (("" (inst - "r!1")
              (("" (skosimp) (("" (inst + "x!1") nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((bijective? const-decl "bool" functions nil)
    (T2 formal-type-decl nil function_props_aux nil)
    (T1 formal-type-decl nil function_props_aux nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (surjective? const-decl "bool" functions nil))
   shostak))
 (composition_inverse_alt_TCC3 0
  (composition_inverse_alt_TCC3-1 nil 3301539767
   ("" (skosimp)
    (("" (typepred "f2!1")
      (("" (expand "bijective?")
        (("" (expand "surjective?")
          (("" (flatten)
            (("" (skosimp)
              (("" (inst - "r!1")
                (("" (skosimp) (("" (inst + "x!1") nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((bijective? const-decl "bool" functions nil)
    (T3 formal-type-decl nil function_props_aux nil)
    (T2 formal-type-decl nil function_props_aux nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (surjective? const-decl "bool" functions nil))
   shostak))
 (composition_inverse_alt 0
  (composition_inverse_alt-1 nil 3301540008
   ("" (skosimp)
    (("" (typepred "f1!1")
      (("" (typepred "f2!1")
        (("" (apply-extensionality :hide? t)
          (("1"
            (lemma "composition_bijective[T1,T2,T3]"
             ("f1" "f1!1" "f2" "f2!1"))
            (("1"
              (lemma "unique_bijective_inverse_alt[T1,T3]"
               ("f" "f2!1 o f1!1" "r" "x!1"))
              (("1"
                (lemma "unique_bijective_inverse_alt[T2,T3]"
                 ("f" "f2!1" "r" "x!1"))
                (("1"
                  (lemma "unique_bijective_inverse_alt[T1,T2]"
                   ("f" "f1!1" "r" "inverse_alt(f2!1)(x!1)"))
                  (("1" (expand "o" 1 2)
                    (("1" (expand "bijective?")
                      (("1" (flatten)
                        (("1" (expand "injective?")
                          (("1"
                            (inst - "inverse_alt(f2!1 o f1!1)(x!1)"
                             "inverse_alt(f1!1)(inverse_alt(f2!1)(x!1))")
                            (("1" (split -4)
                              (("1" (propax) nil nil)
                               ("2"
                                (replace -3)
                                (("2"
                                  (expand "o" 1)
                                  (("2"
                                    (replace -1)
                                    (("2"
                                      (replace -2)
                                      (("2" (propax) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (hide-all-but (-8 1))
                              (("2"
                                (expand "surjective?")
                                (("2"
                                  (flatten)
                                  (("2"
                                    (skosimp)
                                    (("2"
                                      (inst - "r!1")
                                      (("2"
                                        (skosimp)
                                        (("2" (inst + "x!2") nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("3" (hide-all-but (1 -6))
                              (("3"
                                (expand "surjective?")
                                (("3"
                                  (skosimp*)
                                  (("3"
                                    (inst - "r!1")
                                    (("3"
                                      (skosimp)
                                      (("3" (inst + "x!2") nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("4" (hide-all-but (-4 1))
                              (("4"
                                (expand "surjective?")
                                (("4"
                                  (skosimp*)
                                  (("4"
                                    (inst - "r!1")
                                    (("4"
                                      (skosimp)
                                      (("4" (inst + "x!2") nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (hide-all-but (-5 1))
                    (("2" (expand "bijective?")
                      (("2" (expand "surjective?")
                        (("2" (flatten)
                          (("2" (skosimp)
                            (("2" (inst - "r!1")
                              (("2"
                                (skosimp)
                                (("2" (inst + "x!2") nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide-all-but (-3 1))
                  (("2" (expand "bijective?")
                    (("2" (expand "surjective?")
                      (("2" (flatten)
                        (("2" (skosimp)
                          (("2" (inst - "r!1")
                            (("2" (skosimp)
                              (("2" (inst + "x!2") nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (hide-all-but (-1 1))
                (("2" (expand "bijective?")
                  (("2" (expand "surjective?")
                    (("2" (flatten)
                      (("2" (skosimp)
                        (("2" (inst - "r!1")
                          (("2" (skosimp)
                            (("2" (inst + "x!2") nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide -2)
            (("2" (expand "bijective?")
              (("2" (expand "surjective?")
                (("2" (flatten)
                  (("2" (skosimp)
                    (("2" (inst - "r!1")
                      (("2" (skosimp) (("2" (inst + "x!1") nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("3" (hide -1)
            (("3" (expand "bijective?")
              (("3" (expand "surjective?")
                (("3" (flatten)
                  (("3" (skosimp)
                    (("3" (inst - "r!1")
                      (("3" (skosimp) (("3" (inst + "x!1") nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("4" (expand "bijective?")
            (("4" (expand "surjective?")
              (("4" (flatten)
                (("4" (skosimp)
                  (("4" (inst - "r!1")
                    (("4" (skosimp)
                      (("4" (inst - "x!1")
                        (("4" (skosimp) (("4" (inst + "x!2") nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((bijective? const-decl "bool" functions nil)
    (T2 formal-type-decl nil function_props_aux nil)
    (T1 formal-type-decl nil function_props_aux nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (O const-decl "T3" function_props nil)
    (inverse_alt const-decl "inverses(f)" function_inverse_alt nil)
    (inverses nonempty-type-eq-decl nil function_inverse_alt nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (unique_bijective_inverse_alt application-judgement
     "{d | f(d) = r}" function_inverse_alt nil)
    (bijective_inverse_alt_is_bijective application-judgement
     "(bijective?[R, D])" function_inverse_alt nil)
    (composition_bijective application-judgement "(bijective?[T1, T3])"
     function_props nil)
    (composition_surjective application-judgement
     "(surjective?[T1, T3])" function_props nil)
    (composition_injective application-judgement "(injective?[T1, T3])"
     function_props nil)
    (unique_bijective_inverse_alt judgement-tcc nil
     function_inverse_alt nil)
    (injective? const-decl "bool" functions nil)
    (composition_bijective judgement-tcc nil function_props nil)
    (T3 formal-type-decl nil function_props_aux nil))
   shostak)))


¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.8Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Begriffe der Konzeptbildung
Was zu einem Entwurf gehört
Begriffe der Konzeptbildung
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff