open Preamble

open Types

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Positive

open Z

(** val internal_ram_size : Z.z **)
let internal_ram_size =
  Z.two_p
    (Z.z_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      Nat.O)))))))))

(** val external_ram_size : Z.z **)
let external_ram_size =
  Z.two_p
    (Z.z_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      Nat.O)))))))))))))))))