Quelle  linear_functions.prf

(linear_functions
 (linear_add 0
  (linear_add-1 nil 3430728751
   ("" (skosimp*)
    (("" (expand "linear?")
      (("" (skosimp*)
        (("" (inst + "m!1+m!2" "k!1+k!2")
          (("" (expand "+ ")
            (("" (replace -1 * lr)
              (("" (hide -1)
                (("" (replace -1 * lr)
                  (("" (hide -1) (("" (assert) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (linear? const-decl "bool" linear_functions nil)
    (real_plus_real_is_real application-judgement "real" reals 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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/"))
   shostak)))