Valid builders have no empty chunks and partition their length into shared
source bytes and bytes copied while preparing bounded slices.
674def dataBytesBuilderMetadataValid =
675 (lambda unrestricted length : Nat .
676 (lambda unrestricted chunks : Nat .
677 (lambda unrestricted sharedBytes : Nat .
678 (lambda unrestricted preparationCopiedBytes : Nat .
679 (nat-eliminate
680 (lambda unrestricted current : Nat . Nat)
681 zero
682 (lambda unrestricted basicPredecessor : Nat .
683 (lambda unrestricted basicInduction : Nat .
684 (nat-eliminate
685 (lambda unrestricted current : Nat . Nat)
686 zero
687 (lambda unrestricted sumPredecessor : Nat .
688 (lambda unrestricted sumInduction : Nat .
689 (naturalEqual (naturalAdd sharedBytes preparationCopiedBytes) length)))
690 (naturalLessOrEqual
691 preparationCopiedBytes
692 (naturalSaturatingSubtract length sharedBytes)))))
693 (naturalAnd (naturalLessOrEqual chunks length) (naturalLessOrEqual sharedBytes length)))))))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.