Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Arrays2 / Arrays2.smt2 @ eb639349

History | View | Annotate | Download (121 KB)

1
(declare-datatypes () ((arrays2_arrays2__type POINTArrays2_Arrays2 POINT__TO__ARRAYS2_A_1 ARRAYS2_A__TO__ARRAYS2_B_1 ARRAYS2_B__TO__ARRAYS2_C_1 ARRAYS2_C__TO__ARRAYS2_A_1 ARRAYS2_A_IDL ARRAYS2_B_IDL ARRAYS2_C_IDL)));
2

    
3
; Arrays2_A_ex
4
(declare-var Arrays2_A_ex.idArrays2_Arrays2_1 Int)
5
(declare-var Arrays2_A_ex.isInner Bool)
6
(declare-var Arrays2_A_ex.idArrays2_Arrays2 Int)
7
(declare-var Arrays2_A_ex.idArrays2_Arrays2_2 Int)
8
(declare-rel Arrays2_A_ex (Int Bool Int))
9
(rule (=> 
10
  (and (and (or (not (= (not Arrays2_A_ex.isInner) true))
11
               (= Arrays2_A_ex.idArrays2_Arrays2_2 0))
12
            (or (not (= (not Arrays2_A_ex.isInner) false))
13
               (= Arrays2_A_ex.idArrays2_Arrays2_2 Arrays2_A_ex.idArrays2_Arrays2_1))
14
       )
15
       (= Arrays2_A_ex.idArrays2_Arrays2 Arrays2_A_ex.idArrays2_Arrays2_1)
16
       )
17
  (Arrays2_A_ex Arrays2_A_ex.idArrays2_Arrays2_1 Arrays2_A_ex.isInner Arrays2_A_ex.idArrays2_Arrays2)
18
))
19

    
20
; Arrays2_B_en
21
(declare-var Arrays2_B_en.idArrays2_Arrays2_1 Int)
22
(declare-var Arrays2_B_en.x_1_2_1 Real)
23
(declare-var Arrays2_B_en.x_2_2_1 Real)
24
(declare-var Arrays2_B_en.isInner Bool)
25
(declare-var Arrays2_B_en.idArrays2_Arrays2 Int)
26
(declare-var Arrays2_B_en.x_1_2 Real)
27
(declare-var Arrays2_B_en.x_2_2 Real)
28
(declare-var Arrays2_B_en.__Arrays2_B_en_1 Bool)
29
(declare-var Arrays2_B_en.x_1_2_2 Real)
30
(declare-var Arrays2_B_en.x_2_2_2 Real)
31
(declare-rel Arrays2_B_en (Int Real Real Bool Int Real Real))
32
(rule (=> 
33
  (and (= Arrays2_B_en.__Arrays2_B_en_1 (not Arrays2_B_en.isInner))
34
       (and (or (not (= Arrays2_B_en.__Arrays2_B_en_1 false))
35
               (and (= Arrays2_B_en.x_2_2_2 Arrays2_B_en.x_2_2_1)
36
                    (= Arrays2_B_en.x_1_2_2 Arrays2_B_en.x_1_2_1)
37
                    ))
38
            (or (not (= Arrays2_B_en.__Arrays2_B_en_1 true))
39
               (and (= Arrays2_B_en.x_2_2_2 (- Arrays2_B_en.x_2_2_1 1.))
40
                    (= Arrays2_B_en.x_1_2_2 (+ Arrays2_B_en.x_1_2_1 1.))
41
                    ))
42
       )
43
       (= Arrays2_B_en.x_2_2 Arrays2_B_en.x_2_2_2)
44
       (= Arrays2_B_en.x_1_2 Arrays2_B_en.x_1_2_2)
45
       (= Arrays2_B_en.idArrays2_Arrays2 525)
46
       )
47
  (Arrays2_B_en Arrays2_B_en.idArrays2_Arrays2_1 Arrays2_B_en.x_1_2_1 Arrays2_B_en.x_2_2_1 Arrays2_B_en.isInner Arrays2_B_en.idArrays2_Arrays2 Arrays2_B_en.x_1_2 Arrays2_B_en.x_2_2)
48
))
49

    
50
; Arrays2_B_ex
51
(declare-var Arrays2_B_ex.idArrays2_Arrays2_1 Int)
52
(declare-var Arrays2_B_ex.isInner Bool)
53
(declare-var Arrays2_B_ex.idArrays2_Arrays2 Int)
54
(declare-var Arrays2_B_ex.idArrays2_Arrays2_2 Int)
55
(declare-rel Arrays2_B_ex (Int Bool Int))
56
(rule (=> 
57
  (and (and (or (not (= (not Arrays2_B_ex.isInner) true))
58
               (= Arrays2_B_ex.idArrays2_Arrays2_2 0))
59
            (or (not (= (not Arrays2_B_ex.isInner) false))
60
               (= Arrays2_B_ex.idArrays2_Arrays2_2 Arrays2_B_ex.idArrays2_Arrays2_1))
61
       )
62
       (= Arrays2_B_ex.idArrays2_Arrays2 Arrays2_B_ex.idArrays2_Arrays2_1)
63
       )
64
  (Arrays2_B_ex Arrays2_B_ex.idArrays2_Arrays2_1 Arrays2_B_ex.isInner Arrays2_B_ex.idArrays2_Arrays2)
65
))
66

    
67
; Arrays2_C_en
68
(declare-var Arrays2_C_en.idArrays2_Arrays2_1 Int)
69
(declare-var Arrays2_C_en.x_1_3_1 Real)
70
(declare-var Arrays2_C_en.x_2_3_1 Real)
71
(declare-var Arrays2_C_en.isInner Bool)
72
(declare-var Arrays2_C_en.idArrays2_Arrays2 Int)
73
(declare-var Arrays2_C_en.x_1_3 Real)
74
(declare-var Arrays2_C_en.x_2_3 Real)
75
(declare-var Arrays2_C_en.__Arrays2_C_en_1 Bool)
76
(declare-var Arrays2_C_en.x_1_3_2 Real)
77
(declare-var Arrays2_C_en.x_2_3_2 Real)
78
(declare-rel Arrays2_C_en (Int Real Real Bool Int Real Real))
79
(rule (=> 
80
  (and (= Arrays2_C_en.__Arrays2_C_en_1 (not Arrays2_C_en.isInner))
81
       (and (or (not (= Arrays2_C_en.__Arrays2_C_en_1 false))
82
               (and (= Arrays2_C_en.x_2_3_2 Arrays2_C_en.x_2_3_1)
83
                    (= Arrays2_C_en.x_1_3_2 Arrays2_C_en.x_1_3_1)
84
                    ))
85
            (or (not (= Arrays2_C_en.__Arrays2_C_en_1 true))
86
               (and (= Arrays2_C_en.x_2_3_2 (- Arrays2_C_en.x_2_3_1 1.))
87
                    (= Arrays2_C_en.x_1_3_2 (+ Arrays2_C_en.x_1_3_1 1.))
88
                    ))
89
       )
90
       (= Arrays2_C_en.x_2_3 Arrays2_C_en.x_2_3_2)
91
       (= Arrays2_C_en.x_1_3 Arrays2_C_en.x_1_3_2)
92
       (= Arrays2_C_en.idArrays2_Arrays2 526)
93
       )
94
  (Arrays2_C_en Arrays2_C_en.idArrays2_Arrays2_1 Arrays2_C_en.x_1_3_1 Arrays2_C_en.x_2_3_1 Arrays2_C_en.isInner Arrays2_C_en.idArrays2_Arrays2 Arrays2_C_en.x_1_3 Arrays2_C_en.x_2_3)
95
))
96

    
97
; Arrays2_A_en
98
(declare-var Arrays2_A_en.idArrays2_Arrays2_1 Int)
99
(declare-var Arrays2_A_en.x_1_1_1 Real)
100
(declare-var Arrays2_A_en.x_2_1_1 Real)
101
(declare-var Arrays2_A_en.isInner Bool)
102
(declare-var Arrays2_A_en.idArrays2_Arrays2 Int)
103
(declare-var Arrays2_A_en.x_1_1 Real)
104
(declare-var Arrays2_A_en.x_2_1 Real)
105
(declare-var Arrays2_A_en.__Arrays2_A_en_1 Bool)
106
(declare-var Arrays2_A_en.x_1_1_2 Real)
107
(declare-var Arrays2_A_en.x_2_1_2 Real)
108
(declare-rel Arrays2_A_en (Int Real Real Bool Int Real Real))
109
(rule (=> 
110
  (and (= Arrays2_A_en.__Arrays2_A_en_1 (not Arrays2_A_en.isInner))
111
       (and (or (not (= Arrays2_A_en.__Arrays2_A_en_1 false))
112
               (and (= Arrays2_A_en.x_2_1_2 Arrays2_A_en.x_2_1_1)
113
                    (= Arrays2_A_en.x_1_1_2 Arrays2_A_en.x_1_1_1)
114
                    ))
115
            (or (not (= Arrays2_A_en.__Arrays2_A_en_1 true))
116
               (and (= Arrays2_A_en.x_2_1_2 (- Arrays2_A_en.x_2_1_1 1.))
117
                    (= Arrays2_A_en.x_1_1_2 (+ Arrays2_A_en.x_1_1_1 1.))
118
                    ))
119
       )
120
       (= Arrays2_A_en.x_2_1 Arrays2_A_en.x_2_1_2)
121
       (= Arrays2_A_en.x_1_1 Arrays2_A_en.x_1_1_2)
122
       (= Arrays2_A_en.idArrays2_Arrays2 524)
123
       )
124
  (Arrays2_A_en Arrays2_A_en.idArrays2_Arrays2_1 Arrays2_A_en.x_1_1_1 Arrays2_A_en.x_2_1_1 Arrays2_A_en.isInner Arrays2_A_en.idArrays2_Arrays2 Arrays2_A_en.x_1_1 Arrays2_A_en.x_2_1)
125
))
126

    
127
; Arrays2_C_ex
128
(declare-var Arrays2_C_ex.idArrays2_Arrays2_1 Int)
129
(declare-var Arrays2_C_ex.isInner Bool)
130
(declare-var Arrays2_C_ex.idArrays2_Arrays2 Int)
131
(declare-var Arrays2_C_ex.idArrays2_Arrays2_2 Int)
132
(declare-rel Arrays2_C_ex (Int Bool Int))
133
(rule (=> 
134
  (and (and (or (not (= (not Arrays2_C_ex.isInner) true))
135
               (= Arrays2_C_ex.idArrays2_Arrays2_2 0))
136
            (or (not (= (not Arrays2_C_ex.isInner) false))
137
               (= Arrays2_C_ex.idArrays2_Arrays2_2 Arrays2_C_ex.idArrays2_Arrays2_1))
138
       )
139
       (= Arrays2_C_ex.idArrays2_Arrays2 Arrays2_C_ex.idArrays2_Arrays2_1)
140
       )
141
  (Arrays2_C_ex Arrays2_C_ex.idArrays2_Arrays2_1 Arrays2_C_ex.isInner Arrays2_C_ex.idArrays2_Arrays2)
142
))
143

    
144
; arrays2_arrays2__ARRAYS2_A_IDL_handler_until
145
(declare-var arrays2_arrays2__ARRAYS2_A_IDL_handler_until.idArrays2_Arrays2_1 Int)
146
(declare-var arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_1_1_1 Real)
147
(declare-var arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_2_1_1 Real)
148
(declare-var arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_1_2_1 Real)
149
(declare-var arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_2_2_1 Real)
150
(declare-var arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_1_3_1 Real)
151
(declare-var arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_2_3_1 Real)
152
(declare-var arrays2_arrays2__ARRAYS2_A_IDL_handler_until.arrays2_arrays2__restart_in Bool)
153
(declare-var arrays2_arrays2__ARRAYS2_A_IDL_handler_until.arrays2_arrays2__state_in arrays2_arrays2__type)
154
(declare-var arrays2_arrays2__ARRAYS2_A_IDL_handler_until.idArrays2_Arrays2_out Int)
155
(declare-var arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_1_1_out Real)
156
(declare-var arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_1_2_out Real)
157
(declare-var arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_1_3_out Real)
158
(declare-var arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_2_1_out Real)
159
(declare-var arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_2_2_out Real)
160
(declare-var arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_2_3_out Real)
161
(declare-rel arrays2_arrays2__ARRAYS2_A_IDL_handler_until (Int Real Real Real Real Real Real Bool arrays2_arrays2__type Int Real Real Real Real Real Real))
162
(rule (=> 
163
  (and (= arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_2_3_out arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_2_3_1)
164
       (= arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_2_2_out arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_2_2_1)
165
       (= arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_2_1_out arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_2_1_1)
166
       (= arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_1_3_out arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_1_3_1)
167
       (= arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_1_2_out arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_1_2_1)
168
       (= arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_1_1_out arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_1_1_1)
169
       (= arrays2_arrays2__ARRAYS2_A_IDL_handler_until.idArrays2_Arrays2_out arrays2_arrays2__ARRAYS2_A_IDL_handler_until.idArrays2_Arrays2_1)
170
       (= arrays2_arrays2__ARRAYS2_A_IDL_handler_until.arrays2_arrays2__state_in POINTArrays2_Arrays2)
171
       (= arrays2_arrays2__ARRAYS2_A_IDL_handler_until.arrays2_arrays2__restart_in true)
172
       )
173
  (arrays2_arrays2__ARRAYS2_A_IDL_handler_until arrays2_arrays2__ARRAYS2_A_IDL_handler_until.idArrays2_Arrays2_1 arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_1_1_1 arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_2_1_1 arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_1_2_1 arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_2_2_1 arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_1_3_1 arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_2_3_1 arrays2_arrays2__ARRAYS2_A_IDL_handler_until.arrays2_arrays2__restart_in arrays2_arrays2__ARRAYS2_A_IDL_handler_until.arrays2_arrays2__state_in arrays2_arrays2__ARRAYS2_A_IDL_handler_until.idArrays2_Arrays2_out arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_1_1_out arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_1_2_out arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_1_3_out arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_2_1_out arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_2_2_out arrays2_arrays2__ARRAYS2_A_IDL_handler_until.x_2_3_out)
174
))
175

    
176
; arrays2_arrays2__ARRAYS2_A_IDL_unless
177
(declare-var arrays2_arrays2__ARRAYS2_A_IDL_unless.arrays2_arrays2__restart_in Bool)
178
(declare-var arrays2_arrays2__ARRAYS2_A_IDL_unless.arrays2_arrays2__state_in arrays2_arrays2__type)
179
(declare-var arrays2_arrays2__ARRAYS2_A_IDL_unless.arrays2_arrays2__restart_act Bool)
180
(declare-var arrays2_arrays2__ARRAYS2_A_IDL_unless.arrays2_arrays2__state_act arrays2_arrays2__type)
181
(declare-rel arrays2_arrays2__ARRAYS2_A_IDL_unless (Bool arrays2_arrays2__type Bool arrays2_arrays2__type))
182
(rule (=> 
183
  (and (= arrays2_arrays2__ARRAYS2_A_IDL_unless.arrays2_arrays2__state_act arrays2_arrays2__ARRAYS2_A_IDL_unless.arrays2_arrays2__state_in)
184
       (= arrays2_arrays2__ARRAYS2_A_IDL_unless.arrays2_arrays2__restart_act arrays2_arrays2__ARRAYS2_A_IDL_unless.arrays2_arrays2__restart_in)
185
       )
186
  (arrays2_arrays2__ARRAYS2_A_IDL_unless arrays2_arrays2__ARRAYS2_A_IDL_unless.arrays2_arrays2__restart_in arrays2_arrays2__ARRAYS2_A_IDL_unless.arrays2_arrays2__state_in arrays2_arrays2__ARRAYS2_A_IDL_unless.arrays2_arrays2__restart_act arrays2_arrays2__ARRAYS2_A_IDL_unless.arrays2_arrays2__state_act)
187
))
188

    
189
; arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until
190
(declare-var arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.idArrays2_Arrays2_1 Int)
191
(declare-var arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_1_1_1 Real)
192
(declare-var arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_2_1_1 Real)
193
(declare-var arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_1_2_1 Real)
194
(declare-var arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_2_2_1 Real)
195
(declare-var arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_1_3_1 Real)
196
(declare-var arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_2_3_1 Real)
197
(declare-var arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.arrays2_arrays2__restart_in Bool)
198
(declare-var arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.arrays2_arrays2__state_in arrays2_arrays2__type)
199
(declare-var arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.idArrays2_Arrays2_out Int)
200
(declare-var arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_1_1_out Real)
201
(declare-var arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_1_2_out Real)
202
(declare-var arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_1_3_out Real)
203
(declare-var arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_2_1_out Real)
204
(declare-var arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_2_2_out Real)
205
(declare-var arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_2_3_out Real)
206
(declare-var arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.idArrays2_Arrays2_2 Int)
207
(declare-var arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.idArrays2_Arrays2_3 Int)
208
(declare-var arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_1_2_2 Real)
209
(declare-var arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_2_2_2 Real)
210
(declare-rel arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until (Int Real Real Real Real Real Real Bool arrays2_arrays2__type Int Real Real Real Real Real Real))
211
(rule (=> 
212
  (and (= arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_2_3_out arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_2_3_1)
213
       (Arrays2_A_ex arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.idArrays2_Arrays2_1
214
                     false
215
                     arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.idArrays2_Arrays2_2)
216
       (Arrays2_B_en arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.idArrays2_Arrays2_2
217
                     arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_1_2_1
218
                     arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_2_2_1
219
                     false
220
                     arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.idArrays2_Arrays2_3
221
                     arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_1_2_2
222
                     arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_2_2_2)
223
       (= arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_2_2_out arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_2_2_2)
224
       (= arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_2_1_out arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_2_1_1)
225
       (= arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_1_3_out arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_1_3_1)
226
       (= arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_1_2_out arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_1_2_2)
227
       (= arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_1_1_out arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_1_1_1)
228
       (= arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.idArrays2_Arrays2_out arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.idArrays2_Arrays2_3)
229
       (= arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.arrays2_arrays2__state_in POINTArrays2_Arrays2)
230
       (= arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.arrays2_arrays2__restart_in true)
231
       )
232
  (arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.idArrays2_Arrays2_1 arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_1_1_1 arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_2_1_1 arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_1_2_1 arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_2_2_1 arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_1_3_1 arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_2_3_1 arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.arrays2_arrays2__restart_in arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.arrays2_arrays2__state_in arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.idArrays2_Arrays2_out arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_1_1_out arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_1_2_out arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_1_3_out arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_2_1_out arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_2_2_out arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until.x_2_3_out)
233
))
234

    
235
; arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_unless
236
(declare-var arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_unless.arrays2_arrays2__restart_in Bool)
237
(declare-var arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_unless.arrays2_arrays2__state_in arrays2_arrays2__type)
238
(declare-var arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_unless.arrays2_arrays2__restart_act Bool)
239
(declare-var arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_unless.arrays2_arrays2__state_act arrays2_arrays2__type)
240
(declare-rel arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_unless (Bool arrays2_arrays2__type Bool arrays2_arrays2__type))
241
(rule (=> 
242
  (and (= arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_unless.arrays2_arrays2__state_act arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_unless.arrays2_arrays2__state_in)
243
       (= arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_unless.arrays2_arrays2__restart_act arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_unless.arrays2_arrays2__restart_in)
244
       )
245
  (arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_unless arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_unless.arrays2_arrays2__restart_in arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_unless.arrays2_arrays2__state_in arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_unless.arrays2_arrays2__restart_act arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_unless.arrays2_arrays2__state_act)
246
))
247

    
248
; arrays2_arrays2__ARRAYS2_B_IDL_handler_until
249
(declare-var arrays2_arrays2__ARRAYS2_B_IDL_handler_until.idArrays2_Arrays2_1 Int)
250
(declare-var arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_1_1_1 Real)
251
(declare-var arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_2_1_1 Real)
252
(declare-var arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_1_2_1 Real)
253
(declare-var arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_2_2_1 Real)
254
(declare-var arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_1_3_1 Real)
255
(declare-var arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_2_3_1 Real)
256
(declare-var arrays2_arrays2__ARRAYS2_B_IDL_handler_until.arrays2_arrays2__restart_in Bool)
257
(declare-var arrays2_arrays2__ARRAYS2_B_IDL_handler_until.arrays2_arrays2__state_in arrays2_arrays2__type)
258
(declare-var arrays2_arrays2__ARRAYS2_B_IDL_handler_until.idArrays2_Arrays2_out Int)
259
(declare-var arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_1_1_out Real)
260
(declare-var arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_1_2_out Real)
261
(declare-var arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_1_3_out Real)
262
(declare-var arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_2_1_out Real)
263
(declare-var arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_2_2_out Real)
264
(declare-var arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_2_3_out Real)
265
(declare-rel arrays2_arrays2__ARRAYS2_B_IDL_handler_until (Int Real Real Real Real Real Real Bool arrays2_arrays2__type Int Real Real Real Real Real Real))
266
(rule (=> 
267
  (and (= arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_2_3_out arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_2_3_1)
268
       (= arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_2_2_out arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_2_2_1)
269
       (= arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_2_1_out arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_2_1_1)
270
       (= arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_1_3_out arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_1_3_1)
271
       (= arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_1_2_out arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_1_2_1)
272
       (= arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_1_1_out arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_1_1_1)
273
       (= arrays2_arrays2__ARRAYS2_B_IDL_handler_until.idArrays2_Arrays2_out arrays2_arrays2__ARRAYS2_B_IDL_handler_until.idArrays2_Arrays2_1)
274
       (= arrays2_arrays2__ARRAYS2_B_IDL_handler_until.arrays2_arrays2__state_in POINTArrays2_Arrays2)
275
       (= arrays2_arrays2__ARRAYS2_B_IDL_handler_until.arrays2_arrays2__restart_in true)
276
       )
277
  (arrays2_arrays2__ARRAYS2_B_IDL_handler_until arrays2_arrays2__ARRAYS2_B_IDL_handler_until.idArrays2_Arrays2_1 arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_1_1_1 arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_2_1_1 arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_1_2_1 arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_2_2_1 arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_1_3_1 arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_2_3_1 arrays2_arrays2__ARRAYS2_B_IDL_handler_until.arrays2_arrays2__restart_in arrays2_arrays2__ARRAYS2_B_IDL_handler_until.arrays2_arrays2__state_in arrays2_arrays2__ARRAYS2_B_IDL_handler_until.idArrays2_Arrays2_out arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_1_1_out arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_1_2_out arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_1_3_out arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_2_1_out arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_2_2_out arrays2_arrays2__ARRAYS2_B_IDL_handler_until.x_2_3_out)
278
))
279

    
280
; arrays2_arrays2__ARRAYS2_B_IDL_unless
281
(declare-var arrays2_arrays2__ARRAYS2_B_IDL_unless.arrays2_arrays2__restart_in Bool)
282
(declare-var arrays2_arrays2__ARRAYS2_B_IDL_unless.arrays2_arrays2__state_in arrays2_arrays2__type)
283
(declare-var arrays2_arrays2__ARRAYS2_B_IDL_unless.arrays2_arrays2__restart_act Bool)
284
(declare-var arrays2_arrays2__ARRAYS2_B_IDL_unless.arrays2_arrays2__state_act arrays2_arrays2__type)
285
(declare-rel arrays2_arrays2__ARRAYS2_B_IDL_unless (Bool arrays2_arrays2__type Bool arrays2_arrays2__type))
286
(rule (=> 
287
  (and (= arrays2_arrays2__ARRAYS2_B_IDL_unless.arrays2_arrays2__state_act arrays2_arrays2__ARRAYS2_B_IDL_unless.arrays2_arrays2__state_in)
288
       (= arrays2_arrays2__ARRAYS2_B_IDL_unless.arrays2_arrays2__restart_act arrays2_arrays2__ARRAYS2_B_IDL_unless.arrays2_arrays2__restart_in)
289
       )
290
  (arrays2_arrays2__ARRAYS2_B_IDL_unless arrays2_arrays2__ARRAYS2_B_IDL_unless.arrays2_arrays2__restart_in arrays2_arrays2__ARRAYS2_B_IDL_unless.arrays2_arrays2__state_in arrays2_arrays2__ARRAYS2_B_IDL_unless.arrays2_arrays2__restart_act arrays2_arrays2__ARRAYS2_B_IDL_unless.arrays2_arrays2__state_act)
291
))
292

    
293
; arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until
294
(declare-var arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.idArrays2_Arrays2_1 Int)
295
(declare-var arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_1_1_1 Real)
296
(declare-var arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_2_1_1 Real)
297
(declare-var arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_1_2_1 Real)
298
(declare-var arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_2_2_1 Real)
299
(declare-var arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_1_3_1 Real)
300
(declare-var arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_2_3_1 Real)
301
(declare-var arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.arrays2_arrays2__restart_in Bool)
302
(declare-var arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.arrays2_arrays2__state_in arrays2_arrays2__type)
303
(declare-var arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.idArrays2_Arrays2_out Int)
304
(declare-var arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_1_1_out Real)
305
(declare-var arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_1_2_out Real)
306
(declare-var arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_1_3_out Real)
307
(declare-var arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_2_1_out Real)
308
(declare-var arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_2_2_out Real)
309
(declare-var arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_2_3_out Real)
310
(declare-var arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.idArrays2_Arrays2_2 Int)
311
(declare-var arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.idArrays2_Arrays2_3 Int)
312
(declare-var arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_1_3_2 Real)
313
(declare-var arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_2_3_2 Real)
314
(declare-rel arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until (Int Real Real Real Real Real Real Bool arrays2_arrays2__type Int Real Real Real Real Real Real))
315
(rule (=> 
316
  (and (Arrays2_B_ex arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.idArrays2_Arrays2_1
317
                     false
318
                     arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.idArrays2_Arrays2_2)
319
       (Arrays2_C_en arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.idArrays2_Arrays2_2
320
                     arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_1_3_1
321
                     arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_2_3_1
322
                     false
323
                     arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.idArrays2_Arrays2_3
324
                     arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_1_3_2
325
                     arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_2_3_2)
326
       (= arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_2_3_out arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_2_3_2)
327
       (= arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_2_2_out arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_2_2_1)
328
       (= arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_2_1_out arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_2_1_1)
329
       (= arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_1_3_out arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_1_3_2)
330
       (= arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_1_2_out arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_1_2_1)
331
       (= arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_1_1_out arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_1_1_1)
332
       (= arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.idArrays2_Arrays2_out arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.idArrays2_Arrays2_3)
333
       (= arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.arrays2_arrays2__state_in POINTArrays2_Arrays2)
334
       (= arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.arrays2_arrays2__restart_in true)
335
       )
336
  (arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.idArrays2_Arrays2_1 arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_1_1_1 arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_2_1_1 arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_1_2_1 arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_2_2_1 arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_1_3_1 arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_2_3_1 arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.arrays2_arrays2__restart_in arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.arrays2_arrays2__state_in arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.idArrays2_Arrays2_out arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_1_1_out arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_1_2_out arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_1_3_out arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_2_1_out arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_2_2_out arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until.x_2_3_out)
337
))
338

    
339
; arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_unless
340
(declare-var arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_unless.arrays2_arrays2__restart_in Bool)
341
(declare-var arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_unless.arrays2_arrays2__state_in arrays2_arrays2__type)
342
(declare-var arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_unless.arrays2_arrays2__restart_act Bool)
343
(declare-var arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_unless.arrays2_arrays2__state_act arrays2_arrays2__type)
344
(declare-rel arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_unless (Bool arrays2_arrays2__type Bool arrays2_arrays2__type))
345
(rule (=> 
346
  (and (= arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_unless.arrays2_arrays2__state_act arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_unless.arrays2_arrays2__state_in)
347
       (= arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_unless.arrays2_arrays2__restart_act arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_unless.arrays2_arrays2__restart_in)
348
       )
349
  (arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_unless arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_unless.arrays2_arrays2__restart_in arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_unless.arrays2_arrays2__state_in arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_unless.arrays2_arrays2__restart_act arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_unless.arrays2_arrays2__state_act)
350
))
351

    
352
; arrays2_arrays2__ARRAYS2_C_IDL_handler_until
353
(declare-var arrays2_arrays2__ARRAYS2_C_IDL_handler_until.idArrays2_Arrays2_1 Int)
354
(declare-var arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_1_1_1 Real)
355
(declare-var arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_2_1_1 Real)
356
(declare-var arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_1_2_1 Real)
357
(declare-var arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_2_2_1 Real)
358
(declare-var arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_1_3_1 Real)
359
(declare-var arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_2_3_1 Real)
360
(declare-var arrays2_arrays2__ARRAYS2_C_IDL_handler_until.arrays2_arrays2__restart_in Bool)
361
(declare-var arrays2_arrays2__ARRAYS2_C_IDL_handler_until.arrays2_arrays2__state_in arrays2_arrays2__type)
362
(declare-var arrays2_arrays2__ARRAYS2_C_IDL_handler_until.idArrays2_Arrays2_out Int)
363
(declare-var arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_1_1_out Real)
364
(declare-var arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_1_2_out Real)
365
(declare-var arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_1_3_out Real)
366
(declare-var arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_2_1_out Real)
367
(declare-var arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_2_2_out Real)
368
(declare-var arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_2_3_out Real)
369
(declare-rel arrays2_arrays2__ARRAYS2_C_IDL_handler_until (Int Real Real Real Real Real Real Bool arrays2_arrays2__type Int Real Real Real Real Real Real))
370
(rule (=> 
371
  (and (= arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_2_3_out arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_2_3_1)
372
       (= arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_2_2_out arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_2_2_1)
373
       (= arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_2_1_out arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_2_1_1)
374
       (= arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_1_3_out arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_1_3_1)
375
       (= arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_1_2_out arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_1_2_1)
376
       (= arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_1_1_out arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_1_1_1)
377
       (= arrays2_arrays2__ARRAYS2_C_IDL_handler_until.idArrays2_Arrays2_out arrays2_arrays2__ARRAYS2_C_IDL_handler_until.idArrays2_Arrays2_1)
378
       (= arrays2_arrays2__ARRAYS2_C_IDL_handler_until.arrays2_arrays2__state_in POINTArrays2_Arrays2)
379
       (= arrays2_arrays2__ARRAYS2_C_IDL_handler_until.arrays2_arrays2__restart_in true)
380
       )
381
  (arrays2_arrays2__ARRAYS2_C_IDL_handler_until arrays2_arrays2__ARRAYS2_C_IDL_handler_until.idArrays2_Arrays2_1 arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_1_1_1 arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_2_1_1 arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_1_2_1 arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_2_2_1 arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_1_3_1 arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_2_3_1 arrays2_arrays2__ARRAYS2_C_IDL_handler_until.arrays2_arrays2__restart_in arrays2_arrays2__ARRAYS2_C_IDL_handler_until.arrays2_arrays2__state_in arrays2_arrays2__ARRAYS2_C_IDL_handler_until.idArrays2_Arrays2_out arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_1_1_out arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_1_2_out arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_1_3_out arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_2_1_out arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_2_2_out arrays2_arrays2__ARRAYS2_C_IDL_handler_until.x_2_3_out)
382
))
383

    
384
; arrays2_arrays2__ARRAYS2_C_IDL_unless
385
(declare-var arrays2_arrays2__ARRAYS2_C_IDL_unless.arrays2_arrays2__restart_in Bool)
386
(declare-var arrays2_arrays2__ARRAYS2_C_IDL_unless.arrays2_arrays2__state_in arrays2_arrays2__type)
387
(declare-var arrays2_arrays2__ARRAYS2_C_IDL_unless.arrays2_arrays2__restart_act Bool)
388
(declare-var arrays2_arrays2__ARRAYS2_C_IDL_unless.arrays2_arrays2__state_act arrays2_arrays2__type)
389
(declare-rel arrays2_arrays2__ARRAYS2_C_IDL_unless (Bool arrays2_arrays2__type Bool arrays2_arrays2__type))
390
(rule (=> 
391
  (and (= arrays2_arrays2__ARRAYS2_C_IDL_unless.arrays2_arrays2__state_act arrays2_arrays2__ARRAYS2_C_IDL_unless.arrays2_arrays2__state_in)
392
       (= arrays2_arrays2__ARRAYS2_C_IDL_unless.arrays2_arrays2__restart_act arrays2_arrays2__ARRAYS2_C_IDL_unless.arrays2_arrays2__restart_in)
393
       )
394
  (arrays2_arrays2__ARRAYS2_C_IDL_unless arrays2_arrays2__ARRAYS2_C_IDL_unless.arrays2_arrays2__restart_in arrays2_arrays2__ARRAYS2_C_IDL_unless.arrays2_arrays2__state_in arrays2_arrays2__ARRAYS2_C_IDL_unless.arrays2_arrays2__restart_act arrays2_arrays2__ARRAYS2_C_IDL_unless.arrays2_arrays2__state_act)
395
))
396

    
397
; arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until
398
(declare-var arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.idArrays2_Arrays2_1 Int)
399
(declare-var arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_1_1_1 Real)
400
(declare-var arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_2_1_1 Real)
401
(declare-var arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_1_2_1 Real)
402
(declare-var arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_2_2_1 Real)
403
(declare-var arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_1_3_1 Real)
404
(declare-var arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_2_3_1 Real)
405
(declare-var arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.arrays2_arrays2__restart_in Bool)
406
(declare-var arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.arrays2_arrays2__state_in arrays2_arrays2__type)
407
(declare-var arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.idArrays2_Arrays2_out Int)
408
(declare-var arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_1_1_out Real)
409
(declare-var arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_1_2_out Real)
410
(declare-var arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_1_3_out Real)
411
(declare-var arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_2_1_out Real)
412
(declare-var arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_2_2_out Real)
413
(declare-var arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_2_3_out Real)
414
(declare-var arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.idArrays2_Arrays2_2 Int)
415
(declare-var arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.idArrays2_Arrays2_3 Int)
416
(declare-var arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_1_1_2 Real)
417
(declare-var arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_2_1_2 Real)
418
(declare-rel arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until (Int Real Real Real Real Real Real Bool arrays2_arrays2__type Int Real Real Real Real Real Real))
419
(rule (=> 
420
  (and (= arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_2_3_out arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_2_3_1)
421
       (= arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_2_2_out arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_2_2_1)
422
       (Arrays2_C_ex arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.idArrays2_Arrays2_1
423
                     false
424
                     arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.idArrays2_Arrays2_2)
425
       (Arrays2_A_en arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.idArrays2_Arrays2_2
426
                     arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_1_1_1
427
                     arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_2_1_1
428
                     false
429
                     arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.idArrays2_Arrays2_3
430
                     arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_1_1_2
431
                     arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_2_1_2)
432
       (= arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_2_1_out arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_2_1_2)
433
       (= arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_1_3_out arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_1_3_1)
434
       (= arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_1_2_out arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_1_2_1)
435
       (= arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_1_1_out arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_1_1_2)
436
       (= arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.idArrays2_Arrays2_out arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.idArrays2_Arrays2_3)
437
       (= arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.arrays2_arrays2__state_in POINTArrays2_Arrays2)
438
       (= arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.arrays2_arrays2__restart_in true)
439
       )
440
  (arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.idArrays2_Arrays2_1 arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_1_1_1 arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_2_1_1 arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_1_2_1 arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_2_2_1 arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_1_3_1 arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_2_3_1 arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.arrays2_arrays2__restart_in arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.arrays2_arrays2__state_in arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.idArrays2_Arrays2_out arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_1_1_out arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_1_2_out arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_1_3_out arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_2_1_out arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_2_2_out arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until.x_2_3_out)
441
))
442

    
443
; arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_unless
444
(declare-var arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_unless.arrays2_arrays2__restart_in Bool)
445
(declare-var arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_unless.arrays2_arrays2__state_in arrays2_arrays2__type)
446
(declare-var arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_unless.arrays2_arrays2__restart_act Bool)
447
(declare-var arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_unless.arrays2_arrays2__state_act arrays2_arrays2__type)
448
(declare-rel arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_unless (Bool arrays2_arrays2__type Bool arrays2_arrays2__type))
449
(rule (=> 
450
  (and (= arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_unless.arrays2_arrays2__state_act arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_unless.arrays2_arrays2__state_in)
451
       (= arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_unless.arrays2_arrays2__restart_act arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_unless.arrays2_arrays2__restart_in)
452
       )
453
  (arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_unless arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_unless.arrays2_arrays2__restart_in arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_unless.arrays2_arrays2__state_in arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_unless.arrays2_arrays2__restart_act arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_unless.arrays2_arrays2__state_act)
454
))
455

    
456
; arrays2_arrays2__POINTArrays2_Arrays2_handler_until
457
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_handler_until.idArrays2_Arrays2_1 Int)
458
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_1_1_1 Real)
459
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_2_1_1 Real)
460
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_1_2_1 Real)
461
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_2_2_1 Real)
462
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_1_3_1 Real)
463
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_2_3_1 Real)
464
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_handler_until.arrays2_arrays2__restart_in Bool)
465
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_handler_until.arrays2_arrays2__state_in arrays2_arrays2__type)
466
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_handler_until.idArrays2_Arrays2_out Int)
467
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_1_1_out Real)
468
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_1_2_out Real)
469
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_1_3_out Real)
470
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_2_1_out Real)
471
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_2_2_out Real)
472
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_2_3_out Real)
473
(declare-rel arrays2_arrays2__POINTArrays2_Arrays2_handler_until (Int Real Real Real Real Real Real Bool arrays2_arrays2__type Int Real Real Real Real Real Real))
474
(rule (=> 
475
  (and (= arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_2_3_out arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_2_3_1)
476
       (= arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_2_2_out arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_2_2_1)
477
       (= arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_2_1_out arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_2_1_1)
478
       (= arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_1_3_out arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_1_3_1)
479
       (= arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_1_2_out arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_1_2_1)
480
       (= arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_1_1_out arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_1_1_1)
481
       (= arrays2_arrays2__POINTArrays2_Arrays2_handler_until.idArrays2_Arrays2_out arrays2_arrays2__POINTArrays2_Arrays2_handler_until.idArrays2_Arrays2_1)
482
       (= arrays2_arrays2__POINTArrays2_Arrays2_handler_until.arrays2_arrays2__state_in POINTArrays2_Arrays2)
483
       (= arrays2_arrays2__POINTArrays2_Arrays2_handler_until.arrays2_arrays2__restart_in false)
484
       )
485
  (arrays2_arrays2__POINTArrays2_Arrays2_handler_until arrays2_arrays2__POINTArrays2_Arrays2_handler_until.idArrays2_Arrays2_1 arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_1_1_1 arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_2_1_1 arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_1_2_1 arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_2_2_1 arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_1_3_1 arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_2_3_1 arrays2_arrays2__POINTArrays2_Arrays2_handler_until.arrays2_arrays2__restart_in arrays2_arrays2__POINTArrays2_Arrays2_handler_until.arrays2_arrays2__state_in arrays2_arrays2__POINTArrays2_Arrays2_handler_until.idArrays2_Arrays2_out arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_1_1_out arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_1_2_out arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_1_3_out arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_2_1_out arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_2_2_out arrays2_arrays2__POINTArrays2_Arrays2_handler_until.x_2_3_out)
486
))
487

    
488
; arrays2_arrays2__POINTArrays2_Arrays2_unless
489
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_unless.arrays2_arrays2__restart_in Bool)
490
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_unless.arrays2_arrays2__state_in arrays2_arrays2__type)
491
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_unless.idArrays2_Arrays2_1 Int)
492
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_unless.E Bool)
493
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_unless.arrays2_arrays2__restart_act Bool)
494
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_unless.arrays2_arrays2__state_act arrays2_arrays2__type)
495
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_unless.__arrays2_arrays2__POINTArrays2_Arrays2_unless_1 Bool)
496
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_unless.__arrays2_arrays2__POINTArrays2_Arrays2_unless_2 Bool)
497
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_unless.__arrays2_arrays2__POINTArrays2_Arrays2_unless_3 Bool)
498
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_unless.__arrays2_arrays2__POINTArrays2_Arrays2_unless_4 Bool)
499
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_unless.__arrays2_arrays2__POINTArrays2_Arrays2_unless_5 Bool)
500
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_unless.__arrays2_arrays2__POINTArrays2_Arrays2_unless_6 Bool)
501
(declare-var arrays2_arrays2__POINTArrays2_Arrays2_unless.__arrays2_arrays2__POINTArrays2_Arrays2_unless_7 Bool)
502
(declare-rel arrays2_arrays2__POINTArrays2_Arrays2_unless (Bool arrays2_arrays2__type Int Bool Bool arrays2_arrays2__type))
503
(rule (=> 
504
  (and (= arrays2_arrays2__POINTArrays2_Arrays2_unless.__arrays2_arrays2__POINTArrays2_Arrays2_unless_7 (= arrays2_arrays2__POINTArrays2_Arrays2_unless.idArrays2_Arrays2_1 526))
505
       (= arrays2_arrays2__POINTArrays2_Arrays2_unless.__arrays2_arrays2__POINTArrays2_Arrays2_unless_6 (= arrays2_arrays2__POINTArrays2_Arrays2_unless.idArrays2_Arrays2_1 525))
506
       (= arrays2_arrays2__POINTArrays2_Arrays2_unless.__arrays2_arrays2__POINTArrays2_Arrays2_unless_5 (= arrays2_arrays2__POINTArrays2_Arrays2_unless.idArrays2_Arrays2_1 524))
507
       (= arrays2_arrays2__POINTArrays2_Arrays2_unless.__arrays2_arrays2__POINTArrays2_Arrays2_unless_4 (and (= arrays2_arrays2__POINTArrays2_Arrays2_unless.idArrays2_Arrays2_1 526) arrays2_arrays2__POINTArrays2_Arrays2_unless.E))
508
       (= arrays2_arrays2__POINTArrays2_Arrays2_unless.__arrays2_arrays2__POINTArrays2_Arrays2_unless_3 (and (= arrays2_arrays2__POINTArrays2_Arrays2_unless.idArrays2_Arrays2_1 525) arrays2_arrays2__POINTArrays2_Arrays2_unless.E))
509
       (= arrays2_arrays2__POINTArrays2_Arrays2_unless.__arrays2_arrays2__POINTArrays2_Arrays2_unless_2 (and (= arrays2_arrays2__POINTArrays2_Arrays2_unless.idArrays2_Arrays2_1 524) arrays2_arrays2__POINTArrays2_Arrays2_unless.E))
510
       (= arrays2_arrays2__POINTArrays2_Arrays2_unless.__arrays2_arrays2__POINTArrays2_Arrays2_unless_1 (= arrays2_arrays2__POINTArrays2_Arrays2_unless.idArrays2_Arrays2_1 0))
511
       (and (or (not (= arrays2_arrays2__POINTArrays2_Arrays2_unless.__arrays2_arrays2__POINTArrays2_Arrays2_unless_1 false))
512
               (and (or (not (= arrays2_arrays2__POINTArrays2_Arrays2_unless.__arrays2_arrays2__POINTArrays2_Arrays2_unless_2 false))
513
                       (and (or (not (= arrays2_arrays2__POINTArrays2_Arrays2_unless.__arrays2_arrays2__POINTArrays2_Arrays2_unless_3 false))
514
                               (and (or (not (= arrays2_arrays2__POINTArrays2_Arrays2_unless.__arrays2_arrays2__POINTArrays2_Arrays2_unless_4 false))
515
                                       (and (or (not (= arrays2_arrays2__POINTArrays2_Arrays2_unless.__arrays2_arrays2__POINTArrays2_Arrays2_unless_5 false))
516
                                               (and (or (not (= arrays2_arrays2__POINTArrays2_Arrays2_unless.__arrays2_arrays2__POINTArrays2_Arrays2_unless_6 false))
517
                                                       (and (or (not (= arrays2_arrays2__POINTArrays2_Arrays2_unless.__arrays2_arrays2__POINTArrays2_Arrays2_unless_7 false))
518
                                                               (and (= arrays2_arrays2__POINTArrays2_Arrays2_unless.arrays2_arrays2__state_act arrays2_arrays2__POINTArrays2_Arrays2_unless.arrays2_arrays2__state_in)
519
                                                                    (= arrays2_arrays2__POINTArrays2_Arrays2_unless.arrays2_arrays2__restart_act arrays2_arrays2__POINTArrays2_Arrays2_unless.arrays2_arrays2__restart_in)
520
                                                                    ))
521
                                                            (or (not (= arrays2_arrays2__POINTArrays2_Arrays2_unless.__arrays2_arrays2__POINTArrays2_Arrays2_unless_7 true))
522
                                                               (and (= arrays2_arrays2__POINTArrays2_Arrays2_unless.arrays2_arrays2__state_act ARRAYS2_C_IDL)
523
                                                                    (= arrays2_arrays2__POINTArrays2_Arrays2_unless.arrays2_arrays2__restart_act true)
524
                                                                    ))
525
                                                       ))
526
                                                    (or (not (= arrays2_arrays2__POINTArrays2_Arrays2_unless.__arrays2_arrays2__POINTArrays2_Arrays2_unless_6 true))
527
                                                       (and (= arrays2_arrays2__POINTArrays2_Arrays2_unless.arrays2_arrays2__state_act ARRAYS2_B_IDL)
528
                                                            (= arrays2_arrays2__POINTArrays2_Arrays2_unless.arrays2_arrays2__restart_act true)
529
                                                            ))
530
                                               ))
531
                                            (or (not (= arrays2_arrays2__POINTArrays2_Arrays2_unless.__arrays2_arrays2__POINTArrays2_Arrays2_unless_5 true))
532
                                               (and (= arrays2_arrays2__POINTArrays2_Arrays2_unless.arrays2_arrays2__state_act ARRAYS2_A_IDL)
533
                                                    (= arrays2_arrays2__POINTArrays2_Arrays2_unless.arrays2_arrays2__restart_act true)
534
                                                    ))
535
                                       ))
536
                                    (or (not (= arrays2_arrays2__POINTArrays2_Arrays2_unless.__arrays2_arrays2__POINTArrays2_Arrays2_unless_4 true))
537
                                       (and (= arrays2_arrays2__POINTArrays2_Arrays2_unless.arrays2_arrays2__state_act ARRAYS2_C__TO__ARRAYS2_A_1)
538
                                            (= arrays2_arrays2__POINTArrays2_Arrays2_unless.arrays2_arrays2__restart_act true)
539
                                            ))
540
                               ))
541
                            (or (not (= arrays2_arrays2__POINTArrays2_Arrays2_unless.__arrays2_arrays2__POINTArrays2_Arrays2_unless_3 true))
542
                               (and (= arrays2_arrays2__POINTArrays2_Arrays2_unless.arrays2_arrays2__state_act ARRAYS2_B__TO__ARRAYS2_C_1)
543
                                    (= arrays2_arrays2__POINTArrays2_Arrays2_unless.arrays2_arrays2__restart_act true)
544
                                    ))
545
                       ))
546
                    (or (not (= arrays2_arrays2__POINTArrays2_Arrays2_unless.__arrays2_arrays2__POINTArrays2_Arrays2_unless_2 true))
547
                       (and (= arrays2_arrays2__POINTArrays2_Arrays2_unless.arrays2_arrays2__state_act ARRAYS2_A__TO__ARRAYS2_B_1)
548
                            (= arrays2_arrays2__POINTArrays2_Arrays2_unless.arrays2_arrays2__restart_act true)
549
                            ))
550
               ))
551
            (or (not (= arrays2_arrays2__POINTArrays2_Arrays2_unless.__arrays2_arrays2__POINTArrays2_Arrays2_unless_1 true))
552
               (and (= arrays2_arrays2__POINTArrays2_Arrays2_unless.arrays2_arrays2__state_act POINT__TO__ARRAYS2_A_1)
553
                    (= arrays2_arrays2__POINTArrays2_Arrays2_unless.arrays2_arrays2__restart_act true)
554
                    ))
555
       )
556
       )
557
  (arrays2_arrays2__POINTArrays2_Arrays2_unless arrays2_arrays2__POINTArrays2_Arrays2_unless.arrays2_arrays2__restart_in arrays2_arrays2__POINTArrays2_Arrays2_unless.arrays2_arrays2__state_in arrays2_arrays2__POINTArrays2_Arrays2_unless.idArrays2_Arrays2_1 arrays2_arrays2__POINTArrays2_Arrays2_unless.E arrays2_arrays2__POINTArrays2_Arrays2_unless.arrays2_arrays2__restart_act arrays2_arrays2__POINTArrays2_Arrays2_unless.arrays2_arrays2__state_act)
558
))
559

    
560
; arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until
561
(declare-var arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.idArrays2_Arrays2_1 Int)
562
(declare-var arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_1_1_1 Real)
563
(declare-var arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_2_1_1 Real)
564
(declare-var arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_1_2_1 Real)
565
(declare-var arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_2_2_1 Real)
566
(declare-var arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_1_3_1 Real)
567
(declare-var arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_2_3_1 Real)
568
(declare-var arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.arrays2_arrays2__restart_in Bool)
569
(declare-var arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.arrays2_arrays2__state_in arrays2_arrays2__type)
570
(declare-var arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.idArrays2_Arrays2_out Int)
571
(declare-var arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_1_1_out Real)
572
(declare-var arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_1_2_out Real)
573
(declare-var arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_1_3_out Real)
574
(declare-var arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_2_1_out Real)
575
(declare-var arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_2_2_out Real)
576
(declare-var arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_2_3_out Real)
577
(declare-var arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.idArrays2_Arrays2_2 Int)
578
(declare-var arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_1_1_2 Real)
579
(declare-var arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_2_1_2 Real)
580
(declare-rel arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until (Int Real Real Real Real Real Real Bool arrays2_arrays2__type Int Real Real Real Real Real Real))
581
(rule (=> 
582
  (and (= arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_2_3_out arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_2_3_1)
583
       (= arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_2_2_out arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_2_2_1)
584
       (Arrays2_A_en arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.idArrays2_Arrays2_1
585
                     arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_1_1_1
586
                     arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_2_1_1
587
                     false
588
                     arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.idArrays2_Arrays2_2
589
                     arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_1_1_2
590
                     arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_2_1_2)
591
       (= arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_2_1_out arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_2_1_2)
592
       (= arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_1_3_out arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_1_3_1)
593
       (= arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_1_2_out arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_1_2_1)
594
       (= arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_1_1_out arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_1_1_2)
595
       (= arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.idArrays2_Arrays2_out arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.idArrays2_Arrays2_2)
596
       (= arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.arrays2_arrays2__state_in POINTArrays2_Arrays2)
597
       (= arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.arrays2_arrays2__restart_in true)
598
       )
599
  (arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.idArrays2_Arrays2_1 arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_1_1_1 arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_2_1_1 arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_1_2_1 arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_2_2_1 arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_1_3_1 arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_2_3_1 arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.arrays2_arrays2__restart_in arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.arrays2_arrays2__state_in arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.idArrays2_Arrays2_out arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_1_1_out arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_1_2_out arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_1_3_out arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_2_1_out arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_2_2_out arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until.x_2_3_out)
600
))
601

    
602
; arrays2_arrays2__POINT__TO__ARRAYS2_A_1_unless
603
(declare-var arrays2_arrays2__POINT__TO__ARRAYS2_A_1_unless.arrays2_arrays2__restart_in Bool)
604
(declare-var arrays2_arrays2__POINT__TO__ARRAYS2_A_1_unless.arrays2_arrays2__state_in arrays2_arrays2__type)
605
(declare-var arrays2_arrays2__POINT__TO__ARRAYS2_A_1_unless.arrays2_arrays2__restart_act Bool)
606
(declare-var arrays2_arrays2__POINT__TO__ARRAYS2_A_1_unless.arrays2_arrays2__state_act arrays2_arrays2__type)
607
(declare-rel arrays2_arrays2__POINT__TO__ARRAYS2_A_1_unless (Bool arrays2_arrays2__type Bool arrays2_arrays2__type))
608
(rule (=> 
609
  (and (= arrays2_arrays2__POINT__TO__ARRAYS2_A_1_unless.arrays2_arrays2__state_act arrays2_arrays2__POINT__TO__ARRAYS2_A_1_unless.arrays2_arrays2__state_in)
610
       (= arrays2_arrays2__POINT__TO__ARRAYS2_A_1_unless.arrays2_arrays2__restart_act arrays2_arrays2__POINT__TO__ARRAYS2_A_1_unless.arrays2_arrays2__restart_in)
611
       )
612
  (arrays2_arrays2__POINT__TO__ARRAYS2_A_1_unless arrays2_arrays2__POINT__TO__ARRAYS2_A_1_unless.arrays2_arrays2__restart_in arrays2_arrays2__POINT__TO__ARRAYS2_A_1_unless.arrays2_arrays2__state_in arrays2_arrays2__POINT__TO__ARRAYS2_A_1_unless.arrays2_arrays2__restart_act arrays2_arrays2__POINT__TO__ARRAYS2_A_1_unless.arrays2_arrays2__state_act)
613
))
614

    
615
; Arrays2_Arrays2_node
616
(declare-var Arrays2_Arrays2_node.idArrays2_Arrays2_1 Int)
617
(declare-var Arrays2_Arrays2_node.x_1_1_1 Real)
618
(declare-var Arrays2_Arrays2_node.x_2_1_1 Real)
619
(declare-var Arrays2_Arrays2_node.E Bool)
620
(declare-var Arrays2_Arrays2_node.x_1_2_1 Real)
621
(declare-var Arrays2_Arrays2_node.x_2_2_1 Real)
622
(declare-var Arrays2_Arrays2_node.x_1_3_1 Real)
623
(declare-var Arrays2_Arrays2_node.x_2_3_1 Real)
624
(declare-var Arrays2_Arrays2_node.idArrays2_Arrays2 Int)
625
(declare-var Arrays2_Arrays2_node.x_1_1 Real)
626
(declare-var Arrays2_Arrays2_node.x_2_1 Real)
627
(declare-var Arrays2_Arrays2_node.x_1_2 Real)
628
(declare-var Arrays2_Arrays2_node.x_2_2 Real)
629
(declare-var Arrays2_Arrays2_node.x_1_3 Real)
630
(declare-var Arrays2_Arrays2_node.x_2_3 Real)
631
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_c Bool)
632
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_c arrays2_arrays2__type)
633
(declare-var Arrays2_Arrays2_node.ni_4._arrow._first_c Bool)
634
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_m Bool)
635
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_m arrays2_arrays2__type)
636
(declare-var Arrays2_Arrays2_node.ni_4._arrow._first_m Bool)
637
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_x Bool)
638
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_x arrays2_arrays2__type)
639
(declare-var Arrays2_Arrays2_node.ni_4._arrow._first_x Bool)
640
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_1 Bool)
641
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_10 arrays2_arrays2__type)
642
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_11 Bool)
643
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_12 arrays2_arrays2__type)
644
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_13 Bool)
645
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_14 arrays2_arrays2__type)
646
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_15 Bool)
647
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_16 arrays2_arrays2__type)
648
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_17 Bool)
649
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_18 arrays2_arrays2__type)
650
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_19 Int)
651
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_2 arrays2_arrays2__type)
652
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_20 Real)
653
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_21 Real)
654
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_22 Real)
655
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_23 Real)
656
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_24 Real)
657
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_25 Real)
658
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_26 Bool)
659
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_27 arrays2_arrays2__type)
660
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_28 Int)
661
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_29 Real)
662
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_3 Bool)
663
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_30 Real)
664
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_31 Real)
665
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_32 Real)
666
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_33 Real)
667
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_34 Real)
668
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_35 Bool)
669
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_36 arrays2_arrays2__type)
670
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_37 Int)
671
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_38 Real)
672
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_39 Real)
673
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_4 arrays2_arrays2__type)
674
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_40 Real)
675
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_41 Real)
676
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_42 Real)
677
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_43 Real)
678
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_44 Bool)
679
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_45 arrays2_arrays2__type)
680
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_46 Int)
681
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_47 Real)
682
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_48 Real)
683
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_49 Real)
684
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_5 Bool)
685
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_50 Real)
686
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_51 Real)
687
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_52 Real)
688
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_53 Bool)
689
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_54 arrays2_arrays2__type)
690
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_55 Int)
691
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_56 Real)
692
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_57 Real)
693
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_58 Real)
694
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_59 Real)
695
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_6 arrays2_arrays2__type)
696
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_60 Real)
697
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_61 Real)
698
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_62 Bool)
699
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_63 arrays2_arrays2__type)
700
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_64 Int)
701
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_65 Real)
702
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_66 Real)
703
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_67 Real)
704
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_68 Real)
705
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_69 Real)
706
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_7 Bool)
707
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_70 Real)
708
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_71 Bool)
709
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_72 arrays2_arrays2__type)
710
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_73 Int)
711
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_74 Real)
712
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_75 Real)
713
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_76 Real)
714
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_77 Real)
715
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_78 Real)
716
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_79 Real)
717
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_8 arrays2_arrays2__type)
718
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_80 Bool)
719
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_81 arrays2_arrays2__type)
720
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_82 Int)
721
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_83 Real)
722
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_84 Real)
723
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_85 Real)
724
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_86 Real)
725
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_87 Real)
726
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_88 Real)
727
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_89 Bool)
728
(declare-var Arrays2_Arrays2_node.__Arrays2_Arrays2_node_9 Bool)
729
(declare-var Arrays2_Arrays2_node.arrays2_arrays2__next_restart_in Bool)
730
(declare-var Arrays2_Arrays2_node.arrays2_arrays2__next_state_in arrays2_arrays2__type)
731
(declare-var Arrays2_Arrays2_node.arrays2_arrays2__restart_act Bool)
732
(declare-var Arrays2_Arrays2_node.arrays2_arrays2__restart_in Bool)
733
(declare-var Arrays2_Arrays2_node.arrays2_arrays2__state_act arrays2_arrays2__type)
734
(declare-var Arrays2_Arrays2_node.arrays2_arrays2__state_in arrays2_arrays2__type)
735
(declare-rel Arrays2_Arrays2_node_reset (Bool arrays2_arrays2__type Bool Bool arrays2_arrays2__type Bool))
736
(declare-rel Arrays2_Arrays2_node_step (Int Real Real Bool Real Real Real Real Int Real Real Real Real Real Real Bool arrays2_arrays2__type Bool Bool arrays2_arrays2__type Bool))
737

    
738
(rule (=> 
739
  (and 
740
       (= Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_m Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_c)
741
       (= Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_m Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_c)
742
       (= Arrays2_Arrays2_node.ni_4._arrow._first_m true)
743
  )
744
  (Arrays2_Arrays2_node_reset Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_c
745
                              Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_c
746
                              Arrays2_Arrays2_node.ni_4._arrow._first_c
747
                              Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_m
748
                              Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_m
749
                              Arrays2_Arrays2_node.ni_4._arrow._first_m)
750
))
751

    
752
(rule (=> 
753
  (and (= Arrays2_Arrays2_node.ni_4._arrow._first_m Arrays2_Arrays2_node.ni_4._arrow._first_c)
754
       (and (= Arrays2_Arrays2_node.__Arrays2_Arrays2_node_89 (ite Arrays2_Arrays2_node.ni_4._arrow._first_m true false))
755
            (= Arrays2_Arrays2_node.ni_4._arrow._first_x false))
756
       (and (or (not (= Arrays2_Arrays2_node.__Arrays2_Arrays2_node_89 false))
757
               (and (= Arrays2_Arrays2_node.arrays2_arrays2__state_in Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_c)
758
                    (= Arrays2_Arrays2_node.arrays2_arrays2__restart_in Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_c)
759
                    ))
760
            (or (not (= Arrays2_Arrays2_node.__Arrays2_Arrays2_node_89 true))
761
               (and (= Arrays2_Arrays2_node.arrays2_arrays2__state_in POINTArrays2_Arrays2)
762
                    (= Arrays2_Arrays2_node.arrays2_arrays2__restart_in false)
763
                    ))
764
       )
765
       (and (or (not (= Arrays2_Arrays2_node.arrays2_arrays2__state_in ARRAYS2_A_IDL))
766
               (and (arrays2_arrays2__ARRAYS2_A_IDL_unless Arrays2_Arrays2_node.arrays2_arrays2__restart_in
767
                                                           Arrays2_Arrays2_node.arrays2_arrays2__state_in
768
                                                           Arrays2_Arrays2_node.__Arrays2_Arrays2_node_5
769
                                                           Arrays2_Arrays2_node.__Arrays2_Arrays2_node_6)
770
                    (= Arrays2_Arrays2_node.arrays2_arrays2__state_act Arrays2_Arrays2_node.__Arrays2_Arrays2_node_6)
771
                    (= Arrays2_Arrays2_node.arrays2_arrays2__restart_act Arrays2_Arrays2_node.__Arrays2_Arrays2_node_5)
772
                    ))
773
            (or (not (= Arrays2_Arrays2_node.arrays2_arrays2__state_in ARRAYS2_A__TO__ARRAYS2_B_1))
774
               (and (arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_unless 
775
                    Arrays2_Arrays2_node.arrays2_arrays2__restart_in
776
                    Arrays2_Arrays2_node.arrays2_arrays2__state_in
777
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_11
778
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_12)
779
                    (= Arrays2_Arrays2_node.arrays2_arrays2__state_act Arrays2_Arrays2_node.__Arrays2_Arrays2_node_12)
780
                    (= Arrays2_Arrays2_node.arrays2_arrays2__restart_act Arrays2_Arrays2_node.__Arrays2_Arrays2_node_11)
781
                    ))
782
            (or (not (= Arrays2_Arrays2_node.arrays2_arrays2__state_in ARRAYS2_B_IDL))
783
               (and (arrays2_arrays2__ARRAYS2_B_IDL_unless Arrays2_Arrays2_node.arrays2_arrays2__restart_in
784
                                                           Arrays2_Arrays2_node.arrays2_arrays2__state_in
785
                                                           Arrays2_Arrays2_node.__Arrays2_Arrays2_node_3
786
                                                           Arrays2_Arrays2_node.__Arrays2_Arrays2_node_4)
787
                    (= Arrays2_Arrays2_node.arrays2_arrays2__state_act Arrays2_Arrays2_node.__Arrays2_Arrays2_node_4)
788
                    (= Arrays2_Arrays2_node.arrays2_arrays2__restart_act Arrays2_Arrays2_node.__Arrays2_Arrays2_node_3)
789
                    ))
790
            (or (not (= Arrays2_Arrays2_node.arrays2_arrays2__state_in ARRAYS2_B__TO__ARRAYS2_C_1))
791
               (and (arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_unless 
792
                    Arrays2_Arrays2_node.arrays2_arrays2__restart_in
793
                    Arrays2_Arrays2_node.arrays2_arrays2__state_in
794
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_9
795
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_10)
796
                    (= Arrays2_Arrays2_node.arrays2_arrays2__state_act Arrays2_Arrays2_node.__Arrays2_Arrays2_node_10)
797
                    (= Arrays2_Arrays2_node.arrays2_arrays2__restart_act Arrays2_Arrays2_node.__Arrays2_Arrays2_node_9)
798
                    ))
799
            (or (not (= Arrays2_Arrays2_node.arrays2_arrays2__state_in ARRAYS2_C_IDL))
800
               (and (arrays2_arrays2__ARRAYS2_C_IDL_unless Arrays2_Arrays2_node.arrays2_arrays2__restart_in
801
                                                           Arrays2_Arrays2_node.arrays2_arrays2__state_in
802
                                                           Arrays2_Arrays2_node.__Arrays2_Arrays2_node_1
803
                                                           Arrays2_Arrays2_node.__Arrays2_Arrays2_node_2)
804
                    (= Arrays2_Arrays2_node.arrays2_arrays2__state_act Arrays2_Arrays2_node.__Arrays2_Arrays2_node_2)
805
                    (= Arrays2_Arrays2_node.arrays2_arrays2__restart_act Arrays2_Arrays2_node.__Arrays2_Arrays2_node_1)
806
                    ))
807
            (or (not (= Arrays2_Arrays2_node.arrays2_arrays2__state_in ARRAYS2_C__TO__ARRAYS2_A_1))
808
               (and (arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_unless 
809
                    Arrays2_Arrays2_node.arrays2_arrays2__restart_in
810
                    Arrays2_Arrays2_node.arrays2_arrays2__state_in
811
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_7
812
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_8)
813
                    (= Arrays2_Arrays2_node.arrays2_arrays2__state_act Arrays2_Arrays2_node.__Arrays2_Arrays2_node_8)
814
                    (= Arrays2_Arrays2_node.arrays2_arrays2__restart_act Arrays2_Arrays2_node.__Arrays2_Arrays2_node_7)
815
                    ))
816
            (or (not (= Arrays2_Arrays2_node.arrays2_arrays2__state_in POINTArrays2_Arrays2))
817
               (and (arrays2_arrays2__POINTArrays2_Arrays2_unless Arrays2_Arrays2_node.arrays2_arrays2__restart_in
818
                                                                  Arrays2_Arrays2_node.arrays2_arrays2__state_in
819
                                                                  Arrays2_Arrays2_node.idArrays2_Arrays2_1
820
                                                                  Arrays2_Arrays2_node.E
821
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_15
822
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_16)
823
                    (= Arrays2_Arrays2_node.arrays2_arrays2__state_act Arrays2_Arrays2_node.__Arrays2_Arrays2_node_16)
824
                    (= Arrays2_Arrays2_node.arrays2_arrays2__restart_act Arrays2_Arrays2_node.__Arrays2_Arrays2_node_15)
825
                    ))
826
            (or (not (= Arrays2_Arrays2_node.arrays2_arrays2__state_in POINT__TO__ARRAYS2_A_1))
827
               (and (arrays2_arrays2__POINT__TO__ARRAYS2_A_1_unless Arrays2_Arrays2_node.arrays2_arrays2__restart_in
828
                                                                    Arrays2_Arrays2_node.arrays2_arrays2__state_in
829
                                                                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_13
830
                                                                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_14)
831
                    (= Arrays2_Arrays2_node.arrays2_arrays2__state_act Arrays2_Arrays2_node.__Arrays2_Arrays2_node_14)
832
                    (= Arrays2_Arrays2_node.arrays2_arrays2__restart_act Arrays2_Arrays2_node.__Arrays2_Arrays2_node_13)
833
                    ))
834
       )
835
       (and (or (not (= Arrays2_Arrays2_node.arrays2_arrays2__state_act ARRAYS2_A_IDL))
836
               (and (arrays2_arrays2__ARRAYS2_A_IDL_handler_until Arrays2_Arrays2_node.idArrays2_Arrays2_1
837
                                                                  Arrays2_Arrays2_node.x_1_1_1
838
                                                                  Arrays2_Arrays2_node.x_2_1_1
839
                                                                  Arrays2_Arrays2_node.x_1_2_1
840
                                                                  Arrays2_Arrays2_node.x_2_2_1
841
                                                                  Arrays2_Arrays2_node.x_1_3_1
842
                                                                  Arrays2_Arrays2_node.x_2_3_1
843
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_35
844
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_36
845
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_37
846
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_38
847
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_39
848
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_40
849
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_41
850
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_42
851
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_43)
852
                    (= Arrays2_Arrays2_node.x_2_3 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_43)
853
                    (= Arrays2_Arrays2_node.x_2_2 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_42)
854
                    (= Arrays2_Arrays2_node.x_2_1 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_41)
855
                    (= Arrays2_Arrays2_node.x_1_3 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_40)
856
                    (= Arrays2_Arrays2_node.x_1_2 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_39)
857
                    (= Arrays2_Arrays2_node.x_1_1 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_38)
858
                    (= Arrays2_Arrays2_node.idArrays2_Arrays2 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_37)
859
                    (= Arrays2_Arrays2_node.arrays2_arrays2__next_state_in Arrays2_Arrays2_node.__Arrays2_Arrays2_node_36)
860
                    (= Arrays2_Arrays2_node.arrays2_arrays2__next_restart_in Arrays2_Arrays2_node.__Arrays2_Arrays2_node_35)
861
                    ))
862
            (or (not (= Arrays2_Arrays2_node.arrays2_arrays2__state_act ARRAYS2_A__TO__ARRAYS2_B_1))
863
               (and (arrays2_arrays2__ARRAYS2_A__TO__ARRAYS2_B_1_handler_until 
864
                    Arrays2_Arrays2_node.idArrays2_Arrays2_1
865
                    Arrays2_Arrays2_node.x_1_1_1
866
                    Arrays2_Arrays2_node.x_2_1_1
867
                    Arrays2_Arrays2_node.x_1_2_1
868
                    Arrays2_Arrays2_node.x_2_2_1
869
                    Arrays2_Arrays2_node.x_1_3_1
870
                    Arrays2_Arrays2_node.x_2_3_1
871
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_62
872
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_63
873
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_64
874
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_65
875
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_66
876
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_67
877
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_68
878
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_69
879
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_70)
880
                    (= Arrays2_Arrays2_node.x_2_3 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_70)
881
                    (= Arrays2_Arrays2_node.x_2_2 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_69)
882
                    (= Arrays2_Arrays2_node.x_2_1 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_68)
883
                    (= Arrays2_Arrays2_node.x_1_3 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_67)
884
                    (= Arrays2_Arrays2_node.x_1_2 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_66)
885
                    (= Arrays2_Arrays2_node.x_1_1 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_65)
886
                    (= Arrays2_Arrays2_node.idArrays2_Arrays2 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_64)
887
                    (= Arrays2_Arrays2_node.arrays2_arrays2__next_state_in Arrays2_Arrays2_node.__Arrays2_Arrays2_node_63)
888
                    (= Arrays2_Arrays2_node.arrays2_arrays2__next_restart_in Arrays2_Arrays2_node.__Arrays2_Arrays2_node_62)
889
                    ))
890
            (or (not (= Arrays2_Arrays2_node.arrays2_arrays2__state_act ARRAYS2_B_IDL))
891
               (and (arrays2_arrays2__ARRAYS2_B_IDL_handler_until Arrays2_Arrays2_node.idArrays2_Arrays2_1
892
                                                                  Arrays2_Arrays2_node.x_1_1_1
893
                                                                  Arrays2_Arrays2_node.x_2_1_1
894
                                                                  Arrays2_Arrays2_node.x_1_2_1
895
                                                                  Arrays2_Arrays2_node.x_2_2_1
896
                                                                  Arrays2_Arrays2_node.x_1_3_1
897
                                                                  Arrays2_Arrays2_node.x_2_3_1
898
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_26
899
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_27
900
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_28
901
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_29
902
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_30
903
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_31
904
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_32
905
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_33
906
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_34)
907
                    (= Arrays2_Arrays2_node.x_2_3 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_34)
908
                    (= Arrays2_Arrays2_node.x_2_2 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_33)
909
                    (= Arrays2_Arrays2_node.x_2_1 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_32)
910
                    (= Arrays2_Arrays2_node.x_1_3 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_31)
911
                    (= Arrays2_Arrays2_node.x_1_2 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_30)
912
                    (= Arrays2_Arrays2_node.x_1_1 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_29)
913
                    (= Arrays2_Arrays2_node.idArrays2_Arrays2 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_28)
914
                    (= Arrays2_Arrays2_node.arrays2_arrays2__next_state_in Arrays2_Arrays2_node.__Arrays2_Arrays2_node_27)
915
                    (= Arrays2_Arrays2_node.arrays2_arrays2__next_restart_in Arrays2_Arrays2_node.__Arrays2_Arrays2_node_26)
916
                    ))
917
            (or (not (= Arrays2_Arrays2_node.arrays2_arrays2__state_act ARRAYS2_B__TO__ARRAYS2_C_1))
918
               (and (arrays2_arrays2__ARRAYS2_B__TO__ARRAYS2_C_1_handler_until 
919
                    Arrays2_Arrays2_node.idArrays2_Arrays2_1
920
                    Arrays2_Arrays2_node.x_1_1_1
921
                    Arrays2_Arrays2_node.x_2_1_1
922
                    Arrays2_Arrays2_node.x_1_2_1
923
                    Arrays2_Arrays2_node.x_2_2_1
924
                    Arrays2_Arrays2_node.x_1_3_1
925
                    Arrays2_Arrays2_node.x_2_3_1
926
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_53
927
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_54
928
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_55
929
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_56
930
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_57
931
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_58
932
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_59
933
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_60
934
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_61)
935
                    (= Arrays2_Arrays2_node.x_2_3 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_61)
936
                    (= Arrays2_Arrays2_node.x_2_2 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_60)
937
                    (= Arrays2_Arrays2_node.x_2_1 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_59)
938
                    (= Arrays2_Arrays2_node.x_1_3 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_58)
939
                    (= Arrays2_Arrays2_node.x_1_2 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_57)
940
                    (= Arrays2_Arrays2_node.x_1_1 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_56)
941
                    (= Arrays2_Arrays2_node.idArrays2_Arrays2 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_55)
942
                    (= Arrays2_Arrays2_node.arrays2_arrays2__next_state_in Arrays2_Arrays2_node.__Arrays2_Arrays2_node_54)
943
                    (= Arrays2_Arrays2_node.arrays2_arrays2__next_restart_in Arrays2_Arrays2_node.__Arrays2_Arrays2_node_53)
944
                    ))
945
            (or (not (= Arrays2_Arrays2_node.arrays2_arrays2__state_act ARRAYS2_C_IDL))
946
               (and (arrays2_arrays2__ARRAYS2_C_IDL_handler_until Arrays2_Arrays2_node.idArrays2_Arrays2_1
947
                                                                  Arrays2_Arrays2_node.x_1_1_1
948
                                                                  Arrays2_Arrays2_node.x_2_1_1
949
                                                                  Arrays2_Arrays2_node.x_1_2_1
950
                                                                  Arrays2_Arrays2_node.x_2_2_1
951
                                                                  Arrays2_Arrays2_node.x_1_3_1
952
                                                                  Arrays2_Arrays2_node.x_2_3_1
953
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_17
954
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_18
955
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_19
956
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_20
957
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_21
958
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_22
959
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_23
960
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_24
961
                                                                  Arrays2_Arrays2_node.__Arrays2_Arrays2_node_25)
962
                    (= Arrays2_Arrays2_node.x_2_3 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_25)
963
                    (= Arrays2_Arrays2_node.x_2_2 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_24)
964
                    (= Arrays2_Arrays2_node.x_2_1 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_23)
965
                    (= Arrays2_Arrays2_node.x_1_3 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_22)
966
                    (= Arrays2_Arrays2_node.x_1_2 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_21)
967
                    (= Arrays2_Arrays2_node.x_1_1 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_20)
968
                    (= Arrays2_Arrays2_node.idArrays2_Arrays2 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_19)
969
                    (= Arrays2_Arrays2_node.arrays2_arrays2__next_state_in Arrays2_Arrays2_node.__Arrays2_Arrays2_node_18)
970
                    (= Arrays2_Arrays2_node.arrays2_arrays2__next_restart_in Arrays2_Arrays2_node.__Arrays2_Arrays2_node_17)
971
                    ))
972
            (or (not (= Arrays2_Arrays2_node.arrays2_arrays2__state_act ARRAYS2_C__TO__ARRAYS2_A_1))
973
               (and (arrays2_arrays2__ARRAYS2_C__TO__ARRAYS2_A_1_handler_until 
974
                    Arrays2_Arrays2_node.idArrays2_Arrays2_1
975
                    Arrays2_Arrays2_node.x_1_1_1
976
                    Arrays2_Arrays2_node.x_2_1_1
977
                    Arrays2_Arrays2_node.x_1_2_1
978
                    Arrays2_Arrays2_node.x_2_2_1
979
                    Arrays2_Arrays2_node.x_1_3_1
980
                    Arrays2_Arrays2_node.x_2_3_1
981
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_44
982
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_45
983
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_46
984
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_47
985
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_48
986
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_49
987
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_50
988
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_51
989
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_52)
990
                    (= Arrays2_Arrays2_node.x_2_3 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_52)
991
                    (= Arrays2_Arrays2_node.x_2_2 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_51)
992
                    (= Arrays2_Arrays2_node.x_2_1 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_50)
993
                    (= Arrays2_Arrays2_node.x_1_3 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_49)
994
                    (= Arrays2_Arrays2_node.x_1_2 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_48)
995
                    (= Arrays2_Arrays2_node.x_1_1 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_47)
996
                    (= Arrays2_Arrays2_node.idArrays2_Arrays2 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_46)
997
                    (= Arrays2_Arrays2_node.arrays2_arrays2__next_state_in Arrays2_Arrays2_node.__Arrays2_Arrays2_node_45)
998
                    (= Arrays2_Arrays2_node.arrays2_arrays2__next_restart_in Arrays2_Arrays2_node.__Arrays2_Arrays2_node_44)
999
                    ))
1000
            (or (not (= Arrays2_Arrays2_node.arrays2_arrays2__state_act POINTArrays2_Arrays2))
1001
               (and (arrays2_arrays2__POINTArrays2_Arrays2_handler_until 
1002
                    Arrays2_Arrays2_node.idArrays2_Arrays2_1
1003
                    Arrays2_Arrays2_node.x_1_1_1
1004
                    Arrays2_Arrays2_node.x_2_1_1
1005
                    Arrays2_Arrays2_node.x_1_2_1
1006
                    Arrays2_Arrays2_node.x_2_2_1
1007
                    Arrays2_Arrays2_node.x_1_3_1
1008
                    Arrays2_Arrays2_node.x_2_3_1
1009
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_80
1010
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_81
1011
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_82
1012
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_83
1013
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_84
1014
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_85
1015
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_86
1016
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_87
1017
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_88)
1018
                    (= Arrays2_Arrays2_node.x_2_3 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_88)
1019
                    (= Arrays2_Arrays2_node.x_2_2 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_87)
1020
                    (= Arrays2_Arrays2_node.x_2_1 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_86)
1021
                    (= Arrays2_Arrays2_node.x_1_3 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_85)
1022
                    (= Arrays2_Arrays2_node.x_1_2 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_84)
1023
                    (= Arrays2_Arrays2_node.x_1_1 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_83)
1024
                    (= Arrays2_Arrays2_node.idArrays2_Arrays2 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_82)
1025
                    (= Arrays2_Arrays2_node.arrays2_arrays2__next_state_in Arrays2_Arrays2_node.__Arrays2_Arrays2_node_81)
1026
                    (= Arrays2_Arrays2_node.arrays2_arrays2__next_restart_in Arrays2_Arrays2_node.__Arrays2_Arrays2_node_80)
1027
                    ))
1028
            (or (not (= Arrays2_Arrays2_node.arrays2_arrays2__state_act POINT__TO__ARRAYS2_A_1))
1029
               (and (arrays2_arrays2__POINT__TO__ARRAYS2_A_1_handler_until 
1030
                    Arrays2_Arrays2_node.idArrays2_Arrays2_1
1031
                    Arrays2_Arrays2_node.x_1_1_1
1032
                    Arrays2_Arrays2_node.x_2_1_1
1033
                    Arrays2_Arrays2_node.x_1_2_1
1034
                    Arrays2_Arrays2_node.x_2_2_1
1035
                    Arrays2_Arrays2_node.x_1_3_1
1036
                    Arrays2_Arrays2_node.x_2_3_1
1037
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_71
1038
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_72
1039
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_73
1040
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_74
1041
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_75
1042
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_76
1043
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_77
1044
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_78
1045
                    Arrays2_Arrays2_node.__Arrays2_Arrays2_node_79)
1046
                    (= Arrays2_Arrays2_node.x_2_3 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_79)
1047
                    (= Arrays2_Arrays2_node.x_2_2 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_78)
1048
                    (= Arrays2_Arrays2_node.x_2_1 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_77)
1049
                    (= Arrays2_Arrays2_node.x_1_3 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_76)
1050
                    (= Arrays2_Arrays2_node.x_1_2 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_75)
1051
                    (= Arrays2_Arrays2_node.x_1_1 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_74)
1052
                    (= Arrays2_Arrays2_node.idArrays2_Arrays2 Arrays2_Arrays2_node.__Arrays2_Arrays2_node_73)
1053
                    (= Arrays2_Arrays2_node.arrays2_arrays2__next_state_in Arrays2_Arrays2_node.__Arrays2_Arrays2_node_72)
1054
                    (= Arrays2_Arrays2_node.arrays2_arrays2__next_restart_in Arrays2_Arrays2_node.__Arrays2_Arrays2_node_71)
1055
                    ))
1056
       )
1057
       (= Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_x Arrays2_Arrays2_node.arrays2_arrays2__next_state_in)
1058
       (= Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_x Arrays2_Arrays2_node.arrays2_arrays2__next_restart_in)
1059
       )
1060
  (Arrays2_Arrays2_node_step Arrays2_Arrays2_node.idArrays2_Arrays2_1
1061
                             Arrays2_Arrays2_node.x_1_1_1
1062
                             Arrays2_Arrays2_node.x_2_1_1
1063
                             Arrays2_Arrays2_node.E
1064
                             Arrays2_Arrays2_node.x_1_2_1
1065
                             Arrays2_Arrays2_node.x_2_2_1
1066
                             Arrays2_Arrays2_node.x_1_3_1
1067
                             Arrays2_Arrays2_node.x_2_3_1
1068
                             Arrays2_Arrays2_node.idArrays2_Arrays2
1069
                             Arrays2_Arrays2_node.x_1_1
1070
                             Arrays2_Arrays2_node.x_2_1
1071
                             Arrays2_Arrays2_node.x_1_2
1072
                             Arrays2_Arrays2_node.x_2_2
1073
                             Arrays2_Arrays2_node.x_1_3
1074
                             Arrays2_Arrays2_node.x_2_3
1075
                             Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_c
1076
                             Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_c
1077
                             Arrays2_Arrays2_node.ni_4._arrow._first_c
1078
                             Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_x
1079
                             Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_x
1080
                             Arrays2_Arrays2_node.ni_4._arrow._first_x)
1081
))
1082

    
1083
; Arrays2_Arrays2
1084
(declare-var Arrays2_Arrays2.E Bool)
1085
(declare-var Arrays2_Arrays2.x_1_1 Real)
1086
(declare-var Arrays2_Arrays2.x_1_2 Real)
1087
(declare-var Arrays2_Arrays2.x_1_3 Real)
1088
(declare-var Arrays2_Arrays2.x_2_1 Real)
1089
(declare-var Arrays2_Arrays2.x_2_2 Real)
1090
(declare-var Arrays2_Arrays2.x_2_3 Real)
1091
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_10_c Real)
1092
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_11_c Real)
1093
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_12_c Real)
1094
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_13_c Real)
1095
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_14_c Real)
1096
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_15_c Real)
1097
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_9_c Int)
1098
(declare-var Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_c Bool)
1099
(declare-var Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_c arrays2_arrays2__type)
1100
(declare-var Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.ni_4._arrow._first_c Bool)
1101
(declare-var Arrays2_Arrays2.ni_3._arrow._first_c Bool)
1102
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_10_m Real)
1103
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_11_m Real)
1104
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_12_m Real)
1105
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_13_m Real)
1106
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_14_m Real)
1107
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_15_m Real)
1108
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_9_m Int)
1109
(declare-var Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_m Bool)
1110
(declare-var Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_m arrays2_arrays2__type)
1111
(declare-var Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.ni_4._arrow._first_m Bool)
1112
(declare-var Arrays2_Arrays2.ni_3._arrow._first_m Bool)
1113
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_10_x Real)
1114
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_11_x Real)
1115
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_12_x Real)
1116
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_13_x Real)
1117
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_14_x Real)
1118
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_15_x Real)
1119
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_9_x Int)
1120
(declare-var Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_x Bool)
1121
(declare-var Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_x arrays2_arrays2__type)
1122
(declare-var Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.ni_4._arrow._first_x Bool)
1123
(declare-var Arrays2_Arrays2.ni_3._arrow._first_x Bool)
1124
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_1 Int)
1125
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_2 Real)
1126
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_3 Real)
1127
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_4 Real)
1128
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_5 Real)
1129
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_6 Real)
1130
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_7 Real)
1131
(declare-var Arrays2_Arrays2.__Arrays2_Arrays2_8 Bool)
1132
(declare-var Arrays2_Arrays2.idArrays2_Arrays2 Int)
1133
(declare-var Arrays2_Arrays2.idArrays2_Arrays2_1 Int)
1134
(declare-var Arrays2_Arrays2.x_1_1_1 Real)
1135
(declare-var Arrays2_Arrays2.x_1_2_1 Real)
1136
(declare-var Arrays2_Arrays2.x_1_3_1 Real)
1137
(declare-var Arrays2_Arrays2.x_2_1_1 Real)
1138
(declare-var Arrays2_Arrays2.x_2_2_1 Real)
1139
(declare-var Arrays2_Arrays2.x_2_3_1 Real)
1140
(declare-rel Arrays2_Arrays2_reset (Real Real Real Real Real Real Int Bool arrays2_arrays2__type Bool Bool Real Real Real Real Real Real Int Bool arrays2_arrays2__type Bool Bool))
1141
(declare-rel Arrays2_Arrays2_step (Bool Real Real Real Real Real Real Real Real Real Real Real Real Int Bool arrays2_arrays2__type Bool Bool Real Real Real Real Real Real Int Bool arrays2_arrays2__type Bool Bool))
1142

    
1143
(rule (=> 
1144
  (and 
1145
       (= Arrays2_Arrays2.__Arrays2_Arrays2_10_m Arrays2_Arrays2.__Arrays2_Arrays2_10_c)
1146
       (= Arrays2_Arrays2.__Arrays2_Arrays2_11_m Arrays2_Arrays2.__Arrays2_Arrays2_11_c)
1147
       (= Arrays2_Arrays2.__Arrays2_Arrays2_12_m Arrays2_Arrays2.__Arrays2_Arrays2_12_c)
1148
       (= Arrays2_Arrays2.__Arrays2_Arrays2_13_m Arrays2_Arrays2.__Arrays2_Arrays2_13_c)
1149
       (= Arrays2_Arrays2.__Arrays2_Arrays2_14_m Arrays2_Arrays2.__Arrays2_Arrays2_14_c)
1150
       (= Arrays2_Arrays2.__Arrays2_Arrays2_15_m Arrays2_Arrays2.__Arrays2_Arrays2_15_c)
1151
       (= Arrays2_Arrays2.__Arrays2_Arrays2_9_m Arrays2_Arrays2.__Arrays2_Arrays2_9_c)
1152
       (= Arrays2_Arrays2.ni_3._arrow._first_m true)
1153
       (Arrays2_Arrays2_node_reset Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_c
1154
                                   Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_c
1155
                                   Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.ni_4._arrow._first_c
1156
                                   Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_m
1157
                                   Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_m
1158
                                   Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.ni_4._arrow._first_m)
1159
  )
1160
  (Arrays2_Arrays2_reset Arrays2_Arrays2.__Arrays2_Arrays2_10_c
1161
                         Arrays2_Arrays2.__Arrays2_Arrays2_11_c
1162
                         Arrays2_Arrays2.__Arrays2_Arrays2_12_c
1163
                         Arrays2_Arrays2.__Arrays2_Arrays2_13_c
1164
                         Arrays2_Arrays2.__Arrays2_Arrays2_14_c
1165
                         Arrays2_Arrays2.__Arrays2_Arrays2_15_c
1166
                         Arrays2_Arrays2.__Arrays2_Arrays2_9_c
1167
                         Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_c
1168
                         Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_c
1169
                         Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.ni_4._arrow._first_c
1170
                         Arrays2_Arrays2.ni_3._arrow._first_c
1171
                         Arrays2_Arrays2.__Arrays2_Arrays2_10_m
1172
                         Arrays2_Arrays2.__Arrays2_Arrays2_11_m
1173
                         Arrays2_Arrays2.__Arrays2_Arrays2_12_m
1174
                         Arrays2_Arrays2.__Arrays2_Arrays2_13_m
1175
                         Arrays2_Arrays2.__Arrays2_Arrays2_14_m
1176
                         Arrays2_Arrays2.__Arrays2_Arrays2_15_m
1177
                         Arrays2_Arrays2.__Arrays2_Arrays2_9_m
1178
                         Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_m
1179
                         Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_m
1180
                         Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.ni_4._arrow._first_m
1181
                         Arrays2_Arrays2.ni_3._arrow._first_m)
1182
))
1183

    
1184
(rule (=> 
1185
  (and (= Arrays2_Arrays2.ni_3._arrow._first_m Arrays2_Arrays2.ni_3._arrow._first_c)
1186
       (and (= Arrays2_Arrays2.__Arrays2_Arrays2_8 (ite Arrays2_Arrays2.ni_3._arrow._first_m true false))
1187
            (= Arrays2_Arrays2.ni_3._arrow._first_x false))
1188
       (and (or (not (= Arrays2_Arrays2.__Arrays2_Arrays2_8 false))
1189
               (and (= Arrays2_Arrays2.x_2_3_1 Arrays2_Arrays2.__Arrays2_Arrays2_10_c)
1190
                    (= Arrays2_Arrays2.x_2_2_1 Arrays2_Arrays2.__Arrays2_Arrays2_11_c)
1191
                    (= Arrays2_Arrays2.x_2_1_1 Arrays2_Arrays2.__Arrays2_Arrays2_12_c)
1192
                    (= Arrays2_Arrays2.x_1_3_1 Arrays2_Arrays2.__Arrays2_Arrays2_13_c)
1193
                    (= Arrays2_Arrays2.x_1_2_1 Arrays2_Arrays2.__Arrays2_Arrays2_14_c)
1194
                    (= Arrays2_Arrays2.x_1_1_1 Arrays2_Arrays2.__Arrays2_Arrays2_15_c)
1195
                    (= Arrays2_Arrays2.idArrays2_Arrays2_1 Arrays2_Arrays2.__Arrays2_Arrays2_9_c)
1196
                    ))
1197
            (or (not (= Arrays2_Arrays2.__Arrays2_Arrays2_8 true))
1198
               (and (= Arrays2_Arrays2.x_2_3_1 1.)
1199
                    (= Arrays2_Arrays2.x_2_2_1 1.)
1200
                    (= Arrays2_Arrays2.x_2_1_1 1.)
1201
                    (= Arrays2_Arrays2.x_1_3_1 1.)
1202
                    (= Arrays2_Arrays2.x_1_2_1 1.)
1203
                    (= Arrays2_Arrays2.x_1_1_1 1.)
1204
                    (= Arrays2_Arrays2.idArrays2_Arrays2_1 0)
1205
                    ))
1206
       )
1207
       (and (= Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_m Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_c)
1208
            (= Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_m Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_c)
1209
            (= Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.ni_4._arrow._first_m Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.ni_4._arrow._first_c)
1210
            )
1211
       (Arrays2_Arrays2_node_step Arrays2_Arrays2.idArrays2_Arrays2_1
1212
                                  Arrays2_Arrays2.x_1_1_1
1213
                                  Arrays2_Arrays2.x_2_1_1
1214
                                  Arrays2_Arrays2.E
1215
                                  Arrays2_Arrays2.x_1_2_1
1216
                                  Arrays2_Arrays2.x_2_2_1
1217
                                  Arrays2_Arrays2.x_1_3_1
1218
                                  Arrays2_Arrays2.x_2_3_1
1219
                                  Arrays2_Arrays2.__Arrays2_Arrays2_1
1220
                                  Arrays2_Arrays2.__Arrays2_Arrays2_2
1221
                                  Arrays2_Arrays2.__Arrays2_Arrays2_3
1222
                                  Arrays2_Arrays2.__Arrays2_Arrays2_4
1223
                                  Arrays2_Arrays2.__Arrays2_Arrays2_5
1224
                                  Arrays2_Arrays2.__Arrays2_Arrays2_6
1225
                                  Arrays2_Arrays2.__Arrays2_Arrays2_7
1226
                                  Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_m
1227
                                  Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_m
1228
                                  Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.ni_4._arrow._first_m
1229
                                  Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_x
1230
                                  Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_x
1231
                                  Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.ni_4._arrow._first_x)
1232
       (and (or (not (= Arrays2_Arrays2.E false))
1233
               (and (= Arrays2_Arrays2.x_2_3 Arrays2_Arrays2.x_2_3_1)
1234
                    (= Arrays2_Arrays2.x_2_2 Arrays2_Arrays2.x_2_2_1)
1235
                    (= Arrays2_Arrays2.x_2_1 Arrays2_Arrays2.x_2_1_1)
1236
                    (= Arrays2_Arrays2.x_1_3 Arrays2_Arrays2.x_1_3_1)
1237
                    (= Arrays2_Arrays2.x_1_2 Arrays2_Arrays2.x_1_2_1)
1238
                    (= Arrays2_Arrays2.x_1_1 Arrays2_Arrays2.x_1_1_1)
1239
                    (= Arrays2_Arrays2.idArrays2_Arrays2 Arrays2_Arrays2.idArrays2_Arrays2_1)
1240
                    ))
1241
            (or (not (= Arrays2_Arrays2.E true))
1242
               (and (= Arrays2_Arrays2.x_2_3 Arrays2_Arrays2.__Arrays2_Arrays2_7)
1243
                    (= Arrays2_Arrays2.x_2_2 Arrays2_Arrays2.__Arrays2_Arrays2_5)
1244
                    (= Arrays2_Arrays2.x_2_1 Arrays2_Arrays2.__Arrays2_Arrays2_3)
1245
                    (= Arrays2_Arrays2.x_1_3 Arrays2_Arrays2.__Arrays2_Arrays2_6)
1246
                    (= Arrays2_Arrays2.x_1_2 Arrays2_Arrays2.__Arrays2_Arrays2_4)
1247
                    (= Arrays2_Arrays2.x_1_1 Arrays2_Arrays2.__Arrays2_Arrays2_2)
1248
                    (= Arrays2_Arrays2.idArrays2_Arrays2 Arrays2_Arrays2.__Arrays2_Arrays2_1)
1249
                    ))
1250
       )
1251
       (= Arrays2_Arrays2.__Arrays2_Arrays2_9_x Arrays2_Arrays2.idArrays2_Arrays2)
1252
       (= Arrays2_Arrays2.__Arrays2_Arrays2_15_x Arrays2_Arrays2.x_1_1)
1253
       (= Arrays2_Arrays2.__Arrays2_Arrays2_14_x Arrays2_Arrays2.x_1_2)
1254
       (= Arrays2_Arrays2.__Arrays2_Arrays2_13_x Arrays2_Arrays2.x_1_3)
1255
       (= Arrays2_Arrays2.__Arrays2_Arrays2_12_x Arrays2_Arrays2.x_2_1)
1256
       (= Arrays2_Arrays2.__Arrays2_Arrays2_11_x Arrays2_Arrays2.x_2_2)
1257
       (= Arrays2_Arrays2.__Arrays2_Arrays2_10_x Arrays2_Arrays2.x_2_3)
1258
       )
1259
  (Arrays2_Arrays2_step Arrays2_Arrays2.E
1260
                        Arrays2_Arrays2.x_1_1
1261
                        Arrays2_Arrays2.x_1_2
1262
                        Arrays2_Arrays2.x_1_3
1263
                        Arrays2_Arrays2.x_2_1
1264
                        Arrays2_Arrays2.x_2_2
1265
                        Arrays2_Arrays2.x_2_3
1266
                        Arrays2_Arrays2.__Arrays2_Arrays2_10_c
1267
                        Arrays2_Arrays2.__Arrays2_Arrays2_11_c
1268
                        Arrays2_Arrays2.__Arrays2_Arrays2_12_c
1269
                        Arrays2_Arrays2.__Arrays2_Arrays2_13_c
1270
                        Arrays2_Arrays2.__Arrays2_Arrays2_14_c
1271
                        Arrays2_Arrays2.__Arrays2_Arrays2_15_c
1272
                        Arrays2_Arrays2.__Arrays2_Arrays2_9_c
1273
                        Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_c
1274
                        Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_c
1275
                        Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.ni_4._arrow._first_c
1276
                        Arrays2_Arrays2.ni_3._arrow._first_c
1277
                        Arrays2_Arrays2.__Arrays2_Arrays2_10_x
1278
                        Arrays2_Arrays2.__Arrays2_Arrays2_11_x
1279
                        Arrays2_Arrays2.__Arrays2_Arrays2_12_x
1280
                        Arrays2_Arrays2.__Arrays2_Arrays2_13_x
1281
                        Arrays2_Arrays2.__Arrays2_Arrays2_14_x
1282
                        Arrays2_Arrays2.__Arrays2_Arrays2_15_x
1283
                        Arrays2_Arrays2.__Arrays2_Arrays2_9_x
1284
                        Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_x
1285
                        Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_x
1286
                        Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.ni_4._arrow._first_x
1287
                        Arrays2_Arrays2.ni_3._arrow._first_x)
1288
))
1289

    
1290
; Arrays2
1291
(declare-var Arrays2.In1_1_1 Real)
1292
(declare-var Arrays2.Out1_1_1 Real)
1293
(declare-var Arrays2.Out1_1_2 Real)
1294
(declare-var Arrays2.Out1_1_3 Real)
1295
(declare-var Arrays2.Out1_1_4 Real)
1296
(declare-var Arrays2.Out1_1_5 Real)
1297
(declare-var Arrays2.Out1_1_6 Real)
1298
(declare-var Arrays2.__Arrays2_2_c Real)
1299
(declare-var Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_10_c Real)
1300
(declare-var Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_11_c Real)
1301
(declare-var Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_12_c Real)
1302
(declare-var Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_13_c Real)
1303
(declare-var Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_14_c Real)
1304
(declare-var Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_15_c Real)
1305
(declare-var Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_9_c Int)
1306
(declare-var Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_c Bool)
1307
(declare-var Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_c arrays2_arrays2__type)
1308
(declare-var Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.ni_4._arrow._first_c Bool)
1309
(declare-var Arrays2.ni_0.Arrays2_Arrays2.ni_3._arrow._first_c Bool)
1310
(declare-var Arrays2.ni_1._arrow._first_c Bool)
1311
(declare-var Arrays2.__Arrays2_2_m Real)
1312
(declare-var Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_10_m Real)
1313
(declare-var Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_11_m Real)
1314
(declare-var Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_12_m Real)
1315
(declare-var Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_13_m Real)
1316
(declare-var Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_14_m Real)
1317
(declare-var Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_15_m Real)
1318
(declare-var Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_9_m Int)
1319
(declare-var Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_m Bool)
1320
(declare-var Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_m arrays2_arrays2__type)
1321
(declare-var Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.ni_4._arrow._first_m Bool)
1322
(declare-var Arrays2.ni_0.Arrays2_Arrays2.ni_3._arrow._first_m Bool)
1323
(declare-var Arrays2.ni_1._arrow._first_m Bool)
1324
(declare-var Arrays2.__Arrays2_2_x Real)
1325
(declare-var Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_10_x Real)
1326
(declare-var Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_11_x Real)
1327
(declare-var Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_12_x Real)
1328
(declare-var Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_13_x Real)
1329
(declare-var Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_14_x Real)
1330
(declare-var Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_15_x Real)
1331
(declare-var Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_9_x Int)
1332
(declare-var Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_x Bool)
1333
(declare-var Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_x arrays2_arrays2__type)
1334
(declare-var Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.ni_4._arrow._first_x Bool)
1335
(declare-var Arrays2.ni_0.Arrays2_Arrays2.ni_3._arrow._first_x Bool)
1336
(declare-var Arrays2.ni_1._arrow._first_x Bool)
1337
(declare-var Arrays2.Arrays2In1_1_1_event Bool)
1338
(declare-var Arrays2.Arrays2_1_1 Real)
1339
(declare-var Arrays2.Arrays2_1_2 Real)
1340
(declare-var Arrays2.Arrays2_1_3 Real)
1341
(declare-var Arrays2.Arrays2_1_4 Real)
1342
(declare-var Arrays2.Arrays2_1_5 Real)
1343
(declare-var Arrays2.Arrays2_1_6 Real)
1344
(declare-var Arrays2.__Arrays2_1 Bool)
1345
(declare-var Arrays2.i_virtual_local Real)
1346
(declare-rel Arrays2_reset (Real Real Real Real Real Real Real Int Bool arrays2_arrays2__type Bool Bool Bool Real Real Real Real Real Real Real Int Bool arrays2_arrays2__type Bool Bool Bool))
1347
(declare-rel Arrays2_step (Real Real Real Real Real Real Real Real Real Real Real Real Real Real Int Bool arrays2_arrays2__type Bool Bool Bool Real Real Real Real Real Real Real Int Bool arrays2_arrays2__type Bool Bool Bool))
1348

    
1349
(rule (=> 
1350
  (and 
1351
       (= Arrays2.__Arrays2_2_m Arrays2.__Arrays2_2_c)
1352
       (= Arrays2.ni_1._arrow._first_m true)
1353
       (Arrays2_Arrays2_reset Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_10_c
1354
                              Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_11_c
1355
                              Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_12_c
1356
                              Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_13_c
1357
                              Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_14_c
1358
                              Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_15_c
1359
                              Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_9_c
1360
                              Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_c
1361
                              Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_c
1362
                              Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.ni_4._arrow._first_c
1363
                              Arrays2.ni_0.Arrays2_Arrays2.ni_3._arrow._first_c
1364
                              Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_10_m
1365
                              Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_11_m
1366
                              Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_12_m
1367
                              Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_13_m
1368
                              Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_14_m
1369
                              Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_15_m
1370
                              Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_9_m
1371
                              Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_m
1372
                              Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_m
1373
                              Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.ni_4._arrow._first_m
1374
                              Arrays2.ni_0.Arrays2_Arrays2.ni_3._arrow._first_m)
1375
  )
1376
  (Arrays2_reset Arrays2.__Arrays2_2_c
1377
                 Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_10_c
1378
                 Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_11_c
1379
                 Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_12_c
1380
                 Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_13_c
1381
                 Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_14_c
1382
                 Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_15_c
1383
                 Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_9_c
1384
                 Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_c
1385
                 Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_c
1386
                 Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.ni_4._arrow._first_c
1387
                 Arrays2.ni_0.Arrays2_Arrays2.ni_3._arrow._first_c
1388
                 Arrays2.ni_1._arrow._first_c
1389
                 Arrays2.__Arrays2_2_m
1390
                 Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_10_m
1391
                 Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_11_m
1392
                 Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_12_m
1393
                 Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_13_m
1394
                 Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_14_m
1395
                 Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_15_m
1396
                 Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_9_m
1397
                 Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_m
1398
                 Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_m
1399
                 Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.ni_4._arrow._first_m
1400
                 Arrays2.ni_0.Arrays2_Arrays2.ni_3._arrow._first_m
1401
                 Arrays2.ni_1._arrow._first_m)
1402
))
1403

    
1404
(rule (=> 
1405
  (and (= Arrays2.ni_1._arrow._first_m Arrays2.ni_1._arrow._first_c)(and (= Arrays2.__Arrays2_1 (ite Arrays2.ni_1._arrow._first_m true false))
1406
                                                                    (= Arrays2.ni_1._arrow._first_x false))
1407
       (and (or (not (= Arrays2.__Arrays2_1 false))
1408
               (and (= Arrays2.i_virtual_local 1.)
1409
                    (= Arrays2.Arrays2In1_1_1_event (and (<= Arrays2.__Arrays2_2_c 0.) (> Arrays2.In1_1_1 0.)))
1410
                    ))
1411
            (or (not (= Arrays2.__Arrays2_1 true))
1412
               (and (= Arrays2.i_virtual_local 0.)
1413
                    (= Arrays2.Arrays2In1_1_1_event false)
1414
                    ))
1415
       )
1416
       (= Arrays2.__Arrays2_2_x Arrays2.In1_1_1)
1417
       (and (= Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_10_m Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_10_c)
1418
            (= Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_11_m Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_11_c)
1419
            (= Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_12_m Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_12_c)
1420
            (= Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_13_m Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_13_c)
1421
            (= Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_14_m Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_14_c)
1422
            (= Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_15_m Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_15_c)
1423
            (= Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_9_m Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_9_c)
1424
            (= Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_m Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_c)
1425
            (= Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_m Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_c)
1426
            (= Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.ni_4._arrow._first_m Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.ni_4._arrow._first_c)
1427
            (= Arrays2.ni_0.Arrays2_Arrays2.ni_3._arrow._first_m Arrays2.ni_0.Arrays2_Arrays2.ni_3._arrow._first_c)
1428
            )
1429
       (Arrays2_Arrays2_step Arrays2.Arrays2In1_1_1_event
1430
                             Arrays2.Arrays2_1_1
1431
                             Arrays2.Arrays2_1_2
1432
                             Arrays2.Arrays2_1_3
1433
                             Arrays2.Arrays2_1_4
1434
                             Arrays2.Arrays2_1_5
1435
                             Arrays2.Arrays2_1_6
1436
                             Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_10_m
1437
                             Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_11_m
1438
                             Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_12_m
1439
                             Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_13_m
1440
                             Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_14_m
1441
                             Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_15_m
1442
                             Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_9_m
1443
                             Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_m
1444
                             Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_m
1445
                             Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.ni_4._arrow._first_m
1446
                             Arrays2.ni_0.Arrays2_Arrays2.ni_3._arrow._first_m
1447
                             Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_10_x
1448
                             Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_11_x
1449
                             Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_12_x
1450
                             Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_13_x
1451
                             Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_14_x
1452
                             Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_15_x
1453
                             Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_9_x
1454
                             Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_x
1455
                             Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_x
1456
                             Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.ni_4._arrow._first_x
1457
                             Arrays2.ni_0.Arrays2_Arrays2.ni_3._arrow._first_x)
1458
       (= Arrays2.Out1_1_6 Arrays2.Arrays2_1_6)
1459
       (= Arrays2.Out1_1_5 Arrays2.Arrays2_1_5)
1460
       (= Arrays2.Out1_1_4 Arrays2.Arrays2_1_4)
1461
       (= Arrays2.Out1_1_3 Arrays2.Arrays2_1_3)
1462
       (= Arrays2.Out1_1_2 Arrays2.Arrays2_1_2)
1463
       (= Arrays2.Out1_1_1 Arrays2.Arrays2_1_1)
1464
       )
1465
  (Arrays2_step Arrays2.In1_1_1
1466
                Arrays2.Out1_1_1
1467
                Arrays2.Out1_1_2
1468
                Arrays2.Out1_1_3
1469
                Arrays2.Out1_1_4
1470
                Arrays2.Out1_1_5
1471
                Arrays2.Out1_1_6
1472
                Arrays2.__Arrays2_2_c
1473
                Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_10_c
1474
                Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_11_c
1475
                Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_12_c
1476
                Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_13_c
1477
                Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_14_c
1478
                Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_15_c
1479
                Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_9_c
1480
                Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_c
1481
                Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_c
1482
                Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.ni_4._arrow._first_c
1483
                Arrays2.ni_0.Arrays2_Arrays2.ni_3._arrow._first_c
1484
                Arrays2.ni_1._arrow._first_c
1485
                Arrays2.__Arrays2_2_x
1486
                Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_10_x
1487
                Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_11_x
1488
                Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_12_x
1489
                Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_13_x
1490
                Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_14_x
1491
                Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_15_x
1492
                Arrays2.ni_0.Arrays2_Arrays2.__Arrays2_Arrays2_9_x
1493
                Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_90_x
1494
                Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.__Arrays2_Arrays2_node_91_x
1495
                Arrays2.ni_0.Arrays2_Arrays2.ni_2.Arrays2_Arrays2_node.ni_4._arrow._first_x
1496
                Arrays2.ni_0.Arrays2_Arrays2.ni_3._arrow._first_x
1497
                Arrays2.ni_1._arrow._first_x)
1498
))
1499