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

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: non_empty_bounded_sets.pvs   Sprache: Unknown

(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)))


[ zur Elbe Produktseite wechseln0.13Quellennavigators  Analyse erneut starten  ]