So Lyndon & Schupp's Combinatorial Group Theory states that if $A$ and $B$ are finitely generated with solvable word problem, then $A*B$ (the free product) has solvable word problem.
This appears as a corollary to the Normal Form Theorem, which states that every element of $A*B$ can be expressed as a reduced sequence $g_1,g_2,...,g_n$ such that $g_1 \in A$, $g_2 \in B$, $g_3 \in A$, $g_4 \in B, ...$ and all $g_i \neq 1$
My question is, how does the corollary follow from the Normal Form Theorem? An answer is given to this question here: Solvable word for the free product and direct product of two groups.
To tell whether a word in the free product $G*H$ is trivial, write it as a product $$g_1h_1g_2h_2\cdots g_mh_m$$ where $g_i\in G$, $h_i\in H$, $h_i\neq 1$ for $i=1,\ldots m-1$, and $g_i\neq 1$ for $i=2,\ldots,m$. This will be trivial if and only if $m=1$, $g_1=1$ and $h_1=1$.
(The notation is slightly different from mine, but the problem is the same.) This seems like it might work, but how does this supposed algorithm "write it as the product" in the first place? To my understanding the word problem asks for an algorithm that takes any word -- as in not just words in normal form -- and determines whether it is identity.
Use a generating set $X \cup Y$ of $G = A*B$ where $X$ and $Y$ are finite generating sets of $A$ and $B$ respectively.
Any word $w$ in the generators $X \cup Y$ can be decomposed uniquely as $u_1v_1\cdots u_mv_m$, where $u_i$ and $v_i$ are words in $X$ and $Y$ respectively, and only $u_1$ and $v_m$ are allowed to be empty. If $m=0$ then $w =_G 1$, so suppose not.
Use the word problem algorithms in $A$ and $B$ to decide whether any of the nonempty words $u_i$ and $v_i$ equal the identity in $A$ or $B$. If not then $w \ne_G 1$. If, say $u_i =_A 1$, then remove the word $u_i$ from $w$, and repeat the algorithm on the resulting shorter word. Similarly if $v_i =_B 1$.