DFA prefix states and block-boundary path observations

For all natural numbers $r,m$, every deterministic binary automaton $B$ with $r$ states, and every binary word $x$ of length $m$, the function $B.\mathrm{stateAfter}(x,t)$, defined for each natural number $t$, is the state obtained by starting at the specified initial state of $B$ and applying its transition function successively to the first $\min(t,m)$ bits of $x$ in index order. Thus at $t=0$ it returns the initial state; at $t\ge m$ it returns the state after the entire word, and for $m=0$ it returns the initial state for every $t$. The accepting set plays no role. An automaton with $r=0$ cannot be supplied because its structure requires an initial state.

For all natural numbers $q,r,n$, every deterministic binary automaton $B$ with $r$ states, every map $\varphi$ from its state set to the set of $q$ states, all natural numbers $v,s$, and every binary word $x$ of length $v+ns$, the function $B.\mathrm{sampledPath}(\varphi,v,s,x)$ is the sequence of $n+1$ states whose entry at each index $i=0,\ldots,n$ is $\varphi$ applied to the state of $B$ after it reads the first $v+si$ bits of $x$. The automaton starts at its specified initial state and reads prefixes from that same start for these evaluations. The final observation is at the full word length $v+ns$. This definition imposes no positivity conditions on $v$ or $s$: if $v=0$, the first observed state is the projection of the initial state, and if $s=0$, all entries are the projection of the same state reached after $v$ bits. If $n=0$, the sequence has just the observation after $v$ bits. The accepting set is unused. The initial-state field requires $r>0$, and existence of the supplied map from that inhabited state set requires $q>0$.