Compiler.NaturalMagnitudeArithmetic

75def magnitudePredecessor =
76  (lambda unrestricted digits : Bytes .
77    (magnitudeNormalize
78      (app
79        (bytes-eliminate
80          (lambda unrestricted rest : Bytes . (pi unrestricted force : Nat . Bytes))
81          (lambda unrestricted force : Nat . b"")
82          (lambda unrestricted head : Byte .
83            (lambda unrestricted tail : Bytes .
84              (lambda unrestricted continue : (pi unrestricted force : Nat . Bytes) .
85                (lambda unrestricted force : Nat .
86                  (app
87                    (nat-eliminate
88                      (lambda unrestricted flag : Nat . (pi unrestricted force : Nat . Bytes))
89                      (lambda unrestricted force : Nat .
90                        (bytes-cons
91                          (nat-to-byte
92                            (Std.Natural/naturalSaturatingSubtract (byte-to-nat head) (succ zero)))
93                          tail))
94                      (lambda unrestricted predecessor : Nat .
95                        (lambda unrestricted induction : (pi unrestricted force : Nat . Bytes) .
96                          (lambda unrestricted force : Nat . (bytes-cons (byte 9) (continue zero)))))
97                      (byte-equal head (byte 0)))
98                    zero)))))
99          (magnitudeNormalize digits))
100        zero)))