; Automatically generated by SBV. Do not modify!
; |e @(SBV Integer -> SBV Integer)| :: SInteger -> SInteger, |o @(SBV Integer -> SBV Integer)| :: SInteger -> SInteger
(define-funs-rec
  ((|e @(SBV Integer -> SBV Integer)| ((l1_s0 Int)) Int)
   (|o @(SBV Integer -> SBV Integer)| ((l2_s0 Int)) Int))
  (; Definition of: |e @(SBV Integer -> SBV Integer)| :: SInteger -> SInteger. [Refers to: |o @(SBV Integer -> SBV Integer)|]
                           (let ((l1_s1 1))
                           (let ((l1_s2 (- l1_s0 l1_s1)))
                           (let ((l1_s3 (|o @(SBV Integer -> SBV Integer)| l1_s2)))
                           l1_s3)))
   ; Definition of: |o @(SBV Integer -> SBV Integer)| :: SInteger -> SInteger. [Refers to: |e @(SBV Integer -> SBV Integer)|]
                                           (let ((l2_s1 1))
                                           (let ((l2_s2 (- l2_s0 l2_s1)))
                                           (let ((l2_s3 (|e @(SBV Integer -> SBV Integer)| l2_s2)))
                                           l2_s3)))))