# Allow match-branching and concurrent-match in Regular Expressions

I wish to use strings, and string substitutions, to implement a theorem prover
This would allow me to implement a full-fledged (symbolic) theorem prover using only a few lines of code

Given the following string composed of axioms

``````let a = "1 + 1 = 2 | 2 + 2 = 4 | 1 + 1 + 2 = 4"
``````

I wish to use the first- and second axioms to prove the third by
string replace and expanding on both ends to obtain the following (inline) result

``````a = "| 1 + 1 + 1 + 1 = 1 + 1 + 1 + 1"
``````

However, this is not possible, via current inline find-/replace-/match string substitution methods

I encounter the following issues

1. string matching requires a bi-directional match option!
``````let a = "1 + 1 = 2 | 2 + 2 = 4 | 1 + 1 + 2 = 4"
``````

Once the RE engine encounters "1 + 1" match, it cannot be called again to evaluate the new sub expression ( to obtain "| 2 + 2 = 4 | 2 + 2 = 4", )

1. string matching requires an option to match in a concurrent manner!
``````let a = "1 + 0 = 1 | 0 + 0 = 0 | 0 + 1 + 0 + 0 = 1"
``````

In the above example, string match could employ the second axiom replace indefinitely! This replace method is required yet it yields a non-determinism,
which can be cured if the replace instead spawns branches which can be evaluated in a concurrent (parallel?) manner

1. string matching requires an option to match recursively, and or indefinitely!
``````let a = "1 + 1 = 2 | 2 + 2 = 4 | 0 + 0 = 0 | 1 + 1 + 2 = 4 + 0 + 0"
``````

In the above example, the use of a replace callback ultimately fails because subsequent matching would not branch concurrently and as a result go deep enough to reach the available solution, which occurs in an isolated branch

1. String.search, String.find, String.replace should return a (more) flexible list!

Because of the aforementioned limitations, the above methods currently return incomplete or incompatible lists for recursive use

My theorem prover library currently employs symbolic substitution

Implementing a full-fledged symbolic prover using inline string match would allow me to reduce my entire library to only a few lines of code!