Hey all, I'd like to give an explicit example of a standard BM2 expression that never terminates. This expression is (0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,1).
First, let's show how (0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,1) is in fact standard:
We start from (0,0,0,0)(1,1,1,1). Then, we have:
(0,0,0,0)(1,1,1,1)
(0,0,0)(1,1,1)(2,2,2)
(0,0,0)(1,1,1)(2,2,1)(3,3,1)
(0,0,0)(1,1,1)(2,2,1)(3,3,0)
(0,0,0)(1,1,1)(2,2,1)(3,2,0)
(0,0,0)(1,1,1)(2,2,1)(3,1,1)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(4,2,1)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(4,2,0)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(4,1,0)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(4,0,0)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(3,0,0)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,1)
So (0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,1) is standard. Now, I will show how this expression never terminates. Pay attention to each checkpoint.
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,1) - first checkpoint
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,0)(3,3,1)(4,4,1)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,0)(3,3,1)(4,4,0)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,0)(3,3,1)(4,3,1)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,0)(3,3,1)(4,3,0)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,0)(3,3,1)(4,2,0)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,0)(3,3,1)(4,1,1)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,0)(3,3,1)(4,1,0)(5,2,1)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,0)(3,3,1)(4,1,0)(5,2,0)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,0)(3,3,1)(4,1,0)(5,1,0)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,0)(3,3,1)(4,1,0)(5,0,0)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,0)(3,3,1)(4,1,0)(4,1,0)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,0)(3,3,1)(4,1,0)(4,0,0)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,0)(3,3,1)(4,1,0)(3,3,1) - second checkpoint
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,0)(3,3,1)(4,1,0)(3,3,0)(4,4,1)(5,3,0)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,0)(3,3,1)(4,1,0)(3,3,0)(4,4,1)(5,2,1)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,0)(3,3,1)(4,1,0)(3,3,0)(4,4,1)(5,2,0)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,0)(3,3,1)(4,1,0)(3,3,0)(4,4,1)(5,1,0)(6,3,1)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,0)(3,3,1)(4,1,0)(3,3,0)(4,4,1)(5,1,0)(6,3,0)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,0)(3,3,1)(4,1,0)(3,3,0)(4,4,1)(5,1,0)(6,2,0)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,0)(3,3,1)(4,1,0)(3,3,0)(4,4,1)(5,1,0)(6,1,0)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,0)(3,3,1)(4,1,0)(3,3,0)(4,4,1)(5,1,0)(6,0,0)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,0)(3,3,1)(4,1,0)(3,3,0)(4,4,1)(5,1,0)(5,2,0)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,0)(3,3,1)(4,1,0)(3,3,0)(4,4,1)(5,1,0)(5,1,0)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,0)(3,3,1)(4,1,0)(3,3,0)(4,4,1)(5,1,0)(5,0,0)
(0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,0)(3,3,1)(4,1,0)(3,3,0)(4,4,1)(5,1,0)(4,4,1) - third checkpoint
The checkpoints form a pattern:
1: (0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,1)
2: (0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,0)(3,3,1)(4,1,0)(3,3,1)
3: (0,0,0)(1,1,1)(2,2,1)(3,1,0)(2,2,0)(3,3,1)(4,1,0)(3,3,0)(4,4,1)(5,1,0)(4,4,1)
This pattern will never end, and thus BM2 does not terminate.
I believe that the newly defined BM3 fixes this issue, but it also becomes much weaker. (0,0,0)(1,1,1)(2,2,0) is only \(\psi(\varepsilon_{\Omega_\omega+1})\) in BM3, but it is \(\psi(\varepsilon_{T+1})\) in BM2, which is WAAAAAYYYYYYY bigger.