(fun_preds_partial
 (strict_increasing_is_increasing 0
  (strict_increasing_is_increasing-1 nil 3314595658
   ("" (skosimp)
    (("" (typepred "x!1")
      (("" (expand "strict_increasing?")
        (("" (expand "increasing?")
          (("" (skosimp)
            (("" (inst - "x!2" "y!1")
              (("" (replace 1)
                (("" (replace -1)
                  (("" (expand "/=")
                    (("" (typepred "le2")
                      (("" (expand "partial_order?")
                        (("" (expand "preorder?")
                          (("" (expand "reflexive?")
                            (("" (flatten)
                              ((""
                                (inst - "x!1(x!2)")
                                (("" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((strict_increasing? const-decl "bool" fun_preds_partial nil)
    (T2 formal-type-decl nil fun_preds_partial nil)
    (T1 formal-type-decl nil fun_preds_partial nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (increasing? const-decl "bool" fun_preds_partial nil)
    (pred type-eq-decl nil defined_types nil)
    (partial_order? const-decl "bool" orders nil)
    (le2 formal-const-decl "(partial_order?[T2])" fun_preds_partial
     nil)
    (preorder? const-decl "bool" orders nil)
    (reflexive? const-decl "bool" relations nil)
    (/= const-decl "boolean" notequal nil))
   shostak))
 (strict_decreasing_is_decreasing 0
  (strict_decreasing_is_decreasing-1 nil 3314595773
   ("" (skosimp)
    (("" (typepred "x!1")
      (("" (expand "strict_decreasing?")
        (("" (expand "decreasing?")
          (("" (skosimp)
            (("" (typepred "le2")
              (("" (expand "partial_order?")
                (("" (expand "preorder?")
                  (("" (expand "reflexive?")
                    (("" (flatten)
                      (("" (inst - "x!1(y!1)")
                        (("" (inst - "x!2" "y!1")
                          (("" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((strict_decreasing? const-decl "bool" fun_preds_partial nil)
    (T2 formal-type-decl nil fun_preds_partial nil)
    (T1 formal-type-decl nil fun_preds_partial nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (decreasing? const-decl "bool" fun_preds_partial nil)
    (le2 formal-const-decl "(partial_order?[T2])" fun_preds_partial
     nil)
    (partial_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (preorder? const-decl "bool" orders nil)
    (reflexive? const-decl "bool" relations nil))
   shostak))
 (strict_monotonic_is_monotonic 0
  (strict_monotonic_is_monotonic-1 nil 3330921270
   ("" (skosimp)
    (("" (typepred "x!1")
      (("" (expand "strict_monotonic?")
        (("" (expand "monotonic?")
          (("" (flatten)
            (("" (split)
              (("1" (use "strict_increasing_is_increasing") nil nil)
               ("2" (use "strict_decreasing_is_decreasing") nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((strict_monotonic? const-decl "bool" fun_preds_partial nil)
    (T2 formal-type-decl nil fun_preds_partial nil)
    (T1 formal-type-decl nil fun_preds_partial nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (monotonic? const-decl "bool" fun_preds_partial nil)
    (strict_increasing_is_increasing judgement-tcc nil
     fun_preds_partial nil)
    (strict_increasing? const-decl "bool" fun_preds_partial nil)
    (x!1 skolem-const-decl "(strict_monotonic?)" fun_preds_partial nil)
    (strict_decreasing_is_decreasing judgement-tcc nil
     fun_preds_partial nil)
    (strict_decreasing? const-decl "bool" fun_preds_partial nil))
   shostak)))