The least register below `count` for which `free` holds, or `count`.
953def sm121LowerFirst =
954 (lambda unrestricted count : Nat .
955 (lambda unrestricted free : (pi unrestricted register : Nat . Nat) .
956 (nat-eliminate
957 (lambda unrestricted current : Nat . Nat)
958 count
959 (lambda unrestricted predecessor : Nat .
960 (lambda unrestricted induction : Nat .
961 (let unrestricted register = (nat-subtract count (succ predecessor)) in
962 (naturalSelect (free register) register induction))))
963 count)))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.