there are *lots* of things that could've gone wrong in the process of getting these rules, so they definitely need independent verification (or at least checking for small inputs), but:```
A(a,b+3,2c) -> A(a,b,3c)
A(a,b+1,2c+1) -> A(a,b,3c+1)
A(a+2,0,2c) -> A(a,15c-17,2m+1)
A(a+2,1,2c) -> A(a,15c-7,2)
A(a+8,2,4c) -> A(a,45c+15m-10,2)
A(a+7,2,4c+2) -> B(a,45c+15m+8,1,2)
A(a+7,0,4c+1) -> B(a,45c+15m-7,1,2)
A(a+8,0,4c+3) -> A(a,45c+15m+20,2)
B(a,b,c+3,2d) -> B(a,b,c,3d)
B(a,b,c+1,2d+1) -> B(a,b,c,3d+1)
B(a,b+3,0,2d) -> B(a,b,15d-10,2)
B(a,b+1,1,2d) -> B(a,b,15d-11,2)
B(a+3,2b,2,2d) -> A(a,3b+15d-3,2)
B(a+2,2b+1,2,2d) -> B(a,3b+15d-6,1,2)
B(a+2,2b,0,2d+1) -> B(a,3b+15d-1,1,2)
B(a+3,2b+1,0,2d+1) -> A(a,3b+15d+5,2)```