The source bounds the length of a shortest distinguishing input by an explicit arithmetic expression in the two codes ($Transducers.RegDec.codeBound$, from the crossing-sequence decomposition of a two-way run and Schützenberger's rank criterion, $PartC/Reg*.lean$) and compares the two coded transducers on all inputs up to that bound over the letters of the codes and one fresh letter ($PartC/RegEqDec.lean$, $PartC/TwoWaySimPrimrec.lean$). The concept's codes are the same lists as the source's; the bridge identifies the coded transducers ($twoWayCodeAut_toSrc$), their relations and the totality promise, and $DecidableUnderPromise$ unfolds identically.

Theorem C.1.4 of Transducers, Part C; formalised by Aristotle (Harmonic).