765def geluSM86Plan =
766 (lambda unrestricted kind : (family GELUSM86ProgramKind) .
767 (lambda unrestricted elements : Nat .
768 (nat-eliminate
769 (lambda unrestricted nonzero : Nat . (family GELUSM86PlanResult))
770 (constructor
771 GELUSM86PlanResult
772 GELUSM86PlanFailed
773 (constructor GELUSM86FailureCode GELUSM86ElementCountZero)
774 (geluSM86RejectedTelemetry
775 (constructor GELUSM86FailureCode GELUSM86ElementCountZero)
776 zero))
777 (lambda unrestricted nonzeroPredecessor : Nat .
778 (lambda unrestricted nonzeroInduction : (family GELUSM86PlanResult) .
779 (nat-eliminate
780 (lambda unrestricted aligned : Nat . (family GELUSM86PlanResult))
781 (constructor
782 GELUSM86PlanResult
783 GELUSM86PlanFailed
784 (constructor GELUSM86FailureCode GELUSM86ElementCountMisaligned)
785 (geluSM86RejectedTelemetry
786 (constructor GELUSM86FailureCode GELUSM86ElementCountMisaligned)
787 elements))
788 (lambda unrestricted alignedPredecessor : Nat .
789 (lambda unrestricted alignedInduction : (family GELUSM86PlanResult) .
790 (app
791 (lambda unrestricted program : (family SM86Program) .
792 (app
793 (lambda unrestricted actual : Nat .
794 (nat-eliminate
795 (lambda unrestricted countValid : Nat . (family GELUSM86PlanResult))
796 (constructor
797 GELUSM86PlanResult
798 GELUSM86PlanFailed
799 (constructor GELUSM86FailureCode GELUSM86InstructionCountMismatch)
800 (geluSM86RejectedTelemetry
801 (constructor GELUSM86FailureCode GELUSM86InstructionCountMismatch)
802 actual))
803 (lambda unrestricted countPredecessor : Nat .
804 (lambda unrestricted countInduction : (family GELUSM86PlanResult) .
805 (constructor
806 GELUSM86PlanResult
807 GELUSM86PlanReady
808 (constructor
809 GELUSM86Plan
810 GELUSM86PlanValue
811 kind
812 elements
813 program
814 geluSM86ScalarBindings
815 (constructor
816 GELUSM86Telemetry
817 GELUSM86TelemetryValue
818 kind
819 (geluSM86ExpectedInstructions kind)
820 actual
821 (geluSM86RegisterCount kind)
822 elements
823 (naturalDivideUnchecked elements geluSM86BlockX)
824 geluSM86BlockX
825 geluSM86NaturalFive
826 zero
827 zero
828 zero
829 zero)))))
830 (naturalEqual actual (geluSM86ExpectedInstructions kind))))
831 (sm86ProgramCount program)))
832 (geluSM86Program kind))))
833 (naturalIsZero (naturalModuloUnchecked elements geluSM86BlockX)))))
834 (naturalNonzero elements))))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.