Compiler.NaturalMagnitudeArithmetic

133def magnitudeCompareSameLength =
134  (lambda unrestricted left : Bytes .
135    (lambda unrestricted right : Bytes .
136      (app
137        (bytes-eliminate
138          (lambda unrestricted rest : Bytes . (pi unrestricted right : Bytes . Nat))
139          (lambda unrestricted right : Bytes .
140            (app
141              (nat-eliminate
142                (lambda unrestricted flag : Nat . (pi unrestricted force : Nat . Nat))
143                (lambda unrestricted force : Nat . (succ zero))
144                (lambda unrestricted predecessor : Nat .
145                  (lambda unrestricted induction : (pi unrestricted force : Nat . Nat) .
146                    (lambda unrestricted force : Nat . zero)))
147                (bytes-equal right b""))
148              zero))
149          (lambda unrestricted head : Byte .
150            (lambda unrestricted tail : Bytes .
151              (lambda unrestricted continue : (pi unrestricted right : Bytes . Nat) .
152                (lambda unrestricted right : Bytes .
153                  (app
154                    (nat-eliminate
155                      (lambda unrestricted flag : Nat . (pi unrestricted force : Nat . Nat))
156                      (lambda unrestricted force : Nat .
157                        (app
158                          (lambda unrestricted higher : Nat .
159                            (app
160                              (nat-eliminate
161                                (lambda unrestricted flag : Nat .
162                                  (pi unrestricted force : Nat . Nat))
163                                (lambda unrestricted force : Nat . higher)
164                                (lambda unrestricted predecessor : Nat .
165                                  (lambda unrestricted induction : (pi unrestricted force : Nat . Nat) .
166                                    (lambda unrestricted force : Nat .
167                                      (app
168                                        (nat-eliminate
169                                        (lambda unrestricted flag : Nat .
170                                        (pi unrestricted force : Nat . Nat))
171                                        (lambda unrestricted force : Nat .
172                                        (app
173                                        (nat-eliminate
174                                        (lambda unrestricted flag : Nat .
175                                        (pi unrestricted force : Nat . Nat))
176                                        (lambda unrestricted force : Nat . (succ (succ zero)))
177                                        (lambda unrestricted predecessor : Nat .
178                                        (lambda unrestricted induction : (pi unrestricted force : Nat . Nat) .
179                                        (lambda unrestricted force : Nat . zero)))
180                                        (byte-equal head (bytes-head right)))
181                                        zero))
182                                        (lambda unrestricted predecessor : Nat .
183                                        (lambda unrestricted induction : (pi unrestricted force : Nat . Nat) .
184                                        (lambda unrestricted force : Nat . (succ zero))))
185                                        (nat-less-than
186                                        (byte-to-nat head)
187                                        (byte-to-nat (bytes-head right))))
188                                        zero))))
189                                (Std.Natural/naturalIsZero higher))
190                              zero))
191                          (continue (bytes-tail right))))
192                      (lambda unrestricted predecessor : Nat .
193                        (lambda unrestricted induction : (pi unrestricted force : Nat . Nat) .
194                          (lambda unrestricted force : Nat . (succ (succ zero)))))
195                      (bytes-equal right b""))
196                    zero)))))
197          left)
198        right)))