test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
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)