(|max_seq| (|Imax_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL)))
 (|Imax_TCC2| "" (SUBTYPE-TCC) NIL)
 (|Imax_TCC3| ""
  (INST 1 "(LAMBDA ((s: seqs), (ii: dom(s)), (jj:abv(ii, s))):
                    Imax[length(s),T,<=](seq(s),ii,jj))")
  (("" (SKOSIMP*)
    (("" (TYPEPRED "Imax[length(s!1), T, <=](seq(s!1), ii!1, jj!1)")
      (("" (INST -3 "j!1") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))))))))
 (|Imax_1_TCC1| "" (SUBTYPE-TCC) NIL)
 (|Imax_1| "" (SKOSIMP*)
  (("" (TYPEPRED "Imax(s!1, ii!1, ii!1)")
    (("1" (INST?) (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))
     ("2" (SKOSIMP*) (("2" (ASSERT) NIL)))))))
 (|imax_TCC1| "" (INST 1 "(LAMBDA s: Imax(s,0,length(s)-1))")
  (("" (SKOSIMP*)
    (("" (TYPEPRED "Imax(s!1, 0, length(s!1) - 1)")
      (("1" (ASSERT) (("1" (SKOSIMP*) (("1" (INST?) (("1" (ASSERT) NIL)))))))
       ("2" (HIDE 2) (("2" (SKOSIMP*) (("2" (ASSERT) NIL)))))))))))
 (|max_TCC1| "" (INST 1 "(LAMBDA s: seq(s)(imax(s)))")
  (("" (SKOSIMP*)
    (("" (PROP)
      (("1" (SKOSIMP*) (("1" (TYPEPRED "imax(s!1)") (("1" (INST?) NIL)))))
       ("2" (INST?) NIL)))))))
 (|max_seq_lem| "" (SKOSIMP*) (("" (TYPEPRED "max(s!1)") (("" (INST?) NIL)))))
 (|max_seq_in?| "" (SKOSIMP*)
  (("" (EXPAND "in?")
    (("" (TYPEPRED "max(s!1)")
      (("" (SKOSIMP*)
        (("" (HIDE -1) (("" (INST?) (("" (ASSERT) NIL)))))))))))))
 (|imax_seq_lem| "" (SKOSIMP*)
  (("" (TYPEPRED "imax(s!1)")
    (("" (TYPEPRED "max(s!1)")
      (("" (SKOSIMP*)
        (("" (REPLACE -2 * RL)
          (("" (HIDE -2)
            (("" (INST?)
              (("" (INST -3 "jj!1")
                (("" (TYPEPRED "max_seq.<=")
                  (("" (EXPAND "total_order?")
                    (("" (EXPAND "partial_order?")
                      (("" (FLATTEN)
                        (("" (EXPAND "antisymmetric?")
                          (("" (INST?)
                            (("" (ASSERT) NIL)))))))))))))))))))))))))))))
 (|max_seq_def| "" (SKOSIMP*)
  (("" (PROP)
    (("1" (LEMMA "max_seq_lem") (("1" (INST?) NIL)))
     ("2" (REWRITE "max_seq_in?") NIL)))))
 (|max_seq_it_is| "" (SKOSIMP*)
  (("" (TYPEPRED "max(s!1)")
    (("" (EXPAND "in?")
      (("" (SKOSIMP*)
        (("" (REPLACE -2 * RL)
          (("" (HIDE -2)
            (("" (REPLACE -3)
              (("" (HIDE -3)
                (("" (INST?)
                  (("" (INST -2 "jj!1")
                    (("" (TYPEPRED "<=")
                      (("" (EXPAND "total_order?")
                        (("" (EXPAND "partial_order?")
                          (("" (FLATTEN)
                            (("" (EXPAND "antisymmetric?")
                              (("" (INST?)
                                (("" (ASSERT)
                                  NIL)))))))))))))))))))))))))))))))))
 (|imax_seq_1| "" (SKOSIMP*)
  (("" (TYPEPRED "imax(s!1)") (("" (ASSERT) NIL)))))
 (|max_seq_2_TCC1| "" (SUBTYPE-TCC) NIL)
 (|max_seq_2_TCC2| "" (SUBTYPE-TCC) NIL)
 (|max_seq_2| "" (SKOSIMP*)
  (("" (TYPEPRED "max(s!1)")
    (("" (SKOSIMP*)
      (("" (REPLACE -2 * RL)
        (("" (HIDE -2)
          (("" (INST-CP -1 "0")
            (("" (INST -1 "1")
              (("1" (LIFT-IF)
                (("1" (GROUND)
                  (("1" (CASE-REPLACE "jj!1 = 0 OR jj!1 = 1")
                    (("1" (TYPEPRED "max_seq.<=")
                      (("1" (EXPAND "total_order?")
                        (("1" (EXPAND "partial_order?")
                          (("1" (FLATTEN)
                            (("1" (EXPAND "antisymmetric?")
                              (("1" (INST?) (("1" (ASSERT) NIL)))))))))))))
                     ("2" (HIDE -1 -2 -3 2)
                      (("2" (TYPEPRED "jj!1") (("2" (GROUND) NIL)))))))))))
               ("2" (ASSERT) NIL))))))))))))))))