module Compiler.NaturalMagnitudeArithmetic

import Std.Natural

-- Internal arithmetic on canonical decimal digit bytes, least significant first.
-- Zero is empty; every digit is 0..9 and the final digit is nonzero.
-- The checked owner validates external input before calling these operations.
-- Whole-value Nat conversion is only for existing unary values or bounded carries.
-- Normalization and addition assemble a BytesBuilder and materialize once;
-- repeated bytes-cons of complete suffixes would copy quadratic byte volume.
-- A carry digit uses explicit low-byte conversion of total + 246 for total
-- in 10..19, which equals total - 10. Addition preserves canonical inputs.
def magnitudeNormalize =
  (lambda unrestricted digits : Bytes .
    (bytes-builder-build
      (second
        (bytes-eliminate
          (lambda unrestricted rest : Bytes . (sigma unrestricted active : Nat . BytesBuilder))
          (pair (sigma unrestricted active : Nat . BytesBuilder) zero (bytes-builder-empty))
          (lambda unrestricted head : Byte .
            (lambda unrestricted tail : Bytes .
              (lambda unrestricted continue : (sigma unrestricted active : Nat . BytesBuilder) .
                (app
                  (nat-eliminate
                    (lambda unrestricted flag : Nat .
                      (pi unrestricted force : Nat .
                        (sigma unrestricted active : Nat . BytesBuilder)))
                    (lambda unrestricted force : Nat .
                      (pair
                        (sigma unrestricted active : Nat . BytesBuilder)
                        (succ zero)
                        (bytes-builder-append
                          (bytes-builder-chunk (bytes-cons head b""))
                          (second continue))))
                    (lambda unrestricted predecessor : Nat .
                      (lambda unrestricted induction : (pi unrestricted force : Nat . (sigma unrestricted active : Nat . BytesBuilder)) .
                        (lambda unrestricted force : Nat . continue)))
                    (Std.Natural/naturalAnd
                      (byte-equal head (byte 0))
                      (Std.Natural/naturalIsZero (first continue))))
                  zero))))
          digits))))

def magnitudeEqual =
  (lambda unrestricted left : Bytes .
    (lambda unrestricted right : Bytes .
      (bytes-equal (magnitudeNormalize left) (magnitudeNormalize right))))

def magnitudeSuccessorDigits =
  (lambda unrestricted digits : Bytes .
    (app
      (bytes-eliminate
        (lambda unrestricted rest : Bytes . (pi unrestricted force : Nat . Bytes))
        (lambda unrestricted force : Nat . (bytes 1))
        (lambda unrestricted head : Byte .
          (lambda unrestricted tail : Bytes .
            (lambda unrestricted continue : (pi unrestricted force : Nat . Bytes) .
              (lambda unrestricted force : Nat .
                (app
                  (nat-eliminate
                    (lambda unrestricted flag : Nat . (pi unrestricted force : Nat . Bytes))
                    (lambda unrestricted force : Nat .
                      (bytes-cons (nat-to-byte (succ (byte-to-nat head))) tail))
                    (lambda unrestricted predecessor : Nat .
                      (lambda unrestricted induction : (pi unrestricted force : Nat . Bytes) .
                        (lambda unrestricted force : Nat . (bytes-cons (byte 0) (continue zero)))))
                    (byte-equal head (byte 9)))
                  zero)))))
        digits)
      zero))

def magnitudeSuccessor =
  (lambda unrestricted digits : Bytes . (magnitudeSuccessorDigits (magnitudeNormalize digits)))

def magnitudePredecessor =
  (lambda unrestricted digits : Bytes .
    (magnitudeNormalize
      (app
        (bytes-eliminate
          (lambda unrestricted rest : Bytes . (pi unrestricted force : Nat . Bytes))
          (lambda unrestricted force : Nat . b"")
          (lambda unrestricted head : Byte .
            (lambda unrestricted tail : Bytes .
              (lambda unrestricted continue : (pi unrestricted force : Nat . Bytes) .
                (lambda unrestricted force : Nat .
                  (app
                    (nat-eliminate
                      (lambda unrestricted flag : Nat . (pi unrestricted force : Nat . Bytes))
                      (lambda unrestricted force : Nat .
                        (bytes-cons
                          (nat-to-byte
                            (Std.Natural/naturalSaturatingSubtract (byte-to-nat head) (succ zero)))
                          tail))
                      (lambda unrestricted predecessor : Nat .
                        (lambda unrestricted induction : (pi unrestricted force : Nat . Bytes) .
                          (lambda unrestricted force : Nat . (bytes-cons (byte 9) (continue zero)))))
                      (byte-equal head (byte 0)))
                    zero)))))
          (magnitudeNormalize digits))
        zero)))

def magnitudeFromNatural =
  (lambda unrestricted value : Nat .
    (nat-eliminate
      (lambda unrestricted count : Nat . Bytes)
      b""
      (lambda unrestricted predecessor : Nat .
        (lambda unrestricted digits : Bytes . (magnitudeSuccessorDigits digits)))
      value))

-- Evaluate decimal digits modulo 256 without constructing the whole natural.
def magnitudeByteDouble =
  (lambda unrestricted value : Byte .
    (nat-to-byte (Std.Natural/naturalAdd (byte-to-nat value) (byte-to-nat value))))

def magnitudeLowByte =
  (lambda unrestricted digits : Bytes .
    (bytes-eliminate
      (lambda unrestricted rest : Bytes . Byte)
      (byte 0)
      (lambda unrestricted head : Byte .
        (lambda unrestricted tail : Bytes .
          (lambda unrestricted continue : Byte .
            (nat-to-byte
              (Std.Natural/naturalAdd
                (byte-to-nat head)
                (Std.Natural/naturalAdd
                  (byte-to-nat (magnitudeByteDouble continue))
                  (byte-to-nat
                    (magnitudeByteDouble (magnitudeByteDouble (magnitudeByteDouble continue))))))))))
      digits))

def magnitudeCompareSameLength =
  (lambda unrestricted left : Bytes .
    (lambda unrestricted right : Bytes .
      (app
        (bytes-eliminate
          (lambda unrestricted rest : Bytes . (pi unrestricted right : Bytes . Nat))
          (lambda unrestricted right : Bytes .
            (app
              (nat-eliminate
                (lambda unrestricted flag : Nat . (pi unrestricted force : Nat . Nat))
                (lambda unrestricted force : Nat . (succ zero))
                (lambda unrestricted predecessor : Nat .
                  (lambda unrestricted induction : (pi unrestricted force : Nat . Nat) .
                    (lambda unrestricted force : Nat . zero)))
                (bytes-equal right b""))
              zero))
          (lambda unrestricted head : Byte .
            (lambda unrestricted tail : Bytes .
              (lambda unrestricted continue : (pi unrestricted right : Bytes . Nat) .
                (lambda unrestricted right : Bytes .
                  (app
                    (nat-eliminate
                      (lambda unrestricted flag : Nat . (pi unrestricted force : Nat . Nat))
                      (lambda unrestricted force : Nat .
                        (app
                          (lambda unrestricted higher : Nat .
                            (app
                              (nat-eliminate
                                (lambda unrestricted flag : Nat .
                                  (pi unrestricted force : Nat . Nat))
                                (lambda unrestricted force : Nat . higher)
                                (lambda unrestricted predecessor : Nat .
                                  (lambda unrestricted induction : (pi unrestricted force : Nat . Nat) .
                                    (lambda unrestricted force : Nat .
                                      (app
                                        (nat-eliminate
                                        (lambda unrestricted flag : Nat .
                                        (pi unrestricted force : Nat . Nat))
                                        (lambda unrestricted force : Nat .
                                        (app
                                        (nat-eliminate
                                        (lambda unrestricted flag : Nat .
                                        (pi unrestricted force : Nat . Nat))
                                        (lambda unrestricted force : Nat . (succ (succ zero)))
                                        (lambda unrestricted predecessor : Nat .
                                        (lambda unrestricted induction : (pi unrestricted force : Nat . Nat) .
                                        (lambda unrestricted force : Nat . zero)))
                                        (byte-equal head (bytes-head right)))
                                        zero))
                                        (lambda unrestricted predecessor : Nat .
                                        (lambda unrestricted induction : (pi unrestricted force : Nat . Nat) .
                                        (lambda unrestricted force : Nat . (succ zero))))
                                        (nat-less-than
                                        (byte-to-nat head)
                                        (byte-to-nat (bytes-head right))))
                                        zero))))
                                (Std.Natural/naturalIsZero higher))
                              zero))
                          (continue (bytes-tail right))))
                      (lambda unrestricted predecessor : Nat .
                        (lambda unrestricted induction : (pi unrestricted force : Nat . Nat) .
                          (lambda unrestricted force : Nat . (succ (succ zero)))))
                      (bytes-equal right b""))
                    zero)))))
          left)
        right)))

-- Internal canonical comparison can decide unequal digit lengths immediately.
-- This avoids repeatedly scanning a long divisor for shorter partial remainders.
def magnitudeCompareCanonical =
  (lambda unrestricted left : Bytes .
    (lambda unrestricted right : Bytes .
      (app
        (nat-eliminate
          (lambda unrestricted shorter : Nat . (pi unrestricted force : Nat . Nat))
          (lambda unrestricted force : Nat .
            (app
              (nat-eliminate
                (lambda unrestricted longer : Nat . (pi unrestricted force : Nat . Nat))
                (lambda unrestricted force : Nat . (magnitudeCompareSameLength left right))
                (lambda unrestricted predecessor : Nat .
                  (lambda unrestricted induction : (pi unrestricted force : Nat . Nat) .
                    (lambda unrestricted force : Nat . (succ (succ zero)))))
                (nat-less-than (bytes-length right) (bytes-length left)))
              zero))
          (lambda unrestricted predecessor : Nat .
            (lambda unrestricted induction : (pi unrestricted force : Nat . Nat) .
              (lambda unrestricted force : Nat . (succ zero))))
          (nat-less-than (bytes-length left) (bytes-length right)))
        zero)))

def magnitudeCompare =
  (lambda unrestricted left : Bytes .
    (lambda unrestricted right : Bytes .
      (magnitudeCompareCanonical (magnitudeNormalize left) (magnitudeNormalize right))))

def magnitudeLessCanonical =
  (lambda unrestricted left : Bytes .
    (lambda unrestricted right : Bytes .
      (Std.Natural/naturalEqual (magnitudeCompareCanonical left right) (succ zero))))

def magnitudeLess =
  (lambda unrestricted left : Bytes .
    (lambda unrestricted right : Bytes .
      (Std.Natural/naturalEqual (magnitudeCompare left right) (succ zero))))

def magnitudeAdd =
  (lambda unrestricted left : Bytes .
    (lambda unrestricted right : Bytes .
      (bytes-builder-build
        (app
          (bytes-eliminate
            (lambda unrestricted rest : Bytes .
              (pi unrestricted right : Bytes . (pi unrestricted carry : Nat . BytesBuilder)))
            (lambda unrestricted right : Bytes .
              (lambda unrestricted carry : Nat .
                (bytes-builder-chunk
                  (app
                    (nat-eliminate
                      (lambda unrestricted flag : Nat . (pi unrestricted force : Nat . Bytes))
                      (lambda unrestricted force : Nat . right)
                      (lambda unrestricted predecessor : Nat .
                        (lambda unrestricted induction : (pi unrestricted force : Nat . Bytes) .
                          (lambda unrestricted force : Nat . (magnitudeSuccessorDigits right))))
                      carry)
                    zero))))
            (lambda unrestricted head : Byte .
              (lambda unrestricted tail : Bytes .
                (lambda unrestricted continue : (pi unrestricted right : Bytes . (pi unrestricted carry : Nat . BytesBuilder)) .
                  (lambda unrestricted right : Bytes .
                    (lambda unrestricted carry : Nat .
                      (app
                        (lambda unrestricted total : Nat .
                          (app
                            (nat-eliminate
                              (lambda unrestricted flag : Nat .
                                (pi unrestricted force : Nat . BytesBuilder))
                              (lambda unrestricted force : Nat .
                                (bytes-builder-append
                                  (bytes-builder-chunk
                                    (bytes-cons
                                      (nat-to-byte
                                        (Std.Natural/naturalAdd total (byte-to-nat (byte 246))))
                                      b""))
                                  (continue (bytes-tail right) (succ zero))))
                              (lambda unrestricted predecessor : Nat .
                                (lambda unrestricted induction : (pi unrestricted force : Nat . BytesBuilder) .
                                  (lambda unrestricted force : Nat .
                                    (bytes-builder-append
                                      (bytes-builder-chunk (bytes-cons (nat-to-byte total) b""))
                                      (continue (bytes-tail right) zero)))))
                              (nat-less-than total (byte-to-nat (byte 10))))
                            zero))
                        (Std.Natural/naturalAdd
                          carry
                          (Std.Natural/naturalAdd
                            (byte-to-nat head)
                            (byte-to-nat (bytes-head right))))))))))
            left)
          right
          zero))))

-- Saturating subtraction over canonical digits. Compare before borrowing so
-- underflow produces canonical zero. All Nat arithmetic is bounded to 0..19;
-- the numeric value is never expanded to a unary natural.
def magnitudeSubtractBorrow =
  (lambda unrestricted digit : Byte .
    (lambda unrestricted subtrahend : Nat . (nat-less-than (byte-to-nat digit) subtrahend)))

def magnitudeSubtractDigit =
  (lambda unrestricted digit : Byte .
    (lambda unrestricted subtrahend : Nat .
      (lambda unrestricted borrow : Nat .
        (nat-to-byte
          (Std.Natural/naturalSaturatingSubtract
            (Std.Natural/naturalAdd
              (byte-to-nat digit)
              (Std.Natural/naturalMultiply borrow (byte-to-nat (byte 10))))
            subtrahend)))))

def magnitudeSubtractOrdered =
  (lambda unrestricted left : Bytes .
    (lambda unrestricted right : Bytes .
      (magnitudeNormalize
        (bytes-builder-build
          (app
            (bytes-eliminate
              (lambda unrestricted rest : Bytes .
                (pi unrestricted right : Bytes . (pi unrestricted borrow : Nat . BytesBuilder)))
              (lambda unrestricted right : Bytes .
                (lambda unrestricted borrow : Nat . (bytes-builder-empty)))
              (lambda unrestricted head : Byte .
                (lambda unrestricted tail : Bytes .
                  (lambda unrestricted continue : (pi unrestricted right : Bytes . (pi unrestricted borrow : Nat . BytesBuilder)) .
                    (lambda unrestricted right : Bytes .
                      (lambda unrestricted borrow : Nat .
                        (app
                          (lambda unrestricted subtrahend : Nat .
                            (app
                              (lambda unrestricted nextBorrow : Nat .
                                (bytes-builder-append
                                  (bytes-builder-chunk
                                    (bytes-cons
                                      (magnitudeSubtractDigit head subtrahend nextBorrow)
                                      b""))
                                  (continue (bytes-tail right) nextBorrow)))
                              (magnitudeSubtractBorrow head subtrahend)))
                          (Std.Natural/naturalAdd (byte-to-nat (bytes-head right)) borrow)))))))
              left)
            right
            zero)))))

def magnitudeSubtract =
  (lambda unrestricted left : Bytes .
    (lambda unrestricted right : Bytes .
      (app
        (nat-eliminate
          (lambda unrestricted underflow : Nat . (pi unrestricted force : Nat . Bytes))
          (lambda unrestricted force : Nat . (magnitudeSubtractOrdered left right))
          (lambda unrestricted predecessor : Nat .
            (lambda unrestricted induction : (pi unrestricted force : Nat . Bytes) .
              (lambda unrestricted force : Nat . b"")))
          (magnitudeLess left right))
        zero)))

-- Decimal long division: with remainder < divisor, bringing down one digit
-- makes the next quotient digit at most nine. The bounded digit loop never
-- iterates a number of times proportional to the dividend's numeric value.
def magnitudeDivideDigit =
  (lambda unrestricted divisor : Bytes .
    (lambda unrestricted dividend : Bytes .
      (app
        (nat-eliminate
          (lambda unrestricted count : Nat .
            (pi unrestricted state : (sigma unrestricted quotient : Nat . Bytes) .
              (sigma unrestricted quotient : Nat . Bytes)))
          (lambda unrestricted state : (sigma unrestricted quotient : Nat . Bytes) . state)
          (lambda unrestricted predecessor : Nat .
            (lambda unrestricted continue : (pi unrestricted state : (sigma unrestricted quotient : Nat . Bytes) . (sigma unrestricted quotient : Nat . Bytes)) .
              (lambda unrestricted state : (sigma unrestricted quotient : Nat . Bytes) .
                (app
                  (nat-eliminate
                    (lambda unrestricted smaller : Nat .
                      (pi unrestricted force : Nat . (sigma unrestricted quotient : Nat . Bytes)))
                    (lambda unrestricted force : Nat .
                      (continue
                        (pair
                          (sigma unrestricted quotient : Nat . Bytes)
                          (succ (first state))
                          (magnitudeSubtractOrdered (second state) divisor))))
                    (lambda unrestricted unused : Nat .
                      (lambda unrestricted ignored : (pi unrestricted force : Nat . (sigma unrestricted quotient : Nat . Bytes)) .
                        (lambda unrestricted force : Nat . state)))
                    (magnitudeLessCanonical (second state) divisor))
                  zero))))
          (byte-to-nat (byte 9)))
        (pair (sigma unrestricted quotient : Nat . Bytes) zero dividend))))

def magnitudeDivideStep =
  (lambda unrestricted divisor : Bytes .
    (lambda unrestricted digit : Byte .
      (lambda unrestricted state : (sigma unrestricted quotient : BytesBuilder . Bytes) .
        (app
          (lambda unrestricted next : (sigma unrestricted quotientDigit : Nat . Bytes) .
            (pair
              (sigma unrestricted quotient : BytesBuilder . Bytes)
              (bytes-builder-append
                (bytes-builder-chunk (bytes-cons (nat-to-byte (first next)) b""))
                (first state))
              (second next)))
          (magnitudeDivideDigit divisor (magnitudeNormalize (bytes-cons digit (second state))))))))

def magnitudeDivModNonzero =
  (lambda unrestricted dividend : Bytes .
    (lambda unrestricted divisor : Bytes .
      (app
        (lambda unrestricted result : (sigma unrestricted quotient : BytesBuilder . Bytes) .
          (pair
            (sigma unrestricted quotient : Bytes . Bytes)
            (magnitudeNormalize (bytes-builder-build (first result)))
            (second result)))
        (bytes-eliminate
          (lambda unrestricted rest : Bytes . (sigma unrestricted quotient : BytesBuilder . Bytes))
          (pair (sigma unrestricted quotient : BytesBuilder . Bytes) (bytes-builder-empty) b"")
          (lambda unrestricted head : Byte .
            (lambda unrestricted tail : Bytes .
              (lambda unrestricted prefix : (sigma unrestricted quotient : BytesBuilder . Bytes) .
                (magnitudeDivideStep divisor head prefix))))
          dividend))))

-- Same total convention as the compile-time core: x/0 = 0, x mod 0 = x.
-- Inputs use the canonical internal representation; the checked owner admits
-- external digits before entering this arithmetic layer.
def magnitudeDivMod =
  (lambda unrestricted dividend : Bytes .
    (lambda unrestricted divisor : Bytes .
      (app
        (nat-eliminate
          (lambda unrestricted isZero : Nat .
            (pi unrestricted force : Nat . (sigma unrestricted quotient : Bytes . Bytes)))
          (lambda unrestricted force : Nat . (magnitudeDivModNonzero dividend divisor))
          (lambda unrestricted predecessor : Nat .
            (lambda unrestricted induction : (pi unrestricted force : Nat . (sigma unrestricted quotient : Bytes . Bytes)) .
              (lambda unrestricted force : Nat .
                (pair (sigma unrestricted quotient : Bytes . Bytes) b"" dividend))))
          (bytes-equal divisor b""))
        zero)))

def magnitudeDivide =
  (lambda unrestricted dividend : Bytes .
    (lambda unrestricted divisor : Bytes . (first (magnitudeDivMod dividend divisor))))

def magnitudeModulo =
  (lambda unrestricted dividend : Bytes .
    (lambda unrestricted divisor : Bytes . (second (magnitudeDivMod dividend divisor))))

def magnitudeDouble =
  (lambda unrestricted digits : Bytes .
    (bytes-builder-build
      (app
        (bytes-eliminate
          (lambda unrestricted rest : Bytes . (pi unrestricted carry : Nat . BytesBuilder))
          (lambda unrestricted carry : Nat .
            (app
              (nat-eliminate
                (lambda unrestricted flag : Nat . (pi unrestricted force : Nat . BytesBuilder))
                (lambda unrestricted force : Nat . (bytes-builder-empty))
                (lambda unrestricted predecessor : Nat .
                  (lambda unrestricted induction : (pi unrestricted force : Nat . BytesBuilder) .
                    (lambda unrestricted force : Nat .
                      (bytes-builder-chunk (bytes-cons (byte 1) b"")))))
                carry)
              zero))
          (lambda unrestricted head : Byte .
            (lambda unrestricted tail : Bytes .
              (lambda unrestricted continue : (pi unrestricted carry : Nat . BytesBuilder) .
                (lambda unrestricted carry : Nat .
                  (app
                    (nat-eliminate
                      (lambda unrestricted flag : Nat .
                        (pi unrestricted force : Nat . BytesBuilder))
                      (lambda unrestricted force : Nat .
                        (app
                          (lambda unrestricted reduced : Nat .
                            (bytes-builder-append
                              (bytes-builder-chunk
                                (bytes-cons
                                  (nat-to-byte
                                    (Std.Natural/naturalAdd
                                      carry
                                      (Std.Natural/naturalAdd reduced reduced)))
                                  b""))
                              (continue (succ zero))))
                          (byte-to-nat
                            (nat-to-byte
                              (Std.Natural/naturalAdd (byte-to-nat head) (byte-to-nat (byte 251)))))))
                      (lambda unrestricted predecessor : Nat .
                        (lambda unrestricted induction : (pi unrestricted force : Nat . BytesBuilder) .
                          (lambda unrestricted force : Nat .
                            (bytes-builder-append
                              (bytes-builder-chunk
                                (bytes-cons
                                  (nat-to-byte
                                    (Std.Natural/naturalAdd
                                      carry
                                      (Std.Natural/naturalAdd (byte-to-nat head) (byte-to-nat head))))
                                  b""))
                              (continue zero)))))
                      (byte-less-than head (byte 5)))
                    zero)))))
          digits)
        zero)))

def magnitudeMultiplyDigit =
  (lambda unrestricted digits : Bytes .
    (lambda unrestricted factor : Byte .
      (magnitudeNormalize
        (app
          (bytes-eliminate
            (lambda unrestricted rest : Bytes . (pi unrestricted carry : Nat . Bytes))
            (lambda unrestricted carry : Nat . (magnitudeFromNatural carry))
            (lambda unrestricted head : Byte .
              (lambda unrestricted tail : Bytes .
                (lambda unrestricted continue : (pi unrestricted carry : Nat . Bytes) .
                  (lambda unrestricted carry : Nat .
                    (app
                      (lambda unrestricted total : Nat .
                        (app
                          (lambda unrestricted nextCarry : Nat .
                            (bytes-cons
                              (nat-to-byte
                                (Std.Natural/naturalSaturatingSubtract
                                  total
                                  (Std.Natural/naturalMultiply nextCarry (byte-to-nat (byte 10)))))
                              (continue nextCarry)))
                          (Std.Natural/naturalDivideUnchecked total (byte-to-nat (byte 10)))))
                      (Std.Natural/naturalAdd
                        (Std.Natural/naturalMultiply (byte-to-nat head) (byte-to-nat factor))
                        carry))))))
            digits)
          zero))))

def magnitudeMultiply =
  (lambda unrestricted left : Bytes .
    (lambda unrestricted right : Bytes .
      (bytes-eliminate
        (lambda unrestricted rest : Bytes . Bytes)
        b""
        (lambda unrestricted head : Byte .
          (lambda unrestricted tail : Bytes .
            (lambda unrestricted continue : Bytes .
              (magnitudeAdd
                (magnitudeMultiplyDigit left head)
                (app
                  (nat-eliminate
                    (lambda unrestricted flag : Nat . (pi unrestricted force : Nat . Bytes))
                    (lambda unrestricted force : Nat . (bytes-cons (byte 0) continue))
                    (lambda unrestricted predecessor : Nat .
                      (lambda unrestricted induction : (pi unrestricted force : Nat . Bytes) .
                        (lambda unrestricted force : Nat . b"")))
                    (bytes-equal continue b""))
                  zero)))))
        right)))

def magnitudeRepeatSmall =
  (lambda erased State : Type 0 .
    (lambda unrestricted count : Nat .
      (lambda unrestricted step : (pi unrestricted value : State . State) .
        (lambda unrestricted seed : State .
          (nat-eliminate
            (lambda unrestricted index : Nat . State)
            seed
            (lambda unrestricted predecessor : Nat .
              (lambda unrestricted induction : State . (step induction)))
            count)))))

def magnitudeIterate =
  (lambda erased State : Type 0 .
    (lambda unrestricted digits : Bytes .
      (lambda unrestricted step : (pi unrestricted value : State . State) .
        (lambda unrestricted seed : State .
          (app
            (bytes-eliminate
              (lambda unrestricted rest : Bytes .
                (pi unrestricted step : (pi unrestricted value : State . State) .
                  (pi unrestricted seed : State . State)))
              (lambda unrestricted step : (pi unrestricted value : State . State) .
                (lambda unrestricted seed : State . seed))
              (lambda unrestricted head : Byte .
                (lambda unrestricted tail : Bytes .
                  (lambda unrestricted continue : (pi unrestricted step : (pi unrestricted value : State . State) . (pi unrestricted seed : State . State)) .
                    (lambda unrestricted step : (pi unrestricted value : State . State) .
                      (lambda unrestricted seed : State .
                        (continue
                          (lambda unrestricted state : State .
                            (magnitudeRepeatSmall State (byte-to-nat (byte 10)) step state))
                          (magnitudeRepeatSmall State (byte-to-nat head) step seed)))))))
              digits)
            step
            seed)))))