# Decision procedure: necessary condition #

We introduce a condition `Decstr`

and show that if a string `en`

is `Derivable`

, then `Decstr en`

holds.

Using this, we give a negative answer to the question: is `"MU"`

derivable?

## Tags #

miu, decision procedure

### Numerical condition on the `I`

count #

Suppose `st : Miustr`

. Then `count I st`

is the number of `I`

s in `st`

. We'll show, if
`Derivable st`

, then `count I st`

must be 1 or 2 modulo 3. To do this, it suffices to show that if
the `en : Miustr`

is derived from `st`

, then `count I en`

moudulo 3 is either equal to or is twice
`count I st`

, modulo 3.

Given `st en : Miustr`

, the relation `CountEquivOrEquivTwoMulMod3 st en`

holds if `st`

and
`en`

either have equal `count I`

, modulo 3, or `count I en`

is twice `count I st`

, modulo 3.

## Equations

- Miu.CountEquivOrEquivTwoMulMod3 st en = let a := List.count Miu.MiuAtom.I st; let b := List.count Miu.MiuAtom.I en; b ≡ a [MOD 3] ∨ b ≡ 2 * a [MOD 3]

## Instances For

`count_equiv_one_or_two_mod3_of_derivable`

shows any derivable string must have a `count I`

that
is 1 or 2 modulo 3.

Using the above theorem, we solve the MU puzzle, showing that `"MU"`

is not derivable.
Once we have proved that `Derivable`

is an instance of `DecidablePred`

, this will follow
immediately from `dec_trivial`

.

### Condition on `M`

#

That solves the MU puzzle, but we'll proceed by demonstrating the other necessary condition for a string to be derivable, namely that the string must start with an M and contain no M in its tail.

`Goodm xs`

holds if `xs : Miustr`

begins with `M`

and has no `M`

in its tail.

## Equations

- Miu.Goodm xs = (List.headI xs = Miu.MiuAtom.M ∧ Miu.MiuAtom.M ∉ List.tail xs)

## Instances For

## Equations

- Miu.instDecidablePredMiustrGoodm = id inferInstance

Demonstration that `"MI"`

starts with `M`

and has no `M`

in its tail.

We'll show, for each `i`

from 1 to 4, that if `en`

follows by Rule `i`

from `st`

and if
`Goodm st`

holds, then so does `Goodm en`

.

The proof of the next lemma is identical, on the tactic level, to the previous proof.

Any derivable string must begin with `M`

and have no `M`

in its tail.

We put together our two conditions to give one necessary condition `Decstr`

for an `Miustr`

to be
derivable.

`Decstr en`

is the condition that `count I en`

is 1 or 2 modulo 3, that `en`

starts with `M`

, and
that `en`

has no `M`

in its tail. We automatically derive that this is a decidable predicate.

## Equations

- Miu.Decstr en = (Miu.Goodm en ∧ (List.count Miu.MiuAtom.I en % 3 = 1 ∨ List.count Miu.MiuAtom.I en % 3 = 2))

## Instances For

## Equations

- Miu.instDecidablePredMiustrDecstr = id inferInstance

Suppose `en : Miustr`

. If `en`

is `Derivable`

, then the condition `Decstr en`

holds.