Space-unconstructable function in the proof of Savitch's theorem
Starting Point: ​ ​ ​ ​ ​ ​ ​ For inputs x, if ​ ​ ​ [there is no sequence of choices

which makes the non-deterministic machine accept x] ​ and

[for all positive integers S, there is a sequence of non-deterministic choices that,

when made for input x, will cause the non-deterministic machine to use more than S space]

then on input x, the deterministic machine is allowed

to run forever with no bound on its space usage.

Otherwise, such simulation would suffice for solving the halting problem:

Run the simulator until it halts or loops, then output accordingly.

With that in mind, the simulation works as follows:

S = 1
while True:
    run CAN_YIELD with space-bound S
    if that accepts then accept
    increase S by 1
    for end_state in configurations_at_which_the_nondeterministic_machine_might_have_just_used_more_than_space_(S):
        run CAN_YIELD with space-bound S and end_state
        if that accepts then break out of the for loop
    if the for loop ended without a break then REJECT