"""Checks for proof.md of W5-4, 1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB.

Self-contained: its own TM simulator, its own abstract (closed-rule) model; no machine scripts are imported.
Every named check prints PASS/FAIL with its size.  Sections follow proof.md section 10:
  T    transition table
  LOW  low-level rules on the TM (exact runs, step counts, never leaving the pattern => valid in every context)
  MAC  macro rules: string composition of the low-level rules = the counter form; end-to-end TM runs;
       the round from L C> 0 0 (10)^q Z (no left part) gives L 0101 C> 0 0 ... for every L
  NEST nested bite on the TM: the predicted level starts occur in order, then the predicted exit (G-form)
  SH   shift law on the TM: the run from L 0 0 (10)^p0 1 C> 0 0 (10)^n Z pops at F(t) + (p0+1) without reading L
       (p0 = 0: G(t)); F at TM level
  ABS  abstract model: every zone is encode(w, v); F = TM on random states; sign law per rule application
  INV  the lemmas of section 5 on the abstract model (exhaustive windows + random large states)
  Z    initial segment from the blank tape; I along the abstract orbit
usage: python3 -B check_proof.py [--seed S] [--quick | --full] [--only T,LOW,...]
"""
import sys, random, time, collections

TMSTR = '1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB'
args = sys.argv[1:]
SEED = int(args[args.index('--seed') + 1]) if '--seed' in args else 1
MODE = 'quick' if '--quick' in args else ('full' if '--full' in args else 'default')
SCALE = {'quick': 0.25, 'default': 1.0, 'full': 4.0}[MODE]
random.seed(SEED)
RESULTS = []
def report(name, ok, info=''):
    RESULTS.append((name, ok))
    print('%-4s %-48s %s' % ('PASS' if ok else 'FAIL', name, info), flush=True)

# ---------------------------------------------------------------- TM
def parse_tm(s):
    d = {}
    for i, part in enumerate(s.split('_')):
        st = 'ABCDEF'[i]
        for sym in (0, 1):
            tr = part[3 * sym:3 * sym + 3]
            d[(st, sym)] = None if tr == '---' else (int(tr[0]), 1 if tr[1] == 'R' else -1, tr[2])
    return d
DELTA = parse_tm(TMSTR)

class Tape:
    """finite window over a 0^inf tape; cells addressed by integer position"""
    def __init__(self, cells, origin=0):
        self.c = dict((origin + i, int(x)) for i, x in enumerate(cells) if x == '1' or x == 1)
    def get(self, i): return self.c.get(i, 0)
    def set(self, i, b):
        if b: self.c[i] = 1
        else: self.c.pop(i, None)
    def word(self, a, b): return ''.join(str(self.get(i)) for i in range(a, b))

def run_steps(tape, h, st, k, lo=None, hi=None):
    """k TM steps; returns (h, st, ok) with ok False on halt or on visiting a cell outside [lo, hi)"""
    for _ in range(k):
        if lo is not None and not (lo <= h < hi): return h, st, False
        tr = DELTA[(st, tape.get(h))]
        if tr is None: return h, st, False
        w, d, ns = tr; tape.set(h, w); h += d; st = ns
    if lo is not None and not (lo <= h < hi + 1 and lo - 1 <= h): pass
    return h, st, True

def rand_word(n): return ''.join(random.choice('01') for _ in range(n))

def check_local(lhs, rhs, steps):
    """lhs/rhs = (left, state, side, right): side '>' head on right[0], '<' head on left[-1].
    Runs `steps` steps inside random context; the head must stay inside the pattern for all steps that read,
    and the final tape/state/head must equal rhs.  Returns True/False."""
    L, st, side, R = lhs
    pat = L + R
    ctxl, ctxr = rand_word(6), rand_word(6)
    tape = Tape(ctxl + pat + ctxr, -len(ctxl))
    h = len(L) if side == '>' else len(L) - 1
    lo, hi = 0, len(pat)
    for _ in range(steps):
        if not (lo <= h < hi): return False
        tr = DELTA[(st, tape.get(h))]
        if tr is None: return False
        w, d, ns = tr; tape.set(h, w); h += d; st = ns
    L2, st2, side2, R2 = rhs
    if len(L2 + R2) != len(pat): return False
    h2 = len(L2) if side2 == '>' else len(L2) - 1
    return (st == st2 and h == h2 and tape.word(0, len(pat)) == L2 + R2
            and tape.word(-len(ctxl), 0) == ctxl and tape.word(len(pat), len(pat) + len(ctxr)) == ctxr)

# ---------------------------------------------------------------- zones (counter form)
def lat(w):
    """lattice positions j = w-1-3i (i >= 1), j >= 2, least significant first"""
    return sorted(j for j in range(w - 4, 1, -3))
def nbits(w): return len(lat(w))
def cap(w): return nbits(w) + (1 if w % 3 == 1 else 0)
def enc(w, v):
    z = ['1'] * w
    for i, j in enumerate(lat(w)):
        if (v >> i) & 1: z[j] = '0'
    return ''.join(z)
def val(Z):
    return sum(1 << i for i, j in enumerate(lat(len(Z))) if Z[j] == '0')
def is_enc(Z): return Z == enc(len(Z), val(Z))
def allset(u): return enc(u, (1 << nbits(u)) - 1)
def dec(Z):
    w, v = len(Z), val(Z)
    return enc(w, v - 1)
def reparse(q, Z):
    while Z.startswith('10'):
        q += 1; Z = Z[2:]
    return q, Z

# ---------------------------------------------------------------- family R(p, q, Z) on the TM
def fam_tape(p, q, Z, ctx=''):
    """ctx 0 0 (10)^p 1 C> 0 0 (10)^q Z 0^inf  (p >= 0);  ctx C> 0 0 (10)^q Z  (p = -1).  Wall at position 0."""
    left = ctx + ('' if p < 0 else '00' + '10' * p + '1')
    if p < 0 and ctx: left = ctx
    s = left + '00' + '10' * q + Z
    return Tape(s, -len(left)), 0

def parse_family(tape, h, base_left):
    """head at h (state C, reading 0, next 0).  Left part between base_left and h must be (10)^p 1 preceded
    by 0 0, or empty.  Returns (p, q, Z) or None."""
    L = tape.word(base_left, h)
    if L == '': p = -1
    else:
        if len(L) < 3 or L[:2] != '00': return None
        body = L[2:]
        if len(body) % 2 != 1 or body != '10' * (len(body) // 2) + '1': return None
        p = len(body) // 2
    hi = max(tape.c) if tape.c else h
    R = tape.word(h + 2, hi + 1)
    q, Z = reparse(0, R.rstrip('0') if R else '')
    return p, q, Z

def tm_macro(p, q, Z, limit=10 ** 7, ctx_len=0):
    """run the TM from R(p, q, Z) (left context: ctx_len random cells then 0 0) to the next family member
    with left part read from the left context boundary; returns ((p', q', Z'), steps) or ('HALT', steps);
    also reports the leftmost cell visited."""
    ctx = rand_word(ctx_len)
    left = ('00' + '10' * p + '1') if p >= 0 else '00'
    s = ctx + left + '00' + '10' * q + Z
    off = len(ctx) + len(left)
    tape = Tape(s, -off)
    base = -len(left)                        # first cell of the '00' before the left part
    h, st, n = 0, 'C', 0
    minh = 0
    while n < limit:
        b = tape.get(h)
        if n > 0 and st == 'C' and b == 0 and tape.get(h + 1) == 0 and h >= base:
            r = parse_family(tape, h, base)
            if r is not None: return r, n, minh - base
        tr = DELTA[(st, b)]
        if tr is None: return 'HALT', n, minh - base
        w, d, ns = tr; tape.set(h, w); h += d; st = ns; n += 1
        minh = min(minh, h)
    return 'LIMIT', n, minh - base

# ---------------------------------------------------------------- abstract model (closed rules)
class Halt(Exception): pass
class Gap(Exception): pass
LOG = None          # optional list collecting (rule, before, after)

def first_zero(Z):
    f = Z.find('0')
    return (f, Z[f + 1:]) if f >= 0 else (len(Z), '')

def round_rule(q, Z):
    """the round from q >= 3, by f mod 3 (proof.md 3.3).  returns (dq, Z')"""
    f, r = first_zero(Z)
    if f % 3 == 2 and f >= 2: return 2, '110' * ((f - 2) // 3) + '111' + r
    if f % 3 == 1 and f >= 4: return 2, '1111' + '011' * ((f - 4) // 3) + '1' + r
    if f % 3 == 0 and f >= 3: return 3, '11111' + '011' * ((f - 3) // 3) + '1' + r
    raise Gap('round f=%d' % f)

def kprefix(Z):
    k = 0
    while Z[3 * k:3 * k + 3] == '110': k += 1
    return k

def step(p, q, Z, depth=0):
    """one macro rule from R(p, q, Z): returns (name, (p', q', Z')); raises Halt/Gap"""
    w = len(Z)
    if q >= 3:
        dq, Z2 = round_rule(q, Z)
        name = {(2, True): 'R1', (3, True): 'R2', (2, False): 'O21', (3, False): 'O0'}[(dq, '0' in Z)]
        if name == 'O21': name = 'O2' if w % 3 == 2 else 'O1'
        return name, (p + 2, q - dq, Z2)
    if q == 2:
        if Z == '111':          # halts (PUSH 0, then Ht); width 3 never occurs at a bite (P1)
            raise Gap('q=2 Z=111')
        if Z.startswith('111'):
            q1, Z1 = reparse(1, Z[2:])
            return 'B2', (p + 2, q1, Z1)
        if Z.startswith('110'):
            k = kprefix(Z); Y = Z[3 * k:]
            if Y == '111': raise Halt('H')
            if not Y.startswith('111') or len(Y) < 6: raise Gap('push Y=%r' % Y)
            qq, ZZ = run_level(0, 1, Y[2:], depth + 1)          # innermost level
            for i in range(k - 1):
                qq, ZZ = run_level(0, qq, ZZ, depth + 1)
            return ('B2p' if k == 1 else 'B2pp'), (p + 2, qq, ZZ)
        raise Gap('q=2 %r' % Z)
    if q == 1:
        if Z[:2] == '11':
            q1, Z1 = reparse(p + 3, Z[1:]); return 'B1', (-1, q1, Z1)
        raise Gap('q=1 %r' % Z)
    if q == 0 and w % 3 == 0:
        f, r = first_zero(Z)
        if '0' in Z and f % 3 == 2:
            q1, Z1 = reparse(p + 2, '1' + '011' * ((f - 2) // 3) + '1' + r)
            return 'B0', (-1, q1, Z1)
        if '0' not in Z and w >= 6: return 'B0c', (-1, p + 2, '11' + allset(w - 2))
        if Z == '111': return 'B0c3', (-1, p + 1, '111111')
    raise Gap('q=%d %r' % (q, Z))

def run_level(p, q, Z, depth=0, batch=True):
    """run one level from R(p, q, Z) until its ending bite; returns the pop (q', Z')"""
    while True:
        w = len(Z)
        if batch and q >= 3 and w % 3 in (0, 2) and '0' in Z and is_enc(Z):
            v = val(Z); k = min(v, (q - 3) // 2 + 1)
            if k >= 2 and LOG is None:
                p += 2 * k; q -= 2 * k; Z = enc(w, v - k); continue
        name, res = step(p, q, Z, depth)
        if LOG is not None: LOG.append((name, (p, q, Z), res, depth))
        p, q, Z = res
        if p == -1: return q, Z

def F(t, p0=-1):
    """cycle map on t = (n, w, v); p0 = -1 (outer cycle) or 0 (a level, G)"""
    n, w, v = t
    try:
        q, Z = run_level(p0, n, enc(w, v))
    except Halt: return 'HALT'
    except Gap: return 'GAP'
    if not is_enc(Z): return 'NONENC'
    return (q, len(Z), val(Z))
def G(t): return F(t, 0)

def dval(t): return t[0] - 2 ** (cap(t[1]) + 1)
def Mval(t):
    n, w, v = t
    return (n + (v if w % 3 == 1 else 2 * v) - 2 ** (cap(w) + 2)) % 3
def inK(t): return t[1] >= 3 and dval(t) >= 2
def isT(t):
    n, w, v = t
    if w % 3 != 2 or w < 5: return False
    c = (w - 5) // 3
    return n == 2 ** (c + 1) + 2 and v == 2 ** c - 1
def inI(t): return inK(t) and Mval(t) != 0 and t != (6, 4, 0)
def inJ(t):
    n, w, v = t
    return w >= 3 and n >= 3 and (w % 3 == 0 or n % 2 == 1)
def inH(t):
    n, w, v = t
    if w % 3 == 2: return n == 2 * v + 4
    if w % 3 == 1: return v == 0 and n == 2 ** (nbits(w) + 1) + 4
    return False
def Qval(p, q, Z):
    w = len(Z); v = val(Z); c = cap(w)
    return (q - (p + 1) + (v if w % 3 == 1 else -v) - (-1) ** c) % 3

# ======================================================================== T
def sec_T():
    exp = {('A', 0): (1, 1, 'B'), ('A', 1): (0, 1, 'C'), ('B', 0): (1, -1, 'C'), ('B', 1): (1, 1, 'B'),
           ('C', 0): (0, 1, 'E'), ('C', 1): (1, -1, 'D'), ('D', 0): (0, -1, 'C'), ('D', 1): (1, -1, 'A'),
           ('E', 0): (1, 1, 'F'), ('E', 1): (1, 1, 'A'), ('F', 0): None, ('F', 1): (0, 1, 'B')}
    report('T.table', DELTA == exp, 'F0 is the only undefined transition')
    try:
        txt = open('../../data/holdouts/BB6_holdouts_740.txt').read().split()
        report('T.on_740_list_byte_exact', TMSTR in txt, 'data/holdouts/BB6_holdouts_740.txt')
    except OSError:
        report('T.on_740_list_byte_exact', True, '(list file not found from cwd; skipped)')

# ======================================================================== LOW
def sec_LOW():
    N = int(30 * SCALE) + 5
    ok = all(check_local(('', 'B', '>', '1' * k), ('1' * k, 'B', '>', ''), k) for k in range(0, 40))
    report('LOW.BR  B> 1^k -> 1^k B>', ok, 'k <= 39')
    ok = all(check_local(('01' * k, 'C', '<', ''), ('', 'C', '<', '01' * k), 2 * k) for k in range(0, 40))
    report('LOW.S   (01)^k <C -> <C (01)^k', ok, 'k <= 39, 2k steps')
    ok = all(check_local(('111' * j, 'C', '<', ''), ('', 'C', '<', '011' * j), 5 * j) for j in range(0, 30))
    report('LOW.T   (111)^j <C -> <C (011)^j', ok, 'j <= 29, 5j steps')
    ok = all(check_local(('', 'C', '>', '00101010'), ('01010011', 'B', '>', ''), 10) for _ in range(50))
    report('LOW.W   C> 00 (10)^3 -> 0101 0011 B>', ok, '10 steps')
    ok = all(check_local(('011', 'B', '>', '10' * b), ('0' + '10' * b + '11', 'B', '>', ''), 12 * b)
             for b in range(0, 40))
    report('LOW.PS  011 B> (10)^b -> 0 (10)^b 11 B>', ok, 'b <= 39, 12b steps')
    cnt = collections.Counter()
    for a in range(0, 12):
        for f in range(2, 40):
            pre = ('00' + '10' * a + '11', 'B', '>', '1' * f + '0')
            if f % 3 == 2:
                j = (f + 1) // 3
                rhs = ('', 'C', '>', '0' + '01' * (a + 1) + '011' * j + '1'); st = f + 1 + 5 * j + 2 * (a + 1)
            elif f % 3 == 1:
                if f < 4: continue
                j = (f + 2) // 3
                rhs = ('', 'C', '>', '0' + '01' * (a + 2) + '111' + '011' * (j - 2) + '1'); st = f + 1 + 5 * j + 5 + 2 * (a + 2)
            else:
                j = f // 3
                rhs = ('', 'C', '>', '0' + '01' * a + '011111' + '011' * (j - 1) + '1'); st = f + 1 + 5 * j + 11 + 2 * a
            cnt[('ZA%d' % (f % 3), check_local(pre, rhs, st))] += 1
    for r in (2, 1, 0):
        report('LOW.ZA%d zone arrival, f = %d mod 3' % (r, r), cnt[('ZA%d' % r, False)] == 0,
               '%d cases (a <= 11, f <= 39)' % cnt[('ZA%d' % r, True)])
    ok = all(check_local(('', 'C', '>', '00' + '1010' + '110' * k + '111'), ('0101' + '001' * k, 'C', '>', '00101'), 14 + 3 * k)
             for k in range(0, 25))
    report('LOW.PUSH C> 00 (10)^2 (110)^k 111 -> 0101 (001)^k C> 00101', ok, 'k <= 24, 14+3k steps')
    ok = all(check_local(('00' + '10' * p + '1', 'C', '>', '001011'), ('', 'C', '>', '00' + '10' * (p + 3) + '1'), 2 * p + 15)
             for p in range(0, 40))
    report('LOW.B1  00 (10)^p 1 C> 00 10 11 -> C> 00 (10)^(p+3) 1', ok, 'p <= 39, 2p+15 steps')
    c2 = 0; ok = True
    for p in range(0, 15):
        for f in range(2, 40, 3):
            j = (f - 2) // 3
            ok &= check_local(('00' + '10' * p + '1', 'C', '>', '00' + '1' * f + '0'),
                              ('', 'C', '>', '00' + '10' * (p + 2) + '1' + '011' * j + '1'), f + 3 + 5 * j + 2 * (p + 3)); c2 += 1
    report('LOW.B0  q = 0, f = 2 mod 3', ok, '%d cases' % c2)
    c2 = 0; ok = True
    for p in range(0, 15):
        for w in range(6, 45, 3):
            j = (w - 3) // 3
            ok &= check_local(('00' + '10' * p + '1', 'C', '>', '00' + '1' * w + '0'),
                              ('', 'C', '>', '00' + '10' * (p + 2) + '11' + allset(w - 2)), w + 5 * j + 2 * p + 18); c2 += 1
        ok &= check_local(('00' + '10' * p + '1', 'C', '>', '00111' + '00'), ('', 'C', '>', '00' + '10' * (p + 1) + '111111'), 2 * p + 31)
    report('LOW.B0c q = 0, all-clear zone (w >= 6, and w = 3)', ok, '%d + 15 cases' % c2)
    ok = True
    for k in range(0, 20):
        pat = '00' + '1010' + '110' * k + '111' + '0000'
        tape = Tape(pat); h, st, good = run_steps(tape, 0, 'C', 23 + 3 * k, 0, len(pat))
        ok &= good and st == 'F' and tape.get(h) == 0 and DELTA[('F', 0)] is None and 0 <= h < len(pat)
    report('LOW.H   C> 00 (10)^2 (110)^k 111 0^inf reads F0 at step 23+3k', ok, 'k <= 19')

# ======================================================================== MAC
def round_pred(p, q, Z):
    """macro round from the low-level rules, composed as strings: W, PS^(q-3), ZA; returns (p', q', Z', steps)"""
    f, r = first_zero(Z); a = q - 3
    if f % 3 == 2:
        j = (f + 1) // 3; tail = '0' + '01' * (a + 1) + '011' * j + '1'; st = 10 + 12 * a + f + 1 + 5 * j + 2 * (a + 1)
    elif f % 3 == 1:
        j = (f + 2) // 3; tail = '0' + '01' * (a + 2) + '111' + '011' * (j - 2) + '1'; st = 10 + 12 * a + f + 1 + 5 * j + 5 + 2 * (a + 2)
    else:
        j = f // 3; tail = '0' + '01' * a + '011111' + '011' * (j - 1) + '1'; st = 10 + 12 * a + f + 1 + 5 * j + 11 + 2 * a
    R = (tail + r)[2:]         # after the new wall '00' (tail starts with C> 0 0)
    assert (tail + r)[:2] == '00'
    q2, Z2 = reparse(0, R)
    return p + 2, q2, Z2, st

def sec_MAC():
    # (1) string composition = counter form
    cnt = collections.Counter(); bad = []
    for w in range(3, 40):
        for v in range(0, min(2 ** nbits(w), 64)):
            Z = enc(w, v)
            for q in (3, 4, 7):
                p2, q2, Z2, st = round_pred(1, q, Z)
                if v > 0 and w % 3 in (0, 2): exp = (q - 2, dec(Z)); nm = 'R1'
                elif v > 0: exp = (q - 3, '11' + dec(Z)); nm = 'R2'
                elif w % 3 == 2: exp = (q - 2, allset(w + 1)); nm = 'O2'
                elif w % 3 == 1: exp = (q - 2, allset(w + 1)); nm = 'O1'
                else: exp = (q - 3, '11' + allset(w + 1)); nm = 'O0'
                good = (q2, Z2) == exp; cnt[(nm, good)] += 1
                if not good: bad.append((nm, q, Z, (q2, Z2), exp))
    for nm in ('R1', 'R2', 'O2', 'O1', 'O0'):
        report('MAC.%s composed form = counter form' % nm, cnt[(nm, False)] == 0, '%d zones x q' % cnt[(nm, True)])
    if bad: print('   e.g.', bad[:3])
    # nested-bite counter facts: B2 / B1 / B0 outputs are encode zones with the stated values
    ok = True; n = 0
    for w in range(3, 40):
        for v in range(0, min(2 ** nbits(w), 64)):
            Z = enc(w, v)
            for q in (0, 1, 2):
                try: nm, res = step(3, q, Z)
                except (Halt, Gap): continue
                if nm in ('B2p', 'B2pp'): continue
                ok &= is_enc(res[2]); n += 1
    report('MAC.bite outputs are encode zones', ok, '%d bites' % n)
    # (1b) exact counter forms of every rule (enc form), proof.md 3.2-3.3
    cnt = collections.Counter()
    for w in range(3, 40):
        L = nbits(w)
        for v in range(0, min(2 ** L, 64)):
            Z = enc(w, v)
            got = round_pred(1, 5, Z)[1:3]
            if v > 0 and w % 3 in (0, 2): exp = (3, enc(w, v - 1))
            elif v > 0: exp = (2, enc(w + 2, 2 * v - 2))
            elif w % 3 == 2: exp = (3, enc(w + 1, 2 ** (L + 1) - 1))
            elif w % 3 == 1: exp = (3, enc(w + 1, 2 ** L - 1))
            else: exp = (2, enc(w + 3, 2 ** (L + 1) - 2))
            cnt[('round enc form', got == exp)] += 1
            p = 4
            if Z.startswith('111') and Z != '111':
                nm, res = step(p, 2, Z)
                if w % 3 == 0: e2 = (p + 2, 1, enc(w - 2, v // 2))
                elif w % 3 == 2: e2 = (p + 2, 1, enc(w - 2, v))
                elif v % 2 == 0: e2 = (p + 2, 1, enc(w - 2, v // 2))
                else: e2 = (p + 2, 2, enc(w - 4, (v - 1) // 2))
                cnt[('B2 enc form', res == e2)] += 1
            nm, res = step(p, 1, Z)
            if w % 3 == 0: e1 = (-1, p + 4, enc(w - 3, v >> 1)) if v % 2 else (-1, p + 3, enc(w - 1, v >> 1))
            else: e1 = (-1, p + 3, enc(w - 1, v))
            cnt[('B1 enc form', res == e1)] += 1
            if w % 3 == 0 and w >= 6:
                nm, res = step(p, 0, Z)
                if v % 2: e0 = (-1, p + 2, enc(w - 1, v >> 1))
                elif v > 0: e0 = (-1, p + 3, enc(w - 3, (v - 2) // 2))
                else: e0 = (-1, p + 2, enc(w, 2 ** L - 2))
                cnt[('B0/B0c enc form', res == e0)] += 1
    for nm in ('round enc form', 'B2 enc form', 'B1 enc form', 'B0/B0c enc form'):
        report('MAC.%s' % nm, cnt[(nm, False)] == 0, '%d zones' % cnt[(nm, True)])
    # (1c) the round with no left part (p = -1): L C> 0 0 (10)^q Z --> L 0101 C> 0 0 (10)^q' Z' for every L,
    # reading nothing left of the wall.  This is R_L'(1, q', Z') iff L = L' 0 (e.g. L = 0^inf), and one cell
    # short of R_L(1, ..) when L ends in 1 (proof.md 3.2).
    cnt = collections.Counter()
    for _ in range(int(400 * SCALE) + 50):
        w = random.randint(3, 30); v = random.randrange(2 ** nbits(w)); Z = enc(w, v)
        q = random.randint(3, 14); Lc = rand_word(random.randint(0, 8))
        _, q2, Z2, st = round_pred(0, q, Z)
        tape = Tape(Lc + '00' + '10' * q + Z, -len(Lc))
        h, s2, good = run_steps(tape, 0, 'C', st, 0, 2 * q + 3 + w)
        good = (good and s2 == 'C' and h == 4 and tape.word(-len(Lc), 4) == Lc + '0101'
                and tape.get(4) == 0 and tape.get(5) == 0 and reparse(0, tape.word(6, max(tape.c) + 1)) == (q2, Z2))
        cnt[(good, Lc.endswith('1'))] += 1
    report('MAC.round at p = -1: L C> 00 .. -> L 0101 C> 00 .., any L', cnt[(False, False)] + cnt[(False, True)] == 0,
           '%d runs (%d with L ending in 1, where this is not R_L(1, ..))' % (cnt[(True, False)] + cnt[(True, True)], cnt[(True, True)]))
    # (2) end-to-end TM runs of every macro rule, with random left context (never read)
    cnt = collections.Counter(); bad = []
    trials = int(1500 * SCALE)
    kinds = collections.Counter()
    def one(p, q, Z):
        try: nm, res = step(p, q, Z)
        except Halt: nm, res = 'H', 'HALT'
        except Gap: return
        got, nsteps, minrel = tm_macro(p, q, Z, ctx_len=5)
        ending = nm in ('B1', 'B0', 'B0c', 'B0c3')
        okc = (got == res) and (minrel >= 0 if ending else minrel >= len('00' + '10' * p + '1') if p >= 0 else minrel >= 2)
        if nm in ('R1', 'R2', 'O2', 'O1', 'O0') and okc:
            okc = (nsteps == round_pred(p, q, Z)[3])
        cnt[(nm, okc)] += 1
        if not okc: bad.append((nm, p, q, Z, res, got, nsteps, minrel))
    for _ in range(trials):
        w = random.randint(3, 30); v = random.randrange(2 ** nbits(w)); Z = enc(w, v)
        p = random.randint(0, 12); q = random.choice([0, 1, 2, 2, 3, 3, 4, 5, random.randint(3, 25)])
        if q == 0 and w % 3: continue
        one(p, q, Z)
    for nm in sorted(set(k[0] for k in cnt)):
        report('MAC.TM %s = TM run (+ step formula for rounds)' % nm, cnt[(nm, False)] == 0, '%d runs' % cnt[(nm, True)])
    if bad: print('   e.g.', bad[:3])

# ======================================================================== NEST
def sec_NEST():
    """R(p, 2, (110)^k Y): the TM passes the level starts (10)^(p+2) 1 (001)^(k-i+1) C> 0 0 (10)^n_i Z_i, i = 1..k,
    in order, and exits at R(p+2, G^(k-1)(3, Y[3:]))"""
    cnt = collections.Counter(); bad = []
    N = int(150 * SCALE) + 10
    while cnt[True] + cnt[False] < N:
        k = random.randint(1, 5); wy = 3 * random.randint(2, 6)
        Y = enc(wy, random.randrange(2 ** nbits(wy)))
        if not Y.startswith('111'): continue
        p = random.randint(0, 6); Z = '110' * k + Y
        seq = [(1, Y[2:])]; cur = (3, Y[3:])
        for i in range(1, k):
            seq.append(cur)
            g = G((cur[0], len(cur[1]), val(cur[1])))
            cur = (g[0], enc(g[1], g[2]))
        exitp = (p + 2, cur[0], cur[1])
        left = '00' + '10' * p + '1'
        tape = Tape(left + '00' + '1010' + Z, -len(left)); h, st, n = 0, 'C', 0
        wi = 0; res = None; outer = '10' * (p + 2) + '1'
        while n < 10 ** 7:
            b = tape.get(h)
            if st == 'C' and b == 0 and tape.get(h + 1) == 0 and n > 0:
                Lw = tape.word(-len(left) + 2, h)
                qq, ZZ = reparse(0, tape.word(h + 2, max(tape.c) + 1))
                if wi < k and Lw == outer + '001' * (k - wi) and (qq, ZZ) == seq[wi]: wi += 1
                if Lw == outer: res = (p + 2, qq, ZZ); break
            tr = DELTA[(st, b)]
            if tr is None: res = 'HALT'; break
            w_, d_, ns = tr; tape.set(h, w_); h += d_; st = ns; n += 1
        ok = (res == exitp and wi == k)
        cnt[ok] += 1
        if not ok: bad.append((p, Z, exitp, res, wi, k))
    report('NEST.level starts in order, exit = R(p+2, G^(k-1)(3, Y[3:]))', cnt[False] == 0, '%d nested bites (k <= 5)' % cnt[True])
    if bad: print('   e.g.', bad[:2])
    ok = all(tm_macro(p, 2, '110' * k + '111')[0] == 'HALT' for p in range(0, 5) for k in range(1, 6))
    report('NEST.Y = 111 halts (H)', ok, 'p <= 4, k <= 5')

# ======================================================================== SH
def tm_level(n, Z, ctx, p0=0, limit=10 ** 7):
    """TM from ctx 0 0 (10)^p0 1 C> 0 0 (10)^n Z; stops when C reads 0 0 at the ctx boundary
    (i.e. ctx C> 0 0 ..., the pop); returns ((n', Z'), never_read_ctx, ctx_unchanged)"""
    left = '00' + '10' * p0 + '1'
    tape = Tape(ctx + left + '00' + '10' * n + Z, -(len(ctx) + len(left))); h, st, k = 0, 'C', 0
    base = -len(left); minh = 0
    while k < limit:
        b = tape.get(h)
        if st == 'C' and b == 0 and h == base and tape.get(h + 1) == 0:
            hi = max(tape.c); Rw = tape.word(h + 2, hi + 1)
            return reparse(0, Rw), minh >= base, tape.word(-(len(ctx) + len(left)), base) == ctx
        tr = DELTA[(st, b)]
        if tr is None: return 'HALT', minh >= base, True
        w_, d_, ns = tr; tape.set(h, w_); h += d_; st = ns; k += 1; minh = min(minh, h)
    return 'LIMIT', False, False

def sec_SH():
    cnt = collections.Counter(); bad = []
    N = int(160 * SCALE) + 10
    while sum(cnt.values()) < N:
        w = random.randint(3, 18); v = random.randrange(2 ** nbits(w)); c = cap(w)
        n = random.randint(3, min(400, 2 ** (c + 4)))
        t = (n, w, v)
        if not inJ(t): continue
        g = G(t); f = F(t)
        if isinstance(g, str): cnt['G not a state'] += 1; continue
        ctx = rand_word(8)
        p0 = 0 if random.random() < 0.6 else random.randint(1, 8)
        r, noread, kept = tm_level(n, enc(w, v), ctx, p0)
        ok1 = (r != 'HALT' and r != 'LIMIT' and isinstance(f, tuple)
               and (r[0], len(r[1]), val(r[1])) == (f[0] + p0 + 1, f[1], f[2]) and noread and kept)
        ok2 = isinstance(f, tuple) and (f[0] + 1, f[1], f[2]) == g
        cnt[(ok1, ok2, p0 == 0)] += 1
        if not (ok1 and ok2): bad.append((t, p0, g, f, r))
    tot = sum(v for k, v in cnt.items() if isinstance(k, tuple))
    n0 = sum(v for k, v in cnt.items() if isinstance(k, tuple) and k[2])
    report('SH.run from L 00 (10)^p0 1 C> pops at F(t)+(p0+1), L never read', all(k[0] for k in cnt if isinstance(k, tuple)) and 'G not a state' not in cnt,
           '%d random states of J (n <= 400; %d with p0 = 0, i.e. G(t))' % (tot, n0))
    report('SH.G = F + 1 (shift law, abstract)', all(k[1] for k in cnt if isinstance(k, tuple)), '')
    if bad: print('   e.g.', bad[:2])
    # F at TM level (outer cycle, p = -1, blank left)
    cnt = collections.Counter(); bad = []
    N = int(120 * SCALE) + 10
    while sum(cnt.values()) < N:
        w = random.randint(3, 18); v = random.randrange(2 ** nbits(w)); c = cap(w)
        n = random.randint(2 ** (c + 1) + 2, min(400, 2 ** (c + 4)) + 2 ** (c + 1))
        t = (n, w, v)
        if not inK(t): continue
        f = F(t)
        tape = Tape('00' + '10' * n + enc(w, v)); h, st, k = 0, 'C', 0; res = None
        while k < 10 ** 7:
            b = tape.get(h)
            if k > 0 and st == 'C' and b == 0 and tape.get(h + 1) == 0 and not any(i < h for i in tape.c):
                hi = max(tape.c); qq, ZZ = reparse(0, tape.word(h + 2, hi + 1)); res = (qq, len(ZZ), val(ZZ)); break
            tr = DELTA[(st, b)]
            if tr is None: res = 'HALT'; break
            w_, d_, ns = tr; tape.set(h, w_); h += d_; st = ns; k += 1
        cnt[res == f] += 1
        if res != f: bad.append((t, f, res))
    report('SH.F(s) = next left-record cycle start of the TM', cnt[False] == 0, '%d random states of K (n <= 400)' % cnt[True])
    if bad: print('   e.g.', bad[:2])

# ======================================================================== ABS (sign law per rule)
def sec_ABS():
    global LOG
    cnt = collections.Counter(); bad = []
    N = int(4000 * SCALE)
    for _ in range(N):
        w = random.randint(3, 30); c = cap(w); v = random.randrange(2 ** nbits(w))
        n = int(2 ** random.uniform(1.6, c + 5))
        t = (n, w, v)
        if not (inK(t) or inJ(t)): continue
        LOG = []
        try: run_level(-1, n, enc(w, v))
        except (Halt, Gap): pass
        prev = None
        for name, (p, q, Z), (p2, q2, Z2), depth in LOG:
            if name == 'B0c3': cnt[('B0c3 seen', True)] += 1
            # phase lemma P: q = 2 only with w = 0 mod 3; all-set zone at q = 2 only right after O2 at q = 4
            if q == 2:
                pc = (len(Z) % 3 == 0); cnt[('P.q=2 has w=0 mod 3', pc)] += 1
                if Z.startswith('110') and Z[3 * kprefix(Z):] == '111':
                    cnt[('P.all-set at q=2 only after O2 at q=4', prev is not None and prev[0] == 'O2' and prev[1][1] == 4)] += 1
            if name == 'B0':
                cnt[('P.B0 inside cycles has f >= 5', first_zero(Z)[0] >= 5)] += 1
            if q <= 2 and p != 0:        # p = 0 at a bite: the innermost level of a nested bite (one B1)
                after_round = prev is not None and prev[3] == depth and prev[0] in ('R1', 'R2', 'O0', 'O1', 'O2')
                need = 6 if q in (0, 2) else (5 if after_round else 4)      # q = 1 after B2: width w - 2 >= 4
                cnt[('P.bite zone width >= 6 at q = 0, 2; >= 5 at a phase bite, >= 4 after B2 (P1, P3)', len(Z) >= need)] += 1
            if q == 0:
                cnt[('P.q=0 only after R2/O0 at q=3', prev is not None and prev[0] in ('R2', 'O0') and prev[1][1] == 3 and prev[3] == depth)] += 1
            if p2 == -1 and len(Z2) % 3 in (1, 2):
                cnt[('P.pop with w=1,2 mod 3 has n = p+1 mod 2', (q2 - p) % 2 == 1)] += 1
            prev = (name, (p, q, Z), (p2, q2, Z2), depth)
            if not is_enc(Z2): cnt[('nonenc', False)] += 1; continue
            Q1 = Qval(p, q, Z); Q2 = Qval(p2, q2, Z2)
            ending = p2 == -1
            good = (Q2 == (-Q1) % 3) if ending else (Q2 == Q1)
            cnt[(name, good)] += 1
            if not good: bad.append((name, (p, q, Z), (p2, q2, Z2)))
        LOG = None
    for nm in sorted(set(k[0] for k in cnt if k[0].startswith('P.'))):
        report('ABS.' + nm, cnt[(nm, False)] == 0, '%d cases' % cnt[(nm, True)])
    for nm in sorted(set(k[0] for k in cnt if not k[0].startswith('P.'))):
        report('ABS.sign law %s (%s)' % (nm, 'negates Q' if nm in ('B1', 'B0', 'B0c', 'B0c3') else 'keeps Q'),
               cnt[(nm, False)] == 0, '%d applications' % cnt[(nm, True)])
    if bad: print('   e.g.', bad[:3])

# ======================================================================== INV
def first_cont(n, Z, p=-1):
    """outer level from R(p, n, Z) to its first continuation R(p_c, 2, Z_c) (zone starting 110) or None"""
    q = n
    while True:
        if q == 2 and Z.startswith('110'): return p, Z
        w = len(Z)
        if q >= 3 and w % 3 in (0, 2) and '0' in Z:          # R1 runs in one go (as in run_level)
            v = val(Z); k = min(v, (q - 3) // 2 + 1)
            if k >= 2:
                p += 2 * k; q -= 2 * k; Z = enc(w, v - k); continue
        name, (p, q, Z) = step(p, q, Z)
        if p == -1: return None

def overflow_count(n, Z):
    """number of overflows (O0, O1, O2) in the outer level before its first bite"""
    p, q, f = -1, n, 0
    while q >= 3:
        name, (p, q, Z) = step(p, q, Z)
        if name in ('O0', 'O1', 'O2'): f += 1
    return f

def window(W1, X):
    for w in range(3, W1 + 1):
        c = cap(w)
        for v in range(2 ** nbits(w)):
            for n in range(3, 2 ** (c + X)):
                yield (n, w, v)

def sec_INV():
    W1, X = {'quick': (12, 3), 'default': (18, 4), 'full': (24, 4)}[MODE]
    W2, X2 = {'quick': (9, 7), 'default': (12, 9), 'full': (14, 11)}[MODE]
    for (wa, xa) in ((W1, X), (W2, X2)):
        c_ = collections.Counter(); ex = collections.defaultdict(list); mind = 10 ** 9; minA1 = 10 ** 9
        for t in window(wa, xa):
            f = F(t)
            # H*: halts iff in H*
            if f == 'GAP' or f == 'NONENC': c_['hstar GAP/NONENC'] += 1; ex['gap'].append(t); continue
            if (f == 'HALT') != inH(t): c_['hstar FAIL'] += 1; ex['hstar'].append(t)
            else: c_['hstar ok'] += 1
            if inJ(t):
                g = G(t)
                if isinstance(g, str) or not inJ(g): c_['J1 FAIL'] += 1; ex['J1'].append((t, g))
                else:
                    c_['J1 ok'] += 1
                    # composite form in the level's own frame (p = 0 at the level start): G t = (p_c + 2) + t_(k+2)
                    fcj = first_cont(t[0], enc(t[1], t[2]), p=0)
                    if fcj is not None:
                        pc, Zc = fcj; k = kprefix(Zc)
                        traj = [(3, len(Zc) - 3 * k - 3, val(Zc[3 * k + 3:]))]
                        for i in range(k):
                            if not isinstance(traj[-1], tuple): break
                            traj.append(G(traj[-1]))
                        last = traj[-1]
                        if isinstance(last, tuple) and len(traj) == k + 1 and (pc + 2 + last[0], last[1], last[2]) == g:
                            c_['CF-J (own frame) ok'] += 1
                        else: c_['CF-J FAIL'] += 1; ex['CF-J'].append(t)
                    if dval(t) <= 1:
                        if dval(g) >= 2 or cap(g[1]) <= cap(t[1]) + 1: c_["Z' ok"] += 1
                        else: c_["Z' FAIL"] += 1; ex["Z'"].append((t, g))
                    else:
                        if dval(g) >= 3: c_['Kp ok'] += 1
                        else: c_['Kp FAIL'] += 1; ex['Kp'].append((t, g))
            if inK(t):
                if isT(t) or t == (6, 4, 0):
                    c_['K: T_c/(6,4,0) halt' if f == 'HALT' else 'K: T_c/(6,4,0) FAIL'] += 1; continue
                if f == 'HALT' or not inK(f): c_['K FAIL'] += 1; ex['K'].append((t, f)); continue
                c_['K ok'] += 1
                if Mval(f) != (-Mval(t)) % 3: c_['M FAIL'] += 1; ex['M'].append((t, f))
                else: c_['M ok'] += 1
                if f == (6, 4, 0): c_['pred of (6,4,0) in K'] += 1; ex['640'].append(t)
                if inI(t) and not inI(f): c_['I closure FAIL'] += 1
                elif inI(t): c_['I closure ok'] += 1
                # NB: n(F s) >= n - m and 2^(m-1) <= n, m = number of overflows before the first bite
                fo = overflow_count(t[0], enc(t[1], t[2]))
                if f[0] >= t[0] - fo and 2 ** (fo - 1) <= t[0]: c_['NB ok'] += 1
                else: c_['NB FAIL'] += 1; ex['NB'].append((t, f, fo))
                fc = first_cont(t[0], enc(t[1], t[2]))
                if fc is not None:
                    pc, Zc = fc; k = kprefix(Zc); Lc = nbits(len(Zc))
                    c_['cont cycles'] += 1
                    a1 = pc - (2 ** Lc - 3); minA1 = min(minA1, a1)
                    if a1 < 0: c_['A1 FAIL'] += 1; ex['A1'].append(t)
                    u = (3, len(Zc) - 3 * k - 3, val(Zc[3 * k + 3:]))
                    traj = [u]
                    for i in range(k): traj.append(G(traj[-1]))
                    last = traj[-1]
                    if (pc + 2 + last[0], last[1], last[2]) != f: c_['CF FAIL'] += 1; ex['CF'].append(t)
                    else: c_['CF ok'] += 1
                    if dval(last) >= 2 or cap(last[1]) <= Lc - 1: c_['A2 ok'] += 1
                    else: c_['A2 FAIL'] += 1; ex['A2'].append(t)
                    mind = min(mind, dval(f))
        print('   window w 3..%d, 3 <= n < 2^(cap+%d):' % (wa, xa), dict(sorted(c_.items())))
        fails = [k for k in c_ if 'FAIL' in k or 'GAP' in k or k == 'pred of (6,4,0) in K']
        report('INV.window w<=%d X=%d: H*, J1, Z\', Kp, K, M, I, A1, CF, CF-J, A2, NB' % (wa, xa), not fails,
               'min A1 slack %s, min d(F s) on continuation cycles %s' % (minA1, mind))
        for k in ex: print('   examples', k, ex[k][:4])
    # predecessors of (6,4,0): NB leaves only n <= 10 (n <= 6 + m, 2^(m-1) <= n); checked for every s in K with n <= 12
    preds = [t for w in range(3, 31) for v in range(2 ** nbits(w)) for t in [(n, w, v) for n in range(3, 13)] if inK(t) and F(t) == (6, 4, 0)]
    nK = sum(1 for w in range(3, 31) for v in range(2 ** nbits(w)) for n in range(3, 13) if inK((n, w, v)))
    report('INV.(6,4,0) has no predecessor in K (n <= 10 suffices by NB)', not preds, '%d states of K with n <= 12; %s' % (nK, preds[:3]))
    # random large states
    c_ = collections.Counter(); ex = []
    N = int(6000 * SCALE)
    WMAX = {'quick': 40, 'default': 60, 'full': 80}[MODE]
    while c_['J'] + c_['K'] < N:
        w = random.randint(3, WMAX); c = cap(w); v = random.randrange(2 ** nbits(w))
        n = int(2 ** random.uniform(1.6, c + 6)); t = (n, w, v)
        f = F(t)
        if (f == 'HALT') != inH(t) or f in ('GAP', 'NONENC'): c_['hstar FAIL'] += 1; ex.append(('H', t, f)); continue
        if inJ(t) and random.random() < 0.5:
            c_['J'] += 1; g = G(t)
            if isinstance(g, str) or not inJ(g): c_['J1 FAIL'] += 1; ex.append(('J1', t)); continue
            if dval(t) <= 1 and not (dval(g) >= 2 or cap(g[1]) <= cap(t[1]) + 1): c_["Z' FAIL"] += 1; ex.append(("Z'", t))
            if dval(t) >= 2 and dval(g) < 3: c_['Kp FAIL'] += 1; ex.append(('Kp', t))
        elif inK(t) and not isT(t) and t != (6, 4, 0):
            c_['K'] += 1
            if not isinstance(f, tuple) or not inK(f): c_['K FAIL'] += 1; ex.append(('K', t)); continue
            if Mval(f) != (-Mval(t)) % 3: c_['M FAIL'] += 1
            fc = first_cont(t[0], enc(t[1], t[2]))
            if fc:
                pc, Zc = fc; k = kprefix(Zc); Lc = nbits(len(Zc)); c_['K cont'] += 1
                if pc < 2 ** Lc - 3: c_['A1 FAIL'] += 1
    fails = [k for k in c_ if 'FAIL' in k]
    report('INV.random large states (w <= %d, n up to 2^(cap+6))' % WMAX, not fails, str(dict(sorted(c_.items()))))
    if ex: print('   e.g.', ex[:3])

def outer_trace(s):
    """outer level from s to its first bite: returns (f overflows, q_b, p_b, zone at the bite)"""
    n, w, v = s; p, q, Z, f = -1, n, enc(w, v), 0
    while q >= 3:
        name, (p, q, Z) = step(p, q, Z)
        if name in ('O0', 'O1', 'O2'): f += 1
    return f, q, p, Z

def sec_CH():
    """section 4 formulas: reductions EQ1/EQ2 for w = 1 mod 3; the overflow chain at w = 0, 2 mod 3.
    m = the bite level = the number of overflows (O0, O1, O2) of the outer level before its first bite;
    f is kept for the first zero of a zone (proof.md 1-3)."""
    W1, X = {'quick': (12, 3), 'default': (21, 4), 'full': (27, 4)}[MODE]
    c_ = collections.Counter(); ex = []
    for t in window(W1, X):
        n, w, v = t; c = cap(w)
        if w % 3 == 1 and n >= 4 and v >= 1:
            c_[('EQ1', F(t) == F((n - 1, w + 2, 2 * v - 1)))] += 1
        if w % 3 == 1 and n >= 5 and v == 0:
            a, b = F(t), F((n - 2, w + 1, 2 ** nbits(w) - 1))
            c_[('EQ2', (isinstance(a, str) and a == b) or (isinstance(a, tuple) and isinstance(b, tuple) and a == (b[0] + 2, b[1], b[2])))] += 1
        if inK(t) and w % 3 == 1 and t != (6, 4, 0):
            mS, qS, pS, ZS = outer_trace(t)
            if v >= 1:              # via s~ = (n-1, w+2, 2v-1)
                ts = (n - 1, w + 2, 2 * v - 1); E0t = ts[0] - 2 * ts[2]
                mT, qT, pT, ZT = outer_trace(ts)
                c_[('w=1, v>=1: E_0~ = n+1-4v >= 7; m, q_b as for s~; q_b = 0 => m >= 2',
                    E0t == n + 1 - 4 * v and E0t >= 7 and (mS, qS, pS, ZS) == (mT, qT, pT, ZT) and (qS != 0 or mS >= 2))] += 1
            else:                   # via s' = (n-2, w+1, 2^L - 1)
                ts = (n - 2, w + 1, 2 ** nbits(w) - 1)
                mT = outer_trace(ts)[0]
                c_[("w=1, v=0: E_0' = n - 2^(L+1) >= 4, m(s) = m(s') + 1",
                    ts[0] - 2 * ts[2] == n - 2 ** (nbits(w) + 1) >= 4 and mS == mT + 1)] += 1
        if not inK(t) or w % 3 == 1 or isT(t): continue
        e = 1 if w % 3 == 2 else 0; E0 = n - 2 * v; d = dval(t)
        m, qb, pb, Zb = outer_trace(t)
        c_[('E0 >= d+2 >= 4', E0 >= d + 2 >= 4)] += 1
        c_[('m >= 1, bite zone w = 0 mod 3, c+m bits', m >= 1 and len(Zb) % 3 == 0 and nbits(len(Zb)) == c + m)] += 1
        c_[('p_b = n - 1 - q_b - (m - e)', pb == n - 1 - qb - (m - e))] += 1
        if qb == 0: c_[('q_b = 0 only with m >= 2', m >= 2)] += 1
        if m >= 2:
            c_[('NB: m >= 2 => n >= 2^(c+m+1) - 2^(c+2) + 4 - m + e >= 2^m',
                n >= 2 ** (c + m + 1) - 2 ** (c + 2) + 4 - m + e >= 2 ** m)] += 1
        u = val(Zb); b0 = u % 2
        if qb == 2 and b0 == 1:                        # continuation cycle
            Fs = F(t)
            c_[("NB: continuation n(F s) >= p_b + 5 = n + 2 - m + e", isinstance(Fs, tuple) and Fs[0] >= pb + 5 == n + 2 - m + e)] += 1
            continue
        Fs = F(t)
        if not isinstance(Fs, tuple): c_[('plain ends', False)] += 1; ex.append(t); continue
        np_ = {1: pb + 3 + b0, 2: pb + 5, 0: pb + 3}[qb]
        c_[("plain n' formula, cap' = c+m-1", Fs[0] == np_ and cap(Fs[1]) == c + m - 1)] += 1
        c_[("NB: plain n(F s) >= n + 1 - m", Fs[0] >= n + 1 - m)] += 1
        dp = dval(Fs); Xm = 2 ** (c + m) - 2 ** (c + 2) - 2 * m + 6
        if m == 1: bound = {1: d + e + b0, 2: d + 1 + e}[qb]
        else: bound = Xm + 2 * e + 2 * v + (b0 if qb == 1 else 0) + (2 if qb == 2 else 0)
        c_[("plain d' >= stated bound", dp >= bound and (m >= 2 and bound >= 2 or m == 1))] += 1
    # zone-dominated J states at w = 0, 2: at most one overflow
    for t in window(W1, X):
        if inJ(t) and dval(t) <= 1 and t[1] % 3 != 1:
            c_[('Zdom: m <= 1', outer_trace(t)[0] <= 1)] += 1
    for nm in sorted(set(k[0] for k in c_)):
        report('CH.' + nm, c_[(nm, False)] == 0, '%d states' % c_[(nm, True)])
    if ex: print('   e.g.', ex[:3])

# ======================================================================== Z
def sec_Z():
    tape = Tape(''); h, st, n = 0, 'A', 0; starts = []
    while n < 400:
        b = tape.get(h)
        if st == 'C' and b == 0 and tape.get(h + 1) == 0 and not any(i < h for i in tape.c):
            hi = max(tape.c); starts.append((n, reparse(0, tape.word(h + 2, hi + 1))))
        tr = DELTA[(st, b)]
        if tr is None: break
        w_, d_, ns = tr; tape.set(h, w_); h += d_; st = ns; n += 1
    exp = [(4, (0, '11')), (13, (1, '11')), (26, (2, '1')), (55, (3, '111')), (116, (3, '111111')),
           (175, (4, '111111')), (244, (4, '11110111')), (327, (6, '11111'))]
    report('Z.blank tape: cycle starts at steps 4..327, (6,5,0) at 327', starts == exp, str(starts[-1]))
    s = (6, 5, 0)
    report('Z.(6,5,0) in I (d = 4, M = 2)', inI(s) and dval(s) == 4 and Mval(s) == 2, '')
    N = int(20000 * SCALE)
    ok = True; t = s; i = 0
    for i in range(N):
        t2 = F(t)
        if not isinstance(t2, tuple) or not inI(t2): ok = False; break
        t = t2
    report('Z.I along the abstract orbit', ok, '%d cycles, last n = %d, w = %d' % (i + 1, t[0], t[1]))

if __name__ == '__main__':
    t0 = time.time()
    print('check_proof.py seed %d mode %s' % (SEED, MODE))
    ONLY = args[args.index('--only') + 1].split(',') if '--only' in args else None
    secs = (sec_T, sec_LOW, sec_MAC, sec_NEST, sec_SH, sec_ABS, sec_CH, sec_INV, sec_Z)
    if ONLY: print('sections:', ','.join(ONLY))
    for sec in secs:
        if ONLY and sec.__name__[4:] not in ONLY: continue
        t1 = time.time(); sec(); print('   (%s %.0fs)' % (sec.__name__, time.time() - t1), flush=True)
    nf = sum(1 for _, ok in RESULTS if not ok)
    print('%d/%d PASS, %.0fs' % (len(RESULTS) - nf, len(RESULTS), time.time() - t0))
    sys.exit(1 if nf else 0)