extracted/smallstep.ml

   1 open Preamble
   2
   3 open CostLabel
   4
   5 open Proper
   6
   7 open PositiveMap
   8
   9 open Deqsets
  10
  11 open Extralib
  12
  13 open Lists
  14
  15 open Identifiers
  16
  17 open Integers
  18
  19 open AST
  20
  21 open Division
  22
  23 open Exp
  24
  25 open Arithmetic
  26
  27 open Extranat
  28
  29 open Vector
  30
  31 open FoldStuff
  32
  33 open BitVector
  34
  35 open Z
  36
  37 open BitVectorZ
  38
  39 open Pointers
  40
  41 open ErrorMessages
  42
  43 open Option
  44
  45 open Setoids
  46
  47 open Monad
  48
  49 open Positive
  50
  51 open PreIdentifiers
  52
  53 open Errors
  54
  55 open Div_and_mod
  56
  57 open Jmeq
  58
  59 open Russell
  60
  61 open Util
  62
  63 open Bool
  64
  65 open Relations
  66
  67 open Nat
  68
  69 open List
  70
  71 open Hints_declaration
  72
  73 open Core_notation
  74
  75 open Pts
  76
  77 open Logic
  78
  79 open Types
  80
  81 open Coqlib
  82
  83 open Values
  84
  85 open Events
  86
  87 type transrel =
  88 | Mk_transrel
  89
  90 (** val transrel_rect_Type4 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
  91 let rec transrel_rect_Type4 h_mk_transrel = function
  92 | Mk_transrel -> h_mk_transrel __ __ __
  93
  94 (** val transrel_rect_Type5 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
  95 let rec transrel_rect_Type5 h_mk_transrel = function
  96 | Mk_transrel -> h_mk_transrel __ __ __
  97
  98 (** val transrel_rect_Type3 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
  99 let rec transrel_rect_Type3 h_mk_transrel = function
 100 | Mk_transrel -> h_mk_transrel __ __ __
 101
 102 (** val transrel_rect_Type2 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
 103 let rec transrel_rect_Type2 h_mk_transrel = function
 104 | Mk_transrel -> h_mk_transrel __ __ __
 105
 106 (** val transrel_rect_Type1 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
 107 let rec transrel_rect_Type1 h_mk_transrel = function
 108 | Mk_transrel -> h_mk_transrel __ __ __
 109
 110 (** val transrel_rect_Type0 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
 111 let rec transrel_rect_Type0 h_mk_transrel = function
 112 | Mk_transrel -> h_mk_transrel __ __ __
 113
 114 type genv = __
 115
 116 type state = __
 117
 118 (** val transrel_inv_rect_Type4 :
 119     transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 120 let transrel_inv_rect_Type4 hterm h1 =
 121   let hcut = transrel_rect_Type4 h1 hterm in hcut __
 122
 123 (** val transrel_inv_rect_Type3 :
 124     transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 125 let transrel_inv_rect_Type3 hterm h1 =
 126   let hcut = transrel_rect_Type3 h1 hterm in hcut __
 127
 128 (** val transrel_inv_rect_Type2 :
 129     transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 130 let transrel_inv_rect_Type2 hterm h1 =
 131   let hcut = transrel_rect_Type2 h1 hterm in hcut __
 132
 133 (** val transrel_inv_rect_Type1 :
 134     transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 135 let transrel_inv_rect_Type1 hterm h1 =
 136   let hcut = transrel_rect_Type1 h1 hterm in hcut __
 137
 138 (** val transrel_inv_rect_Type0 :
 139     transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 140 let transrel_inv_rect_Type0 hterm h1 =
 141   let hcut = transrel_rect_Type0 h1 hterm in hcut __
 142
 143 (** val transrel_jmdiscr : transrel -> transrel -> __ **)
 144 let transrel_jmdiscr x y =
 145   Logic.eq_rect_Type2 x
 146     (let Mk_transrel = x in Obj.magic (fun _ dH -> dH __ __ __)) y
 147
 148 type program_behavior =
 149 | Terminates of Events.trace * Integers.int
 150 | Diverges of Events.trace
 151 | Reacts of Events.traceinf
 152 | Goes_wrong of Events.trace
 153
 154 (** val program_behavior_rect_Type4 :
 155     (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
 156     (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
 157     'a1 **)
 158 let rec program_behavior_rect_Type4 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
 159 | Terminates (x_6965, x_6964) -> h_Terminates x_6965 x_6964
 160 | Diverges x_6966 -> h_Diverges x_6966
 161 | Reacts x_6967 -> h_Reacts x_6967
 162 | Goes_wrong x_6968 -> h_Goes_wrong x_6968
 163
 164 (** val program_behavior_rect_Type5 :
 165     (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
 166     (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
 167     'a1 **)
 168 let rec program_behavior_rect_Type5 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
 169 | Terminates (x_6975, x_6974) -> h_Terminates x_6975 x_6974
 170 | Diverges x_6976 -> h_Diverges x_6976
 171 | Reacts x_6977 -> h_Reacts x_6977
 172 | Goes_wrong x_6978 -> h_Goes_wrong x_6978
 173
 174 (** val program_behavior_rect_Type3 :
 175     (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
 176     (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
 177     'a1 **)
 178 let rec program_behavior_rect_Type3 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
 179 | Terminates (x_6985, x_6984) -> h_Terminates x_6985 x_6984
 180 | Diverges x_6986 -> h_Diverges x_6986
 181 | Reacts x_6987 -> h_Reacts x_6987
 182 | Goes_wrong x_6988 -> h_Goes_wrong x_6988
 183
 184 (** val program_behavior_rect_Type2 :
 185     (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
 186     (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
 187     'a1 **)
 188 let rec program_behavior_rect_Type2 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
 189 | Terminates (x_6995, x_6994) -> h_Terminates x_6995 x_6994
 190 | Diverges x_6996 -> h_Diverges x_6996
 191 | Reacts x_6997 -> h_Reacts x_6997
 192 | Goes_wrong x_6998 -> h_Goes_wrong x_6998
 193
 194 (** val program_behavior_rect_Type1 :
 195     (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
 196     (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
 197     'a1 **)
 198 let rec program_behavior_rect_Type1 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
 199 | Terminates (x_7005, x_7004) -> h_Terminates x_7005 x_7004
 200 | Diverges x_7006 -> h_Diverges x_7006
 201 | Reacts x_7007 -> h_Reacts x_7007
 202 | Goes_wrong x_7008 -> h_Goes_wrong x_7008
 203
 204 (** val program_behavior_rect_Type0 :
 205     (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
 206     (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
 207     'a1 **)
 208 let rec program_behavior_rect_Type0 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
 209 | Terminates (x_7015, x_7014) -> h_Terminates x_7015 x_7014
 210 | Diverges x_7016 -> h_Diverges x_7016
 211 | Reacts x_7017 -> h_Reacts x_7017
 212 | Goes_wrong x_7018 -> h_Goes_wrong x_7018
 213
 214 (** val program_behavior_inv_rect_Type4 :
 215     program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
 216     (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
 217     (Events.trace -> __ -> 'a1) -> 'a1 **)
 218 let program_behavior_inv_rect_Type4 hterm h1 h2 h3 h4 =
 219   let hcut = program_behavior_rect_Type4 h1 h2 h3 h4 hterm in hcut __
 220
 221 (** val program_behavior_inv_rect_Type3 :
 222     program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
 223     (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
 224     (Events.trace -> __ -> 'a1) -> 'a1 **)
 225 let program_behavior_inv_rect_Type3 hterm h1 h2 h3 h4 =
 226   let hcut = program_behavior_rect_Type3 h1 h2 h3 h4 hterm in hcut __
 227
 228 (** val program_behavior_inv_rect_Type2 :
 229     program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
 230     (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
 231     (Events.trace -> __ -> 'a1) -> 'a1 **)
 232 let program_behavior_inv_rect_Type2 hterm h1 h2 h3 h4 =
 233   let hcut = program_behavior_rect_Type2 h1 h2 h3 h4 hterm in hcut __
 234
 235 (** val program_behavior_inv_rect_Type1 :
 236     program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
 237     (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
 238     (Events.trace -> __ -> 'a1) -> 'a1 **)
 239 let program_behavior_inv_rect_Type1 hterm h1 h2 h3 h4 =
 240   let hcut = program_behavior_rect_Type1 h1 h2 h3 h4 hterm in hcut __
 241
 242 (** val program_behavior_inv_rect_Type0 :
 243     program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
 244     (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
 245     (Events.trace -> __ -> 'a1) -> 'a1 **)
 246 let program_behavior_inv_rect_Type0 hterm h1 h2 h3 h4 =
 247   let hcut = program_behavior_rect_Type0 h1 h2 h3 h4 hterm in hcut __
 248
 249 (** val program_behavior_discr :
 250     program_behavior -> program_behavior -> __ **)
 251 let program_behavior_discr x y =
 252   Logic.eq_rect_Type2 x
 253     (match x with
 254      | Terminates (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 255      | Diverges a0 -> Obj.magic (fun _ dH -> dH __)
 256      | Reacts a0 -> Obj.magic (fun _ dH -> dH __)
 257      | Goes_wrong a0 -> Obj.magic (fun _ dH -> dH __)) y
 258
 259 (** val program_behavior_jmdiscr :
 260     program_behavior -> program_behavior -> __ **)
 261 let program_behavior_jmdiscr x y =
 262   Logic.eq_rect_Type2 x
 263     (match x with
 264      | Terminates (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 265      | Diverges a0 -> Obj.magic (fun _ dH -> dH __)
 266      | Reacts a0 -> Obj.magic (fun _ dH -> dH __)
 267      | Goes_wrong a0 -> Obj.magic (fun _ dH -> dH __)) y
 268
 269 type semantics = { trans : transrel; ge : __ }
 270
 271 (** val semantics_rect_Type4 :
 272     (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
 273 let rec semantics_rect_Type4 h_mk_semantics x_7345 =
 274   let { trans = trans0; ge = ge0 } = x_7345 in
 275   h_mk_semantics trans0 __ __ ge0
 276
 277 (** val semantics_rect_Type5 :
 278     (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
 279 let rec semantics_rect_Type5 h_mk_semantics x_7347 =
 280   let { trans = trans0; ge = ge0 } = x_7347 in
 281   h_mk_semantics trans0 __ __ ge0
 282
 283 (** val semantics_rect_Type3 :
 284     (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
 285 let rec semantics_rect_Type3 h_mk_semantics x_7349 =
 286   let { trans = trans0; ge = ge0 } = x_7349 in
 287   h_mk_semantics trans0 __ __ ge0
 288
 289 (** val semantics_rect_Type2 :
 290     (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
 291 let rec semantics_rect_Type2 h_mk_semantics x_7351 =
 292   let { trans = trans0; ge = ge0 } = x_7351 in
 293   h_mk_semantics trans0 __ __ ge0
 294
 295 (** val semantics_rect_Type1 :
 296     (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
 297 let rec semantics_rect_Type1 h_mk_semantics x_7353 =
 298   let { trans = trans0; ge = ge0 } = x_7353 in
 299   h_mk_semantics trans0 __ __ ge0
 300
 301 (** val semantics_rect_Type0 :
 302     (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
 303 let rec semantics_rect_Type0 h_mk_semantics x_7355 =
 304   let { trans = trans0; ge = ge0 } = x_7355 in
 305   h_mk_semantics trans0 __ __ ge0
 306
 307 (** val trans : semantics -> transrel **)
 308 let rec trans xxx =
 309   xxx.trans
 310
 311 (** val ge : semantics -> __ **)
 312 let rec ge xxx =
 313   xxx.ge
 314
 315 (** val semantics_inv_rect_Type4 :
 316     semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 317 let semantics_inv_rect_Type4 hterm h1 =
 318   let hcut = semantics_rect_Type4 h1 hterm in hcut __
 319
 320 (** val semantics_inv_rect_Type3 :
 321     semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 322 let semantics_inv_rect_Type3 hterm h1 =
 323   let hcut = semantics_rect_Type3 h1 hterm in hcut __
 324
 325 (** val semantics_inv_rect_Type2 :
 326     semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 327 let semantics_inv_rect_Type2 hterm h1 =
 328   let hcut = semantics_rect_Type2 h1 hterm in hcut __
 329
 330 (** val semantics_inv_rect_Type1 :
 331     semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 332 let semantics_inv_rect_Type1 hterm h1 =
 333   let hcut = semantics_rect_Type1 h1 hterm in hcut __
 334
 335 (** val semantics_inv_rect_Type0 :
 336     semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 337 let semantics_inv_rect_Type0 hterm h1 =
 338   let hcut = semantics_rect_Type0 h1 hterm in hcut __
 339
 340 (** val semantics_jmdiscr : semantics -> semantics -> __ **)
 341 let semantics_jmdiscr x y =
 342   Logic.eq_rect_Type2 x
 343     (let { trans = a0; ge = a3 } = x in
 344     Obj.magic (fun _ dH -> dH __ __ __ __)) y
 345
 346 type related_semantics = { sem1 : semantics; sem2 : semantics }
 347
 348 (** val related_semantics_rect_Type4 :
 349     (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
 350     'a1 **)
 351 let rec related_semantics_rect_Type4 h_mk_related_semantics x_7374 =
 352   let { sem1 = sem3; sem2 = sem4 } = x_7374 in
 353   h_mk_related_semantics sem3 sem4 __ __ __
 354
 355 (** val related_semantics_rect_Type5 :
 356     (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
 357     'a1 **)
 358 let rec related_semantics_rect_Type5 h_mk_related_semantics x_7376 =
 359   let { sem1 = sem3; sem2 = sem4 } = x_7376 in
 360   h_mk_related_semantics sem3 sem4 __ __ __
 361
 362 (** val related_semantics_rect_Type3 :
 363     (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
 364     'a1 **)
 365 let rec related_semantics_rect_Type3 h_mk_related_semantics x_7378 =
 366   let { sem1 = sem3; sem2 = sem4 } = x_7378 in
 367   h_mk_related_semantics sem3 sem4 __ __ __
 368
 369 (** val related_semantics_rect_Type2 :
 370     (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
 371     'a1 **)
 372 let rec related_semantics_rect_Type2 h_mk_related_semantics x_7380 =
 373   let { sem1 = sem3; sem2 = sem4 } = x_7380 in
 374   h_mk_related_semantics sem3 sem4 __ __ __
 375
 376 (** val related_semantics_rect_Type1 :
 377     (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
 378     'a1 **)
 379 let rec related_semantics_rect_Type1 h_mk_related_semantics x_7382 =
 380   let { sem1 = sem3; sem2 = sem4 } = x_7382 in
 381   h_mk_related_semantics sem3 sem4 __ __ __
 382
 383 (** val related_semantics_rect_Type0 :
 384     (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
 385     'a1 **)
 386 let rec related_semantics_rect_Type0 h_mk_related_semantics x_7384 =
 387   let { sem1 = sem3; sem2 = sem4 } = x_7384 in
 388   h_mk_related_semantics sem3 sem4 __ __ __
 389
 390 (** val sem1 : related_semantics -> semantics **)
 391 let rec sem1 xxx =
 392   xxx.sem1
 393
 394 (** val sem2 : related_semantics -> semantics **)
 395 let rec sem2 xxx =
 396   xxx.sem2
 397
 398 (** val related_semantics_inv_rect_Type4 :
 399     related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
 400     'a1) -> 'a1 **)
 401 let related_semantics_inv_rect_Type4 hterm h1 =
 402   let hcut = related_semantics_rect_Type4 h1 hterm in hcut __
 403
 404 (** val related_semantics_inv_rect_Type3 :
 405     related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
 406     'a1) -> 'a1 **)
 407 let related_semantics_inv_rect_Type3 hterm h1 =
 408   let hcut = related_semantics_rect_Type3 h1 hterm in hcut __
 409
 410 (** val related_semantics_inv_rect_Type2 :
 411     related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
 412     'a1) -> 'a1 **)
 413 let related_semantics_inv_rect_Type2 hterm h1 =
 414   let hcut = related_semantics_rect_Type2 h1 hterm in hcut __
 415
 416 (** val related_semantics_inv_rect_Type1 :
 417     related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
 418     'a1) -> 'a1 **)
 419 let related_semantics_inv_rect_Type1 hterm h1 =
 420   let hcut = related_semantics_rect_Type1 h1 hterm in hcut __
 421
 422 (** val related_semantics_inv_rect_Type0 :
 423     related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
 424     'a1) -> 'a1 **)
 425 let related_semantics_inv_rect_Type0 hterm h1 =
 426   let hcut = related_semantics_rect_Type0 h1 hterm in hcut __
 427
 428 (** val related_semantics_jmdiscr :
 429     related_semantics -> related_semantics -> __ **)
 430 let related_semantics_jmdiscr x y =
 431   Logic.eq_rect_Type2 x
 432     (let { sem1 = a0; sem2 = a1 } = x in
 433     Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
 434
 435 type order_sim =
 436   related_semantics
 437   (* singleton inductive, whose constructor was mk_order_sim *)
 438
 439 (** val order_sim_rect_Type4 :
 440     (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
 441 let rec order_sim_rect_Type4 h_mk_order_sim x_7405 =
 442   let sem = x_7405 in h_mk_order_sim sem __ __
 443
 444 (** val order_sim_rect_Type5 :
 445     (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
 446 let rec order_sim_rect_Type5 h_mk_order_sim x_7407 =
 447   let sem = x_7407 in h_mk_order_sim sem __ __
 448
 449 (** val order_sim_rect_Type3 :
 450     (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
 451 let rec order_sim_rect_Type3 h_mk_order_sim x_7409 =
 452   let sem = x_7409 in h_mk_order_sim sem __ __
 453
 454 (** val order_sim_rect_Type2 :
 455     (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
 456 let rec order_sim_rect_Type2 h_mk_order_sim x_7411 =
 457   let sem = x_7411 in h_mk_order_sim sem __ __
 458
 459 (** val order_sim_rect_Type1 :
 460     (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
 461 let rec order_sim_rect_Type1 h_mk_order_sim x_7413 =
 462   let sem = x_7413 in h_mk_order_sim sem __ __
 463
 464 (** val order_sim_rect_Type0 :
 465     (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
 466 let rec order_sim_rect_Type0 h_mk_order_sim x_7415 =
 467   let sem = x_7415 in h_mk_order_sim sem __ __
 468
 469 (** val sem : order_sim -> related_semantics **)
 470 let rec sem xxx =
 471   let yyy = xxx in yyy
 472
 473 (** val order_sim_inv_rect_Type4 :
 474     order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 475 let order_sim_inv_rect_Type4 hterm h1 =
 476   let hcut = order_sim_rect_Type4 h1 hterm in hcut __
 477
 478 (** val order_sim_inv_rect_Type3 :
 479     order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 480 let order_sim_inv_rect_Type3 hterm h1 =
 481   let hcut = order_sim_rect_Type3 h1 hterm in hcut __
 482
 483 (** val order_sim_inv_rect_Type2 :
 484     order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 485 let order_sim_inv_rect_Type2 hterm h1 =
 486   let hcut = order_sim_rect_Type2 h1 hterm in hcut __
 487
 488 (** val order_sim_inv_rect_Type1 :
 489     order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 490 let order_sim_inv_rect_Type1 hterm h1 =
 491   let hcut = order_sim_rect_Type1 h1 hterm in hcut __
 492
 493 (** val order_sim_inv_rect_Type0 :
 494     order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 495 let order_sim_inv_rect_Type0 hterm h1 =
 496   let hcut = order_sim_rect_Type0 h1 hterm in hcut __
 497
 498 (** val order_sim_jmdiscr : order_sim -> order_sim -> __ **)
 499 let order_sim_jmdiscr x y =
 500   Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __ __)) y
 501