(* Generated by coq-of-rust *)
Require Import CoqOfRust.CoqOfRust.

Module num.
  Module dec2flt.
    Module decimal.
      (* StructRecord
        {
          name := "Decimal";
          const_params := [];
          ty_params := [];
          fields :=
            [
              ("num_digits", Ty.path "usize");
              ("decimal_point", Ty.path "i32");
              ("truncated", Ty.path "bool");
              ("digits",
                Ty.apply
                  (Ty.path "array")
                  [
                    M.unevaluated_const
                      (M.get_constant (|
                        "core::num::dec2flt::decimal::Decimal::digits_discriminant"
                      |))
                  ]
                  [ Ty.path "u8" ])
            ];
        } *)
      
      Module Impl_core_clone_Clone_for_core_num_dec2flt_decimal_Decimal.
        Definition Self : Ty.t := Ty.path "core::num::dec2flt::decimal::Decimal".
        
        (* Clone *)
        Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              Value.StructRecord
                "core::num::dec2flt::decimal::Decimal"
                [
                  ("num_digits",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.path "usize",
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::num::dec2flt::decimal::Decimal",
                          "num_digits"
                        |)
                      ]
                    |));
                  ("decimal_point",
                    M.call_closure (|
                      M.get_trait_method (| "core::clone::Clone", Ty.path "i32", [], "clone", [] |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::num::dec2flt::decimal::Decimal",
                          "decimal_point"
                        |)
                      ]
                    |));
                  ("truncated",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.path "bool",
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::num::dec2flt::decimal::Decimal",
                          "truncated"
                        |)
                      ]
                    |));
                  ("digits",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.apply
                          (Ty.path "array")
                          [ Value.Integer IntegerKind.Usize 768 ]
                          [ Ty.path "u8" ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::num::dec2flt::decimal::Decimal",
                          "digits"
                        |)
                      ]
                    |))
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::clone::Clone"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("clone", InstanceField.Method clone) ].
      End Impl_core_clone_Clone_for_core_num_dec2flt_decimal_Decimal.
      
      Module Impl_core_default_Default_for_core_num_dec2flt_decimal_Decimal.
        Definition Self : Ty.t := Ty.path "core::num::dec2flt::decimal::Decimal".
        
        (*
            fn default() -> Self {
                Self { num_digits: 0, decimal_point: 0, truncated: false, digits: [0; Self::MAX_DIGITS] }
            }
        *)
        Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [] =>
            ltac:(M.monadic
              (Value.StructRecord
                "core::num::dec2flt::decimal::Decimal"
                [
                  ("num_digits", Value.Integer IntegerKind.Usize 0);
                  ("decimal_point", Value.Integer IntegerKind.I32 0);
                  ("truncated", Value.Bool false);
                  ("digits",
                    repeat (|
                      Value.Integer IntegerKind.U8 0,
                      Value.Integer IntegerKind.Usize 768
                    |))
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::default::Default"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("default", InstanceField.Method default) ].
      End Impl_core_default_Default_for_core_num_dec2flt_decimal_Decimal.
      
      Module Impl_core_num_dec2flt_decimal_Decimal.
        Definition Self : Ty.t := Ty.path "core::num::dec2flt::decimal::Decimal".
        
        (*     pub const MAX_DIGITS: usize = 768; *)
        (* Ty.path "usize" *)
        Definition value_MAX_DIGITS : Value.t :=
          M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 768 |))).
        
        Axiom AssociatedConstant_value_MAX_DIGITS :
          M.IsAssociatedConstant Self "value_MAX_DIGITS" value_MAX_DIGITS.
        
        (*     pub const MAX_DIGITS_WITHOUT_OVERFLOW: usize = 19; *)
        (* Ty.path "usize" *)
        Definition value_MAX_DIGITS_WITHOUT_OVERFLOW : Value.t :=
          M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 19 |))).
        
        Axiom AssociatedConstant_value_MAX_DIGITS_WITHOUT_OVERFLOW :
          M.IsAssociatedConstant
            Self
            "value_MAX_DIGITS_WITHOUT_OVERFLOW"
            value_MAX_DIGITS_WITHOUT_OVERFLOW.
        
        (*     pub const DECIMAL_POINT_RANGE: i32 = 2047; *)
        (* Ty.path "i32" *)
        Definition value_DECIMAL_POINT_RANGE : Value.t :=
          M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.I32 2047 |))).
        
        Axiom AssociatedConstant_value_DECIMAL_POINT_RANGE :
          M.IsAssociatedConstant Self "value_DECIMAL_POINT_RANGE" value_DECIMAL_POINT_RANGE.
        
        (*
            pub fn try_add_digit(&mut self, digit: u8) {
                if self.num_digits < Self::MAX_DIGITS {
                    self.digits[self.num_digits] = digit;
                }
                self.num_digits += 1;
            }
        *)
        Definition try_add_digit (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self; digit ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let digit := M.alloc (| digit |) in
              M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.lt (|
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "core::num::dec2flt::decimal::Decimal",
                                      "num_digits"
                                    |)
                                  |),
                                  M.read (|
                                    M.get_constant (| "core::num::dec2flt::decimal::MAX_DIGITS" |)
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ :=
                            M.write (|
                              M.SubPointer.get_array_field (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "core::num::dec2flt::decimal::Decimal",
                                  "digits"
                                |),
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "core::num::dec2flt::decimal::Decimal",
                                  "num_digits"
                                |)
                              |),
                              M.read (| digit |)
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  let β :=
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::num::dec2flt::decimal::Decimal",
                      "num_digits"
                    |) in
                  M.write (|
                    β,
                    BinOp.Wrap.add (| M.read (| β |), Value.Integer IntegerKind.Usize 1 |)
                  |) in
                M.alloc (| Value.Tuple [] |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_try_add_digit :
          M.IsAssociatedFunction Self "try_add_digit" try_add_digit.
        
        (*
            pub fn trim(&mut self) {
                // All of the following calls to `Decimal::trim` can't panic because:
                //
                //  1. `parse_decimal` sets `num_digits` to a max of `Decimal::MAX_DIGITS`.
                //  2. `right_shift` sets `num_digits` to `write_index`, which is bounded by `num_digits`.
                //  3. `left_shift` `num_digits` to a max of `Decimal::MAX_DIGITS`.
                //
                // Trim is only called in `right_shift` and `left_shift`.
                debug_assert!(self.num_digits <= Self::MAX_DIGITS);
                while self.num_digits != 0 && self.digits[self.num_digits - 1] == 0 {
                    self.num_digits -= 1;
                }
            }
        *)
        Definition trim (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.use (M.alloc (| Value.Bool true |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          UnOp.not (|
                                            BinOp.le (|
                                              M.read (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| self |),
                                                  "core::num::dec2flt::decimal::Decimal",
                                                  "num_digits"
                                                |)
                                              |),
                                              M.read (|
                                                M.get_constant (|
                                                  "core::num::dec2flt::decimal::MAX_DIGITS"
                                                |)
                                              |)
                                            |)
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      M.never_to_any (|
                                        M.call_closure (|
                                          M.get_function (| "core::panicking::panic", [] |),
                                          [
                                            M.read (|
                                              Value.String
                                                "assertion failed: self.num_digits <= Self::MAX_DIGITS"
                                            |)
                                          ]
                                        |)
                                      |)
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.loop (|
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  LogicalOp.and (|
                                    BinOp.ne (|
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::num::dec2flt::decimal::Decimal",
                                          "num_digits"
                                        |)
                                      |),
                                      Value.Integer IntegerKind.Usize 0
                                    |),
                                    ltac:(M.monadic
                                      (BinOp.eq (|
                                        M.read (|
                                          M.SubPointer.get_array_field (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "core::num::dec2flt::decimal::Decimal",
                                              "digits"
                                            |),
                                            M.alloc (|
                                              BinOp.Wrap.sub (|
                                                M.read (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| self |),
                                                    "core::num::dec2flt::decimal::Decimal",
                                                    "num_digits"
                                                  |)
                                                |),
                                                Value.Integer IntegerKind.Usize 1
                                              |)
                                            |)
                                          |)
                                        |),
                                        Value.Integer IntegerKind.U8 0
                                      |)))
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            let~ _ :=
                              let β :=
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "core::num::dec2flt::decimal::Decimal",
                                  "num_digits"
                                |) in
                              M.write (|
                                β,
                                BinOp.Wrap.sub (|
                                  M.read (| β |),
                                  Value.Integer IntegerKind.Usize 1
                                |)
                              |) in
                            M.alloc (| Value.Tuple [] |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  let~ _ :=
                                    M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |) in
                                  M.alloc (| Value.Tuple [] |)
                                |)
                              |)
                            |)))
                      ]
                    |)))
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_trim : M.IsAssociatedFunction Self "trim" trim.
        
        (*
            pub fn round(&self) -> u64 {
                if self.num_digits == 0 || self.decimal_point < 0 {
                    return 0;
                } else if self.decimal_point > 18 {
                    return 0xFFFF_FFFF_FFFF_FFFF_u64;
                }
                let dp = self.decimal_point as usize;
                let mut n = 0_u64;
                for i in 0..dp {
                    n *= 10;
                    if i < self.num_digits {
                        n += self.digits[i] as u64;
                    }
                }
                let mut round_up = false;
                if dp < self.num_digits {
                    round_up = self.digits[dp] >= 5;
                    if self.digits[dp] == 5 && dp + 1 == self.num_digits {
                        round_up = self.truncated || ((dp != 0) && (1 & self.digits[dp - 1] != 0))
                    }
                }
                if round_up {
                    n += 1;
                }
                n
            }
        *)
        Definition round (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    LogicalOp.or (|
                                      BinOp.eq (|
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "core::num::dec2flt::decimal::Decimal",
                                            "num_digits"
                                          |)
                                        |),
                                        Value.Integer IntegerKind.Usize 0
                                      |),
                                      ltac:(M.monadic
                                        (BinOp.lt (|
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "core::num::dec2flt::decimal::Decimal",
                                              "decimal_point"
                                            |)
                                          |),
                                          Value.Integer IntegerKind.I32 0
                                        |)))
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.read (| M.return_ (| Value.Integer IntegerKind.U64 0 |) |)
                                |)
                              |)));
                          fun γ =>
                            ltac:(M.monadic
                              (M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ :=
                                        M.use
                                          (M.alloc (|
                                            BinOp.gt (|
                                              M.read (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| self |),
                                                  "core::num::dec2flt::decimal::Decimal",
                                                  "decimal_point"
                                                |)
                                              |),
                                              Value.Integer IntegerKind.I32 18
                                            |)
                                          |)) in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            M.return_ (|
                                              Value.Integer IntegerKind.U64 18446744073709551615
                                            |)
                                          |)
                                        |)
                                      |)));
                                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                ]
                              |)))
                        ]
                      |) in
                    let~ dp :=
                      M.alloc (|
                        M.rust_cast
                          (M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::num::dec2flt::decimal::Decimal",
                              "decimal_point"
                            |)
                          |))
                      |) in
                    let~ n := M.alloc (| Value.Integer IntegerKind.U64 0 |) in
                    let~ _ :=
                      M.use
                        (M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::collect::IntoIterator",
                                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                                [],
                                "into_iter",
                                []
                              |),
                              [
                                Value.StructRecord
                                  "core::ops::range::Range"
                                  [
                                    ("start", Value.Integer IntegerKind.Usize 0);
                                    ("end_", M.read (| dp |))
                                  ]
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let iter := M.copy (| γ |) in
                                M.loop (|
                                  ltac:(M.monadic
                                    (let~ _ :=
                                      M.match_operator (|
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::iter::traits::iterator::Iterator",
                                              Ty.apply
                                                (Ty.path "core::ops::range::Range")
                                                []
                                                [ Ty.path "usize" ],
                                              [],
                                              "next",
                                              []
                                            |),
                                            [ iter ]
                                          |)
                                        |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let _ :=
                                                M.is_struct_tuple (|
                                                  γ,
                                                  "core::option::Option::None"
                                                |) in
                                              M.alloc (|
                                                M.never_to_any (| M.read (| M.break (||) |) |)
                                              |)));
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ0_0 :=
                                                M.SubPointer.get_struct_tuple_field (|
                                                  γ,
                                                  "core::option::Option::Some",
                                                  0
                                                |) in
                                              let i := M.copy (| γ0_0 |) in
                                              let~ _ :=
                                                let β := n in
                                                M.write (|
                                                  β,
                                                  BinOp.Wrap.mul (|
                                                    M.read (| β |),
                                                    Value.Integer IntegerKind.U64 10
                                                  |)
                                                |) in
                                              M.match_operator (|
                                                M.alloc (| Value.Tuple [] |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ :=
                                                        M.use
                                                          (M.alloc (|
                                                            BinOp.lt (|
                                                              M.read (| i |),
                                                              M.read (|
                                                                M.SubPointer.get_struct_record_field (|
                                                                  M.read (| self |),
                                                                  "core::num::dec2flt::decimal::Decimal",
                                                                  "num_digits"
                                                                |)
                                                              |)
                                                            |)
                                                          |)) in
                                                      let _ :=
                                                        M.is_constant_or_break_match (|
                                                          M.read (| γ |),
                                                          Value.Bool true
                                                        |) in
                                                      let~ _ :=
                                                        let β := n in
                                                        M.write (|
                                                          β,
                                                          BinOp.Wrap.add (|
                                                            M.read (| β |),
                                                            M.rust_cast
                                                              (M.read (|
                                                                M.SubPointer.get_array_field (|
                                                                  M.SubPointer.get_struct_record_field (|
                                                                    M.read (| self |),
                                                                    "core::num::dec2flt::decimal::Decimal",
                                                                    "digits"
                                                                  |),
                                                                  i
                                                                |)
                                                              |))
                                                          |)
                                                        |) in
                                                      M.alloc (| Value.Tuple [] |)));
                                                  fun γ =>
                                                    ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                                ]
                                              |)))
                                        ]
                                      |) in
                                    M.alloc (| Value.Tuple [] |)))
                                |)))
                          ]
                        |)) in
                    let~ round_up := M.alloc (| Value.Bool false |) in
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    BinOp.lt (|
                                      M.read (| dp |),
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::num::dec2flt::decimal::Decimal",
                                          "num_digits"
                                        |)
                                      |)
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ _ :=
                                M.write (|
                                  round_up,
                                  BinOp.ge (|
                                    M.read (|
                                      M.SubPointer.get_array_field (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::num::dec2flt::decimal::Decimal",
                                          "digits"
                                        |),
                                        dp
                                      |)
                                    |),
                                    Value.Integer IntegerKind.U8 5
                                  |)
                                |) in
                              M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ :=
                                        M.use
                                          (M.alloc (|
                                            LogicalOp.and (|
                                              BinOp.eq (|
                                                M.read (|
                                                  M.SubPointer.get_array_field (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| self |),
                                                      "core::num::dec2flt::decimal::Decimal",
                                                      "digits"
                                                    |),
                                                    dp
                                                  |)
                                                |),
                                                Value.Integer IntegerKind.U8 5
                                              |),
                                              ltac:(M.monadic
                                                (BinOp.eq (|
                                                  BinOp.Wrap.add (|
                                                    M.read (| dp |),
                                                    Value.Integer IntegerKind.Usize 1
                                                  |),
                                                  M.read (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| self |),
                                                      "core::num::dec2flt::decimal::Decimal",
                                                      "num_digits"
                                                    |)
                                                  |)
                                                |)))
                                            |)
                                          |)) in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      M.write (|
                                        round_up,
                                        LogicalOp.or (|
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "core::num::dec2flt::decimal::Decimal",
                                              "truncated"
                                            |)
                                          |),
                                          ltac:(M.monadic
                                            (LogicalOp.and (|
                                              BinOp.ne (|
                                                M.read (| dp |),
                                                Value.Integer IntegerKind.Usize 0
                                              |),
                                              ltac:(M.monadic
                                                (BinOp.ne (|
                                                  BinOp.bit_and
                                                    (Value.Integer IntegerKind.U8 1)
                                                    (M.read (|
                                                      M.SubPointer.get_array_field (|
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.read (| self |),
                                                          "core::num::dec2flt::decimal::Decimal",
                                                          "digits"
                                                        |),
                                                        M.alloc (|
                                                          BinOp.Wrap.sub (|
                                                            M.read (| dp |),
                                                            Value.Integer IntegerKind.Usize 1
                                                          |)
                                                        |)
                                                      |)
                                                    |)),
                                                  Value.Integer IntegerKind.U8 0
                                                |)))
                                            |)))
                                        |)
                                      |)));
                                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                ]
                              |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ := M.use round_up in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ _ :=
                                let β := n in
                                M.write (|
                                  β,
                                  BinOp.Wrap.add (|
                                    M.read (| β |),
                                    Value.Integer IntegerKind.U64 1
                                  |)
                                |) in
                              M.alloc (| Value.Tuple [] |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    n
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_round : M.IsAssociatedFunction Self "round" round.
        
        (*
            pub fn left_shift(&mut self, shift: usize) {
                if self.num_digits == 0 {
                    return;
                }
                let num_new_digits = number_of_digits_decimal_left_shift(self, shift);
                let mut read_index = self.num_digits;
                let mut write_index = self.num_digits + num_new_digits;
                let mut n = 0_u64;
                while read_index != 0 {
                    read_index -= 1;
                    write_index -= 1;
                    n += (self.digits[read_index] as u64) << shift;
                    let quotient = n / 10;
                    let remainder = n - (10 * quotient);
                    if write_index < Self::MAX_DIGITS {
                        self.digits[write_index] = remainder as u8;
                    } else if remainder > 0 {
                        self.truncated = true;
                    }
                    n = quotient;
                }
                while n > 0 {
                    write_index -= 1;
                    let quotient = n / 10;
                    let remainder = n - (10 * quotient);
                    if write_index < Self::MAX_DIGITS {
                        self.digits[write_index] = remainder as u8;
                    } else if remainder > 0 {
                        self.truncated = true;
                    }
                    n = quotient;
                }
                self.num_digits += num_new_digits;
                if self.num_digits > Self::MAX_DIGITS {
                    self.num_digits = Self::MAX_DIGITS;
                }
                self.decimal_point += num_new_digits as i32;
                self.trim();
            }
        *)
        Definition left_shift (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self; shift ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let shift := M.alloc (| shift |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    BinOp.eq (|
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::num::dec2flt::decimal::Decimal",
                                          "num_digits"
                                        |)
                                      |),
                                      Value.Integer IntegerKind.Usize 0
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              M.alloc (|
                                M.never_to_any (| M.read (| M.return_ (| Value.Tuple [] |) |) |)
                              |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    let~ num_new_digits :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (|
                            "core::num::dec2flt::decimal::number_of_digits_decimal_left_shift",
                            []
                          |),
                          [ M.read (| self |); M.read (| shift |) ]
                        |)
                      |) in
                    let~ read_index :=
                      M.copy (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::num::dec2flt::decimal::Decimal",
                          "num_digits"
                        |)
                      |) in
                    let~ write_index :=
                      M.alloc (|
                        BinOp.Wrap.add (|
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::num::dec2flt::decimal::Decimal",
                              "num_digits"
                            |)
                          |),
                          M.read (| num_new_digits |)
                        |)
                      |) in
                    let~ n := M.alloc (| Value.Integer IntegerKind.U64 0 |) in
                    let~ _ :=
                      M.loop (|
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.ne (|
                                          M.read (| read_index |),
                                          Value.Integer IntegerKind.Usize 0
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  let~ _ :=
                                    let β := read_index in
                                    M.write (|
                                      β,
                                      BinOp.Wrap.sub (|
                                        M.read (| β |),
                                        Value.Integer IntegerKind.Usize 1
                                      |)
                                    |) in
                                  let~ _ :=
                                    let β := write_index in
                                    M.write (|
                                      β,
                                      BinOp.Wrap.sub (|
                                        M.read (| β |),
                                        Value.Integer IntegerKind.Usize 1
                                      |)
                                    |) in
                                  let~ _ :=
                                    let β := n in
                                    M.write (|
                                      β,
                                      BinOp.Wrap.add (|
                                        M.read (| β |),
                                        BinOp.Wrap.shl (|
                                          M.rust_cast
                                            (M.read (|
                                              M.SubPointer.get_array_field (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| self |),
                                                  "core::num::dec2flt::decimal::Decimal",
                                                  "digits"
                                                |),
                                                read_index
                                              |)
                                            |)),
                                          M.read (| shift |)
                                        |)
                                      |)
                                    |) in
                                  let~ quotient :=
                                    M.alloc (|
                                      BinOp.Wrap.div (|
                                        M.read (| n |),
                                        Value.Integer IntegerKind.U64 10
                                      |)
                                    |) in
                                  let~ remainder :=
                                    M.alloc (|
                                      BinOp.Wrap.sub (|
                                        M.read (| n |),
                                        BinOp.Wrap.mul (|
                                          Value.Integer IntegerKind.U64 10,
                                          M.read (| quotient |)
                                        |)
                                      |)
                                    |) in
                                  let~ _ :=
                                    M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ :=
                                              M.use
                                                (M.alloc (|
                                                  BinOp.lt (|
                                                    M.read (| write_index |),
                                                    M.read (|
                                                      M.get_constant (|
                                                        "core::num::dec2flt::decimal::MAX_DIGITS"
                                                      |)
                                                    |)
                                                  |)
                                                |)) in
                                            let _ :=
                                              M.is_constant_or_break_match (|
                                                M.read (| γ |),
                                                Value.Bool true
                                              |) in
                                            let~ _ :=
                                              M.write (|
                                                M.SubPointer.get_array_field (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| self |),
                                                    "core::num::dec2flt::decimal::Decimal",
                                                    "digits"
                                                  |),
                                                  write_index
                                                |),
                                                M.rust_cast (M.read (| remainder |))
                                              |) in
                                            M.alloc (| Value.Tuple [] |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (M.match_operator (|
                                              M.alloc (| Value.Tuple [] |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ :=
                                                      M.use
                                                        (M.alloc (|
                                                          BinOp.gt (|
                                                            M.read (| remainder |),
                                                            Value.Integer IntegerKind.U64 0
                                                          |)
                                                        |)) in
                                                    let _ :=
                                                      M.is_constant_or_break_match (|
                                                        M.read (| γ |),
                                                        Value.Bool true
                                                      |) in
                                                    let~ _ :=
                                                      M.write (|
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.read (| self |),
                                                          "core::num::dec2flt::decimal::Decimal",
                                                          "truncated"
                                                        |),
                                                        Value.Bool true
                                                      |) in
                                                    M.alloc (| Value.Tuple [] |)));
                                                fun γ =>
                                                  ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                              ]
                                            |)))
                                      ]
                                    |) in
                                  let~ _ := M.write (| n, M.read (| quotient |) |) in
                                  M.alloc (| Value.Tuple [] |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        let~ _ :=
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |) in
                                        M.alloc (| Value.Tuple [] |)
                                      |)
                                    |)
                                  |)))
                            ]
                          |)))
                      |) in
                    let~ _ :=
                      M.loop (|
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.gt (|
                                          M.read (| n |),
                                          Value.Integer IntegerKind.U64 0
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  let~ _ :=
                                    let β := write_index in
                                    M.write (|
                                      β,
                                      BinOp.Wrap.sub (|
                                        M.read (| β |),
                                        Value.Integer IntegerKind.Usize 1
                                      |)
                                    |) in
                                  let~ quotient :=
                                    M.alloc (|
                                      BinOp.Wrap.div (|
                                        M.read (| n |),
                                        Value.Integer IntegerKind.U64 10
                                      |)
                                    |) in
                                  let~ remainder :=
                                    M.alloc (|
                                      BinOp.Wrap.sub (|
                                        M.read (| n |),
                                        BinOp.Wrap.mul (|
                                          Value.Integer IntegerKind.U64 10,
                                          M.read (| quotient |)
                                        |)
                                      |)
                                    |) in
                                  let~ _ :=
                                    M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ :=
                                              M.use
                                                (M.alloc (|
                                                  BinOp.lt (|
                                                    M.read (| write_index |),
                                                    M.read (|
                                                      M.get_constant (|
                                                        "core::num::dec2flt::decimal::MAX_DIGITS"
                                                      |)
                                                    |)
                                                  |)
                                                |)) in
                                            let _ :=
                                              M.is_constant_or_break_match (|
                                                M.read (| γ |),
                                                Value.Bool true
                                              |) in
                                            let~ _ :=
                                              M.write (|
                                                M.SubPointer.get_array_field (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| self |),
                                                    "core::num::dec2flt::decimal::Decimal",
                                                    "digits"
                                                  |),
                                                  write_index
                                                |),
                                                M.rust_cast (M.read (| remainder |))
                                              |) in
                                            M.alloc (| Value.Tuple [] |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (M.match_operator (|
                                              M.alloc (| Value.Tuple [] |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ :=
                                                      M.use
                                                        (M.alloc (|
                                                          BinOp.gt (|
                                                            M.read (| remainder |),
                                                            Value.Integer IntegerKind.U64 0
                                                          |)
                                                        |)) in
                                                    let _ :=
                                                      M.is_constant_or_break_match (|
                                                        M.read (| γ |),
                                                        Value.Bool true
                                                      |) in
                                                    let~ _ :=
                                                      M.write (|
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.read (| self |),
                                                          "core::num::dec2flt::decimal::Decimal",
                                                          "truncated"
                                                        |),
                                                        Value.Bool true
                                                      |) in
                                                    M.alloc (| Value.Tuple [] |)));
                                                fun γ =>
                                                  ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                              ]
                                            |)))
                                      ]
                                    |) in
                                  let~ _ := M.write (| n, M.read (| quotient |) |) in
                                  M.alloc (| Value.Tuple [] |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        let~ _ :=
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |) in
                                        M.alloc (| Value.Tuple [] |)
                                      |)
                                    |)
                                  |)))
                            ]
                          |)))
                      |) in
                    let~ _ :=
                      let β :=
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::num::dec2flt::decimal::Decimal",
                          "num_digits"
                        |) in
                      M.write (|
                        β,
                        BinOp.Wrap.add (| M.read (| β |), M.read (| num_new_digits |) |)
                      |) in
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    BinOp.gt (|
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::num::dec2flt::decimal::Decimal",
                                          "num_digits"
                                        |)
                                      |),
                                      M.read (|
                                        M.get_constant (|
                                          "core::num::dec2flt::decimal::MAX_DIGITS"
                                        |)
                                      |)
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ _ :=
                                M.write (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::num::dec2flt::decimal::Decimal",
                                    "num_digits"
                                  |),
                                  M.read (|
                                    M.get_constant (| "core::num::dec2flt::decimal::MAX_DIGITS" |)
                                  |)
                                |) in
                              M.alloc (| Value.Tuple [] |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    let~ _ :=
                      let β :=
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::num::dec2flt::decimal::Decimal",
                          "decimal_point"
                        |) in
                      M.write (|
                        β,
                        BinOp.Wrap.add (|
                          M.read (| β |),
                          M.rust_cast (M.read (| num_new_digits |))
                        |)
                      |) in
                    let~ _ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::num::dec2flt::decimal::Decimal",
                            "trim",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      |) in
                    M.alloc (| Value.Tuple [] |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_left_shift : M.IsAssociatedFunction Self "left_shift" left_shift.
        
        (*
            pub fn right_shift(&mut self, shift: usize) {
                let mut read_index = 0;
                let mut write_index = 0;
                let mut n = 0_u64;
                while (n >> shift) == 0 {
                    if read_index < self.num_digits {
                        n = (10 * n) + self.digits[read_index] as u64;
                        read_index += 1;
                    } else if n == 0 {
                        return;
                    } else {
                        while (n >> shift) == 0 {
                            n *= 10;
                            read_index += 1;
                        }
                        break;
                    }
                }
                self.decimal_point -= read_index as i32 - 1;
                if self.decimal_point < -Self::DECIMAL_POINT_RANGE {
                    // `self = Self::Default()`, but without the overhead of clearing `digits`.
                    self.num_digits = 0;
                    self.decimal_point = 0;
                    self.truncated = false;
                    return;
                }
                let mask = (1_u64 << shift) - 1;
                while read_index < self.num_digits {
                    let new_digit = (n >> shift) as u8;
                    n = (10 * (n & mask)) + self.digits[read_index] as u64;
                    read_index += 1;
                    self.digits[write_index] = new_digit;
                    write_index += 1;
                }
                while n > 0 {
                    let new_digit = (n >> shift) as u8;
                    n = 10 * (n & mask);
                    if write_index < Self::MAX_DIGITS {
                        self.digits[write_index] = new_digit;
                        write_index += 1;
                    } else if new_digit > 0 {
                        self.truncated = true;
                    }
                }
                self.num_digits = write_index;
                self.trim();
            }
        *)
        Definition right_shift (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self; shift ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let shift := M.alloc (| shift |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ read_index := M.alloc (| Value.Integer IntegerKind.Usize 0 |) in
                    let~ write_index := M.alloc (| Value.Integer IntegerKind.Usize 0 |) in
                    let~ n := M.alloc (| Value.Integer IntegerKind.U64 0 |) in
                    let~ _ :=
                      M.loop (|
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.eq (|
                                          BinOp.Wrap.shr (| M.read (| n |), M.read (| shift |) |),
                                          Value.Integer IntegerKind.U64 0
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                BinOp.lt (|
                                                  M.read (| read_index |),
                                                  M.read (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| self |),
                                                      "core::num::dec2flt::decimal::Decimal",
                                                      "num_digits"
                                                    |)
                                                  |)
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          let~ _ :=
                                            M.write (|
                                              n,
                                              BinOp.Wrap.add (|
                                                BinOp.Wrap.mul (|
                                                  Value.Integer IntegerKind.U64 10,
                                                  M.read (| n |)
                                                |),
                                                M.rust_cast
                                                  (M.read (|
                                                    M.SubPointer.get_array_field (|
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| self |),
                                                        "core::num::dec2flt::decimal::Decimal",
                                                        "digits"
                                                      |),
                                                      read_index
                                                    |)
                                                  |))
                                              |)
                                            |) in
                                          let~ _ :=
                                            let β := read_index in
                                            M.write (|
                                              β,
                                              BinOp.Wrap.add (|
                                                M.read (| β |),
                                                Value.Integer IntegerKind.Usize 1
                                              |)
                                            |) in
                                          M.alloc (| Value.Tuple [] |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.use
                                                      (M.alloc (|
                                                        BinOp.eq (|
                                                          M.read (| n |),
                                                          Value.Integer IntegerKind.U64 0
                                                        |)
                                                      |)) in
                                                  let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Bool true
                                                    |) in
                                                  M.alloc (|
                                                    M.never_to_any (|
                                                      M.read (| M.return_ (| Value.Tuple [] |) |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (M.alloc (|
                                                    M.never_to_any (|
                                                      M.read (|
                                                        let~ _ :=
                                                          M.loop (|
                                                            ltac:(M.monadic
                                                              (M.match_operator (|
                                                                M.alloc (| Value.Tuple [] |),
                                                                [
                                                                  fun γ =>
                                                                    ltac:(M.monadic
                                                                      (let γ :=
                                                                        M.use
                                                                          (M.alloc (|
                                                                            BinOp.eq (|
                                                                              BinOp.Wrap.shr (|
                                                                                M.read (| n |),
                                                                                M.read (| shift |)
                                                                              |),
                                                                              Value.Integer
                                                                                IntegerKind.U64
                                                                                0
                                                                            |)
                                                                          |)) in
                                                                      let _ :=
                                                                        M.is_constant_or_break_match (|
                                                                          M.read (| γ |),
                                                                          Value.Bool true
                                                                        |) in
                                                                      let~ _ :=
                                                                        let β := n in
                                                                        M.write (|
                                                                          β,
                                                                          BinOp.Wrap.mul (|
                                                                            M.read (| β |),
                                                                            Value.Integer
                                                                              IntegerKind.U64
                                                                              10
                                                                          |)
                                                                        |) in
                                                                      let~ _ :=
                                                                        let β := read_index in
                                                                        M.write (|
                                                                          β,
                                                                          BinOp.Wrap.add (|
                                                                            M.read (| β |),
                                                                            Value.Integer
                                                                              IntegerKind.Usize
                                                                              1
                                                                          |)
                                                                        |) in
                                                                      M.alloc (|
                                                                        Value.Tuple []
                                                                      |)));
                                                                  fun γ =>
                                                                    ltac:(M.monadic
                                                                      (M.alloc (|
                                                                        M.never_to_any (|
                                                                          M.read (|
                                                                            let~ _ :=
                                                                              M.alloc (|
                                                                                M.never_to_any (|
                                                                                  M.read (|
                                                                                    M.break (||)
                                                                                  |)
                                                                                |)
                                                                              |) in
                                                                            M.alloc (|
                                                                              Value.Tuple []
                                                                            |)
                                                                          |)
                                                                        |)
                                                                      |)))
                                                                ]
                                                              |)))
                                                          |) in
                                                        M.break (||)
                                                      |)
                                                    |)
                                                  |)))
                                            ]
                                          |)))
                                    ]
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        let~ _ :=
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |) in
                                        M.alloc (| Value.Tuple [] |)
                                      |)
                                    |)
                                  |)))
                            ]
                          |)))
                      |) in
                    let~ _ :=
                      let β :=
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::num::dec2flt::decimal::Decimal",
                          "decimal_point"
                        |) in
                      M.write (|
                        β,
                        BinOp.Wrap.sub (|
                          M.read (| β |),
                          BinOp.Wrap.sub (|
                            M.rust_cast (M.read (| read_index |)),
                            Value.Integer IntegerKind.I32 1
                          |)
                        |)
                      |) in
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    BinOp.lt (|
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::num::dec2flt::decimal::Decimal",
                                          "decimal_point"
                                        |)
                                      |),
                                      UnOp.neg (|
                                        M.read (|
                                          M.get_constant (|
                                            "core::num::dec2flt::decimal::DECIMAL_POINT_RANGE"
                                          |)
                                        |)
                                      |)
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    let~ _ :=
                                      M.write (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::num::dec2flt::decimal::Decimal",
                                          "num_digits"
                                        |),
                                        Value.Integer IntegerKind.Usize 0
                                      |) in
                                    let~ _ :=
                                      M.write (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::num::dec2flt::decimal::Decimal",
                                          "decimal_point"
                                        |),
                                        Value.Integer IntegerKind.I32 0
                                      |) in
                                    let~ _ :=
                                      M.write (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::num::dec2flt::decimal::Decimal",
                                          "truncated"
                                        |),
                                        Value.Bool false
                                      |) in
                                    M.return_ (| Value.Tuple [] |)
                                  |)
                                |)
                              |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    let~ mask :=
                      M.alloc (|
                        BinOp.Wrap.sub (|
                          BinOp.Wrap.shl (| Value.Integer IntegerKind.U64 1, M.read (| shift |) |),
                          Value.Integer IntegerKind.U64 1
                        |)
                      |) in
                    let~ _ :=
                      M.loop (|
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.lt (|
                                          M.read (| read_index |),
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "core::num::dec2flt::decimal::Decimal",
                                              "num_digits"
                                            |)
                                          |)
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  let~ new_digit :=
                                    M.alloc (|
                                      M.rust_cast
                                        (BinOp.Wrap.shr (| M.read (| n |), M.read (| shift |) |))
                                    |) in
                                  let~ _ :=
                                    M.write (|
                                      n,
                                      BinOp.Wrap.add (|
                                        BinOp.Wrap.mul (|
                                          Value.Integer IntegerKind.U64 10,
                                          BinOp.bit_and (M.read (| n |)) (M.read (| mask |))
                                        |),
                                        M.rust_cast
                                          (M.read (|
                                            M.SubPointer.get_array_field (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| self |),
                                                "core::num::dec2flt::decimal::Decimal",
                                                "digits"
                                              |),
                                              read_index
                                            |)
                                          |))
                                      |)
                                    |) in
                                  let~ _ :=
                                    let β := read_index in
                                    M.write (|
                                      β,
                                      BinOp.Wrap.add (|
                                        M.read (| β |),
                                        Value.Integer IntegerKind.Usize 1
                                      |)
                                    |) in
                                  let~ _ :=
                                    M.write (|
                                      M.SubPointer.get_array_field (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::num::dec2flt::decimal::Decimal",
                                          "digits"
                                        |),
                                        write_index
                                      |),
                                      M.read (| new_digit |)
                                    |) in
                                  let~ _ :=
                                    let β := write_index in
                                    M.write (|
                                      β,
                                      BinOp.Wrap.add (|
                                        M.read (| β |),
                                        Value.Integer IntegerKind.Usize 1
                                      |)
                                    |) in
                                  M.alloc (| Value.Tuple [] |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        let~ _ :=
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |) in
                                        M.alloc (| Value.Tuple [] |)
                                      |)
                                    |)
                                  |)))
                            ]
                          |)))
                      |) in
                    let~ _ :=
                      M.loop (|
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.gt (|
                                          M.read (| n |),
                                          Value.Integer IntegerKind.U64 0
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  let~ new_digit :=
                                    M.alloc (|
                                      M.rust_cast
                                        (BinOp.Wrap.shr (| M.read (| n |), M.read (| shift |) |))
                                    |) in
                                  let~ _ :=
                                    M.write (|
                                      n,
                                      BinOp.Wrap.mul (|
                                        Value.Integer IntegerKind.U64 10,
                                        BinOp.bit_and (M.read (| n |)) (M.read (| mask |))
                                      |)
                                    |) in
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                BinOp.lt (|
                                                  M.read (| write_index |),
                                                  M.read (|
                                                    M.get_constant (|
                                                      "core::num::dec2flt::decimal::MAX_DIGITS"
                                                    |)
                                                  |)
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          let~ _ :=
                                            M.write (|
                                              M.SubPointer.get_array_field (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| self |),
                                                  "core::num::dec2flt::decimal::Decimal",
                                                  "digits"
                                                |),
                                                write_index
                                              |),
                                              M.read (| new_digit |)
                                            |) in
                                          let~ _ :=
                                            let β := write_index in
                                            M.write (|
                                              β,
                                              BinOp.Wrap.add (|
                                                M.read (| β |),
                                                Value.Integer IntegerKind.Usize 1
                                              |)
                                            |) in
                                          M.alloc (| Value.Tuple [] |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.use
                                                      (M.alloc (|
                                                        BinOp.gt (|
                                                          M.read (| new_digit |),
                                                          Value.Integer IntegerKind.U8 0
                                                        |)
                                                      |)) in
                                                  let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Bool true
                                                    |) in
                                                  let~ _ :=
                                                    M.write (|
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| self |),
                                                        "core::num::dec2flt::decimal::Decimal",
                                                        "truncated"
                                                      |),
                                                      Value.Bool true
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |)))
                                    ]
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        let~ _ :=
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |) in
                                        M.alloc (| Value.Tuple [] |)
                                      |)
                                    |)
                                  |)))
                            ]
                          |)))
                      |) in
                    let~ _ :=
                      M.write (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::num::dec2flt::decimal::Decimal",
                          "num_digits"
                        |),
                        M.read (| write_index |)
                      |) in
                    let~ _ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::num::dec2flt::decimal::Decimal",
                            "trim",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      |) in
                    M.alloc (| Value.Tuple [] |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_right_shift :
          M.IsAssociatedFunction Self "right_shift" right_shift.
      End Impl_core_num_dec2flt_decimal_Decimal.
      
      (*
      pub fn parse_decimal(mut s: &[u8]) -> Decimal {
          let mut d = Decimal::default();
          let start = s;
      
          while let Some((&b'0', s_next)) = s.split_first() {
              s = s_next;
          }
      
          s = s.parse_digits(|digit| d.try_add_digit(digit));
      
          if let Some((b'.', s_next)) = s.split_first() {
              s = s_next;
              let first = s;
              // Skip leading zeros.
              if d.num_digits == 0 {
                  while let Some((&b'0', s_next)) = s.split_first() {
                      s = s_next;
                  }
              }
              while s.len() >= 8 && d.num_digits + 8 < Decimal::MAX_DIGITS {
                  let v = s.read_u64();
                  if !is_8digits(v) {
                      break;
                  }
                  d.digits[d.num_digits..].write_u64(v - 0x3030_3030_3030_3030);
                  d.num_digits += 8;
                  s = &s[8..];
              }
              s = s.parse_digits(|digit| d.try_add_digit(digit));
              d.decimal_point = s.len() as i32 - first.len() as i32;
          }
          if d.num_digits != 0 {
              // Ignore the trailing zeros if there are any
              let mut n_trailing_zeros = 0;
              for &c in start[..(start.len() - s.len())].iter().rev() {
                  if c == b'0' {
                      n_trailing_zeros += 1;
                  } else if c != b'.' {
                      break;
                  }
              }
              d.decimal_point += n_trailing_zeros as i32;
              d.num_digits -= n_trailing_zeros;
              d.decimal_point += d.num_digits as i32;
              if d.num_digits > Decimal::MAX_DIGITS {
                  d.truncated = true;
                  d.num_digits = Decimal::MAX_DIGITS;
              }
          }
          if let Some((&ch, s_next)) = s.split_first() {
              if ch == b'e' || ch == b'E' {
                  s = s_next;
                  let mut neg_exp = false;
                  if let Some((&ch, s_next)) = s.split_first() {
                      neg_exp = ch == b'-';
                      if ch == b'-' || ch == b'+' {
                          s = s_next;
                      }
                  }
                  let mut exp_num = 0_i32;
      
                  s.parse_digits(|digit| {
                      if exp_num < 0x10000 {
                          exp_num = 10 * exp_num + digit as i32;
                      }
                  });
      
                  d.decimal_point += if neg_exp { -exp_num } else { exp_num };
              }
          }
          for i in d.num_digits..Decimal::MAX_DIGITS_WITHOUT_OVERFLOW {
              d.digits[i] = 0;
          }
          d
      }
      *)
      Definition parse_decimal (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ s ] =>
          ltac:(M.monadic
            (let s := M.alloc (| s |) in
            M.read (|
              let~ d :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.path "core::num::dec2flt::decimal::Decimal",
                      [],
                      "default",
                      []
                    |),
                    []
                  |)
                |) in
              let~ start := M.copy (| s |) in
              let~ _ :=
                M.loop (|
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                    "split_first",
                                    []
                                  |),
                                  [ M.read (| s |) ]
                                |)
                              |) in
                            let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::option::Option::Some",
                                0
                              |) in
                            let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                            let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                            let γ1_0 := M.read (| γ1_0 |) in
                            let _ :=
                              M.is_constant_or_break_match (|
                                M.read (| γ1_0 |),
                                Value.Integer IntegerKind.U8 48
                              |) in
                            let s_next := M.copy (| γ1_1 |) in
                            let~ _ := M.write (| s, M.read (| s_next |) |) in
                            M.alloc (| Value.Tuple [] |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  let~ _ :=
                                    M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |) in
                                  M.alloc (| Value.Tuple [] |)
                                |)
                              |)
                            |)))
                      ]
                    |)))
                |) in
              let~ _ :=
                M.write (|
                  s,
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::num::dec2flt::common::ByteSlice",
                      Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                      [],
                      "parse_digits",
                      [ Ty.function [ Ty.tuple [ Ty.path "u8" ] ] (Ty.tuple []) ]
                    |),
                    [
                      M.read (| s |);
                      M.closure
                        (fun γ =>
                          ltac:(M.monadic
                            match γ with
                            | [ α0 ] =>
                              ltac:(M.monadic
                                (M.match_operator (|
                                  M.alloc (| α0 |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let digit := M.copy (| γ |) in
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "core::num::dec2flt::decimal::Decimal",
                                            "try_add_digit",
                                            []
                                          |),
                                          [ d; M.read (| digit |) ]
                                        |)))
                                  ]
                                |)))
                            | _ => M.impossible "wrong number of arguments"
                            end))
                    ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                "split_first",
                                []
                              |),
                              [ M.read (| s |) ]
                            |)
                          |) in
                        let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                        let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                        let γ1_0 := M.read (| γ1_0 |) in
                        let _ :=
                          M.is_constant_or_break_match (|
                            M.read (| γ1_0 |),
                            Value.Integer IntegerKind.U8 46
                          |) in
                        let s_next := M.copy (| γ1_1 |) in
                        let~ _ := M.write (| s, M.read (| s_next |) |) in
                        let~ first := M.copy (| s |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.eq (|
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              d,
                                              "core::num::dec2flt::decimal::Decimal",
                                              "num_digits"
                                            |)
                                          |),
                                          Value.Integer IntegerKind.Usize 0
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.loop (|
                                    ltac:(M.monadic
                                      (M.match_operator (|
                                        M.alloc (| Value.Tuple [] |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ :=
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path "slice")
                                                        []
                                                        [ Ty.path "u8" ],
                                                      "split_first",
                                                      []
                                                    |),
                                                    [ M.read (| s |) ]
                                                  |)
                                                |) in
                                              let γ0_0 :=
                                                M.SubPointer.get_struct_tuple_field (|
                                                  γ,
                                                  "core::option::Option::Some",
                                                  0
                                                |) in
                                              let γ1_0 :=
                                                M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                              let γ1_1 :=
                                                M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                              let γ1_0 := M.read (| γ1_0 |) in
                                              let _ :=
                                                M.is_constant_or_break_match (|
                                                  M.read (| γ1_0 |),
                                                  Value.Integer IntegerKind.U8 48
                                                |) in
                                              let s_next := M.copy (| γ1_1 |) in
                                              let~ _ := M.write (| s, M.read (| s_next |) |) in
                                              M.alloc (| Value.Tuple [] |)));
                                          fun γ =>
                                            ltac:(M.monadic
                                              (M.alloc (|
                                                M.never_to_any (|
                                                  M.read (|
                                                    let~ _ :=
                                                      M.alloc (|
                                                        M.never_to_any (|
                                                          M.read (| M.break (||) |)
                                                        |)
                                                      |) in
                                                    M.alloc (| Value.Tuple [] |)
                                                  |)
                                                |)
                                              |)))
                                        ]
                                      |)))
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        let~ _ :=
                          M.loop (|
                            ltac:(M.monadic
                              (M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ :=
                                        M.use
                                          (M.alloc (|
                                            LogicalOp.and (|
                                              BinOp.ge (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                                    "len",
                                                    []
                                                  |),
                                                  [ M.read (| s |) ]
                                                |),
                                                Value.Integer IntegerKind.Usize 8
                                              |),
                                              ltac:(M.monadic
                                                (BinOp.lt (|
                                                  BinOp.Wrap.add (|
                                                    M.read (|
                                                      M.SubPointer.get_struct_record_field (|
                                                        d,
                                                        "core::num::dec2flt::decimal::Decimal",
                                                        "num_digits"
                                                      |)
                                                    |),
                                                    Value.Integer IntegerKind.Usize 8
                                                  |),
                                                  M.read (|
                                                    M.get_constant (|
                                                      "core::num::dec2flt::decimal::MAX_DIGITS"
                                                    |)
                                                  |)
                                                |)))
                                            |)
                                          |)) in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      let~ v :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::num::dec2flt::common::ByteSlice",
                                              Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                              [],
                                              "read_u64",
                                              []
                                            |),
                                            [ M.read (| s |) ]
                                          |)
                                        |) in
                                      let~ _ :=
                                        M.match_operator (|
                                          M.alloc (| Value.Tuple [] |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let γ :=
                                                  M.use
                                                    (M.alloc (|
                                                      UnOp.not (|
                                                        M.call_closure (|
                                                          M.get_function (|
                                                            "core::num::dec2flt::common::is_8digits",
                                                            []
                                                          |),
                                                          [ M.read (| v |) ]
                                                        |)
                                                      |)
                                                    |)) in
                                                let _ :=
                                                  M.is_constant_or_break_match (|
                                                    M.read (| γ |),
                                                    Value.Bool true
                                                  |) in
                                                M.alloc (|
                                                  M.never_to_any (| M.read (| M.break (||) |) |)
                                                |)));
                                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                          ]
                                        |) in
                                      let~ _ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::num::dec2flt::common::ByteSlice",
                                              Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                              [],
                                              "write_u64",
                                              []
                                            |),
                                            [
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::index::IndexMut",
                                                  Ty.apply
                                                    (Ty.path "array")
                                                    [ Value.Integer IntegerKind.Usize 768 ]
                                                    [ Ty.path "u8" ],
                                                  [
                                                    Ty.apply
                                                      (Ty.path "core::ops::range::RangeFrom")
                                                      []
                                                      [ Ty.path "usize" ]
                                                  ],
                                                  "index_mut",
                                                  []
                                                |),
                                                [
                                                  M.SubPointer.get_struct_record_field (|
                                                    d,
                                                    "core::num::dec2flt::decimal::Decimal",
                                                    "digits"
                                                  |);
                                                  Value.StructRecord
                                                    "core::ops::range::RangeFrom"
                                                    [
                                                      ("start",
                                                        M.read (|
                                                          M.SubPointer.get_struct_record_field (|
                                                            d,
                                                            "core::num::dec2flt::decimal::Decimal",
                                                            "num_digits"
                                                          |)
                                                        |))
                                                    ]
                                                ]
                                              |);
                                              BinOp.Wrap.sub (|
                                                M.read (| v |),
                                                Value.Integer IntegerKind.U64 3472328296227680304
                                              |)
                                            ]
                                          |)
                                        |) in
                                      let~ _ :=
                                        let β :=
                                          M.SubPointer.get_struct_record_field (|
                                            d,
                                            "core::num::dec2flt::decimal::Decimal",
                                            "num_digits"
                                          |) in
                                        M.write (|
                                          β,
                                          BinOp.Wrap.add (|
                                            M.read (| β |),
                                            Value.Integer IntegerKind.Usize 8
                                          |)
                                        |) in
                                      let~ _ :=
                                        M.write (|
                                          s,
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::ops::index::Index",
                                              Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                              [
                                                Ty.apply
                                                  (Ty.path "core::ops::range::RangeFrom")
                                                  []
                                                  [ Ty.path "usize" ]
                                              ],
                                              "index",
                                              []
                                            |),
                                            [
                                              M.read (| s |);
                                              Value.StructRecord
                                                "core::ops::range::RangeFrom"
                                                [ ("start", Value.Integer IntegerKind.Usize 8) ]
                                            ]
                                          |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            let~ _ :=
                                              M.alloc (|
                                                M.never_to_any (| M.read (| M.break (||) |) |)
                                              |) in
                                            M.alloc (| Value.Tuple [] |)
                                          |)
                                        |)
                                      |)))
                                ]
                              |)))
                          |) in
                        let~ _ :=
                          M.write (|
                            s,
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::num::dec2flt::common::ByteSlice",
                                Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                [],
                                "parse_digits",
                                [ Ty.function [ Ty.tuple [ Ty.path "u8" ] ] (Ty.tuple []) ]
                              |),
                              [
                                M.read (| s |);
                                M.closure
                                  (fun γ =>
                                    ltac:(M.monadic
                                      match γ with
                                      | [ α0 ] =>
                                        ltac:(M.monadic
                                          (M.match_operator (|
                                            M.alloc (| α0 |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let digit := M.copy (| γ |) in
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path
                                                        "core::num::dec2flt::decimal::Decimal",
                                                      "try_add_digit",
                                                      []
                                                    |),
                                                    [ d; M.read (| digit |) ]
                                                  |)))
                                            ]
                                          |)))
                                      | _ => M.impossible "wrong number of arguments"
                                      end))
                              ]
                            |)
                          |) in
                        let~ _ :=
                          M.write (|
                            M.SubPointer.get_struct_record_field (|
                              d,
                              "core::num::dec2flt::decimal::Decimal",
                              "decimal_point"
                            |),
                            BinOp.Wrap.sub (|
                              M.rust_cast
                                (M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                    "len",
                                    []
                                  |),
                                  [ M.read (| s |) ]
                                |)),
                              M.rust_cast
                                (M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                    "len",
                                    []
                                  |),
                                  [ M.read (| first |) ]
                                |))
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.ne (|
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    d,
                                    "core::num::dec2flt::decimal::Decimal",
                                    "num_digits"
                                  |)
                                |),
                                Value.Integer IntegerKind.Usize 0
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ n_trailing_zeros := M.alloc (| Value.Integer IntegerKind.Usize 0 |) in
                        let~ _ :=
                          M.use
                            (M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::iter::traits::collect::IntoIterator",
                                    Ty.apply
                                      (Ty.path "core::iter::adapters::rev::Rev")
                                      []
                                      [
                                        Ty.apply
                                          (Ty.path "core::slice::iter::Iter")
                                          []
                                          [ Ty.path "u8" ]
                                      ],
                                    [],
                                    "into_iter",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        Ty.apply
                                          (Ty.path "core::slice::iter::Iter")
                                          []
                                          [ Ty.path "u8" ],
                                        [],
                                        "rev",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                            "iter",
                                            []
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::index::Index",
                                                Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                                [
                                                  Ty.apply
                                                    (Ty.path "core::ops::range::RangeTo")
                                                    []
                                                    [ Ty.path "usize" ]
                                                ],
                                                "index",
                                                []
                                              |),
                                              [
                                                M.read (| start |);
                                                Value.StructRecord
                                                  "core::ops::range::RangeTo"
                                                  [
                                                    ("end_",
                                                      BinOp.Wrap.sub (|
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.apply
                                                              (Ty.path "slice")
                                                              []
                                                              [ Ty.path "u8" ],
                                                            "len",
                                                            []
                                                          |),
                                                          [ M.read (| start |) ]
                                                        |),
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.apply
                                                              (Ty.path "slice")
                                                              []
                                                              [ Ty.path "u8" ],
                                                            "len",
                                                            []
                                                          |),
                                                          [ M.read (| s |) ]
                                                        |)
                                                      |))
                                                  ]
                                              ]
                                            |)
                                          ]
                                        |)
                                      ]
                                    |)
                                  ]
                                |)
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let iter := M.copy (| γ |) in
                                    M.loop (|
                                      ltac:(M.monadic
                                        (let~ _ :=
                                          M.match_operator (|
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::iter::traits::iterator::Iterator",
                                                  Ty.apply
                                                    (Ty.path "core::iter::adapters::rev::Rev")
                                                    []
                                                    [
                                                      Ty.apply
                                                        (Ty.path "core::slice::iter::Iter")
                                                        []
                                                        [ Ty.path "u8" ]
                                                    ],
                                                  [],
                                                  "next",
                                                  []
                                                |),
                                                [ iter ]
                                              |)
                                            |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let _ :=
                                                    M.is_struct_tuple (|
                                                      γ,
                                                      "core::option::Option::None"
                                                    |) in
                                                  M.alloc (|
                                                    M.never_to_any (| M.read (| M.break (||) |) |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::option::Option::Some",
                                                      0
                                                    |) in
                                                  let γ0_0 := M.read (| γ0_0 |) in
                                                  let c := M.copy (| γ0_0 |) in
                                                  M.match_operator (|
                                                    M.alloc (| Value.Tuple [] |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ :=
                                                            M.use
                                                              (M.alloc (|
                                                                BinOp.eq (|
                                                                  M.read (| c |),
                                                                  M.read (| UnsupportedLiteral |)
                                                                |)
                                                              |)) in
                                                          let _ :=
                                                            M.is_constant_or_break_match (|
                                                              M.read (| γ |),
                                                              Value.Bool true
                                                            |) in
                                                          let~ _ :=
                                                            let β := n_trailing_zeros in
                                                            M.write (|
                                                              β,
                                                              BinOp.Wrap.add (|
                                                                M.read (| β |),
                                                                Value.Integer IntegerKind.Usize 1
                                                              |)
                                                            |) in
                                                          M.alloc (| Value.Tuple [] |)));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (M.match_operator (|
                                                            M.alloc (| Value.Tuple [] |),
                                                            [
                                                              fun γ =>
                                                                ltac:(M.monadic
                                                                  (let γ :=
                                                                    M.use
                                                                      (M.alloc (|
                                                                        BinOp.ne (|
                                                                          M.read (| c |),
                                                                          M.read (|
                                                                            UnsupportedLiteral
                                                                          |)
                                                                        |)
                                                                      |)) in
                                                                  let _ :=
                                                                    M.is_constant_or_break_match (|
                                                                      M.read (| γ |),
                                                                      Value.Bool true
                                                                    |) in
                                                                  M.alloc (|
                                                                    M.never_to_any (|
                                                                      M.read (| M.break (||) |)
                                                                    |)
                                                                  |)));
                                                              fun γ =>
                                                                ltac:(M.monadic
                                                                  (M.alloc (| Value.Tuple [] |)))
                                                            ]
                                                          |)))
                                                    ]
                                                  |)))
                                            ]
                                          |) in
                                        M.alloc (| Value.Tuple [] |)))
                                    |)))
                              ]
                            |)) in
                        let~ _ :=
                          let β :=
                            M.SubPointer.get_struct_record_field (|
                              d,
                              "core::num::dec2flt::decimal::Decimal",
                              "decimal_point"
                            |) in
                          M.write (|
                            β,
                            BinOp.Wrap.add (|
                              M.read (| β |),
                              M.rust_cast (M.read (| n_trailing_zeros |))
                            |)
                          |) in
                        let~ _ :=
                          let β :=
                            M.SubPointer.get_struct_record_field (|
                              d,
                              "core::num::dec2flt::decimal::Decimal",
                              "num_digits"
                            |) in
                          M.write (|
                            β,
                            BinOp.Wrap.sub (| M.read (| β |), M.read (| n_trailing_zeros |) |)
                          |) in
                        let~ _ :=
                          let β :=
                            M.SubPointer.get_struct_record_field (|
                              d,
                              "core::num::dec2flt::decimal::Decimal",
                              "decimal_point"
                            |) in
                          M.write (|
                            β,
                            BinOp.Wrap.add (|
                              M.read (| β |),
                              M.rust_cast
                                (M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    d,
                                    "core::num::dec2flt::decimal::Decimal",
                                    "num_digits"
                                  |)
                                |))
                            |)
                          |) in
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      BinOp.gt (|
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            d,
                                            "core::num::dec2flt::decimal::Decimal",
                                            "num_digits"
                                          |)
                                        |),
                                        M.read (|
                                          M.get_constant (|
                                            "core::num::dec2flt::decimal::MAX_DIGITS"
                                          |)
                                        |)
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      d,
                                      "core::num::dec2flt::decimal::Decimal",
                                      "truncated"
                                    |),
                                    Value.Bool true
                                  |) in
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      d,
                                      "core::num::dec2flt::decimal::Decimal",
                                      "num_digits"
                                    |),
                                    M.read (|
                                      M.get_constant (| "core::num::dec2flt::decimal::MAX_DIGITS" |)
                                    |)
                                  |) in
                                M.alloc (| Value.Tuple [] |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                "split_first",
                                []
                              |),
                              [ M.read (| s |) ]
                            |)
                          |) in
                        let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                        let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                        let γ1_0 := M.read (| γ1_0 |) in
                        let ch := M.copy (| γ1_0 |) in
                        let s_next := M.copy (| γ1_1 |) in
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      LogicalOp.or (|
                                        BinOp.eq (|
                                          M.read (| ch |),
                                          M.read (| UnsupportedLiteral |)
                                        |),
                                        ltac:(M.monadic
                                          (BinOp.eq (|
                                            M.read (| ch |),
                                            M.read (| UnsupportedLiteral |)
                                          |)))
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                let~ _ := M.write (| s, M.read (| s_next |) |) in
                                let~ neg_exp := M.alloc (| Value.Bool false |) in
                                let~ _ :=
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                                  "split_first",
                                                  []
                                                |),
                                                [ M.read (| s |) ]
                                              |)
                                            |) in
                                          let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                          let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                          let γ1_0 := M.read (| γ1_0 |) in
                                          let ch := M.copy (| γ1_0 |) in
                                          let s_next := M.copy (| γ1_1 |) in
                                          let~ _ :=
                                            M.write (|
                                              neg_exp,
                                              BinOp.eq (|
                                                M.read (| ch |),
                                                M.read (| UnsupportedLiteral |)
                                              |)
                                            |) in
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.use
                                                      (M.alloc (|
                                                        LogicalOp.or (|
                                                          BinOp.eq (|
                                                            M.read (| ch |),
                                                            M.read (| UnsupportedLiteral |)
                                                          |),
                                                          ltac:(M.monadic
                                                            (BinOp.eq (|
                                                              M.read (| ch |),
                                                              M.read (| UnsupportedLiteral |)
                                                            |)))
                                                        |)
                                                      |)) in
                                                  let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Bool true
                                                    |) in
                                                  let~ _ := M.write (| s, M.read (| s_next |) |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                let~ exp_num := M.alloc (| Value.Integer IntegerKind.I32 0 |) in
                                let~ _ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::num::dec2flt::common::ByteSlice",
                                        Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                        [],
                                        "parse_digits",
                                        [ Ty.function [ Ty.tuple [ Ty.path "u8" ] ] (Ty.tuple []) ]
                                      |),
                                      [
                                        M.read (| s |);
                                        M.closure
                                          (fun γ =>
                                            ltac:(M.monadic
                                              match γ with
                                              | [ α0 ] =>
                                                ltac:(M.monadic
                                                  (M.match_operator (|
                                                    M.alloc (| α0 |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let digit := M.copy (| γ |) in
                                                          M.read (|
                                                            M.match_operator (|
                                                              M.alloc (| Value.Tuple [] |),
                                                              [
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (let γ :=
                                                                      M.use
                                                                        (M.alloc (|
                                                                          BinOp.lt (|
                                                                            M.read (| exp_num |),
                                                                            Value.Integer
                                                                              IntegerKind.I32
                                                                              65536
                                                                          |)
                                                                        |)) in
                                                                    let _ :=
                                                                      M.is_constant_or_break_match (|
                                                                        M.read (| γ |),
                                                                        Value.Bool true
                                                                      |) in
                                                                    let~ _ :=
                                                                      M.write (|
                                                                        exp_num,
                                                                        BinOp.Wrap.add (|
                                                                          BinOp.Wrap.mul (|
                                                                            Value.Integer
                                                                              IntegerKind.I32
                                                                              10,
                                                                            M.read (| exp_num |)
                                                                          |),
                                                                          M.rust_cast
                                                                            (M.read (| digit |))
                                                                        |)
                                                                      |) in
                                                                    M.alloc (| Value.Tuple [] |)));
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (M.alloc (| Value.Tuple [] |)))
                                                              ]
                                                            |)
                                                          |)))
                                                    ]
                                                  |)))
                                              | _ => M.impossible "wrong number of arguments"
                                              end))
                                      ]
                                    |)
                                  |) in
                                let~ _ :=
                                  let β :=
                                    M.SubPointer.get_struct_record_field (|
                                      d,
                                      "core::num::dec2flt::decimal::Decimal",
                                      "decimal_point"
                                    |) in
                                  M.write (|
                                    β,
                                    BinOp.Wrap.add (|
                                      M.read (| β |),
                                      M.read (|
                                        M.match_operator (|
                                          M.alloc (| Value.Tuple [] |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let γ := M.use neg_exp in
                                                let _ :=
                                                  M.is_constant_or_break_match (|
                                                    M.read (| γ |),
                                                    Value.Bool true
                                                  |) in
                                                M.alloc (| UnOp.neg (| M.read (| exp_num |) |) |)));
                                            fun γ => ltac:(M.monadic exp_num)
                                          ]
                                        |)
                                      |)
                                    |)
                                  |) in
                                M.alloc (| Value.Tuple [] |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.use
                  (M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::collect::IntoIterator",
                          Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                          [],
                          "into_iter",
                          []
                        |),
                        [
                          Value.StructRecord
                            "core::ops::range::Range"
                            [
                              ("start",
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    d,
                                    "core::num::dec2flt::decimal::Decimal",
                                    "num_digits"
                                  |)
                                |));
                              ("end_",
                                M.read (|
                                  M.get_constant (|
                                    "core::num::dec2flt::decimal::MAX_DIGITS_WITHOUT_OVERFLOW"
                                  |)
                                |))
                            ]
                        ]
                      |)
                    |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let iter := M.copy (| γ |) in
                          M.loop (|
                            ltac:(M.monadic
                              (let~ _ :=
                                M.match_operator (|
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        Ty.apply
                                          (Ty.path "core::ops::range::Range")
                                          []
                                          [ Ty.path "usize" ],
                                        [],
                                        "next",
                                        []
                                      |),
                                      [ iter ]
                                    |)
                                  |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let _ :=
                                          M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                        M.alloc (|
                                          M.never_to_any (| M.read (| M.break (||) |) |)
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ0_0 :=
                                          M.SubPointer.get_struct_tuple_field (|
                                            γ,
                                            "core::option::Option::Some",
                                            0
                                          |) in
                                        let i := M.copy (| γ0_0 |) in
                                        let~ _ :=
                                          M.write (|
                                            M.SubPointer.get_array_field (|
                                              M.SubPointer.get_struct_record_field (|
                                                d,
                                                "core::num::dec2flt::decimal::Decimal",
                                                "digits"
                                              |),
                                              i
                                            |),
                                            Value.Integer IntegerKind.U8 0
                                          |) in
                                        M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              M.alloc (| Value.Tuple [] |)))
                          |)))
                    ]
                  |)) in
              d
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_parse_decimal :
        M.IsFunction "core::num::dec2flt::decimal::parse_decimal" parse_decimal.
      
      (*
      fn number_of_digits_decimal_left_shift(d: &Decimal, mut shift: usize) -> usize {
          #[rustfmt::skip]
          const TABLE: [u16; 65] = [
              0x0000, 0x0800, 0x0801, 0x0803, 0x1006, 0x1009, 0x100D, 0x1812, 0x1817, 0x181D, 0x2024,
              0x202B, 0x2033, 0x203C, 0x2846, 0x2850, 0x285B, 0x3067, 0x3073, 0x3080, 0x388E, 0x389C,
              0x38AB, 0x38BB, 0x40CC, 0x40DD, 0x40EF, 0x4902, 0x4915, 0x4929, 0x513E, 0x5153, 0x5169,
              0x5180, 0x5998, 0x59B0, 0x59C9, 0x61E3, 0x61FD, 0x6218, 0x6A34, 0x6A50, 0x6A6D, 0x6A8B,
              0x72AA, 0x72C9, 0x72E9, 0x7B0A, 0x7B2B, 0x7B4D, 0x8370, 0x8393, 0x83B7, 0x83DC, 0x8C02,
              0x8C28, 0x8C4F, 0x9477, 0x949F, 0x94C8, 0x9CF2, 0x051C, 0x051C, 0x051C, 0x051C,
          ];
          #[rustfmt::skip]
          const TABLE_POW5: [u8; 0x051C] = [
              5, 2, 5, 1, 2, 5, 6, 2, 5, 3, 1, 2, 5, 1, 5, 6, 2, 5, 7, 8, 1, 2, 5, 3, 9, 0, 6, 2, 5, 1,
              9, 5, 3, 1, 2, 5, 9, 7, 6, 5, 6, 2, 5, 4, 8, 8, 2, 8, 1, 2, 5, 2, 4, 4, 1, 4, 0, 6, 2, 5,
              1, 2, 2, 0, 7, 0, 3, 1, 2, 5, 6, 1, 0, 3, 5, 1, 5, 6, 2, 5, 3, 0, 5, 1, 7, 5, 7, 8, 1, 2,
              5, 1, 5, 2, 5, 8, 7, 8, 9, 0, 6, 2, 5, 7, 6, 2, 9, 3, 9, 4, 5, 3, 1, 2, 5, 3, 8, 1, 4, 6,
              9, 7, 2, 6, 5, 6, 2, 5, 1, 9, 0, 7, 3, 4, 8, 6, 3, 2, 8, 1, 2, 5, 9, 5, 3, 6, 7, 4, 3, 1,
              6, 4, 0, 6, 2, 5, 4, 7, 6, 8, 3, 7, 1, 5, 8, 2, 0, 3, 1, 2, 5, 2, 3, 8, 4, 1, 8, 5, 7, 9,
              1, 0, 1, 5, 6, 2, 5, 1, 1, 9, 2, 0, 9, 2, 8, 9, 5, 5, 0, 7, 8, 1, 2, 5, 5, 9, 6, 0, 4, 6,
              4, 4, 7, 7, 5, 3, 9, 0, 6, 2, 5, 2, 9, 8, 0, 2, 3, 2, 2, 3, 8, 7, 6, 9, 5, 3, 1, 2, 5, 1,
              4, 9, 0, 1, 1, 6, 1, 1, 9, 3, 8, 4, 7, 6, 5, 6, 2, 5, 7, 4, 5, 0, 5, 8, 0, 5, 9, 6, 9, 2,
              3, 8, 2, 8, 1, 2, 5, 3, 7, 2, 5, 2, 9, 0, 2, 9, 8, 4, 6, 1, 9, 1, 4, 0, 6, 2, 5, 1, 8, 6,
              2, 6, 4, 5, 1, 4, 9, 2, 3, 0, 9, 5, 7, 0, 3, 1, 2, 5, 9, 3, 1, 3, 2, 2, 5, 7, 4, 6, 1, 5,
              4, 7, 8, 5, 1, 5, 6, 2, 5, 4, 6, 5, 6, 6, 1, 2, 8, 7, 3, 0, 7, 7, 3, 9, 2, 5, 7, 8, 1, 2,
              5, 2, 3, 2, 8, 3, 0, 6, 4, 3, 6, 5, 3, 8, 6, 9, 6, 2, 8, 9, 0, 6, 2, 5, 1, 1, 6, 4, 1, 5,
              3, 2, 1, 8, 2, 6, 9, 3, 4, 8, 1, 4, 4, 5, 3, 1, 2, 5, 5, 8, 2, 0, 7, 6, 6, 0, 9, 1, 3, 4,
              6, 7, 4, 0, 7, 2, 2, 6, 5, 6, 2, 5, 2, 9, 1, 0, 3, 8, 3, 0, 4, 5, 6, 7, 3, 3, 7, 0, 3, 6,
              1, 3, 2, 8, 1, 2, 5, 1, 4, 5, 5, 1, 9, 1, 5, 2, 2, 8, 3, 6, 6, 8, 5, 1, 8, 0, 6, 6, 4, 0,
              6, 2, 5, 7, 2, 7, 5, 9, 5, 7, 6, 1, 4, 1, 8, 3, 4, 2, 5, 9, 0, 3, 3, 2, 0, 3, 1, 2, 5, 3,
              6, 3, 7, 9, 7, 8, 8, 0, 7, 0, 9, 1, 7, 1, 2, 9, 5, 1, 6, 6, 0, 1, 5, 6, 2, 5, 1, 8, 1, 8,
              9, 8, 9, 4, 0, 3, 5, 4, 5, 8, 5, 6, 4, 7, 5, 8, 3, 0, 0, 7, 8, 1, 2, 5, 9, 0, 9, 4, 9, 4,
              7, 0, 1, 7, 7, 2, 9, 2, 8, 2, 3, 7, 9, 1, 5, 0, 3, 9, 0, 6, 2, 5, 4, 5, 4, 7, 4, 7, 3, 5,
              0, 8, 8, 6, 4, 6, 4, 1, 1, 8, 9, 5, 7, 5, 1, 9, 5, 3, 1, 2, 5, 2, 2, 7, 3, 7, 3, 6, 7, 5,
              4, 4, 3, 2, 3, 2, 0, 5, 9, 4, 7, 8, 7, 5, 9, 7, 6, 5, 6, 2, 5, 1, 1, 3, 6, 8, 6, 8, 3, 7,
              7, 2, 1, 6, 1, 6, 0, 2, 9, 7, 3, 9, 3, 7, 9, 8, 8, 2, 8, 1, 2, 5, 5, 6, 8, 4, 3, 4, 1, 8,
              8, 6, 0, 8, 0, 8, 0, 1, 4, 8, 6, 9, 6, 8, 9, 9, 4, 1, 4, 0, 6, 2, 5, 2, 8, 4, 2, 1, 7, 0,
              9, 4, 3, 0, 4, 0, 4, 0, 0, 7, 4, 3, 4, 8, 4, 4, 9, 7, 0, 7, 0, 3, 1, 2, 5, 1, 4, 2, 1, 0,
              8, 5, 4, 7, 1, 5, 2, 0, 2, 0, 0, 3, 7, 1, 7, 4, 2, 2, 4, 8, 5, 3, 5, 1, 5, 6, 2, 5, 7, 1,
              0, 5, 4, 2, 7, 3, 5, 7, 6, 0, 1, 0, 0, 1, 8, 5, 8, 7, 1, 1, 2, 4, 2, 6, 7, 5, 7, 8, 1, 2,
              5, 3, 5, 5, 2, 7, 1, 3, 6, 7, 8, 8, 0, 0, 5, 0, 0, 9, 2, 9, 3, 5, 5, 6, 2, 1, 3, 3, 7, 8,
              9, 0, 6, 2, 5, 1, 7, 7, 6, 3, 5, 6, 8, 3, 9, 4, 0, 0, 2, 5, 0, 4, 6, 4, 6, 7, 7, 8, 1, 0,
              6, 6, 8, 9, 4, 5, 3, 1, 2, 5, 8, 8, 8, 1, 7, 8, 4, 1, 9, 7, 0, 0, 1, 2, 5, 2, 3, 2, 3, 3,
              8, 9, 0, 5, 3, 3, 4, 4, 7, 2, 6, 5, 6, 2, 5, 4, 4, 4, 0, 8, 9, 2, 0, 9, 8, 5, 0, 0, 6, 2,
              6, 1, 6, 1, 6, 9, 4, 5, 2, 6, 6, 7, 2, 3, 6, 3, 2, 8, 1, 2, 5, 2, 2, 2, 0, 4, 4, 6, 0, 4,
              9, 2, 5, 0, 3, 1, 3, 0, 8, 0, 8, 4, 7, 2, 6, 3, 3, 3, 6, 1, 8, 1, 6, 4, 0, 6, 2, 5, 1, 1,
              1, 0, 2, 2, 3, 0, 2, 4, 6, 2, 5, 1, 5, 6, 5, 4, 0, 4, 2, 3, 6, 3, 1, 6, 6, 8, 0, 9, 0, 8,
              2, 0, 3, 1, 2, 5, 5, 5, 5, 1, 1, 1, 5, 1, 2, 3, 1, 2, 5, 7, 8, 2, 7, 0, 2, 1, 1, 8, 1, 5,
              8, 3, 4, 0, 4, 5, 4, 1, 0, 1, 5, 6, 2, 5, 2, 7, 7, 5, 5, 5, 7, 5, 6, 1, 5, 6, 2, 8, 9, 1,
              3, 5, 1, 0, 5, 9, 0, 7, 9, 1, 7, 0, 2, 2, 7, 0, 5, 0, 7, 8, 1, 2, 5, 1, 3, 8, 7, 7, 7, 8,
              7, 8, 0, 7, 8, 1, 4, 4, 5, 6, 7, 5, 5, 2, 9, 5, 3, 9, 5, 8, 5, 1, 1, 3, 5, 2, 5, 3, 9, 0,
              6, 2, 5, 6, 9, 3, 8, 8, 9, 3, 9, 0, 3, 9, 0, 7, 2, 2, 8, 3, 7, 7, 6, 4, 7, 6, 9, 7, 9, 2,
              5, 5, 6, 7, 6, 2, 6, 9, 5, 3, 1, 2, 5, 3, 4, 6, 9, 4, 4, 6, 9, 5, 1, 9, 5, 3, 6, 1, 4, 1,
              8, 8, 8, 2, 3, 8, 4, 8, 9, 6, 2, 7, 8, 3, 8, 1, 3, 4, 7, 6, 5, 6, 2, 5, 1, 7, 3, 4, 7, 2,
              3, 4, 7, 5, 9, 7, 6, 8, 0, 7, 0, 9, 4, 4, 1, 1, 9, 2, 4, 4, 8, 1, 3, 9, 1, 9, 0, 6, 7, 3,
              8, 2, 8, 1, 2, 5, 8, 6, 7, 3, 6, 1, 7, 3, 7, 9, 8, 8, 4, 0, 3, 5, 4, 7, 2, 0, 5, 9, 6, 2,
              2, 4, 0, 6, 9, 5, 9, 5, 3, 3, 6, 9, 1, 4, 0, 6, 2, 5,
          ];
      
          shift &= 63;
          let x_a = TABLE[shift];
          let x_b = TABLE[shift + 1];
          let num_new_digits = (x_a >> 11) as _;
          let pow5_a = (0x7FF & x_a) as usize;
          let pow5_b = (0x7FF & x_b) as usize;
          let pow5 = &TABLE_POW5[pow5_a..];
          for (i, &p5) in pow5.iter().enumerate().take(pow5_b - pow5_a) {
              if i >= d.num_digits {
                  return num_new_digits - 1;
              } else if d.digits[i] == p5 {
                  continue;
              } else if d.digits[i] < p5 {
                  return num_new_digits - 1;
              } else {
                  return num_new_digits;
              }
          }
          num_new_digits
      }
      *)
      Definition number_of_digits_decimal_left_shift
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [], [ d; shift ] =>
          ltac:(M.monadic
            (let d := M.alloc (| d |) in
            let shift := M.alloc (| shift |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    let β := shift in
                    M.write (|
                      β,
                      BinOp.bit_and (M.read (| β |)) (Value.Integer IntegerKind.Usize 63)
                    |) in
                  let~ x_a :=
                    M.copy (|
                      M.SubPointer.get_array_field (|
                        M.get_constant (|
                          "core::num::dec2flt::decimal::number_of_digits_decimal_left_shift::TABLE"
                        |),
                        shift
                      |)
                    |) in
                  let~ x_b :=
                    M.copy (|
                      M.SubPointer.get_array_field (|
                        M.get_constant (|
                          "core::num::dec2flt::decimal::number_of_digits_decimal_left_shift::TABLE"
                        |),
                        M.alloc (|
                          BinOp.Wrap.add (| M.read (| shift |), Value.Integer IntegerKind.Usize 1 |)
                        |)
                      |)
                    |) in
                  let~ num_new_digits :=
                    M.alloc (|
                      M.rust_cast
                        (BinOp.Wrap.shr (| M.read (| x_a |), Value.Integer IntegerKind.I32 11 |))
                    |) in
                  let~ pow5_a :=
                    M.alloc (|
                      M.rust_cast
                        (BinOp.bit_and (Value.Integer IntegerKind.U16 2047) (M.read (| x_a |)))
                    |) in
                  let~ pow5_b :=
                    M.alloc (|
                      M.rust_cast
                        (BinOp.bit_and (Value.Integer IntegerKind.U16 2047) (M.read (| x_b |)))
                    |) in
                  let~ pow5 :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::index::Index",
                          Ty.apply
                            (Ty.path "array")
                            [ Value.Integer IntegerKind.Usize 1308 ]
                            [ Ty.path "u8" ],
                          [ Ty.apply (Ty.path "core::ops::range::RangeFrom") [] [ Ty.path "usize" ]
                          ],
                          "index",
                          []
                        |),
                        [
                          M.get_constant (|
                            "core::num::dec2flt::decimal::number_of_digits_decimal_left_shift::TABLE_POW5"
                          |);
                          Value.StructRecord
                            "core::ops::range::RangeFrom"
                            [ ("start", M.read (| pow5_a |)) ]
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.use
                      (M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::collect::IntoIterator",
                              Ty.apply
                                (Ty.path "core::iter::adapters::take::Take")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "core::iter::adapters::enumerate::Enumerate")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "core::slice::iter::Iter")
                                        []
                                        [ Ty.path "u8" ]
                                    ]
                                ],
                              [],
                              "into_iter",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::iter::traits::iterator::Iterator",
                                  Ty.apply
                                    (Ty.path "core::iter::adapters::enumerate::Enumerate")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "core::slice::iter::Iter")
                                        []
                                        [ Ty.path "u8" ]
                                    ],
                                  [],
                                  "take",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      Ty.apply
                                        (Ty.path "core::slice::iter::Iter")
                                        []
                                        [ Ty.path "u8" ],
                                      [],
                                      "enumerate",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                          "iter",
                                          []
                                        |),
                                        [ M.read (| pow5 |) ]
                                      |)
                                    ]
                                  |);
                                  BinOp.Wrap.sub (| M.read (| pow5_b |), M.read (| pow5_a |) |)
                                ]
                              |)
                            ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let iter := M.copy (| γ |) in
                              M.loop (|
                                ltac:(M.monadic
                                  (let~ _ :=
                                    M.match_operator (|
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::iter::traits::iterator::Iterator",
                                            Ty.apply
                                              (Ty.path "core::iter::adapters::take::Take")
                                              []
                                              [
                                                Ty.apply
                                                  (Ty.path
                                                    "core::iter::adapters::enumerate::Enumerate")
                                                  []
                                                  [
                                                    Ty.apply
                                                      (Ty.path "core::slice::iter::Iter")
                                                      []
                                                      [ Ty.path "u8" ]
                                                  ]
                                              ],
                                            [],
                                            "next",
                                            []
                                          |),
                                          [ iter ]
                                        |)
                                      |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let _ :=
                                              M.is_struct_tuple (|
                                                γ,
                                                "core::option::Option::None"
                                              |) in
                                            M.alloc (|
                                              M.never_to_any (| M.read (| M.break (||) |) |)
                                            |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ0_0 :=
                                              M.SubPointer.get_struct_tuple_field (|
                                                γ,
                                                "core::option::Option::Some",
                                                0
                                              |) in
                                            let γ1_0 :=
                                              M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                            let γ1_1 :=
                                              M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                            let i := M.copy (| γ1_0 |) in
                                            let γ1_1 := M.read (| γ1_1 |) in
                                            let p5 := M.copy (| γ1_1 |) in
                                            M.match_operator (|
                                              M.alloc (| Value.Tuple [] |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ :=
                                                      M.use
                                                        (M.alloc (|
                                                          BinOp.ge (|
                                                            M.read (| i |),
                                                            M.read (|
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.read (| d |),
                                                                "core::num::dec2flt::decimal::Decimal",
                                                                "num_digits"
                                                              |)
                                                            |)
                                                          |)
                                                        |)) in
                                                    let _ :=
                                                      M.is_constant_or_break_match (|
                                                        M.read (| γ |),
                                                        Value.Bool true
                                                      |) in
                                                    M.alloc (|
                                                      M.never_to_any (|
                                                        M.read (|
                                                          M.return_ (|
                                                            BinOp.Wrap.sub (|
                                                              M.read (| num_new_digits |),
                                                              Value.Integer IntegerKind.Usize 1
                                                            |)
                                                          |)
                                                        |)
                                                      |)
                                                    |)));
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (M.match_operator (|
                                                      M.alloc (| Value.Tuple [] |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ :=
                                                              M.use
                                                                (M.alloc (|
                                                                  BinOp.eq (|
                                                                    M.read (|
                                                                      M.SubPointer.get_array_field (|
                                                                        M.SubPointer.get_struct_record_field (|
                                                                          M.read (| d |),
                                                                          "core::num::dec2flt::decimal::Decimal",
                                                                          "digits"
                                                                        |),
                                                                        i
                                                                      |)
                                                                    |),
                                                                    M.read (| p5 |)
                                                                  |)
                                                                |)) in
                                                            let _ :=
                                                              M.is_constant_or_break_match (|
                                                                M.read (| γ |),
                                                                Value.Bool true
                                                              |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (| M.continue (||) |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.match_operator (|
                                                              M.alloc (| Value.Tuple [] |),
                                                              [
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (let γ :=
                                                                      M.use
                                                                        (M.alloc (|
                                                                          BinOp.lt (|
                                                                            M.read (|
                                                                              M.SubPointer.get_array_field (|
                                                                                M.SubPointer.get_struct_record_field (|
                                                                                  M.read (| d |),
                                                                                  "core::num::dec2flt::decimal::Decimal",
                                                                                  "digits"
                                                                                |),
                                                                                i
                                                                              |)
                                                                            |),
                                                                            M.read (| p5 |)
                                                                          |)
                                                                        |)) in
                                                                    let _ :=
                                                                      M.is_constant_or_break_match (|
                                                                        M.read (| γ |),
                                                                        Value.Bool true
                                                                      |) in
                                                                    M.alloc (|
                                                                      M.never_to_any (|
                                                                        M.read (|
                                                                          M.return_ (|
                                                                            BinOp.Wrap.sub (|
                                                                              M.read (|
                                                                                num_new_digits
                                                                              |),
                                                                              Value.Integer
                                                                                IntegerKind.Usize
                                                                                1
                                                                            |)
                                                                          |)
                                                                        |)
                                                                      |)
                                                                    |)));
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (M.alloc (|
                                                                      M.never_to_any (|
                                                                        M.read (|
                                                                          M.return_ (|
                                                                            M.read (|
                                                                              num_new_digits
                                                                            |)
                                                                          |)
                                                                        |)
                                                                      |)
                                                                    |)))
                                                              ]
                                                            |)))
                                                      ]
                                                    |)))
                                              ]
                                            |)))
                                      ]
                                    |) in
                                  M.alloc (| Value.Tuple [] |)))
                              |)))
                        ]
                      |)) in
                  num_new_digits
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_number_of_digits_decimal_left_shift :
        M.IsFunction
          "core::num::dec2flt::decimal::number_of_digits_decimal_left_shift"
          number_of_digits_decimal_left_shift.
      
      Module number_of_digits_decimal_left_shift.
        Definition value_TABLE : Value.t :=
          M.run
            ltac:(M.monadic
              (M.alloc (|
                Value.Array
                  [
                    Value.Integer IntegerKind.U16 0;
                    Value.Integer IntegerKind.U16 2048;
                    Value.Integer IntegerKind.U16 2049;
                    Value.Integer IntegerKind.U16 2051;
                    Value.Integer IntegerKind.U16 4102;
                    Value.Integer IntegerKind.U16 4105;
                    Value.Integer IntegerKind.U16 4109;
                    Value.Integer IntegerKind.U16 6162;
                    Value.Integer IntegerKind.U16 6167;
                    Value.Integer IntegerKind.U16 6173;
                    Value.Integer IntegerKind.U16 8228;
                    Value.Integer IntegerKind.U16 8235;
                    Value.Integer IntegerKind.U16 8243;
                    Value.Integer IntegerKind.U16 8252;
                    Value.Integer IntegerKind.U16 10310;
                    Value.Integer IntegerKind.U16 10320;
                    Value.Integer IntegerKind.U16 10331;
                    Value.Integer IntegerKind.U16 12391;
                    Value.Integer IntegerKind.U16 12403;
                    Value.Integer IntegerKind.U16 12416;
                    Value.Integer IntegerKind.U16 14478;
                    Value.Integer IntegerKind.U16 14492;
                    Value.Integer IntegerKind.U16 14507;
                    Value.Integer IntegerKind.U16 14523;
                    Value.Integer IntegerKind.U16 16588;
                    Value.Integer IntegerKind.U16 16605;
                    Value.Integer IntegerKind.U16 16623;
                    Value.Integer IntegerKind.U16 18690;
                    Value.Integer IntegerKind.U16 18709;
                    Value.Integer IntegerKind.U16 18729;
                    Value.Integer IntegerKind.U16 20798;
                    Value.Integer IntegerKind.U16 20819;
                    Value.Integer IntegerKind.U16 20841;
                    Value.Integer IntegerKind.U16 20864;
                    Value.Integer IntegerKind.U16 22936;
                    Value.Integer IntegerKind.U16 22960;
                    Value.Integer IntegerKind.U16 22985;
                    Value.Integer IntegerKind.U16 25059;
                    Value.Integer IntegerKind.U16 25085;
                    Value.Integer IntegerKind.U16 25112;
                    Value.Integer IntegerKind.U16 27188;
                    Value.Integer IntegerKind.U16 27216;
                    Value.Integer IntegerKind.U16 27245;
                    Value.Integer IntegerKind.U16 27275;
                    Value.Integer IntegerKind.U16 29354;
                    Value.Integer IntegerKind.U16 29385;
                    Value.Integer IntegerKind.U16 29417;
                    Value.Integer IntegerKind.U16 31498;
                    Value.Integer IntegerKind.U16 31531;
                    Value.Integer IntegerKind.U16 31565;
                    Value.Integer IntegerKind.U16 33648;
                    Value.Integer IntegerKind.U16 33683;
                    Value.Integer IntegerKind.U16 33719;
                    Value.Integer IntegerKind.U16 33756;
                    Value.Integer IntegerKind.U16 35842;
                    Value.Integer IntegerKind.U16 35880;
                    Value.Integer IntegerKind.U16 35919;
                    Value.Integer IntegerKind.U16 38007;
                    Value.Integer IntegerKind.U16 38047;
                    Value.Integer IntegerKind.U16 38088;
                    Value.Integer IntegerKind.U16 40178;
                    Value.Integer IntegerKind.U16 1308;
                    Value.Integer IntegerKind.U16 1308;
                    Value.Integer IntegerKind.U16 1308;
                    Value.Integer IntegerKind.U16 1308
                  ]
              |))).
        
        Definition value_TABLE_POW5 : Value.t :=
          M.run
            ltac:(M.monadic
              (M.alloc (|
                Value.Array
                  [
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 8;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 7;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 5;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 3;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 9;
                    Value.Integer IntegerKind.U8 1;
                    Value.Integer IntegerKind.U8 4;
                    Value.Integer IntegerKind.U8 0;
                    Value.Integer IntegerKind.U8 6;
                    Value.Integer IntegerKind.U8 2;
                    Value.Integer IntegerKind.U8 5
                  ]
              |))).
      End number_of_digits_decimal_left_shift.
    End decimal.
  End dec2flt.
End num.
