1068def greedyArgmaxSM86SlotPrograms =
1069 (lambda unrestricted vocabulary : Nat .
1070 (app
1071 (lambda unrestricted fullSlots : Nat .
1072 (app
1073 (lambda unrestricted remainder : Nat .
1074 (app
1075 (lambda unrestricted fullProgram : (family SM86Program) .
1076 (nat-eliminate
1077 (lambda unrestricted tailLanes : Nat . (family SM86Program))
1078 fullProgram
1079 (lambda unrestricted lastLane : Nat .
1080 (lambda unrestricted tailInduction : (family SM86Program) .
1081 (sm86ProgramAppend
1082 fullProgram
1083 (greedyArgmaxSM86PartialSlotProgram fullSlots lastLane))))
1084 remainder))
1085 (greedyArgmaxSM86FullSlotPrograms fullSlots)))
1086 (naturalModuloUnchecked vocabulary greedyArgmaxSM86N256)))
1087 (naturalDivideUnchecked vocabulary greedyArgmaxSM86N256)))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.