MM2 Example: Counter Machine

Monotonic rewriting system version of https://en.wikipedia.org/wiki/Counter_machine#Program

Run in MORK/kernel with cargo run --release -- run resources/counter_machine_5.mm2

or for a fixed number of extra steps (e.g. 0 running just one step) cargo run --release -- run resources/counter_machine_5.mm2 --steps 0

; The following program is encoded in S-expressions or the metagraph
; Function: it copies the contents of register 2 to register 3
; 0   1   2   3   4   5   6   7   8   9
; JZ  DEC INC INC JZ  JZ  DEC INC JZ  H  ; instruction
; 2   2   3   1   0   1   1   2   0      ; register it checks
; 5               0   9           5      ; jump to instruction number
(program Z (JZ 2 (S (S (S (S (S Z))))) ))
(program (S Z) (DEC 2))
(program (S (S Z)) (INC 3))
(program (S (S (S Z))) (INC 1))
(program (S (S (S (S Z)))) (JZ 0 Z))
(program (S (S (S (S (S Z))))) (JZ 1 (S (S (S (S (S (S (S (S (S Z)))))))))))
(program (S (S (S (S (S (S Z)))))) (DEC 1))
(program (S (S (S (S (S (S (S Z))))))) (INC 2))
(program (S (S (S (S (S (S (S (S Z)))))))) (JZ 0 (S (S (S (S (S Z)))))))
(program (S (S (S (S (S (S (S (S (S Z))))))))) H)
; Initial state of the registers
; 0 1 2 3 4  ; register
; 0 0 5 0 0  ; contents
(state Z (REG 0 Z))
(state Z (REG 1 Z))
(state Z (REG 2 (S (S (S (S (S Z)))))))  ; so we want to copy the number 5 from here
(state Z (REG 3 Z))  ; to here (currently 0)
(state Z (REG 4 Z))
; Set the instruction counter to 0
(state Z (IC Z))
; (if <peano_nonzero> <then> <else> <result>) -- ignore the highlighting, it's not built-in
(if (S $n) $x $y $x)
(if Z $x $y $y)
; Get all other registers (can be done via grounding, written out here)
(0 != 1) (0 != 2) (0 != 3) (0 != 4)
(1 != 0) (1 != 2) (1 != 3) (1 != 4)
(2 != 1) (2 != 0) (2 != 3) (2 != 4)
(3 != 1) (3 != 2) (3 != 0) (3 != 4)
(4 != 1) (4 != 2) (4 != 0) (4 != 3)

; These are the three rules "(state k <previous_state>) => (state <k+1> <next_state>)" that evolve the system

; Update instruction counter to $j if $r is zero (keep the rest the same)
((step JZ $ts)
; for the current IC, maybe get the JZ instruction, get the register it checks, calculate next IC, and get all other state
  (, (state $ts (IC $i)) (program $i (JZ $r $j)) (state $ts (REG $r $v)) (if $v (S $i) $j $ni) (state $ts (REG $k $kv)))
; set the next calculate IC, and and keep all registers the same
  (, (state (S $ts) (IC $ni)) (state (S $ts) (REG $k $kv))))

; Increment register $r (keep the rest the same)
((step INC $ts)
; for the current IC, maybe get the INC instruction, get the register, and all other, registers
  (, (state $ts (IC $i)) (program $i (INC $r)) (state $ts (REG $r $v)) ($r != $o) (state $ts (REG $o $ov)))
; set the next IC (just incremented), the calculated new register value, and keep all other registers
  (, (state (S $ts) (IC (S $i))) (state (S $ts) (REG $r (S $v))) (state (S $ts) (REG $o $ov))))

; Decrement register $r (keep the rest the same), analogous to INC
((step DEC $ts)
  (, (state $ts (IC $i)) (program $i (DEC $r)) (state $ts (REG $r (S $v))) ($r != $o) (state $ts (REG $o $ov)))
  (, (state (S $ts) (IC (S $i))) (state (S $ts) (REG $r $v)) (state (S $ts) (REG $o $ov))))  

; Halt, no progression to the next state
((step HALT $ts)
; for the current IC, maybe get the H instruction
  (, (state $ts (IC $i)) (program $i H))
; set the global halted property with the final state's clock
  (, (HALTED $ts)))

; Run the counter machine, increment the clock every cycle, keeping all previous states
; Only scheduling the next batch of steps for execution when there's a next timestep state (not the case with halt)
(exec (clocked Z)  ; start clock at 0
        (, (exec (clocked $ts) $p1 $t1)       ; given our current executing rewrite rule (reflective!)
           (state $ts (IC $_))                ; when there is some state to continue on (not halted)
           ((step $k $ts) $p0 $t0))           ; get the rewrite rule for each of the counter machine cases
        (, (exec ($k $ts) $p0 $t0)            ; schedule the case rewrite rule
           (exec (clocked (S $ts)) $p1 $t1))) ; schedule our rewrite rule again (for execution after the steps)

Full program output

; v  Yeeey we halted!  v
(HALTED (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))))))))))))
((step JZ $a) (, (state $a (IC $b)) (program $b (JZ $c $d)) (state $a (REG $c $e)) (if $e (S $b) $d $f) (state $a (REG $g $h))) (, (state (S $a) (IC $f)) (state (S $a) (REG $g $h))))
((step DEC $a) (, (state $a (IC $b)) (program $b (DEC $c)) (state $a (REG $c (S $d))) ($c != $e) (state $a (REG $e $f))) (, (state (S $a) (IC (S $b))) (state (S $a) (REG $c $d)) (state (S $a) (REG $e $f))))
((step INC $a) (, (state $a (IC $b)) (program $b (INC $c)) (state $a (REG $c $d)) ($c != $e) (state $a (REG $e $f))) (, (state (S $a) (IC (S $b))) (state (S $a) (REG $c (S $d))) (state (S $a) (REG $e $f))))
((step HALT $a) (, (state $a (IC $b)) (program $b H)) (, (HALTED $a)))
(0 != 1)
(0 != 2)
(0 != 3)
(0 != 4)
(1 != 0)
(1 != 2)
(1 != 3)
(1 != 4)
(2 != 0)
(2 != 1)
(2 != 3)
(2 != 4)
(3 != 0)
(3 != 1)
(3 != 2)
(3 != 4)
(4 != 0)
(4 != 1)
(4 != 2)
(4 != 3)
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))))))))))) (IC (S (S (S (S (S (S (S (S (S Z)))))))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))))))))))) (REG 1 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))))))))))) (REG 2 (S (S (S (S (S Z)))))))
; v  Yeeey, our final state has 5 in register 3, the copying we wanted to do!  v
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))))))))))) (REG 3 (S (S (S (S (S Z)))))))
; ^  success  ^
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))))))))))) (IC (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))))))))))) (REG 1 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))))))))))) (REG 2 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))))))))))) (REG 3 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))))))))) (IC (S (S (S (S (S (S (S (S Z))))))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))))))))) (REG 1 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))))))))) (REG 2 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))))))))) (REG 3 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))))))))) (IC (S (S (S (S (S (S (S Z)))))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))))))))) (REG 1 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))))))))) (REG 2 (S (S (S (S Z))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))))))))) (REG 3 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))))))) (IC (S (S (S (S (S (S Z))))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))))))) (REG 1 (S Z)))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))))))) (REG 2 (S (S (S (S Z))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))))))) (REG 3 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))))))) (IC (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))))))) (REG 1 (S Z)))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))))))) (REG 2 (S (S (S (S Z))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))))))) (REG 3 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))))) (IC (S (S (S (S (S (S (S (S Z))))))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))))) (REG 1 (S Z)))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))))) (REG 2 (S (S (S (S Z))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))))) (REG 3 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))))) (IC (S (S (S (S (S (S (S Z)))))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))))) (REG 1 (S Z)))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))))) (REG 2 (S (S (S Z)))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))))) (REG 3 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))) (IC (S (S (S (S (S (S Z))))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))) (REG 1 (S (S Z))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))) (REG 2 (S (S (S Z)))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))) (REG 3 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))) (IC (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))) (REG 1 (S (S Z))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))) (REG 2 (S (S (S Z)))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))) (REG 3 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))) (IC (S (S (S (S (S (S (S (S Z))))))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))) (REG 1 (S (S Z))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))) (REG 2 (S (S (S Z)))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))) (REG 3 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))) (IC (S (S (S (S (S (S (S Z)))))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))) (REG 1 (S (S Z))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))) (REG 2 (S (S Z))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))) (REG 3 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))) (IC (S (S (S (S (S (S Z))))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))) (REG 1 (S (S (S Z)))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))) (REG 2 (S (S Z))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))) (REG 3 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))) (IC (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))) (REG 1 (S (S (S Z)))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))) (REG 2 (S (S Z))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))) (REG 3 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))) (IC (S (S (S (S (S (S (S (S Z))))))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))) (REG 1 (S (S (S Z)))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))) (REG 2 (S (S Z))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))) (REG 3 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))) (IC (S (S (S (S (S (S (S Z)))))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))) (REG 1 (S (S (S Z)))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))) (REG 2 (S Z)))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))) (REG 3 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))) (IC (S (S (S (S (S (S Z))))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))) (REG 1 (S (S (S (S Z))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))) (REG 2 (S Z)))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))) (REG 3 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))) (IC (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))) (REG 1 (S (S (S (S Z))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))) (REG 2 (S Z)))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))) (REG 3 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))) (IC (S (S (S (S (S (S (S (S Z))))))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))) (REG 1 (S (S (S (S Z))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))) (REG 2 (S Z)))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))) (REG 3 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))) (IC (S (S (S (S (S (S (S Z)))))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))) (REG 1 (S (S (S (S Z))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))) (REG 2 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))) (REG 3 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))) (IC (S (S (S (S (S (S Z))))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))) (REG 1 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))) (REG 2 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))) (REG 3 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))) (IC (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))) (REG 1 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))) (REG 2 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))) (REG 3 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))) (IC Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))) (REG 1 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))) (REG 2 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))) (REG 3 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))) (IC (S (S (S (S Z))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))) (REG 1 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))) (REG 2 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))) (REG 3 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))) (IC (S (S (S Z)))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))) (REG 1 (S (S (S (S Z))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))) (REG 2 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))) (REG 3 (S (S (S (S (S Z)))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))) (IC (S (S Z))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))) (REG 1 (S (S (S (S Z))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))) (REG 2 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))) (REG 3 (S (S (S (S Z))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))) (IC (S Z)))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))) (REG 1 (S (S (S (S Z))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))) (REG 2 (S Z)))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))) (REG 3 (S (S (S (S Z))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))) (IC Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))) (REG 1 (S (S (S (S Z))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))) (REG 2 (S Z)))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))) (REG 3 (S (S (S (S Z))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))) (IC (S (S (S (S Z))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))) (REG 1 (S (S (S (S Z))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))) (REG 2 (S Z)))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))) (REG 3 (S (S (S (S Z))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))) (IC (S (S (S Z)))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))) (REG 1 (S (S (S Z)))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))) (REG 2 (S Z)))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))) (REG 3 (S (S (S (S Z))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))) (IC (S (S Z))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))) (REG 1 (S (S (S Z)))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))) (REG 2 (S Z)))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))) (REG 3 (S (S (S Z)))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))) (IC (S Z)))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))) (REG 1 (S (S (S Z)))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))) (REG 2 (S (S Z))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))) (REG 3 (S (S (S Z)))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))) (IC Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))) (REG 1 (S (S (S Z)))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))) (REG 2 (S (S Z))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))) (REG 3 (S (S (S Z)))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))) (IC (S (S (S (S Z))))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))) (REG 1 (S (S (S Z)))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))) (REG 2 (S (S Z))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))) (REG 3 (S (S (S Z)))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))) (IC (S (S (S Z)))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))) (REG 1 (S (S Z))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))) (REG 2 (S (S Z))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))) (REG 3 (S (S (S Z)))))
(state (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) (IC (S (S Z))))
(state (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) (REG 1 (S (S Z))))
(state (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) (REG 2 (S (S Z))))
(state (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) (REG 3 (S (S Z))))
(state (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S (S Z))))))))))) (IC (S Z)))
(state (S (S (S (S (S (S (S (S (S (S (S Z))))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S (S Z))))))))))) (REG 1 (S (S Z))))
(state (S (S (S (S (S (S (S (S (S (S (S Z))))))))))) (REG 2 (S (S (S Z)))))
(state (S (S (S (S (S (S (S (S (S (S (S Z))))))))))) (REG 3 (S (S Z))))
(state (S (S (S (S (S (S (S (S (S (S (S Z))))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S (S Z)))))))))) (IC Z))
(state (S (S (S (S (S (S (S (S (S (S Z)))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S (S Z)))))))))) (REG 1 (S (S Z))))
(state (S (S (S (S (S (S (S (S (S (S Z)))))))))) (REG 2 (S (S (S Z)))))
(state (S (S (S (S (S (S (S (S (S (S Z)))))))))) (REG 3 (S (S Z))))
(state (S (S (S (S (S (S (S (S (S (S Z)))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S (S Z))))))))) (IC (S (S (S (S Z))))))
(state (S (S (S (S (S (S (S (S (S Z))))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S (S Z))))))))) (REG 1 (S (S Z))))
(state (S (S (S (S (S (S (S (S (S Z))))))))) (REG 2 (S (S (S Z)))))
(state (S (S (S (S (S (S (S (S (S Z))))))))) (REG 3 (S (S Z))))
(state (S (S (S (S (S (S (S (S (S Z))))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S (S Z)))))))) (IC (S (S (S Z)))))
(state (S (S (S (S (S (S (S (S Z)))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S (S Z)))))))) (REG 1 (S Z)))
(state (S (S (S (S (S (S (S (S Z)))))))) (REG 2 (S (S (S Z)))))
(state (S (S (S (S (S (S (S (S Z)))))))) (REG 3 (S (S Z))))
(state (S (S (S (S (S (S (S (S Z)))))))) (REG 4 Z))
(state (S (S (S (S (S (S (S Z))))))) (IC (S (S Z))))
(state (S (S (S (S (S (S (S Z))))))) (REG 0 Z))
(state (S (S (S (S (S (S (S Z))))))) (REG 1 (S Z)))
(state (S (S (S (S (S (S (S Z))))))) (REG 2 (S (S (S Z)))))
(state (S (S (S (S (S (S (S Z))))))) (REG 3 (S Z)))
(state (S (S (S (S (S (S (S Z))))))) (REG 4 Z))
(state (S (S (S (S (S (S Z)))))) (IC (S Z)))
(state (S (S (S (S (S (S Z)))))) (REG 0 Z))
(state (S (S (S (S (S (S Z)))))) (REG 1 (S Z)))
(state (S (S (S (S (S (S Z)))))) (REG 2 (S (S (S (S Z))))))
(state (S (S (S (S (S (S Z)))))) (REG 3 (S Z)))
(state (S (S (S (S (S (S Z)))))) (REG 4 Z))
(state (S (S (S (S (S Z))))) (IC Z))
(state (S (S (S (S (S Z))))) (REG 0 Z))
(state (S (S (S (S (S Z))))) (REG 1 (S Z)))
(state (S (S (S (S (S Z))))) (REG 2 (S (S (S (S Z))))))
(state (S (S (S (S (S Z))))) (REG 3 (S Z)))
(state (S (S (S (S (S Z))))) (REG 4 Z))
(state (S (S (S (S Z)))) (IC (S (S (S (S Z))))))
(state (S (S (S (S Z)))) (REG 0 Z))
(state (S (S (S (S Z)))) (REG 1 (S Z)))
(state (S (S (S (S Z)))) (REG 2 (S (S (S (S Z))))))
(state (S (S (S (S Z)))) (REG 3 (S Z)))
(state (S (S (S (S Z)))) (REG 4 Z))
(state (S (S (S Z))) (IC (S (S (S Z)))))
(state (S (S (S Z))) (REG 0 Z))
(state (S (S (S Z))) (REG 1 Z))
(state (S (S (S Z))) (REG 2 (S (S (S (S Z))))))
(state (S (S (S Z))) (REG 3 (S Z)))
(state (S (S (S Z))) (REG 4 Z))
(state (S (S Z)) (IC (S (S Z))))
(state (S (S Z)) (REG 0 Z))
(state (S (S Z)) (REG 1 Z))
(state (S (S Z)) (REG 2 (S (S (S (S Z))))))
(state (S (S Z)) (REG 3 Z))
(state (S (S Z)) (REG 4 Z))
(state (S Z) (IC (S Z)))
(state (S Z) (REG 0 Z))
(state (S Z) (REG 1 Z))
(state (S Z) (REG 2 (S (S (S (S (S Z)))))))
(state (S Z) (REG 3 Z))
(state (S Z) (REG 4 Z))
(state Z (IC Z))
(state Z (REG 0 Z))
(state Z (REG 1 Z))
(state Z (REG 2 (S (S (S (S (S Z)))))))
(state Z (REG 3 Z))
(state Z (REG 4 Z))
(program (S (S (S (S (S (S (S (S (S Z))))))))) H)
(program (S (S (S (S (S (S (S (S Z)))))))) (JZ 0 (S (S (S (S (S Z)))))))
(program (S (S (S (S (S (S (S Z))))))) (INC 2))
(program (S (S (S (S (S (S Z)))))) (DEC 1))
(program (S (S (S (S (S Z))))) (JZ 1 (S (S (S (S (S (S (S (S (S Z)))))))))))
(program (S (S (S (S Z)))) (JZ 0 Z))
(program (S (S (S Z))) (INC 1))
(program (S (S Z)) (INC 3))
(program (S Z) (DEC 2))
(program Z (JZ 2 (S (S (S (S (S Z)))))))
(if (S $a) $b $c $b)
(if Z $a $b $b)