Second independent verification run: Lemma 5.2 and the dihedral Artin groups
free group, m =  4: True  (6 identities)
free group, m =  6: True  (6 identities)
free group, m =  8: True  (6 identities)
free group, m = 10: True  (6 identities)
free group, m = 12: True  (6 identities)
free group, m = 14: True  (6 identities)
free group, m = 16: True  (6 identities)
free group, m = 18: True  (6 identities)
free group, m = 20: True  (6 identities)
A(I2( 3)): True  (6 checks)
A(I2( 4)): True  (11 checks)
A(I2( 5)): True  (6 checks)
A(I2( 6)): True  (11 checks)
A(I2( 7)): True  (6 checks)
A(I2( 8)): True  (11 checks)
A(I2( 9)): True  (6 checks)
A(I2(10)): True  (11 checks)
A(I2(11)): True  (6 checks)
A(I2(12)): True  (11 checks)
A(I2(13)): True  (6 checks)
A(I2(14)): True  (11 checks)
A(I2(15)): True  (6 checks)
A(I2(16)): True  (11 checks)
A(I2(17)): True  (6 checks)
A(I2(18)): True  (11 checks)
A(I2(19)): True  (6 checks)
A(I2(20)): True  (11 checks)
solver consistency on random words (w w^-1 = 1, conjugated relators = 1): True
mutation: wrong eta (b -> b^-1) does not preserve the relation True
mutation: wrong sign (eta^k(a) = a Delta^-1) rejected True
mutation: Delta central in A(I2(5)) rejected True
mutation: eta^(k-1) claimed to be a transvection rejected True
mutation: aba = bab in A(I2(4)) rejected True
checks listed per type:
  even m: solver: defining relation holds
  even m: solver: ab != ba, Pi(a,b;m-1) != Pi(b,a;m-1), a^2 != 1, (ab)^m != (ba)^m a
  even m: Tietze (m even): a y^k = y^k a in A, Delta = y^k
  even m: Delta central, l(Delta) = m, class of Delta = (k, k)
  even m: eta, psi, gamma, eps preserve the relation in A
  even m: psi eta = eta psi = id in A
  even m: eta^k = T_lambda, lambda(a) = 1, lambda(b) = -1, lambda(Delta) = 0
  even m: gamma eta gamma = eta^-1 (= psi), eps eta eps = eta, gamma eps = eps gamma in A
  even m: eta^j is not a transvection for 0 < j < k
  even m: l(eta^{kj}(a)) = 1 + jm != 1 (no power of eta^k is inner), j = 1, 2, 3
  even m: |(Z/k x| Z/2) x Z/2| = 2m
  odd m:  solver: defining relation holds
  odd m:  solver: ab != ba, Pi(a,b;m-1) != Pi(b,a;m-1), a^2 != 1, (ab)^m != (ba)^m a
  odd m:  Tietze (m odd): y^-k x = a, x y^-k = b, x^2 = y^m in A
  odd m:  Delta^2 central, Delta not central (w0 != -1)
  odd m:  conjugation by Delta swaps a and b (gamma inner)
  odd m:  l(Delta^2) = 2m
ALL CHECKS PASSED: True
