#!/usr/bin/env python3
"""symexec.py: a small symbolic Turing-machine executor in the style of busycoq's `es` tactic.

It replays the upstream proof of Sk1like_TC_v1.v Module TM1 (busycoq, ccz181078, 2026-03-11)
case by case: every case of RInc_spec and Inc_spec is a finite symbolic run made of
  - ordinary steps on concrete cells,
  - shift-rule crossings of a block x^n (n symbolic), exactly busycoq's shift_rule_R / shift_rule_L
    (a fixed context d of 0..5 cells travels with the head; the one-copy premise is run concretely),
  - for the two recursive digits, one application of the induction hypothesis RInc_spec r at the
    abstract tail toRC r (three outcomes Tp0/Tp1/Tp2 with fresh r', dn).
The same driver runs any table in TM1's frame, so the delta for the twin (D1 = 0RF, F0 = 1LA) is
checked by running both tables on the same symbolic cases and comparing end configurations.

Tape items (each side is a list, nearest-to-head first):
  0 / 1               a concrete cell
  ('P', word, cnt)    a block word^cnt; word is in left-to-right tape order on BOTH sides;
                      cnt is a Lin (symbolic, at least one variable)
  ('L',)              the abstract left context l of RInc_spec (reading it ends the run)
  ('R', name)         an abstract right tail toRC r (reading it in state C = apply the IH)
  ('Z',)              0^inf
Imports nothing outside the standard library.
"""
import itertools

W = (0, 0, 0, 1)                      # Notation w := [0;0;0;1]
ST = 'ABCDEF'

def parse_tm(s):
    tab = {}
    for qi, row in enumerate(s.split('_')):
        for r in (0, 1):
            t = row[3 * r:3 * r + 3]
            tab[(ST[qi], r)] = None if t == '---' else (int(t[0]), t[1], t[2])
    return tab

def flip_str(s):
    return s.translate(str.maketrans('LR', 'RL'))

# ------------------------------------------------------------------ linear counts
class Lin:
    """const + sum(coef * var), coefficients positive ints."""
    __slots__ = ('c', 'v')
    def __init__(self, c=0, v=None):
        self.c = c; self.v = dict(v or {})
        self.v = {k: x for k, x in self.v.items() if x}
    def __add__(self, o):
        if isinstance(o, int): o = Lin(o)
        v = dict(self.v)
        for k, x in o.v.items(): v[k] = v.get(k, 0) + x
        return Lin(self.c + o.c, v)
    __radd__ = __add__
    def __eq__(self, o):
        if isinstance(o, int): o = Lin(o)
        return self.c == o.c and self.v == o.v
    def __hash__(self):
        return hash((self.c, tuple(sorted(self.v.items()))))
    def is_const(self): return not self.v
    def ev(self, env): return self.c + sum(x * env[k] for k, x in self.v.items())
    def __repr__(self):
        parts = [('%s' % k if x == 1 else '%d%s' % (x, k)) for k, x in sorted(self.v.items())]
        if self.c or not parts: parts = ([str(self.c)] if self.c else []) + parts
        return '+'.join(parts) if parts else '0'

def var(name): return Lin(0, {name: 1})

def N_OS(n):
    """busycoq's N_OS on a Lin that is either the literal 0 or 1 + (rest)."""
    if n == Lin(0): return None
    if n.c >= 1: return Lin(n.c - 1, n.v)
    raise ValueError('N_OS undecided on %r' % (n,))

# ------------------------------------------------------------------ digit words of Sk1like_TC_v1.v
RD = {
    'D00101': [0,0,1,0,1], 'D0011': [0,0,1,1], 'D0011001': [0,0,1,1,0,0,1],
    'D001101': [0,0,1,1,0,1], 'D00111': [0,0,1,1,1], 'D00001': [0,0,0,0,1],
    'D001': [0,0,1], 'D01': [0,1],
    'D0011_011001': [0,0,1,1,0,1,1,0,0,1], 'D001111001': [0,0,1,1,1,1,0,0,1],
    'D00101001': [0,0,1,0,1,0,0,1],
    'D0011_011': [0,0,1,1,0,1,1], 'D001111': [0,0,1,1,1,1],
    'D00011': [0,0,0,1,1],
    'D0011_01101': [0,0,1,1,0,1,1,0,1], 'D00111101': [0,0,1,1,1,1,0,1], 'D0010101': [0,0,1,0,1,0,1],
    'D0011_0111': [0,0,1,1,0,1,1,1], 'D0011111': [0,0,1,1,1,1,1], 'D001011': [0,0,1,0,1,1],
    'D0011_000101': [0,0,1,1,0,0,0,1,0,1], 'D0011_00101': [0,0,1,1,0,0,1,0,1],
    'D0011_0101': [0,0,1,1,0,1,0,1], 'D0011101': [0,0,1,1,1,0,1],
    'D0000101': [0,0,0,0,1,0,1],
}
RDN = list(RD)     # declaration order of the Coq Inductive RD

# An RC value: list of (digit, Lin) then a tail: ('O',) = RC_O D001T, or ('A', name) abstract.
def rc(*digits, tail):
    return (tuple(digits), tail)

class IHCall(Exception):
    pass

def RInc(x, ih, twin=False):
    """Transcription of Fixpoint RInc (dep is irrelevant above 0 for the symbolic cases).
    twin=True: the twin's map RIncF (the exit digit is D0011001, D01 returns Tp3, D00111 accepts Tp3).
    ih(name) -> (r', dn, tp) gives the outcome of the recursive call on an abstract tail.
    Returns ('inl', x', dn, tp) or ('inr',)."""
    digs, tail = x
    if not digs:
        if tail == ('O',): return ('inl', ((), ('O',)), Lin(0), 1)
        raise ValueError('RInc on an abstract tail outside a recursive call')
    (a, n), rest = digs[0], digs[1:]
    r = (rest, tail)
    def S(d, k, rr): return ((d, k),) + rr[0], rr[1]
    def head_of(rr):
        if rr[0]: return rr[0][0][0], rr[0][0][1], (rr[0][1:], rr[1])
        return None
    def rec(rr):
        if rr[0] == () and rr[1][0] == 'A':
            return ih(rr[1][1])
        res = RInc(rr, ih, twin)
        if res[0] == 'inr': return None
        return res[1], res[2], res[3]
    if a == 'D00101':
        m = N_OS(n)
        if m is not None: return ('inl', S('D0011', m, r), Lin(1), 0)
        h = head_of(r)
        if h is None: return ('inr',)
        b, n0, r0 = h
        if b == 'D00101':
            m0 = N_OS(n0)
            if m0 is not None: return ('inl', S('D0011001' if twin else 'D0000101', m0, r0), Lin(1), 1)
            return ('inr',)
        if b == 'D0011001': return ('inl', S('D001', n0, r0), Lin(2), 0)
        if b == 'D001101': return ('inl', S('D01', n0, r0), Lin(2), 0)
        if b == 'D00111': return ('inl', S('D00011', n0, r0), Lin(1), 0)
        return ('inr',)
    if a == 'D0011':
        m = N_OS(n)
        if m is not None: return ('inl', S('D0011001', m, r), Lin(0), 0)
        h = head_of(r)
        if h is None: return ('inr',)
        b, n0, r0 = h
        tbl = {'D01': 'D00111', 'D00101': 'D0011_0101', 'D0011': 'D0011_011',
               'D0011001': 'D0011_011001', 'D001101': 'D0011_01101', 'D00111': 'D0011_0111',
               'D0000101': 'D0011_000101'}
        if b in tbl: return ('inl', S(tbl[b], n0, r0), Lin(0), 0)
        return ('inr',)
    simple = {'D0011001': 'D001101', 'D001101': 'D00111', 'D00001': 'D0011',
              'D0011_011001': 'D001111001', 'D001111001': 'D00101001',
              'D0011_011': 'D001111', 'D001111': 'D00101',
              'D0011_01101': 'D00111101', 'D00111101': 'D0010101',
              'D0011_0111': 'D0011111', 'D0011111': 'D001011',
              'D0011_000101': 'D0011_00101', 'D0011_00101': 'D0011_0101', 'D0011_0101': 'D0011101',
              'D0000101': 'D001101'}
    if a in simple: return ('inl', S(simple[a], n, r), Lin(0), 0)
    if a == 'D00111':
        o = rec(r)
        if o is None: return ('inr',)
        r2, dn, tp = o
        if tp == 0: return ('inl', S('D00101', n + dn, r2), Lin(0), 0)
        if tp == 1: return ('inl', r2, 1 + n + dn, 2)
        if tp == 3: return ('inl', S('D0011001', dn, r2), n, 2)
        m = N_OS(n)
        if m is None: return ('inr',)
        return ('inl', S('D00001', dn, r2), 1 + m, 2)
    if a == 'D001':
        m = N_OS(n)
        if m is None: return ('inr',)
        return ('inl', S('D0011', m, r), Lin(0), 1)
    if a == 'D01':
        m = N_OS(n)
        if m is None: return ('inr',)
        if twin: return ('inl', r, m, 3)
        return ('inl', S('D01', m, r), Lin(0), 2)
    if a == 'D00101001':
        o = rec(r)
        if o is None: return ('inr',)
        r2, dn, tp = o
        if tp == 0: return ('inl', r2, 2 + n + dn, 0)
        return ('inr',)
    if a == 'D00011': return ('inl', r, 1 + n, 0)
    if a == 'D0010101':
        m = N_OS(n)
        if m is None: return ('inr',)
        return ('inl', S('D0011', m, r), Lin(1), 1)
    if a == 'D001011':
        m = N_OS(n)
        if m is None: return ('inr',)
        return ('inl', S('D0011001', m, r), Lin(0), 1)
    if a == 'D0011101':
        m = N_OS(n)
        if m is None: return ('inr',)
        return ('inl', S('D0011001' if twin else 'D0000101', m, r), Lin(0), 2)
    raise ValueError(a)

def Inc(x, ih, twin=False):
    """Definition Inc: x = (n, r).  Returns ('inl', (n', r')) or ('inr',)."""
    n, r = x
    o = ih(r[1][1]) if (r[0] == () and r[1][0] == 'A') else None
    if o is None:
        res = RInc(r, ih, twin)
        if res[0] == 'inr': return ('inr',)
        r2, dn, tp = res[1], res[2], res[3]
    else:
        r2, dn, tp = o
    if tp == 0: return ('inl', (n + dn + 1, r2))
    if tp == 1: return ('inl', (Lin(1), ((('D0011', n + dn),) + r2[0], r2[1])))
    m = N_OS(n)
    if m is None: return ('inr',)
    if tp == 3: return ('inl', (Lin(1), ((('D0011', m), ('D0011001', dn)) + r2[0], r2[1])))
    return ('inl', (Lin(1), ((('D0011', m), ('D00001', dn)) + r2[0], r2[1])))

# ------------------------------------------------------------------ tape construction
def pow_items(word, cnt):
    """word^cnt as items: cnt.c concrete copies, then a block for the symbolic part."""
    out = []
    for _ in range(cnt.c): out += list(word)
    if cnt.v: out.append(('P', tuple(word), Lin(0, cnt.v)))
    return out

def toRC_items(x):
    digs, tail = x
    out = []
    for d, k in digs:
        out += RD[d]
        out += pow_items(W, k)
    if tail == ('O',): out += [0, 0, 1, ('Z',)]
    else: out.append(('R', tail[1]))
    return out

PREFIX = {0: [0], 1: [0, 0, 1], 2: [0, 0, 0, 1], 3: [0, 1, 1, 0, 0, 1]}   # 3: the twin's Tp3
TPSTATE = {0: 'E', 1: 'B', 2: 'B', 3: 'B'}      # state of the head on l after RInc_spec, per Tp

# ------------------------------------------------------------------ canonical form of a side
def canon(items, side='R'):
    """Flatten, merge blocks of the same word, absorb adjacent full copies, drop 0s next to 0^inf.
    Used only to compare end configurations; both machines are compared with the same function."""
    seq = list(items)
    changed = True
    while changed:
        changed = False
        out = []
        for it in seq:
            if isinstance(it, tuple) and it[0] == 'P' and it[2] == Lin(0):
                changed = True; continue
            out.append(it)
        seq = out
        for i, it in enumerate(seq):
            if isinstance(it, tuple) and it[0] == 'P':
                wd = list(it[1]); k = len(wd)
                if side == 'R':
                    pre = seq[max(0, i - k):i]; post = seq[i + 1:i + 1 + k]
                else:   # left side is nearest-first: tape order reversed
                    pre = seq[i + 1:i + 1 + k][::-1]; post = seq[max(0, i - k):i][::-1]
                if pre == wd:
                    if side == 'R': seq = seq[:i - k] + [('P', it[1], it[2] + 1)] + seq[i + 1:]
                    else: seq = seq[:i] + [('P', it[1], it[2] + 1)] + seq[i + 1 + k:]
                    changed = True; break
                if post == wd:
                    if side == 'R': seq = seq[:i] + [('P', it[1], it[2] + 1)] + seq[i + 1 + k:]
                    else: seq = seq[:i - k] + [('P', it[1], it[2] + 1)] + seq[i + 1:]
                    changed = True; break
                if i + 1 < len(seq) and isinstance(seq[i + 1], tuple) and seq[i + 1][0] == 'P' \
                        and seq[i + 1][1] == it[1]:
                    seq = seq[:i] + [('P', it[1], it[2] + seq[i + 1][2])] + seq[i + 2:]
                    changed = True; break
        if not changed and seq and seq[-1] == ('Z',) and len(seq) >= 2 and seq[-2] == 0:
            seq = seq[:-2] + [('Z',)]; changed = True
    return seq

def rotate_side(items, side='R'):
    """busycoq simpl_rotate (lpow_rotate, lpow_rotate_const0), applied eagerly: a block whose
    nearest-first word starts with a, followed (away from the head) by the cell a, becomes
    a followed by the rotated block; a block whose nearest-first word starts with 0 before 0^inf
    likewise.  Returns a new list."""
    seq = list(items)
    changed = True
    while changed:
        changed = False
        for i in range(len(seq) - 1):
            it = seq[i]
            if isinstance(it, tuple) and it[0] == 'P':
                nf = list(it[1]) if side == 'R' else list(it[1])[::-1]
                nxt = seq[i + 1]
                if (isinstance(nxt, int) and nxt == nf[0]) or (nxt == ('Z',) and nf[0] == 0):
                    rot = nf[1:] + nf[:1]
                    word = tuple(rot) if side == 'R' else tuple(rot[::-1])
                    if nxt == ('Z',):
                        seq = seq[:i] + [nf[0], ('P', word, it[2])] + seq[i + 1:]
                    else:
                        seq = seq[:i] + [nf[0], ('P', word, it[2])] + seq[i + 2:]
                    changed = True
                    break
    return seq

def expand(items, env, side='R'):
    out = []
    for it in items:
        if isinstance(it, int): out.append(it)
        elif it[0] == 'P':
            wd = list(it[1]) if side == 'R' else list(it[1])[::-1]
            out += wd * it[2].ev(env)
        else: out.append(it)
    while len(out) >= 2 and out[-1] == ('Z',) and out[-2] == 0:
        out.pop(-2)
    return out

def same_side(a, b, side='R', grid=4):
    """a == b as tapes for every assignment of the variables in {0..grid-1} (exhaustive)."""
    vs = sorted({k for it in list(a) + list(b) if isinstance(it, tuple) and it[0] == 'P' for k in it[2].v})
    for vals in itertools.product(range(grid), repeat=len(vs)):
        env = dict(zip(vs, vals))
        if expand(a, env, side) != expand(b, env, side):
            return False
    return True

def fmt(items, side='R'):
    s = []
    for it in items:
        if isinstance(it, int): s.append(str(it))
        elif it[0] == 'P': s.append('(%s)^%r' % (''.join(map(str, it[1])), it[2]))
        elif it[0] == 'Z': s.append('0^inf')
        elif it[0] == 'L': s.append('l')
        elif it[0] == 'R': s.append('toRC(%s)' % it[1])
    if side == 'L': s = s[::-1]
    return ' '.join(s)

# ------------------------------------------------------------------ the executor
class Stuck(Exception):
    pass

class Run:
    def __init__(self, tab, state, left, right, ih=None, goal=None, maxsteps=100000):
        self.tab = tab; self.q = state; self.L = list(left); self.R = list(right)
        self.ih = ih or {}; self.goal = goal; self.maxsteps = maxsteps
        self.steps = Lin(0)        # number of TM steps, symbolic
        self.trans = []            # concrete transitions used, in order: (q, read)
        self.shift = []            # shift rules used: (dir, state, word, d, word')
        self.ihused = []
        self.end = None

    def step_concrete(self):
        rd = self.R[0]
        t = self.tab[(self.q, rd)]
        if t is None: raise Stuck('halt on %s%d' % (self.q, rd))
        wr, d, nq = t
        self.trans.append((self.q, rd))
        self.steps = self.steps + 1
        self.R[0] = wr
        self.q = nq
        if d == 'R':
            self.L.insert(0, self.R.pop(0))
            if not self.R: raise Stuck('ran off the right side')
        else:
            self.move_left()

    def move_left(self):
        it = self.L.pop(0)
        if isinstance(it, int):
            self.R.insert(0, it)
        elif it == ('Z',):
            self.L.insert(0, ('Z',)); self.R.insert(0, 0)
        elif it == ('L',):
            self.end = ('L', self.q, list(self.R)); self.L.insert(0, it)
        elif it[0] == 'P':
            self.shift_left(it)
        else:
            raise Stuck('bad left item %r' % (it,))

    def shift_left(self, blk):
        """head on the last cell of blk = x^n (left side), state q, d = next k right cells."""
        x = list(blk[1])
        for k in range(0, 6):
            d = self.R[:k]
            if len(d) < k or not all(isinstance(c, int) for c in d): break
            span = x + d
            pos = len(x) - 1; q = self.q; n = 0; ok = False; used = []
            while 0 <= pos < len(span) and n < 1000:
                t = self.tab[(q, span[pos])]
                if t is None: break
                used.append((q, span[pos]))
                span[pos] = t[0]; q = t[2]; pos += 1 if t[1] == 'R' else -1; n += 1
                if pos == -1: ok = True; break
            if ok and q == self.q and span[:k] == d:
                xp = tuple(span[k:])
                self.shift.append(('L', self.q, tuple(x), tuple(d), xp, tuple(used)))
                self.steps = self.steps + Lin(0, {k2: n * c for k2, c in blk[2].v.items()})
                self.R = d + [('P', xp, blk[2])] + self.R[k:]
                self.move_left()
                return
        raise Stuck('no left shift rule for state %s over %r' % (self.q, blk))

    def shift_right(self):
        blk = self.R[0]
        x = list(blk[1])
        for k in range(0, 6):
            d = self.L[:k][::-1]           # tape order
            if len(d) < k or not all(isinstance(c, int) for c in d): break
            span = d + x
            pos = k; q = self.q; n = 0; ok = False; used = []
            while 0 <= pos < len(span) and n < 1000:
                t = self.tab[(q, span[pos])]
                if t is None: break
                used.append((q, span[pos]))
                span[pos] = t[0]; q = t[2]; pos += 1 if t[1] == 'R' else -1; n += 1
                if pos == len(span): ok = True; break
            if ok and q == self.q and span[len(x):] == d:
                xp = tuple(span[:len(x)])
                self.shift.append(('R', self.q, tuple(x), tuple(d), xp, tuple(used)))
                self.steps = self.steps + Lin(0, {k2: n * c for k2, c in blk[2].v.items()})
                self.L = d[::-1] + [('P', xp, blk[2])] + self.L[k:]
                self.R.pop(0)
                return
        raise Stuck('no right shift rule for state %s over %r' % (self.q, blk))

    def at_goal(self):
        if self.goal is None: return False
        gq, gL, gR = self.goal
        if self.q != gq: return False
        if not same_side(self.L, gL, 'L', grid=2): return False
        if not same_side(self.R, gR, 'R', grid=2): return False
        return same_side(self.L, gL, 'L') and same_side(self.R, gR, 'R')

    def run(self):
        while self.end is None:
            if self.steps != Lin(0) and self.at_goal():
                self.end = ('goal', self.q, list(self.R)); break
            if self.steps.c > self.maxsteps: raise Stuck('step cap')
            self.R = rotate_side(self.R, 'R'); self.L = rotate_side(self.L, 'L')
            h = self.R[0]
            if isinstance(h, int):
                self.step_concrete()
            elif h == ('Z',):
                self.R.insert(0, 0)
            elif h[0] == 'P':
                self.shift_right()
            elif h[0] == 'R':
                if self.q != 'C' or h[1] not in self.ih:
                    raise Stuck('reached abstract tail %s in state %s' % (h[1], self.q))
                tp, r2, dn = self.ih.pop(h[1])
                self.ihused.append((h[1], tp))
                st = TPSTATE[tp]
                self.R = PREFIX[tp] + pow_items(W, dn) + [('R', r2)]
                self.q = st
                self.move_left()
            else:
                raise Stuck('bad right item %r' % (h,))
        return self

# ------------------------------------------------------------------ case enumeration
def rinc_cases(twin=False):
    """Every symbolic case of Lemma RInc_spec (the proof's case split), as
    (label, x, ih) where ih maps abstract tail names to (tp, r', dn) for the recursive digits."""
    cases = []
    c = var('c'); n = var('n'); n0 = var('n0'); c0 = var('c0')
    absr = ('A', 'r')
    cases.append(('RC_O D001T', ((), ('O',)), {}))
    nos = {'D00101', 'D0011', 'D001', 'D01', 'D0010101', 'D001011', 'D0011101'}
    for a in RDN:
        if a in ('D00111', 'D00101001'):
            for tp in ((0, 1, 2, 3) if twin else (0, 1, 2)):
                ih = {'r': (tp, "r'", var('dn'))}
                if a == 'D00111' and tp == 2:
                    for nn, lab in ((Lin(0), '0'), (1 + c, '1+c')):
                        cases.append(('%s n=%s | IH Tp%d' % (a, lab, tp), (((a, nn),), absr), dict(ih)))
                else:
                    cases.append(('%s n | IH Tp%d' % (a, tp), (((a, n),), absr), dict(ih)))
            continue
        if a not in nos:
            cases.append(('%s n' % a, (((a, n),), absr), {}))
            continue
        cases.append(('%s n=1+c' % a, (((a, 1 + c),), absr), {}))
        if a in ('D00101', 'D0011'):
            for b in RDN:
                if a == 'D00101' and b == 'D00101':
                    for nn, lab in ((Lin(0), '0'), (1 + c0, '1+c0')):
                        cases.append(('%s n=0, r=%s n0=%s' % (a, b, lab), (((a, Lin(0)), (b, nn)), absr), {}))
                else:
                    cases.append(('%s n=0, r=%s n0' % (a, b), (((a, Lin(0)), (b, n0)), absr), {}))
            cases.append(('%s n=0, r=RC_O D001T' % a, (((a, Lin(0)),), ('O',)), {}))
        else:
            cases.append(('%s n=0' % a, (((a, Lin(0)),), absr), {}))
    return cases

def inc_cases(twin=False):
    n = var('n'); c = var('c')
    out = []
    for tp in ((0, 1, 2, 3) if twin else (0, 1, 2)):
        ih = {'r': (tp, "r'", var('dn'))}
        if tp >= 2:
            out.append(('Inc | IH Tp%d, n=0' % tp, (Lin(0), ((), ('A', 'r'))), ih))
            out.append(('Inc | IH Tp%d, n=1+c' % tp, (1 + c, ((), ('A', 'r'))), dict(ih)))
        else:
            out.append(('Inc | IH Tp%d' % tp, (n, ((), ('A', 'r'))), ih))
    return out

def ih_fn(ih):
    def f(name):
        tp, r2, dn = ih[name]
        return ((), ('A', r2)), dn, tp
    return f

def run_rinc_case(tab, x, ih, twin=False):
    """Returns (status, run, expected) where status in {'skip','ok','mismatch','stuck'}."""
    res = RInc(x, ih_fn(ih), twin)
    if res[0] == 'inr':
        return 'skip', None, None
    x2, dn, tp = res[1], res[2], res[3]
    st = TPSTATE[tp]
    exp = (st, PREFIX[tp] + pow_items(W, dn) + toRC_items(x2))
    run = Run(tab, 'C', [('L',)], toRC_items(x), ih=dict(ih))
    try:
        run.run()
    except Stuck as e:
        return 'stuck: %s' % e, run, exp
    kind, q, R = run.end
    ok = kind == 'L' and q == exp[0] and same_side(R, exp[1]) and not run.ih
    return ('ok' if ok else 'mismatch'), run, exp

def run_inc_case(tab, x, ih, twin=False):
    res = Inc(x, ih_fn(ih), twin)
    if res[0] == 'inr':
        return 'skip', None, None
    n2, r2 = res[1]
    goal = ('C', [('Z',)], pow_items(W, n2) + toRC_items(r2))
    run = Run(tab, 'C', [('Z',)], pow_items(W, x[0]) + toRC_items(x[1]), ih=dict(ih), goal=goal)
    try:
        run.run()
    except Stuck as e:
        return 'stuck: %s' % e, run, goal
    ok = run.end[0] == 'goal' and not run.ih
    return ('ok' if ok else 'mismatch'), run, goal

# ------------------------------------------------------------------ concrete abstract iteration
# The RC value as a stack: st[-1] is the first digit; st[0] is the tail marker 'T' (RC_O D001T)
# or 'X' (an abstract tail that must never be read).  twin=True gives the twin's map (RIncF).
SIMPLE = {'D0011001': 'D001101', 'D001101': 'D00111', 'D00001': 'D0011',
          'D0011_011001': 'D001111001', 'D001111001': 'D00101001',
          'D0011_011': 'D001111', 'D001111': 'D00101',
          'D0011_01101': 'D00111101', 'D00111101': 'D0010101',
          'D0011_0111': 'D0011111', 'D0011111': 'D001011',
          'D0011_000101': 'D0011_00101', 'D0011_00101': 'D0011_0101', 'D0011_0101': 'D0011101',
          'D0000101': 'D001101'}
D0011_NEXT = {'D01': 'D00111', 'D00101': 'D0011_0101', 'D0011': 'D0011_011',
              'D0011001': 'D0011_011001', 'D001101': 'D0011_01101', 'D00111': 'D0011_0111',
              'D0000101': 'D0011_000101'}

class Inr(Exception):
    pass

class TouchedTail(Exception):
    pass

def rinc_c(st, twin, stats=None, depth=0):
    """Concrete Fixpoint RInc (twin=False) or the twin's RIncF (twin=True), on a stack.
    Mutates st into x'; returns (dn, tp).  Raises Inr for inr, TouchedTail if the abstract tail is read."""
    if depth > 1000: raise Inr('maxD')
    top = st[-1]
    if top == 'X': raise TouchedTail()
    if top == 'T':
        if stats is not None: stats['D001T'] = stats.get('D001T', 0) + 1
        return 0, 1
    a, n = top
    def nxt():
        if len(st) < 2 or st[-2] == 'X': raise TouchedTail()
        return st[-2]
    if stats is not None:
        stats[a] = stats.get(a, 0) + 1
    if a == 'D00101':
        if n > 0:
            st[-1] = ('D0011', n - 1); return 1, 0
        b = nxt()
        if b == 'T': raise Inr(a)
        b, n0 = b
        if b == 'D00101':
            if n0 == 0: raise Inr(a)
            st.pop(); st[-1] = ('D0011001' if twin else 'D0000101', n0 - 1)
            if stats is not None: stats['EXIT:D00101.D00101'] = stats.get('EXIT:D00101.D00101', 0) + 1
            return 1, 1
        if b == 'D0011001': st.pop(); st[-1] = ('D001', n0); return 2, 0
        if b == 'D001101': st.pop(); st[-1] = ('D01', n0); return 2, 0
        if b == 'D00111': st.pop(); st[-1] = ('D00011', n0); return 1, 0
        raise Inr(a + '.' + b)
    if a == 'D0011':
        if n > 0:
            st[-1] = ('D0011001', n - 1); return 0, 0
        b = nxt()
        if b == 'T': raise Inr(a)
        b, n0 = b
        if b in D0011_NEXT:
            st.pop(); st[-1] = (D0011_NEXT[b], n0); return 0, 0
        raise Inr(a + '.' + b)
    if a in SIMPLE:
        st[-1] = (SIMPLE[a], n); return 0, 0
    if a == 'D00111':
        st.pop()
        dn, tp = rinc_c(st, twin, stats, depth + 1)
        if tp == 0: st.append(('D00101', n + dn)); return 0, 0
        if tp == 1: return 1 + n + dn, 2
        if tp == 2:
            if n == 0: raise Inr('D00111.Tp2.n0')
            st.append(('D00001', dn)); return n, 2
        # tp == 3 (twin only)
        if stats is not None: stats['D00111<-Tp3'] = stats.get('D00111<-Tp3', 0) + 1
        st.append(('D0011001', dn)); return n, 2
    if a == 'D001':
        if n == 0: raise Inr(a)
        st[-1] = ('D0011', n - 1); return 0, 1
    if a == 'D01':
        if n == 0: raise Inr(a)
        if stats is not None: stats['EXIT:D01'] = stats.get('EXIT:D01', 0) + 1
        if twin:
            st.pop(); return n - 1, 3
        st[-1] = ('D01', n - 1); return 0, 2
    if a == 'D00101001':
        st.pop()
        dn, tp = rinc_c(st, twin, stats, depth + 1)
        if tp == 0: return 2 + n + dn, 0
        raise Inr('D00101001.Tp%d' % tp)
    if a == 'D00011':
        st.pop(); return 1 + n, 0
    if a == 'D0010101':
        if n == 0: raise Inr(a)
        st[-1] = ('D0011', n - 1); return 1, 1
    if a == 'D001011':
        if n == 0: raise Inr(a)
        st[-1] = ('D0011001', n - 1); return 0, 1
    if a == 'D0011101':
        if n == 0: raise Inr(a)
        if stats is not None: stats['EXIT:D0011101'] = stats.get('EXIT:D0011101', 0) + 1
        st[-1] = ('D0011001' if twin else 'D0000101', n - 1); return 0, 2
    raise ValueError(a)

def inc_c(x, twin, stats=None):
    """Concrete Definition Inc (or the twin's IncF).  x = [n, st]; mutates; raises Inr."""
    n, st = x
    dn, tp = rinc_c(st, twin, stats)
    if tp == 0:
        x[0] = n + dn + 1
    elif tp == 1:
        st.append(('D0011', n + dn)); x[0] = 1
    elif tp == 2:
        if n == 0: raise Inr('Inc.Tp2.n0')
        st.append(('D00001', dn)); st.append(('D0011', n - 1)); x[0] = 1
    else:
        if n == 0: raise Inr('Inc.Tp3.n0')
        if stats is not None: stats['Inc<-Tp3'] = stats.get('Inc<-Tp3', 0) + 1
        st.append(('D0011001', dn)); st.append(('D0011', n - 1)); x[0] = 1

def x0_c():
    return [1, ['T', ('D0011', 5), ('D0011', 14)]]

def fmt_c(x, k=8):
    n, st = x
    return '(%d, %s)' % (n, ' '.join('%s %d' % d if isinstance(d, tuple) else d for d in st[::-1][:k]))