Quelle  sigma_bijection.prf

(sigma_bijection
 (sigma_bijection_TCC1 0
  (sigma_bijection_TCC1-1 nil 3322649560
   ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   shostak))
 (sigma_bijection_TCC2 0
  (sigma_bijection_TCC2-1 nil 3322910536
   ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   shostak))
 (sigma_bijection_TCC3 0
  (sigma_bijection_TCC3-1 nil 3322910537
   ("" (skosimp*)
    ((""
      (lemma "connected_domain" ("x" "low!1" "y" "high!1" "z" "z!1"))
      (("" (assert) nil nil)) nil))
    nil)
   ((integer nonempty-type-from-decl nil integers nil)
    (T formal-subtype-decl nil sigma_bijection nil)
    (T_pred const-decl "[int -> boolean]" sigma_bijection nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (connected_domain formula-decl nil sigma_bijection nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   shostak))
 (sigma_bijection 0
  (sigma_bijection-1 nil 3322649953
   (""
    (case "forall (n:nat,F:[below[n+1]->real],phi:(bijective?[below[n+1],below[n+1]])): sigma[below[n+1]](0,n,F)=sigma[below[n+1]](0,n,F o phi)")
    (("1" (skosimp)
      (("1" (skosimp)
        (("1" (typepred "phi!1")
          (("1" (name "N" "high!1-low!1")
            (("1"
              (name "PHI"
                    "LAMBDA (n:below[N+1]): phi!1(n+low!1)-low!1")
              (("1"
                (name "FF" "LAMBDA (n: below[N + 1]): F!1(n+low!1)")
                (("1" (inst - "N" "FF" "PHI")
                  (("1" (hide -1 -2 -3 -4)
                    (("1"
                      (case "forall (n:nat): n <= N => sigma[below[1 + N]](0,n,FF)=sigma[subrange_T(low!1, high!1)]
          (low!1, low!1+n,
           restrict[T, subrange_T(low!1, high!1), real](F!1))")
                      (("1" (inst - "N")
                        (("1" (assert)
                          (("1" (replace -1 -2)
                            (("1" (hide -1)
                              (("1"
                                (expand "N" -1 1)
                                (("1"
                                  (replace -1)
                                  (("1"
                                    (hide -1)
                                    (("1"
                                      (case
                                       "forall (n:nat): n <= N => sigma[below[1 + N]](0, n, FF o PHI) =
       sigma[subrange_T(low!1, high!1)](low!1, low!1+n, F!1 o phi!1)")
                                      (("1"
                                        (inst - "N")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (replace -1)
                                            (("1"
                                              (expand "N")
                                              (("1" (propax) nil nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (assert)
                                          (("2"
                                            (expand "N")
                                            (("2" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (hide 2)
                                        (("2"
                                          (induct "n")
                                          (("1"
                                            (flatten)
                                            (("1"
                                              (expand "sigma")
                                              (("1"
                                                (expand "o")
                                                (("1"
                                                  (expand "PHI")
                                                  (("1"
                                                    (expand "FF")
                                                    (("1"
                                                      (expand "sigma")
                                                      (("1"
                                                        (propax)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (skosimp*)
                                            (("2"
                                              (assert)
                                              (("2"
                                                (expand "sigma" 1)
                                                (("2"
                                                  (replace -1 1 rl)
                                                  (("2"
                                                    (assert)
                                                    (("2"
                                                      (hide -1)
                                                      (("2"
                                                        (expand "PHI")
                                                        (("2"
                                                          (expand "FF")
                                                          (("2"
                                                            (expand
                                                             "o ")
                                                            (("2"
                                                              (propax)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("3"
                                            (skosimp*)
                                            (("3"
                                              (expand "N")
                                              (("3"
                                                (assert)
                                                (("3"
                                                  (lemma
                                                   "connected_domain"
                                                   ("x"
                                                    "low!1"
                                                    "y"
                                                    "high!1"
                                                    "z"
                                                    "z!1"))
                                                  (("3"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("4"
                                            (skosimp*)
                                            (("4"
                                              (expand "N")
                                              (("4"
                                                (lemma
                                                 "connected_domain"
                                                 ("x"
                                                  "low!1"
                                                  "y"
                                                  "high!1"
                                                  "z"
                                                  "n!2+low!1"))
                                                (("4"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("5"
                                            (skosimp*)
                                            (("5" (assert) nil nil))
                                            nil)
                                           ("6"
                                            (skosimp*)
                                            (("6"
                                              (expand "PHI")
                                              (("6"
                                                (expand "N")
                                                (("6"
                                                  (assert)
                                                  (("6"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("7"
                                            (skosimp*)
                                            (("7" (assert) nil nil))
                                            nil)
                                           ("8"
                                            (skosimp*)
                                            (("8" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("3"
                                        (skosimp)
                                        (("3"
                                          (expand "N")
                                          (("3"
                                            (lemma
                                             "connected_domain"
                                             ("x"
                                              "low!1"
                                              "y"
                                              "high!1"
                                              "z"
                                              "n!1+low!1"))
                                            (("3" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("4"
                                        (skosimp)
                                        (("4"
                                          (expand "N")
                                          (("4" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (expand "N") (("2" (assert) nil nil))
                          nil))
                        nil)
                       ("2" (hide 2)
                        (("2" (induct "n")
                          (("1" (assert)
                            (("1" (flatten)
                              (("1"
                                (expand "sigma")
                                (("1"
                                  (expand "restrict")
                                  (("1"
                                    (expand "FF")
                                    (("1"
                                      (expand "sigma")
                                      (("1" (propax) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (skosimp*)
                            (("2" (assert)
                              (("2"
                                (expand "sigma" 1)
                                (("2"
                                  (replace -1)
                                  (("2"
                                    (assert)
                                    (("2"
                                      (expand "restrict")
                                      (("2"
                                        (expand "FF")
                                        (("2" (propax) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("3" (skosimp*)
                            (("3" (assert)
                              (("3"
                                (lemma
                                 "connected_domain"
                                 ("x" "low!1" "y" "high!1" "z" "z!1"))
                                (("3" (assert) nil nil))
                                nil))
                              nil))
                            nil)
                           ("4" (skosimp*)
                            (("4" (expand "N")
                              (("4"
                                (lemma
                                 "connected_domain"
                                 ("x"
                                  "low!1"
                                  "y"
                                  "high!1"
                                  "z"
                                  "n!2+low!1"))
                                (("4" (assert) nil nil))
                                nil))
                              nil))
                            nil)
                           ("5" (skosimp) nil nil)
                           ("6" (skosimp*) (("6" (assert) nil nil))
                            nil)
                           ("7" (skosimp*) (("7" (assert) nil nil))
                            nil))
                          nil))
                        nil)
                       ("3" (skosimp*)
                        (("3"
                          (lemma "connected_domain"
                           ("x" "low!1" "y" "high!1" "z" "z!1"))
                          (("3" (assert) nil nil)) nil))
                        nil)
                       ("4" (skosimp)
                        (("4" (expand "N")
                          (("4"
                            (lemma "connected_domain"
                             ("x" "low!1" "y" "high!1" "z"
                              "n!1+low!1"))
                            (("4" (assert) nil nil)) nil))
                          nil))
                        nil)
                       ("5" (skosimp*)
                        (("5" (expand "N")
                          (("5" (assert)
                            (("5" (typepred "y!1")
                              (("5"
                                (expand "N")
                                (("5" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("6" (skosimp)
                        (("6" (expand "N") (("6" (assert) nil nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (hide 2)
                    (("2" (split 1)
                      (("1" (skosimp)
                        (("1" (expand "PHI")
                          (("1" (expand "N")
                            (("1" (assert)
                              (("1"
                                (typepred "x1!1")
                                (("1"
                                  (typepred "phi!1(low!1+x1!1)")
                                  (("1" (assert) nil nil)
                                   ("2"
                                    (expand "N")
                                    (("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (hide -1 -2 -3)
                        (("2" (expand "bijective?")
                          (("2" (flatten)
                            (("2" (expand "PHI")
                              (("2"
                                (split)
                                (("1"
                                  (expand "injective?")
                                  (("1"
                                    (skosimp)
                                    (("1"
                                      (inst
                                       -
                                       "x1!1 + low!1"
                                       "x2!1 + low!1")
                                      (("1" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (expand "surjective?")
                                  (("2"
                                    (skosimp)
                                    (("2"
                                      (inst - "y!1+low!1")
                                      (("1"
                                        (skosimp)
                                        (("1"
                                          (typepred "x!1")
                                          (("1"
                                            (inst + "x!1-low!1")
                                            (("1" (assert) nil nil)
                                             ("2"
                                              (expand "N")
                                              (("2" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (lemma
                                         "connected_domain"
                                         ("x"
                                          "low!1"
                                          "y"
                                          "high!1"
                                          "z"
                                          "low!1+y!1"))
                                        (("2"
                                          (assert)
                                          (("2"
                                            (typepred "y!1")
                                            (("2"
                                              (expand "N")
                                              (("2" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("3" (expand "N") (("3" (assert) nil nil)) nil))
                  nil)
                 ("2" (skosimp)
                  (("2"
                    (lemma "connected_domain"
                     ("x" "low!1" "y" "high!1" "z" "n!1+low!1"))
                    (("2" (assert) nil nil)) nil))
                  nil))
                nil)
               ("2" (skosimp)
                (("2" (typepred "n!1")
                  (("2" (replace -2 -1 rl)
                    (("2"
                      (lemma "connected_domain"
                       ("x" "low!1" "y" "high!1" "z" "n!1+low!1"))
                      (("2" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil)
               ("3" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (hide 2)
      (("2"
        (case "FORALL (n: nat, F: [nat -> real],
              phi: (bijective?[below[n + 1], below[n + 1]])):
        sigma[nat](0, n, F) = sigma[nat](0, n, F o (LAMBDA (i:nat): IF i < n+1 THEN phi(i) ELSE i ENDIF))")
        (("1" (skosimp)
          (("1" (inst - "n!1" "_" "phi!1")
            (("1"
              (inst -
               "LAMBDA (n:nat): IF n < 1+n!1 THEN F!1(n) ELSE 0 ENDIF")
              (("1" (expand "o")
                (("1"
                  (case "forall (i:nat): i <= n!1 => sigma[nat]
          (0, i,
           LAMBDA (n: nat): IF n < 1 + n!1 THEN F!1(n) ELSE 0 ENDIF) = sigma[below[1 + n!1]](0, i, F!1)")
                  (("1" (inst - "n!1")
                    (("1" (assert)
                      (("1" (replace -1)
                        (("1" (replace -2)
                          (("1" (hide -1 -2)
                            (("1"
                              (case "forall (i:nat): i <= n!1 => sigma[nat]
          (0, i,
           LAMBDA (x: nat):
             IF IF x < 1 + n!1 THEN phi!1(x) ELSE x ENDIF < 1 + n!1
               THEN IF x < 1 + n!1 THEN F!1(phi!1(x)) ELSE F!1(x) ENDIF
             ELSE 0
             ENDIF)
       =
       sigma[below[1 + n!1]]
           (0, i, LAMBDA (x: below[1 + n!1]): F!1(phi!1(x)))")
                              (("1"
                                (inst - "n!1")
                                (("1" (assert) nil nil))
                                nil)
                               ("2"
                                (hide 2)
                                (("2"
                                  (induct "i")
                                  (("1"
                                    (assert)
                                    (("1"
                                      (expand "sigma")
                                      (("1"
                                        (typepred "phi!1(0)")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (expand "sigma")
                                            (("1" (propax) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (skosimp*)
                                    (("2"
                                      (assert)
                                      (("2"
                                        (expand "sigma" 1)
                                        (("2"
                                          (replace -1)
                                          (("2"
                                            (hide -1)
                                            (("2"
                                              (typepred
                                               "phi!1(1 + j!1)")
                                              (("2" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("3"
                                    (skosimp)
                                    (("3"
                                      (assert)
                                      (("3"
                                        (skosimp*)
                                        (("3" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("4"
                                    (skosimp)
                                    (("4" (assert) nil nil))
                                    nil)
                                   ("5"
                                    (skosimp*)
                                    (("5" (assert) nil nil))
                                    nil)
                                   ("6"
                                    (skosimp*)
                                    (("6" (assert) nil nil))
                                    nil))
                                  nil))
                                nil)
                               ("3"
                                (skosimp*)
                                (("3" (assert) nil nil))
                                nil)
                               ("4"
                                (hide 2)
                                (("4"
                                  (skosimp*)
                                  (("4" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (hide-all-but 1)
                    (("2" (induct "i")
                      (("1" (assert)
                        (("1" (expand "sigma")
                          (("1" (expand "sigma")
                            (("1" (propax) nil nil)) nil))
                          nil))
                        nil)
                       ("2" (skosimp*)
                        (("2" (expand "sigma" 1)
                          (("2" (assert) nil nil)) nil))
                        nil)
                       ("3" (skosimp)
                        (("3" (assert)
                          (("3" (skosimp*) (("3" (assert) nil nil))
                            nil))
                          nil))
                        nil)
                       ("4" (skosimp*) (("4" (assert) nil nil)) nil)
                       ("5" (skosimp*) (("5" (assert) nil nil)) nil))
                      nil))
                    nil)
                   ("3" (skosimp)
                    (("3" (skosimp) (("3" (assert) nil nil)) nil)) nil)
                   ("4" (skosimp) (("4" (assert) nil nil)) nil)
                   ("5" (skosimp)
                    (("5" (skosimp) (("5" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (hide 2)
          (("2" (induct "n")
            (("1" (skosimp)
              (("1" (expand "sigma")
                (("1" (expand "o")
                  (("1" (typepred "phi!1(0)")
                    (("1" (assert)
                      (("1" (expand "sigma") (("1" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (skosimp*)
              (("2" (expand "sigma" 1)
                (("2" (expand "o")
                  (("2" (case "phi!1(1+j!1)<= 1+j!1")
                    (("1" (expand "<=" -1)
                      (("1" (split -1)
                        (("1" (typepred "phi!1")
                          (("1"
                            (lemma
                             "surjective_inverse_exists[below[2 + j!1], below[2 + j!1]]"
                             ("f" "phi!1"))
                            (("1" (skosimp)
                              (("1"
                                (lemma
                                 "bij_inv_is_bij_alt[below[2 + j!1], below[2 + j!1]]"
                                 ("f" "phi!1" "g" "g!1"))
                                (("1"
                                  (case "g!1(1+j!1)<1+j!1")
                                  (("1"
                                    (name
                                     "PHI"
                                     "LAMBDA (n:below[1+j!1]): IF n = g!1(1+j!1) THEN phi!1(1+j!1) ELSE phi!1(n) ENDIF")
                                    (("1"
                                      (case
                                       "bijective?[below[1 + j!1], below[1 + j!1]](PHI)")
                                      (("1"
                                        (case
                                         "PHI(g!1(1+j!1)) = phi!1(1+j!1)")
                                        (("1"
                                          (name
                                           "FF"
                                           "LAMBDA (n:nat): IF n = phi!1(1 + j!1) THEN F!1(1 + j!1)  ELSE F!1(n) ENDIF")
                                          (("1"
                                            (inst - "FF" "PHI")
                                            (("1"
                                              (lemma
                                               "sigma_with[nat]"
                                               ("low"
                                                "0"
                                                "high"
                                                "j!1"
                                                "F"
                                                "F!1"
                                                "G"
                                                "FF"
                                                "i"
                                                "phi!1(1+j!1)"
                                                "a"
                                                "F!1(phi!1(1 + j!1))"))
                                              (("1"
                                                (split -1)
                                                (("1"
                                                  (replace -1)
                                                  (("1"
                                                    (assert)
                                                    (("1"
                                                      (replace -11 1)
                                                      (("1"
                                                        (hide -1 -11)
                                                        (("1"
                                                          (assert)
                                                          (("1"
                                                            (expand
                                                             "FF"
                                                             1
                                                             3)
                                                            (("1"
                                                              (lemma
                                                               "sigma_eq[nat]"
                                                               ("low"
                                                                "0"
                                                                "high"
                                                                "j!1"
                                                                "F"
                                                                "LAMBDA (x: nat):
             IF x < 1 + j!1 THEN FF(PHI(x)) ELSE FF(x) ENDIF"
                                                                "G"
                                                                "LAMBDA (x: nat):
               IF x < 2 + j!1 THEN F!1(phi!1(x)) ELSE F!1(x) ENDIF"))
                                                              (("1"
                                                                (split
                                                                 -1)
                                                                (("1"
                                                                  (propax)
                                                                  nil
                                                                  nil)
                                                                 ("2"
                                                                  (hide
                                                                   -1
                                                                   -4
                                                                   2)
                                                                  (("2"
                                                                    (skosimp)
                                                                    (("2"
                                                                      (typepred
                                                                       "n!1")
                                                                      (("2"
                                                                        (assert)
                                                                        (("2"
                                                                          (expand
                                                                           "PHI")
                                                                          (("2"
                                                                            (expand
                                                                             "FF")
                                                                            (("2"
                                                                              (lift-if
                                                                               1)
                                                                              (("2"
                                                                                (case-replace
                                                                                 "n!1 = g!1(1 + j!1)")
                                                                                (("1"
                                                                                  (assert)
                                                                                  (("1"
                                                                                    (lemma
                                                                                     "comp_inverse_right_surj_alt[below[2 + j!1], below[2 + j!1]]"
                                                                                     ("f"
                                                                                      "phi!1"
                                                                                      "g"
                                                                                      "g!1"
                                                                                      "r"
                                                                                      "1+j!1"))
                                                                                    (("1"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("2"
                                                                                  (assert)
                                                                                  (("2"
                                                                                    (case-replace
                                                                                     "phi!1(n!1) = phi!1(1 + j!1)")
                                                                                    (("1"
                                                                                      (expand
                                                                                       "bijective?")
                                                                                      (("1"
                                                                                        (flatten)
                                                                                        (("1"
                                                                                          (expand
                                                                                           "injective?")
                                                                                          (("1"
                                                                                            (inst
                                                                                             -10
                                                                                             "n!1"
                                                                                             "1+j!1")
                                                                                            (("1"
                                                                                              (assert)
                                                                                              nil
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil)
                                                                                     ("2"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2" (assert) nil nil)
                                                 ("3" (assert) nil nil)
                                                 ("4"
                                                  (hide 2 -1 -4 -10)
                                                  (("4"
                                                    (apply-extensionality
                                                     1
                                                     :hide?
                                                     t)
                                                    (("4"
                                                      (case-replace
                                                       "x!1=phi!1(1 + j!1)")
                                                      (("1"
                                                        (assert)
                                                        nil
                                                        nil)
                                                       ("2"
                                                        (assert)
                                                        (("2"
                                                          (expand "FF")
                                                          (("2"
                                                            (propax)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (skosimp)
                                                (("2"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (hide 2 -8)
                                          (("2"
                                            (expand "PHI")
                                            (("2" (propax) nil nil))
                                            nil))
                                          nil)
                                         ("3" (propax) nil nil))
                                        nil)
                                       ("2"
                                        (hide-all-but
                                         (-2 -3 -4 -5 -6 1))
                                        (("2"
                                          (expand "bijective?")
                                          (("2"
                                            (flatten)
                                            (("2"
                                              (split)
                                              (("1"
                                                (expand "injective?")
                                                (("1"
                                                  (skosimp)
                                                  (("1"
                                                    (expand "PHI")
                                                    (("1"
                                                      (case-replace
                                                       "x1!1 = g!1(1 + j!1)")
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (inst
                                                           -7
                                                           "1+j!1"
                                                           "x2!1")
                                                          (("1"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (assert)
                                                        (("2"
                                                          (case-replace
                                                           "x2!1 = g!1(1 + j!1)")
                                                          (("1"
                                                            (inst
                                                             -7
                                                             "x1!1"
                                                             "1+j!1")
                                                            (("1"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (assert)
                                                            (("2"
                                                              (inst
                                                               -6
                                                               "x1!1"
                                                               "x2!1")
                                                              (("2"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (expand "surjective?")
                                                (("2"
                                                  (expand "PHI")
                                                  (("2"
                                                    (skosimp)
                                                    (("2"
                                                      (typepred "y!1")
                                                      (("2"
                                                        (inst -7 "y!1")
                                                        (("2"
                                                          (skosimp)
                                                          (("2"
                                                            (typepred
                                                             "x!1")
                                                            (("2"
                                                              (case-replace
                                                               "x!1=g!1(1+j!1)")
                                                              (("1"
                                                                (inst
                                                                 +
                                                                 "x!1")
                                                                (("1"
                                                                  (assert)
                                                                  (("1"
                                                                    (lemma
                                                                     "comp_inverse_right_surj_alt[below[2 + j!1],below[2 + j!1]]"
                                                                     ("f"
                                                                      "phi!1"
                                                                      "g"
                                                                      "g!1"
                                                                      "r"
                                                                      "1+j!1"))
                                                                    (("1"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (case
                                                                 "x!1=1+j!1")
                                                                (("1"
                                                                  (replace
                                                                   -1)
                                                                  (("1"
                                                                    (hide
                                                                     -1
                                                                     -2)
                                                                    (("1"
                                                                      (inst
                                                                       +
                                                                       "g!1(1 + j!1)")
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (inst
                                                                   +
                                                                   "x!1")
                                                                  (("1"
                                                                    (assert)
                                                                    nil
                                                                    nil)
                                                                   ("2"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("3"
                                        (hide-all-but
                                         (-2 -6 -3 -4 -5 1))
                                        (("3"
                                          (skosimp)
                                          (("3"
                                            (typepred "x1!1")
                                            (("3"
                                              (expand "PHI")
                                              (("3"
                                                (case-replace
                                                 "x1!1 = g!1(1 + j!1)")
                                                (("3"
                                                  (assert)
                                                  (("3"
                                                    (expand
                                                     "bijective?")
                                                    (("3"
                                                      (flatten)
                                                      (("3"
                                                        (expand
                                                         "injective?")
                                                        (("3"
                                                          (inst
                                                           -6
                                                           "x1!1"
                                                           "g!1(1+j!1)")
                                                          (("3"
                                                            (assert)
                                                            (("3"
                                                              (lemma
                                                               "comp_inverse_right_surj_alt[below[2 + j!1],below[2 + j!1]]"
                                                               ("f"
                                                                "phi!1"
                                                                "g"
                                                                "g!1"
                                                                "r"
                                                                "1+j!1"))
                                                              (("3"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (hide-all-but (-1 -2 -3 -4 1))
                                    (("2"
                                      (expand "bijective?")
                                      (("2"
                                        (flatten)
                                        (("2"
                                          (expand "injective?")
                                          (("2"
                                            (inst
                                             -
                                             "1+j!1"
                                             "phi!1(1+j!1)")
                                            (("2"
                                              (split -1)
                                              (("1" (assert) nil nil)
                                               ("2"
                                                (lemma
                                                 "comp_inverse_left_inj_alt[below[2 + j!1],below[2 + j!1]]"
                                                 ("f"
                                                  "phi!1"
                                                  "g"
                                                  "g!1"
                                                  "d"
                                                  "1+j!1"))
                                                (("2"
                                                  (replace -1)
                                                  (("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2" (propax) nil nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (replace -1)
                          (("2" (assert)
                            (("2"
                              (inst - "F!1"
                               "LAMBDA (n:below[1 + j!1]): phi!1(n)")
                              (("1"
                                (replace -2)
                                (("1"
                                  (lemma
                                   "sigma_eq[nat]"
                                   ("low"
                                    "0"
                                    "high"
                                    "j!1"
                                    "F"
                                    "LAMBDA (x: nat):
             IF x < 1 + j!1 THEN F!1(phi!1(x)) ELSE F!1(x) ENDIF"
                                    "G"
                                    "
             LAMBDA (x: nat):
               IF x < 2 + j!1 THEN F!1(phi!1(x)) ELSE F!1(x) ENDIF"))
                                  (("1"
                                    (split -1)
                                    (("1" (propax) nil nil)
                                     ("2"
                                      (hide 2)
                                      (("2"
                                        (skosimp)
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (skosimp)
                                    (("2" (assert) nil nil))
                                    nil)
                                   ("3"
                                    (skosimp)
                                    (("3" (assert) nil nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (typepred "phi!1")
                                (("2"
                                  (hide 2)
                                  (("2"
                                    (expand "bijective?")
                                    (("2"
                                      (flatten)
                                      (("2"
                                        (split)
                                        (("1"
                                          (expand "injective?")
                                          (("1"
                                            (skosimp)
                                            (("1"
                                              (inst - "x1!1" "x2!1")
                                              (("1" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (expand "surjective?")
                                          (("2"
                                            (skosimp)
                                            (("2"
                                              (inst - "y!1")
                                              (("2"
                                                (skosimp)
                                                (("2"
                                                  (typepred "x!1")
                                                  (("2"
                                                    (expand
                                                     "injective?")
                                                    (("2"
                                                      (inst + "x!1")
                                                      (("2"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("3"
                                (hide 2)
                                (("3"
                                  (skosimp)
                                  (("3"
                                    (typepred "n!1")
                                    (("3"
                                      (typepred "phi!1")
                                      (("3"
                                        (expand "bijective?")
                                        (("3"
                                          (flatten)
                                          (("3"
                                            (expand "injective?")
                                            (("3"
                                              (inst - "n!1" "1+j!1")
                                              (("3" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (typepred "phi!1(1+j!1)")
                      (("2" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil)
             ("3" (skosimp) nil nil)
             ("4" (skosimp*) (("4" (assert) nil nil)) nil))
            nil))
          nil)
         ("3" (skosimp) nil nil)
         ("4" (skosimp) (("4" (skosimp) (("4" (assert) nil nil)) nil))
          nil))
        nil))
      nil)
     ("3" (skosimp)
      (("3" (skosimp)
        (("3" (typepred "x!1") (("3" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((phi!1 skolem-const-decl
     "(bijective?[below[2 + j!1], below[2 + j!1]])" sigma_bijection
     nil)
    (x!1 skolem-const-decl "below[2 + j!1]" sigma_bijection nil)
    (sigma_with formula-decl nil sigma "reals/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (sigma_eq formula-decl nil sigma "reals/")
    (subrange type-eq-decl nil integers nil)
    (comp_inverse_right_surj_alt formula-decl nil function_inverse_def
     nil)
    (FF skolem-const-decl "[nat -> real]" sigma_bijection nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (PHI skolem-const-decl "[below[1 + j!1] -> below[2 + j!1]]"
     sigma_bijection nil)
    (j!1 skolem-const-decl "nat" sigma_bijection nil)
    (x!1 skolem-const-decl "below[2 + j!1]" sigma_bijection nil)
    (g!1 skolem-const-decl "[below[2 + j!1] -> below[2 + j!1]]"
     sigma_bijection nil)
    (comp_inverse_left_inj_alt formula-decl nil function_inverse_def
     nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (bij_inv_is_bij_alt formula-decl nil function_inverse_def nil)
    (surjective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (n!1 skolem-const-decl "nat" sigma_bijection nil)
    (phi!1 skolem-const-decl
     "(bijective?[below[1 + n!1], below[1 + n!1]])" sigma_bijection
     nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T_pred const-decl "[int -> boolean]" sigma_bijection nil)
    (T formal-subtype-decl nil sigma_bijection nil)
    (subrange_T type-eq-decl nil sigma_bijection nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (N skolem-const-decl "int" sigma_bijection nil)
    (PHI skolem-const-decl "[below[N + 1] -> int]" sigma_bijection nil)
    (restrict const-decl "R" restrict nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (low!1 skolem-const-decl "T" sigma_bijection nil)
    (high!1 skolem-const-decl "T" sigma_bijection nil)
    (pred type-eq-decl nil defined_types nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (FF skolem-const-decl "[below[N + 1] -> real]" sigma_bijection nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (connected_domain formula-decl nil sigma_bijection nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (surjective? const-decl "bool" functions nil)
    (y!1 skolem-const-decl "below[1 + N]" sigma_bijection nil)
    (x!1 skolem-const-decl "subrange_T(low!1, high!1)" sigma_bijection
     nil)
    (injective? const-decl "bool" functions nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (integer nonempty-type-from-decl nil integers nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (below type-eq-decl nil nat_types nil)
    (bijective? const-decl "bool" functions nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (T_low type-eq-decl nil sigma "reals/")
    (T_high type-eq-decl nil sigma "reals/")
    (sigma def-decl "real" sigma "reals/")
    (O const-decl "T3" function_props nil))
   shostak)))