diff options
Diffstat (limited to 'test/regress/regress1/quantifiers/stream-x2014-09-18-unsat.smt2')
| -rw-r--r-- | test/regress/regress1/quantifiers/stream-x2014-09-18-unsat.smt2 | 185 |
1 files changed, 185 insertions, 0 deletions
diff --git a/test/regress/regress1/quantifiers/stream-x2014-09-18-unsat.smt2 b/test/regress/regress1/quantifiers/stream-x2014-09-18-unsat.smt2 new file mode 100644 index 000000000..9243654b4 --- /dev/null +++ b/test/regress/regress1/quantifiers/stream-x2014-09-18-unsat.smt2 @@ -0,0 +1,185 @@ +; 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) |