localRule

proof body

Definition body.

  71  match n.left, n.center, n.right with
  72  -- Signal propagation: Signal moves right
  73  | _, .Signal, .Wire => .Signal
  74  | _, .Signal, .Blank => .Signal
  75  -- Wire carries signal
  76  | .Signal, .Wire, _ => .Signal
  77  | .Signal, .Blank, _ => .Blank  -- Signal consumed
  78  -- AND gate: both inputs must be One
  79  | .One, .Gate, .One => .One
  80  | .One, .Gate, .Zero => .Zero
  81  | .Zero, .Gate, .One => .Zero
  82  | .Zero, .Gate, .Zero => .Zero
  83  -- OR gate: either input is One
  84  | .One, .Wire, .One => .One
  85  | .One, .Wire, .Zero => .One
  86  | .Zero, .Wire, .One => .One
  87  | .Zero, .Wire, .Zero => .Zero
  88  -- NOT gate: invert center when activated
  89  | .Signal, .Zero, _ => .One
  90  | .Signal, .One, _ => .Zero
  91  -- Default: preserve state
  92  | _, c, _ => c
  93
  94/-- Apply local rule globally to create successor tape -/