1 when ordinal `b` is one the launch stands for: the generators are
nested (each stride is at least the extent of those inside it), so the
decomposition is greedy
529def deviceArenaGenerated =
530 (lambda unrestricted base : Nat .
531 (lambda unrestricted generators : (family DeviceArenaGenerators) .
532 (lambda unrestricted b : Nat .
533 (naturalAnd
534 (naturalLessOrEqual base b)
535 (app
536 (eliminate
537 DeviceArenaGenerators
538 (lambda unrestricted current : (family DeviceArenaGenerators) .
539 (pi unrestricted rest : Nat . Nat))
540 generators
541 (branch
542 DeviceArenaGeneratorsEnd
543 .
544 (lambda unrestricted rest : Nat . (naturalIsZero rest)))
545 (branch
546 DeviceArenaGeneratorsNext
547 stride
548 count
549 tail
550 induction
551 .
552 (lambda unrestricted rest : Nat .
553 (naturalAnd
554 (naturalLess (naturalDivideUnchecked rest stride) count)
555 (induction (naturalModuloUnchecked rest stride))))))
556 (naturalSaturatingSubtract b base))))))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.