; COMMAND-LINE: --lang=smt2.5
; EXPECT: unsat
(set-logic ALL_SUPPORTED)
(set-info :status unsat)
(declare-sort A$ 0)
(declare-sort B$ 0)
(declare-sort A_set$ 0)
(declare-sort B_set$ 0)
(declare-sort A_a_fun$ 0)
(declare-sort A_b_fun$ 0)
(declare-sort B_a_fun$ 0)
(declare-sort B_b_fun$ 0)
(declare-sort A_stream_set$ 0)
(declare-sort B_stream_set$ 0)
(declare-sort A_a_stream_fun$ 0)
(declare-sort A_b_stream_fun$ 0)
(declare-sort A_stream_a_fun$ 0)
(declare-sort A_stream_b_fun$ 0)
(declare-sort B_a_stream_fun$ 0)
(declare-sort B_b_stream_fun$ 0)
(declare-sort B_stream_a_fun$ 0)
(declare-sort B_stream_b_fun$ 0)
(declare-sort A_stream_stream_set$ 0)
(declare-sort B_stream_stream_set$ 0)
(declare-sort A_stream_a_stream_fun$ 0)
(declare-sort B_stream_b_stream_fun$ 0)
(declare-sort A_stream_stream_a_stream_stream_fun$ 0)
(declare-sort B_stream_stream_b_stream_stream_fun$ 0)
(declare-sort A_stream_stream_stream_a_stream_stream_stream_fun$ 0)
(declare-sort B_stream_stream_stream_b_stream_stream_stream_fun$ 0)
(declare-datatypes () ((Nat$ (zero$) (suc$ (pred$ Nat$)))))
(declare-codatatypes () ((A_stream$ (sCons$ (shd$ A$) (stl$ A_stream$)))
  (B_stream$ (sCons$a (shd$a B$) (stl$a B_stream$)))
  (B_stream_stream$ (sCons$b (shd$b B_stream$) (stl$b B_stream_stream$)))
  (B_stream_stream_stream$ (sCons$c (shd$c B_stream_stream$) (stl$c B_stream_stream_stream$)))
  (A_stream_stream$ (sCons$d (shd$d A_stream$) (stl$d A_stream_stream$)))
  (A_stream_stream_stream$ (sCons$e (shd$e A_stream_stream$) (stl$e A_stream_stream_stream$)))))
(declare-fun f$ () B_a_fun$)
(declare-fun x$ () B$)
(declare-fun id$ () B_b_fun$)
(declare-fun id$a () A_a_fun$)
(declare-fun id$b () B_stream_stream_b_stream_stream_fun$)
(declare-fun id$c () A_stream_stream_a_stream_stream_fun$)
(declare-fun id$d () A_stream_a_stream_fun$)
(declare-fun id$e () B_stream_b_stream_fun$)
(declare-fun id$f () B_stream_stream_stream_b_stream_stream_stream_fun$)
(declare-fun id$g () A_stream_stream_stream_a_stream_stream_stream_fun$)
(declare-fun smap$ (B_a_fun$ B_stream$) A_stream$)
(declare-fun snth$ (B_stream_stream$ Nat$) B_stream$)
(declare-fun sdrop$ (Nat$ B_stream_stream$) B_stream_stream$)
(declare-fun smap$a (B_b_fun$) B_stream_b_stream_fun$)
(declare-fun smap$b (A_a_fun$) A_stream_a_stream_fun$)
(declare-fun smap$c (B_stream_stream_b_stream_stream_fun$) B_stream_stream_stream_b_stream_stream_stream_fun$)
(declare-fun smap$d (A_stream_stream_a_stream_stream_fun$) A_stream_stream_stream_a_stream_stream_stream_fun$)
(declare-fun smap$e (A_stream_a_stream_fun$) A_stream_stream_a_stream_stream_fun$)
(declare-fun smap$f (B_stream_b_stream_fun$) B_stream_stream_b_stream_stream_fun$)
(declare-fun smap$g (B_b_stream_fun$ B_stream$) B_stream_stream$)
(declare-fun smap$h (B_a_stream_fun$ B_stream$) A_stream_stream$)
(declare-fun smap$i (A_b_stream_fun$ A_stream$) B_stream_stream$)
(declare-fun smap$j (A_a_stream_fun$ A_stream$) A_stream_stream$)
(declare-fun smap$k (A_b_fun$ A_stream$) B_stream$)
(declare-fun smap$l (B_stream_b_fun$ B_stream_stream$) B_stream$)
(declare-fun smap$m (A_stream_b_fun$ A_stream_stream$) B_stream$)
(declare-fun smap$n (B_stream_a_fun$ B_stream_stream$) A_stream$)
(declare-fun smap$o (A_stream_a_fun$ A_stream_stream$) A_stream$)
(declare-fun snth$a (B_stream$ Nat$) B$)
(declare-fun snth$b (A_stream_stream$ Nat$) A_stream$)
(declare-fun snth$c (A_stream$ Nat$) A$)
(declare-fun member$ (B_stream$ B_stream_set$) Bool)
(declare-fun sdrop$a (Nat$ B_stream$) B_stream$)
(declare-fun sdrop$b (Nat$ A_stream_stream$) A_stream_stream$)
(declare-fun sdrop$c (Nat$ A_stream$) A_stream$)
(declare-fun fun_app$ (B_b_stream_fun$ B$) B_stream$)
(declare-fun member$a (B$ B_set$) Bool)
(declare-fun member$b (A$ A_set$) Bool)
(declare-fun member$c (A_stream$ A_stream_set$) Bool)
(declare-fun member$d (B_stream_stream$ B_stream_stream_set$) Bool)
(declare-fun member$e (A_stream_stream$ A_stream_stream_set$) Bool)
(declare-fun streams$ (B_set$) B_stream_set$)
(declare-fun fun_app$a (A_a_stream_fun$ A$) A_stream$)
(declare-fun fun_app$b (B_a_fun$ B$) A$)
(declare-fun fun_app$c (B_stream_b_stream_fun$ B_stream$) B_stream$)
(declare-fun fun_app$d (B_b_fun$ B$) B$)
(declare-fun fun_app$e (A_stream_a_stream_fun$ A_stream$) A_stream$)
(declare-fun fun_app$f (A_a_fun$ A$) A$)
(declare-fun fun_app$g (B_stream_stream_stream_b_stream_stream_stream_fun$ B_stream_stream_stream$) B_stream_stream_stream$)
(declare-fun fun_app$h (A_stream_stream_stream_a_stream_stream_stream_fun$ A_stream_stream_stream$) A_stream_stream_stream$)
(declare-fun fun_app$i (A_stream_stream_a_stream_stream_fun$ A_stream_stream$) A_stream_stream$)
(declare-fun fun_app$j (B_stream_stream_b_stream_stream_fun$ B_stream_stream$) B_stream_stream$)
(declare-fun fun_app$k (B_a_stream_fun$ B$) A_stream$)
(declare-fun fun_app$l (A_b_stream_fun$ A$) B_stream$)
(declare-fun fun_app$m (A_b_fun$ A$) B$)
(declare-fun fun_app$n (B_stream_b_fun$ B_stream$) B$)
(declare-fun fun_app$o (A_stream_b_fun$ A_stream$) B$)
(declare-fun fun_app$p (B_stream_a_fun$ B_stream$) A$)
(declare-fun fun_app$q (A_stream_a_fun$ A_stream$) A$)
(declare-fun siterate$ (B_b_fun$) B_b_stream_fun$)
(declare-fun streams$a (A_set$) A_stream_set$)
(declare-fun streams$b (B_stream_set$) B_stream_stream_set$)
(declare-fun streams$c (A_stream_set$) A_stream_stream_set$)
(declare-fun siterate$a (A_a_fun$) A_a_stream_fun$)
(assert (! (not (= (smap$ f$ (fun_app$ (siterate$ id$) x$)) (fun_app$a (siterate$a id$a) (fun_app$b f$ x$)))) :named a0))
(assert (! (forall ((?v0 B_b_fun$) (?v1 B$)) (= (fun_app$c (smap$a ?v0) (fun_app$ (siterate$ ?v0) ?v1)) (fun_app$ (siterate$ ?v0) (fun_app$d ?v0 ?v1)))) :named a1))
(assert (! (forall ((?v0 A_a_fun$) (?v1 A$)) (= (fun_app$e (smap$b ?v0) (fun_app$a (siterate$a ?v0) ?v1)) (fun_app$a (siterate$a ?v0) (fun_app$f ?v0 ?v1)))) :named a2))
(assert (! (forall ((?v0 B_stream_stream_stream$)) (= (fun_app$g (smap$c id$b) ?v0) ?v0)) :named a3))
(assert (! (forall ((?v0 A_stream_stream_stream$)) (= (fun_app$h (smap$d id$c) ?v0) ?v0)) :named a4))
(assert (! (forall ((?v0 A_stream_stream$)) (= (fun_app$i (smap$e id$d) ?v0) ?v0)) :named a5))
(assert (! (forall ((?v0 B_stream_stream$)) (= (fun_app$j (smap$f id$e) ?v0) ?v0)) :named a6))
(assert (! (forall ((?v0 B_stream$)) (= (fun_app$c (smap$a id$) ?v0) ?v0)) :named a7))
(assert (! (forall ((?v0 A_stream$)) (= (fun_app$e (smap$b id$a) ?v0) ?v0)) :named a8))
(assert (! (= (smap$c id$b) id$f) :named a9))
(assert (! (= (smap$d id$c) id$g) :named a10))
(assert (! (= (smap$e id$d) id$c) :named a11))
(assert (! (= (smap$f id$e) id$b) :named a12))
(assert (! (= (smap$a id$) id$e) :named a13))
(assert (! (= (smap$b id$a) id$d) :named a14))
(assert (! (forall ((?v0 B_stream_stream$)) (! (= (fun_app$j id$b ?v0) ?v0) :pattern ((fun_app$j id$b ?v0)))) :named a15))
(assert (! (forall ((?v0 A_stream_stream$)) (! (= (fun_app$i id$c ?v0) ?v0) :pattern ((fun_app$i id$c ?v0)))) :named a16))
(assert (! (forall ((?v0 A_stream$)) (! (= (fun_app$e id$d ?v0) ?v0) :pattern ((fun_app$e id$d ?v0)))) :named a17))
(assert (! (forall ((?v0 B_stream$)) (! (= (fun_app$c id$e ?v0) ?v0) :pattern ((fun_app$c id$e ?v0)))) :named a18))
(assert (! (forall ((?v0 B$)) (! (= (fun_app$d id$ ?v0) ?v0) :pattern ((fun_app$d id$ ?v0)))) :named a19))
(assert (! (forall ((?v0 A$)) (! (= (fun_app$f id$a ?v0) ?v0) :pattern ((fun_app$f id$a ?v0)))) :named a20))
(assert (! (forall ((?v0 B_stream_stream$)) (! (= (fun_app$j id$b ?v0) ?v0) :pattern ((fun_app$j id$b ?v0)))) :named a21))
(assert (! (forall ((?v0 A_stream_stream$)) (! (= (fun_app$i id$c ?v0) ?v0) :pattern ((fun_app$i id$c ?v0)))) :named a22))
(assert (! (forall ((?v0 A_stream$)) (! (= (fun_app$e id$d ?v0) ?v0) :pattern ((fun_app$e id$d ?v0)))) :named a23))
(assert (! (forall ((?v0 B_stream$)) (! (= (fun_app$c id$e ?v0) ?v0) :pattern ((fun_app$c id$e ?v0)))) :named a24))
(assert (! (forall ((?v0 B$)) (! (= (fun_app$d id$ ?v0) ?v0) :pattern ((fun_app$d id$ ?v0)))) :named a25))
(assert (! (forall ((?v0 A$)) (! (= (fun_app$f id$a ?v0) ?v0) :pattern ((fun_app$f id$a ?v0)))) :named a26))
(assert (! (forall ((?v0 B_b_stream_fun$) (?v1 B_stream$) (?v2 Nat$)) (= (snth$ (smap$g ?v0 ?v1) ?v2) (fun_app$ ?v0 (snth$a ?v1 ?v2)))) :named a27))
(assert (! (forall ((?v0 B_a_stream_fun$) (?v1 B_stream$) (?v2 Nat$)) (= (snth$b (smap$h ?v0 ?v1) ?v2) (fun_app$k ?v0 (snth$a ?v1 ?v2)))) :named a28))
(assert (! (forall ((?v0 A_b_stream_fun$) (?v1 A_stream$) (?v2 Nat$)) (= (snth$ (smap$i ?v0 ?v1) ?v2) (fun_app$l ?v0 (snth$c ?v1 ?v2)))) :named a29))
(assert (! (forall ((?v0 A_a_stream_fun$) (?v1 A_stream$) (?v2 Nat$)) (= (snth$b (smap$j ?v0 ?v1) ?v2) (fun_app$a ?v0 (snth$c ?v1 ?v2)))) :named a30))
(assert (! (forall ((?v0 A_b_fun$) (?v1 A_stream$) (?v2 Nat$)) (= (snth$a (smap$k ?v0 ?v1) ?v2) (fun_app$m ?v0 (snth$c ?v1 ?v2)))) :named a31))
(assert (! (forall ((?v0 A_a_fun$) (?v1 A_stream$) (?v2 Nat$)) (= (snth$c (fun_app$e (smap$b ?v0) ?v1) ?v2) (fun_app$f ?v0 (snth$c ?v1 ?v2)))) :named a32))
(assert (! (forall ((?v0 B_b_fun$) (?v1 B_stream$) (?v2 Nat$)) (= (snth$a (fun_app$c (smap$a ?v0) ?v1) ?v2) (fun_app$d ?v0 (snth$a ?v1 ?v2)))) :named a33))
(assert (! (forall ((?v0 B_a_fun$) (?v1 B_stream$) (?v2 Nat$)) (= (snth$c (smap$ ?v0 ?v1) ?v2) (fun_app$b ?v0 (snth$a ?v1 ?v2)))) :named a34))
(assert (! (forall ((?v0 Nat$) (?v1 B_b_stream_fun$) (?v2 B_stream$)) (= (sdrop$ ?v0 (smap$g ?v1 ?v2)) (smap$g ?v1 (sdrop$a ?v0 ?v2)))) :named a35))
(assert (! (forall ((?v0 Nat$) (?v1 B_a_stream_fun$) (?v2 B_stream$)) (= (sdrop$b ?v0 (smap$h ?v1 ?v2)) (smap$h ?v1 (sdrop$a ?v0 ?v2)))) :named a36))
(assert (! (forall ((?v0 Nat$) (?v1 A_b_stream_fun$) (?v2 A_stream$)) (= (sdrop$ ?v0 (smap$i ?v1 ?v2)) (smap$i ?v1 (sdrop$c ?v0 ?v2)))) :named a37))
(assert (! (forall ((?v0 Nat$) (?v1 A_a_stream_fun$) (?v2 A_stream$)) (= (sdrop$b ?v0 (smap$j ?v1 ?v2)) (smap$j ?v1 (sdrop$c ?v0 ?v2)))) :named a38))
(assert (! (forall ((?v0 Nat$) (?v1 A_b_fun$) (?v2 A_stream$)) (= (sdrop$a ?v0 (smap$k ?v1 ?v2)) (smap$k ?v1 (sdrop$c ?v0 ?v2)))) :named a39))
(assert (! (forall ((?v0 Nat$) (?v1 A_a_fun$) (?v2 A_stream$)) (= (sdrop$c ?v0 (fun_app$e (smap$b ?v1) ?v2)) (fun_app$e (smap$b ?v1) (sdrop$c ?v0 ?v2)))) :named a40))
(assert (! (forall ((?v0 Nat$) (?v1 B_b_fun$) (?v2 B_stream$)) (= (sdrop$a ?v0 (fun_app$c (smap$a ?v1) ?v2)) (fun_app$c (smap$a ?v1) (sdrop$a ?v0 ?v2)))) :named a41))
(assert (! (forall ((?v0 Nat$) (?v1 B_a_fun$) (?v2 B_stream$)) (= (sdrop$c ?v0 (smap$ ?v1 ?v2)) (smap$ ?v1 (sdrop$a ?v0 ?v2)))) :named a42))
(assert (! (forall ((?v0 B_b_stream_fun$) (?v1 B_stream$)) (= (shd$b (smap$g ?v0 ?v1)) (fun_app$ ?v0 (shd$a ?v1)))) :named a43))
(assert (! (forall ((?v0 B_a_stream_fun$) (?v1 B_stream$)) (= (shd$d (smap$h ?v0 ?v1)) (fun_app$k ?v0 (shd$a ?v1)))) :named a44))
(assert (! (forall ((?v0 A_b_stream_fun$) (?v1 A_stream$)) (= (shd$b (smap$i ?v0 ?v1)) (fun_app$l ?v0 (shd$ ?v1)))) :named a45))
(assert (! (forall ((?v0 A_a_stream_fun$) (?v1 A_stream$)) (= (shd$d (smap$j ?v0 ?v1)) (fun_app$a ?v0 (shd$ ?v1)))) :named a46))
(assert (! (forall ((?v0 A_b_fun$) (?v1 A_stream$)) (= (shd$a (smap$k ?v0 ?v1)) (fun_app$m ?v0 (shd$ ?v1)))) :named a47))
(assert (! (forall ((?v0 A_a_fun$) (?v1 A_stream$)) (= (shd$ (fun_app$e (smap$b ?v0) ?v1)) (fun_app$f ?v0 (shd$ ?v1)))) :named a48))
(assert (! (forall ((?v0 B_b_fun$) (?v1 B_stream$)) (= (shd$a (fun_app$c (smap$a ?v0) ?v1)) (fun_app$d ?v0 (shd$a ?v1)))) :named a49))
(assert (! (forall ((?v0 B_a_fun$) (?v1 B_stream$)) (= (shd$ (smap$ ?v0 ?v1)) (fun_app$b ?v0 (shd$a ?v1)))) :named a50))
(assert (! (forall ((?v0 B_b_stream_fun$) (?v1 B_stream$)) (= (stl$b (smap$g ?v0 ?v1)) (smap$g ?v0 (stl$a ?v1)))) :named a51))
(assert (! (forall ((?v0 B_a_stream_fun$) (?v1 B_stream$)) (= (stl$d (smap$h ?v0 ?v1)) (smap$h ?v0 (stl$a ?v1)))) :named a52))
(assert (! (forall ((?v0 A_b_stream_fun$) (?v1 A_stream$)) (= (stl$b (smap$i ?v0 ?v1)) (smap$i ?v0 (stl$ ?v1)))) :named a53))
(assert (! (forall ((?v0 A_a_stream_fun$) (?v1 A_stream$)) (= (stl$d (smap$j ?v0 ?v1)) (smap$j ?v0 (stl$ ?v1)))) :named a54))
(assert (! (forall ((?v0 A_b_fun$) (?v1 A_stream$)) (= (stl$a (smap$k ?v0 ?v1)) (smap$k ?v0 (stl$ ?v1)))) :named a55))
(assert (! (forall ((?v0 A_a_fun$) (?v1 A_stream$)) (= (stl$ (fun_app$e (smap$b ?v0) ?v1)) (fun_app$e (smap$b ?v0) (stl$ ?v1)))) :named a56))
(assert (! (forall ((?v0 B_b_fun$) (?v1 B_stream$)) (= (stl$a (fun_app$c (smap$a ?v0) ?v1)) (fun_app$c (smap$a ?v0) (stl$a ?v1)))) :named a57))
(assert (! (forall ((?v0 B_a_fun$) (?v1 B_stream$)) (= (stl$ (smap$ ?v0 ?v1)) (smap$ ?v0 (stl$a ?v1)))) :named a58))
(assert (! (forall ((?v0 B_b_stream_fun$) (?v1 B_stream$) (?v2 B_stream_stream$)) (= (= (smap$g ?v0 ?v1) ?v2) (forall ((?v3 Nat$)) (= (fun_app$ ?v0 (snth$a ?v1 ?v3)) (snth$ ?v2 ?v3))))) :named a59))
(assert (! (forall ((?v0 B_a_stream_fun$) (?v1 B_stream$) (?v2 A_stream_stream$)) (= (= (smap$h ?v0 ?v1) ?v2) (forall ((?v3 Nat$)) (= (fun_app$k ?v0 (snth$a ?v1 ?v3)) (snth$b ?v2 ?v3))))) :named a60))
(assert (! (forall ((?v0 A_b_stream_fun$) (?v1 A_stream$) (?v2 B_stream_stream$)) (= (= (smap$i ?v0 ?v1) ?v2) (forall ((?v3 Nat$)) (= (fun_app$l ?v0 (snth$c ?v1 ?v3)) (snth$ ?v2 ?v3))))) :named a61))
(assert (! (forall ((?v0 A_a_stream_fun$) (?v1 A_stream$) (?v2 A_stream_stream$)) (= (= (smap$j ?v0 ?v1) ?v2) (forall ((?v3 Nat$)) (= (fun_app$a ?v0 (snth$c ?v1 ?v3)) (snth$b ?v2 ?v3))))) :named a62))
(assert (! (forall ((?v0 A_b_fun$) (?v1 A_stream$) (?v2 B_stream$)) (= (= (smap$k ?v0 ?v1) ?v2) (forall ((?v3 Nat$)) (= (fun_app$m ?v0 (snth$c ?v1 ?v3)) (snth$a ?v2 ?v3))))) :named a63))
(assert (! (forall ((?v0 A_a_fun$) (?v1 A_stream$) (?v2 A_stream$)) (= (= (fun_app$e (smap$b ?v0) ?v1) ?v2) (forall ((?v3 Nat$)) (= (fun_app$f ?v0 (snth$c ?v1 ?v3)) (snth$c ?v2 ?v3))))) :named a64))
(assert (! (forall ((?v0 B_b_fun$) (?v1 B_stream$) (?v2 B_stream$)) (= (= (fun_app$c (smap$a ?v0) ?v1) ?v2) (forall ((?v3 Nat$)) (= (fun_app$d ?v0 (snth$a ?v1 ?v3)) (snth$a ?v2 ?v3))))) :named a65))
(assert (! (forall ((?v0 B_a_fun$) (?v1 B_stream$) (?v2 A_stream$)) (= (= (smap$ ?v0 ?v1) ?v2) (forall ((?v3 Nat$)) (= (fun_app$b ?v0 (snth$a ?v1 ?v3)) (snth$c ?v2 ?v3))))) :named a66))
(assert (! (forall ((?v0 B_stream$) (?v1 B_set$) (?v2 B_a_fun$) (?v3 A_set$)) (=> (and (member$ ?v0 (streams$ ?v1)) (forall ((?v4 B$)) (=> (member$a ?v4 ?v1) (member$b (fun_app$b ?v2 ?v4) ?v3)))) (member$c (smap$ ?v2 ?v0) (streams$a ?v3)))) :named a67))
(assert (! (forall ((?v0 A_stream$) (?v1 A_set$) (?v2 A_b_fun$) (?v3 B_set$)) (=> (and (member$c ?v0 (streams$a ?v1)) (forall ((?v4 A$)) (=> (member$b ?v4 ?v1) (member$a (fun_app$m ?v2 ?v4) ?v3)))) (member$ (smap$k ?v2 ?v0) (streams$ ?v3)))) :named a68))
(assert (! (forall ((?v0 A_stream$) (?v1 A_set$) (?v2 A_a_fun$) (?v3 A_set$)) (=> (and (member$c ?v0 (streams$a ?v1)) (forall ((?v4 A$)) (=> (member$b ?v4 ?v1) (member$b (fun_app$f ?v2 ?v4) ?v3)))) (member$c (fun_app$e (smap$b ?v2) ?v0) (streams$a ?v3)))) :named a69))
(assert (! (forall ((?v0 B_stream$) (?v1 B_set$) (?v2 B_b_fun$) (?v3 B_set$)) (=> (and (member$ ?v0 (streams$ ?v1)) (forall ((?v4 B$)) (=> (member$a ?v4 ?v1) (member$a (fun_app$d ?v2 ?v4) ?v3)))) (member$ (fun_app$c (smap$a ?v2) ?v0) (streams$ ?v3)))) :named a70))
(assert (! (forall ((?v0 B_stream_stream$) (?v1 B_stream_set$) (?v2 B_stream_b_fun$) (?v3 B_set$)) (=> (and (member$d ?v0 (streams$b ?v1)) (forall ((?v4 B_stream$)) (=> (member$ ?v4 ?v1) (member$a (fun_app$n ?v2 ?v4) ?v3)))) (member$ (smap$l ?v2 ?v0) (streams$ ?v3)))) :named a71))
(assert (! (forall ((?v0 A_stream_stream$) (?v1 A_stream_set$) (?v2 A_stream_b_fun$) (?v3 B_set$)) (=> (and (member$e ?v0 (streams$c ?v1)) (forall ((?v4 A_stream$)) (=> (member$c ?v4 ?v1) (member$a (fun_app$o ?v2 ?v4) ?v3)))) (member$ (smap$m ?v2 ?v0) (streams$ ?v3)))) :named a72))
(assert (! (forall ((?v0 B_stream_stream$) (?v1 B_stream_set$) (?v2 B_stream_a_fun$) (?v3 A_set$)) (=> (and (member$d ?v0 (streams$b ?v1)) (forall ((?v4 B_stream$)) (=> (member$ ?v4 ?v1) (member$b (fun_app$p ?v2 ?v4) ?v3)))) (member$c (smap$n ?v2 ?v0) (streams$a ?v3)))) :named a73))
(assert (! (forall ((?v0 A_stream_stream$) (?v1 A_stream_set$) (?v2 A_stream_a_fun$) (?v3 A_set$)) (=> (and (member$e ?v0 (streams$c ?v1)) (forall ((?v4 A_stream$)) (=> (member$c ?v4 ?v1) (member$b (fun_app$q ?v2 ?v4) ?v3)))) (member$c (smap$o ?v2 ?v0) (streams$a ?v3)))) :named a74))
(assert (! (forall ((?v0 B_stream$) (?v1 B_set$) (?v2 B_b_stream_fun$) (?v3 B_stream_set$)) (=> (and (member$ ?v0 (streams$ ?v1)) (forall ((?v4 B$)) (=> (member$a ?v4 ?v1) (member$ (fun_app$ ?v2 ?v4) ?v3)))) (member$d (smap$g ?v2 ?v0) (streams$b ?v3)))) :named a75))
(assert (! (forall ((?v0 B_stream$) (?v1 B_set$) (?v2 B_a_stream_fun$) (?v3 A_stream_set$)) (=> (and (member$ ?v0 (streams$ ?v1)) (forall ((?v4 B$)) (=> (member$a ?v4 ?v1) (member$c (fun_app$k ?v2 ?v4) ?v3)))) (member$e (smap$h ?v2 ?v0) (streams$c ?v3)))) :named a76))
(assert (! (forall ((?v0 B_b_fun$) (?v1 B$)) (= (shd$a (fun_app$ (siterate$ ?v0) ?v1)) ?v1)) :named a77))
(assert (! (forall ((?v0 A_a_fun$) (?v1 A$)) (= (shd$ (fun_app$a (siterate$a ?v0) ?v1)) ?v1)) :named a78))
(assert (! (forall ((?v0 B_b_fun$) (?v1 B$)) (= (stl$a (fun_app$ (siterate$ ?v0) ?v1)) (fun_app$ (siterate$ ?v0) (fun_app$d ?v0 ?v1)))) :named a79))
(assert (! (forall ((?v0 A_a_fun$) (?v1 A$)) (= (stl$ (fun_app$a (siterate$a ?v0) ?v1)) (fun_app$a (siterate$a ?v0) (fun_app$f ?v0 ?v1)))) :named a80))
(assert (! (forall ((?v0 B_b_fun$) (?v1 B$)) (= (fun_app$ (siterate$ ?v0) ?v1) (sCons$a ?v1 (fun_app$ (siterate$ ?v0) (fun_app$d ?v0 ?v1))))) :named a81))
(assert (! (forall ((?v0 A_a_fun$) (?v1 A$)) (= (fun_app$a (siterate$a ?v0) ?v1) (sCons$ ?v1 (fun_app$a (siterate$a ?v0) (fun_app$f ?v0 ?v1))))) :named a82))
(check-sat)