Quelle function_props_aux.prf Sprache: Lisp

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

quality100%

¤ Dauer der Verarbeitung: 0.22 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.