MIU prover from Escher, Godel, Bach

miu.py

import sys

def addU(s):
  if s[-1] == 'I':
    return [f'{s}U']
  else:
    return []

def dupMx(s):
  if s[0] == 'M':
    return [f'M{s[1:]}{s[1:]}']
  else:
    return []
  
def repIII(s):
  reps = []
  for i in range(len(s)):
    if s[i:i+3] == 'III':
      tok = f'{s[:i]}U{s[i+3:]}'
      if not tok in reps:
        reps.append(f'{s[:i]}U{s[i+3:]}')
  return reps
  
def repUU(s):
  reps = []
  for i in range(len(s)):
    if s[i:i+2] == 'UU':
      tok = f'{s[:i]}{s[i+2:]}'
      if not tok in reps:
        reps.append(f'{s[:i]}{s[i+2:]}')
  return reps

def getMU(d,start="MI"):
  toks = [start]
  newtoks = []
  i = 0
  while i < d:
    for t in toks:
      for s in addU(t):
        if s not in newtoks:
            newtoks.append(s)
      for s in dupMx(t):
        if s not in newtoks:
            newtoks.append(s)
      for s in repIII(t):
        if s not in newtoks:
            newtoks.append(s)
      for s in repUU(t):
        if s not in newtoks:
            newtoks.append(s)
    i += 1
    toks = [ *newtoks ]

  for t in toks:
    print(t)
  if 'MU' in toks:
    print(f'#toks = {len(toks)} Found MU')
  else:
    print(f'#toks = {len(toks)} No MU found yet')

def main():
  argc = len(sys.argv)
  if argc>1 and argc <3:
    getMU(int(sys.argv[1]))
  elif argc == 3:
    getMU(int(sys.argv[1]),sys.argv[2])
  else:
    getMU(2)

if __name__ == '__main__':
  main()