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