In reply to VE:
I demonstrated that
(##1 fell(b)[->1] ##1 b[=1]) within e[->1];
expands to this
(1[*0:] ##1 fell(b)[->1] ##1 b[->1] ##1 !b[*0] ##1 1[*0:]) or // thread1
(1[*0:$] ##1 fell(b)[->1] ##1 b[->1] ##1 !b[*1] ##1 1[*0:]) or //thread 2
(1[*0:$] ##1 fell(b)[->1] ##1 b[->1] ##1 !b[*2] ##1 1[*0:]) or
…
Thus any of those threads can pass.
Consider thread1
**(1[*0:$] ##1 fell(b)[->1] ##1 b[->1] ##1 !b[*0] ##1 1[*0:])
**
This expands to:
(1[*0:$] ##1 fell(b)[->1] ##1 b[->1] ##1 !b[*0] ##1 1[*0]) or
// x[*0] ##1[*0] w // is a no match (1[*0:] ##1 fell(b)[->1] ##1 b[->1] ##1 !b[*0] ##1 1[*1]) or
(1[*0:] ##1 fell(b)[->1] ##1 b[->1] ##1 !b[*0] ##1 1[*1]) or
// x[*0] ##1[*1] /w/ is same as w
// thus that one above gets reduced to
(1[*0:] ##1 fell(b)[->1] ##1 b[->1] ##1 1[*1]
(1[*0:] ##1 fell(b)[->1] ##1 b[->1] ##1 1[*2])
..
(1[*0:] ##1 fell(b)[->1] ##1 b[->1] ##1 1[*n])
Thus, we can say that
**(1[*0:] ##1 fell(b)[->1] ##1 b[->1] ##1 !b[*0] ##1 1[*0:])
**
is same as
**(1[*0:$] ##1 fell(b)[->1] ##1 b[->1] ##1 1[*0:])
**
In this thread, after a fall of b and then 1 occurrence of b you have many
threads of true with one of them matching the intersection of an occurrence of e.
Any second occurrence of “b” is ignored. Note *b[->1] ##1 1[0:$]