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

- 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", )

- 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

- 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

- 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!