1319def stdU32DivisionStep =
1320 (lambda unrestricted divisor : (family ModelWord32) .
1321 (lambda unrestricted state : (family StdU32DivisionState) .
1322 (eliminate
1323 StdU32DivisionState
1324 (lambda unrestricted current : (family StdU32DivisionState) . (family StdU32DivisionState))
1325 state
1326 (branch
1327 StdU32DivisionStateOf
1328 remainder
1329 quotient
1330 dividend
1331 .
1332 (app
1333 (lambda unrestricted shifted : (family ModelWord32) .
1334 (app
1335 (lambda unrestricted shiftedQuotient : (family ModelWord32) .
1336 (app
1337 (lambda unrestricted shiftedDividend : (family ModelWord32) .
1338 (nat-eliminate
1339 (lambda unrestricted current : Nat . (family StdU32DivisionState))
1340 (constructor
1341 StdU32DivisionState
1342 StdU32DivisionStateOf
1343 shifted
1344 shiftedQuotient
1345 shiftedDividend)
1346 (lambda unrestricted predecessor : Nat .
1347 (lambda unrestricted induction : (family StdU32DivisionState) .
1348 (constructor
1349 StdU32DivisionState
1350 StdU32DivisionStateOf
1351 (stdU32SubtractWrapping shifted divisor)
1352 (modelWord32Add shiftedQuotient modelWord32One)
1353 shiftedDividend)))
1354 (stdFlagOr
1355 (stdU32HighBit remainder)
1356 (stdFlagNot (stdU32LessThan shifted divisor)))))
1357 (modelWord32ShiftLeftOne dividend)))
1358 (modelWord32ShiftLeftOne quotient)))
1359 (modelWord32Add
1360 (modelWord32ShiftLeftOne remainder)
1361 (stdU32Select (stdU32HighBit dividend) modelWord32One modelWord32Zero)))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.