The handed program on a no-instance #
DescriptiveComplexity.Draw.Data.wideRegAccept_of_out_of_rules is the
forward half of the machine's correctness: a sentence true at the guessed stage
makes the emitted instance a yes-instance. This file is the other half – if the
sentence is true at no stage, the machine does not accept – and it is where the
backward reading of an accepting run is used.
The shape of the argument is the yes-direction's turned round. An accepting run
starts where the channel wrote (exists_stepsIn_of_wideRegAccept); read as a
sequence, it has a first post-guess configuration whose tape is a tape state
(exists_entry_state) and whose phase is the walk home; the evaluation from
there returns the verdict as the sentence's own value at the stage the guess
left, which is assignOfTrack of the tracks the reading recovered; and a false
verdict cannot stand beside an accepting run (not_acc_of_entry_verdict).
Everything else – the marking, the file's ends, the rounds, the exits, the parked scratch and the region the atoms stay inside – is what the yes-direction supplies, and is supplied here the same way.