 Edge-labelled walk matching

Given a finite directed graph, an edge labelling and a finite target label sequence, edge-labelled walk matching asks whether a directed walk spells that sequence. Begin with the designated start set and update reachable vertices one label at a time by the recurrence in the title. Appending a final matching edge proves the invariant by induction. Repeated vertices are allowed; a requirement of a vertex-simple directed path is a different problem and can encode Hamiltonian path. Scanning all edges and clearing a vertex layer costs $O(k(|V|+|E|))$ for $k$ labels.