What's going on
We are concerned with establishing a 1-to-1 association between the strings of two languages. One language, call it Ll, consists of all the finite non-empty sequences of characters from some alphabet S0. The other language, call it Ls, consists of all the finite non-empty sequences of characters drawn from S1 (where S1 ‚ S0) that begin with a character from S2 (S2 ‚ S1). We want some restrictions on the association. We want the association to basically have the form of a bunch of (literal) pattern replacements --- that is, where pattern a appears in the string in Ll, pattern b appears in the string in Ls, for a bunch of client-specified a and b.
The technique used is as follows. Ignore for the moment the restriction on the initial character of a string in Ls --- we'll translate from Ll to Lm, where Lm = S1+, then make a seperate step from Lm to Ls.
For getting from Ll to Lm, we restrict the a's to be single characters. Identify in S1 an "escape character" y. Define a substitution function q, which associates with every character c in S0- (where S0- = S0-S1) a unique string b in S1-+ (where S1- = S1-{y}, and + means a non-empty finite string thereof). Let B be the range of q. The relation is as follows: ync in a string in Ll maps to y2n+1b in Lm when c S0- and q(c)=b. ynb maps to y2nb when b B and to ynb otherwise; b must contain only characters from S1-.
To translate sm (in Lm) to ss (in Ls), pick another escape character (call it f), this time from S2. Scan sm and find the first character (call it d) that's not f. If you run out of string, or if d S2, then ss = sm; otherwise ss = fsm.
Now we do it precisely.
Given
S2 ‚ S1 ‚ S0
y S1, f S2
q: S0- é B
Where
S0- = S0 - S1
S1- = S1 - {y}
Ll = S0+
Lm = S1+
Ls = S2 S1*
B ‚ S1-+
B has the prefix property: