mathlib3

5d2256da - feat(miu_language): a formalisation of the MIU language described by D. Hofstadter in "Gödel, Escher, Bach". (#3739)

feat(miu_language): a formalisation of the MIU language described by D. Hofstadter in "Gödel, Escher, Bach". (#3739) We define an inductive type `derivable` so that `derivable x` represents the notion that the MIU string `x` is derivable in the MIU language. We show `derivable x` is equivalent to `decstr x`, viz. the condition that `x` begins with an `M`, has no `M` in its tail, and for which `count I` is congruent to 1 or 2 modulo 3. By showing `decidable_pred decstr`, we deduce that `derivable` is decidable.