Can the following proof calculus show that any finitely presented free group is free?

Question

If a finitely presented group is free, will it always have a proof in the proof calculus outlined in this question that it is free?

---

I recently saw this question.

I tried to show that the group was free by rewriting it until it had no relations. This is what I came up with:

1. $ \langle a,b,c \mid aabacacab = 1 \rangle $
2. Apply $[b := a^{-1}b]$
3. $ \langle a,b,c \mid aaa^{-1}bacacaa^{-1}b = 1 \rangle $
4. Simplify
5. $ \langle a,b,c \mid abacacb = 1 \rangle$
6. Apply $[c := a^{-1}c]$
7. $ \langle a,b,c \mid abaa^{-1}caa^{-1}cb = 1 \rangle $
8. Simplify.
9. $ \langle a,b,c \mid abccb = 1 \rangle $
10. Isolate $a$ in the first relation.
11. $ \langle a, b,c \mid a = b^{-1}c^{-1}c^{-1}b^{-1} \rangle $
12. $a$ is defined in terms of the other generators, so remove $a$ from the set of generators and replace it with its definition in the remaining relations.
13. $ \langle b, c \rangle $
14. The group has no relations and is thus free.

I'm wondering whether this "freedom-preserving proof calculus" works in general for showing that a free finitely-presented group is in fact free. (As an aside, I want to take finding a concrete witness that a finitely presented group is NOT free out of scope for the purposes of this question.)

The freedom-preserving proof calculus has four kinds of steps.

Groups with no relations are self-evidently free.

We need to stop somewhere. If we manage to rewrite away all the relations, then the group is free.

General Manipulation

A general manipulation step is one that is valid in any group, such as $aa^{-1} \mapsto 1$ or $a1 \mapsto a$ or $a = b \mapsto ab^{-1} = 1$.

Also, $\varepsilon = \delta \mapsto \alpha \varepsilon \beta = \alpha \delta \beta$, i.e. we can left or right multiply by constants freely.

Rotation

I'm calling this operation rotation because we're basically taking one generator and flipping it around.

$ \langle g_1 \cdots g_m \mid \delta_1 = \varepsilon_1 \cdots \delta_n = \varepsilon_n \rangle [g_i := \varphi] $ where $\varphi$ is an expression involving $g_i$ exactly once.

It rewrites to:

$$ \langle g_1 \cdots g_m \mid \delta_1[g_i := \varphi] = \varepsilon_1[g_i := \varphi] \cdots \delta_n[g_i := \varphi] = \varepsilon_n[g_i := \varphi] \rangle $$

Removal

If I have a generators-and-relations presentation of the form $\langle g_1 \cdots g_m \mid g_i = \varphi, \delta_1 = \varepsilon_1 \cdots \delta_n = \varepsilon_n \rangle $ where $\varphi$ does not contain $g_i$.

In a sense, the equation $g_i = \varphi$ tells me that $g_i$ is redundant and can be removed (and replaced with its definition). So we do so.

We rewrite the group to:

$$ \langle g_1 \cdots g_{i-1}, g_{i+1} \cdots g_m \mid \delta_1[g_i := \varphi] = \varepsilon_1[g_i := \varphi] \cdots \delta_n[g_i := \varphi] = \varepsilon_n[g_i := \varphi] \rangle $$

Soundness

I claim that all of the steps somewhat obviously preserve the group up to isomorphism, although the interpretation of each individual generator is not preserved from step to step.

Since the group up to isomorphism is preserved, it never transitions from free to nonfree.

Completeness

For this, I am stuck.