Quelle  fun_preds_partial.prf

(fun_preds_partial
 (strict_increasing_is_increasing 0
  (strict_increasing_is_increasing-1 nil 3314595658
   ("" (expand "strict_increasing?")
    (("" (expand "increasing?")
      (("" (skosimp*)
        (("" (inst - "x!1" "y!1")
          (("" (case-replace "x!1/=y!1")
            (("1" (assert) nil nil)
             ("2" (expand "/=")
              (("2" (typepred "le2")
                (("2" (expand "partial_order?")
                  (("2" (expand "preorder?")
                    (("2" (expand "reflexive?")
                      (("2" (flatten)
                        (("2" (inst - "f!1(x!1)")
                          (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((increasing? const-decl "bool" fun_preds_partial nil)
    (T1 formal-type-decl nil fun_preds_partial nil)
    (reflexive? const-decl "bool" relations nil)
    (preorder? const-decl "bool" orders nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T2 formal-type-decl nil 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)
    (/= const-decl "boolean" notequal nil)
    (boolean nonempty-type-decl nil booleans nil)
    (strict_increasing? const-decl "bool" fun_preds_partial nil))
   shostak))
 (strict_decreasing_is_decreasing 0
  (strict_decreasing_is_decreasing-1 nil 3314595773
   ("" (expand "strict_decreasing?")
    (("" (expand "decreasing?")
      (("" (skosimp*)
        (("" (inst - "x!1" "y!1")
          (("" (expand "/=")
            (("" (case-replace "x!1=y!1")
              (("1" (typepred "le2")
                (("1" (expand "partial_order?")
                  (("1" (expand "preorder?")
                    (("1" (expand "reflexive?")
                      (("1" (flatten)
                        (("1" (inst - "f!1(y!1)") nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((decreasing? const-decl "bool" fun_preds_partial nil)
    (T1 formal-type-decl nil fun_preds_partial nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (reflexive? const-decl "bool" relations nil)
    (preorder? const-decl "bool" orders nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T2 formal-type-decl nil 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)
    (/= const-decl "boolean" notequal nil)
    (strict_decreasing? const-decl "bool" fun_preds_partial nil))
   shostak)))