(set-logic ALL) ; has unbounded values, using catch-all.
(declare-datatypes ((SBVTuple2 2)) ((par (T1 T2)
                                    ((mkSBVTuple2 (proj_1_SBVTuple2 T1)
                                                  (proj_2_SBVTuple2 T2))))))
(define-fun s35 () Int 0)
(define-fun s40 () Int 1)
(declare-fun s0 () (Seq Int)) ; tracks user variable "__internal_sbv_s0"
(declare-fun s1 () (Seq Int)) ; tracks user variable "__internal_sbv_s1"
(declare-fun s2 () (SBVTuple2 (Seq Int) (Seq Int))) ; tracks user variable "__internal_sbv_s2"
(declare-fun s17 () (Seq Int)) ; tracks user variable "xs"
(declare-fun s18 () (Seq Int)) ; tracks user variable "ys"
(declare-fun s19 () (SBVTuple2 (Seq Int) (Seq Int))) ; tracks user variable "alts"
(define-fun-rec sbv.reverse_165260 ((lst (Seq Int))) (Seq Int)
                (ite (= lst (as seq.empty (Seq Int)))
                     (as seq.empty (Seq Int))
                     (seq.++ (sbv.reverse_165260 (seq.extract lst 1 (- (seq.len lst) 1))) (seq.unit (seq.nth lst 0)))))
(define-fun-rec uninterleave ((l1_s0 (Seq Int)) (l1_s1 (SBVTuple2 (Seq Int) (Seq Int)))) (SBVTuple2 (Seq Int) (Seq Int))
                          (let ((l1_s3 0))
                          (let ((l1_s10 1))
                          (let ((l1_s2 (seq.len l1_s0)))
                          (let ((l1_s4 (= l1_s2 l1_s3)))
                          (let ((l1_s5 (proj_1_SBVTuple2 l1_s1)))
                          (let ((l1_s6 (sbv.reverse_165260 l1_s5)))
                          (let ((l1_s7 (proj_2_SBVTuple2 l1_s1)))
                          (let ((l1_s8 (sbv.reverse_165260 l1_s7)))
                          (let ((l1_s9 ((as mkSBVTuple2 (SBVTuple2 (Seq Int) (Seq Int))) l1_s6 l1_s8)))
                          (let ((l1_s11 (- l1_s2 l1_s10)))
                          (let ((l1_s12 (seq.extract l1_s0 l1_s10 l1_s11)))
                          (let ((l1_s13 (seq.nth l1_s0 l1_s3)))
                          (let ((l1_s14 (seq.unit l1_s13)))
                          (let ((l1_s15 (seq.++ l1_s14 l1_s5)))
                          (let ((l1_s16 ((as mkSBVTuple2 (SBVTuple2 (Seq Int) (Seq Int))) l1_s7 l1_s15)))
                          (let ((l1_s17 (uninterleave l1_s12 l1_s16)))
                          (let ((l1_s18 (ite l1_s4 l1_s9 l1_s17)))
                          l1_s18))))))))))))))))))
(define-fun-rec interleave ((l1_s0 (Seq Int)) (l1_s1 (Seq Int))) (Seq Int)
                          (let ((l1_s3 0))
                          (let ((l1_s7 1))
                          (let ((l1_s2 (seq.len l1_s0)))
                          (let ((l1_s4 (= l1_s2 l1_s3)))
                          (let ((l1_s5 (seq.nth l1_s0 l1_s3)))
                          (let ((l1_s6 (seq.unit l1_s5)))
                          (let ((l1_s8 (- l1_s2 l1_s7)))
                          (let ((l1_s9 (seq.extract l1_s0 l1_s7 l1_s8)))
                          (let ((l1_s10 (interleave l1_s1 l1_s9)))
                          (let ((l1_s11 (seq.++ l1_s6 l1_s10)))
                          (let ((l1_s12 (ite l1_s4 l1_s1 l1_s11)))
                          l1_s12))))))))))))
(define-fun s3 () Int (seq.len s0))
(define-fun s4 () Int (seq.len s1))
(define-fun s5 () Bool (= s3 s4))
(define-fun s6 () (Seq Int) (interleave s0 s1))
(define-fun s7 () (SBVTuple2 (Seq Int) (Seq Int)) (uninterleave s6 s2))
(define-fun s8 () (Seq Int) (proj_1_SBVTuple2 s2))
(define-fun s9 () (Seq Int) (sbv.reverse_165260 s8))
(define-fun s10 () (Seq Int) (seq.++ s9 s0))
(define-fun s11 () (Seq Int) (proj_2_SBVTuple2 s2))
(define-fun s12 () (Seq Int) (sbv.reverse_165260 s11))
(define-fun s13 () (Seq Int) (seq.++ s12 s1))
(define-fun s14 () (SBVTuple2 (Seq Int) (Seq Int)) ((as mkSBVTuple2 (SBVTuple2 (Seq Int) (Seq Int))) s10 s13))
(define-fun s15 () Bool (= s7 s14))
(define-fun s16 () Bool (=> s5 s15))
(define-fun s20 () Int (seq.len s17))
(define-fun s21 () Int (seq.len s18))
(define-fun s22 () Bool (= s20 s21))
(define-fun s23 () (Seq Int) (interleave s17 s18))
(define-fun s24 () (SBVTuple2 (Seq Int) (Seq Int)) (uninterleave s23 s19))
(define-fun s25 () (Seq Int) (proj_1_SBVTuple2 s19))
(define-fun s26 () (Seq Int) (sbv.reverse_165260 s25))
(define-fun s27 () (Seq Int) (seq.++ s26 s17))
(define-fun s28 () (Seq Int) (proj_2_SBVTuple2 s19))
(define-fun s29 () (Seq Int) (sbv.reverse_165260 s28))
(define-fun s30 () (Seq Int) (seq.++ s29 s18))
(define-fun s31 () (SBVTuple2 (Seq Int) (Seq Int)) ((as mkSBVTuple2 (SBVTuple2 (Seq Int) (Seq Int))) s27 s30))
(define-fun s32 () Bool (= s24 s31))
(define-fun s33 () Bool (=> s22 s32))
(define-fun s34 () Bool s33) ; Observing: P(xs, ys, alts)
(define-fun s36 () Bool (= s20 s35))
(define-fun s37 () Bool (not s36))
(define-fun s38 () Int (seq.nth s17 s35))
(define-fun s39 () (Seq Int) (seq.unit s38))
(define-fun s41 () Int (- s20 s40))
(define-fun s42 () (Seq Int) (seq.extract s17 s40 s41))
(define-fun s43 () (Seq Int) (interleave s18 s42))
(define-fun s44 () (Seq Int) (seq.++ s39 s43))
(define-fun s45 () (SBVTuple2 (Seq Int) (Seq Int)) (uninterleave s44 s19))
(define-fun s46 () Bool (= s24 s45))
(define-fun s47 () (Seq Int) (seq.++ s39 s25))
(define-fun s48 () (SBVTuple2 (Seq Int) (Seq Int)) ((as mkSBVTuple2 (SBVTuple2 (Seq Int) (Seq Int))) s28 s47))
(define-fun s49 () (SBVTuple2 (Seq Int) (Seq Int)) (uninterleave s43 s48))
(define-fun s50 () Bool (= s45 s49))
(define-fun s51 () Bool (forall ((l1_s0 Bool))
                          (let ((l1_s1 l1_s0)) ; SORRY: KnuckleDragger, proof uses "sorry"
                          l1_s1)))
(define-fun s52 () Bool s51) ; sorry
(define-fun s53 () Bool (= s31 s49))
(define-fun s54 () Int (seq.len s42))
(define-fun s55 () Int (+ s21 s54))
(define-fun s56 () Int (+ s20 s21))
(define-fun s57 () Bool (< s55 s56))
(define-fun s58 () Bool (= s21 s54))
(define-fun s59 () (Seq Int) (proj_1_SBVTuple2 s48))
(define-fun s60 () (Seq Int) (sbv.reverse_165260 s59))
(define-fun s61 () (Seq Int) (seq.++ s60 s18))
(define-fun s62 () (Seq Int) (proj_2_SBVTuple2 s48))
(define-fun s63 () (Seq Int) (sbv.reverse_165260 s62))
(define-fun s64 () (Seq Int) (seq.++ s63 s42))
(define-fun s65 () (SBVTuple2 (Seq Int) (Seq Int)) ((as mkSBVTuple2 (SBVTuple2 (Seq Int) (Seq Int))) s61 s64))
(define-fun s66 () Bool (= s49 s65))
(define-fun s67 () Bool (=> s58 s66))
(define-fun s68 () Bool (=> s57 s67))
(define-fun s69 () Bool s68) ; IH @ (xs |-> <symbolic> :: [SInteger],ys |-> <symbolic> :: [SInteger],alts |-> <symbolic> :: ([SInteger], [SInteger]))
(define-fun s77 () Bool (and s52 s69))
(define-fun s78 () Bool (and s22 s77))
(assert s78)
(exit)