71 open Hints_declaration
90 val transrel_rect_Type4 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1
92 val transrel_rect_Type5 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1
94 val transrel_rect_Type3 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1
96 val transrel_rect_Type2 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1
98 val transrel_rect_Type1 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1
100 val transrel_rect_Type0 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1
106 val transrel_inv_rect_Type4 :
107 transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
109 val transrel_inv_rect_Type3 :
110 transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
112 val transrel_inv_rect_Type2 :
113 transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
115 val transrel_inv_rect_Type1 :
116 transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
118 val transrel_inv_rect_Type0 :
119 transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
121 val transrel_jmdiscr : transrel -> transrel -> __
123 type program_behavior =
124 | Terminates of Events.trace * Integers.int
125 | Diverges of Events.trace
126 | Reacts of Events.traceinf
127 | Goes_wrong of Events.trace
129 val program_behavior_rect_Type4 :
130 (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
131 (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
134 val program_behavior_rect_Type5 :
135 (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
136 (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
139 val program_behavior_rect_Type3 :
140 (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
141 (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
144 val program_behavior_rect_Type2 :
145 (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
146 (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
149 val program_behavior_rect_Type1 :
150 (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
151 (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
154 val program_behavior_rect_Type0 :
155 (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
156 (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
159 val program_behavior_inv_rect_Type4 :
160 program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
161 (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
162 (Events.trace -> __ -> 'a1) -> 'a1
164 val program_behavior_inv_rect_Type3 :
165 program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
166 (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
167 (Events.trace -> __ -> 'a1) -> 'a1
169 val program_behavior_inv_rect_Type2 :
170 program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
171 (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
172 (Events.trace -> __ -> 'a1) -> 'a1
174 val program_behavior_inv_rect_Type1 :
175 program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
176 (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
177 (Events.trace -> __ -> 'a1) -> 'a1
179 val program_behavior_inv_rect_Type0 :
180 program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
181 (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
182 (Events.trace -> __ -> 'a1) -> 'a1
184 val program_behavior_discr : program_behavior -> program_behavior -> __
186 val program_behavior_jmdiscr : program_behavior -> program_behavior -> __
188 type semantics = { trans : transrel; ge : __ }
190 val semantics_rect_Type4 :
191 (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1
193 val semantics_rect_Type5 :
194 (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1
196 val semantics_rect_Type3 :
197 (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1
199 val semantics_rect_Type2 :
200 (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1
202 val semantics_rect_Type1 :
203 (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1
205 val semantics_rect_Type0 :
206 (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1
208 val trans : semantics -> transrel
210 val ge : semantics -> __
212 val semantics_inv_rect_Type4 :
213 semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
215 val semantics_inv_rect_Type3 :
216 semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
218 val semantics_inv_rect_Type2 :
219 semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
221 val semantics_inv_rect_Type1 :
222 semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
224 val semantics_inv_rect_Type0 :
225 semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
227 val semantics_jmdiscr : semantics -> semantics -> __
229 type related_semantics = { sem1 : semantics; sem2 : semantics }
231 val related_semantics_rect_Type4 :
232 (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
235 val related_semantics_rect_Type5 :
236 (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
239 val related_semantics_rect_Type3 :
240 (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
243 val related_semantics_rect_Type2 :
244 (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
247 val related_semantics_rect_Type1 :
248 (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
251 val related_semantics_rect_Type0 :
252 (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
255 val sem1 : related_semantics -> semantics
257 val sem2 : related_semantics -> semantics
259 val related_semantics_inv_rect_Type4 :
260 related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
263 val related_semantics_inv_rect_Type3 :
264 related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
267 val related_semantics_inv_rect_Type2 :
268 related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
271 val related_semantics_inv_rect_Type1 :
272 related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
275 val related_semantics_inv_rect_Type0 :
276 related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
279 val related_semantics_jmdiscr : related_semantics -> related_semantics -> __
283 (* singleton inductive, whose constructor was mk_order_sim *)
285 val order_sim_rect_Type4 :
286 (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1
288 val order_sim_rect_Type5 :
289 (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1
291 val order_sim_rect_Type3 :
292 (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1
294 val order_sim_rect_Type2 :
295 (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1
297 val order_sim_rect_Type1 :
298 (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1
300 val order_sim_rect_Type0 :
301 (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1
303 val sem : order_sim -> related_semantics
305 val order_sim_inv_rect_Type4 :
306 order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1
308 val order_sim_inv_rect_Type3 :
309 order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1
311 val order_sim_inv_rect_Type2 :
312 order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1
314 val order_sim_inv_rect_Type1 :
315 order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1
317 val order_sim_inv_rect_Type0 :
318 order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1
320 val order_sim_jmdiscr : order_sim -> order_sim -> __