# The MU Puzzle

The puzzle cannot be solved: it is impossible to change the string MI into MU by repeatedly applying the given rules. In other words, MU is not a theorem of the MIU formal system. To prove this, one must step "outside" the formal system itself. Wikipedia

`using Metatheory, Test`

Here are the axioms of MU:

- Composition of the string monoid is associative
- Add a uf to the end of any string ending in I
- Double the string after the M
- Replace any III with a U
- Remove any UU

```
function ⋅ end
miu = @theory x y z begin
x ⋅ (y ⋅ z) --> (x ⋅ y) ⋅ z
x ⋅ :I ⋅ :END --> x ⋅ :I ⋅ :U ⋅ :END
:M ⋅ x ⋅ :END --> :M ⋅ x ⋅ x ⋅ :END
:I ⋅ :I ⋅ :I --> :U
x ⋅ :U ⋅ :U ⋅ y --> x ⋅ y
end
```

5-element Vector{RewriteRule}: ~x ⋅ (~y ⋅ ~z) --> (~x ⋅ ~y) ⋅ ~z (~x ⋅ I) ⋅ END --> ((~x ⋅ I) ⋅ U) ⋅ END (M ⋅ ~x) ⋅ END --> ((M ⋅ ~x) ⋅ ~x) ⋅ END (I ⋅ I) ⋅ I --> U ((~x ⋅ U) ⋅ U) ⋅ ~y --> ~x ⋅ ~y

No matter the timeout we set here, MU is not a theorem of the MIU system

```
params = SaturationParams(timeout = 12, eclasslimit = 8000)
start = :(M ⋅ I ⋅ END)
g = EGraph(start)
saturate!(g, miu)
@test false == areequal(g, miu, start, :(M ⋅ U ⋅ END); params = params)
```

Test Passed

*This page was generated using Literate.jl.*