(* Test that words can handle numbers between 0 and 31 *)
val _ = if 5 <= Word.wordSize then () else raise (Fail ("wordSize less than 5"));

structure Uint32 : sig
  val set_bit : Word32.word -> IntInf.int -> bool -> Word32.word
  val shiftl : Word32.word -> IntInf.int -> Word32.word
  val shiftr : Word32.word -> IntInf.int -> Word32.word
  val shiftr_signed : Word32.word -> IntInf.int -> Word32.word
  val test_bit : Word32.word -> IntInf.int -> bool
end = struct

fun set_bit x n b =
  let val mask = Word32.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))
  in if b then Word32.orb (x, mask)
     else Word32.andb (x, Word32.notb mask)
  end

fun shiftl x n =
  Word32.<< (x, Word.fromLargeInt (IntInf.toLarge n))

fun shiftr x n =
  Word32.>> (x, Word.fromLargeInt (IntInf.toLarge n))

fun shiftr_signed x n =
  Word32.~>> (x, Word.fromLargeInt (IntInf.toLarge n))

fun test_bit x n =
  Word32.andb (x, Word32.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word32.fromInt 0

end; (* struct Uint32 *)


structure STArray = struct

datatype 'a Cell = Invalid | Value of 'a array;

exception AccessedOldVersion;

type 'a array = 'a Cell Unsynchronized.ref;

fun fromList l = Unsynchronized.ref (Value (Array.fromList l));
fun array (size, v) = Unsynchronized.ref (Value (Array.array (size,v)));
fun tabulate (size, f) = Unsynchronized.ref (Value (Array.tabulate(size, f)));
fun sub (Unsynchronized.ref Invalid, idx) = raise AccessedOldVersion |
    sub (Unsynchronized.ref (Value a), idx) = Array.sub (a,idx);
fun update (aref,idx,v) =
  case aref of
    (Unsynchronized.ref Invalid) => raise AccessedOldVersion |
    (Unsynchronized.ref (Value a)) => (
      aref := Invalid;
      Array.update (a,idx,v);
      Unsynchronized.ref (Value a)
    );

fun length (Unsynchronized.ref Invalid) = raise AccessedOldVersion |
    length (Unsynchronized.ref (Value a)) = Array.length a

fun grow (aref, i, x) = case aref of 
  (Unsynchronized.ref Invalid) => raise AccessedOldVersion |
  (Unsynchronized.ref (Value a)) => (
    let val len=Array.length a;
        val na = Array.array (len+i,x) 
    in
      aref := Invalid;
      Array.copy {src=a, dst=na, di=0};
      Unsynchronized.ref (Value na)
    end
    );

fun shrink (aref, sz) = case aref of
  (Unsynchronized.ref Invalid) => raise AccessedOldVersion |
  (Unsynchronized.ref (Value a)) => (
    if sz > Array.length a then 
      raise Size
    else (
      aref:=Invalid;
      Unsynchronized.ref (Value (Array.tabulate (sz,fn i => Array.sub (a,i))))
    )
  );

structure IsabelleMapping = struct
type 'a ArrayType = 'a array;

fun new_array (a:'a) (n:int) = array (n, a);

fun array_length (a:'a ArrayType) = length a;

fun array_get (a:'a ArrayType) (i:int) = sub (a, i);

fun array_set (a:'a ArrayType) (i:int) (e:'a) = update (a, i, e);

fun array_of_list (xs:'a list) = fromList xs;

fun array_grow (a:'a ArrayType) (i:int) (x:'a) = grow (a, i, x);

fun array_shrink (a:'a ArrayType) (sz:int) = shrink (a,sz);

end;

end;

structure FArray = struct
  datatype 'a Cell = Value of 'a Array.array | Upd of (int*'a*'a Cell Unsynchronized.ref);

  type 'a array = 'a Cell Unsynchronized.ref;

  fun array (size,v) = Unsynchronized.ref (Value (Array.array (size,v)));
  fun tabulate (size, f) = Unsynchronized.ref (Value (Array.tabulate(size, f)));
  fun fromList l = Unsynchronized.ref (Value (Array.fromList l));

  fun sub (Unsynchronized.ref (Value a), idx) = Array.sub (a,idx) |
      sub (Unsynchronized.ref (Upd (i,v,cr)),idx) =
        if i=idx then v
        else sub (cr,idx);

  fun length (Unsynchronized.ref (Value a)) = Array.length a |
      length (Unsynchronized.ref (Upd (i,v,cr))) = length cr;

  fun realize_aux (aref, v) =
    case aref of
      (Unsynchronized.ref (Value a)) => (
        let
          val len = Array.length a;
          val a' = Array.array (len,v);
        in
          Array.copy {src=a, dst=a', di=0};
          Unsynchronized.ref (Value a')
        end
      ) |
      (Unsynchronized.ref (Upd (i,v,cr))) => (
        let val res=realize_aux (cr,v) in
          case res of
            (Unsynchronized.ref (Value a)) => (Array.update (a,i,v); res)
        end
      );

  fun realize aref =
    case aref of
      (Unsynchronized.ref (Value _)) => aref |
      (Unsynchronized.ref (Upd (i,v,cr))) => realize_aux(aref,v);

  fun update (aref,idx,v) =
    case aref of
      (Unsynchronized.ref (Value a)) => (
        let val nref=Unsynchronized.ref (Value a) in
          aref := Upd (idx,Array.sub(a,idx),nref);
          Array.update (a,idx,v);
          nref
        end
      ) |
      (Unsynchronized.ref (Upd _)) =>
        let val ra = realize_aux(aref,v) in
          case ra of
            (Unsynchronized.ref (Value a)) => Array.update (a,idx,v);
          ra
        end
      ;

  fun grow (aref, inc, x) = case aref of 
    (Unsynchronized.ref (Value a)) => (
      let val len=Array.length a;
          val na = Array.array (len+inc,x) 
      in
        Array.copy {src=a, dst=na, di=0};
        Unsynchronized.ref (Value na)
      end
      )
  | (Unsynchronized.ref (Upd _)) => (
    grow (realize aref, inc, x)
  );

  fun shrink (aref, sz) = case aref of
    (Unsynchronized.ref (Value a)) => (
      if sz > Array.length a then 
        raise Size
      else (
        Unsynchronized.ref (Value (Array.tabulate (sz,fn i => Array.sub (a,i))))
      )
    ) |
    (Unsynchronized.ref (Upd _)) => (
      shrink (realize aref,sz)
    );

structure IsabelleMapping = struct
type 'a ArrayType = 'a array;

fun new_array (a:'a) (n:int) = array (n, a);

fun array_length (a:'a ArrayType) = length a;

fun array_get (a:'a ArrayType) (i:int) = sub (a, i);

fun array_set (a:'a ArrayType) (i:int) (e:'a) = update (a, i, e);

fun array_of_list (xs:'a list) = fromList xs;

fun array_grow (a:'a ArrayType) (i:int) (x:'a) = grow (a, i, x);

fun array_shrink (a:'a ArrayType) (sz:int) = shrink (a,sz);

fun array_get_oo (d:'a) (a:'a ArrayType) (i:int) = 
  sub (a,i) handle Subscript => d

fun array_set_oo (d:(unit->'a ArrayType)) (a:'a ArrayType) (i:int) (e:'a) = 
  update (a, i, e) handle Subscript => d ()

end;
end;




structure Bits_Integer : sig
  val set_bit : IntInf.int -> IntInf.int -> bool -> IntInf.int
  val shiftl : IntInf.int -> IntInf.int -> IntInf.int
  val shiftr : IntInf.int -> IntInf.int -> IntInf.int
  val test_bit : IntInf.int -> IntInf.int -> bool
end = struct

val maxWord = IntInf.pow (2, Word.wordSize);

fun set_bit x n b =
  if n < maxWord then
    if b then IntInf.orb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n)))
    else IntInf.andb (x, IntInf.notb (IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))))
  else raise (Fail ("Bit index too large: " ^ IntInf.toString n));

fun shiftl x n =
  if n < maxWord then IntInf.<< (x, Word.fromLargeInt (IntInf.toLarge n))
  else raise (Fail ("Shift operand too large: " ^ IntInf.toString n));

fun shiftr x n =
  if n < maxWord then IntInf.~>> (x, Word.fromLargeInt (IntInf.toLarge n))
  else raise (Fail ("Shift operand too large: " ^ IntInf.toString n));

fun test_bit x n =
  if n < maxWord then IntInf.andb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))) <> 0
  else raise (Fail ("Bit index too large: " ^ IntInf.toString n));

end; (*struct Bits_Integer*)

structure Lorenz : sig
  datatype int = Int_of_integer of IntInf.int
  type num
  type nat
  type float
  type real
  type 'a pdevs
  type nibble
  type char
  type 'a sctn
  type 'a dres
  type ('a, 'b, 'c, 'd) options_ext
  val nat_of_integer : IntInf.int -> nat
  val lorenzc :
    int ->
      int ->
        int ->
          int ->
            int ->
              int ->
                int ->
                  int ->
                    int ->
                      int ->
                        ((((real * (real * real)) *
                            (real * (real * real)) pdevs) list *
                           (real * (real * real)) sctn) list)
                          dres
  val lorenz_irects : nat -> nat -> int -> int -> ((int list) list) dres
end = struct

type 'a uminus = {uminus : 'a -> 'a};
val uminus = #uminus : 'a uminus -> 'a -> 'a;

fun uminus_funa B_ a x = uminus B_ (a x);

fun uminus_fun B_ = {uminus = uminus_funa B_} : ('a -> 'b) uminus;

datatype int = Int_of_integer of IntInf.int;

fun integer_of_int (Int_of_integer k) = k;

fun equal_inta k l = (((integer_of_int k) : IntInf.int) = (integer_of_int l));

type 'a equal = {equal : 'a -> 'a -> bool};
val equal = #equal : 'a equal -> 'a -> 'a -> bool;

val equal_int = {equal = equal_inta} : int equal;

fun uminus_inta k = Int_of_integer (IntInf.~ (integer_of_int k));

val zero_inta : int = Int_of_integer (0 : IntInf.int);

fun less_int k l = IntInf.< (integer_of_int k, integer_of_int l);

fun abs_inta i = (if less_int i zero_inta then uminus_inta i else i);

type 'a abs = {abs : 'a -> 'a};
val abs = #abs : 'a abs -> 'a -> 'a;

val abs_int = {abs = abs_inta} : int abs;

datatype num = One | Bit0 of num | Bit1 of num;

val one_inta : int = Int_of_integer (1 : IntInf.int);

type 'a one = {one : 'a};
val one = #one : 'a one -> 'a;

val one_int = {one = one_inta} : int one;

fun plus_inta k l =
  Int_of_integer (IntInf.+ (integer_of_int k, integer_of_int l));

type 'a plus = {plus : 'a -> 'a -> 'a};
val plus = #plus : 'a plus -> 'a -> 'a -> 'a;

val plus_int = {plus = plus_inta} : int plus;

type 'a zero = {zero : 'a};
val zero = #zero : 'a zero -> 'a;

val zero_int = {zero = zero_inta} : int zero;

fun times_inta k l =
  Int_of_integer (IntInf.* (integer_of_int k, integer_of_int l));

type 'a times = {times : 'a -> 'a -> 'a};
val times = #times : 'a times -> 'a -> 'a -> 'a;

type 'a power = {one_power : 'a one, times_power : 'a times};
val one_power = #one_power : 'a power -> 'a one;
val times_power = #times_power : 'a power -> 'a times;

val times_int = {times = times_inta} : int times;

val power_int = {one_power = one_int, times_power = times_int} : int power;

fun minus_inta k l =
  Int_of_integer (IntInf.- (integer_of_int k, integer_of_int l));

type 'a minus = {minus : 'a -> 'a -> 'a};
val minus = #minus : 'a minus -> 'a -> 'a -> 'a;

val minus_int = {minus = minus_inta} : int minus;

val uminus_int = {uminus = uminus_inta} : int uminus;

fun less_eq_int k l = IntInf.<= (integer_of_int k, integer_of_int l);

type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};
val less_eq = #less_eq : 'a ord -> 'a -> 'a -> bool;
val less = #less : 'a ord -> 'a -> 'a -> bool;

val ord_int = {less_eq = less_eq_int, less = less_int} : int ord;

datatype nat = Nat of IntInf.int;

fun integer_of_nat (Nat x) = x;

fun equal_nata m n = (((integer_of_nat m) : IntInf.int) = (integer_of_nat n));

val equal_nat = {equal = equal_nata} : nat equal;

fun less_eq_nat m n = IntInf.<= (integer_of_nat m, integer_of_nat n);

fun less_nat m n = IntInf.< (integer_of_nat m, integer_of_nat n);

val ord_nat = {less_eq = less_eq_nat, less = less_nat} : nat ord;

type 'a preorder = {ord_preorder : 'a ord};
val ord_preorder = #ord_preorder : 'a preorder -> 'a ord;

type 'a order = {preorder_order : 'a preorder};
val preorder_order = #preorder_order : 'a order -> 'a preorder;

val preorder_nat = {ord_preorder = ord_nat} : nat preorder;

val order_nat = {preorder_order = preorder_nat} : nat order;

type 'a linorder = {order_linorder : 'a order};
val order_linorder = #order_linorder : 'a linorder -> 'a order;

val linorder_nat = {order_linorder = order_nat} : nat linorder;

fun uminus_boola x = not x;

val uminus_bool = {uminus = uminus_boola} : bool uminus;

fun eq A_ a b = equal A_ a b;

fun equal_lista A_ [] (x21 :: x22) = false
  | equal_lista A_ (x21 :: x22) [] = false
  | equal_lista A_ (x21 :: x22) (y21 :: y22) =
    eq A_ x21 y21 andalso equal_lista A_ x22 y22
  | equal_lista A_ [] [] = true;

fun equal_list A_ = {equal = equal_lista A_} : ('a list) equal;

datatype float = Float of int * int;

fun uminus_floata (Float (m1, e1)) = Float (uminus_inta m1, e1);

fun power_inta (Int_of_integer a) (Int_of_integer b) =
  Int_of_integer (IntInf.pow (a, b));

fun plus_floata (Float (m1, e1)) (Float (m2, e2)) =
  (if equal_inta m1 zero_inta then Float (m2, e2)
    else (if equal_inta m2 zero_inta then Float (m1, e1)
           else (if less_eq_int e1 e2
                  then Float (plus_inta m1
                                (times_inta m2
                                  (power_inta (Int_of_integer (2 : IntInf.int))
                                    (minus_inta e2 e1))),
                               e1)
                  else Float (plus_inta m2
                                (times_inta m1
                                  (power_inta (Int_of_integer (2 : IntInf.int))
                                    (minus_inta e1 e2))),
                               e2))));

fun minus_floata f g = plus_floata f (uminus_floata g);

fun is_float_zero (Float (m, e)) = equal_inta zero_inta m;

fun equal_float f g = is_float_zero (minus_floata f g);

datatype real = Floatreal of float;

fun equal_reala (Floatreal x) (Floatreal y) = equal_float x y;

val equal_real = {equal = equal_reala} : real equal;

fun abs_float (Float (m, e)) = Float (abs_inta m, e);

fun abs_reala (Floatreal x) = Floatreal (abs_float x);

val abs_real = {abs = abs_reala} : real abs;

val one_reala : real =
  Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta));

val one_real = {one = one_reala} : real one;

fun uminus_reala (Floatreal x) = Floatreal (uminus_floata x);

fun is_float_pos (Float (m, e)) = less_int zero_inta m;

fun less_float a b = is_float_pos (minus_floata b a);

fun less_real (Floatreal x) (Floatreal y) = less_float x y;

fun sgn_reala a =
  (if equal_reala a (Floatreal (Float (zero_inta, zero_inta)))
    then Floatreal (Float (zero_inta, zero_inta))
    else (if less_real (Floatreal (Float (zero_inta, zero_inta))) a
           then Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta))
           else uminus_reala
                  (Floatreal
                    (Float (Int_of_integer (1 : IntInf.int), zero_inta)))));

type 'a sgn = {sgn : 'a -> 'a};
val sgn = #sgn : 'a sgn -> 'a -> 'a;

val sgn_real = {sgn = sgn_reala} : real sgn;

fun plus_reala (Floatreal x) (Floatreal y) = Floatreal (plus_floata x y);

val plus_real = {plus = plus_reala} : real plus;

val zero_reala : real = Floatreal (Float (zero_inta, zero_inta));

val zero_real = {zero = zero_reala} : real zero;

fun times_floata (Float (m1, e1)) (Float (m2, e2)) =
  Float (times_inta m1 m2, plus_inta e1 e2);

fun times_reala (Floatreal x) (Floatreal y) = Floatreal (times_floata x y);

val times_real = {times = times_reala} : real times;

val power_real = {one_power = one_real, times_power = times_real} : real power;

fun minus_reala (Floatreal x) (Floatreal y) = Floatreal (minus_floata x y);

val minus_real = {minus = minus_reala} : real minus;

fun min A_ a b = (if less_eq A_ a b then a else b);

fun is_float_nonneg (Float (m, e)) = less_eq_int zero_inta m;

fun less_eq_float a b = is_float_nonneg (minus_floata b a);

fun less_eq_real (Floatreal x) (Floatreal y) = less_eq_float x y;

val ord_real = {less_eq = less_eq_real, less = less_real} : real ord;

fun inf_realc x = min ord_real x;

type 'a inf = {inf : 'a -> 'a -> 'a};
val inf = #inf : 'a inf -> 'a -> 'a -> 'a;

val inf_real = {inf = inf_realc} : real inf;

fun max A_ a b = (if less_eq A_ a b then b else a);

fun sup_realc x = max ord_real x;

type 'a sup = {sup : 'a -> 'a -> 'a};
val sup = #sup : 'a sup -> 'a -> 'a -> 'a;

val sup_real = {sup = sup_realc} : real sup;

val uminus_real = {uminus = uminus_reala} : real uminus;

val preorder_real = {ord_preorder = ord_real} : real preorder;

val order_real = {preorder_order = preorder_real} : real order;

type 'a semigroup_add = {plus_semigroup_add : 'a plus};
val plus_semigroup_add = #plus_semigroup_add : 'a semigroup_add -> 'a plus;

type 'a cancel_semigroup_add =
  {semigroup_add_cancel_semigroup_add : 'a semigroup_add};
val semigroup_add_cancel_semigroup_add = #semigroup_add_cancel_semigroup_add :
  'a cancel_semigroup_add -> 'a semigroup_add;

type 'a monoid_add =
  {semigroup_add_monoid_add : 'a semigroup_add, zero_monoid_add : 'a zero};
val semigroup_add_monoid_add = #semigroup_add_monoid_add :
  'a monoid_add -> 'a semigroup_add;
val zero_monoid_add = #zero_monoid_add : 'a monoid_add -> 'a zero;

type 'a group_add =
  {cancel_semigroup_add_group_add : 'a cancel_semigroup_add,
    minus_group_add : 'a minus, monoid_add_group_add : 'a monoid_add,
    uminus_group_add : 'a uminus};
val cancel_semigroup_add_group_add = #cancel_semigroup_add_group_add :
  'a group_add -> 'a cancel_semigroup_add;
val minus_group_add = #minus_group_add : 'a group_add -> 'a minus;
val monoid_add_group_add = #monoid_add_group_add :
  'a group_add -> 'a monoid_add;
val uminus_group_add = #uminus_group_add : 'a group_add -> 'a uminus;

val semigroup_add_real = {plus_semigroup_add = plus_real} : real semigroup_add;

val cancel_semigroup_add_real =
  {semigroup_add_cancel_semigroup_add = semigroup_add_real} :
  real cancel_semigroup_add;

val monoid_add_real =
  {semigroup_add_monoid_add = semigroup_add_real, zero_monoid_add = zero_real} :
  real monoid_add;

val group_add_real =
  {cancel_semigroup_add_group_add = cancel_semigroup_add_real,
    minus_group_add = minus_real, monoid_add_group_add = monoid_add_real,
    uminus_group_add = uminus_real}
  : real group_add;

type 'a semilattice_sup =
  {sup_semilattice_sup : 'a sup, order_semilattice_sup : 'a order};
val sup_semilattice_sup = #sup_semilattice_sup : 'a semilattice_sup -> 'a sup;
val order_semilattice_sup = #order_semilattice_sup :
  'a semilattice_sup -> 'a order;

type 'a semilattice_inf =
  {inf_semilattice_inf : 'a inf, order_semilattice_inf : 'a order};
val inf_semilattice_inf = #inf_semilattice_inf : 'a semilattice_inf -> 'a inf;
val order_semilattice_inf = #order_semilattice_inf :
  'a semilattice_inf -> 'a order;

type 'a lattice =
  {semilattice_inf_lattice : 'a semilattice_inf,
    semilattice_sup_lattice : 'a semilattice_sup};
val semilattice_inf_lattice = #semilattice_inf_lattice :
  'a lattice -> 'a semilattice_inf;
val semilattice_sup_lattice = #semilattice_sup_lattice :
  'a lattice -> 'a semilattice_sup;

val semilattice_sup_real =
  {sup_semilattice_sup = sup_real, order_semilattice_sup = order_real} :
  real semilattice_sup;

val semilattice_inf_real =
  {inf_semilattice_inf = inf_real, order_semilattice_inf = order_real} :
  real semilattice_inf;

val lattice_real =
  {semilattice_inf_lattice = semilattice_inf_real,
    semilattice_sup_lattice = semilattice_sup_real}
  : real lattice;

type 'a zero_neq_one = {one_zero_neq_one : 'a one, zero_zero_neq_one : 'a zero};
val one_zero_neq_one = #one_zero_neq_one : 'a zero_neq_one -> 'a one;
val zero_zero_neq_one = #zero_zero_neq_one : 'a zero_neq_one -> 'a zero;

val zero_neq_one_real =
  {one_zero_neq_one = one_real, zero_zero_neq_one = zero_real} :
  real zero_neq_one;

type 'a ab_semigroup_add = {semigroup_add_ab_semigroup_add : 'a semigroup_add};
val semigroup_add_ab_semigroup_add = #semigroup_add_ab_semigroup_add :
  'a ab_semigroup_add -> 'a semigroup_add;

type 'a cancel_ab_semigroup_add =
  {ab_semigroup_add_cancel_ab_semigroup_add : 'a ab_semigroup_add,
    cancel_semigroup_add_cancel_ab_semigroup_add : 'a cancel_semigroup_add};
val ab_semigroup_add_cancel_ab_semigroup_add =
  #ab_semigroup_add_cancel_ab_semigroup_add :
  'a cancel_ab_semigroup_add -> 'a ab_semigroup_add;
val cancel_semigroup_add_cancel_ab_semigroup_add =
  #cancel_semigroup_add_cancel_ab_semigroup_add :
  'a cancel_ab_semigroup_add -> 'a cancel_semigroup_add;

type 'a comm_monoid_add =
  {ab_semigroup_add_comm_monoid_add : 'a ab_semigroup_add,
    monoid_add_comm_monoid_add : 'a monoid_add};
val ab_semigroup_add_comm_monoid_add = #ab_semigroup_add_comm_monoid_add :
  'a comm_monoid_add -> 'a ab_semigroup_add;
val monoid_add_comm_monoid_add = #monoid_add_comm_monoid_add :
  'a comm_monoid_add -> 'a monoid_add;

type 'a cancel_comm_monoid_add =
  {cancel_ab_semigroup_add_cancel_comm_monoid_add : 'a cancel_ab_semigroup_add,
    comm_monoid_add_cancel_comm_monoid_add : 'a comm_monoid_add};
val cancel_ab_semigroup_add_cancel_comm_monoid_add =
  #cancel_ab_semigroup_add_cancel_comm_monoid_add :
  'a cancel_comm_monoid_add -> 'a cancel_ab_semigroup_add;
val comm_monoid_add_cancel_comm_monoid_add =
  #comm_monoid_add_cancel_comm_monoid_add :
  'a cancel_comm_monoid_add -> 'a comm_monoid_add;

type 'a ab_group_add =
  {cancel_comm_monoid_add_ab_group_add : 'a cancel_comm_monoid_add,
    group_add_ab_group_add : 'a group_add};
val cancel_comm_monoid_add_ab_group_add = #cancel_comm_monoid_add_ab_group_add :
  'a ab_group_add -> 'a cancel_comm_monoid_add;
val group_add_ab_group_add = #group_add_ab_group_add :
  'a ab_group_add -> 'a group_add;

val ab_semigroup_add_real =
  {semigroup_add_ab_semigroup_add = semigroup_add_real} : real ab_semigroup_add;

val cancel_ab_semigroup_add_real =
  {ab_semigroup_add_cancel_ab_semigroup_add = ab_semigroup_add_real,
    cancel_semigroup_add_cancel_ab_semigroup_add = cancel_semigroup_add_real}
  : real cancel_ab_semigroup_add;

val comm_monoid_add_real =
  {ab_semigroup_add_comm_monoid_add = ab_semigroup_add_real,
    monoid_add_comm_monoid_add = monoid_add_real}
  : real comm_monoid_add;

val cancel_comm_monoid_add_real =
  {cancel_ab_semigroup_add_cancel_comm_monoid_add =
     cancel_ab_semigroup_add_real,
    comm_monoid_add_cancel_comm_monoid_add = comm_monoid_add_real}
  : real cancel_comm_monoid_add;

val ab_group_add_real =
  {cancel_comm_monoid_add_ab_group_add = cancel_comm_monoid_add_real,
    group_add_ab_group_add = group_add_real}
  : real ab_group_add;

datatype 'a set = Set of 'a list | Coset of 'a list;

type 'a infa = {infa : 'a set -> 'a};
val infa = #infa : 'a infa -> 'a set -> 'a;

fun inf_realb _ = raise Fail "Real.Inf_real_inst.Inf_real";

val inf_reala = {infa = inf_realb} : real infa;

type 'a supa = {supa : 'a set -> 'a};
val supa = #supa : 'a supa -> 'a set -> 'a;

fun sup_realb _ = raise Fail "Real.Sup_real_inst.Sup_real";

val sup_reala = {supa = sup_realb} : real supa;

fun dist_reala x y = abs_reala (minus_reala x y);

type 'a dist = {dist : 'a -> 'a -> real};
val dist = #dist : 'a dist -> 'a -> 'a -> real;

val dist_real = {dist = dist_reala} : real dist;

fun norm_reala r = abs_reala r;

type 'a norm = {norm : 'a -> real};
val norm = #norm : 'a norm -> 'a -> real;

val norm_real = {norm = norm_reala} : real norm;

fun open_reala _ = raise Fail "Real_Vector_Spaces.open_real_inst.open_real";

type 'a opena = {opena : 'a set -> bool};
val opena = #opena : 'a opena -> 'a set -> bool;

val open_real = {opena = open_reala} : real opena;

fun scaleR_reala a x = times_reala a x;

fun inner_real x = times_reala x;

type 'a scaleR = {scaleR : real -> 'a -> 'a};
val scaleR = #scaleR : 'a scaleR -> real -> 'a -> 'a;

type 'a sgn_div_norm =
  {sgn_sgn_div_norm : 'a sgn, norm_sgn_div_norm : 'a norm,
    scaleR_sgn_div_norm : 'a scaleR};
val sgn_sgn_div_norm = #sgn_sgn_div_norm : 'a sgn_div_norm -> 'a sgn;
val norm_sgn_div_norm = #norm_sgn_div_norm : 'a sgn_div_norm -> 'a norm;
val scaleR_sgn_div_norm = #scaleR_sgn_div_norm : 'a sgn_div_norm -> 'a scaleR;

type 'a topological_space = {open_topological_space : 'a opena};
val open_topological_space = #open_topological_space :
  'a topological_space -> 'a opena;

type 'a first_countable_topology =
  {topological_space_first_countable_topology : 'a topological_space};
val topological_space_first_countable_topology =
  #topological_space_first_countable_topology :
  'a first_countable_topology -> 'a topological_space;

type 'a open_dist = {dist_open_dist : 'a dist, open_open_dist : 'a opena};
val dist_open_dist = #dist_open_dist : 'a open_dist -> 'a dist;
val open_open_dist = #open_open_dist : 'a open_dist -> 'a opena;

type 'a t0_space = {topological_space_t0_space : 'a topological_space};
val topological_space_t0_space = #topological_space_t0_space :
  'a t0_space -> 'a topological_space;

type 'a t1_space = {t0_space_t1_space : 'a t0_space};
val t0_space_t1_space = #t0_space_t1_space : 'a t1_space -> 'a t0_space;

type 'a t2_space = {t1_space_t2_space : 'a t1_space};
val t1_space_t2_space = #t1_space_t2_space : 'a t2_space -> 'a t1_space;

type 'a metric_space =
  {open_dist_metric_space : 'a open_dist,
    first_countable_topology_metric_space : 'a first_countable_topology,
    t2_space_metric_space : 'a t2_space};
val open_dist_metric_space = #open_dist_metric_space :
  'a metric_space -> 'a open_dist;
val first_countable_topology_metric_space =
  #first_countable_topology_metric_space :
  'a metric_space -> 'a first_countable_topology;
val t2_space_metric_space = #t2_space_metric_space :
  'a metric_space -> 'a t2_space;

type 'a real_vector =
  {ab_group_add_real_vector : 'a ab_group_add, scaleR_real_vector : 'a scaleR};
val ab_group_add_real_vector = #ab_group_add_real_vector :
  'a real_vector -> 'a ab_group_add;
val scaleR_real_vector = #scaleR_real_vector : 'a real_vector -> 'a scaleR;

type 'a dist_norm =
  {minus_dist_norm : 'a minus, dist_dist_norm : 'a dist,
    norm_dist_norm : 'a norm};
val minus_dist_norm = #minus_dist_norm : 'a dist_norm -> 'a minus;
val dist_dist_norm = #dist_dist_norm : 'a dist_norm -> 'a dist;
val norm_dist_norm = #norm_dist_norm : 'a dist_norm -> 'a norm;

type 'a real_normed_vector =
  {dist_norm_real_normed_vector : 'a dist_norm,
    metric_space_real_normed_vector : 'a metric_space,
    real_vector_real_normed_vector : 'a real_vector,
    sgn_div_norm_real_normed_vector : 'a sgn_div_norm};
val dist_norm_real_normed_vector = #dist_norm_real_normed_vector :
  'a real_normed_vector -> 'a dist_norm;
val metric_space_real_normed_vector = #metric_space_real_normed_vector :
  'a real_normed_vector -> 'a metric_space;
val real_vector_real_normed_vector = #real_vector_real_normed_vector :
  'a real_normed_vector -> 'a real_vector;
val sgn_div_norm_real_normed_vector = #sgn_div_norm_real_normed_vector :
  'a real_normed_vector -> 'a sgn_div_norm;

type 'a real_inner =
  {real_normed_vector_real_inner : 'a real_normed_vector,
    inner : 'a -> 'a -> real};
val real_normed_vector_real_inner = #real_normed_vector_real_inner :
  'a real_inner -> 'a real_normed_vector;
val inner = #inner : 'a real_inner -> 'a -> 'a -> real;

val scaleR_real = {scaleR = scaleR_reala} : real scaleR;

val sgn_div_norm_real =
  {sgn_sgn_div_norm = sgn_real, norm_sgn_div_norm = norm_real,
    scaleR_sgn_div_norm = scaleR_real}
  : real sgn_div_norm;

val topological_space_real = {open_topological_space = open_real} :
  real topological_space;

val first_countable_topology_real =
  {topological_space_first_countable_topology = topological_space_real} :
  real first_countable_topology;

val open_dist_real = {dist_open_dist = dist_real, open_open_dist = open_real} :
  real open_dist;

val t0_space_real = {topological_space_t0_space = topological_space_real} :
  real t0_space;

val t1_space_real = {t0_space_t1_space = t0_space_real} : real t1_space;

val t2_space_real = {t1_space_t2_space = t1_space_real} : real t2_space;

val metric_space_real =
  {open_dist_metric_space = open_dist_real,
    first_countable_topology_metric_space = first_countable_topology_real,
    t2_space_metric_space = t2_space_real}
  : real metric_space;

val real_vector_real =
  {ab_group_add_real_vector = ab_group_add_real,
    scaleR_real_vector = scaleR_real}
  : real real_vector;

val dist_norm_real =
  {minus_dist_norm = minus_real, dist_dist_norm = dist_real,
    norm_dist_norm = norm_real}
  : real dist_norm;

val real_normed_vector_real =
  {dist_norm_real_normed_vector = dist_norm_real,
    metric_space_real_normed_vector = metric_space_real,
    real_vector_real_normed_vector = real_vector_real,
    sgn_div_norm_real_normed_vector = sgn_div_norm_real}
  : real real_normed_vector;

val real_inner_real =
  {real_normed_vector_real_inner = real_normed_vector_real, inner = inner_real}
  : real real_inner;

type 'a distrib_lattice = {lattice_distrib_lattice : 'a lattice};
val lattice_distrib_lattice = #lattice_distrib_lattice :
  'a distrib_lattice -> 'a lattice;

val distrib_lattice_real = {lattice_distrib_lattice = lattice_real} :
  real distrib_lattice;

type 'a complete_space = {metric_space_complete_space : 'a metric_space};
val metric_space_complete_space = #metric_space_complete_space :
  'a complete_space -> 'a metric_space;

type 'a banach =
  {complete_space_banach : 'a complete_space,
    real_normed_vector_banach : 'a real_normed_vector};
val complete_space_banach = #complete_space_banach :
  'a banach -> 'a complete_space;
val real_normed_vector_banach = #real_normed_vector_banach :
  'a banach -> 'a real_normed_vector;

val complete_space_real = {metric_space_complete_space = metric_space_real} :
  real complete_space;

val banach_real =
  {complete_space_banach = complete_space_real,
    real_normed_vector_banach = real_normed_vector_real}
  : real banach;

type 'a ordered_ab_semigroup_add =
  {ab_semigroup_add_ordered_ab_semigroup_add : 'a ab_semigroup_add,
    order_ordered_ab_semigroup_add : 'a order};
val ab_semigroup_add_ordered_ab_semigroup_add =
  #ab_semigroup_add_ordered_ab_semigroup_add :
  'a ordered_ab_semigroup_add -> 'a ab_semigroup_add;
val order_ordered_ab_semigroup_add = #order_ordered_ab_semigroup_add :
  'a ordered_ab_semigroup_add -> 'a order;

type 'a ordered_cancel_ab_semigroup_add =
  {cancel_ab_semigroup_add_ordered_cancel_ab_semigroup_add :
     'a cancel_ab_semigroup_add,
    ordered_ab_semigroup_add_ordered_cancel_ab_semigroup_add :
      'a ordered_ab_semigroup_add};
val cancel_ab_semigroup_add_ordered_cancel_ab_semigroup_add =
  #cancel_ab_semigroup_add_ordered_cancel_ab_semigroup_add :
  'a ordered_cancel_ab_semigroup_add -> 'a cancel_ab_semigroup_add;
val ordered_ab_semigroup_add_ordered_cancel_ab_semigroup_add =
  #ordered_ab_semigroup_add_ordered_cancel_ab_semigroup_add :
  'a ordered_cancel_ab_semigroup_add -> 'a ordered_ab_semigroup_add;

type 'a ordered_ab_semigroup_add_imp_le =
  {ordered_cancel_ab_semigroup_add_ordered_ab_semigroup_add_imp_le :
     'a ordered_cancel_ab_semigroup_add};
val ordered_cancel_ab_semigroup_add_ordered_ab_semigroup_add_imp_le =
  #ordered_cancel_ab_semigroup_add_ordered_ab_semigroup_add_imp_le :
  'a ordered_ab_semigroup_add_imp_le -> 'a ordered_cancel_ab_semigroup_add;

type 'a ordered_comm_monoid_add =
  {comm_monoid_add_ordered_comm_monoid_add : 'a comm_monoid_add,
    ordered_cancel_ab_semigroup_add_ordered_comm_monoid_add :
      'a ordered_cancel_ab_semigroup_add};
val comm_monoid_add_ordered_comm_monoid_add =
  #comm_monoid_add_ordered_comm_monoid_add :
  'a ordered_comm_monoid_add -> 'a comm_monoid_add;
val ordered_cancel_ab_semigroup_add_ordered_comm_monoid_add =
  #ordered_cancel_ab_semigroup_add_ordered_comm_monoid_add :
  'a ordered_comm_monoid_add -> 'a ordered_cancel_ab_semigroup_add;

type 'a ordered_ab_group_add =
  {ab_group_add_ordered_ab_group_add : 'a ab_group_add,
    ordered_ab_semigroup_add_imp_le_ordered_ab_group_add :
      'a ordered_ab_semigroup_add_imp_le,
    ordered_comm_monoid_add_ordered_ab_group_add : 'a ordered_comm_monoid_add};
val ab_group_add_ordered_ab_group_add = #ab_group_add_ordered_ab_group_add :
  'a ordered_ab_group_add -> 'a ab_group_add;
val ordered_ab_semigroup_add_imp_le_ordered_ab_group_add =
  #ordered_ab_semigroup_add_imp_le_ordered_ab_group_add :
  'a ordered_ab_group_add -> 'a ordered_ab_semigroup_add_imp_le;
val ordered_comm_monoid_add_ordered_ab_group_add =
  #ordered_comm_monoid_add_ordered_ab_group_add :
  'a ordered_ab_group_add -> 'a ordered_comm_monoid_add;

val ordered_ab_semigroup_add_real =
  {ab_semigroup_add_ordered_ab_semigroup_add = ab_semigroup_add_real,
    order_ordered_ab_semigroup_add = order_real}
  : real ordered_ab_semigroup_add;

val ordered_cancel_ab_semigroup_add_real =
  {cancel_ab_semigroup_add_ordered_cancel_ab_semigroup_add =
     cancel_ab_semigroup_add_real,
    ordered_ab_semigroup_add_ordered_cancel_ab_semigroup_add =
      ordered_ab_semigroup_add_real}
  : real ordered_cancel_ab_semigroup_add;

val ordered_ab_semigroup_add_imp_le_real =
  {ordered_cancel_ab_semigroup_add_ordered_ab_semigroup_add_imp_le =
     ordered_cancel_ab_semigroup_add_real}
  : real ordered_ab_semigroup_add_imp_le;

val ordered_comm_monoid_add_real =
  {comm_monoid_add_ordered_comm_monoid_add = comm_monoid_add_real,
    ordered_cancel_ab_semigroup_add_ordered_comm_monoid_add =
      ordered_cancel_ab_semigroup_add_real}
  : real ordered_comm_monoid_add;

val ordered_ab_group_add_real =
  {ab_group_add_ordered_ab_group_add = ab_group_add_real,
    ordered_ab_semigroup_add_imp_le_ordered_ab_group_add =
      ordered_ab_semigroup_add_imp_le_real,
    ordered_comm_monoid_add_ordered_ab_group_add = ordered_comm_monoid_add_real}
  : real ordered_ab_group_add;

val bot_set : 'a set = Set [];

fun removeAll A_ x [] = []
  | removeAll A_ x (y :: xs) =
    (if eq A_ x y then removeAll A_ x xs else y :: removeAll A_ x xs);

fun membera A_ [] y = false
  | membera A_ (x :: xs) y = eq A_ x y orelse membera A_ xs y;

fun inserta A_ x xs = (if membera A_ xs x then xs else x :: xs);

fun insert A_ x (Coset xs) = Coset (removeAll A_ x xs)
  | insert A_ x (Set xs) = Set (inserta A_ x xs);

val basis_real : real set =
  insert equal_real
    (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta))) bot_set;

type 'a second_countable_topology =
  {first_countable_topology_second_countable_topology :
     'a first_countable_topology};
val first_countable_topology_second_countable_topology =
  #first_countable_topology_second_countable_topology :
  'a second_countable_topology -> 'a first_countable_topology;

type 'a polish_space =
  {complete_space_polish_space : 'a complete_space,
    second_countable_topology_polish_space : 'a second_countable_topology};
val complete_space_polish_space = #complete_space_polish_space :
  'a polish_space -> 'a complete_space;
val second_countable_topology_polish_space =
  #second_countable_topology_polish_space :
  'a polish_space -> 'a second_countable_topology;

type 'a heine_borel = {complete_space_heine_borel : 'a complete_space};
val complete_space_heine_borel = #complete_space_heine_borel :
  'a heine_borel -> 'a complete_space;

type 'a perfect_space =
  {topological_space_perfect_space : 'a topological_space};
val topological_space_perfect_space = #topological_space_perfect_space :
  'a perfect_space -> 'a topological_space;

type 'a euclidean_space =
  {real_inner_euclidean_space : 'a real_inner,
    banach_euclidean_space : 'a banach,
    perfect_space_euclidean_space : 'a perfect_space,
    heine_borel_euclidean_space : 'a heine_borel,
    polish_space_euclidean_space : 'a polish_space, basis : 'a set};
val real_inner_euclidean_space = #real_inner_euclidean_space :
  'a euclidean_space -> 'a real_inner;
val banach_euclidean_space = #banach_euclidean_space :
  'a euclidean_space -> 'a banach;
val perfect_space_euclidean_space = #perfect_space_euclidean_space :
  'a euclidean_space -> 'a perfect_space;
val heine_borel_euclidean_space = #heine_borel_euclidean_space :
  'a euclidean_space -> 'a heine_borel;
val polish_space_euclidean_space = #polish_space_euclidean_space :
  'a euclidean_space -> 'a polish_space;
val basis = #basis : 'a euclidean_space -> 'a set;

val second_countable_topology_real =
  {first_countable_topology_second_countable_topology =
     first_countable_topology_real}
  : real second_countable_topology;

val polish_space_real =
  {complete_space_polish_space = complete_space_real,
    second_countable_topology_polish_space = second_countable_topology_real}
  : real polish_space;

val heine_borel_real = {complete_space_heine_borel = complete_space_real} :
  real heine_borel;

val perfect_space_real =
  {topological_space_perfect_space = topological_space_real} :
  real perfect_space;

val euclidean_space_real =
  {real_inner_euclidean_space = real_inner_real,
    banach_euclidean_space = banach_real,
    perfect_space_euclidean_space = perfect_space_real,
    heine_borel_euclidean_space = heine_borel_real,
    polish_space_euclidean_space = polish_space_real, basis = basis_real}
  : real euclidean_space;

type 'a ordered_ab_group_add_abs =
  {abs_ordered_ab_group_add_abs : 'a abs,
    ordered_ab_group_add_ordered_ab_group_add_abs : 'a ordered_ab_group_add};
val abs_ordered_ab_group_add_abs = #abs_ordered_ab_group_add_abs :
  'a ordered_ab_group_add_abs -> 'a abs;
val ordered_ab_group_add_ordered_ab_group_add_abs =
  #ordered_ab_group_add_ordered_ab_group_add_abs :
  'a ordered_ab_group_add_abs -> 'a ordered_ab_group_add;

val ordered_ab_group_add_abs_real =
  {abs_ordered_ab_group_add_abs = abs_real,
    ordered_ab_group_add_ordered_ab_group_add_abs = ordered_ab_group_add_real}
  : real ordered_ab_group_add_abs;

type 'a ordered_real_vector =
  {ordered_ab_group_add_ordered_real_vector : 'a ordered_ab_group_add,
    real_vector_ordered_real_vector : 'a real_vector};
val ordered_ab_group_add_ordered_real_vector =
  #ordered_ab_group_add_ordered_real_vector :
  'a ordered_real_vector -> 'a ordered_ab_group_add;
val real_vector_ordered_real_vector = #real_vector_ordered_real_vector :
  'a ordered_real_vector -> 'a real_vector;

val ordered_real_vector_real =
  {ordered_ab_group_add_ordered_real_vector = ordered_ab_group_add_real,
    real_vector_ordered_real_vector = real_vector_real}
  : real ordered_real_vector;

type 'a conditionally_complete_lattice =
  {inf_conditionally_complete_lattice : 'a infa,
    sup_conditionally_complete_lattice : 'a supa,
    lattice_conditionally_complete_lattice : 'a lattice};
val inf_conditionally_complete_lattice = #inf_conditionally_complete_lattice :
  'a conditionally_complete_lattice -> 'a infa;
val sup_conditionally_complete_lattice = #sup_conditionally_complete_lattice :
  'a conditionally_complete_lattice -> 'a supa;
val lattice_conditionally_complete_lattice =
  #lattice_conditionally_complete_lattice :
  'a conditionally_complete_lattice -> 'a lattice;

type 'a ordered_euclidean_space =
  {conditionally_complete_lattice_ordered_euclidean_space :
     'a conditionally_complete_lattice,
    euclidean_space_ordered_euclidean_space : 'a euclidean_space,
    ordered_ab_group_add_abs_ordered_euclidean_space :
      'a ordered_ab_group_add_abs,
    distrib_lattice_ordered_euclidean_space : 'a distrib_lattice,
    ordered_real_vector_ordered_euclidean_space : 'a ordered_real_vector};
val conditionally_complete_lattice_ordered_euclidean_space =
  #conditionally_complete_lattice_ordered_euclidean_space :
  'a ordered_euclidean_space -> 'a conditionally_complete_lattice;
val euclidean_space_ordered_euclidean_space =
  #euclidean_space_ordered_euclidean_space :
  'a ordered_euclidean_space -> 'a euclidean_space;
val ordered_ab_group_add_abs_ordered_euclidean_space =
  #ordered_ab_group_add_abs_ordered_euclidean_space :
  'a ordered_euclidean_space -> 'a ordered_ab_group_add_abs;
val distrib_lattice_ordered_euclidean_space =
  #distrib_lattice_ordered_euclidean_space :
  'a ordered_euclidean_space -> 'a distrib_lattice;
val ordered_real_vector_ordered_euclidean_space =
  #ordered_real_vector_ordered_euclidean_space :
  'a ordered_euclidean_space -> 'a ordered_real_vector;

val conditionally_complete_lattice_real =
  {inf_conditionally_complete_lattice = inf_reala,
    sup_conditionally_complete_lattice = sup_reala,
    lattice_conditionally_complete_lattice = lattice_real}
  : real conditionally_complete_lattice;

val ordered_euclidean_space_real =
  {conditionally_complete_lattice_ordered_euclidean_space =
     conditionally_complete_lattice_real,
    euclidean_space_ordered_euclidean_space = euclidean_space_real,
    ordered_ab_group_add_abs_ordered_euclidean_space =
      ordered_ab_group_add_abs_real,
    distrib_lattice_ordered_euclidean_space = distrib_lattice_real,
    ordered_real_vector_ordered_euclidean_space = ordered_real_vector_real}
  : real ordered_euclidean_space;

fun sgn_integer k =
  (if ((k : IntInf.int) = (0 : IntInf.int)) then (0 : IntInf.int)
    else (if IntInf.< (k, (0 : IntInf.int)) then (~1 : IntInf.int)
           else (1 : IntInf.int)));

fun abs_integer k = (if IntInf.< (k, (0 : IntInf.int)) then IntInf.~ k else k);

fun apsnd f (x, y) = (x, f y);

fun divmod_integer k l =
  (if ((k : IntInf.int) = (0 : IntInf.int))
    then ((0 : IntInf.int), (0 : IntInf.int))
    else (if ((l : IntInf.int) = (0 : IntInf.int)) then ((0 : IntInf.int), k)
           else (apsnd o (fn a => fn b => IntInf.* (a, b)) o sgn_integer) l
                  (if (((sgn_integer k) : IntInf.int) = (sgn_integer l))
                    then IntInf.divMod (IntInf.abs k, IntInf.abs l)
                    else let
                           val (r, s) =
                             IntInf.divMod (IntInf.abs k, IntInf.abs l);
                         in
                           (if ((s : IntInf.int) = (0 : IntInf.int))
                             then (IntInf.~ r, (0 : IntInf.int))
                             else (IntInf.- (IntInf.~ r, (1 : IntInf.int)),
                                    IntInf.- (abs_integer l, s)))
                         end)));

fun fst (x1, x2) = x1;

fun div_integer k l = fst (divmod_integer k l);

fun div_int k l =
  Int_of_integer (div_integer (integer_of_int k) (integer_of_int l));

fun int_of_nat n = Int_of_integer (integer_of_nat n);

fun log2 (Int_of_integer a) = Int_of_integer (IntInf.log2 a);

fun bitlen a =
  (if less_int zero_inta a
    then plus_inta (log2 a) (Int_of_integer (1 : IntInf.int)) else zero_inta);

fun float_round_down prec (Float (m, e)) =
  let
    val d = minus_inta (bitlen (abs_inta m)) (int_of_nat prec);
  in
    (if less_int zero_inta d
      then let
             val p = power_inta (Int_of_integer (2 : IntInf.int)) d;
             val n = div_int m p;
           in
             Float (n, plus_inta e d)
           end
      else Float (m, e))
  end;

fun truncate_down prec (Floatreal f) = Floatreal (float_round_down prec f);

fun eucl_truncate_down_real prec b = truncate_down prec b;

fun float_round_up prec x =
  uminus_floata (float_round_down prec (uminus_floata x));

fun truncate_up prec (Floatreal f) = Floatreal (float_round_up prec f);

fun eucl_truncate_up_real prec b = truncate_up prec b;

val basis_list_real : real list =
  [Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta))];

fun float_down p (Float (m, e)) =
  (if less_int (plus_inta p e) zero_inta
    then Float (div_int m
                  (power_inta (Int_of_integer (2 : IntInf.int))
                    (uminus_inta (plus_inta p e))),
                 uminus_inta p)
    else Float (m, e));

fun round_down prec (Floatreal f) = Floatreal (float_down prec f);

fun eucl_down_real prec b = round_down prec b;

type 'a executable_euclidean_space =
  {ordered_euclidean_space_executable_euclidean_space :
     'a ordered_euclidean_space,
    basis_list : 'a list, eucl_down : int -> 'a -> 'a,
    eucl_truncate_down : nat -> 'a -> 'a, eucl_truncate_up : nat -> 'a -> 'a};
val ordered_euclidean_space_executable_euclidean_space =
  #ordered_euclidean_space_executable_euclidean_space :
  'a executable_euclidean_space -> 'a ordered_euclidean_space;
val basis_list = #basis_list : 'a executable_euclidean_space -> 'a list;
val eucl_down = #eucl_down : 'a executable_euclidean_space -> int -> 'a -> 'a;
val eucl_truncate_down = #eucl_truncate_down :
  'a executable_euclidean_space -> nat -> 'a -> 'a;
val eucl_truncate_up = #eucl_truncate_up :
  'a executable_euclidean_space -> nat -> 'a -> 'a;

val executable_euclidean_space_real =
  {ordered_euclidean_space_executable_euclidean_space =
     ordered_euclidean_space_real,
    basis_list = basis_list_real, eucl_down = eucl_down_real,
    eucl_truncate_down = eucl_truncate_down_real,
    eucl_truncate_up = eucl_truncate_up_real}
  : real executable_euclidean_space;

val one_floata : float = Float (Int_of_integer (1 : IntInf.int), zero_inta);

val one_float = {one = one_floata} : float one;

val zero_floata : float = Float (zero_inta, zero_inta);

type 'a mult_zero = {times_mult_zero : 'a times, zero_mult_zero : 'a zero};
val times_mult_zero = #times_mult_zero : 'a mult_zero -> 'a times;
val zero_mult_zero = #zero_mult_zero : 'a mult_zero -> 'a zero;

type 'a semigroup_mult = {times_semigroup_mult : 'a times};
val times_semigroup_mult = #times_semigroup_mult :
  'a semigroup_mult -> 'a times;

type 'a semiring =
  {ab_semigroup_add_semiring : 'a ab_semigroup_add,
    semigroup_mult_semiring : 'a semigroup_mult};
val ab_semigroup_add_semiring = #ab_semigroup_add_semiring :
  'a semiring -> 'a ab_semigroup_add;
val semigroup_mult_semiring = #semigroup_mult_semiring :
  'a semiring -> 'a semigroup_mult;

type 'a semiring_0 =
  {comm_monoid_add_semiring_0 : 'a comm_monoid_add,
    mult_zero_semiring_0 : 'a mult_zero, semiring_semiring_0 : 'a semiring};
val comm_monoid_add_semiring_0 = #comm_monoid_add_semiring_0 :
  'a semiring_0 -> 'a comm_monoid_add;
val mult_zero_semiring_0 = #mult_zero_semiring_0 :
  'a semiring_0 -> 'a mult_zero;
val semiring_semiring_0 = #semiring_semiring_0 : 'a semiring_0 -> 'a semiring;

type 'a semiring_0_cancel =
  {cancel_comm_monoid_add_semiring_0_cancel : 'a cancel_comm_monoid_add,
    semiring_0_semiring_0_cancel : 'a semiring_0};
val cancel_comm_monoid_add_semiring_0_cancel =
  #cancel_comm_monoid_add_semiring_0_cancel :
  'a semiring_0_cancel -> 'a cancel_comm_monoid_add;
val semiring_0_semiring_0_cancel = #semiring_0_semiring_0_cancel :
  'a semiring_0_cancel -> 'a semiring_0;

type 'a ring =
  {ab_group_add_ring : 'a ab_group_add,
    semiring_0_cancel_ring : 'a semiring_0_cancel};
val ab_group_add_ring = #ab_group_add_ring : 'a ring -> 'a ab_group_add;
val semiring_0_cancel_ring = #semiring_0_cancel_ring :
  'a ring -> 'a semiring_0_cancel;

val plus_float = {plus = plus_floata} : float plus;

val semigroup_add_float = {plus_semigroup_add = plus_float} :
  float semigroup_add;

val cancel_semigroup_add_float =
  {semigroup_add_cancel_semigroup_add = semigroup_add_float} :
  float cancel_semigroup_add;

val ab_semigroup_add_float =
  {semigroup_add_ab_semigroup_add = semigroup_add_float} :
  float ab_semigroup_add;

val cancel_ab_semigroup_add_float =
  {ab_semigroup_add_cancel_ab_semigroup_add = ab_semigroup_add_float,
    cancel_semigroup_add_cancel_ab_semigroup_add = cancel_semigroup_add_float}
  : float cancel_ab_semigroup_add;

val zero_float = {zero = zero_floata} : float zero;

val monoid_add_float =
  {semigroup_add_monoid_add = semigroup_add_float, zero_monoid_add = zero_float}
  : float monoid_add;

val comm_monoid_add_float =
  {ab_semigroup_add_comm_monoid_add = ab_semigroup_add_float,
    monoid_add_comm_monoid_add = monoid_add_float}
  : float comm_monoid_add;

val cancel_comm_monoid_add_float =
  {cancel_ab_semigroup_add_cancel_comm_monoid_add =
     cancel_ab_semigroup_add_float,
    comm_monoid_add_cancel_comm_monoid_add = comm_monoid_add_float}
  : float cancel_comm_monoid_add;

val times_float = {times = times_floata} : float times;

val mult_zero_float =
  {times_mult_zero = times_float, zero_mult_zero = zero_float} :
  float mult_zero;

val semigroup_mult_float = {times_semigroup_mult = times_float} :
  float semigroup_mult;

val semiring_float =
  {ab_semigroup_add_semiring = ab_semigroup_add_float,
    semigroup_mult_semiring = semigroup_mult_float}
  : float semiring;

val semiring_0_float =
  {comm_monoid_add_semiring_0 = comm_monoid_add_float,
    mult_zero_semiring_0 = mult_zero_float,
    semiring_semiring_0 = semiring_float}
  : float semiring_0;

val semiring_0_cancel_float =
  {cancel_comm_monoid_add_semiring_0_cancel = cancel_comm_monoid_add_float,
    semiring_0_semiring_0_cancel = semiring_0_float}
  : float semiring_0_cancel;

val uminus_float = {uminus = uminus_floata} : float uminus;

val minus_float = {minus = minus_floata} : float minus;

val group_add_float =
  {cancel_semigroup_add_group_add = cancel_semigroup_add_float,
    minus_group_add = minus_float, monoid_add_group_add = monoid_add_float,
    uminus_group_add = uminus_float}
  : float group_add;

val ab_group_add_float =
  {cancel_comm_monoid_add_ab_group_add = cancel_comm_monoid_add_float,
    group_add_ab_group_add = group_add_float}
  : float ab_group_add;

val ring_float =
  {ab_group_add_ring = ab_group_add_float,
    semiring_0_cancel_ring = semiring_0_cancel_float}
  : float ring;

type 'a numeral =
  {one_numeral : 'a one, semigroup_add_numeral : 'a semigroup_add};
val one_numeral = #one_numeral : 'a numeral -> 'a one;
val semigroup_add_numeral = #semigroup_add_numeral :
  'a numeral -> 'a semigroup_add;

val numeral_float =
  {one_numeral = one_float, semigroup_add_numeral = semigroup_add_float} :
  float numeral;

val power_float = {one_power = one_float, times_power = times_float} :
  float power;

type 'a monoid_mult =
  {semigroup_mult_monoid_mult : 'a semigroup_mult,
    power_monoid_mult : 'a power};
val semigroup_mult_monoid_mult = #semigroup_mult_monoid_mult :
  'a monoid_mult -> 'a semigroup_mult;
val power_monoid_mult = #power_monoid_mult : 'a monoid_mult -> 'a power;

type 'a semiring_numeral =
  {monoid_mult_semiring_numeral : 'a monoid_mult,
    numeral_semiring_numeral : 'a numeral,
    semiring_semiring_numeral : 'a semiring};
val monoid_mult_semiring_numeral = #monoid_mult_semiring_numeral :
  'a semiring_numeral -> 'a monoid_mult;
val numeral_semiring_numeral = #numeral_semiring_numeral :
  'a semiring_numeral -> 'a numeral;
val semiring_semiring_numeral = #semiring_semiring_numeral :
  'a semiring_numeral -> 'a semiring;

type 'a semiring_1 =
  {semiring_numeral_semiring_1 : 'a semiring_numeral,
    semiring_0_semiring_1 : 'a semiring_0,
    zero_neq_one_semiring_1 : 'a zero_neq_one};
val semiring_numeral_semiring_1 = #semiring_numeral_semiring_1 :
  'a semiring_1 -> 'a semiring_numeral;
val semiring_0_semiring_1 = #semiring_0_semiring_1 :
  'a semiring_1 -> 'a semiring_0;
val zero_neq_one_semiring_1 = #zero_neq_one_semiring_1 :
  'a semiring_1 -> 'a zero_neq_one;

type 'a semiring_1_cancel =
  {semiring_0_cancel_semiring_1_cancel : 'a semiring_0_cancel,
    semiring_1_semiring_1_cancel : 'a semiring_1};
val semiring_0_cancel_semiring_1_cancel = #semiring_0_cancel_semiring_1_cancel :
  'a semiring_1_cancel -> 'a semiring_0_cancel;
val semiring_1_semiring_1_cancel = #semiring_1_semiring_1_cancel :
  'a semiring_1_cancel -> 'a semiring_1;

type 'a neg_numeral =
  {group_add_neg_numeral : 'a group_add, numeral_neg_numeral : 'a numeral};
val group_add_neg_numeral = #group_add_neg_numeral :
  'a neg_numeral -> 'a group_add;
val numeral_neg_numeral = #numeral_neg_numeral : 'a neg_numeral -> 'a numeral;

type 'a ring_1 =
  {neg_numeral_ring_1 : 'a neg_numeral, ring_ring_1 : 'a ring,
    semiring_1_cancel_ring_1 : 'a semiring_1_cancel};
val neg_numeral_ring_1 = #neg_numeral_ring_1 : 'a ring_1 -> 'a neg_numeral;
val ring_ring_1 = #ring_ring_1 : 'a ring_1 -> 'a ring;
val semiring_1_cancel_ring_1 = #semiring_1_cancel_ring_1 :
  'a ring_1 -> 'a semiring_1_cancel;

val monoid_mult_float =
  {semigroup_mult_monoid_mult = semigroup_mult_float,
    power_monoid_mult = power_float}
  : float monoid_mult;

val semiring_numeral_float =
  {monoid_mult_semiring_numeral = monoid_mult_float,
    numeral_semiring_numeral = numeral_float,
    semiring_semiring_numeral = semiring_float}
  : float semiring_numeral;

val zero_neq_one_float =
  {one_zero_neq_one = one_float, zero_zero_neq_one = zero_float} :
  float zero_neq_one;

val semiring_1_float =
  {semiring_numeral_semiring_1 = semiring_numeral_float,
    semiring_0_semiring_1 = semiring_0_float,
    zero_neq_one_semiring_1 = zero_neq_one_float}
  : float semiring_1;

val semiring_1_cancel_float =
  {semiring_0_cancel_semiring_1_cancel = semiring_0_cancel_float,
    semiring_1_semiring_1_cancel = semiring_1_float}
  : float semiring_1_cancel;

val neg_numeral_float =
  {group_add_neg_numeral = group_add_float, numeral_neg_numeral = numeral_float}
  : float neg_numeral;

val ring_1_float =
  {neg_numeral_ring_1 = neg_numeral_float, ring_ring_1 = ring_float,
    semiring_1_cancel_ring_1 = semiring_1_cancel_float}
  : float ring_1;

fun snd (x1, x2) = x2;

datatype ('b, 'a) slist = Abs_slist of ('b * 'a) list;

fun rep_slist B_ (Abs_slist x) = x;

fun filter p [] = []
  | filter p (x :: xs) = (if p x then x :: filter p xs else filter p xs);

fun list_of_slist A_ (B1_, B2_) xa =
  filter (fn x => not (eq B2_ (snd x) (zero B1_))) (rep_slist A_ xa);

datatype 'a pdevs = Pdevs of (nat, 'a) slist;

fun equal_proda A_ B_ (x1, x2) (y1, y2) = eq A_ x1 y1 andalso eq B_ x2 y2;

fun equal_prod A_ B_ = {equal = equal_proda A_ B_} : ('a * 'b) equal;

fun equal_pdevsa (A1_, A2_) (Pdevs a) (Pdevs b) =
  equal_lista (equal_prod equal_nat A2_)
    (list_of_slist linorder_nat (A1_, A2_) a)
    (list_of_slist linorder_nat (A1_, A2_) b);

fun equal_pdevs (A1_, A2_) = {equal = equal_pdevsa (A1_, A2_)} : 'a pdevs equal;

fun abs_proda A_ B_ x = (abs A_ (fst x), abs B_ (snd x));

fun abs_prod A_ B_ = {abs = abs_proda A_ B_} : ('a * 'b) abs;

fun scaleR_proda A_ B_ r a =
  (scaleR (scaleR_real_vector A_) r (fst a),
    scaleR (scaleR_real_vector B_) r (snd a));

fun norm_proda _ = raise Fail "Product_Vector.norm_prod_inst.norm_prod";

fun numeral A_ (Bit1 n) =
  let
    val m = numeral A_ n;
  in
    plus ((plus_semigroup_add o semigroup_add_numeral) A_)
      (plus ((plus_semigroup_add o semigroup_add_numeral) A_) m m)
      (one (one_numeral A_))
  end
  | numeral A_ (Bit0 n) =
    let
      val m = numeral A_ n;
    in
      plus ((plus_semigroup_add o semigroup_add_numeral) A_) m m
    end
  | numeral A_ One = one (one_numeral A_);

fun sgn_int i =
  (if equal_inta i zero_inta then zero_inta
    else (if less_int zero_inta i then Int_of_integer (1 : IntInf.int)
           else uminus_inta (Int_of_integer (1 : IntInf.int))));

fun map_prod f g (a, b) = (f a, g b);

fun divmod_abs k l =
  map_prod Int_of_integer Int_of_integer
    (IntInf.divMod (IntInf.abs (integer_of_int k),
      IntInf.abs (integer_of_int l)));

fun divmod_int k l =
  (if equal_inta k zero_inta then (zero_inta, zero_inta)
    else (if equal_inta l zero_inta then (zero_inta, k)
           else apsnd (times_inta (sgn_int l))
                  (if equal_inta (sgn_int k) (sgn_int l) then divmod_abs k l
                    else let
                           val (r, s) = divmod_abs k l;
                         in
                           (if equal_inta s zero_inta
                             then (uminus_inta r, zero_inta)
                             else (minus_inta (uminus_inta r)
                                     (Int_of_integer (1 : IntInf.int)),
                                    minus_inta (abs_inta l) s))
                         end)));

fun of_int A_ k =
  (if equal_inta k zero_inta
    then zero ((zero_mult_zero o mult_zero_semiring_0 o semiring_0_semiring_1 o
                 semiring_1_semiring_1_cancel o semiring_1_cancel_ring_1)
                A_)
    else (if less_int k zero_inta
           then uminus
                  ((uminus_group_add o group_add_neg_numeral o
                     neg_numeral_ring_1)
                    A_)
                  (of_int A_ (uminus_inta k))
           else let
                  val (l, j) = divmod_int k (Int_of_integer (2 : IntInf.int));
                  val la =
                    times ((times_power o power_monoid_mult o
                             monoid_mult_semiring_numeral o
                             semiring_numeral_semiring_1 o
                             semiring_1_semiring_1_cancel o
                             semiring_1_cancel_ring_1)
                            A_)
                      (numeral ((numeral_neg_numeral o neg_numeral_ring_1) A_)
                        (Bit0 One))
                      (of_int A_ l);
                in
                  (if equal_inta j zero_inta then la
                    else plus ((plus_semigroup_add o semigroup_add_numeral o
                                 numeral_neg_numeral o neg_numeral_ring_1)
                                A_)
                           la (one ((one_numeral o numeral_neg_numeral o
                                      neg_numeral_ring_1)
                                     A_)))
                end));

datatype nibble = Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 |
  Nibble6 | Nibble7 | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD
  | NibbleE | NibbleF;

datatype char = Char of nibble * nibble;

fun inverse_real (Floatreal (Float (a, b))) =
  (if equal_reala (Floatreal (Float (a, b)))
        (Floatreal (of_int ring_1_float (Int_of_integer (2 : IntInf.int))))
    then Floatreal
           (Float
             (Int_of_integer (1 : IntInf.int),
               uminus_inta (Int_of_integer (1 : IntInf.int))))
    else (if equal_inta a (Int_of_integer (1 : IntInf.int))
           then Floatreal
                  (Float (Int_of_integer (1 : IntInf.int), uminus_inta b))
           else (raise Fail "inverse not of 2")
                  (fn _ => inverse_real (Floatreal (Float (a, b))))));

fun sgn_proda A_ B_ x =
  scaleR_proda (real_vector_real_normed_vector A_)
    (real_vector_real_normed_vector B_) (inverse_real (norm_proda x)) x;

fun sgn_prod A_ B_ = {sgn = sgn_proda A_ B_} : ('a * 'b) sgn;

fun plus_proda A_ B_ x y = (plus A_ (fst x) (fst y), plus B_ (snd x) (snd y));

fun plus_prod A_ B_ = {plus = plus_proda A_ B_} : ('a * 'b) plus;

fun zero_proda A_ B_ = (zero A_, zero B_);

fun zero_prod A_ B_ = {zero = zero_proda A_ B_} : ('a * 'b) zero;

fun minus_proda A_ B_ x y =
  (minus A_ (fst x) (fst y), minus B_ (snd x) (snd y));

fun minus_prod A_ B_ = {minus = minus_proda A_ B_} : ('a * 'b) minus;

fun inf_prodc A_ B_ x y = (inf A_ (fst x) (fst y), inf B_ (snd x) (snd y));

fun inf_prod A_ B_ = {inf = inf_prodc A_ B_} : ('a * 'b) inf;

fun sup_prodc A_ B_ x y = (sup A_ (fst x) (fst y), sup B_ (snd x) (snd y));

fun sup_prod A_ B_ = {sup = sup_prodc A_ B_} : ('a * 'b) sup;

fun uminus_proda A_ B_ (a, b) = (uminus A_ a, uminus B_ b);

fun uminus_prod A_ B_ = {uminus = uminus_proda A_ B_} : ('a * 'b) uminus;

fun less_eq_prod A_ B_ x y =
  less_eq A_ (fst x) (fst y) andalso less_eq B_ (snd x) (snd y);

fun less_prod A_ B_ x y =
  less_eq_prod A_ B_ x y andalso not (less_eq_prod A_ B_ y x);

fun ord_prod A_ B_ = {less_eq = less_eq_prod A_ B_, less = less_prod A_ B_} :
  ('a * 'b) ord;

fun preorder_prod A_ B_ =
  {ord_preorder = ord_prod (ord_preorder A_) (ord_preorder B_)} :
  ('a * 'b) preorder;

fun order_prod A_ B_ =
  {preorder_order = preorder_prod (preorder_order A_) (preorder_order B_)} :
  ('a * 'b) order;

fun semigroup_add_prod A_ B_ =
  {plus_semigroup_add =
     plus_prod (plus_semigroup_add A_) (plus_semigroup_add B_)}
  : ('a * 'b) semigroup_add;

fun cancel_semigroup_add_prod A_ B_ =
  {semigroup_add_cancel_semigroup_add =
     semigroup_add_prod (semigroup_add_cancel_semigroup_add A_)
       (semigroup_add_cancel_semigroup_add B_)}
  : ('a * 'b) cancel_semigroup_add;

fun monoid_add_prod A_ B_ =
  {semigroup_add_monoid_add =
     semigroup_add_prod (semigroup_add_monoid_add A_)
       (semigroup_add_monoid_add B_),
    zero_monoid_add = zero_prod (zero_monoid_add A_) (zero_monoid_add B_)}
  : ('a * 'b) monoid_add;

fun group_add_prod A_ B_ =
  {cancel_semigroup_add_group_add =
     cancel_semigroup_add_prod (cancel_semigroup_add_group_add A_)
       (cancel_semigroup_add_group_add B_),
    minus_group_add = minus_prod (minus_group_add A_) (minus_group_add B_),
    monoid_add_group_add =
      monoid_add_prod (monoid_add_group_add A_) (monoid_add_group_add B_),
    uminus_group_add = uminus_prod (uminus_group_add A_) (uminus_group_add B_)}
  : ('a * 'b) group_add;

fun semilattice_sup_prod A_ B_ =
  {sup_semilattice_sup =
     sup_prod (sup_semilattice_sup A_) (sup_semilattice_sup B_),
    order_semilattice_sup =
      order_prod (order_semilattice_sup A_) (order_semilattice_sup B_)}
  : ('a * 'b) semilattice_sup;

fun semilattice_inf_prod A_ B_ =
  {inf_semilattice_inf =
     inf_prod (inf_semilattice_inf A_) (inf_semilattice_inf B_),
    order_semilattice_inf =
      order_prod (order_semilattice_inf A_) (order_semilattice_inf B_)}
  : ('a * 'b) semilattice_inf;

fun lattice_prod A_ B_ =
  {semilattice_inf_lattice =
     semilattice_inf_prod (semilattice_inf_lattice A_)
       (semilattice_inf_lattice B_),
    semilattice_sup_lattice =
      semilattice_sup_prod (semilattice_sup_lattice A_)
        (semilattice_sup_lattice B_)}
  : ('a * 'b) lattice;

fun ab_semigroup_add_prod A_ B_ =
  {semigroup_add_ab_semigroup_add =
     semigroup_add_prod (semigroup_add_ab_semigroup_add A_)
       (semigroup_add_ab_semigroup_add B_)}
  : ('a * 'b) ab_semigroup_add;

fun cancel_ab_semigroup_add_prod A_ B_ =
  {ab_semigroup_add_cancel_ab_semigroup_add =
     ab_semigroup_add_prod (ab_semigroup_add_cancel_ab_semigroup_add A_)
       (ab_semigroup_add_cancel_ab_semigroup_add B_),
    cancel_semigroup_add_cancel_ab_semigroup_add =
      cancel_semigroup_add_prod
        (cancel_semigroup_add_cancel_ab_semigroup_add A_)
        (cancel_semigroup_add_cancel_ab_semigroup_add B_)}
  : ('a * 'b) cancel_ab_semigroup_add;

fun comm_monoid_add_prod A_ B_ =
  {ab_semigroup_add_comm_monoid_add =
     ab_semigroup_add_prod (ab_semigroup_add_comm_monoid_add A_)
       (ab_semigroup_add_comm_monoid_add B_),
    monoid_add_comm_monoid_add =
      monoid_add_prod (monoid_add_comm_monoid_add A_)
        (monoid_add_comm_monoid_add B_)}
  : ('a * 'b) comm_monoid_add;

fun cancel_comm_monoid_add_prod A_ B_ =
  {cancel_ab_semigroup_add_cancel_comm_monoid_add =
     cancel_ab_semigroup_add_prod
       (cancel_ab_semigroup_add_cancel_comm_monoid_add A_)
       (cancel_ab_semigroup_add_cancel_comm_monoid_add B_),
    comm_monoid_add_cancel_comm_monoid_add =
      comm_monoid_add_prod (comm_monoid_add_cancel_comm_monoid_add A_)
        (comm_monoid_add_cancel_comm_monoid_add B_)}
  : ('a * 'b) cancel_comm_monoid_add;

fun ab_group_add_prod A_ B_ =
  {cancel_comm_monoid_add_ab_group_add =
     cancel_comm_monoid_add_prod (cancel_comm_monoid_add_ab_group_add A_)
       (cancel_comm_monoid_add_ab_group_add B_),
    group_add_ab_group_add =
      group_add_prod (group_add_ab_group_add A_) (group_add_ab_group_add B_)}
  : ('a * 'b) ab_group_add;

fun inf_prodb _ = raise Fail "Product_Order.Inf_prod_inst.Inf_prod";

fun inf_proda A_ B_ = {infa = inf_prodb} : ('a * 'b) infa;

fun sup_prodb _ = raise Fail "Product_Order.Sup_prod_inst.Sup_prod";

fun sup_proda A_ B_ = {supa = sup_prodb} : ('a * 'b) supa;

fun dist_proda _ _ = raise Fail "Product_Vector.dist_prod_inst.dist_prod";

fun dist_prod A_ B_ = {dist = dist_proda} : ('a * 'b) dist;

fun norm_prod A_ B_ = {norm = norm_proda} : ('a * 'b) norm;

fun open_proda _ = raise Fail "Product_Vector.open_prod_inst.open_prod";

fun open_prod A_ B_ = {opena = open_proda} : ('a * 'b) opena;

fun inner_prod A_ B_ x y =
  plus_reala (inner A_ (fst x) (fst y)) (inner B_ (snd x) (snd y));

fun scaleR_prod A_ B_ = {scaleR = scaleR_proda A_ B_} : ('a * 'b) scaleR;

fun sgn_div_norm_prod A_ B_ =
  {sgn_sgn_div_norm = sgn_prod A_ B_, norm_sgn_div_norm = norm_prod A_ B_,
    scaleR_sgn_div_norm =
      scaleR_prod (real_vector_real_normed_vector A_)
        (real_vector_real_normed_vector B_)}
  : ('a * 'b) sgn_div_norm;

fun topological_space_prod A_ B_ = {open_topological_space = open_prod A_ B_} :
  ('a * 'b) topological_space;

fun first_countable_topology_prod A_ B_ =
  {topological_space_first_countable_topology =
     topological_space_prod (topological_space_first_countable_topology A_)
       (topological_space_first_countable_topology B_)}
  : ('a * 'b) first_countable_topology;

fun open_dist_prod A_ B_ =
  {dist_open_dist = dist_prod A_ B_,
    open_open_dist =
      open_prod
        ((topological_space_t0_space o t0_space_t1_space o t1_space_t2_space o
           t2_space_metric_space)
          A_)
        ((topological_space_t0_space o t0_space_t1_space o t1_space_t2_space o
           t2_space_metric_space)
          B_)}
  : ('a * 'b) open_dist;

fun t0_space_prod A_ B_ =
  {topological_space_t0_space =
     topological_space_prod (topological_space_t0_space A_)
       (topological_space_t0_space B_)}
  : ('a * 'b) t0_space;

fun t1_space_prod A_ B_ =
  {t0_space_t1_space =
     t0_space_prod (t0_space_t1_space A_) (t0_space_t1_space B_)}
  : ('a * 'b) t1_space;

fun t2_space_prod A_ B_ =
  {t1_space_t2_space =
     t1_space_prod (t1_space_t2_space A_) (t1_space_t2_space B_)}
  : ('a * 'b) t2_space;

fun metric_space_prod A_ B_ =
  {open_dist_metric_space = open_dist_prod A_ B_,
    first_countable_topology_metric_space =
      first_countable_topology_prod (first_countable_topology_metric_space A_)
        (first_countable_topology_metric_space B_),
    t2_space_metric_space =
      t2_space_prod (t2_space_metric_space A_) (t2_space_metric_space B_)}
  : ('a * 'b) metric_space;

fun real_vector_prod A_ B_ =
  {ab_group_add_real_vector =
     ab_group_add_prod (ab_group_add_real_vector A_)
       (ab_group_add_real_vector B_),
    scaleR_real_vector = scaleR_prod A_ B_}
  : ('a * 'b) real_vector;

fun dist_norm_prod A_ B_ =
  {minus_dist_norm =
     minus_prod
       ((minus_group_add o group_add_ab_group_add o ab_group_add_real_vector o
          real_vector_real_normed_vector)
         A_)
       ((minus_group_add o group_add_ab_group_add o ab_group_add_real_vector o
          real_vector_real_normed_vector)
         B_),
    dist_dist_norm =
      dist_prod (metric_space_real_normed_vector A_)
        (metric_space_real_normed_vector B_),
    norm_dist_norm = norm_prod A_ B_}
  : ('a * 'b) dist_norm;

fun real_normed_vector_prod A_ B_ =
  {dist_norm_real_normed_vector = dist_norm_prod A_ B_,
    metric_space_real_normed_vector =
      metric_space_prod (metric_space_real_normed_vector A_)
        (metric_space_real_normed_vector B_),
    real_vector_real_normed_vector =
      real_vector_prod (real_vector_real_normed_vector A_)
        (real_vector_real_normed_vector B_),
    sgn_div_norm_real_normed_vector = sgn_div_norm_prod A_ B_}
  : ('a * 'b) real_normed_vector;

fun real_inner_prod A_ B_ =
  {real_normed_vector_real_inner =
     real_normed_vector_prod (real_normed_vector_real_inner A_)
       (real_normed_vector_real_inner B_),
    inner = inner_prod A_ B_}
  : ('a * 'b) real_inner;

fun distrib_lattice_prod A_ B_ =
  {lattice_distrib_lattice =
     lattice_prod (lattice_distrib_lattice A_) (lattice_distrib_lattice B_)}
  : ('a * 'b) distrib_lattice;

fun complete_space_prod A_ B_ =
  {metric_space_complete_space =
     metric_space_prod (metric_space_complete_space A_)
       (metric_space_complete_space B_)}
  : ('a * 'b) complete_space;

fun banach_prod A_ B_ =
  {complete_space_banach =
     complete_space_prod (complete_space_banach A_) (complete_space_banach B_),
    real_normed_vector_banach =
      real_normed_vector_prod (real_normed_vector_banach A_)
        (real_normed_vector_banach B_)}
  : ('a * 'b) banach;

fun ordered_ab_semigroup_add_prod A_ B_ =
  {ab_semigroup_add_ordered_ab_semigroup_add =
     ab_semigroup_add_prod
       ((ab_semigroup_add_comm_monoid_add o
          comm_monoid_add_cancel_comm_monoid_add o
          cancel_comm_monoid_add_ab_group_add o
          ab_group_add_ordered_ab_group_add o
          ordered_ab_group_add_ordered_ab_group_add_abs o
          ordered_ab_group_add_abs_ordered_euclidean_space)
         A_)
       ((ab_semigroup_add_comm_monoid_add o
          comm_monoid_add_cancel_comm_monoid_add o
          cancel_comm_monoid_add_ab_group_add o
          ab_group_add_ordered_ab_group_add o
          ordered_ab_group_add_ordered_ab_group_add_abs o
          ordered_ab_group_add_abs_ordered_euclidean_space)
         B_),
    order_ordered_ab_semigroup_add =
      order_prod
        ((order_semilattice_inf o semilattice_inf_lattice o
           lattice_distrib_lattice o distrib_lattice_ordered_euclidean_space)
          A_)
        ((order_semilattice_inf o semilattice_inf_lattice o
           lattice_distrib_lattice o distrib_lattice_ordered_euclidean_space)
          B_)}
  : ('a * 'b) ordered_ab_semigroup_add;

fun ordered_cancel_ab_semigroup_add_prod A_ B_ =
  {cancel_ab_semigroup_add_ordered_cancel_ab_semigroup_add =
     cancel_ab_semigroup_add_prod
       ((cancel_ab_semigroup_add_cancel_comm_monoid_add o
          cancel_comm_monoid_add_ab_group_add o
          ab_group_add_ordered_ab_group_add o
          ordered_ab_group_add_ordered_ab_group_add_abs o
          ordered_ab_group_add_abs_ordered_euclidean_space)
         A_)
       ((cancel_ab_semigroup_add_cancel_comm_monoid_add o
          cancel_comm_monoid_add_ab_group_add o
          ab_group_add_ordered_ab_group_add o
          ordered_ab_group_add_ordered_ab_group_add_abs o
          ordered_ab_group_add_abs_ordered_euclidean_space)
         B_),
    ordered_ab_semigroup_add_ordered_cancel_ab_semigroup_add =
      ordered_ab_semigroup_add_prod A_ B_}
  : ('a * 'b) ordered_cancel_ab_semigroup_add;

fun ordered_ab_semigroup_add_imp_le_prod A_ B_ =
  {ordered_cancel_ab_semigroup_add_ordered_ab_semigroup_add_imp_le =
     ordered_cancel_ab_semigroup_add_prod A_ B_}
  : ('a * 'b) ordered_ab_semigroup_add_imp_le;

fun ordered_comm_monoid_add_prod A_ B_ =
  {comm_monoid_add_ordered_comm_monoid_add =
     comm_monoid_add_prod
       ((comm_monoid_add_cancel_comm_monoid_add o
          cancel_comm_monoid_add_ab_group_add o
          ab_group_add_ordered_ab_group_add o
          ordered_ab_group_add_ordered_ab_group_add_abs o
          ordered_ab_group_add_abs_ordered_euclidean_space)
         A_)
       ((comm_monoid_add_cancel_comm_monoid_add o
          cancel_comm_monoid_add_ab_group_add o
          ab_group_add_ordered_ab_group_add o
          ordered_ab_group_add_ordered_ab_group_add_abs o
          ordered_ab_group_add_abs_ordered_euclidean_space)
         B_),
    ordered_cancel_ab_semigroup_add_ordered_comm_monoid_add =
      ordered_cancel_ab_semigroup_add_prod A_ B_}
  : ('a * 'b) ordered_comm_monoid_add;

fun ordered_ab_group_add_prod A_ B_ =
  {ab_group_add_ordered_ab_group_add =
     ab_group_add_prod
       ((ab_group_add_ordered_ab_group_add o
          ordered_ab_group_add_ordered_ab_group_add_abs o
          ordered_ab_group_add_abs_ordered_euclidean_space)
         A_)
       ((ab_group_add_ordered_ab_group_add o
          ordered_ab_group_add_ordered_ab_group_add_abs o
          ordered_ab_group_add_abs_ordered_euclidean_space)
         B_),
    ordered_ab_semigroup_add_imp_le_ordered_ab_group_add =
      ordered_ab_semigroup_add_imp_le_prod A_ B_,
    ordered_comm_monoid_add_ordered_ab_group_add =
      ordered_comm_monoid_add_prod A_ B_}
  : ('a * 'b) ordered_ab_group_add;

fun member A_ x (Coset xs) = not (membera A_ xs x)
  | member A_ x (Set xs) = membera A_ xs x;

fun fold f (x :: xs) s = fold f xs (f x s)
  | fold f [] s = s;

fun sup_set A_ (Coset xs) a = Coset (filter (fn x => not (member A_ x a)) xs)
  | sup_set A_ (Set xs) a = fold (insert A_) xs a;

fun map f [] = []
  | map f (x21 :: x22) = f x21 :: map f x22;

fun image f (Set xs) = Set (map f xs);

fun basis_prod (A1_, A2_) (B1_, B2_) =
  sup_set (equal_prod A2_ B2_)
    (image
      (fn u =>
        (u, zero ((zero_monoid_add o monoid_add_group_add o
                    group_add_ab_group_add o ab_group_add_real_vector o
                    real_vector_real_normed_vector o
                    real_normed_vector_real_inner o real_inner_euclidean_space)
                   B1_)))
      (basis A1_))
    (image
      (fn a =>
        (zero ((zero_monoid_add o monoid_add_group_add o
                 group_add_ab_group_add o ab_group_add_real_vector o
                 real_vector_real_normed_vector o
                 real_normed_vector_real_inner o real_inner_euclidean_space)
                A1_),
          a))
      (basis B1_));

fun second_countable_topology_prod A_ B_ =
  {first_countable_topology_second_countable_topology =
     first_countable_topology_prod
       (first_countable_topology_second_countable_topology A_)
       (first_countable_topology_second_countable_topology B_)}
  : ('a * 'b) second_countable_topology;

fun polish_space_prod A_ B_ =
  {complete_space_polish_space =
     complete_space_prod ((complete_space_banach o banach_euclidean_space) A_)
       ((complete_space_banach o banach_euclidean_space) B_),
    second_countable_topology_polish_space =
      second_countable_topology_prod
        ((second_countable_topology_polish_space o polish_space_euclidean_space)
          A_)
        ((second_countable_topology_polish_space o polish_space_euclidean_space)
          B_)}
  : ('a * 'b) polish_space;

fun heine_borel_prod A_ B_ =
  {complete_space_heine_borel =
     complete_space_prod (complete_space_heine_borel A_)
       (complete_space_heine_borel B_)}
  : ('a * 'b) heine_borel;

fun perfect_space_prod A_ B_ =
  {topological_space_perfect_space =
     topological_space_prod
       ((topological_space_t0_space o t0_space_t1_space o t1_space_t2_space o
          t2_space_metric_space o metric_space_complete_space o
          complete_space_banach o banach_euclidean_space)
         A_)
       ((topological_space_t0_space o t0_space_t1_space o t1_space_t2_space o
          t2_space_metric_space o metric_space_complete_space o
          complete_space_banach o banach_euclidean_space)
         B_)}
  : ('a * 'b) perfect_space;

fun euclidean_space_prod (A1_, A2_) (B1_, B2_) =
  {real_inner_euclidean_space =
     real_inner_prod (real_inner_euclidean_space A1_)
       (real_inner_euclidean_space B1_),
    banach_euclidean_space =
      banach_prod (banach_euclidean_space A1_) (banach_euclidean_space B1_),
    perfect_space_euclidean_space = perfect_space_prod A1_ B1_,
    heine_borel_euclidean_space =
      heine_borel_prod (heine_borel_euclidean_space A1_)
        (heine_borel_euclidean_space B1_),
    polish_space_euclidean_space = polish_space_prod A1_ B1_,
    basis = basis_prod (A1_, A2_) (B1_, B2_)}
  : ('a * 'b) euclidean_space;

fun ordered_ab_group_add_abs_prod A_ B_ =
  {abs_ordered_ab_group_add_abs =
     abs_prod
       ((abs_ordered_ab_group_add_abs o
          ordered_ab_group_add_abs_ordered_euclidean_space)
         A_)
       ((abs_ordered_ab_group_add_abs o
          ordered_ab_group_add_abs_ordered_euclidean_space)
         B_),
    ordered_ab_group_add_ordered_ab_group_add_abs =
      ordered_ab_group_add_prod A_ B_}
  : ('a * 'b) ordered_ab_group_add_abs;

fun ordered_real_vector_prod A_ B_ =
  {ordered_ab_group_add_ordered_real_vector = ordered_ab_group_add_prod A_ B_,
    real_vector_ordered_real_vector =
      real_vector_prod
        ((real_vector_real_normed_vector o real_normed_vector_real_inner o
           real_inner_euclidean_space o euclidean_space_ordered_euclidean_space)
          A_)
        ((real_vector_real_normed_vector o real_normed_vector_real_inner o
           real_inner_euclidean_space o euclidean_space_ordered_euclidean_space)
          B_)}
  : ('a * 'b) ordered_real_vector;

fun conditionally_complete_lattice_prod A_ B_ =
  {inf_conditionally_complete_lattice =
     inf_proda (inf_conditionally_complete_lattice A_)
       (inf_conditionally_complete_lattice B_),
    sup_conditionally_complete_lattice =
      sup_proda (sup_conditionally_complete_lattice A_)
        (sup_conditionally_complete_lattice B_),
    lattice_conditionally_complete_lattice =
      lattice_prod (lattice_conditionally_complete_lattice A_)
        (lattice_conditionally_complete_lattice B_)}
  : ('a * 'b) conditionally_complete_lattice;

fun ordered_euclidean_space_prod (A1_, A2_) (B1_, B2_) =
  {conditionally_complete_lattice_ordered_euclidean_space =
     conditionally_complete_lattice_prod
       (conditionally_complete_lattice_ordered_euclidean_space A2_)
       (conditionally_complete_lattice_ordered_euclidean_space B2_),
    euclidean_space_ordered_euclidean_space =
      euclidean_space_prod (euclidean_space_ordered_euclidean_space A2_, A1_)
        (euclidean_space_ordered_euclidean_space B2_, B1_),
    ordered_ab_group_add_abs_ordered_euclidean_space =
      ordered_ab_group_add_abs_prod A2_ B2_,
    distrib_lattice_ordered_euclidean_space =
      distrib_lattice_prod (distrib_lattice_ordered_euclidean_space A2_)
        (distrib_lattice_ordered_euclidean_space B2_),
    ordered_real_vector_ordered_euclidean_space =
      ordered_real_vector_prod A2_ B2_}
  : ('a * 'b) ordered_euclidean_space;

fun eucl_truncate_down_prod A_ B_ p a =
  (eucl_truncate_down A_ p (fst a), eucl_truncate_down B_ p (snd a));

fun eucl_truncate_up_prod A_ B_ p a =
  (eucl_truncate_up A_ p (fst a), eucl_truncate_up B_ p (snd a));

val zero_nat : nat = Nat (0 : IntInf.int);

fun plus_nat m n = Nat (IntInf.+ (integer_of_nat m, integer_of_nat n));

val one_nat : nat = Nat (1 : IntInf.int);

fun suc n = plus_nat n one_nat;

fun gen_length n (x :: xs) = gen_length (suc n) xs
  | gen_length n [] = n;

fun size_list x = gen_length zero_nat x;

val ord_integer =
  {less_eq = (fn a => fn b => IntInf.<= (a, b)),
    less = (fn a => fn b => IntInf.< (a, b))}
  : IntInf.int ord;

fun minus_nat m n =
  Nat (max ord_integer (0 : IntInf.int)
        (IntInf.- (integer_of_nat m, integer_of_nat n)));

fun replicate n x =
  (if equal_nata n zero_nat then []
    else x :: replicate (minus_nat n one_nat) x);

fun zip (x :: xs) (y :: ys) = (x, y) :: zip xs ys
  | zip xs [] = []
  | zip [] ys = [];

fun basis_list_prod A_ B_ =
  zip (basis_list A_)
    (replicate (size_list (basis_list A_))
      (zero ((zero_monoid_add o monoid_add_group_add o group_add_ab_group_add o
               ab_group_add_ordered_ab_group_add o
               ordered_ab_group_add_ordered_ab_group_add_abs o
               ordered_ab_group_add_abs_ordered_euclidean_space o
               ordered_euclidean_space_executable_euclidean_space)
              B_))) @
    zip (replicate (size_list (basis_list B_))
          (zero ((zero_monoid_add o monoid_add_group_add o
                   group_add_ab_group_add o ab_group_add_ordered_ab_group_add o
                   ordered_ab_group_add_ordered_ab_group_add_abs o
                   ordered_ab_group_add_abs_ordered_euclidean_space o
                   ordered_euclidean_space_executable_euclidean_space)
                  A_)))
      (basis_list B_);

fun eucl_down_prod A_ B_ p a = (eucl_down A_ p (fst a), eucl_down B_ p (snd a));

fun executable_euclidean_space_prod (A1_, A2_) (B1_, B2_) =
  {ordered_euclidean_space_executable_euclidean_space =
     ordered_euclidean_space_prod
       (A2_, ordered_euclidean_space_executable_euclidean_space A1_)
       (B2_, ordered_euclidean_space_executable_euclidean_space B1_),
    basis_list = basis_list_prod A1_ B1_, eucl_down = eucl_down_prod A1_ B1_,
    eucl_truncate_down = eucl_truncate_down_prod A1_ B1_,
    eucl_truncate_up = eucl_truncate_up_prod A1_ B1_}
  : ('a * 'b) executable_euclidean_space;

datatype 'a sctn = Sctn of 'a * real;

fun equal_sctna A_ (Sctn (x1, x2)) (Sctn (y1, y2)) =
  eq A_ x1 y1 andalso equal_reala x2 y2;

fun equal_sctn A_ = {equal = equal_sctna A_} : 'a sctn equal;

datatype 'a dres = DSUCCEEDi | DFAILi | DRETURN of 'a;

datatype 'a realarith = Add of 'a realarith * 'a realarith |
  Minus of 'a realarith | Mult of 'a realarith * 'a realarith |
  Inverse of 'a realarith | Var of nat * 'a | Num of real;

datatype ('a, 'b) euclarith = AddE of ('a, 'b) euclarith * ('a, 'b) euclarith |
  ScaleR of 'a realarith * 'b;

datatype ('a, 'b, 'c, 'd) options_ext =
  Options_ext of
    nat * real * real * nat * nat * nat * real * real * real * real * 'a sctn *
      'a sctn list * 'a sctn list * ('b -> bool) * real * real * real * real *
      ('b -> unit) * nat *
      (nat * (real * ('b * (real * ('b * (real * 'b))) list)) -> 'c) * real *
      real * nat * 'd;

fun id x = (fn xa => xa) x;

fun nat k = Nat (max ord_integer (0 : IntInf.int) (integer_of_int k));

fun nth (x :: xs) n =
  (if equal_nata n zero_nat then x else nth xs (minus_nat n one_nat));

fun rev xs = fold (fn a => fn b => a :: b) xs [];

fun upt i j = (if less_nat i j then i :: upt (suc i) j else []);

fun drop n [] = []
  | drop n (x :: xs) =
    (if equal_nata n zero_nat then x :: xs else drop (minus_nat n one_nat) xs);

fun find uu [] = NONE
  | find p (x :: xs) = (if p x then SOME x else find p xs);

fun maps f [] = []
  | maps f (x :: xs) = f x @ maps f xs;

fun null [] = true
  | null (x :: xs) = false;

fun take n [] = []
  | take n (x :: xs) =
    (if equal_nata n zero_nat then [] else x :: take (minus_nat n one_nat) xs);

fun upto_aux i j js =
  (if less_int j i then js
    else upto_aux i (minus_inta j (Int_of_integer (1 : IntInf.int))) (j :: js));

fun upto i j = upto_aux i j [];

fun foldr f [] = id
  | foldr f (x :: xs) = f x o foldr f xs;

fun map_option f NONE = NONE
  | map_option f (SOME x2) = SOME (f x2);

fun those [] = SOME []
  | those (x :: xs) =
    (case x of NONE => NONE | SOME y => map_option (fn a => y :: a) (those xs));

fun map_of A_ ((l, v) :: ps) k = (if eq A_ l k then SOME v else map_of A_ ps k)
  | map_of A_ [] k = NONE;

fun bind NONE f = NONE
  | bind (SOME x) f = f x;

fun foldli [] c f sigma = sigma
  | foldli (x :: xs) c f sigma =
    (if c sigma then foldli xs c f (f x sigma) else sigma);

fun hd (x21 :: x22) = x21;

fun tl [] = []
  | tl (x21 :: x22) = x22;

fun list_ex p [] = false
  | list_ex p (x :: xs) = p x orelse list_ex p xs;

fun remdups A_ [] = []
  | remdups A_ (x :: xs) =
    (if membera A_ xs x then remdups A_ xs else x :: remdups A_ xs);

fun remove1 A_ x [] = []
  | remove1 A_ x (y :: xs) = (if eq A_ x y then xs else y :: remove1 A_ x xs);

fun println x = let
                  val _ = TextIO.print x;
                in
                  TextIO.print "\n"
                end;

fun dropWhile p [] = []
  | dropWhile p (x :: xs) = (if p x then dropWhile p xs else x :: xs);

fun partition p [] = ([], [])
  | partition p (x :: xs) =
    let
      val (yes, no) = partition p xs;
    in
      (if p x then (x :: yes, no) else (yes, x :: no))
    end;

fun pred_list p [] = true
  | pred_list p (x :: xs) = p x andalso pred_list p xs;

fun is_none (SOME x) = false
  | is_none NONE = true;

fun bind_err err (SOME x) f = f x
  | bind_err err NONE f = let
                            val _ = println err;
                          in
                            NONE
                          end;

fun mod_integer k l = snd (divmod_integer k l);

fun mod_int k l =
  Int_of_integer (mod_integer (integer_of_int k) (integer_of_int l));

fun normfloat (Float (m, e)) =
  (if equal_inta (mod_int m (Int_of_integer (2 : IntInf.int))) zero_inta andalso
        not (equal_inta m zero_inta)
    then normfloat
           (Float
             (div_int m (Int_of_integer (2 : IntInf.int)),
               plus_inta e (Int_of_integer (1 : IntInf.int))))
    else (if equal_inta m zero_inta then Float (zero_inta, zero_inta)
           else Float (m, e)));

fun rat_precision prec x y =
  minus_inta (int_of_nat prec) (minus_inta (bitlen x) (bitlen y));

fun rapprox_posrat prec x y =
  let
    val l = rat_precision prec (int_of_nat x) (int_of_nat y);
    val xa =
      (if less_eq_int zero_inta l
        then (times_inta (int_of_nat x)
                (power_inta (Int_of_integer (2 : IntInf.int)) l),
               int_of_nat y)
        else (int_of_nat x,
               times_inta (int_of_nat y)
                 (power_inta (Int_of_integer (2 : IntInf.int))
                   (uminus_inta l))));
    val (d, m) = divmod_int (fst xa) (snd xa);
  in
    normfloat
      (Float
        (plus_inta d
           (if equal_inta m zero_inta orelse equal_nata y zero_nat
             then zero_inta else Int_of_integer (1 : IntInf.int)),
          uminus_inta l))
  end;

fun lapprox_posrat prec x y =
  let
    val l = rat_precision prec (int_of_nat x) (int_of_nat y);
    val d =
      (if less_eq_int zero_inta l
        then div_int
               (times_inta (int_of_nat x)
                 (power_inta (Int_of_integer (2 : IntInf.int)) l))
               (int_of_nat y)
        else div_int
               (div_int (int_of_nat x)
                 (power_inta (Int_of_integer (2 : IntInf.int)) (uminus_inta l)))
               (int_of_nat y));
  in
    normfloat (Float (d, uminus_inta l))
  end;

fun lapprox_rat prec x y =
  (if equal_inta y zero_inta then Float (zero_inta, zero_inta)
    else (if less_eq_int zero_inta x
           then (if less_int zero_inta y
                  then lapprox_posrat prec (nat x) (nat y)
                  else uminus_floata
                         (rapprox_posrat prec (nat x) (nat (uminus_inta y))))
           else (if less_int zero_inta y
                  then uminus_floata
                         (rapprox_posrat prec (nat (uminus_inta x)) (nat y))
                  else lapprox_posrat prec (nat (uminus_inta x))
                         (nat (uminus_inta y)))));

fun float_divl prec (Float (m1, s1)) (Float (m2, s2)) =
  times_floata (lapprox_rat prec m1 m2)
    (Float (Int_of_integer (1 : IntInf.int), minus_inta s1 s2));

fun real_divl p (Floatreal x) (Floatreal y) = Floatreal (float_divl p x y);

fun float_divr prec x y = uminus_floata (float_divl prec (uminus_floata x) y);

fun real_divr p (Floatreal x) (Floatreal y) = Floatreal (float_divr p x y);

fun map_filter f [] = []
  | map_filter f (x :: xs) =
    (case f x of NONE => map_filter f xs | SOME y => y :: map_filter f xs);

fun listsuma A_ xs =
  foldr (plus ((plus_semigroup_add o semigroup_add_monoid_add) A_)) xs
    (zero (zero_monoid_add A_));

fun tdev_slist A_ xa =
  listsuma
    ((monoid_add_group_add o group_add_ab_group_add o
       ab_group_add_ordered_ab_group_add o
       ordered_ab_group_add_ordered_ab_group_add_abs o
       ordered_ab_group_add_abs_ordered_euclidean_space)
      A_)
    (map (abs ((abs_ordered_ab_group_add_abs o
                 ordered_ab_group_add_abs_ordered_euclidean_space)
                A_) o
           snd)
      (rep_slist linorder_nat xa));

fun tdev A_ (Pdevs xs) = tdev_slist A_ xs;

fun det3 (xp, yp) (xq, yq) (xr, yr) =
  minus_reala
    (minus_reala
      (minus_reala
        (plus_reala (plus_reala (times_reala xp yq) (times_reala yp xr))
          (times_reala xq yr))
        (times_reala yq xr))
      (times_reala yp xq))
    (times_reala xp yr);

fun independent_pdevs [] = []
  | independent_pdevs (x :: xs) =
    let
      val (cs, is) =
        partition
          (fn c =>
            equal_reala (det3 (zero_proda zero_real zero_real) x c)
              (Floatreal (Float (zero_inta, zero_inta))))
          xs;
      val s =
        plus_proda plus_real plus_real x
          (listsuma (monoid_add_prod monoid_add_real monoid_add_real) cs);
    in
      (if equal_proda equal_real equal_real s (zero_proda zero_real zero_real)
        then [] else [s]) @
        independent_pdevs is
    end;

fun list_of_pdevs (A1_, A2_) (Pdevs xs) =
  list_of_slist linorder_nat (A1_, A2_) xs;

fun lex p q =
  less_real (fst p) (fst q) orelse
    (equal_reala (fst p) (fst q) andalso less_real (snd p) (snd q) orelse
      equal_proda equal_real equal_real p q);

fun nlex_slist xa =
  Abs_slist
    (map (fn (i, x) =>
           (i, (if lex (zero_proda zero_real zero_real) x
                 then uminus_proda uminus_real uminus_real x else x)))
      (rep_slist linorder_nat xa));

fun nlex_pdevs (Pdevs x) = Pdevs (nlex_slist x);

fun inl p =
  independent_pdevs
    (map snd
      (list_of_pdevs
        (zero_prod zero_real zero_real, equal_prod equal_real equal_real)
        (nlex_pdevs p)));

fun pairself f (x, y) = (f x, f y);

fun f2f10_frac (A1_, A2_, A3_, A4_) (B1_, B2_) c p r digits cnt e =
  (if equal_inta r zero_inta then (digits, (cnt, zero_inta))
    else (if eq A4_ p (zero A3_) then (digits, (cnt, r))
           else let
                  val (d, ra) =
                    divmod_int (times_inta r (Int_of_integer (10 : IntInf.int)))
                      (power_inta (Int_of_integer (2 : IntInf.int))
                        (uminus_inta e));
                in
                  f2f10_frac (A1_, A2_, A3_, A4_) (B1_, B2_)
                    (c orelse not (equal_inta d zero_inta))
                    (if not (equal_inta d zero_inta) orelse c
                      then minus A1_ p (one A2_) else p)
                    ra (plus_inta
                         (times_inta digits (Int_of_integer (10 : IntInf.int)))
                         d)
                    (plus B2_ cnt (one B1_))
                end
                  e));

fun float2_float10 prec rd m e =
  let
    val (ma, ea) =
      (if less_int e zero_inta then (m, e)
        else (times_inta m (power_inta (Int_of_integer (2 : IntInf.int)) e),
               zero_inta));
    val sgn = sgn_int ma;
    val mb = abs_inta ma;
    val round_down =
      equal_inta sgn (Int_of_integer (1 : IntInf.int)) andalso rd orelse
        equal_inta sgn (uminus_inta (Int_of_integer (1 : IntInf.int))) andalso
          not rd;
    val (x, r) =
      divmod_int mb
        (power_inta (Int_of_integer (2 : IntInf.int)) (uminus_inta ea));
    val p =
      plus_inta
        (div_int
          (times_inta
            (if equal_inta x zero_inta then prec
              else minus_inta prec
                     (plus_inta (log2 x) (Int_of_integer (1 : IntInf.int))))
            (Int_of_integer (3 : IntInf.int)))
          (Int_of_integer (10 : IntInf.int)))
        (Int_of_integer (1 : IntInf.int));
    val (digits, (e10, ra)) =
      (if less_int zero_inta p
        then f2f10_frac (minus_int, one_int, zero_int, equal_int)
               (one_int, plus_int) (not (equal_inta x zero_inta)) p r zero_inta
               zero_inta ea
        else (zero_inta, (zero_inta, zero_inta)));
    val digitsa =
      (if round_down orelse equal_inta ra zero_inta then digits
        else plus_inta digits (Int_of_integer (1 : IntInf.int)));
  in
    (times_inta sgn
       (plus_inta digitsa
         (times_inta x (power_inta (Int_of_integer (10 : IntInf.int)) e10))),
      uminus_inta e10)
  end;

fun int_to_string x = IntInf.toString (integer_of_int x);

fun print_real (Floatreal (Float (a, b))) =
  let
    val (m, e) = float2_float10 (Int_of_integer (25 : IntInf.int)) true a b;
    val _ = TextIO.print (int_to_string m);
    val _ = TextIO.print "e";
    val _ = TextIO.print (int_to_string e);
  in
    ()
  end;

fun print_eucl A_ x =
  let
    val _ = TextIO.print "(";
    val _ =
      map (fn i =>
            let
              val _ =
                print_real
                  (inner
                    ((real_inner_euclidean_space o
                       euclidean_space_ordered_euclidean_space o
                       ordered_euclidean_space_executable_euclidean_space)
                      A_)
                    x i);
              val _ = TextIO.print ", ";
            in
              ()
            end)
        (basis_list A_);
    val _ = TextIO.print ")";
  in
    ()
  end;

fun dbind DFAILi f = DFAILi
  | dbind DSUCCEEDi f = DSUCCEEDi
  | dbind (DRETURN x) f = f x;

fun binop (C1_, C2_) f z [] [] = []
  | binop (C1_, C2_) f z ((i, x) :: xs) [] =
    (i, f x z) :: binop (C1_, C2_) f z xs []
  | binop (C1_, C2_) f z [] ((i, y) :: ys) =
    (i, f z y) :: binop (C1_, C2_) f z [] ys
  | binop (C1_, C2_) f z ((i, x) :: xs) ((j, y) :: ys) =
    (if eq C1_ i j then (i, f x y) :: binop (C1_, C2_) f z xs ys
      else (if less C2_ j i
             then (i, f x z) :: binop (C1_, C2_) f z xs ((j, y) :: ys)
             else (j, f z y) :: binop (C1_, C2_) f z ((i, x) :: xs) ys));

fun the (SOME x2) = x2;

fun power one times a n =
  (if equal_nata n zero_nat then one
    else times a (power one times a (minus_nat n one_nat)));

fun dWHILE b f s = (if b s then dbind (f s) (dWHILE b f) else DRETURN s);

fun degree_list (A1_, A2_) [] = zero_nat
  | degree_list (A1_, A2_) (x :: xs) =
    (if eq A2_ (snd x) (zero A1_) then degree_list (A1_, A2_) xs
      else suc (fst x));

fun degree_slist (A1_, A2_) xa =
  degree_list (A1_, A2_) (rep_slist linorder_nat xa);

fun degree (A1_, A2_) (Pdevs xs) =
  degree_slist
    ((zero_monoid_add o monoid_add_group_add o group_add_ab_group_add o
       ab_group_add_real_vector)
       A2_,
      A1_)
    xs;

fun inner2 A_ x n l =
  (inner (real_inner_euclidean_space A_) x n,
    inner (real_inner_euclidean_space A_) x l);

fun int_floor_fl (Float (m, e)) =
  (if less_eq_int zero_inta e
    then times_inta m (power_inta (Int_of_integer (2 : IntInf.int)) e)
    else div_int m
           (power_inta (Int_of_integer (2 : IntInf.int)) (uminus_inta e)));

fun product_lists [] = [[]]
  | product_lists (xs :: xss) =
    maps (fn x => map (fn a => x :: a) (product_lists xss)) xs;

fun apfst f (x, y) = (f x, y);

fun update_list n x [] = [(n, x)]
  | update_list n x (y :: ys) =
    (if less_nat (fst y) n then (n, x) :: y :: ys
      else (if equal_nata n (fst y) then (n, x) :: ys
             else y :: update_list n x ys));

fun update_slist xc xd xe =
  Abs_slist (update_list xc xd (rep_slist linorder_nat xe));

fun pdev_upd A_ (Pdevs xs) n x = Pdevs (update_slist n x xs);

fun polychain_of A_ xc [] = []
  | polychain_of A_ xc (xm :: xs) =
    (xc, plus ((plus_semigroup_add o semigroup_add_monoid_add o
                 monoid_add_group_add o group_add_ab_group_add)
                A_)
           xc xm) ::
      polychain_of A_
        (plus ((plus_semigroup_add o semigroup_add_monoid_add o
                 monoid_add_group_add o group_add_ab_group_add)
                A_)
          xc xm)
        xs;

fun one_slist A_ =
  Abs_slist
    (rev (zip (upt zero_nat (size_list (basis_list A_))) (basis_list A_)));

fun add_slist (A1_, A2_) xb xc =
  Abs_slist
    (binop (equal_nat, ord_nat) (plus A1_) (zero A2_)
      (rep_slist linorder_nat xb) (rep_slist linorder_nat xc));

fun map_slist xb xc = Abs_slist (map (apsnd xb) (rep_slist linorder_nat xc));

fun inf_aform A_ x =
  minus ((minus_group_add o group_add_ab_group_add o
           ab_group_add_ordered_ab_group_add o
           ordered_ab_group_add_ordered_ab_group_add_abs o
           ordered_ab_group_add_abs_ordered_euclidean_space)
          A_)
    (fst x) (tdev A_ (snd x));

fun sup_aform A_ x =
  plus ((plus_semigroup_add o semigroup_add_monoid_add o monoid_add_group_add o
          group_add_ab_group_add o ab_group_add_ordered_ab_group_add o
          ordered_ab_group_add_ordered_ab_group_add_abs o
          ordered_ab_group_add_abs_ordered_euclidean_space)
         A_)
    (fst x) (tdev A_ (snd x));

fun add_pdevs A_ (Pdevs xs) (Pdevs ys) =
  Pdevs (add_slist
          ((plus_semigroup_add o semigroup_add_monoid_add o
             monoid_add_group_add o group_add_ab_group_add o
             ab_group_add_real_vector)
             A_,
            (zero_monoid_add o monoid_add_group_add o group_add_ab_group_add o
              ab_group_add_real_vector)
              A_)
          xs ys);

val zero_slist : (nat, 'a) slist = Abs_slist [];

fun zero_pdevs A_ = Pdevs zero_slist;

fun num_aform B_ f = (f, zero_pdevs B_);

fun fold_slist (A1_, A2_) x xc =
  fold (x o snd)
    (filter (fn xa => not (eq A2_ (snd xa) (zero A1_)))
      (rep_slist linorder_nat xc));

fun msum_slist xc xd xe =
  Abs_slist
    (map (apfst (fn n => plus_nat n xc)) (rep_slist linorder_nat xe) @
      dropWhile (fn (i, _) => less_eq_nat xc i) (rep_slist linorder_nat xd));

fun msum_pdevs A_ m (Pdevs xs) (Pdevs ys) = Pdevs (msum_slist m xs ys);

fun msum_aform A_ n f g =
  (plus ((plus_semigroup_add o semigroup_add_monoid_add o monoid_add_group_add o
           group_add_ab_group_add o ab_group_add_real_vector)
          A_)
     (fst f) (fst g),
    msum_pdevs A_ n (snd f) (snd g));

fun infnorm A_ x =
  fold (max ord_real o
         (fn i =>
           abs_reala
             (inner
               ((real_inner_euclidean_space o
                  euclidean_space_ordered_euclidean_space o
                  ordered_euclidean_space_executable_euclidean_space)
                 A_)
               x i)))
    (basis_list A_) (Floatreal (Float (zero_inta, zero_inta)));

fun slist_apply (A1_, A2_) B_ xa =
  (fn i =>
    (case map_of A1_ (rep_slist A2_ xa) i of NONE => zero B_ | SOME b => b));

fun pdevs_inner A_ (Pdevs xs) b =
  Pdevs (map_slist
          (fn x =>
            inner ((real_inner_euclidean_space o
                     euclidean_space_ordered_euclidean_space o
                     ordered_euclidean_space_executable_euclidean_space)
                    A_)
              x b)
          xs);

fun inner_aform A_ x b =
  (inner ((real_inner_euclidean_space o
            euclidean_space_ordered_euclidean_space o
            ordered_euclidean_space_executable_euclidean_space)
           A_)
     (fst x) b,
    pdevs_inner A_ (snd x) b);

fun pdevs_apply A_ (Pdevs x) i = slist_apply (equal_nat, linorder_nat) A_ x i;

fun split_aform A_ x i =
  let
    val xi =
      scaleR (scaleR_real_vector A_)
        (inverse_real
          (Floatreal (of_int ring_1_float (Int_of_integer (2 : IntInf.int)))))
        (pdevs_apply
          ((zero_monoid_add o monoid_add_group_add o group_add_ab_group_add o
             ab_group_add_real_vector)
            A_)
          (snd x) i);
  in
    ((minus ((minus_group_add o group_add_ab_group_add o
               ab_group_add_real_vector)
              A_)
        (fst x) xi,
       pdev_upd A_ (snd x) i xi),
      (plus ((plus_semigroup_add o semigroup_add_monoid_add o
               monoid_add_group_add o group_add_ab_group_add o
               ab_group_add_real_vector)
              A_)
         (fst x) xi,
        pdev_upd A_ (snd x) i xi))
  end;

fun parts n [] = []
  | parts vb (v :: va) =
    (if equal_nata vb zero_nat then [v :: va]
      else take (suc (minus_nat vb one_nat)) (v :: va) ::
             parts (suc (minus_nat vb one_nat))
               (drop (suc (minus_nat vb one_nat)) (v :: va)));

fun powera A_ = power (one (one_power A_)) (times (times_power A_));

fun filter_slist xb xc =
  Abs_slist (filter (fn (a, b) => xb a b) (rep_slist linorder_nat xc));

fun filter_pdevs A_ p (Pdevs xs) = Pdevs (filter_slist p xs);

fun pdevs_inner2 A_ (Pdevs xs) b c =
  Pdevs (map_slist
          (fn x =>
            (inner ((real_inner_euclidean_space o
                      euclidean_space_ordered_euclidean_space o
                      ordered_euclidean_space_executable_euclidean_space)
                     A_)
               x b,
              inner ((real_inner_euclidean_space o
                       euclidean_space_ordered_euclidean_space o
                       ordered_euclidean_space_executable_euclidean_space)
                      A_)
                x c))
          xs);

fun inner2_aform A_ x a b =
  (inner2
     ((euclidean_space_ordered_euclidean_space o
        ordered_euclidean_space_executable_euclidean_space)
       A_)
     (fst x) a b,
    pdevs_inner2 A_ (snd x) a b);

fun pdevs_scaleR A_ (Pdevs rs) x =
  Pdevs (map_slist
          (fn r =>
            scaleR
              ((scaleR_real_vector o real_vector_real_normed_vector o
                 real_normed_vector_real_inner o real_inner_euclidean_space)
                A_)
              r x)
          rs);

fun scaleR_pdevs A_ r (Pdevs xs) =
  Pdevs (map_slist
          (scaleR
            ((scaleR_real_vector o real_vector_real_normed_vector o
               real_normed_vector_real_inner o real_inner_euclidean_space o
               euclidean_space_ordered_euclidean_space o
               ordered_euclidean_space_executable_euclidean_space)
              A_)
            r)
          xs);

fun uminus_pdevs A_ (Pdevs xs) =
  Pdevs (map_slist
          (uminus
            ((uminus_group_add o group_add_ab_group_add o
               ab_group_add_ordered_ab_group_add o
               ordered_ab_group_add_ordered_ab_group_add_abs o
               ordered_ab_group_add_abs_ordered_euclidean_space o
               ordered_euclidean_space_executable_euclidean_space)
              A_))
          xs);

fun uminus_aform A_ B_ x = (uminus A_ (fst x), uminus_pdevs B_ (snd x));

fun mirror_point (A1_, A2_) x y =
  minus A1_
    (scaleR A2_
      (Floatreal (of_int ring_1_float (Int_of_integer (2 : IntInf.int)))) x)
    y;

fun tdeva (A1_, A2_) p (Pdevs xs) =
  fold_slist
    ((zero_monoid_add o monoid_add_group_add o group_add_ab_group_add o
       ab_group_add_ordered_ab_group_add o
       ordered_ab_group_add_ordered_ab_group_add_abs o
       ordered_ab_group_add_abs_ordered_euclidean_space o
       ordered_euclidean_space_executable_euclidean_space)
       A1_,
      A2_)
    (fn a => fn b =>
      eucl_truncate_up A1_ p
        (plus ((plus_semigroup_add o semigroup_add_monoid_add o
                 monoid_add_group_add o group_add_ab_group_add o
                 ab_group_add_ordered_ab_group_add o
                 ordered_ab_group_add_ordered_ab_group_add_abs o
                 ordered_ab_group_add_abs_ordered_euclidean_space o
                 ordered_euclidean_space_executable_euclidean_space)
                A1_)
          (abs ((abs_ordered_ab_group_add_abs o
                  ordered_ab_group_add_abs_ordered_euclidean_space o
                  ordered_euclidean_space_executable_euclidean_space)
                 A1_)
            a)
          b))
    xs (zero ((zero_monoid_add o monoid_add_group_add o group_add_ab_group_add o
                ab_group_add_ordered_ab_group_add o
                ordered_ab_group_add_ordered_ab_group_add_abs o
                ordered_ab_group_add_abs_ordered_euclidean_space o
                ordered_euclidean_space_executable_euclidean_space)
               A1_));

fun lowest_vertex (A1_, A2_) x =
  minus ((minus_group_add o group_add_ab_group_add o
           ab_group_add_ordered_ab_group_add o
           ordered_ab_group_add_ordered_ab_group_add_abs o
           ordered_ab_group_add_abs_ordered_euclidean_space)
          A2_)
    (fst x)
    (listsuma
      ((monoid_add_group_add o group_add_ab_group_add o
         ab_group_add_ordered_ab_group_add o
         ordered_ab_group_add_ordered_ab_group_add_abs o
         ordered_ab_group_add_abs_ordered_euclidean_space)
        A2_)
      (map snd
        (list_of_pdevs
          ((zero_monoid_add o monoid_add_group_add o group_add_ab_group_add o
             ab_group_add_ordered_ab_group_add o
             ordered_ab_group_add_ordered_ab_group_add_abs o
             ordered_ab_group_add_abs_ordered_euclidean_space)
             A2_,
            A1_)
          (snd x))));

fun nat_of_integer k = Nat (max ord_integer (0 : IntInf.int) k);

fun pstn (Sctn (x1, x2)) = x2;

fun inner_scaleR_pdevs A_ x (Pdevs ys) =
  Pdevs (map_slist
          (fn y =>
            scaleR
              ((scaleR_real_vector o real_vector_real_normed_vector o
                 real_normed_vector_real_inner o real_inner_euclidean_space)
                A_)
              (inner (real_inner_euclidean_space A_) x y) y)
          ys);

fun one_pdevs A_ = Pdevs (one_slist A_);

fun pdevs_of_centered_ivl A_ r =
  inner_scaleR_pdevs
    ((euclidean_space_ordered_euclidean_space o
       ordered_euclidean_space_executable_euclidean_space)
      A_)
    r (one_pdevs A_);

fun summarize_pdevs (A1_, A2_) p i d x =
  let
    val t =
      tdeva (A1_, A2_) p
        (filter_pdevs
          ((real_vector_real_normed_vector o real_normed_vector_real_inner o
             real_inner_euclidean_space o
             euclidean_space_ordered_euclidean_space o
             ordered_euclidean_space_executable_euclidean_space)
            A1_)
          (uminus_funa (uminus_fun uminus_bool) i) x);
  in
    msum_pdevs
      ((real_vector_real_normed_vector o real_normed_vector_real_inner o
         real_inner_euclidean_space o euclidean_space_ordered_euclidean_space o
         ordered_euclidean_space_executable_euclidean_space)
        A1_)
      d (filter_pdevs
          ((real_vector_real_normed_vector o real_normed_vector_real_inner o
             real_inner_euclidean_space o
             euclidean_space_ordered_euclidean_space o
             ordered_euclidean_space_executable_euclidean_space)
            A1_)
          i x)
      (pdevs_of_centered_ivl A1_ t)
  end;

fun summarize_threshold (A1_, A2_) p t d x =
  summarize_pdevs (A1_, A2_) p
    (fn _ => fn y =>
      less_eq_real
        (times_reala t
          (infnorm A1_ (eucl_truncate_up A1_ p (tdeva (A1_, A2_) p x))))
        (infnorm A1_ y))
    d x;

fun trunc_err_pdevs A_ p (Pdevs xs) =
  Pdevs (map_slist
          (fn x =>
            minus ((minus_group_add o group_add_ab_group_add o
                     ab_group_add_ordered_ab_group_add o
                     ordered_ab_group_add_ordered_ab_group_add_abs o
                     ordered_ab_group_add_abs_ordered_euclidean_space o
                     ordered_euclidean_space_executable_euclidean_space)
                    A_)
              (eucl_truncate_down A_ p x) x)
          xs);

fun trunc_pdevs A_ p (Pdevs xs) =
  Pdevs (map_slist (eucl_truncate_down A_ p) xs);

fun trunc_bound_pdevs (A1_, A2_) p x =
  (trunc_pdevs A1_ p x, tdeva (A1_, A2_) p (trunc_err_pdevs A1_ p x));

fun trunc_bound_eucl A_ p s =
  let
    val d = eucl_truncate_down A_ p s;
    val ed =
      abs ((abs_ordered_ab_group_add_abs o
             ordered_ab_group_add_abs_ordered_euclidean_space o
             ordered_euclidean_space_executable_euclidean_space)
            A_)
        (minus
          ((minus_group_add o group_add_ab_group_add o
             ab_group_add_ordered_ab_group_add o
             ordered_ab_group_add_ordered_ab_group_add_abs o
             ordered_ab_group_add_abs_ordered_euclidean_space o
             ordered_euclidean_space_executable_euclidean_space)
            A_)
          d s);
  in
    (d, eucl_truncate_up A_ p ed)
  end;

fun divide_real (Floatreal (Float (a, b))) (Floatreal (Float (c, d))) =
  (if equal_reala (Floatreal (Float (c, d)))
        (Floatreal (of_int ring_1_float (Int_of_integer (2 : IntInf.int))))
    then (if equal_inta (mod_int a (Int_of_integer (2 : IntInf.int))) zero_inta
           then Floatreal
                  (Float (div_int a (Int_of_integer (2 : IntInf.int)), b))
           else Floatreal
                  (Float (a, minus_inta b (Int_of_integer (1 : IntInf.int)))))
    else (if equal_inta c (Int_of_integer (1 : IntInf.int))
           then Floatreal (Float (a, minus_inta b d))
           else (raise Fail "division not by 2")
                  (fn _ =>
                    divide_real (Floatreal (Float (a, b)))
                      (Floatreal (Float (c, d))))));

fun sup_aforma p x =
  truncate_up p
    (plus_reala (fst x)
      (tdeva (executable_euclidean_space_real, equal_real) p (snd x)));

fun inf_aforma p x =
  truncate_down p
    (minus_reala (fst x)
      (tdeva (executable_euclidean_space_real, equal_real) p (snd x)));

fun listsum A_ p xs =
  fold (fn a => fn b =>
         eucl_truncate_up A_ p
           (plus ((plus_semigroup_add o semigroup_add_monoid_add o
                    monoid_add_group_add o group_add_ab_group_add o
                    ab_group_add_ordered_ab_group_add o
                    ordered_ab_group_add_ordered_ab_group_add_abs o
                    ordered_ab_group_add_abs_ordered_euclidean_space o
                    ordered_euclidean_space_executable_euclidean_space)
                   A_)
             a b))
    xs (zero ((zero_monoid_add o monoid_add_group_add o group_add_ab_group_add o
                ab_group_add_ordered_ab_group_add o
                ordered_ab_group_add_ordered_ab_group_add_abs o
                ordered_ab_group_add_abs_ordered_euclidean_space o
                ordered_euclidean_space_executable_euclidean_space)
               A_));

fun inverse_aform p n x =
  let
    val l = inf_aforma p x;
    val u = sup_aforma p x;
    val a = min ord_real (abs_reala l) (abs_reala u);
    val b = max ord_real (abs_reala l) (abs_reala u);
    val alpha =
      uminus_reala
        (real_divl p
          (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)))
          (times_reala b b));
    val dmax =
      truncate_up p
        (minus_reala
          (real_divr p
            (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta))) a)
          (times_reala alpha a));
    val dmin =
      truncate_down p
        (minus_reala
          (real_divl p
            (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta))) b)
          (times_reala alpha b));
    val zeta =
      truncate_up p
        (divide_real (plus_reala dmin dmax)
          (Floatreal (of_int ring_1_float (Int_of_integer (2 : IntInf.int)))));
    val zetaa =
      (if less_real l (Floatreal (Float (zero_inta, zero_inta)))
        then uminus_reala zeta else zeta);
    val delta = truncate_up p (minus_reala zetaa dmin);
    val res =
      trunc_bound_eucl executable_euclidean_space_real p
        (plus_reala (times_reala alpha (fst x)) zetaa);
    val zs =
      trunc_bound_pdevs (executable_euclidean_space_real, equal_real) p
        (scaleR_pdevs executable_euclidean_space_real alpha (snd x));
  in
    (fst res,
      pdev_upd real_vector_real (fst zs) n
        (listsum executable_euclidean_space_real p [delta, snd res, snd zs]))
  end;

fun mult_aform p n x y =
  let
    val z0 =
      trunc_bound_eucl executable_euclidean_space_real p
        (times_reala (fst x) (fst y));
    val u =
      trunc_bound_pdevs (executable_euclidean_space_real, equal_real) p
        (scaleR_pdevs executable_euclidean_space_real (fst y) (snd x));
    val v =
      trunc_bound_pdevs (executable_euclidean_space_real, equal_real) p
        (scaleR_pdevs executable_euclidean_space_real (fst x) (snd y));
    val w =
      trunc_bound_pdevs (executable_euclidean_space_real, equal_real) p
        (add_pdevs real_vector_real (fst u) (fst v));
    val l =
      trunc_bound_eucl executable_euclidean_space_real p
        (times_reala (tdev ordered_euclidean_space_real (snd x))
          (tdev ordered_euclidean_space_real (snd y)));
  in
    (fst z0,
      pdev_upd real_vector_real (fst w) n
        (listsum executable_euclidean_space_real p
          [fst l, snd l, snd z0, snd u, snd v, snd w]))
  end;

fun add_aforma (A1_, A2_) p n x y =
  let
    val z0 =
      trunc_bound_eucl A1_ p
        (plus ((plus_semigroup_add o semigroup_add_monoid_add o
                 monoid_add_group_add o group_add_ab_group_add o
                 ab_group_add_ordered_ab_group_add o
                 ordered_ab_group_add_ordered_ab_group_add_abs o
                 ordered_ab_group_add_abs_ordered_euclidean_space o
                 ordered_euclidean_space_executable_euclidean_space)
                A1_)
          (fst x) (fst y));
    val z =
      trunc_bound_pdevs (A1_, A2_) p
        (add_pdevs
          ((real_vector_real_normed_vector o real_normed_vector_real_inner o
             real_inner_euclidean_space o
             euclidean_space_ordered_euclidean_space o
             ordered_euclidean_space_executable_euclidean_space)
            A1_)
          (snd x) (snd y));
  in
    (fst z0,
      pdev_upd
        ((real_vector_real_normed_vector o real_normed_vector_real_inner o
           real_inner_euclidean_space o
           euclidean_space_ordered_euclidean_space o
           ordered_euclidean_space_executable_euclidean_space)
          A1_)
        (fst z) n (listsum A1_ p [snd z0, snd z]))
  end;

fun approx_realarith A_ p (Add (a, b)) vs l =
  bind (approx_realarith A_ p a vs l)
    (fn a1 =>
      let
        val d1 = max ord_nat l (degree (equal_real, real_vector_real) (snd a1));
      in
        bind (approx_realarith A_ p b vs d1)
          (fn a2 =>
            let
              val d1a =
                max ord_nat d1 (degree (equal_real, real_vector_real) (snd a2));
            in
              SOME (add_aforma (executable_euclidean_space_real, equal_real) p
                     d1a a1 a2)
            end)
      end)
  | approx_realarith A_ p (Mult (a, b)) vs l =
    bind (approx_realarith A_ p a vs l)
      (fn a1 =>
        let
          val d1 =
            max ord_nat l (degree (equal_real, real_vector_real) (snd a1));
        in
          bind (approx_realarith A_ p b vs d1)
            (fn a2 =>
              let
                val d2 =
                  max ord_nat d1
                    (degree (equal_real, real_vector_real) (snd a2));
              in
                SOME (mult_aform p d2 a1 a2)
              end)
        end)
  | approx_realarith A_ p (Inverse a) vs m =
    bind (approx_realarith A_ p a vs m)
      (fn aa =>
        let
          val l = inf_aforma p aa;
          val u = sup_aforma p aa;
          val d =
            max ord_nat m (degree (equal_real, real_vector_real) (snd aa));
        in
          (if less_eq_real l (Floatreal (Float (zero_inta, zero_inta))) andalso
                less_eq_real (Floatreal (Float (zero_inta, zero_inta))) u
            then NONE
            else (if less_eq_real l (Floatreal (Float (zero_inta, zero_inta)))
                   then SOME (uminus_aform uminus_real
                               executable_euclidean_space_real
                               (inverse_aform p d
                                 (uminus_aform uminus_real
                                   executable_euclidean_space_real aa)))
                   else SOME (inverse_aform p d aa)))
        end)
  | approx_realarith A_ p (Minus a) vs m =
    map_option (uminus_aform uminus_real executable_euclidean_space_real)
      (approx_realarith A_ p a vs m)
  | approx_realarith A_ p (Num f) vs m = SOME (num_aform zero_real f)
  | approx_realarith A_ p (Var (i, b)) vs m =
    (if less_nat i (size_list vs) then SOME (inner_aform A_ (nth vs i) b)
      else NONE);

fun aform_scaleR A_ x y =
  (scaleR
     ((scaleR_real_vector o real_vector_real_normed_vector o
        real_normed_vector_real_inner o real_inner_euclidean_space)
       A_)
     (fst x) y,
    pdevs_scaleR A_ (snd x) y);

fun add_aform A_ x y =
  (plus ((plus_semigroup_add o semigroup_add_monoid_add o monoid_add_group_add o
           group_add_ab_group_add o ab_group_add_real_vector)
          A_)
     (fst x) (fst y),
    add_pdevs A_ (snd x) (snd y));

fun approx_euclarith A_ (B1_, B2_) p (AddE (a, b)) vs l =
  bind (approx_euclarith A_ (B1_, B2_) p a vs l)
    (fn a1 =>
      let
        val d1 =
          max ord_nat l
            (degree
              (B1_, (real_vector_real_normed_vector o
                      real_normed_vector_real_inner o
                      real_inner_euclidean_space o
                      euclidean_space_ordered_euclidean_space)
                      B2_)
              (snd a1));
      in
        bind (approx_euclarith A_ (B1_, B2_) p b vs d1)
          (fn a2 =>
            let
              val _ =
                max ord_nat d1
                  (degree
                    (B1_, (real_vector_real_normed_vector o
                            real_normed_vector_real_inner o
                            real_inner_euclidean_space o
                            euclidean_space_ordered_euclidean_space)
                            B2_)
                    (snd a2));
            in
              SOME (add_aform
                     ((real_vector_real_normed_vector o
                        real_normed_vector_real_inner o
                        real_inner_euclidean_space o
                        euclidean_space_ordered_euclidean_space)
                       B2_)
                     a1 a2)
            end)
      end)
  | approx_euclarith A_ (B1_, B2_) p (ScaleR (a, b)) vs m =
    map_option
      (fn aa => aform_scaleR (euclidean_space_ordered_euclidean_space B2_) aa b)
      (approx_realarith A_ p a vs m);

fun approx_euclarith_outer (A1_, A2_) (B1_, B2_) p t ea asa =
  let
    val d =
      fold (max ord_nat o
             (fn x =>
               degree
                 (A2_, (real_vector_real_normed_vector o
                         real_normed_vector_real_inner o
                         real_inner_euclidean_space o
                         euclidean_space_ordered_euclidean_space o
                         ordered_euclidean_space_executable_euclidean_space)
                         A1_)
                 (snd x)))
        asa zero_nat;
  in
    bind (approx_euclarith A1_
           (B2_, ordered_euclidean_space_executable_euclidean_space B1_) p ea
           asa d)
      (fn s =>
        SOME (apsnd
               (summarize_threshold (B1_, B2_) p t
                 (max ord_nat d
                   (degree
                     (B2_, (real_vector_real_normed_vector o
                             real_normed_vector_real_inner o
                             real_inner_euclidean_space o
                             euclidean_space_ordered_euclidean_space o
                             ordered_euclidean_space_executable_euclidean_space)
                             B1_)
                     (snd s))))
               s))
  end;

fun lorenz x =
  (fn prec => fn thres => fn xa => fn qs =>
    approx_euclarith_outer
      (executable_euclidean_space_prod
         (executable_euclidean_space_real, equal_real)
         (executable_euclidean_space_prod
            (executable_euclidean_space_real, equal_real)
            (executable_euclidean_space_real, equal_real),
           equal_prod equal_real equal_real),
        equal_prod equal_real (equal_prod equal_real equal_real))
      (executable_euclidean_space_prod
         (executable_euclidean_space_real, equal_real)
         (executable_euclidean_space_prod
            (executable_euclidean_space_real, equal_real)
            (executable_euclidean_space_real, equal_real),
           equal_prod equal_real equal_real),
        equal_prod equal_real (equal_prod equal_real equal_real))
      prec thres
      (AddE (ScaleR
               (Add (Mult (Num (Floatreal
                                 (Float
                                   (uminus_inta
                                      (Int_of_integer
(6004799503160661 : IntInf.int)),
                                     uminus_inta
                                       (Int_of_integer (51 : IntInf.int))))),
                            Var (zero_nat,
                                  (Floatreal (Float (zero_inta, zero_inta)),
                                    (Floatreal (Float (zero_inta, zero_inta)),
                                      Floatreal
(Float (Int_of_integer (1 : IntInf.int), zero_inta)))))),
                      Mult (Add (Var (zero_nat,
                                       (Floatreal
  (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
 (Floatreal (Float (zero_inta, zero_inta)),
   Floatreal (Float (zero_inta, zero_inta))))),
                                  Var (zero_nat,
(Floatreal (Float (zero_inta, zero_inta)),
  (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
    Floatreal (Float (zero_inta, zero_inta)))))),
                             Add (Mult (Num
  (Floatreal
    (Float
      (Int_of_integer (4915166360050299 : IntInf.int),
        uminus_inta (Int_of_integer (51 : IntInf.int))))),
 Var (zero_nat,
       (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
         (Floatreal (Float (zero_inta, zero_inta)),
           Floatreal (Float (zero_inta, zero_inta)))))),
                                   Mult (Num
   (Floatreal
     (Float
       (uminus_inta (Int_of_integer (5777093055467152 : IntInf.int)),
         uminus_inta (Int_of_integer (52 : IntInf.int))))),
  Var (zero_nat,
        (Floatreal (Float (zero_inta, zero_inta)),
          (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
            Floatreal (Float (zero_inta, zero_inta))))))))),
                 (Floatreal (Float (zero_inta, zero_inta)),
                   (Floatreal (Float (zero_inta, zero_inta)),
                     Floatreal
                       (Float (Int_of_integer (1 : IntInf.int), zero_inta))))),
              AddE (ScaleR
                      (Add (Mult (Num (Floatreal
(Float
  (uminus_inta (Int_of_integer (6425432926773530 : IntInf.int)),
    uminus_inta (Int_of_integer (48 : IntInf.int))))),
                                   Var (zero_nat,
 (Floatreal (Float (zero_inta, zero_inta)),
   (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
     Floatreal (Float (zero_inta, zero_inta)))))),
                             Mult (Mult (Num
   (Floatreal
     (Float
       (Int_of_integer (5198143472295670 : IntInf.int),
         uminus_inta (Int_of_integer (54 : IntInf.int))))),
  Add (Var (zero_nat,
             (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
               (Floatreal (Float (zero_inta, zero_inta)),
                 Floatreal (Float (zero_inta, zero_inta))))),
        Var (zero_nat,
              (Floatreal (Float (zero_inta, zero_inta)),
                (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
                  Floatreal (Float (zero_inta, zero_inta))))))),
                                    Var (zero_nat,
  (Floatreal (Float (zero_inta, zero_inta)),
    (Floatreal (Float (zero_inta, zero_inta)),
      Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta))))))),
                        (Floatreal (Float (zero_inta, zero_inta)),
                          (Floatreal
                             (Float
                               (Int_of_integer (1 : IntInf.int), zero_inta)),
                            Floatreal (Float (zero_inta, zero_inta))))),
                     ScaleR
                       (Add (Mult (Num (Floatreal
 (Float
   (Int_of_integer (6658416365912628 : IntInf.int),
     uminus_inta (Int_of_integer (49 : IntInf.int))))),
                                    Var (zero_nat,
  (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
    (Floatreal (Float (zero_inta, zero_inta)),
      Floatreal (Float (zero_inta, zero_inta)))))),
                              Mult (Mult (Minus
    (Num (Floatreal
           (Float
             (Int_of_integer (5198143472295670 : IntInf.int),
               uminus_inta (Int_of_integer (54 : IntInf.int)))))),
   Add (Var (zero_nat,
              (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
                (Floatreal (Float (zero_inta, zero_inta)),
                  Floatreal (Float (zero_inta, zero_inta))))),
         Var (zero_nat,
               (Floatreal (Float (zero_inta, zero_inta)),
                 (Floatreal
                    (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
                   Floatreal (Float (zero_inta, zero_inta))))))),
                                     Var (zero_nat,
   (Floatreal (Float (zero_inta, zero_inta)),
     (Floatreal (Float (zero_inta, zero_inta)),
       Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta))))))),
                         (Floatreal
                            (Float
                              (Int_of_integer (1 : IntInf.int), zero_inta)),
                           (Floatreal (Float (zero_inta, zero_inta)),
                             Floatreal (Float (zero_inta, zero_inta))))))))
      (xa :: qs))
    x;

fun mod_nat m n = Nat (mod_integer (integer_of_nat m) (integer_of_nat n));

fun decimal x ex =
  (if less_eq_int zero_inta ex
    then times_reala x
           (powera power_real
             (Floatreal
               (of_int ring_1_float (Int_of_integer (10 : IntInf.int))))
             (nat ex))
    else real_divl (nat_of_integer (53 : IntInf.int)) x
           (powera power_real
             (Floatreal
               (of_int ring_1_float (Int_of_integer (10 : IntInf.int))))
             (nat (uminus_inta ex))));

fun next_section_turn_distance_factor
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = next_section_turn_distance_factor;

fun transversal_directions B_ inf_of_appr sup_of_appr f =
  let
    val i = inf_of_appr f;
    val s = sup_of_appr f;
  in
    listsuma
      ((monoid_add_group_add o group_add_ab_group_add o
         ab_group_add_ordered_ab_group_add o
         ordered_ab_group_add_ordered_ab_group_add_abs o
         ordered_ab_group_add_abs_ordered_euclidean_space o
         ordered_euclidean_space_executable_euclidean_space)
        B_)
      (map (fn b =>
             scaleR
               ((scaleR_real_vector o real_vector_real_normed_vector o
                  real_normed_vector_real_inner o real_inner_euclidean_space o
                  euclidean_space_ordered_euclidean_space o
                  ordered_euclidean_space_executable_euclidean_space)
                 B_)
               (if less_eq_real
                     (inner
                       ((real_inner_euclidean_space o
                          euclidean_space_ordered_euclidean_space o
                          ordered_euclidean_space_executable_euclidean_space)
                         B_)
                       i b)
                     (Floatreal (Float (zero_inta, zero_inta)))
                 then (if less_eq_real
                            (inner
                              ((real_inner_euclidean_space o
                                 euclidean_space_ordered_euclidean_space o
                                 ordered_euclidean_space_executable_euclidean_space)
                                B_)
                              s b)
                            (Floatreal (Float (zero_inta, zero_inta)))
                        then inner ((real_inner_euclidean_space o
                                      euclidean_space_ordered_euclidean_space o
                                      ordered_euclidean_space_executable_euclidean_space)
                                     B_)
                               s b
                        else Floatreal (Float (zero_inta, zero_inta)))
                 else (if less_eq_real
                            (Floatreal (Float (zero_inta, zero_inta)))
                            (inner
                              ((real_inner_euclidean_space o
                                 euclidean_space_ordered_euclidean_space o
                                 ordered_euclidean_space_executable_euclidean_space)
                                B_)
                              s b)
                        then inner ((real_inner_euclidean_space o
                                      euclidean_space_ordered_euclidean_space o
                                      ordered_euclidean_space_executable_euclidean_space)
                                     B_)
                               i b
                        else Floatreal (Float (zero_inta, zero_inta))))
               b)
        (basis_list B_))
  end;

fun strongest_direction A_ t =
  let
    val b =
      fold (fn b => fn ba =>
             (if less_eq_real
                   (abs_reala
                     (inner
                       ((real_inner_euclidean_space o
                          euclidean_space_ordered_euclidean_space o
                          ordered_euclidean_space_executable_euclidean_space)
                         A_)
                       t ba))
                   (abs_reala
                     (inner
                       ((real_inner_euclidean_space o
                          euclidean_space_ordered_euclidean_space o
                          ordered_euclidean_space_executable_euclidean_space)
                         A_)
                       t b))
               then b else ba))
        (basis_list A_)
        (zero ((zero_monoid_add o monoid_add_group_add o
                 group_add_ab_group_add o ab_group_add_ordered_ab_group_add o
                 ordered_ab_group_add_ordered_ab_group_add_abs o
                 ordered_ab_group_add_abs_ordered_euclidean_space o
                 ordered_euclidean_space_executable_euclidean_space)
                A_));
  in
    (scaleR
       ((scaleR_real_vector o real_vector_real_normed_vector o
          real_normed_vector_real_inner o real_inner_euclidean_space o
          euclidean_space_ordered_euclidean_space o
          ordered_euclidean_space_executable_euclidean_space)
         A_)
       (sgn_reala
         (inner
           ((real_inner_euclidean_space o
              euclidean_space_ordered_euclidean_space o
              ordered_euclidean_space_executable_euclidean_space)
             A_)
           t b))
       b,
      abs_reala
        (inner
          ((real_inner_euclidean_space o
             euclidean_space_ordered_euclidean_space o
             ordered_euclidean_space_executable_euclidean_space)
            A_)
          t b))
  end;

fun strongest_transversal B_ inf_of_appr sup_of_appr f =
  strongest_direction B_ (transversal_directions B_ inf_of_appr sup_of_appr f);

fun normal (Sctn (x1, x2)) = x1;

fun appr_above_sctn A_ appr_inf_inner optns x sctn =
  less_real (pstn sctn) (appr_inf_inner optns x (normal sctn));

fun rk2_param
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = rk2_param;

val bot_dres : 'a dres = DSUCCEEDi;

fun rk2_remainder_dres A_ add_appr scale_appr scale_appr_ivl ode_approx
  ode_d_approx ode_d2_approx h optns xt xttt fxttt =
  let
    val x = rk2_param optns;
  in
    dbind (case ode_d2_approx optns [xttt, fxttt, fxttt, xt] of NONE => bot_dres
            | SOME a => DRETURN a)
      (fn xa =>
        dbind (case ode_d_approx optns [xttt, fxttt, xa, xt] of NONE => bot_dres
                | SOME a => DRETURN a)
          (fn xb =>
            dbind (case ode_d_approx optns [xttt, xb, xa, xt, fxttt]
                    of NONE => bot_dres | SOME a => DRETURN a)
              (fn xc =>
                dbind (case add_appr optns xa xc [xt, xttt, fxttt]
                        of NONE => bot_dres | SOME a => DRETURN a)
                  (fn xd =>
                    dbind (case scale_appr optns
                                  (Floatreal
                                    (Float
                                      (Int_of_integer (1 : IntInf.int),
zero_inta)))
                                  (Floatreal
                                    (of_int ring_1_float
                                      (Int_of_integer (6 : IntInf.int))))
                                  xd
                                  [xt, xttt, fxttt]
                            of NONE => bot_dres | SOME a => DRETURN a)
                      (fn xe =>
                        dbind (case ode_approx optns [xt, xe, xttt, fxttt]
                                of NONE => bot_dres | SOME a => DRETURN a)
                          (fn xf =>
                            dbind (case scale_appr_ivl optns
  (Floatreal (Float (zero_inta, zero_inta)))
  (times_reala h x)
  xf
  [xe, xt, xttt, fxttt]
                                    of NONE => bot_dres | SOME a => DRETURN a)
                              (fn xg =>
                                dbind (case
add_appr optns xt xg [xf, xe, xttt, fxttt] of NONE => bot_dres
| SOME a => DRETURN a)
                                  (fn xh =>
                                    dbind (case
    ode_d2_approx optns [xh, xf, xf, xe, xt, xttt, fxttt] of NONE => bot_dres
    | SOME a => DRETURN a)
                                      (fn xi =>
dbind (case scale_appr optns (uminus_reala x)
              (Floatreal
                (of_int ring_1_float (Int_of_integer (4 : IntInf.int))))
              xi
              [xe, xt, xttt, fxttt]
        of NONE => bot_dres | SOME a => DRETURN a)
  (fn xj =>
    dbind (case add_appr optns xj xe [xt, xttt, fxttt] of NONE => bot_dres
            | SOME a => DRETURN a)
      (fn xk =>
        dbind (case scale_appr optns
                      (powera power_real h (nat_of_integer (3 : IntInf.int)))
                      (Floatreal
                        (Float (Int_of_integer (1 : IntInf.int), zero_inta)))
                      xk
                      [xt, xttt, fxttt]
                of NONE => bot_dres | SOME a => DRETURN a)
          (fn xl =>
            dbind (case scale_appr_ivl optns
                          (Floatreal (Float (zero_inta, zero_inta)))
                          (powera power_real h
                            (nat_of_integer (3 : IntInf.int)))
                          xk
                          [xt, xttt, fxttt]
                    of NONE => bot_dres | SOME a => DRETURN a)
              (fn xm => DRETURN (xl, xm))))))))))))))
  end;

fun ivl_appr_of_appr A_ appr_of_ivl inf_of_appr sup_of_appr x =
  appr_of_ivl (inf_of_appr x) (sup_of_appr x);

fun rk2_incr_dres A_ add_appr scale_appr scale_appr_ivl ode_approx optns h x =
  let
    val xa = rk2_param optns;
  in
    dbind (case ode_approx optns [x] of NONE => bot_dres | SOME a => DRETURN a)
      (fn xaa =>
        dbind (case scale_appr optns
                      (minus_reala
                        (times_reala xa
                          (Floatreal
                            (of_int ring_1_float
                              (Int_of_integer (2 : IntInf.int)))))
                        (Floatreal
                          (Float (Int_of_integer (1 : IntInf.int), zero_inta))))
                      (times_reala xa
                        (Floatreal
                          (of_int ring_1_float
                            (Int_of_integer (2 : IntInf.int)))))
                      xaa
                      [x]
                of NONE => bot_dres | SOME a => DRETURN a)
          (fn xb =>
            dbind (case scale_appr optns (times_reala h xa)
                          (Floatreal
                            (Float
                              (Int_of_integer (1 : IntInf.int), zero_inta)))
                          xaa
                          [xb, x]
                    of NONE => bot_dres | SOME a => DRETURN a)
              (fn xc =>
                dbind (case add_appr optns x xc [xb, x] of NONE => bot_dres
                        | SOME a => DRETURN a)
                  (fn xd =>
                    dbind (case ode_approx optns [xd, x, xb] of NONE => bot_dres
                            | SOME a => DRETURN a)
                      (fn xe =>
                        dbind (case scale_appr optns
                                      (Floatreal
(Float (Int_of_integer (1 : IntInf.int), zero_inta)))
                                      (times_reala xa
(Floatreal (of_int ring_1_float (Int_of_integer (2 : IntInf.int)))))
                                      xe
                                      [x, xb]
                                of NONE => bot_dres | SOME a => DRETURN a)
                          (fn xf =>
                            dbind (case scale_appr_ivl optns
  (Floatreal (Float (zero_inta, zero_inta)))
  (times_reala h xa)
  xaa
  [xb, x]
                                    of NONE => bot_dres | SOME a => DRETURN a)
                              (fn xg =>
                                dbind (case add_appr optns x xg [xb, x]
of NONE => bot_dres | SOME a => DRETURN a)
                                  (fn xh =>
                                    dbind (case ode_approx optns [xh, x, xb]
    of NONE => bot_dres | SOME a => DRETURN a)
                                      (fn xi =>
dbind (case scale_appr optns
              (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)))
              (times_reala xa
                (Floatreal
                  (of_int ring_1_float (Int_of_integer (2 : IntInf.int)))))
              xi
              [x, xb]
        of NONE => bot_dres | SOME a => DRETURN a)
  (fn xj =>
    dbind (case add_appr optns xb xf [x] of NONE => bot_dres
            | SOME a => DRETURN a)
      (fn xk =>
        dbind (case add_appr optns xb xj [x] of NONE => bot_dres
                | SOME a => DRETURN a)
          (fn xl => DRETURN (xk, xl)))))))))))))
  end;

fun p_appr A_ appr_of_ivl msum_appr inf_of_appr sup_of_appr ode_approx optns x0
  h x =
  map_option
    (fn y =>
      msum_appr x0
        (appr_of_ivl
           (inf ((inf_semilattice_inf o semilattice_inf_lattice o
                   lattice_distrib_lattice o
                   distrib_lattice_ordered_euclidean_space o
                   ordered_euclidean_space_executable_euclidean_space)
                  A_)
             (zero ((zero_monoid_add o monoid_add_group_add o
                      group_add_ab_group_add o
                      ab_group_add_ordered_ab_group_add o
                      ordered_ab_group_add_ordered_ab_group_add_abs o
                      ordered_ab_group_add_abs_ordered_euclidean_space o
                      ordered_euclidean_space_executable_euclidean_space)
                     A_))
             (scaleR
               ((scaleR_real_vector o real_vector_real_normed_vector o
                  real_normed_vector_real_inner o real_inner_euclidean_space o
                  euclidean_space_ordered_euclidean_space o
                  ordered_euclidean_space_executable_euclidean_space)
                 A_)
               h (inf_of_appr y)))
          (sup ((sup_semilattice_sup o semilattice_sup_lattice o
                  lattice_distrib_lattice o
                  distrib_lattice_ordered_euclidean_space o
                  ordered_euclidean_space_executable_euclidean_space)
                 A_)
            (zero ((zero_monoid_add o monoid_add_group_add o
                     group_add_ab_group_add o
                     ab_group_add_ordered_ab_group_add o
                     ordered_ab_group_add_ordered_ab_group_add_abs o
                     ordered_ab_group_add_abs_ordered_euclidean_space o
                     ordered_euclidean_space_executable_euclidean_space)
                    A_))
            (scaleR
              ((scaleR_real_vector o real_vector_real_normed_vector o
                 real_normed_vector_real_inner o real_inner_euclidean_space o
                 euclidean_space_ordered_euclidean_space o
                 ordered_euclidean_space_executable_euclidean_space)
                A_)
              h (sup_of_appr y)))))
    (ode_approx optns [x]);

fun widening_mod
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = widening_mod;

fun p_iter A_ appr_of_ivl msum_appr inf_of_appr sup_of_appr ode_approx optns x0
  h i x =
  (if equal_nata i zero_nat
    then let
           val _ = TextIO.print "=P_iter failed: ";
           val _ = print_eucl A_ (inf_of_appr x);
           val _ = TextIO.print " - ";
           val _ = print_eucl A_ (sup_of_appr x);
           val _ = println "";
         in
           NONE
         end
    else bind_err "=P_appr failed"
           (p_appr A_ appr_of_ivl msum_appr inf_of_appr sup_of_appr ode_approx
             optns x0 h x)
           (fn xa =>
             let
               val (l, u) = (inf_of_appr xa, sup_of_appr xa);
               val (la, ua) = (inf_of_appr x, sup_of_appr x);
             in
               (if less_eq
                     ((ord_preorder o preorder_order o order_semilattice_inf o
                        semilattice_inf_lattice o lattice_distrib_lattice o
                        distrib_lattice_ordered_euclidean_space o
                        ordered_euclidean_space_executable_euclidean_space)
                       A_)
                     la l andalso
                     less_eq
                       ((ord_preorder o preorder_order o order_semilattice_inf o
                          semilattice_inf_lattice o lattice_distrib_lattice o
                          distrib_lattice_ordered_euclidean_space o
                          ordered_euclidean_space_executable_euclidean_space)
                         A_)
                       u ua
                 then SOME x
                 else p_iter A_ appr_of_ivl msum_appr inf_of_appr sup_of_appr
                        ode_approx optns x0 h (minus_nat i one_nat)
                        (appr_of_ivl
                           (minus
                             ((minus_group_add o group_add_ab_group_add o
                                ab_group_add_ordered_ab_group_add o
                                ordered_ab_group_add_ordered_ab_group_add_abs o
                                ordered_ab_group_add_abs_ordered_euclidean_space o
                                ordered_euclidean_space_executable_euclidean_space)
                               A_)
                             (inf ((inf_semilattice_inf o
                                     semilattice_inf_lattice o
                                     lattice_distrib_lattice o
                                     distrib_lattice_ordered_euclidean_space o
                                     ordered_euclidean_space_executable_euclidean_space)
                                    A_)
                               l la)
                             (if equal_nata
                                   (mod_nat (minus_nat i one_nat)
                                     (widening_mod optns))
                                   zero_nat
                               then abs ((abs_ordered_ab_group_add_abs o
   ordered_ab_group_add_abs_ordered_euclidean_space o
   ordered_euclidean_space_executable_euclidean_space)
  A_)
                                      (minus
((minus_group_add o group_add_ab_group_add o ab_group_add_ordered_ab_group_add o
   ordered_ab_group_add_ordered_ab_group_add_abs o
   ordered_ab_group_add_abs_ordered_euclidean_space o
   ordered_euclidean_space_executable_euclidean_space)
  A_)
l la)
                               else zero ((zero_monoid_add o
    monoid_add_group_add o group_add_ab_group_add o
    ab_group_add_ordered_ab_group_add o
    ordered_ab_group_add_ordered_ab_group_add_abs o
    ordered_ab_group_add_abs_ordered_euclidean_space o
    ordered_euclidean_space_executable_euclidean_space)
   A_)))
                          (plus ((plus_semigroup_add o
                                   semigroup_add_monoid_add o
                                   monoid_add_group_add o
                                   group_add_ab_group_add o
                                   ab_group_add_ordered_ab_group_add o
                                   ordered_ab_group_add_ordered_ab_group_add_abs o
                                   ordered_ab_group_add_abs_ordered_euclidean_space o
                                   ordered_euclidean_space_executable_euclidean_space)
                                  A_)
                            (sup ((sup_semilattice_sup o
                                    semilattice_sup_lattice o
                                    lattice_distrib_lattice o
                                    distrib_lattice_ordered_euclidean_space o
                                    ordered_euclidean_space_executable_euclidean_space)
                                   A_)
                              u ua)
                            (if equal_nata
                                  (mod_nat (minus_nat i one_nat)
                                    (widening_mod optns))
                                  zero_nat
                              then abs ((abs_ordered_ab_group_add_abs o
  ordered_ab_group_add_abs_ordered_euclidean_space o
  ordered_euclidean_space_executable_euclidean_space)
 A_)
                                     (minus
                                       ((minus_group_add o
  group_add_ab_group_add o ab_group_add_ordered_ab_group_add o
  ordered_ab_group_add_ordered_ab_group_add_abs o
  ordered_ab_group_add_abs_ordered_euclidean_space o
  ordered_euclidean_space_executable_euclidean_space)
 A_)
                                       u ua)
                              else zero ((zero_monoid_add o
   monoid_add_group_add o group_add_ab_group_add o
   ab_group_add_ordered_ab_group_add o
   ordered_ab_group_add_ordered_ab_group_add_abs o
   ordered_ab_group_add_abs_ordered_euclidean_space o
   ordered_euclidean_space_executable_euclidean_space)
  A_)))))
             end));

fun cert_stepsize A_ appr_of_ivl msum_appr inf_of_appr sup_of_appr ode_approx
  optns x0 h n i =
  (if equal_nata i zero_nat
    then let
           val _ = println "=cert_stepsize failed";
         in
           NONE
         end
    else (case p_iter A_ appr_of_ivl msum_appr inf_of_appr sup_of_appr
                 ode_approx optns
                 (ivl_appr_of_appr A_ appr_of_ivl inf_of_appr sup_of_appr x0) h
                 n (ivl_appr_of_appr A_ appr_of_ivl inf_of_appr sup_of_appr x0)
           of NONE =>
             let
               val _ = TextIO.print "=cert_stepsize failed on: ";
               val _ = print_eucl A_ (inf_of_appr x0);
               val _ = TextIO.print " - ";
               val _ = print_eucl A_ (sup_of_appr x0);
               val _ = println "";
             in
               cert_stepsize A_ appr_of_ivl msum_appr inf_of_appr sup_of_appr
                 ode_approx optns x0
                 (divide_real h
                   (Floatreal
                     (of_int ring_1_float (Int_of_integer (2 : IntInf.int)))))
                 n (minus_nat i one_nat)
             end
           | SOME x => SOME (h, x)));

fun halve_stepsizes
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = halve_stepsizes;

fun iterations
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = iterations;

fun stepsize
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = stepsize;

fun rk2_step_dres A_ appr_of_ivl msum_appr inf_of_appr sup_of_appr add_appr
  scale_appr scale_appr_ivl independent_appr width_appr ode_approx ode_d_approx
  ode_d2_approx optns x =
  dbind (case cert_stepsize A_ appr_of_ivl msum_appr inf_of_appr sup_of_appr
                ode_approx optns x (stepsize optns) (iterations optns)
                (halve_stepsizes optns)
          of NONE => bot_dres | SOME a => DRETURN a)
    (fn (a, b) =>
      let
        val xa = independent_appr x b;
      in
        dbind (case ode_approx optns [x] of NONE => bot_dres
                | SOME aa => DRETURN aa)
          (fn _ =>
            dbind (case ode_approx optns [xa, x] of NONE => bot_dres
                    | SOME aa => DRETURN aa)
              (fn xc =>
                dbind (rk2_remainder_dres A_ add_appr scale_appr scale_appr_ivl
                        ode_approx ode_d_approx ode_d2_approx a optns x xa xc)
                  (fn (aa, ba) =>
                    dbind (rk2_incr_dres A_ add_appr scale_appr scale_appr_ivl
                            ode_approx optns a x)
                      (fn (ab, bb) =>
                        dbind (case scale_appr optns a
                                      (Floatreal
(Float (Int_of_integer (1 : IntInf.int), zero_inta)))
                                      ab
                                      [x]
                                of NONE => bot_dres | SOME ac => DRETURN ac)
                          (fn xf =>
                            dbind (case scale_appr_ivl optns
  (Floatreal (Float (zero_inta, zero_inta)))
  a
  bb
  [x]
                                    of NONE => bot_dres | SOME ac => DRETURN ac)
                              (fn xg =>
                                dbind (case add_appr optns x xf []
of NONE => bot_dres | SOME ac => DRETURN ac)
                                  (fn xh =>
                                    dbind (case add_appr optns x xg []
    of NONE => bot_dres | SOME ac => DRETURN ac)
                                      (fn xi =>
let
  val xj =
    msum_appr xh (ivl_appr_of_appr A_ appr_of_ivl inf_of_appr sup_of_appr aa);
  val xk =
    msum_appr xi (ivl_appr_of_appr A_ appr_of_ivl inf_of_appr sup_of_appr ba);
in
  DRETURN (a, (width_appr optns aa, (xk, xj)))
end))))))))
      end);

fun euler_step A_ appr_of_ivl msum_appr inf_of_appr sup_of_appr add_appr
  scale_appr scale_appr_ivl width_appr ode_approx ode_d_approx optns x0 =
  bind_err "=certify stepsize failed"
    (cert_stepsize A_ appr_of_ivl msum_appr inf_of_appr sup_of_appr ode_approx
      optns x0 (stepsize optns) (iterations optns) (halve_stepsizes optns))
    (fn (h, cx) =>
      bind_err "=ode_approx X0 failed" (ode_approx optns [x0])
        (fn x0a =>
          bind_err "=ode_approx CX failed" (ode_approx optns [cx])
            (fn f =>
              bind_err "=ode_d_approx failed" (ode_d_approx optns [cx, f])
                (fn d =>
                  bind_err "=scale_appr err failed"
                    (scale_appr optns (times_reala h h)
                       (Floatreal
                         (of_int ring_1_float
                           (Int_of_integer (2 : IntInf.int))))
                       (ivl_appr_of_appr A_ appr_of_ivl inf_of_appr sup_of_appr
                         d)
                      [])
                    (fn err =>
                      bind_err "=scale_appr euler failed"
                        (scale_appr optns h
                           (Floatreal
                             (Float
                               (Int_of_integer (1 : IntInf.int), zero_inta)))
                           x0a
                          [x0])
                        (fn s =>
                          bind_err "=scale_appr_ivl euler failed"
                            (scale_appr_ivl optns
                               (Floatreal (Float (zero_inta, zero_inta)))
                               h
                               x0a
                              [x0])
                            (fn sa =>
                              bind_err "=add_appr euler failed"
                                (add_appr optns x0 s [])
                                (fn x1 =>
                                  bind_err "=add_appr euler_ivl failed"
                                    (add_appr optns x0 sa [])
                                    (fn cX1 =>
                                      let
val res =
  msum_appr x1 (ivl_appr_of_appr A_ appr_of_ivl inf_of_appr sup_of_appr err);
val res_ivl =
  msum_appr cX1
    (appr_of_ivl
       (inf ((inf_semilattice_inf o semilattice_inf_lattice o
               lattice_distrib_lattice o
               distrib_lattice_ordered_euclidean_space o
               ordered_euclidean_space_executable_euclidean_space)
              A_)
         (zero ((zero_monoid_add o monoid_add_group_add o
                  group_add_ab_group_add o ab_group_add_ordered_ab_group_add o
                  ordered_ab_group_add_ordered_ab_group_add_abs o
                  ordered_ab_group_add_abs_ordered_euclidean_space o
                  ordered_euclidean_space_executable_euclidean_space)
                 A_))
         (inf_of_appr err))
      (sup ((sup_semilattice_sup o semilattice_sup_lattice o
              lattice_distrib_lattice o
              distrib_lattice_ordered_euclidean_space o
              ordered_euclidean_space_executable_euclidean_space)
             A_)
        (zero ((zero_monoid_add o monoid_add_group_add o
                 group_add_ab_group_add o ab_group_add_ordered_ab_group_add o
                 ordered_ab_group_add_ordered_ab_group_add_abs o
                 ordered_ab_group_add_abs_ordered_euclidean_space o
                 ordered_euclidean_space_executable_euclidean_space)
                A_))
        (sup_of_appr err)));
                                      in
SOME (h, (width_appr optns err, (res_ivl, res)))
                                      end)))))))));

fun method_id
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = method_id;

fun do_intersection_dres (A1_, A2_) appr_of_ivl msum_appr inf_of_appr
  sup_of_appr add_appr scale_appr scale_appr_ivl appr_inf_inner inter_appr_plane
  reduce_appr independent_appr width_appr ode_approx ode_d_approx ode_d2_approx
  optns sctn x =
  dbind (dbind
          (case ode_approx optns [x] of NONE => bot_dres | SOME a => DRETURN a)
          (fn xa =>
            dWHILE
              (fn (xb, (f, (_, _))) =>
                not (appr_above_sctn A1_ appr_inf_inner optns xb sctn) andalso
                  eq A2_
                    (fst (strongest_transversal A1_ inf_of_appr sup_of_appr f))
                    (normal sctn))
              (fn (a, (_, (ab, bb))) =>
                dbind (if equal_nata (method_id optns)
                            (nat_of_integer (2 : IntInf.int))
                        then rk2_step_dres A1_ appr_of_ivl msum_appr inf_of_appr
                               sup_of_appr add_appr scale_appr scale_appr_ivl
                               independent_appr width_appr ode_approx
                               ode_d_approx ode_d2_approx optns a
                        else (case euler_step A1_ appr_of_ivl msum_appr
                                     inf_of_appr sup_of_appr add_appr scale_appr
                                     scale_appr_ivl width_appr ode_approx
                                     ode_d_approx optns a
                               of NONE => bot_dres | SOME aa => DRETURN aa))
                  (fn (_, (_, (ae, be))) =>
                    dbind (case inter_appr_plane optns (reduce_appr optns ae)
                                  sctn
                            of NONE => bot_dres | SOME aa => DRETURN aa)
                      (fn xc =>
                        dbind (case ode_approx optns [be] of NONE => bot_dres
                                | SOME aa => DRETURN aa)
                          (fn xd => DRETURN (be, (xd, (xc :: ab, ae :: bb)))))))
              (x, (xa, ([], [x])))))
    (fn (a, (_, (ab, bb))) =>
      DRETURN
        (ab, (bb, (if appr_above_sctn A1_ appr_inf_inner optns a sctn then []
                    else [a]))));

fun intersects_appr A_ appr_inf_inner appr_sup_inner optns x sctn =
  less_eq_real (appr_inf_inner optns x (normal sctn)) (pstn sctn) andalso
    less_eq_real (pstn sctn) (appr_sup_inner optns x (normal sctn));

fun max_intersection_step
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = max_intersection_step;

fun stepsize_update stepsizea
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = Options_ext
      (precision, tolerance, stepsizea stepsize, iterations, halve_stepsizes,
        widening_mod, rk2_param, max_tdev_thres, presplit_summary_tolerance,
        collect_granularity, start_section, checkpoint_sections, stop_sections,
        safe_appr, snap_sections, min_section_distance,
        next_section_distance_factor, next_section_turn_distance_factor,
        printing_fun, irect_mod, result_fun, max_intersection_step,
        adaptive_atol, method_id, more);

fun max_tdev_thres
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = max_tdev_thres;

fun adaptive_atol
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = adaptive_atol;

fun printing_fun
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = printing_fun;

fun safe_appr
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = safe_appr;

fun precision
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = precision;

fun resolve_sctn_dres (A1_, A2_) B_ appr_of_ivl msum_appr inf_of_appr
  sup_of_appr add_appr scale_appr scale_appr_ivl split_appr appr_inf_inner
  appr_sup_inner inter_appr_plane reduce_appr independent_appr width_appr
  ode_approx ode_d_approx ode_d2_approx optns sctn xs =
  dWHILE (fn (xsa, (_, _)) => not (null xsa))
    (fn (a, (aa, ba)) =>
      let
        val (ab, bb) = hd a;
        val xb = removeAll (equal_prod equal_real B_) (ab, bb) a;
        val _ = TextIO.print "= XS: ";
        val _ = println (int_to_string (int_of_nat (size_list a)));
        val _ = TextIO.print "= PS: ";
        val _ = println (int_to_string (int_of_nat (size_list aa)));
        val _ = TextIO.print "= RS:  ";
        val _ = println (int_to_string (int_of_nat (size_list ba)));
      in
        (if less_real (max_tdev_thres optns) (width_appr optns bb)
          then let
                 val _ = TextIO.print "= splitting: ";
                 val _ = print_real (width_appr optns bb);
                 val xk = split_appr optns bb;
               in
                 dbind (if pred_list (safe_appr optns) xk then DRETURN ()
                         else bot_dres)
                   (fn _ =>
                     let
                       val _ = TextIO.print "-->";
                       val _ =
                         map ((fn x =>
                                let
                                  val _ = TextIO.print " ";
                                in
                                  print_real x
                                end) o
                               width_appr optns)
                           xk;
                     in
                       DRETURN (map (fn ac => (ab, ac)) xk @ xb, (aa, ba))
                     end)
               end
          else let
                 val _ = TextIO.print "= euler step: stepsize = ";
                 val _ = print_real ab;
                 val _ = println "";
               in
                 dbind (if equal_nata (method_id optns)
                             (nat_of_integer (2 : IntInf.int))
                         then rk2_step_dres A1_ appr_of_ivl msum_appr
                                inf_of_appr sup_of_appr add_appr scale_appr
                                scale_appr_ivl independent_appr width_appr
                                ode_approx ode_d_approx ode_d2_approx
                                (stepsize_update (fn _ => ab) optns) bb
                         else (case euler_step A1_ appr_of_ivl msum_appr
                                      inf_of_appr sup_of_appr add_appr
                                      scale_appr scale_appr_ivl width_appr
                                      ode_approx ode_d_approx
                                      (stepsize_update (fn _ => ab) optns) bb
                                of NONE => bot_dres | SOME ac => DRETURN ac))
                   (fn (ac, (ad, (ae, be))) =>
                     dbind (if safe_appr optns ae then DRETURN () else bot_dres)
                       (fn _ =>
                         dbind (if safe_appr optns be then DRETURN ()
                                 else bot_dres)
                           (fn _ =>
                             let
                               val _ = println "= interpolated step:";
                               val _ = printing_fun optns ae;
                               val _ = println "= discrete step:";
                               val _ = printing_fun optns be;
                               val _ = TextIO.print "= error: ";
                               val _ = print_real ad;
                               val _ = println "";
                             in
                               (if less_real (adaptive_atol optns) ad
                                 then let
val _ = println "= revoking step because of too large error ";
                                      in
DRETURN
  ((divide_real ac
      (Floatreal (of_int ring_1_float (Int_of_integer (2 : IntInf.int)))),
     bb) ::
     map (fn (h, af) =>
           (divide_real h
              (Floatreal
                (of_int ring_1_float (Int_of_integer (2 : IntInf.int)))),
             af))
       xb,
    (aa, ba))
                                      end
                                 else (if intersects_appr A1_ appr_inf_inner
    appr_sup_inner optns ae sctn orelse
    intersects_appr A1_ appr_inf_inner appr_sup_inner optns be sctn
then let
       val _ = println "= error OK, intersection ";
     in
       (if less_real (max_intersection_step optns) ac
         then let
                val _ =
                  println "= revoke_intersection, can try with smaller steps";
              in
                DRETURN
                  ((divide_real ac
                      (Floatreal
                        (of_int ring_1_float
                          (Int_of_integer (2 : IntInf.int)))),
                     bb) ::
                     xb,
                    (aa, ba))
              end
         else let
                val _ = println "= do_intersection";
              in
                dbind (do_intersection_dres (A1_, A2_) appr_of_ivl msum_appr
                        inf_of_appr sup_of_appr add_appr scale_appr
                        scale_appr_ivl appr_inf_inner inter_appr_plane
                        reduce_appr independent_appr width_appr ode_approx
                        ode_d_approx ode_d2_approx
                        (stepsize_update (fn _ => ac) optns) sctn bb)
                  (fn (af, (ag, bg)) =>
                    dbind (if pred_list (safe_appr optns) af then DRETURN ()
                            else bot_dres)
                      (fn _ =>
                        dbind (if pred_list (safe_appr optns) ag then DRETURN ()
                                else bot_dres)
                          (fn _ =>
                            dbind (if pred_list (safe_appr optns) bg
                                    then DRETURN () else bot_dres)
                              (fn _ =>
                                let
                                  val _ = println "= done_intersection";
                                  val _ =
                                    map (fn x =>
  let
    val _ = println "= interpolated step:";
  in
    printing_fun optns x
  end)
                                      ag;
                                  val _ =
                                    map (fn x =>
  let
    val _ = println "= discrete step:";
  in
    printing_fun optns x
  end)
                                      (bg @ af);
                                in
                                  DRETURN (xb, ((bb, af) :: aa, bg @ ba))
                                end))))
              end)
     end
else let
       val _ = println "= error OK, euler stepped ";
     in
       dbind (case ode_approx optns [be] of NONE => bot_dres
               | SOME af => DRETURN af)
         (fn xw =>
           (if eq A2_
                 (fst (strongest_transversal A1_ inf_of_appr sup_of_appr xw))
                 (normal sctn)
             then DRETURN
                    (xb @ [(min ord_real
                              (divide_real
                                (times_reala
                                  (Floatreal
                                    (of_int ring_1_float
                                      (Int_of_integer (3 : IntInf.int))))
                                  ac)
                                (Floatreal
                                  (of_int ring_1_float
                                    (Int_of_integer (2 : IntInf.int)))))
                              (max ord_real ac
                                (truncate_down (precision optns)
                                  (times_reala ac
                                    (real_divl (precision optns)
                                      (adaptive_atol optns) ad)))),
                             be)],
                      (aa, ba))
             else DRETURN (xb, (aa, be :: ba))))
     end))
                             end)))
               end)
      end)
    (xs, ([], []));

fun disjoint_apprs B_ inf_of_appr sup_of_appr x y =
  let
    val iX = inf_of_appr x;
    val sX = sup_of_appr x;
    val iY = inf_of_appr y;
    val sY = sup_of_appr y;
  in
    list_ex
      (fn i =>
        less_real
          (inner
            ((real_inner_euclidean_space o
               euclidean_space_ordered_euclidean_space o
               ordered_euclidean_space_executable_euclidean_space)
              B_)
            sX i)
          (inner
            ((real_inner_euclidean_space o
               euclidean_space_ordered_euclidean_space o
               ordered_euclidean_space_executable_euclidean_space)
              B_)
            iY i) orelse
          less_real
            (inner
              ((real_inner_euclidean_space o
                 euclidean_space_ordered_euclidean_space o
                 ordered_euclidean_space_executable_euclidean_space)
                B_)
              sY i)
            (inner
              ((real_inner_euclidean_space o
                 euclidean_space_ordered_euclidean_space o
                 ordered_euclidean_space_executable_euclidean_space)
                B_)
              iX i))
      (basis_list B_)
  end;

fun ivl_of_apprs A_ appr_of_ivl inf_of_appr sup_of_appr (x :: xs) =
  appr_of_ivl
    (fold (inf ((inf_semilattice_inf o semilattice_inf_lattice o
                  lattice_distrib_lattice o
                  distrib_lattice_ordered_euclidean_space o
                  ordered_euclidean_space_executable_euclidean_space)
                 A_) o
            inf_of_appr)
      xs (inf_of_appr x))
    (fold (sup ((sup_semilattice_sup o semilattice_sup_lattice o
                  lattice_distrib_lattice o
                  distrib_lattice_ordered_euclidean_space o
                  ordered_euclidean_space_executable_euclidean_space)
                 A_) o
            sup_of_appr)
      xs (sup_of_appr x))
  | ivl_of_apprs A_ appr_of_ivl inf_of_appr sup_of_appr [] =
    appr_of_ivl
      (infa ((inf_conditionally_complete_lattice o
               conditionally_complete_lattice_ordered_euclidean_space o
               ordered_euclidean_space_executable_euclidean_space)
              A_)
        bot_set)
      (supa ((sup_conditionally_complete_lattice o
               conditionally_complete_lattice_ordered_euclidean_space o
               ordered_euclidean_space_executable_euclidean_space)
              A_)
        bot_set);

fun collect_granularity
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = collect_granularity;

fun partition_dres A_ B_ appr_of_ivl inf_of_appr sup_of_appr split_appr
  width_appr optns xs =
  let
    val x = ivl_of_apprs A_ appr_of_ivl inf_of_appr sup_of_appr xs;
  in
    dbind (dWHILE (fn (rs, _) => not (null rs))
            (fn (a, b) =>
              let
                val xb = hd a;
                val xc = removeAll B_ xb a;
                val xd =
                  filter
                    (fn aa =>
                      not (disjoint_apprs A_ inf_of_appr sup_of_appr aa xb))
                    xs;
              in
                (if null xd then DRETURN (xc, b)
                  else (if less_eq_real (width_appr optns xb)
                             (collect_granularity optns)
                         then DRETURN (xc, xb :: b)
                         else let
                                val xe =
                                  ivl_of_apprs A_ appr_of_ivl inf_of_appr
                                    sup_of_appr xd;
                                val xf =
                                  appr_of_ivl
                                    (sup ((sup_semilattice_sup o
    semilattice_sup_lattice o lattice_distrib_lattice o
    distrib_lattice_ordered_euclidean_space o
    ordered_euclidean_space_executable_euclidean_space)
   A_)
                                      (inf_of_appr xb) (inf_of_appr xe))
                                    (inf ((inf_semilattice_inf o
    semilattice_inf_lattice o lattice_distrib_lattice o
    distrib_lattice_ordered_euclidean_space o
    ordered_euclidean_space_executable_euclidean_space)
   A_)
                                      (sup_of_appr xb) (sup_of_appr xe));
                                val xg = split_appr optns xf;
                              in
                                DRETURN (xg @ xc, b)
                              end))
              end)
            ([x], []))
      (fn (_, a) => DRETURN a)
  end;

fun times_nat m n = Nat (IntInf.* (integer_of_nat m, integer_of_nat n));

fun resolve_collect_dres (A1_, A2_) B_ appr_of_ivl msum_appr inf_of_appr
  sup_of_appr add_appr scale_appr scale_appr_ivl split_appr appr_inf_inner
  appr_sup_inner inter_appr_plane reduce_appr independent_appr width_appr
  ode_approx ode_d_approx ode_d2_approx optns sctn x0S =
  dbind (resolve_sctn_dres (A1_, A2_) B_ appr_of_ivl msum_appr inf_of_appr
          sup_of_appr add_appr scale_appr scale_appr_ivl split_appr
          appr_inf_inner appr_sup_inner inter_appr_plane reduce_appr
          independent_appr width_appr ode_approx ode_d_approx ode_d2_approx
          optns sctn (map (fn a => (stepsize optns, a)) x0S))
    (fn (_, (aa, ba)) =>
      (if null aa then DRETURN ([], ([], ba))
        else let
               val xa = map fst aa;
               val xb = maps snd aa;
               val _ = TextIO.print "= partitioning ";
               val _ = TextIO.print (int_to_string (int_of_nat (size_list xb)));
             in
               dbind (partition_dres A1_ B_ appr_of_ivl inf_of_appr sup_of_appr
                       split_appr width_appr optns xb)
                 (fn xe =>
                   let
                     val _ = TextIO.print "partitioned to ";
                     val _ =
                       TextIO.print (int_to_string (int_of_nat (size_list xe)));
                     val _ = println "";
                     val _ = map (printing_fun optns) xe;
                   in
                     (if less_eq_nat
                           (times_nat (nat_of_integer (2 : IntInf.int))
                             (size_list xe))
                           (size_list xb)
                       then DRETURN (xe, (xe, ba)) else DRETURN (xa, (xe, ba)))
                   end)
             end));

fun next_section_distance_factor
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = next_section_distance_factor;

fun min_section_distance
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = min_section_distance;

fun checkpoint_sections
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = checkpoint_sections;

fun max_height A_ appr_sup_inner optns b xs =
  fold (max ord_real o (fn x => appr_sup_inner optns x b)) (tl xs)
    (appr_sup_inner optns (hd xs) b);

fun stop_sections
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = stop_sections;

fun snap_sections
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = snap_sections;

fun next_sections_dres (A1_, A2_) B_ appr_of_ivl inf_of_appr sup_of_appr
  appr_sup_inner ode_approx optns d xs =
  dbind (foldli (remdups B_ xs)
          (fn a =>
            (case a of DSUCCEEDi => false | DFAILi => false
              | DRETURN _ => true))
          (fn x => fn s =>
            dbind s
              (fn sigma =>
                dbind (case ode_approx optns [x] of NONE => bot_dres
                        | SOME a => DRETURN a)
                  (fn xa =>
                    DRETURN
                      ((x, strongest_transversal A1_ inf_of_appr sup_of_appr
                             xa) ::
                        sigma))))
          (DRETURN []))
    (fn x =>
      let
        val _ = TextIO.print "= next sections with d = ";
        val _ = print_real d;
        val _ = println "";
      in
        DRETURN
          (map (fn b =>
                 let
                   val xsa =
                     map_filter
                       (fn xa =>
                         (if let
                               val (_, (ba, _)) = xa;
                             in
                               eq A2_ b ba
                             end
                           then SOME let
                                       val (xb, (_, a)) = xa;
                                     in
                                       (xb, a)
                                     end
                           else NONE))
                       x;
                   val h = max_height A1_ appr_sup_inner optns b (map fst xsa);
                   val f =
                     fold (max ord_real o snd) xsa
                       (Floatreal (Float (zero_inta, zero_inta)));
                   val ha =
                     plus_reala
                       (plus_reala h (abs_reala (min_section_distance optns)))
                       (abs_reala
                         (appr_sup_inner optns
                            (appr_of_ivl
                               (scaleR
                                 ((scaleR_real_vector o
                                    real_vector_real_normed_vector o
                                    real_normed_vector_real_inner o
                                    real_inner_euclidean_space o
                                    euclidean_space_ordered_euclidean_space o
                                    ordered_euclidean_space_executable_euclidean_space)
                                   A1_)
                                 (times_reala (abs_reala d) f) b)
                              (scaleR
                                ((scaleR_real_vector o
                                   real_vector_real_normed_vector o
                                   real_normed_vector_real_inner o
                                   real_inner_euclidean_space o
                                   euclidean_space_ordered_euclidean_space o
                                   ordered_euclidean_space_executable_euclidean_space)
                                  A1_)
                                (times_reala (abs_reala d) f) b))
                           b));
                   val sctn =
                     find (fn sctn =>
                            eq A2_ (normal sctn) b andalso
                              (less_eq_real h (pstn sctn) andalso
                                (less_eq_real
                                   (abs_reala (minus_reala ha (pstn sctn)))
                                   (snap_sections optns) orelse
                                  less_eq_real (pstn sctn) ha)))
                       (stop_sections optns @ checkpoint_sections optns);
                   val a = (case sctn of NONE => Sctn (b, ha) | SOME ba => ba);
                 in
                   (map fst xsa, a)
                 end)
            (remdups A2_ (map (fst o snd) x)))
      end);

fun start_section
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = start_section;

fun poincare_distance_d_dres (A1_, A2_) B_ appr_of_ivl msum_appr inf_of_appr
  sup_of_appr add_appr scale_appr scale_appr_ivl split_appr appr_inf_inner
  appr_sup_inner inter_appr_plane reduce_appr independent_appr width_appr
  ode_approx ode_d_approx ode_d2_approx optns x0s =
  dbind (dWHILE (fn (unres, (cps, _)) => not (null unres) orelse not (null cps))
          (fn (a, (aa, ba)) =>
            (if not (null a)
              then let
                     val (ab, bb) = hd a;
                     val _ = TextIO.print "= unres: ";
                     val _ =
                       TextIO.print (int_to_string (int_of_nat (size_list a)));
                     val _ = TextIO.print " cps: ";
                     val _ =
                       TextIO.print (int_to_string (int_of_nat (size_list aa)));
                     val _ = TextIO.print " stops: ";
                     val _ =
                       TextIO.print (int_to_string (int_of_nat (size_list ba)));
                     val _ = TextIO.print " XS: ";
                     val _ =
                       TextIO.print (int_to_string (int_of_nat (size_list ab)));
                     val _ = TextIO.print " Flowing towards: ";
                     val _ = print_eucl A1_ (normal bb);
                     val _ = TextIO.print " -- ";
                     val _ = print_real (pstn bb);
                     val _ = println "";
                   in
                     dbind (if pred_list (safe_appr optns) ab then DRETURN ()
                             else bot_dres)
                       (fn _ =>
                         dbind (resolve_collect_dres (A1_, A2_) B_ appr_of_ivl
                                 msum_appr inf_of_appr sup_of_appr add_appr
                                 scale_appr scale_appr_ivl split_appr
                                 appr_inf_inner appr_sup_inner inter_appr_plane
                                 reduce_appr independent_appr width_appr
                                 ode_approx ode_d_approx ode_d2_approx optns bb
                                 ab)
                           (fn (ac, (ad, bd)) =>
                             let
                               val _ = println "= resolved and collected";
                             in
                               dbind (next_sections_dres (A1_, A2_) B_
                                       appr_of_ivl inf_of_appr sup_of_appr
                                       appr_sup_inner ode_approx optns
                                       (times_reala
 (next_section_turn_distance_factor optns) (stepsize optns))
                                       bd)
                                 (fn xr =>
                                   (if membera (equal_sctn A2_)
 (stop_sections optns) bb
                                     then let
    val _ = TextIO.print "= stopping ";
  in
    DRETURN (tl a @ xr, (aa, (ad, bb) :: ba))
  end
                                     else (if membera (equal_sctn A2_)
        (checkpoint_sections optns) bb
    then let
           val _ = TextIO.print "= checkpointing ";
         in
           DRETURN (tl a @ xr, ((ad, bb) :: aa, ba))
         end
    else let
           val _ = TextIO.print "= adding ";
           val _ = TextIO.print " XS: ";
           val _ = TextIO.print (int_to_string (int_of_nat (size_list ac)));
           val _ = TextIO.print " RS: ";
           val _ = TextIO.print (int_to_string (int_of_nat (size_list bd)));
           val _ = println "";
         in
           dbind (next_sections_dres (A1_, A2_) B_ appr_of_ivl inf_of_appr
                   sup_of_appr appr_sup_inner ode_approx optns
                   (times_reala (next_section_distance_factor optns)
                     (stepsize optns))
                   ac)
             (fn xy => DRETURN (tl a @ xy @ xr, (aa, ba)))
         end)))
                             end))
                   end
              else let
                     val _ =
                       TextIO.print
                         " We are at a checkpoint, here we can reunite different groups again";
                     val xb = map snd aa;
                     val xc =
                       map (fn sctn =>
                             (maps fst
                                (filter
                                  (fn (_, sctna) => equal_sctna A2_ sctna sctn)
                                  aa),
                               sctn))
                         xb;
                   in
                     dbind (foldli
                             (remdups
                               (equal_prod (equal_list B_) (equal_sctn A2_)) xc)
                             (fn ab =>
                               (case ab of DSUCCEEDi => false | DFAILi => false
                                 | DRETURN _ => true))
                             (fn x => fn s =>
                               dbind s
                                 (fn sigma =>
                                   let
                                     val (ab, _) = x;
                                   in
                                     dbind (next_sections_dres (A1_, A2_) B_
     appr_of_ivl inf_of_appr sup_of_appr appr_sup_inner ode_approx optns
     (times_reala (next_section_distance_factor optns) (stepsize optns)) ab)
                                       (fn xe => DRETURN (xe @ sigma))
                                   end))
                             (DRETURN []))
                       (fn xd => DRETURN (xd, ([], ba)))
                   end))
          ([(x0s, start_section optns)], ([], [])))
    (fn (_, (_, a)) => DRETURN a);

fun scaleQ_componentwise A_ x y [] =
  ScaleR
    (Num (Floatreal (Float (zero_inta, zero_inta))),
      zero ((zero_monoid_add o monoid_add_group_add o group_add_ab_group_add o
              ab_group_add_ordered_ab_group_add o
              ordered_ab_group_add_ordered_ab_group_add_abs o
              ordered_ab_group_add_abs_ordered_euclidean_space o
              ordered_euclidean_space_executable_euclidean_space)
             A_))
  | scaleQ_componentwise A_ x y (b :: bs) =
    AddE (ScaleR (Mult (Mult (Num x, Var (zero_nat, b)), Inverse (Num y)), b),
           scaleQ_componentwise A_ x y bs);

fun scaleQ_aform_componentwise (A1_, A2_) prec tol x z y ys =
  approx_euclarith_outer (A1_, A2_) (A1_, A2_) prec tol
    (scaleQ_componentwise A1_ x z (basis_list A1_)) (y :: ys);

fun add_componentwise A_ [] =
  ScaleR
    (Num (Floatreal (Float (zero_inta, zero_inta))),
      zero ((zero_monoid_add o monoid_add_group_add o group_add_ab_group_add o
              ab_group_add_ordered_ab_group_add o
              ordered_ab_group_add_ordered_ab_group_add_abs o
              ordered_ab_group_add_abs_ordered_euclidean_space o
              ordered_euclidean_space_executable_euclidean_space)
             A_))
  | add_componentwise A_ (b :: bs) =
    AddE (ScaleR (Add (Var (zero_nat, b), Var (one_nat, b)), b),
           add_componentwise A_ bs);

fun add_aform_componentwise (A1_, A2_) prec tol x y ys =
  approx_euclarith_outer (A1_, A2_) (A1_, A2_) prec tol
    (add_componentwise A1_ (basis_list A1_)) (x :: y :: ys);

fun presplit_summary_tolerance
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = presplit_summary_tolerance;

fun max_pdev (A1_, A2_) x =
  fold (fn xa => fn y =>
         (if less_real (infnorm A1_ (snd y)) (infnorm A1_ (snd xa)) then xa
           else y))
    (list_of_pdevs
      ((zero_monoid_add o monoid_add_group_add o group_add_ab_group_add o
         ab_group_add_ordered_ab_group_add o
         ordered_ab_group_add_ordered_ab_group_add_abs o
         ordered_ab_group_add_abs_ordered_euclidean_space o
         ordered_euclidean_space_executable_euclidean_space)
         A1_,
        A2_)
      x)
    (zero_nat,
      zero ((zero_monoid_add o monoid_add_group_add o group_add_ab_group_add o
              ab_group_add_ordered_ab_group_add o
              ordered_ab_group_add_ordered_ab_group_add_abs o
              ordered_ab_group_add_abs_ordered_euclidean_space o
              ordered_euclidean_space_executable_euclidean_space)
             A1_));

fun split_aform_largest_uncond (A1_, A2_) x =
  let
    val (i, _) = max_pdev (A1_, A2_) (snd x);
  in
    split_aform
      ((real_vector_real_normed_vector o real_normed_vector_real_inner o
         real_inner_euclidean_space o euclidean_space_ordered_euclidean_space o
         ordered_euclidean_space_executable_euclidean_space)
        A1_)
      x i
  end;

fun split_aform_largest (E1_, E2_) optns x =
  let
    val (a, b) =
      split_aform_largest_uncond (E1_, E2_)
        (fst x,
          summarize_threshold (E1_, E2_) (precision optns)
            (presplit_summary_tolerance optns)
            (degree
              (E2_, (real_vector_real_normed_vector o
                      real_normed_vector_real_inner o
                      real_inner_euclidean_space o
                      euclidean_space_ordered_euclidean_space o
                      ordered_euclidean_space_executable_euclidean_space)
                      E1_)
              (snd x))
            (snd x));
  in
    [a, b]
  end;

fun scaleR_ivl A_ a [] =
  ScaleR
    (Num (Floatreal (Float (zero_inta, zero_inta))),
      zero ((zero_monoid_add o monoid_add_group_add o group_add_ab_group_add o
              ab_group_add_ordered_ab_group_add o
              ordered_ab_group_add_ordered_ab_group_add_abs o
              ordered_ab_group_add_abs_ordered_euclidean_space o
              ordered_euclidean_space_executable_euclidean_space)
             A_))
  | scaleR_ivl A_ a (b :: bs) =
    AddE (ScaleR (Mult (Var (zero_nat, a), Var (one_nat, b)), b),
           scaleR_ivl A_ a bs);

fun scaleR_aform_ivl (A1_, A2_) prec tol a b y ys =
  approx_euclarith_outer (A1_, A2_) (A1_, A2_) prec tol
    (scaleR_ivl A1_ (hd (basis_list A1_)) (basis_list A1_))
    ((scaleR
        ((scaleR_real_vector o real_vector_real_normed_vector o
           real_normed_vector_real_inner o real_inner_euclidean_space o
           euclidean_space_ordered_euclidean_space o
           ordered_euclidean_space_executable_euclidean_space)
          A1_)
        (divide_real (plus_reala a b)
          (Floatreal (of_int ring_1_float (Int_of_integer (2 : IntInf.int)))))
        (hd (basis_list A1_)),
       pdev_upd
         ((real_vector_real_normed_vector o real_normed_vector_real_inner o
            real_inner_euclidean_space o
            euclidean_space_ordered_euclidean_space o
            ordered_euclidean_space_executable_euclidean_space)
           A1_)
         (zero_pdevs
           ((zero_monoid_add o monoid_add_group_add o group_add_ab_group_add o
              ab_group_add_ordered_ab_group_add o
              ordered_ab_group_add_ordered_ab_group_add_abs o
              ordered_ab_group_add_abs_ordered_euclidean_space o
              ordered_euclidean_space_executable_euclidean_space)
             A1_))
         (fold (max ord_nat o
                 (fn x =>
                   degree
                     (A2_, (real_vector_real_normed_vector o
                             real_normed_vector_real_inner o
                             real_inner_euclidean_space o
                             euclidean_space_ordered_euclidean_space o
                             ordered_euclidean_space_executable_euclidean_space)
                             A1_)
                     (snd x)))
           (y :: ys) zero_nat)
         (scaleR
           ((scaleR_real_vector o real_vector_real_normed_vector o
              real_normed_vector_real_inner o real_inner_euclidean_space o
              euclidean_space_ordered_euclidean_space o
              ordered_euclidean_space_executable_euclidean_space)
             A1_)
           (divide_real (minus_reala b a)
             (Floatreal
               (of_int ring_1_float (Int_of_integer (2 : IntInf.int)))))
           (hd (basis_list A1_)))) ::
      y :: ys);

fun tolerance
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = tolerance;

fun intersect_segment_xlinea p ((x0, y0), (x1, y1)) xl =
  (if less_eq_real x0 xl andalso less_eq_real xl x1
    then (if equal_reala x0 x1
           then SOME (min ord_real y0 y1, max ord_real y0 y1)
           else let
                  val yl =
                    truncate_down p
                      (plus_reala
                        (truncate_down p
                          (times_reala
                            (real_divl p (minus_reala y1 y0)
                              (minus_reala x1 x0))
                            (minus_reala xl x0)))
                        y0);
                  val yr =
                    truncate_up p
                      (plus_reala
                        (truncate_up p
                          (times_reala
                            (real_divr p (minus_reala y1 y0)
                              (minus_reala x1 x0))
                            (minus_reala xl x0)))
                        y0);
                in
                  SOME (yl, yr)
                end)
    else NONE);

fun intersect_segment_xline prec ((a, b), (c, d)) x =
  (if less_eq_real a c then intersect_segment_xlinea prec ((a, b), (c, d)) x
    else intersect_segment_xlinea prec ((c, d), (a, b)) x);

fun bound_intersect_2d prec [] x = NONE
  | bound_intersect_2d prec (x :: xs) xl =
    (case bound_intersect_2d prec xs xl
      of NONE => intersect_segment_xline prec x xl
      | SOME (m, ma) =>
        (case intersect_segment_xline prec x xl of NONE => SOME (m, ma)
          | SOME (mb, mc) => SOME (min ord_real mb m, max ord_real mc ma)));

fun mina le a b = (if le a b then a else b);

fun selsort A_ le (y :: ys) =
  let
    val xm = fold (mina le) ys y;
    val xs = remove1 A_ xm (y :: ys);
  in
    xm :: selsort A_ le xs
  end
  | selsort A_ le [] = [];

fun psi p q r = lex p q andalso lex q r;

fun ccw p q r =
  less_real (Floatreal (Float (zero_inta, zero_inta))) (det3 p q r);

fun ccwa p q r =
  ccw p q r orelse
    equal_reala (det3 p q r) (Floatreal (Float (zero_inta, zero_inta))) andalso
      (psi p q r orelse (psi q r p orelse psi r p q));

fun half_segments_of_aform x =
  let
    val x0 =
      lowest_vertex
        (equal_prod equal_real equal_real,
          ordered_euclidean_space_prod
            (equal_real, ordered_euclidean_space_real)
            (equal_real, ordered_euclidean_space_real))
        (fst x, nlex_pdevs (snd x));
  in
    polychain_of (ab_group_add_prod ab_group_add_real ab_group_add_real) x0
      (map (scaleR_proda real_vector_real real_vector_real
             (Floatreal
               (of_int ring_1_float (Int_of_integer (2 : IntInf.int)))))
        (selsort (equal_prod equal_real equal_real)
          (ccwa (zero_proda zero_real zero_real)) (inl (snd x))))
  end;

fun segments_of_aform x =
  let
    val hs = half_segments_of_aform x;
  in
    hs @ map (pairself
               (mirror_point
                 (minus_prod
                    ((minus_group_add o group_add_ab_group_add o
                       ab_group_add_real_vector)
                      real_vector_real)
                    ((minus_group_add o group_add_ab_group_add o
                       ab_group_add_real_vector)
                      real_vector_real),
                   scaleR_prod real_vector_real real_vector_real)
                 (fst x)))
           hs
  end;

fun bound_intersect_2d_ud prec x xl =
  (case segments_of_aform x
    of [] =>
      (if equal_reala (fst (fst x)) xl
        then let
               val m = snd (fst x);
             in
               SOME (m, m)
             end
        else NONE)
    | [xa] =>
      (case bound_intersect_2d prec
              (filter
                (fn (a, b) =>
                  let
                    val (x1, _) = a;
                  in
                    (fn (x2, _) => less_real x1 x2)
                  end
                    b)
                [xa])
              xl
        of NONE => NONE
        | SOME (m, ma) =>
          (case bound_intersect_2d prec
                  (filter
                    (fn (a, b) =>
                      let
                        val (x1, _) = a;
                      in
                        (fn (x2, _) => less_real x2 x1)
                      end
                        b)
                    [xa])
                  xl
            of NONE => NONE
            | SOME (mb, mc) => SOME (min ord_real m mb, max ord_real mc ma)))
    | [xa, y] => intersect_segment_xline prec xa xl
    | xa :: y :: ad :: lista =>
      (case bound_intersect_2d prec
              (filter
                (fn (a, b) =>
                  let
                    val (x1, _) = a;
                  in
                    (fn (x2, _) => less_real x1 x2)
                  end
                    b)
                (xa :: y :: ad :: lista))
              xl
        of NONE => NONE
        | SOME (m, ma) =>
          (case bound_intersect_2d prec
                  (filter
                    (fn (a, b) =>
                      let
                        val (x1, _) = a;
                      in
                        (fn (x2, _) => less_real x2 x1)
                      end
                        b)
                    (xa :: y :: ad :: lista))
                  xl
            of NONE => NONE
            | SOME (mb, mc) => SOME (min ord_real m mb, max ord_real mc ma))));

fun pdevs_of_ivl A_ l u =
  scaleR_pdevs A_
    (divide_real
      (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)))
      (Floatreal (of_int ring_1_float (Int_of_integer (2 : IntInf.int)))))
    (inner_scaleR_pdevs
      ((euclidean_space_ordered_euclidean_space o
         ordered_euclidean_space_executable_euclidean_space)
        A_)
      (minus
        ((minus_group_add o group_add_ab_group_add o
           ab_group_add_ordered_ab_group_add o
           ordered_ab_group_add_ordered_ab_group_add_abs o
           ordered_ab_group_add_abs_ordered_euclidean_space o
           ordered_euclidean_space_executable_euclidean_space)
          A_)
        u l)
      (one_pdevs A_));

fun aform_of_ivl A_ l u =
  (scaleR
     ((scaleR_real_vector o real_vector_real_normed_vector o
        real_normed_vector_real_inner o real_inner_euclidean_space o
        euclidean_space_ordered_euclidean_space o
        ordered_euclidean_space_executable_euclidean_space)
       A_)
     (inverse_real
       (Floatreal (of_int ring_1_float (Int_of_integer (2 : IntInf.int)))))
     (plus ((plus_semigroup_add o semigroup_add_monoid_add o
              monoid_add_group_add o group_add_ab_group_add o
              ab_group_add_ordered_ab_group_add o
              ordered_ab_group_add_ordered_ab_group_add_abs o
              ordered_ab_group_add_abs_ordered_euclidean_space o
              ordered_euclidean_space_executable_euclidean_space)
             A_)
       l u),
    pdevs_of_ivl A_ l u);

fun inter_aform_plane_ortho A_ p z n g =
  bind (those
         (map (fn b => bound_intersect_2d_ud p (inner2_aform A_ z n b) g)
           (basis_list A_)))
    (fn mMs =>
      let
        val l =
          listsuma
            ((monoid_add_group_add o group_add_ab_group_add o
               ab_group_add_ordered_ab_group_add o
               ordered_ab_group_add_ordered_ab_group_add_abs o
               ordered_ab_group_add_abs_ordered_euclidean_space o
               ordered_euclidean_space_executable_euclidean_space)
              A_)
            (map (fn (b, m) =>
                   scaleR
                     ((scaleR_real_vector o real_vector_real_normed_vector o
                        real_normed_vector_real_inner o
                        real_inner_euclidean_space o
                        euclidean_space_ordered_euclidean_space o
                        ordered_euclidean_space_executable_euclidean_space)
                       A_)
                     m b)
              (zip (basis_list A_) (map fst mMs)));
        val u =
          listsuma
            ((monoid_add_group_add o group_add_ab_group_add o
               ab_group_add_ordered_ab_group_add o
               ordered_ab_group_add_ordered_ab_group_add_abs o
               ordered_ab_group_add_abs_ordered_euclidean_space o
               ordered_euclidean_space_executable_euclidean_space)
              A_)
            (map (fn (b, m) =>
                   scaleR
                     ((scaleR_real_vector o real_vector_real_normed_vector o
                        real_normed_vector_real_inner o
                        real_inner_euclidean_space o
                        euclidean_space_ordered_euclidean_space o
                        ordered_euclidean_space_executable_euclidean_space)
                       A_)
                     m b)
              (zip (basis_list A_) (map snd mMs)));
      in
        SOME (aform_of_ivl A_ l u)
      end);

fun inter_aform_plane E_ optns xs sctn =
  inter_aform_plane_ortho E_ (precision optns) xs (normal sctn) (pstn sctn);

fun aform_of_point A_ x = aform_of_ivl A_ x x;

fun next_section_turn_distance_factor_update next_section_turn_distance_factora
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = Options_ext
      (precision, tolerance, stepsize, iterations, halve_stepsizes,
        widening_mod, rk2_param, max_tdev_thres, presplit_summary_tolerance,
        collect_granularity, start_section, checkpoint_sections, stop_sections,
        safe_appr, snap_sections, min_section_distance,
        next_section_distance_factor,
        next_section_turn_distance_factora next_section_turn_distance_factor,
        printing_fun, irect_mod, result_fun, max_intersection_step,
        adaptive_atol, method_id, more);

fun next_section_distance_factor_update next_section_distance_factora
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = Options_ext
      (precision, tolerance, stepsize, iterations, halve_stepsizes,
        widening_mod, rk2_param, max_tdev_thres, presplit_summary_tolerance,
        collect_granularity, start_section, checkpoint_sections, stop_sections,
        safe_appr, snap_sections, min_section_distance,
        next_section_distance_factora next_section_distance_factor,
        next_section_turn_distance_factor, printing_fun, irect_mod, result_fun,
        max_intersection_step, adaptive_atol, method_id, more);

fun max_intersection_step_update max_intersection_stepa
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = Options_ext
      (precision, tolerance, stepsize, iterations, halve_stepsizes,
        widening_mod, rk2_param, max_tdev_thres, presplit_summary_tolerance,
        collect_granularity, start_section, checkpoint_sections, stop_sections,
        safe_appr, snap_sections, min_section_distance,
        next_section_distance_factor, next_section_turn_distance_factor,
        printing_fun, irect_mod, result_fun,
        max_intersection_stepa max_intersection_step, adaptive_atol, method_id,
        more);

fun collect_granularity_update collect_granularitya
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = Options_ext
      (precision, tolerance, stepsize, iterations, halve_stepsizes,
        widening_mod, rk2_param, max_tdev_thres, presplit_summary_tolerance,
        collect_granularitya collect_granularity, start_section,
        checkpoint_sections, stop_sections, safe_appr, snap_sections,
        min_section_distance, next_section_distance_factor,
        next_section_turn_distance_factor, printing_fun, irect_mod, result_fun,
        max_intersection_step, adaptive_atol, method_id, more);

fun max_tdev_thres_update max_tdev_thresa
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = Options_ext
      (precision, tolerance, stepsize, iterations, halve_stepsizes,
        widening_mod, rk2_param, max_tdev_thresa max_tdev_thres,
        presplit_summary_tolerance, collect_granularity, start_section,
        checkpoint_sections, stop_sections, safe_appr, snap_sections,
        min_section_distance, next_section_distance_factor,
        next_section_turn_distance_factor, printing_fun, irect_mod, result_fun,
        max_intersection_step, adaptive_atol, method_id, more);

fun start_section_update start_sectiona
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = Options_ext
      (precision, tolerance, stepsize, iterations, halve_stepsizes,
        widening_mod, rk2_param, max_tdev_thres, presplit_summary_tolerance,
        collect_granularity, start_sectiona start_section, checkpoint_sections,
        stop_sections, safe_appr, snap_sections, min_section_distance,
        next_section_distance_factor, next_section_turn_distance_factor,
        printing_fun, irect_mod, result_fun, max_intersection_step,
        adaptive_atol, method_id, more);

fun adaptive_atol_update adaptive_atola
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = Options_ext
      (precision, tolerance, stepsize, iterations, halve_stepsizes,
        widening_mod, rk2_param, max_tdev_thres, presplit_summary_tolerance,
        collect_granularity, start_section, checkpoint_sections, stop_sections,
        safe_appr, snap_sections, min_section_distance,
        next_section_distance_factor, next_section_turn_distance_factor,
        printing_fun, irect_mod, result_fun, max_intersection_step,
        adaptive_atola adaptive_atol, method_id, more);

fun one_prod A_ B_ = (one (one_zero_neq_one A_), one (one_zero_neq_one B_));

fun method_id_update method_ida
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = Options_ext
      (precision, tolerance, stepsize, iterations, halve_stepsizes,
        widening_mod, rk2_param, max_tdev_thres, presplit_summary_tolerance,
        collect_granularity, start_section, checkpoint_sections, stop_sections,
        safe_appr, snap_sections, min_section_distance,
        next_section_distance_factor, next_section_turn_distance_factor,
        printing_fun, irect_mod, result_fun, max_intersection_step,
        adaptive_atol, method_ida method_id, more);

fun print_rectangle (A1_, A2_) m i t0 x =
  let
    val _ = TextIO.print "rect: ";
    val _ = TextIO.print (int_to_string i);
    val _ = TextIO.print ": ";
    val _ = print_real t0;
  in
    (if equal_inta (mod_int i m) zero_inta
      then let
             val r =
               tdev (ordered_euclidean_space_executable_euclidean_space A1_)
                 (snd x);
             val _ = TextIO.print ": ";
             val _ =
               print_eucl A1_
                 (minus
                   ((minus_group_add o group_add_ab_group_add o
                      ab_group_add_ordered_ab_group_add o
                      ordered_ab_group_add_ordered_ab_group_add_abs o
                      ordered_ab_group_add_abs_ordered_euclidean_space o
                      ordered_euclidean_space_executable_euclidean_space)
                     A1_)
                   (fst x) r);
             val _ = TextIO.print " - ";
             val _ =
               print_eucl A1_
                 (plus ((plus_semigroup_add o semigroup_add_monoid_add o
                          monoid_add_group_add o group_add_ab_group_add o
                          ab_group_add_ordered_ab_group_add o
                          ordered_ab_group_add_ordered_ab_group_add_abs o
                          ordered_ab_group_add_abs_ordered_euclidean_space o
                          ordered_euclidean_space_executable_euclidean_space)
                         A1_)
                   (fst x) r);
             val _ = TextIO.print "; devs: ";
             val _ =
               TextIO.print
                 (int_to_string
                   (int_of_nat
                     (size_list
                       (list_of_pdevs
                         ((zero_monoid_add o monoid_add_group_add o
                            group_add_ab_group_add o
                            ab_group_add_ordered_ab_group_add o
                            ordered_ab_group_add_ordered_ab_group_add_abs o
                            ordered_ab_group_add_abs_ordered_euclidean_space o
                            ordered_euclidean_space_executable_euclidean_space)
                            A1_,
                           A2_)
                         (snd x)))));
             val _ = TextIO.print "; width: ";
             val _ = print_real (infnorm A1_ r);
             val _ = TextIO.print "; tdev: ";
             val _ = print_eucl A1_ r;
             val _ = TextIO.print "; maxdev: ";
             val _ = print_eucl A1_ (snd (max_pdev (A1_, A2_) (snd x)));
             val _ = println "";
           in
             ()
           end
      else println "")
  end;

fun constrain x y = ();

fun print_aform (A1_, A2_) x =
  let
    val _ = TextIO.print "aform(";
    val _ =
      TextIO.print (int_to_string (int_of_nat (size_list (basis_list A1_))));
    val _ = TextIO.print "): ";
    val _ = print_eucl A1_ (fst x);
    val _ = TextIO.print " -- ";
    val _ =
      map (fn (_, a) => print_eucl A1_ a)
        (list_of_pdevs
          ((zero_monoid_add o monoid_add_group_add o group_add_ab_group_add o
             ab_group_add_ordered_ab_group_add o
             ordered_ab_group_add_ordered_ab_group_add_abs o
             ordered_ab_group_add_abs_ordered_euclidean_space o
             ordered_euclidean_space_executable_euclidean_space)
             A1_,
            A2_)
          (snd x));
    val _ = println "";
  in
    ()
  end;

fun summarize_ivls (A1_, A2_) B_ C_ [] = NONE
  | summarize_ivls (A1_, A2_) B_ C_ (x :: xs) =
    (case summarize_ivls (A1_, A2_) B_ C_ xs of NONE => SOME x
      | SOME (t0, (cl, (cu, (t1, (xl, xu))))) =>
        let
          val (t0a, (cla, (cua, (t1a, (xla, xua))))) = x;
        in
          (if eq A1_ t0a t1
            then SOME (min A2_ t0a t0,
                        (inf B_ cla cl,
                          (sup C_ cua cu,
                            (max A2_ t1a t1,
                              ((if less_eq A2_ t1a t1 then xl else xla),
                                (if less_eq A2_ t1a t1 then xu else xua))))))
            else NONE)
        end);

fun ivls_of_aforms B_ D_ p ress =
  map (fn (t0, (cx, (t1, x))) =>
        (t0, (eucl_truncate_down B_ p
                (inf_aform
                  (ordered_euclidean_space_executable_euclidean_space B_) cx),
               (eucl_truncate_up B_ p
                  (sup_aform
                    (ordered_euclidean_space_executable_euclidean_space B_) cx),
                 (t1, (eucl_truncate_down D_ p
                         (inf_aform
                           (ordered_euclidean_space_executable_euclidean_space
                             D_)
                           x),
                        eucl_truncate_up D_ p
                          (sup_aform
                            (ordered_euclidean_space_executable_euclidean_space
                              D_)
                            x)))))))
    ress;

fun summarize_enclosure (A1_, A2_) B_ C_ p m xs =
  map_filter
    (fn x => (if uminus_funa uminus_bool is_none x then SOME (the x) else NONE))
    (map (summarize_ivls (A1_, A2_)
           ((inf_semilattice_inf o semilattice_inf_lattice o
              lattice_distrib_lattice o
              distrib_lattice_ordered_euclidean_space o
              ordered_euclidean_space_executable_euclidean_space)
             B_)
           ((sup_semilattice_sup o semilattice_sup_lattice o
              lattice_distrib_lattice o
              distrib_lattice_ordered_euclidean_space o
              ordered_euclidean_space_executable_euclidean_space)
             B_))
      (parts m (ivls_of_aforms B_ C_ p xs)));

fun ivls_result (D1_, D2_) E_ F_ p m =
  apsnd (summarize_enclosure (D1_, D2_) E_ F_ p m o snd) o snd;

fun lorenz_optns A_ B_ (C1_, C2_) (D1_, D2_) =
  Options_ext
    (nat_of_integer (53 : IntInf.int),
      Floatreal
        (Float
          (Int_of_integer (1 : IntInf.int),
            uminus_inta (Int_of_integer (4 : IntInf.int)))),
      Floatreal
        (Float
          (Int_of_integer (1 : IntInf.int),
            uminus_inta (Int_of_integer (8 : IntInf.int)))),
      nat_of_integer (40 : IntInf.int), nat_of_integer (10 : IntInf.int),
      nat_of_integer (40 : IntInf.int),
      Floatreal
        (Float
          (Int_of_integer (1 : IntInf.int),
            uminus_inta (Int_of_integer (1 : IntInf.int)))),
      Floatreal
        (Float
          (Int_of_integer (1 : IntInf.int),
            uminus_inta (Int_of_integer (3 : IntInf.int)))),
      Floatreal
        (Float
          (Int_of_integer (1 : IntInf.int),
            uminus_inta (Int_of_integer (2 : IntInf.int)))),
      Floatreal
        (Float
          (Int_of_integer (1 : IntInf.int),
            uminus_inta (Int_of_integer (3 : IntInf.int)))),
      Sctn ((zero A_, (zero B_, uminus C2_ (one C1_))),
             uminus_reala
               (divide_real
                 (divide_real
                   (divide_real
                     (Floatreal
                       (of_int ring_1_float
                         (Int_of_integer (215 : IntInf.int))))
                     (Floatreal
                       (of_int ring_1_float (Int_of_integer (2 : IntInf.int)))))
                   (Floatreal
                     (of_int ring_1_float (Int_of_integer (2 : IntInf.int)))))
                 (Floatreal
                   (of_int ring_1_float (Int_of_integer (2 : IntInf.int)))))),
      [Sctn ((zero A_, (zero B_, one C1_)),
              Floatreal
                (of_int ring_1_float (Int_of_integer (27 : IntInf.int))))],
      [Sctn ((zero A_, (zero B_, uminus C2_ (one C1_))),
              uminus_reala
                (Floatreal
                  (of_int ring_1_float (Int_of_integer (27 : IntInf.int))))),
        Sctn ((zero A_, (zero B_, uminus C2_ (one C1_))),
               Floatreal
                 (Float
                   (uminus_inta (Int_of_integer (25 : IntInf.int)),
                     uminus_inta (Int_of_integer (8 : IntInf.int)))))],
      (fn _ => true),
      divide_real
        (divide_real
          (divide_real
            (divide_real
              (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)))
              (Floatreal
                (of_int ring_1_float (Int_of_integer (2 : IntInf.int)))))
            (Floatreal (of_int ring_1_float (Int_of_integer (2 : IntInf.int)))))
          (Floatreal (of_int ring_1_float (Int_of_integer (2 : IntInf.int)))))
        (Floatreal (of_int ring_1_float (Int_of_integer (2 : IntInf.int)))),
      Floatreal (Float (zero_inta, zero_inta)),
      Floatreal (of_int ring_1_float (Int_of_integer (25 : IntInf.int))),
      Floatreal (Float (zero_inta, zero_inta)),
      let
        val re =
          print_rectangle (D1_, D2_) zero_inta zero_inta
            (Floatreal (Float (zero_inta, zero_inta)));
        val af = print_aform (D1_, D2_);
        val _ = constrain re af;
        val both = (fn c => let
                              val _ = re c;
                            in
                              af c
                            end);
      in
        both
      end,
      nat_of_integer (8 : IntInf.int),
      ivls_result (equal_real, ord_real) D1_ D1_
        (nat_of_integer (20 : IntInf.int)) (nat_of_integer (40 : IntInf.int)),
      Floatreal
        (Float
          (Int_of_integer (1 : IntInf.int),
            uminus_inta (Int_of_integer (10 : IntInf.int)))),
      Floatreal
        (Float
          (Int_of_integer (1 : IntInf.int),
            uminus_inta (Int_of_integer (30 : IntInf.int)))),
      nat_of_integer (2 : IntInf.int), ());

fun lorenzc_optns A_ (B1_, B2_) (C1_, C2_) (D1_, D2_) w m a r =
  method_id_update (fn _ => nat m)
    (max_intersection_step_update
      (fn _ =>
        Floatreal
          (Float
            (Int_of_integer (1 : IntInf.int),
              uminus_inta (Int_of_integer (2 : IntInf.int)))))
      (next_section_turn_distance_factor_update
        (fn _ =>
          (if not (equal_inta r zero_inta)
            then Floatreal (Float (zero_inta, zero_inta))
            else Floatreal
                   (Float
                     (Int_of_integer (1 : IntInf.int),
                       Int_of_integer (100 : IntInf.int)))))
        (next_section_distance_factor_update
          (fn _ =>
            (if not (equal_inta r zero_inta)
              then Floatreal
                     (of_int ring_1_float (Int_of_integer (100 : IntInf.int)))
              else Floatreal
                     (Float
                       (Int_of_integer (1 : IntInf.int),
                         Int_of_integer (100 : IntInf.int)))))
          (start_section_update
            (fn _ =>
              (if not (equal_inta r zero_inta)
                then Sctn ((zero A_,
                             (zero (zero_zero_neq_one B2_),
                               uminus C1_ (one (one_zero_neq_one C2_)))),
                            uminus_reala
                              (Floatreal
                                (of_int ring_1_float
                                  (Int_of_integer (24 : IntInf.int)))))
                else Sctn ((zero A_, uminus_proda B1_ C1_ (one_prod B2_ C2_)),
                            uminus_reala
                              (Floatreal
                                (Float
                                  (Int_of_integer (1 : IntInf.int),
                                    Int_of_integer (100 : IntInf.int)))))))
            (adaptive_atol_update
              (fn _ => Floatreal (Float (Int_of_integer (1 : IntInf.int), a)))
              (max_tdev_thres_update
                (fn _ => Floatreal (Float (Int_of_integer (1 : IntInf.int), w)))
                (collect_granularity_update
                  (fn _ =>
                    Floatreal (Float (Int_of_integer (1 : IntInf.int), w)))
                  (lorenz_optns A_ (zero_zero_neq_one B2_)
                    (one_zero_neq_one C2_, C1_) (D1_, D2_)))))))));

fun aform_sup_inner E_ optns x n =
  sup_aforma (precision optns) (inner_aform E_ x n);

fun aform_inf_inner E_ optns x n =
  inf_aforma (precision optns) (inner_aform E_ x n);

fun lorenz_dd x =
  (fn prec => fn thres => fn xa => fn xaa => fn xb => fn qs =>
    approx_euclarith_outer
      (executable_euclidean_space_prod
         (executable_euclidean_space_real, equal_real)
         (executable_euclidean_space_prod
            (executable_euclidean_space_real, equal_real)
            (executable_euclidean_space_real, equal_real),
           equal_prod equal_real equal_real),
        equal_prod equal_real (equal_prod equal_real equal_real))
      (executable_euclidean_space_prod
         (executable_euclidean_space_real, equal_real)
         (executable_euclidean_space_prod
            (executable_euclidean_space_real, equal_real)
            (executable_euclidean_space_real, equal_real),
           equal_prod equal_real equal_real),
        equal_prod equal_real (equal_prod equal_real equal_real))
      prec thres
      (AddE (ScaleR
               (Add (Mult (Add (Var (suc zero_nat,
                                      (Floatreal
 (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
(Floatreal (Float (zero_inta, zero_inta)),
  Floatreal (Float (zero_inta, zero_inta))))),
                                 Var (suc zero_nat,
                                       (Floatreal
  (Float (zero_inta, zero_inta)),
 (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
   Floatreal (Float (zero_inta, zero_inta)))))),
                            Add (Mult (Num
 (Floatreal
   (Float
     (Int_of_integer (4915166360050299 : IntInf.int),
       uminus_inta (Int_of_integer (51 : IntInf.int))))),
Var (suc (suc zero_nat),
      (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
        (Floatreal (Float (zero_inta, zero_inta)),
          Floatreal (Float (zero_inta, zero_inta)))))),
                                  Mult (Num
  (Floatreal
    (Float
      (uminus_inta (Int_of_integer (5777093055467152 : IntInf.int)),
        uminus_inta (Int_of_integer (52 : IntInf.int))))),
 Var (suc (suc zero_nat),
       (Floatreal (Float (zero_inta, zero_inta)),
         (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
           Floatreal (Float (zero_inta, zero_inta)))))))),
                      Mult (Add (Var (suc (suc zero_nat),
                                       (Floatreal
  (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
 (Floatreal (Float (zero_inta, zero_inta)),
   Floatreal (Float (zero_inta, zero_inta))))),
                                  Var (suc (suc zero_nat),
(Floatreal (Float (zero_inta, zero_inta)),
  (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
    Floatreal (Float (zero_inta, zero_inta)))))),
                             Add (Mult (Num
  (Floatreal
    (Float
      (Int_of_integer (4915166360050299 : IntInf.int),
        uminus_inta (Int_of_integer (51 : IntInf.int))))),
 Var (suc zero_nat,
       (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
         (Floatreal (Float (zero_inta, zero_inta)),
           Floatreal (Float (zero_inta, zero_inta)))))),
                                   Mult (Num
   (Floatreal
     (Float
       (uminus_inta (Int_of_integer (5777093055467152 : IntInf.int)),
         uminus_inta (Int_of_integer (52 : IntInf.int))))),
  Var (suc zero_nat,
        (Floatreal (Float (zero_inta, zero_inta)),
          (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
            Floatreal (Float (zero_inta, zero_inta))))))))),
                 (Floatreal (Float (zero_inta, zero_inta)),
                   (Floatreal (Float (zero_inta, zero_inta)),
                     Floatreal
                       (Float (Int_of_integer (1 : IntInf.int), zero_inta))))),
              AddE (ScaleR
                      (Mult (Num (Floatreal
                                   (Float
                                     (Int_of_integer
(5198143472295670 : IntInf.int),
                                       uminus_inta
 (Int_of_integer (54 : IntInf.int))))),
                              Add (Mult (Add
   (Var (suc zero_nat,
          (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
            (Floatreal (Float (zero_inta, zero_inta)),
              Floatreal (Float (zero_inta, zero_inta))))),
     Var (suc zero_nat,
           (Floatreal (Float (zero_inta, zero_inta)),
             (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
               Floatreal (Float (zero_inta, zero_inta)))))),
  Var (suc (suc zero_nat),
        (Floatreal (Float (zero_inta, zero_inta)),
          (Floatreal (Float (zero_inta, zero_inta)),
            Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)))))),
                                    Mult (Add
    (Var (suc (suc zero_nat),
           (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
             (Floatreal (Float (zero_inta, zero_inta)),
               Floatreal (Float (zero_inta, zero_inta))))),
      Var (suc (suc zero_nat),
            (Floatreal (Float (zero_inta, zero_inta)),
              (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
                Floatreal (Float (zero_inta, zero_inta)))))),
   Var (suc zero_nat,
         (Floatreal (Float (zero_inta, zero_inta)),
           (Floatreal (Float (zero_inta, zero_inta)),
             Floatreal
               (Float (Int_of_integer (1 : IntInf.int), zero_inta)))))))),
                        (Floatreal (Float (zero_inta, zero_inta)),
                          (Floatreal
                             (Float
                               (Int_of_integer (1 : IntInf.int), zero_inta)),
                            Floatreal (Float (zero_inta, zero_inta))))),
                     ScaleR
                       (Add (Mult (Minus (Num
   (Floatreal
     (Float
       (Int_of_integer (5198143472295670 : IntInf.int),
         uminus_inta (Int_of_integer (54 : IntInf.int)))))),
                                    Add (Mult
   (Add (Var (suc zero_nat,
               (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
                 (Floatreal (Float (zero_inta, zero_inta)),
                   Floatreal (Float (zero_inta, zero_inta))))),
          Var (suc zero_nat,
                (Floatreal (Float (zero_inta, zero_inta)),
                  (Floatreal
                     (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
                    Floatreal (Float (zero_inta, zero_inta)))))),
     Var (suc (suc zero_nat),
           (Floatreal (Float (zero_inta, zero_inta)),
             (Floatreal (Float (zero_inta, zero_inta)),
               Floatreal
                 (Float (Int_of_integer (1 : IntInf.int), zero_inta)))))),
  Mult (Add (Var (suc (suc zero_nat),
                   (Floatreal
                      (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
                     (Floatreal (Float (zero_inta, zero_inta)),
                       Floatreal (Float (zero_inta, zero_inta))))),
              Var (suc (suc zero_nat),
                    (Floatreal (Float (zero_inta, zero_inta)),
                      (Floatreal
                         (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
                        Floatreal (Float (zero_inta, zero_inta)))))),
         Var (suc zero_nat,
               (Floatreal (Float (zero_inta, zero_inta)),
                 (Floatreal (Float (zero_inta, zero_inta)),
                   Floatreal
                     (Float (Int_of_integer (1 : IntInf.int), zero_inta)))))))),
                              Mult (Num (Floatreal
  (Float (zero_inta, zero_inta))),
                                     Var (zero_nat,
   (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
     (Floatreal (Float (zero_inta, zero_inta)),
       Floatreal (Float (zero_inta, zero_inta))))))),
                         (Floatreal
                            (Float
                              (Int_of_integer (1 : IntInf.int), zero_inta)),
                           (Floatreal (Float (zero_inta, zero_inta)),
                             Floatreal (Float (zero_inta, zero_inta))))))))
      (xa :: xb :: xaa :: qs))
    x;

fun reduce_aform (E1_, E2_) optns x =
  apsnd (summarize_threshold (E1_, E2_) (precision optns)
          (presplit_summary_tolerance optns)
          (degree
            (E2_, (real_vector_real_normed_vector o
                    real_normed_vector_real_inner o real_inner_euclidean_space o
                    euclidean_space_ordered_euclidean_space o
                    ordered_euclidean_space_executable_euclidean_space)
                    E1_)
            (snd x)))
    x;

fun lorenz_d x =
  (fn prec => fn thres => fn xa => fn xaa => fn qs =>
    approx_euclarith_outer
      (executable_euclidean_space_prod
         (executable_euclidean_space_real, equal_real)
         (executable_euclidean_space_prod
            (executable_euclidean_space_real, equal_real)
            (executable_euclidean_space_real, equal_real),
           equal_prod equal_real equal_real),
        equal_prod equal_real (equal_prod equal_real equal_real))
      (executable_euclidean_space_prod
         (executable_euclidean_space_real, equal_real)
         (executable_euclidean_space_prod
            (executable_euclidean_space_real, equal_real)
            (executable_euclidean_space_real, equal_real),
           equal_prod equal_real equal_real),
        equal_prod equal_real (equal_prod equal_real equal_real))
      prec thres
      (AddE (ScaleR
               (Add (Mult (Num (Floatreal
                                 (Float
                                   (uminus_inta
                                      (Int_of_integer
(6004799503160661 : IntInf.int)),
                                     uminus_inta
                                       (Int_of_integer (51 : IntInf.int))))),
                            Var (suc zero_nat,
                                  (Floatreal (Float (zero_inta, zero_inta)),
                                    (Floatreal (Float (zero_inta, zero_inta)),
                                      Floatreal
(Float (Int_of_integer (1 : IntInf.int), zero_inta)))))),
                      Add (Mult (Add (Var
(zero_nat,
  (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
    (Floatreal (Float (zero_inta, zero_inta)),
      Floatreal (Float (zero_inta, zero_inta))))),
                                       Var
 (zero_nat,
   (Floatreal (Float (zero_inta, zero_inta)),
     (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
       Floatreal (Float (zero_inta, zero_inta)))))),
                                  Add (Mult
 (Num (Floatreal
        (Float
          (Int_of_integer (4915166360050299 : IntInf.int),
            uminus_inta (Int_of_integer (51 : IntInf.int))))),
   Var (suc zero_nat,
         (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
           (Floatreal (Float (zero_inta, zero_inta)),
             Floatreal (Float (zero_inta, zero_inta)))))),
Mult (Num (Floatreal
            (Float
              (uminus_inta (Int_of_integer (5777093055467152 : IntInf.int)),
                uminus_inta (Int_of_integer (52 : IntInf.int))))),
       Var (suc zero_nat,
             (Floatreal (Float (zero_inta, zero_inta)),
               (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
                 Floatreal (Float (zero_inta, zero_inta)))))))),
                            Mult (Add (Var
 (suc zero_nat,
   (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
     (Floatreal (Float (zero_inta, zero_inta)),
       Floatreal (Float (zero_inta, zero_inta))))),
Var (suc zero_nat,
      (Floatreal (Float (zero_inta, zero_inta)),
        (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
          Floatreal (Float (zero_inta, zero_inta)))))),
                                   Add (Mult
  (Num (Floatreal
         (Float
           (Int_of_integer (4915166360050299 : IntInf.int),
             uminus_inta (Int_of_integer (51 : IntInf.int))))),
    Var (zero_nat,
          (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
            (Floatreal (Float (zero_inta, zero_inta)),
              Floatreal (Float (zero_inta, zero_inta)))))),
 Mult (Num (Floatreal
             (Float
               (uminus_inta (Int_of_integer (5777093055467152 : IntInf.int)),
                 uminus_inta (Int_of_integer (52 : IntInf.int))))),
        Var (zero_nat,
              (Floatreal (Float (zero_inta, zero_inta)),
                (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
                  Floatreal (Float (zero_inta, zero_inta)))))))))),
                 (Floatreal (Float (zero_inta, zero_inta)),
                   (Floatreal (Float (zero_inta, zero_inta)),
                     Floatreal
                       (Float (Int_of_integer (1 : IntInf.int), zero_inta))))),
              AddE (ScaleR
                      (Add (Mult (Num (Floatreal
(Float
  (uminus_inta (Int_of_integer (6425432926773530 : IntInf.int)),
    uminus_inta (Int_of_integer (48 : IntInf.int))))),
                                   Var (suc zero_nat,
 (Floatreal (Float (zero_inta, zero_inta)),
   (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
     Floatreal (Float (zero_inta, zero_inta)))))),
                             Add (Mult (Mult
  (Num (Floatreal
         (Float
           (Int_of_integer (5198143472295670 : IntInf.int),
             uminus_inta (Int_of_integer (54 : IntInf.int))))),
    Add (Var (zero_nat,
               (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
                 (Floatreal (Float (zero_inta, zero_inta)),
                   Floatreal (Float (zero_inta, zero_inta))))),
          Var (zero_nat,
                (Floatreal (Float (zero_inta, zero_inta)),
                  (Floatreal
                     (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
                    Floatreal (Float (zero_inta, zero_inta))))))),
 Var (suc zero_nat,
       (Floatreal (Float (zero_inta, zero_inta)),
         (Floatreal (Float (zero_inta, zero_inta)),
           Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)))))),
                                   Mult (Mult
   (Num (Floatreal
          (Float
            (Int_of_integer (5198143472295670 : IntInf.int),
              uminus_inta (Int_of_integer (54 : IntInf.int))))),
     Add (Var (suc zero_nat,
                (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
                  (Floatreal (Float (zero_inta, zero_inta)),
                    Floatreal (Float (zero_inta, zero_inta))))),
           Var (suc zero_nat,
                 (Floatreal (Float (zero_inta, zero_inta)),
                   (Floatreal
                      (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
                     Floatreal (Float (zero_inta, zero_inta))))))),
  Var (zero_nat,
        (Floatreal (Float (zero_inta, zero_inta)),
          (Floatreal (Float (zero_inta, zero_inta)),
            Floatreal
              (Float (Int_of_integer (1 : IntInf.int), zero_inta)))))))),
                        (Floatreal (Float (zero_inta, zero_inta)),
                          (Floatreal
                             (Float
                               (Int_of_integer (1 : IntInf.int), zero_inta)),
                            Floatreal (Float (zero_inta, zero_inta))))),
                     ScaleR
                       (Add (Mult (Num (Floatreal
 (Float
   (Int_of_integer (6658416365912628 : IntInf.int),
     uminus_inta (Int_of_integer (49 : IntInf.int))))),
                                    Var (suc zero_nat,
  (Floatreal (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
    (Floatreal (Float (zero_inta, zero_inta)),
      Floatreal (Float (zero_inta, zero_inta)))))),
                              Minus (Add (Mult
    (Mult (Num (Floatreal
                 (Float
                   (Int_of_integer (5198143472295670 : IntInf.int),
                     uminus_inta (Int_of_integer (54 : IntInf.int))))),
            Add (Var (zero_nat,
                       (Floatreal
                          (Float (Int_of_integer (1 : IntInf.int), zero_inta)),
                         (Floatreal (Float (zero_inta, zero_inta)),
                           Floatreal (Float (zero_inta, zero_inta))))),
                  Var (zero_nat,
                        (Floatreal (Float (zero_inta, zero_inta)),
                          (Floatreal
                             (Float
                               (Int_of_integer (1 : IntInf.int), zero_inta)),
                            Floatreal (Float (zero_inta, zero_inta))))))),
      Var (suc zero_nat,
            (Floatreal (Float (zero_inta, zero_inta)),
              (Floatreal (Float (zero_inta, zero_inta)),
                Floatreal
                  (Float (Int_of_integer (1 : IntInf.int), zero_inta)))))),
   Mult (Mult (Num (Floatreal
                     (Float
                       (Int_of_integer (5198143472295670 : IntInf.int),
                         uminus_inta (Int_of_integer (54 : IntInf.int))))),
                Add (Var (suc zero_nat,
                           (Floatreal
                              (Float
                                (Int_of_integer (1 : IntInf.int), zero_inta)),
                             (Floatreal (Float (zero_inta, zero_inta)),
                               Floatreal (Float (zero_inta, zero_inta))))),
                      Var (suc zero_nat,
                            (Floatreal (Float (zero_inta, zero_inta)),
                              (Floatreal
                                 (Float
                                   (Int_of_integer (1 : IntInf.int),
                                     zero_inta)),
                                Floatreal (Float (zero_inta, zero_inta))))))),
          Var (zero_nat,
                (Floatreal (Float (zero_inta, zero_inta)),
                  (Floatreal (Float (zero_inta, zero_inta)),
                    Floatreal
                      (Float
                        (Int_of_integer (1 : IntInf.int), zero_inta))))))))),
                         (Floatreal
                            (Float
                              (Int_of_integer (1 : IntInf.int), zero_inta)),
                           (Floatreal (Float (zero_inta, zero_inta)),
                             Floatreal (Float (zero_inta, zero_inta))))))))
      (xa :: xaa :: qs))
    x;

fun width_aform (F1_, F2_) optns x =
  let
    val t = tdeva (F1_, F2_) (precision optns) (snd x);
  in
    listsum executable_euclidean_space_real (precision optns)
      (map (inner
             ((real_inner_euclidean_space o
                euclidean_space_ordered_euclidean_space o
                ordered_euclidean_space_executable_euclidean_space)
               F1_)
             t)
        (basis_list F1_))
  end;

fun independent_aform (A1_, A2_) B_ x y =
  msum_aform B_ (degree (A1_, A2_) (snd x))
    (zero ((zero_monoid_add o monoid_add_group_add o group_add_ab_group_add o
             ab_group_add_real_vector)
            B_),
      zero_pdevs
        ((zero_monoid_add o monoid_add_group_add o group_add_ab_group_add o
           ab_group_add_real_vector)
          B_))
    y;

fun lorenzc w m a r x ex y ey u eu =
  poincare_distance_d_dres
    (executable_euclidean_space_prod
       (executable_euclidean_space_real, equal_real)
       (executable_euclidean_space_prod
          (executable_euclidean_space_real, equal_real)
          (executable_euclidean_space_real, equal_real),
         equal_prod equal_real equal_real),
      equal_prod equal_real (equal_prod equal_real equal_real))
    (equal_prod (equal_prod equal_real (equal_prod equal_real equal_real))
      (equal_pdevs
        (zero_prod zero_real (zero_prod zero_real zero_real),
          equal_prod equal_real (equal_prod equal_real equal_real))))
    (aform_of_ivl
      (executable_euclidean_space_prod
        (executable_euclidean_space_real, equal_real)
        (executable_euclidean_space_prod
           (executable_euclidean_space_real, equal_real)
           (executable_euclidean_space_real, equal_real),
          equal_prod equal_real equal_real)))
    (fn xa =>
      msum_aform
        (real_vector_prod real_vector_real
          (real_vector_prod real_vector_real real_vector_real))
        (degree
          (equal_prod equal_real (equal_prod equal_real equal_real),
            real_vector_prod real_vector_real
              (real_vector_prod real_vector_real real_vector_real))
          (snd xa))
        xa)
    (inf_aform
      (ordered_euclidean_space_prod (equal_real, ordered_euclidean_space_real)
        (equal_prod equal_real equal_real,
          ordered_euclidean_space_prod
            (equal_real, ordered_euclidean_space_real)
            (equal_real, ordered_euclidean_space_real))))
    (sup_aform
      (ordered_euclidean_space_prod (equal_real, ordered_euclidean_space_real)
        (equal_prod equal_real equal_real,
          ordered_euclidean_space_prod
            (equal_real, ordered_euclidean_space_real)
            (equal_real, ordered_euclidean_space_real))))
    (fn xa =>
      add_aform_componentwise
        (executable_euclidean_space_prod
           (executable_euclidean_space_real, equal_real)
           (executable_euclidean_space_prod
              (executable_euclidean_space_real, equal_real)
              (executable_euclidean_space_real, equal_real),
             equal_prod equal_real equal_real),
          equal_prod equal_real (equal_prod equal_real equal_real))
        (precision xa) (tolerance xa))
    (fn xa =>
      scaleQ_aform_componentwise
        (executable_euclidean_space_prod
           (executable_euclidean_space_real, equal_real)
           (executable_euclidean_space_prod
              (executable_euclidean_space_real, equal_real)
              (executable_euclidean_space_real, equal_real),
             equal_prod equal_real equal_real),
          equal_prod equal_real (equal_prod equal_real equal_real))
        (precision xa) (tolerance xa))
    (fn xa =>
      scaleR_aform_ivl
        (executable_euclidean_space_prod
           (executable_euclidean_space_real, equal_real)
           (executable_euclidean_space_prod
              (executable_euclidean_space_real, equal_real)
              (executable_euclidean_space_real, equal_real),
             equal_prod equal_real equal_real),
          equal_prod equal_real (equal_prod equal_real equal_real))
        (precision xa) (tolerance xa))
    (split_aform_largest
      (executable_euclidean_space_prod
         (executable_euclidean_space_real, equal_real)
         (executable_euclidean_space_prod
            (executable_euclidean_space_real, equal_real)
            (executable_euclidean_space_real, equal_real),
           equal_prod equal_real equal_real),
        equal_prod equal_real (equal_prod equal_real equal_real)))
    (aform_inf_inner
      (executable_euclidean_space_prod
        (executable_euclidean_space_real, equal_real)
        (executable_euclidean_space_prod
           (executable_euclidean_space_real, equal_real)
           (executable_euclidean_space_real, equal_real),
          equal_prod equal_real equal_real)))
    (aform_sup_inner
      (executable_euclidean_space_prod
        (executable_euclidean_space_real, equal_real)
        (executable_euclidean_space_prod
           (executable_euclidean_space_real, equal_real)
           (executable_euclidean_space_real, equal_real),
          equal_prod equal_real equal_real)))
    (inter_aform_plane
      (executable_euclidean_space_prod
        (executable_euclidean_space_real, equal_real)
        (executable_euclidean_space_prod
           (executable_euclidean_space_real, equal_real)
           (executable_euclidean_space_real, equal_real),
          equal_prod equal_real equal_real)))
    (reduce_aform
      (executable_euclidean_space_prod
         (executable_euclidean_space_real, equal_real)
         (executable_euclidean_space_prod
            (executable_euclidean_space_real, equal_real)
            (executable_euclidean_space_real, equal_real),
           equal_prod equal_real equal_real),
        equal_prod equal_real (equal_prod equal_real equal_real)))
    (independent_aform
      (equal_prod equal_real (equal_prod equal_real equal_real),
        real_vector_prod real_vector_real
          (real_vector_prod real_vector_real real_vector_real))
      (real_vector_prod real_vector_real
        (real_vector_prod real_vector_real real_vector_real)))
    (width_aform
      (executable_euclidean_space_prod
         (executable_euclidean_space_real, equal_real)
         (executable_euclidean_space_prod
            (executable_euclidean_space_real, equal_real)
            (executable_euclidean_space_real, equal_real),
           equal_prod equal_real equal_real),
        equal_prod equal_real (equal_prod equal_real equal_real)))
    (fn optns => fn args =>
      lorenz (precision optns) (tolerance optns) (hd args) (tl args))
    (fn optns => fn args =>
      lorenz_d (precision optns) (tolerance optns) (hd args) (hd (tl args))
        (tl (tl args)))
    (fn optns => fn args =>
      lorenz_dd (precision optns) (tolerance optns) (hd args) (hd (tl args))
        (hd (tl (tl args))) (tl (tl (tl args))))
    (lorenzc_optns zero_real (uminus_real, zero_neq_one_real)
      (uminus_real, zero_neq_one_real)
      (executable_euclidean_space_prod
         (executable_euclidean_space_real, equal_real)
         (executable_euclidean_space_prod
            (executable_euclidean_space_real, equal_real)
            (executable_euclidean_space_real, equal_real),
           equal_prod equal_real equal_real),
        equal_prod equal_real (equal_prod equal_real equal_real))
      w m a r)
    [msum_aform
       (real_vector_prod real_vector_real
         (real_vector_prod real_vector_real real_vector_real))
       (nat_of_integer (53 : IntInf.int))
       (aform_of_point
         (executable_euclidean_space_prod
           (executable_euclidean_space_real, equal_real)
           (executable_euclidean_space_prod
              (executable_euclidean_space_real, equal_real)
              (executable_euclidean_space_real, equal_real),
             equal_prod equal_real equal_real))
         (decimal (Floatreal (of_int ring_1_float x)) ex,
           (decimal (Floatreal (of_int ring_1_float y)) ey,
             Floatreal
               (of_int ring_1_float (Int_of_integer (27 : IntInf.int))))))
       (aform_of_ivl
         (executable_euclidean_space_prod
           (executable_euclidean_space_real, equal_real)
           (executable_euclidean_space_prod
              (executable_euclidean_space_real, equal_real)
              (executable_euclidean_space_real, equal_real),
             equal_prod equal_real equal_real))
         (zero_proda zero_real (zero_prod zero_real zero_real))
         (decimal (Floatreal (of_int ring_1_float u)) eu,
           (decimal (Floatreal (of_int ring_1_float u)) eu,
             Floatreal (Float (zero_inta, zero_inta)))))];

fun irect_mod
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = irect_mod;

fun appr_of_irect A_ appr_of_ivl optns is =
  appr_of_ivl
    (listsuma
      ((monoid_add_group_add o group_add_ab_group_add o
         ab_group_add_ordered_ab_group_add o
         ordered_ab_group_add_ordered_ab_group_add_abs o
         ordered_ab_group_add_abs_ordered_euclidean_space o
         ordered_euclidean_space_executable_euclidean_space)
        A_)
      (map (fn (i, a) =>
             scaleR
               ((scaleR_real_vector o real_vector_real_normed_vector o
                  real_normed_vector_real_inner o real_inner_euclidean_space o
                  euclidean_space_ordered_euclidean_space o
                  ordered_euclidean_space_executable_euclidean_space)
                 A_)
               (Floatreal
                 (Float (i, uminus_inta (int_of_nat (irect_mod optns)))))
               a)
        (zip is (basis_list A_))))
    (listsuma
      ((monoid_add_group_add o group_add_ab_group_add o
         ab_group_add_ordered_ab_group_add o
         ordered_ab_group_add_ordered_ab_group_add_abs o
         ordered_ab_group_add_abs_ordered_euclidean_space o
         ordered_euclidean_space_executable_euclidean_space)
        A_)
      (map (fn (i, a) =>
             scaleR
               ((scaleR_real_vector o real_vector_real_normed_vector o
                  real_normed_vector_real_inner o real_inner_euclidean_space o
                  euclidean_space_ordered_euclidean_space o
                  ordered_euclidean_space_executable_euclidean_space)
                 A_)
               (Floatreal
                 (Float
                   (plus_inta i (Int_of_integer (1 : IntInf.int)),
                     uminus_inta (int_of_nat (irect_mod optns)))))
               a)
        (zip is (basis_list A_))));

fun project_appr A_ appr_of_ivl inf_of_appr sup_of_appr x b y =
  let
    val i = inf_of_appr x;
    val s = sup_of_appr x;
  in
    appr_of_ivl
      (plus ((plus_semigroup_add o semigroup_add_monoid_add o
               monoid_add_group_add o group_add_ab_group_add o
               ab_group_add_ordered_ab_group_add o
               ordered_ab_group_add_ordered_ab_group_add_abs o
               ordered_ab_group_add_abs_ordered_euclidean_space o
               ordered_euclidean_space_executable_euclidean_space)
              A_)
        i (scaleR
            ((scaleR_real_vector o real_vector_real_normed_vector o
               real_normed_vector_real_inner o real_inner_euclidean_space o
               euclidean_space_ordered_euclidean_space o
               ordered_euclidean_space_executable_euclidean_space)
              A_)
            (minus_reala y
              (inner
                ((real_inner_euclidean_space o
                   euclidean_space_ordered_euclidean_space o
                   ordered_euclidean_space_executable_euclidean_space)
                  A_)
                i b))
            b))
      (plus ((plus_semigroup_add o semigroup_add_monoid_add o
               monoid_add_group_add o group_add_ab_group_add o
               ab_group_add_ordered_ab_group_add o
               ordered_ab_group_add_ordered_ab_group_add_abs o
               ordered_ab_group_add_abs_ordered_euclidean_space o
               ordered_euclidean_space_executable_euclidean_space)
              A_)
        s (scaleR
            ((scaleR_real_vector o real_vector_real_normed_vector o
               real_normed_vector_real_inner o real_inner_euclidean_space o
               euclidean_space_ordered_euclidean_space o
               ordered_euclidean_space_executable_euclidean_space)
              A_)
            (minus_reala y
              (inner
                ((real_inner_euclidean_space o
                   euclidean_space_ordered_euclidean_space o
                   ordered_euclidean_space_executable_euclidean_space)
                  A_)
                s b))
            b))
  end;

fun poincare_irects_dres (A1_, A2_) B_ appr_of_ivl msum_appr inf_of_appr
  sup_of_appr add_appr scale_appr scale_appr_ivl split_appr appr_inf_inner
  appr_sup_inner inter_appr_plane reduce_appr independent_appr width_appr
  ode_approx ode_d_approx ode_d2_approx optns is =
  dbind (poincare_distance_d_dres (A1_, A2_) B_ appr_of_ivl msum_appr
          inf_of_appr sup_of_appr add_appr scale_appr scale_appr_ivl split_appr
          appr_inf_inner appr_sup_inner inter_appr_plane reduce_appr
          independent_appr width_appr ode_approx ode_d_approx ode_d2_approx
          optns [appr_of_irect A1_ appr_of_ivl optns is])
    (fn x =>
      DRETURN
        (maps (fn (a, b) =>
                map (fn aa =>
                      project_appr A1_ appr_of_ivl inf_of_appr sup_of_appr aa
                        (normal b) (pstn b))
                  a)
          x));

fun floor_real (Floatreal x) = int_floor_fl x;

fun irects_of_appr B_ inf_of_appr sup_of_appr optns x =
  let
    val i = inf_of_appr x;
    val s = sup_of_appr x;
    val i0s =
      map (fn b =>
            floor_real
              (times_reala
                (inner
                  ((real_inner_euclidean_space o
                     euclidean_space_ordered_euclidean_space o
                     ordered_euclidean_space_executable_euclidean_space)
                    B_)
                  i b)
                (powera power_real
                  (Floatreal
                    (of_int ring_1_float (Int_of_integer (2 : IntInf.int))))
                  (irect_mod optns))))
        (basis_list B_);
    val s0s =
      map (fn b =>
            floor_real
              (times_reala
                (inner
                  ((real_inner_euclidean_space o
                     euclidean_space_ordered_euclidean_space o
                     ordered_euclidean_space_executable_euclidean_space)
                    B_)
                  s b)
                (powera power_real
                  (Floatreal
                    (of_int ring_1_float (Int_of_integer (2 : IntInf.int))))
                  (irect_mod optns))))
        (basis_list B_);
  in
    product_lists (map (fn (a, b) => upto a b) (zip i0s s0s))
  end;

fun irects_of_apprs B_ inf_of_appr sup_of_appr optns xs =
  remdups (equal_list equal_int)
    (maps (irects_of_appr B_ inf_of_appr sup_of_appr optns) xs);

fun print_irects irects =
  let
    val _ =
      map (fn is =>
            let
              val _ =
                map (fn j =>
                      let
                        val _ = TextIO.print (int_to_string j);
                      in
                        TextIO.print " "
                      end)
                  is;
            in
              println ""
            end)
        irects;
  in
    ()
  end;

fun mirror_irects (A1_, A2_, A3_, A4_) =
  map (fn a =>
        (case a of [] => [] | [i] => [i] | [i, j] => [i, j]
          | [i, j, k] =>
            [(if less A4_ j (zero A3_) then uminus A2_ i else i), abs A1_ j, k]
          | i :: j :: k :: af :: lista => i :: j :: k :: af :: lista));

fun irect_mod_update irect_moda
  (Options_ext
    (precision, tolerance, stepsize, iterations, halve_stepsizes, widening_mod,
      rk2_param, max_tdev_thres, presplit_summary_tolerance,
      collect_granularity, start_section, checkpoint_sections, stop_sections,
      safe_appr, snap_sections, min_section_distance,
      next_section_distance_factor, next_section_turn_distance_factor,
      printing_fun, irect_mod, result_fun, max_intersection_step, adaptive_atol,
      method_id, more))
  = Options_ext
      (precision, tolerance, stepsize, iterations, halve_stepsizes,
        widening_mod, rk2_param, max_tdev_thres, presplit_summary_tolerance,
        collect_granularity, start_section, checkpoint_sections, stop_sections,
        safe_appr, snap_sections, min_section_distance,
        next_section_distance_factor, next_section_turn_distance_factor,
        printing_fun, irect_moda irect_mod, result_fun, max_intersection_step,
        adaptive_atol, method_id, more);

fun lorenz_optnsa A_ B_ (C1_, C2_) (D1_, D2_) p w =
  adaptive_atol_update
    (fn _ =>
      Floatreal
        (Float
          (Int_of_integer (1 : IntInf.int),
            uminus_inta
              (int_of_nat (times_nat w (nat_of_integer (2 : IntInf.int)))))))
    (max_tdev_thres_update
      (fn _ =>
        Floatreal
          (Float (Int_of_integer (2 : IntInf.int), uminus_inta (int_of_nat w))))
      (collect_granularity_update
        (fn _ =>
          Floatreal
            (Float
              (Int_of_integer (2 : IntInf.int), uminus_inta (int_of_nat w))))
        (irect_mod_update (fn _ => p)
          (lorenz_optns A_ B_ (C1_, C2_) (D1_, D2_)))));

fun lorenz_irects p w i j =
  let
    val optns =
      lorenz_optnsa zero_real zero_real (one_real, uminus_real)
        (executable_euclidean_space_prod
           (executable_euclidean_space_real, equal_real)
           (executable_euclidean_space_prod
              (executable_euclidean_space_real, equal_real)
              (executable_euclidean_space_real, equal_real),
             equal_prod equal_real equal_real),
          equal_prod equal_real (equal_prod equal_real equal_real))
        p w;
  in
    dbind (poincare_irects_dres
            (executable_euclidean_space_prod
               (executable_euclidean_space_real, equal_real)
               (executable_euclidean_space_prod
                  (executable_euclidean_space_real, equal_real)
                  (executable_euclidean_space_real, equal_real),
                 equal_prod equal_real equal_real),
              equal_prod equal_real (equal_prod equal_real equal_real))
            (equal_prod
              (equal_prod equal_real (equal_prod equal_real equal_real))
              (equal_pdevs
                (zero_prod zero_real (zero_prod zero_real zero_real),
                  equal_prod equal_real (equal_prod equal_real equal_real))))
            (aform_of_ivl
              (executable_euclidean_space_prod
                (executable_euclidean_space_real, equal_real)
                (executable_euclidean_space_prod
                   (executable_euclidean_space_real, equal_real)
                   (executable_euclidean_space_real, equal_real),
                  equal_prod equal_real equal_real)))
            (fn x =>
              msum_aform
                (real_vector_prod real_vector_real
                  (real_vector_prod real_vector_real real_vector_real))
                (degree
                  (equal_prod equal_real (equal_prod equal_real equal_real),
                    real_vector_prod real_vector_real
                      (real_vector_prod real_vector_real real_vector_real))
                  (snd x))
                x)
            (inf_aform
              (ordered_euclidean_space_prod
                (equal_real, ordered_euclidean_space_real)
                (equal_prod equal_real equal_real,
                  ordered_euclidean_space_prod
                    (equal_real, ordered_euclidean_space_real)
                    (equal_real, ordered_euclidean_space_real))))
            (sup_aform
              (ordered_euclidean_space_prod
                (equal_real, ordered_euclidean_space_real)
                (equal_prod equal_real equal_real,
                  ordered_euclidean_space_prod
                    (equal_real, ordered_euclidean_space_real)
                    (equal_real, ordered_euclidean_space_real))))
            (fn x =>
              add_aform_componentwise
                (executable_euclidean_space_prod
                   (executable_euclidean_space_real, equal_real)
                   (executable_euclidean_space_prod
                      (executable_euclidean_space_real, equal_real)
                      (executable_euclidean_space_real, equal_real),
                     equal_prod equal_real equal_real),
                  equal_prod equal_real (equal_prod equal_real equal_real))
                (precision x) (tolerance x))
            (fn x =>
              scaleQ_aform_componentwise
                (executable_euclidean_space_prod
                   (executable_euclidean_space_real, equal_real)
                   (executable_euclidean_space_prod
                      (executable_euclidean_space_real, equal_real)
                      (executable_euclidean_space_real, equal_real),
                     equal_prod equal_real equal_real),
                  equal_prod equal_real (equal_prod equal_real equal_real))
                (precision x) (tolerance x))
            (fn x =>
              scaleR_aform_ivl
                (executable_euclidean_space_prod
                   (executable_euclidean_space_real, equal_real)
                   (executable_euclidean_space_prod
                      (executable_euclidean_space_real, equal_real)
                      (executable_euclidean_space_real, equal_real),
                     equal_prod equal_real equal_real),
                  equal_prod equal_real (equal_prod equal_real equal_real))
                (precision x) (tolerance x))
            (split_aform_largest
              (executable_euclidean_space_prod
                 (executable_euclidean_space_real, equal_real)
                 (executable_euclidean_space_prod
                    (executable_euclidean_space_real, equal_real)
                    (executable_euclidean_space_real, equal_real),
                   equal_prod equal_real equal_real),
                equal_prod equal_real (equal_prod equal_real equal_real)))
            (aform_inf_inner
              (executable_euclidean_space_prod
                (executable_euclidean_space_real, equal_real)
                (executable_euclidean_space_prod
                   (executable_euclidean_space_real, equal_real)
                   (executable_euclidean_space_real, equal_real),
                  equal_prod equal_real equal_real)))
            (aform_sup_inner
              (executable_euclidean_space_prod
                (executable_euclidean_space_real, equal_real)
                (executable_euclidean_space_prod
                   (executable_euclidean_space_real, equal_real)
                   (executable_euclidean_space_real, equal_real),
                  equal_prod equal_real equal_real)))
            (inter_aform_plane
              (executable_euclidean_space_prod
                (executable_euclidean_space_real, equal_real)
                (executable_euclidean_space_prod
                   (executable_euclidean_space_real, equal_real)
                   (executable_euclidean_space_real, equal_real),
                  equal_prod equal_real equal_real)))
            (reduce_aform
              (executable_euclidean_space_prod
                 (executable_euclidean_space_real, equal_real)
                 (executable_euclidean_space_prod
                    (executable_euclidean_space_real, equal_real)
                    (executable_euclidean_space_real, equal_real),
                   equal_prod equal_real equal_real),
                equal_prod equal_real (equal_prod equal_real equal_real)))
            (independent_aform
              (equal_prod equal_real (equal_prod equal_real equal_real),
                real_vector_prod real_vector_real
                  (real_vector_prod real_vector_real real_vector_real))
              (real_vector_prod real_vector_real
                (real_vector_prod real_vector_real real_vector_real)))
            (width_aform
              (executable_euclidean_space_prod
                 (executable_euclidean_space_real, equal_real)
                 (executable_euclidean_space_prod
                    (executable_euclidean_space_real, equal_real)
                    (executable_euclidean_space_real, equal_real),
                   equal_prod equal_real equal_real),
                equal_prod equal_real (equal_prod equal_real equal_real)))
            (fn optnsa => fn args =>
              lorenz (precision optnsa) (tolerance optnsa) (hd args) (tl args))
            (fn optnsa => fn args =>
              lorenz_d (precision optnsa) (tolerance optnsa) (hd args)
                (hd (tl args)) (tl (tl args)))
            (fn optnsa => fn args =>
              lorenz_dd (precision optnsa) (tolerance optnsa) (hd args)
                (hd (tl args)) (hd (tl (tl args))) (tl (tl (tl args))))
            optns
            [i, j,
              times_inta (Int_of_integer (27 : IntInf.int))
                (powera power_int (Int_of_integer (2 : IntInf.int)) p)])
      (fn stops =>
        let
          val (returns, aborted) =
            partition
              (fn x =>
                equal_reala
                  (snd (snd (inf_aform
                              (ordered_euclidean_space_prod
                                (equal_real, ordered_euclidean_space_real)
                                (equal_prod equal_real equal_real,
                                  ordered_euclidean_space_prod
                                    (equal_real, ordered_euclidean_space_real)
                                    (equal_real, ordered_euclidean_space_real)))
                              x)))
                  (Floatreal
                    (of_int ring_1_float (Int_of_integer (27 : IntInf.int)))))
              stops;
          val irects =
            irects_of_apprs
              (executable_euclidean_space_prod
                (executable_euclidean_space_real, equal_real)
                (executable_euclidean_space_prod
                   (executable_euclidean_space_real, equal_real)
                   (executable_euclidean_space_real, equal_real),
                  equal_prod equal_real equal_real))
              (inf_aform
                (ordered_euclidean_space_prod
                  (equal_real, ordered_euclidean_space_real)
                  (equal_prod equal_real equal_real,
                    ordered_euclidean_space_prod
                      (equal_real, ordered_euclidean_space_real)
                      (equal_real, ordered_euclidean_space_real))))
              (sup_aform
                (ordered_euclidean_space_prod
                  (equal_real, ordered_euclidean_space_real)
                  (equal_prod equal_real equal_real,
                    ordered_euclidean_space_prod
                      (equal_real, ordered_euclidean_space_real)
                      (equal_real, ordered_euclidean_space_real))))
              optns returns;
          val irectsa =
            mirror_irects (abs_int, uminus_int, zero_int, ord_int) irects;
          val _ =
            (if less_nat zero_nat (size_list aborted)
              then let
                     val _ = println "= Aborted close to the origin: ";
                     val ivl_abort =
                       ivl_of_apprs
                         (executable_euclidean_space_prod
                           (executable_euclidean_space_real, equal_real)
                           (executable_euclidean_space_prod
                              (executable_euclidean_space_real, equal_real)
                              (executable_euclidean_space_real, equal_real),
                             equal_prod equal_real equal_real))
                         (aform_of_ivl
                           (executable_euclidean_space_prod
                             (executable_euclidean_space_real, equal_real)
                             (executable_euclidean_space_prod
                                (executable_euclidean_space_real, equal_real)
                                (executable_euclidean_space_real, equal_real),
                               equal_prod equal_real equal_real)))
                         (inf_aform
                           (ordered_euclidean_space_prod
                             (equal_real, ordered_euclidean_space_real)
                             (equal_prod equal_real equal_real,
                               ordered_euclidean_space_prod
                                 (equal_real, ordered_euclidean_space_real)
                                 (equal_real, ordered_euclidean_space_real))))
                         (sup_aform
                           (ordered_euclidean_space_prod
                             (equal_real, ordered_euclidean_space_real)
                             (equal_prod equal_real equal_real,
                               ordered_euclidean_space_prod
                                 (equal_real, ordered_euclidean_space_real)
                                 (equal_real, ordered_euclidean_space_real))))
                         aborted;
                     val _ =
                       print_eucl
                         (executable_euclidean_space_prod
                           (executable_euclidean_space_real, equal_real)
                           (executable_euclidean_space_prod
                              (executable_euclidean_space_real, equal_real)
                              (executable_euclidean_space_real, equal_real),
                             equal_prod equal_real equal_real))
                         (inf_aform
                           (ordered_euclidean_space_prod
                             (equal_real, ordered_euclidean_space_real)
                             (equal_prod equal_real equal_real,
                               ordered_euclidean_space_prod
                                 (equal_real, ordered_euclidean_space_real)
                                 (equal_real, ordered_euclidean_space_real)))
                           ivl_abort);
                     val _ = TextIO.print " -- ";
                     val _ =
                       print_eucl
                         (executable_euclidean_space_prod
                           (executable_euclidean_space_real, equal_real)
                           (executable_euclidean_space_prod
                              (executable_euclidean_space_real, equal_real)
                              (executable_euclidean_space_real, equal_real),
                             equal_prod equal_real equal_real))
                         (sup_aform
                           (ordered_euclidean_space_prod
                             (equal_real, ordered_euclidean_space_real)
                             (equal_prod equal_real equal_real,
                               ordered_euclidean_space_prod
                                 (equal_real, ordered_euclidean_space_real)
                                 (equal_real, ordered_euclidean_space_real)))
                           ivl_abort);
                     val _ = println "";
                   in
                     ()
                   end
              else ());
          val _ = println "= Initial Rectangles of Return:";
          val _ = print_irects irectsa;
        in
          DRETURN irectsa
        end)
  end;

end; (*struct Lorenz*)
