Normal form theorem for free products with amalgamation

Given: The objects and hypotheses in the statement.

Let $K$ be embedded in $G$ and $H$ as in def-free-product-with-amalgamation. By def-axiom-of-choice, choose left-coset transversals $S_G,S_H$ containing the identity. A normal word is $s_1\cdots s_nk,$ where $n\in\mathbb N$ (def-natural-numbers), $k\in K$, every $s_j$ is a nonidentity representative from $S_G$ or $S_H$, and consecutive representatives come from different factors. Length zero means the word is just $k$. The written form depends on the transversals. (Transversal normal-form data for an amalgamated free product).

With fixed transversal data, every element of $G$ and $H$ acts by a permutation on normal words. The two actions agree on $K$, inverses act inversely, and with the library's composition convention one has $P_{xy}=P_x\circ P_y$. (Factor elements act consistently by permutations on amalgamated normal words).

Let $G=\langle X\mid R\rangle$ and $H=\langle Y\mid S\rangle$ with disjoint generators, and let $f,h$ embed $K$. If $T$ generates $K$ and words $u_t(X),v_t(Y)$ represent $f(t),h(t)$, then $G\ast_KH\cong\langle X\sqcup Y\mid R\cup S\cup\{u_t v_t^{-1}:t\in T\}\rangle.$ (A free product with amalgamation has the factor presentations plus the amalgamating relations).

Given homomorphisms $f:K\to G$ and $h:K\to H$ as in def-group-homomorphism, a pushout is a group $P$ with homomorphisms $i_G:G\to P$ and $i_H:H\to P$ such that $i_G\circ f=i_H\circ h$, and such that every compatible pair $u:G\to Q$, $v:H\to Q$ factors through a unique $w:P\to Q$ with $w\circ i_G=u$ and $w\circ i_H=v$. The maps $f,h$ need not be injective. (Pushouts of group homomorphisms).