Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Outer1 / Outer1.smt2 @ eb639349

History | View | Annotate | Download (60.7 KB)

1
(declare-datatypes () ((outer1_outer1__type POINTOuter1_Outer1 POINT__TO__OUTER1_A_1 OUTER1_A__TO__OUTER1_A_1 OUTER1_A_IDL)));
2

    
3
; Outer1_A__To__Outer1_A_1_Condition_Action
4
(declare-var Outer1_A__To__Outer1_A_1_Condition_Action.x_1 Int)
5
(declare-var Outer1_A__To__Outer1_A_1_Condition_Action.x Int)
6
(declare-rel Outer1_A__To__Outer1_A_1_Condition_Action (Int Int))
7
(rule (=> 
8
  (= Outer1_A__To__Outer1_A_1_Condition_Action.x (+ Outer1_A__To__Outer1_A_1_Condition_Action.x_1 1))
9
  (Outer1_A__To__Outer1_A_1_Condition_Action Outer1_A__To__Outer1_A_1_Condition_Action.x_1 Outer1_A__To__Outer1_A_1_Condition_Action.x)
10
))
11

    
12
; Outer1_A__To__Outer1_A_1_Transition_Action
13
(declare-var Outer1_A__To__Outer1_A_1_Transition_Action.y_1 Int)
14
(declare-var Outer1_A__To__Outer1_A_1_Transition_Action.y Int)
15
(declare-rel Outer1_A__To__Outer1_A_1_Transition_Action (Int Int))
16
(rule (=> 
17
  (= Outer1_A__To__Outer1_A_1_Transition_Action.y (+ Outer1_A__To__Outer1_A_1_Transition_Action.y_1 1))
18
  (Outer1_A__To__Outer1_A_1_Transition_Action Outer1_A__To__Outer1_A_1_Transition_Action.y_1 Outer1_A__To__Outer1_A_1_Transition_Action.y)
19
))
20

    
21
; Outer1_A_en
22
(declare-var Outer1_A_en.idOuter1_Outer1_1 Int)
23
(declare-var Outer1_A_en.z_1 Int)
24
(declare-var Outer1_A_en.isInner Bool)
25
(declare-var Outer1_A_en.idOuter1_Outer1 Int)
26
(declare-var Outer1_A_en.z Int)
27
(declare-var Outer1_A_en.z_2 Int)
28
(declare-rel Outer1_A_en (Int Int Bool Int Int))
29
(rule (=> 
30
  (and (and (or (not (= (not Outer1_A_en.isInner) true))
31
               (= Outer1_A_en.z_2 (+ Outer1_A_en.z_1 1)))
32
            (or (not (= (not Outer1_A_en.isInner) false))
33
               (= Outer1_A_en.z_2 Outer1_A_en.z_1))
34
       )
35
       (= Outer1_A_en.z Outer1_A_en.z_2)
36
       (= Outer1_A_en.idOuter1_Outer1 1360)
37
       )
38
  (Outer1_A_en Outer1_A_en.idOuter1_Outer1_1 Outer1_A_en.z_1 Outer1_A_en.isInner Outer1_A_en.idOuter1_Outer1 Outer1_A_en.z)
39
))
40

    
41
; Outer1_A_ex
42
(declare-var Outer1_A_ex.w_1 Int)
43
(declare-var Outer1_A_ex.idOuter1_Outer1_1 Int)
44
(declare-var Outer1_A_ex.isInner Bool)
45
(declare-var Outer1_A_ex.w Int)
46
(declare-var Outer1_A_ex.idOuter1_Outer1 Int)
47
(declare-var Outer1_A_ex.__Outer1_A_ex_1 Bool)
48
(declare-var Outer1_A_ex.idOuter1_Outer1_2 Int)
49
(declare-var Outer1_A_ex.w_2 Int)
50
(declare-rel Outer1_A_ex (Int Int Bool Int Int))
51
(rule (=> 
52
  (and (= Outer1_A_ex.__Outer1_A_ex_1 (not Outer1_A_ex.isInner))
53
       (and (or (not (= Outer1_A_ex.__Outer1_A_ex_1 false))
54
               (and (= Outer1_A_ex.w_2 Outer1_A_ex.w_1)
55
                    (= Outer1_A_ex.idOuter1_Outer1_2 Outer1_A_ex.idOuter1_Outer1_1)
56
                    ))
57
            (or (not (= Outer1_A_ex.__Outer1_A_ex_1 true))
58
               (and (= Outer1_A_ex.w_2 (+ Outer1_A_ex.w_1 1))
59
                    (= Outer1_A_ex.idOuter1_Outer1_2 0)
60
                    ))
61
       )
62
       (= Outer1_A_ex.w Outer1_A_ex.w_2)
63
       (= Outer1_A_ex.idOuter1_Outer1 Outer1_A_ex.idOuter1_Outer1_1)
64
       )
65
  (Outer1_A_ex Outer1_A_ex.w_1 Outer1_A_ex.idOuter1_Outer1_1 Outer1_A_ex.isInner Outer1_A_ex.w Outer1_A_ex.idOuter1_Outer1)
66
))
67

    
68
; outer1_outer1__OUTER1_A_IDL_handler_until
69
(declare-var outer1_outer1__OUTER1_A_IDL_handler_until.idOuter1_Outer1_1 Int)
70
(declare-var outer1_outer1__OUTER1_A_IDL_handler_until.z_1 Int)
71
(declare-var outer1_outer1__OUTER1_A_IDL_handler_until.x_1 Int)
72
(declare-var outer1_outer1__OUTER1_A_IDL_handler_until.w_1 Int)
73
(declare-var outer1_outer1__OUTER1_A_IDL_handler_until.y_1 Int)
74
(declare-var outer1_outer1__OUTER1_A_IDL_handler_until.outer1_outer1__restart_in Bool)
75
(declare-var outer1_outer1__OUTER1_A_IDL_handler_until.outer1_outer1__state_in outer1_outer1__type)
76
(declare-var outer1_outer1__OUTER1_A_IDL_handler_until.idOuter1_Outer1_out Int)
77
(declare-var outer1_outer1__OUTER1_A_IDL_handler_until.w_out Int)
78
(declare-var outer1_outer1__OUTER1_A_IDL_handler_until.x_out Int)
79
(declare-var outer1_outer1__OUTER1_A_IDL_handler_until.y_out Int)
80
(declare-var outer1_outer1__OUTER1_A_IDL_handler_until.z_out Int)
81
(declare-rel outer1_outer1__OUTER1_A_IDL_handler_until (Int Int Int Int Int Bool outer1_outer1__type Int Int Int Int Int))
82
(rule (=> 
83
  (and (= outer1_outer1__OUTER1_A_IDL_handler_until.z_out outer1_outer1__OUTER1_A_IDL_handler_until.z_1)
84
       (= outer1_outer1__OUTER1_A_IDL_handler_until.y_out outer1_outer1__OUTER1_A_IDL_handler_until.y_1)
85
       (= outer1_outer1__OUTER1_A_IDL_handler_until.x_out outer1_outer1__OUTER1_A_IDL_handler_until.x_1)
86
       (= outer1_outer1__OUTER1_A_IDL_handler_until.w_out outer1_outer1__OUTER1_A_IDL_handler_until.w_1)
87
       (= outer1_outer1__OUTER1_A_IDL_handler_until.outer1_outer1__state_in POINTOuter1_Outer1)
88
       (= outer1_outer1__OUTER1_A_IDL_handler_until.outer1_outer1__restart_in true)
89
       (= outer1_outer1__OUTER1_A_IDL_handler_until.idOuter1_Outer1_out outer1_outer1__OUTER1_A_IDL_handler_until.idOuter1_Outer1_1)
90
       )
91
  (outer1_outer1__OUTER1_A_IDL_handler_until outer1_outer1__OUTER1_A_IDL_handler_until.idOuter1_Outer1_1 outer1_outer1__OUTER1_A_IDL_handler_until.z_1 outer1_outer1__OUTER1_A_IDL_handler_until.x_1 outer1_outer1__OUTER1_A_IDL_handler_until.w_1 outer1_outer1__OUTER1_A_IDL_handler_until.y_1 outer1_outer1__OUTER1_A_IDL_handler_until.outer1_outer1__restart_in outer1_outer1__OUTER1_A_IDL_handler_until.outer1_outer1__state_in outer1_outer1__OUTER1_A_IDL_handler_until.idOuter1_Outer1_out outer1_outer1__OUTER1_A_IDL_handler_until.w_out outer1_outer1__OUTER1_A_IDL_handler_until.x_out outer1_outer1__OUTER1_A_IDL_handler_until.y_out outer1_outer1__OUTER1_A_IDL_handler_until.z_out)
92
))
93

    
94
; outer1_outer1__OUTER1_A_IDL_unless
95
(declare-var outer1_outer1__OUTER1_A_IDL_unless.outer1_outer1__restart_in Bool)
96
(declare-var outer1_outer1__OUTER1_A_IDL_unless.outer1_outer1__state_in outer1_outer1__type)
97
(declare-var outer1_outer1__OUTER1_A_IDL_unless.outer1_outer1__restart_act Bool)
98
(declare-var outer1_outer1__OUTER1_A_IDL_unless.outer1_outer1__state_act outer1_outer1__type)
99
(declare-rel outer1_outer1__OUTER1_A_IDL_unless (Bool outer1_outer1__type Bool outer1_outer1__type))
100
(rule (=> 
101
  (and (= outer1_outer1__OUTER1_A_IDL_unless.outer1_outer1__state_act outer1_outer1__OUTER1_A_IDL_unless.outer1_outer1__state_in)
102
       (= outer1_outer1__OUTER1_A_IDL_unless.outer1_outer1__restart_act outer1_outer1__OUTER1_A_IDL_unless.outer1_outer1__restart_in)
103
       )
104
  (outer1_outer1__OUTER1_A_IDL_unless outer1_outer1__OUTER1_A_IDL_unless.outer1_outer1__restart_in outer1_outer1__OUTER1_A_IDL_unless.outer1_outer1__state_in outer1_outer1__OUTER1_A_IDL_unless.outer1_outer1__restart_act outer1_outer1__OUTER1_A_IDL_unless.outer1_outer1__state_act)
105
))
106

    
107
; outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until
108
(declare-var outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.idOuter1_Outer1_1 Int)
109
(declare-var outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.z_1 Int)
110
(declare-var outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.x_1 Int)
111
(declare-var outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.w_1 Int)
112
(declare-var outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.y_1 Int)
113
(declare-var outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.outer1_outer1__restart_in Bool)
114
(declare-var outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.outer1_outer1__state_in outer1_outer1__type)
115
(declare-var outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.idOuter1_Outer1_out Int)
116
(declare-var outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.w_out Int)
117
(declare-var outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.x_out Int)
118
(declare-var outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.y_out Int)
119
(declare-var outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.z_out Int)
120
(declare-var outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.idOuter1_Outer1_2 Int)
121
(declare-var outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.idOuter1_Outer1_3 Int)
122
(declare-var outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.w_2 Int)
123
(declare-var outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.x_2 Int)
124
(declare-var outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.y_2 Int)
125
(declare-var outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.z_2 Int)
126
(declare-rel outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until (Int Int Int Int Int Bool outer1_outer1__type Int Int Int Int Int))
127
(rule (=> 
128
  (and (Outer1_A_ex outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.w_1
129
                    outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.idOuter1_Outer1_1
130
                    false
131
                    outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.w_2
132
                    outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.idOuter1_Outer1_2)
133
       (Outer1_A_en outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.idOuter1_Outer1_2
134
                    outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.z_1
135
                    false
136
                    outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.idOuter1_Outer1_3
137
                    outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.z_2)
138
       (= outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.z_out outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.z_2)
139
       (Outer1_A__To__Outer1_A_1_Transition_Action outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.y_1
140
                                                   outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.y_2)
141
       (= outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.y_out outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.y_2)
142
       (Outer1_A__To__Outer1_A_1_Condition_Action outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.x_1
143
                                                  outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.x_2)
144
       (= outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.x_out outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.x_2)
145
       (= outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.w_out outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.w_2)
146
       (= outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.outer1_outer1__state_in POINTOuter1_Outer1)
147
       (= outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.outer1_outer1__restart_in true)
148
       (= outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.idOuter1_Outer1_out outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.idOuter1_Outer1_3)
149
       )
150
  (outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.idOuter1_Outer1_1 outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.z_1 outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.x_1 outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.w_1 outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.y_1 outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.outer1_outer1__restart_in outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.outer1_outer1__state_in outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.idOuter1_Outer1_out outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.w_out outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.x_out outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.y_out outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until.z_out)
151
))
152

    
153
; outer1_outer1__OUTER1_A__TO__OUTER1_A_1_unless
154
(declare-var outer1_outer1__OUTER1_A__TO__OUTER1_A_1_unless.outer1_outer1__restart_in Bool)
155
(declare-var outer1_outer1__OUTER1_A__TO__OUTER1_A_1_unless.outer1_outer1__state_in outer1_outer1__type)
156
(declare-var outer1_outer1__OUTER1_A__TO__OUTER1_A_1_unless.outer1_outer1__restart_act Bool)
157
(declare-var outer1_outer1__OUTER1_A__TO__OUTER1_A_1_unless.outer1_outer1__state_act outer1_outer1__type)
158
(declare-rel outer1_outer1__OUTER1_A__TO__OUTER1_A_1_unless (Bool outer1_outer1__type Bool outer1_outer1__type))
159
(rule (=> 
160
  (and (= outer1_outer1__OUTER1_A__TO__OUTER1_A_1_unless.outer1_outer1__state_act outer1_outer1__OUTER1_A__TO__OUTER1_A_1_unless.outer1_outer1__state_in)
161
       (= outer1_outer1__OUTER1_A__TO__OUTER1_A_1_unless.outer1_outer1__restart_act outer1_outer1__OUTER1_A__TO__OUTER1_A_1_unless.outer1_outer1__restart_in)
162
       )
163
  (outer1_outer1__OUTER1_A__TO__OUTER1_A_1_unless outer1_outer1__OUTER1_A__TO__OUTER1_A_1_unless.outer1_outer1__restart_in outer1_outer1__OUTER1_A__TO__OUTER1_A_1_unless.outer1_outer1__state_in outer1_outer1__OUTER1_A__TO__OUTER1_A_1_unless.outer1_outer1__restart_act outer1_outer1__OUTER1_A__TO__OUTER1_A_1_unless.outer1_outer1__state_act)
164
))
165

    
166
; outer1_outer1__POINTOuter1_Outer1_handler_until
167
(declare-var outer1_outer1__POINTOuter1_Outer1_handler_until.idOuter1_Outer1_1 Int)
168
(declare-var outer1_outer1__POINTOuter1_Outer1_handler_until.z_1 Int)
169
(declare-var outer1_outer1__POINTOuter1_Outer1_handler_until.x_1 Int)
170
(declare-var outer1_outer1__POINTOuter1_Outer1_handler_until.w_1 Int)
171
(declare-var outer1_outer1__POINTOuter1_Outer1_handler_until.y_1 Int)
172
(declare-var outer1_outer1__POINTOuter1_Outer1_handler_until.outer1_outer1__restart_in Bool)
173
(declare-var outer1_outer1__POINTOuter1_Outer1_handler_until.outer1_outer1__state_in outer1_outer1__type)
174
(declare-var outer1_outer1__POINTOuter1_Outer1_handler_until.idOuter1_Outer1_out Int)
175
(declare-var outer1_outer1__POINTOuter1_Outer1_handler_until.w_out Int)
176
(declare-var outer1_outer1__POINTOuter1_Outer1_handler_until.x_out Int)
177
(declare-var outer1_outer1__POINTOuter1_Outer1_handler_until.y_out Int)
178
(declare-var outer1_outer1__POINTOuter1_Outer1_handler_until.z_out Int)
179
(declare-rel outer1_outer1__POINTOuter1_Outer1_handler_until (Int Int Int Int Int Bool outer1_outer1__type Int Int Int Int Int))
180
(rule (=> 
181
  (and (= outer1_outer1__POINTOuter1_Outer1_handler_until.z_out outer1_outer1__POINTOuter1_Outer1_handler_until.z_1)
182
       (= outer1_outer1__POINTOuter1_Outer1_handler_until.y_out outer1_outer1__POINTOuter1_Outer1_handler_until.y_1)
183
       (= outer1_outer1__POINTOuter1_Outer1_handler_until.x_out outer1_outer1__POINTOuter1_Outer1_handler_until.x_1)
184
       (= outer1_outer1__POINTOuter1_Outer1_handler_until.w_out outer1_outer1__POINTOuter1_Outer1_handler_until.w_1)
185
       (= outer1_outer1__POINTOuter1_Outer1_handler_until.outer1_outer1__state_in POINTOuter1_Outer1)
186
       (= outer1_outer1__POINTOuter1_Outer1_handler_until.outer1_outer1__restart_in false)
187
       (= outer1_outer1__POINTOuter1_Outer1_handler_until.idOuter1_Outer1_out outer1_outer1__POINTOuter1_Outer1_handler_until.idOuter1_Outer1_1)
188
       )
189
  (outer1_outer1__POINTOuter1_Outer1_handler_until outer1_outer1__POINTOuter1_Outer1_handler_until.idOuter1_Outer1_1 outer1_outer1__POINTOuter1_Outer1_handler_until.z_1 outer1_outer1__POINTOuter1_Outer1_handler_until.x_1 outer1_outer1__POINTOuter1_Outer1_handler_until.w_1 outer1_outer1__POINTOuter1_Outer1_handler_until.y_1 outer1_outer1__POINTOuter1_Outer1_handler_until.outer1_outer1__restart_in outer1_outer1__POINTOuter1_Outer1_handler_until.outer1_outer1__state_in outer1_outer1__POINTOuter1_Outer1_handler_until.idOuter1_Outer1_out outer1_outer1__POINTOuter1_Outer1_handler_until.w_out outer1_outer1__POINTOuter1_Outer1_handler_until.x_out outer1_outer1__POINTOuter1_Outer1_handler_until.y_out outer1_outer1__POINTOuter1_Outer1_handler_until.z_out)
190
))
191

    
192
; outer1_outer1__POINTOuter1_Outer1_unless
193
(declare-var outer1_outer1__POINTOuter1_Outer1_unless.outer1_outer1__restart_in Bool)
194
(declare-var outer1_outer1__POINTOuter1_Outer1_unless.outer1_outer1__state_in outer1_outer1__type)
195
(declare-var outer1_outer1__POINTOuter1_Outer1_unless.idOuter1_Outer1_1 Int)
196
(declare-var outer1_outer1__POINTOuter1_Outer1_unless.E Bool)
197
(declare-var outer1_outer1__POINTOuter1_Outer1_unless.outer1_outer1__restart_act Bool)
198
(declare-var outer1_outer1__POINTOuter1_Outer1_unless.outer1_outer1__state_act outer1_outer1__type)
199
(declare-var outer1_outer1__POINTOuter1_Outer1_unless.__outer1_outer1__POINTOuter1_Outer1_unless_1 Bool)
200
(declare-var outer1_outer1__POINTOuter1_Outer1_unless.__outer1_outer1__POINTOuter1_Outer1_unless_2 Bool)
201
(declare-var outer1_outer1__POINTOuter1_Outer1_unless.__outer1_outer1__POINTOuter1_Outer1_unless_3 Bool)
202
(declare-rel outer1_outer1__POINTOuter1_Outer1_unless (Bool outer1_outer1__type Int Bool Bool outer1_outer1__type))
203
(rule (=> 
204
  (and (= outer1_outer1__POINTOuter1_Outer1_unless.__outer1_outer1__POINTOuter1_Outer1_unless_3 (= outer1_outer1__POINTOuter1_Outer1_unless.idOuter1_Outer1_1 1360))
205
       (= outer1_outer1__POINTOuter1_Outer1_unless.__outer1_outer1__POINTOuter1_Outer1_unless_2 (and (= outer1_outer1__POINTOuter1_Outer1_unless.idOuter1_Outer1_1 1360) outer1_outer1__POINTOuter1_Outer1_unless.E))
206
       (= outer1_outer1__POINTOuter1_Outer1_unless.__outer1_outer1__POINTOuter1_Outer1_unless_1 (= outer1_outer1__POINTOuter1_Outer1_unless.idOuter1_Outer1_1 0))
207
       (and (or (not (= outer1_outer1__POINTOuter1_Outer1_unless.__outer1_outer1__POINTOuter1_Outer1_unless_1 false))
208
               (and (or (not (= outer1_outer1__POINTOuter1_Outer1_unless.__outer1_outer1__POINTOuter1_Outer1_unless_2 false))
209
                       (and (or (not (= outer1_outer1__POINTOuter1_Outer1_unless.__outer1_outer1__POINTOuter1_Outer1_unless_3 false))
210
                               (and (= outer1_outer1__POINTOuter1_Outer1_unless.outer1_outer1__state_act outer1_outer1__POINTOuter1_Outer1_unless.outer1_outer1__state_in)
211
                                    (= outer1_outer1__POINTOuter1_Outer1_unless.outer1_outer1__restart_act outer1_outer1__POINTOuter1_Outer1_unless.outer1_outer1__restart_in)
212
                                    ))
213
                            (or (not (= outer1_outer1__POINTOuter1_Outer1_unless.__outer1_outer1__POINTOuter1_Outer1_unless_3 true))
214
                               (and (= outer1_outer1__POINTOuter1_Outer1_unless.outer1_outer1__state_act OUTER1_A_IDL)
215
                                    (= outer1_outer1__POINTOuter1_Outer1_unless.outer1_outer1__restart_act true)
216
                                    ))
217
                       ))
218
                    (or (not (= outer1_outer1__POINTOuter1_Outer1_unless.__outer1_outer1__POINTOuter1_Outer1_unless_2 true))
219
                       (and (= outer1_outer1__POINTOuter1_Outer1_unless.outer1_outer1__state_act OUTER1_A__TO__OUTER1_A_1)
220
                            (= outer1_outer1__POINTOuter1_Outer1_unless.outer1_outer1__restart_act true)
221
                            ))
222
               ))
223
            (or (not (= outer1_outer1__POINTOuter1_Outer1_unless.__outer1_outer1__POINTOuter1_Outer1_unless_1 true))
224
               (and (= outer1_outer1__POINTOuter1_Outer1_unless.outer1_outer1__state_act POINT__TO__OUTER1_A_1)
225
                    (= outer1_outer1__POINTOuter1_Outer1_unless.outer1_outer1__restart_act true)
226
                    ))
227
       )
228
       )
229
  (outer1_outer1__POINTOuter1_Outer1_unless outer1_outer1__POINTOuter1_Outer1_unless.outer1_outer1__restart_in outer1_outer1__POINTOuter1_Outer1_unless.outer1_outer1__state_in outer1_outer1__POINTOuter1_Outer1_unless.idOuter1_Outer1_1 outer1_outer1__POINTOuter1_Outer1_unless.E outer1_outer1__POINTOuter1_Outer1_unless.outer1_outer1__restart_act outer1_outer1__POINTOuter1_Outer1_unless.outer1_outer1__state_act)
230
))
231

    
232
; outer1_outer1__POINT__TO__OUTER1_A_1_handler_until
233
(declare-var outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.idOuter1_Outer1_1 Int)
234
(declare-var outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.z_1 Int)
235
(declare-var outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.x_1 Int)
236
(declare-var outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.w_1 Int)
237
(declare-var outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.y_1 Int)
238
(declare-var outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.outer1_outer1__restart_in Bool)
239
(declare-var outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.outer1_outer1__state_in outer1_outer1__type)
240
(declare-var outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.idOuter1_Outer1_out Int)
241
(declare-var outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.w_out Int)
242
(declare-var outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.x_out Int)
243
(declare-var outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.y_out Int)
244
(declare-var outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.z_out Int)
245
(declare-var outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.idOuter1_Outer1_2 Int)
246
(declare-var outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.z_2 Int)
247
(declare-rel outer1_outer1__POINT__TO__OUTER1_A_1_handler_until (Int Int Int Int Int Bool outer1_outer1__type Int Int Int Int Int))
248
(rule (=> 
249
  (and (Outer1_A_en outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.idOuter1_Outer1_1
250
                    outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.z_1
251
                    false
252
                    outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.idOuter1_Outer1_2
253
                    outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.z_2)
254
       (= outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.z_out outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.z_2)
255
       (= outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.y_out outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.y_1)
256
       (= outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.x_out outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.x_1)
257
       (= outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.w_out outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.w_1)
258
       (= outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.outer1_outer1__state_in POINTOuter1_Outer1)
259
       (= outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.outer1_outer1__restart_in true)
260
       (= outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.idOuter1_Outer1_out outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.idOuter1_Outer1_2)
261
       )
262
  (outer1_outer1__POINT__TO__OUTER1_A_1_handler_until outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.idOuter1_Outer1_1 outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.z_1 outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.x_1 outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.w_1 outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.y_1 outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.outer1_outer1__restart_in outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.outer1_outer1__state_in outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.idOuter1_Outer1_out outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.w_out outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.x_out outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.y_out outer1_outer1__POINT__TO__OUTER1_A_1_handler_until.z_out)
263
))
264

    
265
; outer1_outer1__POINT__TO__OUTER1_A_1_unless
266
(declare-var outer1_outer1__POINT__TO__OUTER1_A_1_unless.outer1_outer1__restart_in Bool)
267
(declare-var outer1_outer1__POINT__TO__OUTER1_A_1_unless.outer1_outer1__state_in outer1_outer1__type)
268
(declare-var outer1_outer1__POINT__TO__OUTER1_A_1_unless.outer1_outer1__restart_act Bool)
269
(declare-var outer1_outer1__POINT__TO__OUTER1_A_1_unless.outer1_outer1__state_act outer1_outer1__type)
270
(declare-rel outer1_outer1__POINT__TO__OUTER1_A_1_unless (Bool outer1_outer1__type Bool outer1_outer1__type))
271
(rule (=> 
272
  (and (= outer1_outer1__POINT__TO__OUTER1_A_1_unless.outer1_outer1__state_act outer1_outer1__POINT__TO__OUTER1_A_1_unless.outer1_outer1__state_in)
273
       (= outer1_outer1__POINT__TO__OUTER1_A_1_unless.outer1_outer1__restart_act outer1_outer1__POINT__TO__OUTER1_A_1_unless.outer1_outer1__restart_in)
274
       )
275
  (outer1_outer1__POINT__TO__OUTER1_A_1_unless outer1_outer1__POINT__TO__OUTER1_A_1_unless.outer1_outer1__restart_in outer1_outer1__POINT__TO__OUTER1_A_1_unless.outer1_outer1__state_in outer1_outer1__POINT__TO__OUTER1_A_1_unless.outer1_outer1__restart_act outer1_outer1__POINT__TO__OUTER1_A_1_unless.outer1_outer1__state_act)
276
))
277

    
278
; Outer1_Outer1_node
279
(declare-var Outer1_Outer1_node.idOuter1_Outer1_1 Int)
280
(declare-var Outer1_Outer1_node.z_1 Int)
281
(declare-var Outer1_Outer1_node.E Bool)
282
(declare-var Outer1_Outer1_node.x_1 Int)
283
(declare-var Outer1_Outer1_node.w_1 Int)
284
(declare-var Outer1_Outer1_node.y_1 Int)
285
(declare-var Outer1_Outer1_node.idOuter1_Outer1 Int)
286
(declare-var Outer1_Outer1_node.z Int)
287
(declare-var Outer1_Outer1_node.x Int)
288
(declare-var Outer1_Outer1_node.w Int)
289
(declare-var Outer1_Outer1_node.y Int)
290
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_38_c Bool)
291
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_39_c outer1_outer1__type)
292
(declare-var Outer1_Outer1_node.ni_4._arrow._first_c Bool)
293
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_38_m Bool)
294
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_39_m outer1_outer1__type)
295
(declare-var Outer1_Outer1_node.ni_4._arrow._first_m Bool)
296
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_38_x Bool)
297
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_39_x outer1_outer1__type)
298
(declare-var Outer1_Outer1_node.ni_4._arrow._first_x Bool)
299
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_1 Bool)
300
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_10 outer1_outer1__type)
301
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_11 Int)
302
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_12 Int)
303
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_13 Int)
304
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_14 Int)
305
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_15 Int)
306
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_16 Bool)
307
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_17 outer1_outer1__type)
308
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_18 Int)
309
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_19 Int)
310
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_2 outer1_outer1__type)
311
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_20 Int)
312
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_21 Int)
313
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_22 Int)
314
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_23 Bool)
315
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_24 outer1_outer1__type)
316
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_25 Int)
317
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_26 Int)
318
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_27 Int)
319
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_28 Int)
320
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_29 Int)
321
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_3 Bool)
322
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_30 Bool)
323
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_31 outer1_outer1__type)
324
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_32 Int)
325
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_33 Int)
326
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_34 Int)
327
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_35 Int)
328
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_36 Int)
329
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_37 Bool)
330
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_4 outer1_outer1__type)
331
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_5 Bool)
332
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_6 outer1_outer1__type)
333
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_7 Bool)
334
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_8 outer1_outer1__type)
335
(declare-var Outer1_Outer1_node.__Outer1_Outer1_node_9 Bool)
336
(declare-var Outer1_Outer1_node.outer1_outer1__next_restart_in Bool)
337
(declare-var Outer1_Outer1_node.outer1_outer1__next_state_in outer1_outer1__type)
338
(declare-var Outer1_Outer1_node.outer1_outer1__restart_act Bool)
339
(declare-var Outer1_Outer1_node.outer1_outer1__restart_in Bool)
340
(declare-var Outer1_Outer1_node.outer1_outer1__state_act outer1_outer1__type)
341
(declare-var Outer1_Outer1_node.outer1_outer1__state_in outer1_outer1__type)
342
(declare-rel Outer1_Outer1_node_reset (Bool outer1_outer1__type Bool Bool outer1_outer1__type Bool))
343
(declare-rel Outer1_Outer1_node_step (Int Int Bool Int Int Int Int Int Int Int Int Bool outer1_outer1__type Bool Bool outer1_outer1__type Bool))
344

    
345
(rule (=> 
346
  (and 
347
       (= Outer1_Outer1_node.__Outer1_Outer1_node_38_m Outer1_Outer1_node.__Outer1_Outer1_node_38_c)
348
       (= Outer1_Outer1_node.__Outer1_Outer1_node_39_m Outer1_Outer1_node.__Outer1_Outer1_node_39_c)
349
       (= Outer1_Outer1_node.ni_4._arrow._first_m true)
350
  )
351
  (Outer1_Outer1_node_reset Outer1_Outer1_node.__Outer1_Outer1_node_38_c
352
                            Outer1_Outer1_node.__Outer1_Outer1_node_39_c
353
                            Outer1_Outer1_node.ni_4._arrow._first_c
354
                            Outer1_Outer1_node.__Outer1_Outer1_node_38_m
355
                            Outer1_Outer1_node.__Outer1_Outer1_node_39_m
356
                            Outer1_Outer1_node.ni_4._arrow._first_m)
357
))
358

    
359
(rule (=> 
360
  (and (= Outer1_Outer1_node.ni_4._arrow._first_m Outer1_Outer1_node.ni_4._arrow._first_c)
361
       (and (= Outer1_Outer1_node.__Outer1_Outer1_node_37 (ite Outer1_Outer1_node.ni_4._arrow._first_m true false))
362
            (= Outer1_Outer1_node.ni_4._arrow._first_x false))
363
       (and (or (not (= Outer1_Outer1_node.__Outer1_Outer1_node_37 false))
364
               (and (= Outer1_Outer1_node.outer1_outer1__state_in Outer1_Outer1_node.__Outer1_Outer1_node_39_c)
365
                    (= Outer1_Outer1_node.outer1_outer1__restart_in Outer1_Outer1_node.__Outer1_Outer1_node_38_c)
366
                    ))
367
            (or (not (= Outer1_Outer1_node.__Outer1_Outer1_node_37 true))
368
               (and (= Outer1_Outer1_node.outer1_outer1__state_in POINTOuter1_Outer1)
369
                    (= Outer1_Outer1_node.outer1_outer1__restart_in false)
370
                    ))
371
       )
372
       (and (or (not (= Outer1_Outer1_node.outer1_outer1__state_in OUTER1_A_IDL))
373
               (and (outer1_outer1__OUTER1_A_IDL_unless Outer1_Outer1_node.outer1_outer1__restart_in
374
                                                        Outer1_Outer1_node.outer1_outer1__state_in
375
                                                        Outer1_Outer1_node.__Outer1_Outer1_node_1
376
                                                        Outer1_Outer1_node.__Outer1_Outer1_node_2)
377
                    (= Outer1_Outer1_node.outer1_outer1__state_act Outer1_Outer1_node.__Outer1_Outer1_node_2)
378
                    (= Outer1_Outer1_node.outer1_outer1__restart_act Outer1_Outer1_node.__Outer1_Outer1_node_1)
379
                    ))
380
            (or (not (= Outer1_Outer1_node.outer1_outer1__state_in OUTER1_A__TO__OUTER1_A_1))
381
               (and (outer1_outer1__OUTER1_A__TO__OUTER1_A_1_unless Outer1_Outer1_node.outer1_outer1__restart_in
382
                                                                    Outer1_Outer1_node.outer1_outer1__state_in
383
                                                                    Outer1_Outer1_node.__Outer1_Outer1_node_3
384
                                                                    Outer1_Outer1_node.__Outer1_Outer1_node_4)
385
                    (= Outer1_Outer1_node.outer1_outer1__state_act Outer1_Outer1_node.__Outer1_Outer1_node_4)
386
                    (= Outer1_Outer1_node.outer1_outer1__restart_act Outer1_Outer1_node.__Outer1_Outer1_node_3)
387
                    ))
388
            (or (not (= Outer1_Outer1_node.outer1_outer1__state_in POINTOuter1_Outer1))
389
               (and (outer1_outer1__POINTOuter1_Outer1_unless Outer1_Outer1_node.outer1_outer1__restart_in
390
                                                              Outer1_Outer1_node.outer1_outer1__state_in
391
                                                              Outer1_Outer1_node.idOuter1_Outer1_1
392
                                                              Outer1_Outer1_node.E
393
                                                              Outer1_Outer1_node.__Outer1_Outer1_node_7
394
                                                              Outer1_Outer1_node.__Outer1_Outer1_node_8)
395
                    (= Outer1_Outer1_node.outer1_outer1__state_act Outer1_Outer1_node.__Outer1_Outer1_node_8)
396
                    (= Outer1_Outer1_node.outer1_outer1__restart_act Outer1_Outer1_node.__Outer1_Outer1_node_7)
397
                    ))
398
            (or (not (= Outer1_Outer1_node.outer1_outer1__state_in POINT__TO__OUTER1_A_1))
399
               (and (outer1_outer1__POINT__TO__OUTER1_A_1_unless Outer1_Outer1_node.outer1_outer1__restart_in
400
                                                                 Outer1_Outer1_node.outer1_outer1__state_in
401
                                                                 Outer1_Outer1_node.__Outer1_Outer1_node_5
402
                                                                 Outer1_Outer1_node.__Outer1_Outer1_node_6)
403
                    (= Outer1_Outer1_node.outer1_outer1__state_act Outer1_Outer1_node.__Outer1_Outer1_node_6)
404
                    (= Outer1_Outer1_node.outer1_outer1__restart_act Outer1_Outer1_node.__Outer1_Outer1_node_5)
405
                    ))
406
       )
407
       (and (or (not (= Outer1_Outer1_node.outer1_outer1__state_act OUTER1_A_IDL))
408
               (and (outer1_outer1__OUTER1_A_IDL_handler_until Outer1_Outer1_node.idOuter1_Outer1_1
409
                                                               Outer1_Outer1_node.z_1
410
                                                               Outer1_Outer1_node.x_1
411
                                                               Outer1_Outer1_node.w_1
412
                                                               Outer1_Outer1_node.y_1
413
                                                               Outer1_Outer1_node.__Outer1_Outer1_node_9
414
                                                               Outer1_Outer1_node.__Outer1_Outer1_node_10
415
                                                               Outer1_Outer1_node.__Outer1_Outer1_node_11
416
                                                               Outer1_Outer1_node.__Outer1_Outer1_node_12
417
                                                               Outer1_Outer1_node.__Outer1_Outer1_node_13
418
                                                               Outer1_Outer1_node.__Outer1_Outer1_node_14
419
                                                               Outer1_Outer1_node.__Outer1_Outer1_node_15)
420
                    (= Outer1_Outer1_node.z Outer1_Outer1_node.__Outer1_Outer1_node_15)
421
                    (= Outer1_Outer1_node.y Outer1_Outer1_node.__Outer1_Outer1_node_14)
422
                    (= Outer1_Outer1_node.x Outer1_Outer1_node.__Outer1_Outer1_node_13)
423
                    (= Outer1_Outer1_node.w Outer1_Outer1_node.__Outer1_Outer1_node_12)
424
                    (= Outer1_Outer1_node.outer1_outer1__next_state_in Outer1_Outer1_node.__Outer1_Outer1_node_10)
425
                    (= Outer1_Outer1_node.outer1_outer1__next_restart_in Outer1_Outer1_node.__Outer1_Outer1_node_9)
426
                    (= Outer1_Outer1_node.idOuter1_Outer1 Outer1_Outer1_node.__Outer1_Outer1_node_11)
427
                    ))
428
            (or (not (= Outer1_Outer1_node.outer1_outer1__state_act OUTER1_A__TO__OUTER1_A_1))
429
               (and (outer1_outer1__OUTER1_A__TO__OUTER1_A_1_handler_until 
430
                    Outer1_Outer1_node.idOuter1_Outer1_1
431
                    Outer1_Outer1_node.z_1
432
                    Outer1_Outer1_node.x_1
433
                    Outer1_Outer1_node.w_1
434
                    Outer1_Outer1_node.y_1
435
                    Outer1_Outer1_node.__Outer1_Outer1_node_16
436
                    Outer1_Outer1_node.__Outer1_Outer1_node_17
437
                    Outer1_Outer1_node.__Outer1_Outer1_node_18
438
                    Outer1_Outer1_node.__Outer1_Outer1_node_19
439
                    Outer1_Outer1_node.__Outer1_Outer1_node_20
440
                    Outer1_Outer1_node.__Outer1_Outer1_node_21
441
                    Outer1_Outer1_node.__Outer1_Outer1_node_22)
442
                    (= Outer1_Outer1_node.z Outer1_Outer1_node.__Outer1_Outer1_node_22)
443
                    (= Outer1_Outer1_node.y Outer1_Outer1_node.__Outer1_Outer1_node_21)
444
                    (= Outer1_Outer1_node.x Outer1_Outer1_node.__Outer1_Outer1_node_20)
445
                    (= Outer1_Outer1_node.w Outer1_Outer1_node.__Outer1_Outer1_node_19)
446
                    (= Outer1_Outer1_node.outer1_outer1__next_state_in Outer1_Outer1_node.__Outer1_Outer1_node_17)
447
                    (= Outer1_Outer1_node.outer1_outer1__next_restart_in Outer1_Outer1_node.__Outer1_Outer1_node_16)
448
                    (= Outer1_Outer1_node.idOuter1_Outer1 Outer1_Outer1_node.__Outer1_Outer1_node_18)
449
                    ))
450
            (or (not (= Outer1_Outer1_node.outer1_outer1__state_act POINTOuter1_Outer1))
451
               (and (outer1_outer1__POINTOuter1_Outer1_handler_until 
452
                    Outer1_Outer1_node.idOuter1_Outer1_1
453
                    Outer1_Outer1_node.z_1
454
                    Outer1_Outer1_node.x_1
455
                    Outer1_Outer1_node.w_1
456
                    Outer1_Outer1_node.y_1
457
                    Outer1_Outer1_node.__Outer1_Outer1_node_30
458
                    Outer1_Outer1_node.__Outer1_Outer1_node_31
459
                    Outer1_Outer1_node.__Outer1_Outer1_node_32
460
                    Outer1_Outer1_node.__Outer1_Outer1_node_33
461
                    Outer1_Outer1_node.__Outer1_Outer1_node_34
462
                    Outer1_Outer1_node.__Outer1_Outer1_node_35
463
                    Outer1_Outer1_node.__Outer1_Outer1_node_36)
464
                    (= Outer1_Outer1_node.z Outer1_Outer1_node.__Outer1_Outer1_node_36)
465
                    (= Outer1_Outer1_node.y Outer1_Outer1_node.__Outer1_Outer1_node_35)
466
                    (= Outer1_Outer1_node.x Outer1_Outer1_node.__Outer1_Outer1_node_34)
467
                    (= Outer1_Outer1_node.w Outer1_Outer1_node.__Outer1_Outer1_node_33)
468
                    (= Outer1_Outer1_node.outer1_outer1__next_state_in Outer1_Outer1_node.__Outer1_Outer1_node_31)
469
                    (= Outer1_Outer1_node.outer1_outer1__next_restart_in Outer1_Outer1_node.__Outer1_Outer1_node_30)
470
                    (= Outer1_Outer1_node.idOuter1_Outer1 Outer1_Outer1_node.__Outer1_Outer1_node_32)
471
                    ))
472
            (or (not (= Outer1_Outer1_node.outer1_outer1__state_act POINT__TO__OUTER1_A_1))
473
               (and (outer1_outer1__POINT__TO__OUTER1_A_1_handler_until 
474
                    Outer1_Outer1_node.idOuter1_Outer1_1
475
                    Outer1_Outer1_node.z_1
476
                    Outer1_Outer1_node.x_1
477
                    Outer1_Outer1_node.w_1
478
                    Outer1_Outer1_node.y_1
479
                    Outer1_Outer1_node.__Outer1_Outer1_node_23
480
                    Outer1_Outer1_node.__Outer1_Outer1_node_24
481
                    Outer1_Outer1_node.__Outer1_Outer1_node_25
482
                    Outer1_Outer1_node.__Outer1_Outer1_node_26
483
                    Outer1_Outer1_node.__Outer1_Outer1_node_27
484
                    Outer1_Outer1_node.__Outer1_Outer1_node_28
485
                    Outer1_Outer1_node.__Outer1_Outer1_node_29)
486
                    (= Outer1_Outer1_node.z Outer1_Outer1_node.__Outer1_Outer1_node_29)
487
                    (= Outer1_Outer1_node.y Outer1_Outer1_node.__Outer1_Outer1_node_28)
488
                    (= Outer1_Outer1_node.x Outer1_Outer1_node.__Outer1_Outer1_node_27)
489
                    (= Outer1_Outer1_node.w Outer1_Outer1_node.__Outer1_Outer1_node_26)
490
                    (= Outer1_Outer1_node.outer1_outer1__next_state_in Outer1_Outer1_node.__Outer1_Outer1_node_24)
491
                    (= Outer1_Outer1_node.outer1_outer1__next_restart_in Outer1_Outer1_node.__Outer1_Outer1_node_23)
492
                    (= Outer1_Outer1_node.idOuter1_Outer1 Outer1_Outer1_node.__Outer1_Outer1_node_25)
493
                    ))
494
       )
495
       (= Outer1_Outer1_node.__Outer1_Outer1_node_39_x Outer1_Outer1_node.outer1_outer1__next_state_in)
496
       (= Outer1_Outer1_node.__Outer1_Outer1_node_38_x Outer1_Outer1_node.outer1_outer1__next_restart_in)
497
       )
498
  (Outer1_Outer1_node_step Outer1_Outer1_node.idOuter1_Outer1_1
499
                           Outer1_Outer1_node.z_1
500
                           Outer1_Outer1_node.E
501
                           Outer1_Outer1_node.x_1
502
                           Outer1_Outer1_node.w_1
503
                           Outer1_Outer1_node.y_1
504
                           Outer1_Outer1_node.idOuter1_Outer1
505
                           Outer1_Outer1_node.z
506
                           Outer1_Outer1_node.x
507
                           Outer1_Outer1_node.w
508
                           Outer1_Outer1_node.y
509
                           Outer1_Outer1_node.__Outer1_Outer1_node_38_c
510
                           Outer1_Outer1_node.__Outer1_Outer1_node_39_c
511
                           Outer1_Outer1_node.ni_4._arrow._first_c
512
                           Outer1_Outer1_node.__Outer1_Outer1_node_38_x
513
                           Outer1_Outer1_node.__Outer1_Outer1_node_39_x
514
                           Outer1_Outer1_node.ni_4._arrow._first_x)
515
))
516

    
517
; Outer1_Outer1
518
(declare-var Outer1_Outer1.E Bool)
519
(declare-var Outer1_Outer1.w Int)
520
(declare-var Outer1_Outer1.x Int)
521
(declare-var Outer1_Outer1.z Int)
522
(declare-var Outer1_Outer1.y Int)
523
(declare-var Outer1_Outer1.__Outer1_Outer1_10_c Int)
524
(declare-var Outer1_Outer1.__Outer1_Outer1_11_c Int)
525
(declare-var Outer1_Outer1.__Outer1_Outer1_7_c Int)
526
(declare-var Outer1_Outer1.__Outer1_Outer1_8_c Int)
527
(declare-var Outer1_Outer1.__Outer1_Outer1_9_c Int)
528
(declare-var Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_38_c Bool)
529
(declare-var Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_39_c outer1_outer1__type)
530
(declare-var Outer1_Outer1.ni_2.Outer1_Outer1_node.ni_4._arrow._first_c Bool)
531
(declare-var Outer1_Outer1.ni_3._arrow._first_c Bool)
532
(declare-var Outer1_Outer1.__Outer1_Outer1_10_m Int)
533
(declare-var Outer1_Outer1.__Outer1_Outer1_11_m Int)
534
(declare-var Outer1_Outer1.__Outer1_Outer1_7_m Int)
535
(declare-var Outer1_Outer1.__Outer1_Outer1_8_m Int)
536
(declare-var Outer1_Outer1.__Outer1_Outer1_9_m Int)
537
(declare-var Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_38_m Bool)
538
(declare-var Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_39_m outer1_outer1__type)
539
(declare-var Outer1_Outer1.ni_2.Outer1_Outer1_node.ni_4._arrow._first_m Bool)
540
(declare-var Outer1_Outer1.ni_3._arrow._first_m Bool)
541
(declare-var Outer1_Outer1.__Outer1_Outer1_10_x Int)
542
(declare-var Outer1_Outer1.__Outer1_Outer1_11_x Int)
543
(declare-var Outer1_Outer1.__Outer1_Outer1_7_x Int)
544
(declare-var Outer1_Outer1.__Outer1_Outer1_8_x Int)
545
(declare-var Outer1_Outer1.__Outer1_Outer1_9_x Int)
546
(declare-var Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_38_x Bool)
547
(declare-var Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_39_x outer1_outer1__type)
548
(declare-var Outer1_Outer1.ni_2.Outer1_Outer1_node.ni_4._arrow._first_x Bool)
549
(declare-var Outer1_Outer1.ni_3._arrow._first_x Bool)
550
(declare-var Outer1_Outer1.__Outer1_Outer1_1 Int)
551
(declare-var Outer1_Outer1.__Outer1_Outer1_2 Int)
552
(declare-var Outer1_Outer1.__Outer1_Outer1_3 Int)
553
(declare-var Outer1_Outer1.__Outer1_Outer1_4 Int)
554
(declare-var Outer1_Outer1.__Outer1_Outer1_5 Int)
555
(declare-var Outer1_Outer1.__Outer1_Outer1_6 Bool)
556
(declare-var Outer1_Outer1.idOuter1_Outer1 Int)
557
(declare-var Outer1_Outer1.idOuter1_Outer1_1 Int)
558
(declare-var Outer1_Outer1.w_1 Int)
559
(declare-var Outer1_Outer1.x_1 Int)
560
(declare-var Outer1_Outer1.y_1 Int)
561
(declare-var Outer1_Outer1.z_1 Int)
562
(declare-rel Outer1_Outer1_reset (Int Int Int Int Int Bool outer1_outer1__type Bool Bool Int Int Int Int Int Bool outer1_outer1__type Bool Bool))
563
(declare-rel Outer1_Outer1_step (Bool Int Int Int Int Int Int Int Int Int Bool outer1_outer1__type Bool Bool Int Int Int Int Int Bool outer1_outer1__type Bool Bool))
564

    
565
(rule (=> 
566
  (and 
567
       (= Outer1_Outer1.__Outer1_Outer1_10_m Outer1_Outer1.__Outer1_Outer1_10_c)
568
       (= Outer1_Outer1.__Outer1_Outer1_11_m Outer1_Outer1.__Outer1_Outer1_11_c)
569
       (= Outer1_Outer1.__Outer1_Outer1_7_m Outer1_Outer1.__Outer1_Outer1_7_c)
570
       (= Outer1_Outer1.__Outer1_Outer1_8_m Outer1_Outer1.__Outer1_Outer1_8_c)
571
       (= Outer1_Outer1.__Outer1_Outer1_9_m Outer1_Outer1.__Outer1_Outer1_9_c)
572
       (= Outer1_Outer1.ni_3._arrow._first_m true)
573
       (Outer1_Outer1_node_reset Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_38_c
574
                                 Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_39_c
575
                                 Outer1_Outer1.ni_2.Outer1_Outer1_node.ni_4._arrow._first_c
576
                                 Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_38_m
577
                                 Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_39_m
578
                                 Outer1_Outer1.ni_2.Outer1_Outer1_node.ni_4._arrow._first_m)
579
  )
580
  (Outer1_Outer1_reset Outer1_Outer1.__Outer1_Outer1_10_c
581
                       Outer1_Outer1.__Outer1_Outer1_11_c
582
                       Outer1_Outer1.__Outer1_Outer1_7_c
583
                       Outer1_Outer1.__Outer1_Outer1_8_c
584
                       Outer1_Outer1.__Outer1_Outer1_9_c
585
                       Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_38_c
586
                       Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_39_c
587
                       Outer1_Outer1.ni_2.Outer1_Outer1_node.ni_4._arrow._first_c
588
                       Outer1_Outer1.ni_3._arrow._first_c
589
                       Outer1_Outer1.__Outer1_Outer1_10_m
590
                       Outer1_Outer1.__Outer1_Outer1_11_m
591
                       Outer1_Outer1.__Outer1_Outer1_7_m
592
                       Outer1_Outer1.__Outer1_Outer1_8_m
593
                       Outer1_Outer1.__Outer1_Outer1_9_m
594
                       Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_38_m
595
                       Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_39_m
596
                       Outer1_Outer1.ni_2.Outer1_Outer1_node.ni_4._arrow._first_m
597
                       Outer1_Outer1.ni_3._arrow._first_m)
598
))
599

    
600
(rule (=> 
601
  (and (= Outer1_Outer1.ni_3._arrow._first_m Outer1_Outer1.ni_3._arrow._first_c)
602
       (and (= Outer1_Outer1.__Outer1_Outer1_6 (ite Outer1_Outer1.ni_3._arrow._first_m true false))
603
            (= Outer1_Outer1.ni_3._arrow._first_x false))
604
       (and (or (not (= Outer1_Outer1.__Outer1_Outer1_6 false))
605
               (and (= Outer1_Outer1.z_1 Outer1_Outer1.__Outer1_Outer1_9_c)
606
                    (= Outer1_Outer1.y_1 Outer1_Outer1.__Outer1_Outer1_8_c)
607
                    (= Outer1_Outer1.x_1 Outer1_Outer1.__Outer1_Outer1_10_c)
608
                    (= Outer1_Outer1.w_1 Outer1_Outer1.__Outer1_Outer1_11_c)
609
                    (= Outer1_Outer1.idOuter1_Outer1_1 Outer1_Outer1.__Outer1_Outer1_7_c)
610
                    ))
611
            (or (not (= Outer1_Outer1.__Outer1_Outer1_6 true))
612
               (and (= Outer1_Outer1.z_1 0)
613
                    (= Outer1_Outer1.y_1 0)
614
                    (= Outer1_Outer1.x_1 0)
615
                    (= Outer1_Outer1.w_1 0)
616
                    (= Outer1_Outer1.idOuter1_Outer1_1 0)
617
                    ))
618
       )
619
       (and (= Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_38_m Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_38_c)
620
            (= Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_39_m Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_39_c)
621
            (= Outer1_Outer1.ni_2.Outer1_Outer1_node.ni_4._arrow._first_m Outer1_Outer1.ni_2.Outer1_Outer1_node.ni_4._arrow._first_c)
622
            )
623
       (Outer1_Outer1_node_step Outer1_Outer1.idOuter1_Outer1_1
624
                                Outer1_Outer1.z_1
625
                                Outer1_Outer1.E
626
                                Outer1_Outer1.x_1
627
                                Outer1_Outer1.w_1
628
                                Outer1_Outer1.y_1
629
                                Outer1_Outer1.__Outer1_Outer1_1
630
                                Outer1_Outer1.__Outer1_Outer1_2
631
                                Outer1_Outer1.__Outer1_Outer1_3
632
                                Outer1_Outer1.__Outer1_Outer1_4
633
                                Outer1_Outer1.__Outer1_Outer1_5
634
                                Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_38_m
635
                                Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_39_m
636
                                Outer1_Outer1.ni_2.Outer1_Outer1_node.ni_4._arrow._first_m
637
                                Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_38_x
638
                                Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_39_x
639
                                Outer1_Outer1.ni_2.Outer1_Outer1_node.ni_4._arrow._first_x)
640
       (and (or (not (= Outer1_Outer1.E false))
641
               (and (= Outer1_Outer1.z Outer1_Outer1.z_1)
642
                    (= Outer1_Outer1.y Outer1_Outer1.y_1)
643
                    (= Outer1_Outer1.x Outer1_Outer1.x_1)
644
                    (= Outer1_Outer1.w Outer1_Outer1.w_1)
645
                    (= Outer1_Outer1.idOuter1_Outer1 Outer1_Outer1.idOuter1_Outer1_1)
646
                    ))
647
            (or (not (= Outer1_Outer1.E true))
648
               (and (= Outer1_Outer1.z Outer1_Outer1.__Outer1_Outer1_2)
649
                    (= Outer1_Outer1.y Outer1_Outer1.__Outer1_Outer1_5)
650
                    (= Outer1_Outer1.x Outer1_Outer1.__Outer1_Outer1_3)
651
                    (= Outer1_Outer1.w Outer1_Outer1.__Outer1_Outer1_4)
652
                    (= Outer1_Outer1.idOuter1_Outer1 Outer1_Outer1.__Outer1_Outer1_1)
653
                    ))
654
       )
655
       (= Outer1_Outer1.__Outer1_Outer1_9_x Outer1_Outer1.z)
656
       (= Outer1_Outer1.__Outer1_Outer1_8_x Outer1_Outer1.y)
657
       (= Outer1_Outer1.__Outer1_Outer1_7_x Outer1_Outer1.idOuter1_Outer1)
658
       (= Outer1_Outer1.__Outer1_Outer1_11_x Outer1_Outer1.w)
659
       (= Outer1_Outer1.__Outer1_Outer1_10_x Outer1_Outer1.x)
660
       )
661
  (Outer1_Outer1_step Outer1_Outer1.E
662
                      Outer1_Outer1.w
663
                      Outer1_Outer1.x
664
                      Outer1_Outer1.z
665
                      Outer1_Outer1.y
666
                      Outer1_Outer1.__Outer1_Outer1_10_c
667
                      Outer1_Outer1.__Outer1_Outer1_11_c
668
                      Outer1_Outer1.__Outer1_Outer1_7_c
669
                      Outer1_Outer1.__Outer1_Outer1_8_c
670
                      Outer1_Outer1.__Outer1_Outer1_9_c
671
                      Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_38_c
672
                      Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_39_c
673
                      Outer1_Outer1.ni_2.Outer1_Outer1_node.ni_4._arrow._first_c
674
                      Outer1_Outer1.ni_3._arrow._first_c
675
                      Outer1_Outer1.__Outer1_Outer1_10_x
676
                      Outer1_Outer1.__Outer1_Outer1_11_x
677
                      Outer1_Outer1.__Outer1_Outer1_7_x
678
                      Outer1_Outer1.__Outer1_Outer1_8_x
679
                      Outer1_Outer1.__Outer1_Outer1_9_x
680
                      Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_38_x
681
                      Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_39_x
682
                      Outer1_Outer1.ni_2.Outer1_Outer1_node.ni_4._arrow._first_x
683
                      Outer1_Outer1.ni_3._arrow._first_x)
684
))
685

    
686
; Outer1
687
(declare-var Outer1.E_1_1 Real)
688
(declare-var Outer1.w_1_1 Int)
689
(declare-var Outer1.x_2_1 Int)
690
(declare-var Outer1.z_3_1 Int)
691
(declare-var Outer1.y_4_1 Int)
692
(declare-var Outer1.__Outer1_2_c Real)
693
(declare-var Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_10_c Int)
694
(declare-var Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_11_c Int)
695
(declare-var Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_7_c Int)
696
(declare-var Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_8_c Int)
697
(declare-var Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_9_c Int)
698
(declare-var Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_38_c Bool)
699
(declare-var Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_39_c outer1_outer1__type)
700
(declare-var Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.ni_4._arrow._first_c Bool)
701
(declare-var Outer1.ni_0.Outer1_Outer1.ni_3._arrow._first_c Bool)
702
(declare-var Outer1.ni_1._arrow._first_c Bool)
703
(declare-var Outer1.__Outer1_2_m Real)
704
(declare-var Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_10_m Int)
705
(declare-var Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_11_m Int)
706
(declare-var Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_7_m Int)
707
(declare-var Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_8_m Int)
708
(declare-var Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_9_m Int)
709
(declare-var Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_38_m Bool)
710
(declare-var Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_39_m outer1_outer1__type)
711
(declare-var Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.ni_4._arrow._first_m Bool)
712
(declare-var Outer1.ni_0.Outer1_Outer1.ni_3._arrow._first_m Bool)
713
(declare-var Outer1.ni_1._arrow._first_m Bool)
714
(declare-var Outer1.__Outer1_2_x Real)
715
(declare-var Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_10_x Int)
716
(declare-var Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_11_x Int)
717
(declare-var Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_7_x Int)
718
(declare-var Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_8_x Int)
719
(declare-var Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_9_x Int)
720
(declare-var Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_38_x Bool)
721
(declare-var Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_39_x outer1_outer1__type)
722
(declare-var Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.ni_4._arrow._first_x Bool)
723
(declare-var Outer1.ni_0.Outer1_Outer1.ni_3._arrow._first_x Bool)
724
(declare-var Outer1.ni_1._arrow._first_x Bool)
725
(declare-var Outer1.Outer1E_1_1_event Bool)
726
(declare-var Outer1.Outer1_1_1 Int)
727
(declare-var Outer1.Outer1_2_1 Int)
728
(declare-var Outer1.Outer1_3_1 Int)
729
(declare-var Outer1.Outer1_4_1 Int)
730
(declare-var Outer1.__Outer1_1 Bool)
731
(declare-var Outer1.i_virtual_local Real)
732
(declare-rel Outer1_reset (Real Int Int Int Int Int Bool outer1_outer1__type Bool Bool Bool Real Int Int Int Int Int Bool outer1_outer1__type Bool Bool Bool))
733
(declare-rel Outer1_step (Real Int Int Int Int Real Int Int Int Int Int Bool outer1_outer1__type Bool Bool Bool Real Int Int Int Int Int Bool outer1_outer1__type Bool Bool Bool))
734

    
735
(rule (=> 
736
  (and 
737
       (= Outer1.__Outer1_2_m Outer1.__Outer1_2_c)
738
       (= Outer1.ni_1._arrow._first_m true)
739
       (Outer1_Outer1_reset Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_10_c
740
                            Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_11_c
741
                            Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_7_c
742
                            Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_8_c
743
                            Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_9_c
744
                            Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_38_c
745
                            Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_39_c
746
                            Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.ni_4._arrow._first_c
747
                            Outer1.ni_0.Outer1_Outer1.ni_3._arrow._first_c
748
                            Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_10_m
749
                            Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_11_m
750
                            Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_7_m
751
                            Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_8_m
752
                            Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_9_m
753
                            Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_38_m
754
                            Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_39_m
755
                            Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.ni_4._arrow._first_m
756
                            Outer1.ni_0.Outer1_Outer1.ni_3._arrow._first_m)
757
  )
758
  (Outer1_reset Outer1.__Outer1_2_c
759
                Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_10_c
760
                Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_11_c
761
                Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_7_c
762
                Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_8_c
763
                Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_9_c
764
                Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_38_c
765
                Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_39_c
766
                Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.ni_4._arrow._first_c
767
                Outer1.ni_0.Outer1_Outer1.ni_3._arrow._first_c
768
                Outer1.ni_1._arrow._first_c
769
                Outer1.__Outer1_2_m
770
                Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_10_m
771
                Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_11_m
772
                Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_7_m
773
                Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_8_m
774
                Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_9_m
775
                Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_38_m
776
                Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_39_m
777
                Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.ni_4._arrow._first_m
778
                Outer1.ni_0.Outer1_Outer1.ni_3._arrow._first_m
779
                Outer1.ni_1._arrow._first_m)
780
))
781

    
782
(rule (=> 
783
  (and (= Outer1.ni_1._arrow._first_m Outer1.ni_1._arrow._first_c)(and (= Outer1.__Outer1_1 (ite Outer1.ni_1._arrow._first_m true false))
784
                                                                    (= Outer1.ni_1._arrow._first_x false))
785
       (and (or (not (= Outer1.__Outer1_1 true))
786
               (= Outer1.Outer1E_1_1_event false))
787
            (or (not (= Outer1.__Outer1_1 false))
788
               (= Outer1.Outer1E_1_1_event (or (and (> Outer1.__Outer1_2_c 0.) (<= Outer1.E_1_1 0.)) (and (<= Outer1.__Outer1_2_c 0.) (> Outer1.E_1_1 0.)))))
789
       )
790
       (and (= Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_10_m Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_10_c)
791
            (= Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_11_m Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_11_c)
792
            (= Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_7_m Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_7_c)
793
            (= Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_8_m Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_8_c)
794
            (= Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_9_m Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_9_c)
795
            (= Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_38_m Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_38_c)
796
            (= Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_39_m Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_39_c)
797
            (= Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.ni_4._arrow._first_m Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.ni_4._arrow._first_c)
798
            (= Outer1.ni_0.Outer1_Outer1.ni_3._arrow._first_m Outer1.ni_0.Outer1_Outer1.ni_3._arrow._first_c)
799
            )
800
       (Outer1_Outer1_step Outer1.Outer1E_1_1_event
801
                           Outer1.Outer1_1_1
802
                           Outer1.Outer1_2_1
803
                           Outer1.Outer1_3_1
804
                           Outer1.Outer1_4_1
805
                           Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_10_m
806
                           Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_11_m
807
                           Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_7_m
808
                           Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_8_m
809
                           Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_9_m
810
                           Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_38_m
811
                           Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_39_m
812
                           Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.ni_4._arrow._first_m
813
                           Outer1.ni_0.Outer1_Outer1.ni_3._arrow._first_m
814
                           Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_10_x
815
                           Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_11_x
816
                           Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_7_x
817
                           Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_8_x
818
                           Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_9_x
819
                           Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_38_x
820
                           Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_39_x
821
                           Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.ni_4._arrow._first_x
822
                           Outer1.ni_0.Outer1_Outer1.ni_3._arrow._first_x)
823
       (= Outer1.z_3_1 Outer1.Outer1_3_1)
824
       (= Outer1.y_4_1 Outer1.Outer1_4_1)
825
       (= Outer1.x_2_1 Outer1.Outer1_2_1)
826
       (= Outer1.w_1_1 Outer1.Outer1_1_1)
827
       (and (or (not (= Outer1.__Outer1_1 true))
828
               (= Outer1.i_virtual_local 0.))
829
            (or (not (= Outer1.__Outer1_1 false))
830
               (= Outer1.i_virtual_local 1.))
831
       )
832
       (= Outer1.__Outer1_2_x Outer1.E_1_1)
833
       )
834
  (Outer1_step Outer1.E_1_1
835
               Outer1.w_1_1
836
               Outer1.x_2_1
837
               Outer1.z_3_1
838
               Outer1.y_4_1
839
               Outer1.__Outer1_2_c
840
               Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_10_c
841
               Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_11_c
842
               Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_7_c
843
               Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_8_c
844
               Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_9_c
845
               Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_38_c
846
               Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_39_c
847
               Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.ni_4._arrow._first_c
848
               Outer1.ni_0.Outer1_Outer1.ni_3._arrow._first_c
849
               Outer1.ni_1._arrow._first_c
850
               Outer1.__Outer1_2_x
851
               Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_10_x
852
               Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_11_x
853
               Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_7_x
854
               Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_8_x
855
               Outer1.ni_0.Outer1_Outer1.__Outer1_Outer1_9_x
856
               Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_38_x
857
               Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.__Outer1_Outer1_node_39_x
858
               Outer1.ni_0.Outer1_Outer1.ni_2.Outer1_Outer1_node.ni_4._arrow._first_x
859
               Outer1.ni_0.Outer1_Outer1.ni_3._arrow._first_x
860
               Outer1.ni_1._arrow._first_x)
861
))
862