SSL function_inverse_alt_aux.prf   Interaktion und
PortierbarkeitLisp

(function_inverse_alt_aux
 (inverse_inverse_alt_TCC1 0
  (inverse_inverse_alt_TCC1-1 nil 3301319377
   ("" (skosimp)
    (("" (lemma "inverse_types")
      (("" (split) (("1" (propax) nil nil) ("2" (propax) nil nil))
        nil))
      nil))
    nil)
   ((inverse_types formula-decl nil function_inverse_alt_aux nil))
   shostak))
 (inverse_inverse_alt_TCC2 0
  (inverse_inverse_alt_TCC2-1 nil 3301319377
   ("" (skosimp*) (("" (inst + "f!1(r!1)") nil nil)) nil)
   ((R formal-type-decl nil function_inverse_alt_aux nil)
    (D formal-type-decl nil function_inverse_alt_aux nil))
   shostak))
 (inverse_inverse_alt 0
  (inverse_inverse_alt-1 nil 3301319427
   ("" (skosimp)
    (("" (apply-extensionality :hide? t)
      (("1"
        (lemma "bijective_inverse_alt_is_bijective[D,R]" ("f" "f!1"))
        (("1" (lemma "bijective_inverse_is_inverse_alt[R,D]")
          (("1" (typepred "inverse_alt(f!1)")
            (("1" (inst -2 "inverse_alt(f!1)" "_")
              (("1" (inst - "f!1")
                (("1" (replace -2 * rl) (("1" (propax) nil nil)) nil)
                 ("2" (hide 2)
                  (("2" (name "G" "inverse_alt[D, R](f!1)")
                    (("2" (replace -1)
                      (("2"
                        (lemma "bijective_inverse_alt[D,R]"
                         ("f" "f!1" "g" "G"))
                        (("2" (expand "inverse?")
                          (("2" (skosimp*)
                            (("2" (inst - "r!1" "f!1(r!1)")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (lemma "inverse_types") (("2" (propax) nil nil))
                nil))
              nil))
            nil)
           ("2" (hide-all-but (1 -2))
            (("2" (flatten)
              (("2" (skosimp*) (("2" (inst + "f!1(r!1)") nil nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (lemma "inverse_types") (("2" (propax) nil nil)) nil))
        nil)
       ("2" (flatten)
        (("2" (skosimp*) (("2" (inst + "f!1(r!1)") nil nil)) nil)) nil)
       ("3" (lemma "inverse_types") (("3" (propax) nil nil)) nil))
      nil))
    nil)
   ((D formal-type-decl nil function_inverse_alt_aux nil)
    (R formal-type-decl nil function_inverse_alt_aux 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)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (TRUE const-decl "bool" booleans nil)
    (FALSE const-decl "bool" booleans nil)
    (bijective_inverse_is_inverse_alt formula-decl nil
     function_inverse_alt nil)
    (f!1 skolem-const-decl "[D -> R]" function_inverse_alt_aux nil)
    (bijective_inverse_alt formula-decl nil function_inverse_def nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (inverse_types formula-decl nil function_inverse_alt_aux nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bijective? const-decl "bool" functions nil)
    (bijective_inverse_alt_is_bijective judgement-tcc nil
     function_inverse_alt nil))
   shostak)))