Examine individual changes

'= Proof sketch (mostly computational) = For context, see [[BitChanger Busy beaver]] and [[BitChanger]]. * enumerate programs of the given size * perform minimal static analysis to detect some loops that, once entered, never exit, and can thus be replaced by <code>[]</code> * execute programs for a bounded number of steps * perform cycle detection based on a repeated context (covering all cells inspected, and the whole tape in whatever direction the tape head moved in) * for size 14 a few holdouts remain that can be checked manually. == Size 14 holdouts == The three holdouts evolve into repeating patterns: <pre> }}<[}<}}<[<]}] }}<: 1*1 -- * indicates the tape head, so we have ... 0 0 1 to the left, 1 as the current cell, and 0 0 0 ... to the right [}<}}<: 11*1 [<]}]: 1*111 -- ! [}<}}<: 11*01 [<]}]: 111*1 [}<}}<: 1111*1 [<]}]: 1*11111 -- ! [}<}}<: 11*0111 [<]}]: 111*111 [}<}}<: 1111*01 [<]}]: 11111*1 [}<}}<: 111111*1 [<]}]: 1*1111111 -- ! ETC. </pre> <pre> }<[}}<[<<]}}<] }<: *1 [}}<[<<]: *001 -- ! }}<]: 1*11 [}}<[<<]: 10*0 }}<]: 101*1 [}}<[<<]: *0010101 -- ! }}<]: 1*110101 [}}<[<<]: 10*00101 }}<]: 101*1101 [}}<[<<]: 1010*001 }}<]: 10101*11 [}}<[<<]: 101010*0 }}<]: 1010101*1 [}}<[<<]: *00101010101 -- ! ETC. </pre> <pre> }<[}[<<]}}}<<] }<: *1 [}[<<]: *0 }}}<<]: 1*11 [}[<<]: *00101 -- ! }}}<<]: 1*1001 [}[<<]: 10*001 }}}<<]: 101*1 [}[<<]: 1010*0 }}}<<]: 10101*11 [}[<<]: *001010101 -- ! }}}<<]: 1*10010101 [}[<<]: 10*0010101 }}}<<]: 101*100101 [}[<<]: 1010*00101 }}}<<]: 10101*1001 [}[<<]: 101010*001 }}}<<]: 1010101*1 [}[<<]: 10101010*0 }}}<<]: 101010101*11 [}[<<]: *0010101010101 -- ! ETC. </pre> == Using Timbuk == One can use [https://people.irisa.fr/Thomas.Genet/timbuk/ Timbuk 3.2] to verify non-termination. For example, <code>}<[}[<<]}}}<<]</code> can be encoded as follows: <pre> Ops L:0 L0:1 L1:1 R:0 R0:1 R1:1 F:0 a:2 b:2 c:2 d:2 e:2 f:2 g:2 h:2 i:2 j:2 k:2 l:2 m:2 n:2 o:2 Vars x y TRS P L -> L0(L) R -> R0(R) a(x,R0(y)) -> b(L1(x),y) % } a(x,R1(y)) -> b(L0(x),y) % } b(L0(x),y) -> c(x,R0(y)) % < b(L1(x),y) -> c(x,R1(y)) % < c(x,R0(y)) -> o(x,R0(y)) % [ c(x,R1(y)) -> d(x,R1(y)) % [ d(x,R0(y)) -> e(L1(x),y) % } d(x,R1(y)) -> e(L0(x),y) % } e(x,R0(y)) -> i(x,R0(y)) % [ e(x,R1(y)) -> f(x,R1(y)) % [ f(L0(x),y) -> g(x,R0(y)) % < f(L1(x),y) -> g(x,R1(y)) % < g(L0(x),y) -> h(x,R0(y)) % < g(L1(x),y) -> h(x,R1(y)) % < h(x,R0(y)) -> i(x,R0(y)) % ] h(x,R1(y)) -> f(x,R1(y)) % ] i(x,R0(y)) -> j(L1(x),y) % } i(x,R1(y)) -> j(L0(x),y) % } j(x,R0(y)) -> k(L1(x),y) % } j(x,R1(y)) -> k(L0(x),y) % } k(x,R0(y)) -> l(L1(x),y) % } k(x,R1(y)) -> l(L0(x),y) % } l(L0(x),y) -> m(x,R0(y)) % < l(L1(x),y) -> m(x,R1(y)) % < m(L0(x),y) -> n(x,R0(y)) % < m(L1(x),y) -> n(x,R1(y)) % < n(x,R0(y)) -> o(x,R0(y)) % ] n(x,R1(y)) -> d(x,R1(y)) % ] o(x,y) -> F Set I a(L,R) Patterns F Equations Approx Rules % 42 steps L0(L1(L0(L1(x)))) = L0(L1(x)) R0(R1(R0(x))) = R0(x) </pre> And <code>timbuk 42 <file></code> will report <code>Proof done!</code>. Any larger number instead of 42 will also work. In this encoding, the left part of the tape is represented as a stack using <code>L</code> for the end of the stack, <code>L0</code> for 0, and <code>L1</code> for 1. The right part uses <code>R</code>, <code>R0</code>, and <code>R1</code> analogously, and includes the current cell. Note that the first two rules allow the tape to be expanded to both sides. Each program position becomes a state that's represented as a binary function symbol with left stack and right stack as arguments. The <code>F</code> symbol captures program termination. Using automata techniques, Timbuk can check that we cannot reach the (forbidden) pattern <code>F</code> from the initial state <code>a(L,R)</code>. The final section specifies approximations that help Timbuk construct a finite automaton; in this example they encode that a sequence <code>1010</code> to the left can be collapsed to <code>10</code> and the sequence <code>010</code> to the right can be collapsed to <code>0</code>. === Size 14 holdouts === We only list the approximation rules; the transition rules can be generated automatically. %%% }}<[}<}}<[<]}] (23 steps) L1(L1(L1(x))) = L1(x) R1(R1(R1(x))) = R1(x) %%% }<[}[<<]}}}<<] (42 steps) L0(L1(L0(L1(x)))) = L0(L1(x)) R0(R1(R0(x))) = R0(x) %%% }<[}}<[<<]}}<] (45 steps) L0(L1(L0(x))) = L0(x) R0(R1(R0(x))) = R0(x) === Size 15 holdouts === %%% }}<[}[<<]}}}<<] (38 steps) L1(L0(x)) = x R0(R1(R0(x))) = R0(x) %%% }}<[}}<[<<]}}<] (34 steps) L0(L1(L0(x))) = L0(x) R0(R1(R0(x))) = R0(x) %%% }<[[}}]<[<<]}}] (29 steps) L0(L) = L L0(L1(L)) = L L1(L1(x)) = x R1(R0(R1(x))) = R1(x) R1(R1(R1(x))) = R1(x) %%% }<[[<<]}}[}}]<] (28 steps) L0(L) = L L0(L1(L)) = L L1(L1(x)) = x R1(R0(R1(x))) = R1(x) R1(R1(R1(x))) = R1(x) %%% }<[[<<]}<[}}]<] (30 steps) L1(L0(L1(x))) = L1(x) R1(R0(R1(x))) = R1(x) %%% }<[[}}<[<]<]}}] (35 steps) L1(L1(x)) = x R1(R1(R1(x))) = R1(x) %%% }<[[[<]}}<}}]<] (30 steps) L1(L1(x)) = x R1(R1(R1(x))) = R1(x) %%% }<[[[<<]}}}}]<] (131 steps) L1(L1(L1(L1(x)))) = L1(L1(x)) R1(R1(R1(x))) = R1(x) %%% }<[}}<[[<]<]}}] (40 steps) L0(L) = L L1(L1(L0(L1(x)))) = L1(x) R1(R1(R0(x))) = x === Size 16 holdouts === %%% }}}}<[}<}}<[<]}] (25 steps) %%% }}<[[}}<<]}[<]}] (28 steps) %%% }}<[[}<}}<[<]]}] (25 steps) %%% }}<[[}<}}<[<]}]] (24 steps) %%% }}<[}<[]}}<[<]}] (25 steps) %%% }}<[}}<<[]}[<]}] (27 steps) %%% }}<[}<}}<[<][]}] (24 steps) %%% }}<[}<}}<[[<]]}] (24 steps) %%% }<[[<]}[}<}]}}<] (38 steps) %%% }<[[}<}]}<[<<]}] (33 steps) %%% }<[[}<}]}}<[<]}] (35 steps) %%% }<[[[<]}}]<}}}<] (40 steps) %%% }<[[<[<<]}}]<}<] (56 steps) %%% }<[[<[<]}}<}}]<] (29 steps) L1(L1(L1(x))) = L1(x) R1(R1(R1(x))) = R1(x) %%% }}<<[}[<<]}}}<<] (47 steps) %%% }<[[}}<[<<]]}}<] (53 steps) %%% }<[[}}<[<<]}}<]] (46 steps) %%% }<[}[<[]<]}}}<<] (42 steps) %%% }<[}}<[<<][]}}<] (48 steps) %%% }<[}}<[<<<<]}}<] (47 steps) %%% }<[}}<[[<]<]}}<] (50 steps) %%% }<[}}<[[<<]]}}<] (48 steps) %%% }<[}}<[<[]<]}}<] (47 steps) L0(L1(L0(x))) = L0(x) R0(R1(R0(x))) = R0(x) %%% }<[[}[<<]]}}}<<] (52 steps) %%% }<[[}[<<]}}}<<]] (46 steps) %%% }<[}[<<][]}}}<<] (48 steps) %%% }<[}[<<<<]}}}<<] (55 steps) %%% }<[}[[<]<]}}}<<] (54 steps) %%% }<[}[[<<]]}}}<<] (48 steps) %%% }<[}}[]<[<<]}}<] (34 steps) L1(L0(L1(L0(x)))) = L1(L0(x)) R0(R1(R0(x))) = R0(x) %%% }<[[}[<<]}}}]<<] (52 steps) %%% }<[}[<<]}}}[]<<] (48 steps) L1(L0(L1(L0(x)))) = L1(L0(x)) R1(R0(R1(R0(x)))) = R1(R0(x)) %%% }}<[<[}[<<}]}]<] (45 steps) %%% }<[[}}]<[<<]}}<] (47 steps) L0(L1(L0(x))) = L0(x) R1(R0(R1(R0(x)))) = R1(R0(x)) %%% }}<[[}}]<[<<]}}] (23 steps) %%% }}<[[<<]}}[}}]<] (29 steps) L0(L) = L L1(L1(L1(x))) = L1(x) L1(L0(L0(L1(x)))) = L1(L1(x)) L0(L1(L0(x))) = L0(x) R1(R0(R1(x))) = R1(x) R1(R1(R1(x))) = R1(x) %%% }<[[<<}]}[}]}}<] (51 steps) L0(L0(L0(x))) = L0(x) R1(R1(R1(x))) = R1(x) %%% }}<[[}<]}}<[<]}] (26 steps) L1(L1(L1(L))) = L1(L) R1(R1(R1(R))) = R1(R) %%% }}<[[<<]}<[}}]<] (60 steps) L1(L0(L1(x))) = L1(x) R1(R0(R1(x))) = R1(x) %%% }<[}}<[<[<]<]}}] (46 steps) L0(L1(L1(L0(x)))) = L0(x) R0(R1(R1(R0(x)))) = R0(x) %%% }<[[<]}<[}<}]<<] (46 steps) L1(L1(L1(x))) = L1(L1(x)) R1(R1(R1(x))) = R1(R1(x)) %%% }}<<[}}<[<<]}}<] (46 steps) L0(L1(L0(L1(x)))) = L0(L1(x)) R0(R1(R0(R1(x)))) = R0(R1(x)) %%% }<[}}<[<<]}[<]}] (80 steps) L1(L1(L1(x))) = L1(x) R1(R1(R1(R1(x)))) = R1(R1(x)) %%% }<[<}<[[}<}]}]<] (44 steps) L1(L1(L1(x))) = L1(x) R1(R0(R1(R0(x)))) = R1(R0(x)) %%% }}<[[[<<]}}}}]<] (83 steps) L1(L1(L1(L1(L1(x))))) = L1(L1(L1(x))) R1(R1(R1(R1(x)))) = R1(R1(x)) %%% }<[}[<<<]}}}}<<] (70 steps) L1(L1(L0(L0(L1(L0(L1(L1(L)))))))) = L1(L1(L)) R0(R1(R0(R0(R1(R1(R0(R1(R)))))))) = R0(R1(R)) %%% }}<[[<}<<]}[}]}] (60 steps) L0(L0(L0(x))) = L0(x) L0(L1(L0(L1(x)))) = L0(L1(x)) R1(R1(R1(x))) = R1(x) %%% }<[[<]}<[<}}]<<] (27 steps) L1(L1(L1(x))) = L1(L1(x)) R0(R) = R R1(R1(x)) = R1(x) %%% }<[<<[<]}[}]}<}] (48 steps) L0(L0(x)) = L0(x) L1(L0(L1(x))) = L1(x) L1(L1(L1(x))) = L1(L1(x)) R1(R1(R1(x))) = R1(R1(x)) %%% }<[}}<[<<<]}}}<] (59 steps) L1(L1(L0(L1(L1(L))))) = L1(L1(L)) L0(L1(L0(L1(L1(L))))) = L1(L1(L)) R0(R1(R1(R0(R1(R))))) = R0(R1(R)) R0(R1(R0(R0(R1(R))))) = R0(R1(R)) %%% }<[}}}<[<<<]}}<] (60 steps) L0(L1(L1(L0(L1(L))))) = L0(L1(L)) L0(L1(L0(L0(L1(L))))) = L0(L1(L)) R1(R1(R0(R1(R1(R))))) = R1(R1(R)) R0(R1(R0(R1(R1(R))))) = R1(R1(R)) == Haskell Code == <pre> -- Find small BitChanger busy beavers -- -- - candidates are normalized (using only one version of equivalent sequences of <,}) -- - initialization is minimal -- - no trailing moves after final loop -- -- Note that we miss candidates obtained by padding with < at the front. -- For example, the size 15 candidate with 252 steps, }<[}}<[<<<}]}}, -- can be padded to a size 16 candidate with 253 steps, >}<[}}<[<<<}]}}, -- but the size 16 calculation omits it. import Control.Monad import qualified Data.Array as A import qualified Data.Map as M import Data.Bits import Data.Word import Data.List -- convention 1: ] branches -- convention 2: ] jumps to matching [, incurring an extra step convention = 1 ref | convention == 1 = zip [0..] [0,1,2,3,4,5,8,11,14,17,22,27,36,45,58,252,101] | convention == 2 = zip [0..] [0,1,2,3,4,6,10,14,18,22,26,35,47,59,71,295,123] -- programs data I = L | R | B !Int | E !Int type P = A.Array Int I instance Show I where showsPrec _ L = ('<':) showsPrec _ R = ('}':) showsPrec _ B{} = ('[':) showsPrec _ E{} = (']':) showList = foldr (.) id . map shows -- generate normalized programs of given length prog :: Int -> [P] prog n = map (\p -> A.listArray (0,n-1) p) $ replicate n R : loopy n where -- minimal left excursion, returns to origin le n | odd n = [] | n == 0 = [[]] | n == 2 = [[L,R]] | n == 4 = [[L,L,R,R]] | otherwise = [[L] ++ p ++ [R] | p <- le (n-2)] ++ [[L] ++ p ++ [R,L,R] | p <- le (n-4)] -- minimal right excursion, returns to origin re n = reverse <$> le n -- minimal-ish initialization ini n | n < 2 = [] | otherwise = [p ++ [R] ++ q ++ [L] | i <- [0,2..n-2], p <- jini (n-2-i), q <- re i] ++ [[R] ++ p ++ [L] ++ q ++ [L,R,L] ++ r | i <- [0,2..n-6], j <- [0,2..n-6-i], p <- re i, q <- ll (n-5-i-j), r <- le j] jini 0 = [[]] jini n = (R:) <$> rr (n-1) -- loopy program: initialization, then non-empty loops loopy n | n < 5 = [] | otherwise = [p ++ [B (j+2)] ++ q ++ [E j] ++ r | j <- [1..n-4], k <- [0..n-4-j], p <- ini (n-2-j-k), q <- body j, r <- loopy' k] loopy' n | n < 4 = [[] | n == 0] | otherwise = [p ++ [B (j+2)] ++ q ++ [E j] ++ r | j <- [1..n-3], k <- [1..n-3-j], p <- move (n-2-j-k), q <- body j, r <- loopy' k] rr n | n <= 2 = [replicate n R] | otherwise = ((++ [R]) <$> rr (n-1)) ++ ((++ [R,L,R]) <$> rr (n-3)) ll n | n <= 2 = [replicate n L] | otherwise = ((++ [L]) <$> ll (n-1)) ++ ((++ [L,R,L]) <$> ll (n-3)) -- minimal code consisting just of < and } move n = [p ++ q ++ r | i <- [0,2..n], j <- [0,2..n-i], p <- le i, q <- rr (n-i-j), r <- re j] ++ [p ++ q ++ r | i <- [0,2..n-1], j <- [0,2..n-1-i], p <- re i, q <- ll (n-i-j), r <- le j] -- loop body body n = move n ++ [p ++ [B (j+2)] ++ q ++ [E j] ++ r | i <- [0..n-2], j <- [0..n-2-i], p <- move i, q <- body j, r <- body (n-2-i-j)] ++ [[L,R,L,R] ++ p | n >= 4, p <- body (n-4)] -- cell values (False = 0, True = 1) type V = Bool -- program stack for loops, position, tape type S = (P, Int, Int, Int, [V], V, [V]) -- initial state s0 :: P -> S s0 p = (p, 0, 0, 0, [], False, []) -- single step step :: S -> Maybe S step (p, i, _, _, _, _, _) | not (A.inRange (A.bounds p) i) = Nothing step (p, i, c, o, l, x, r) = Just $ case (p A.! i, l, x, r) of (L, [], x, r) | !o <- o-1 -> (p, i+1, c+1, o, [], False, cons x r) (L, y:l, x, r) | !o <- o-1 -> (p, i+1, c+1, o, l, y, cons x r) (R, l, x, []) | !o <- o+1, !x <- not x -> (p, i+1, c+1, o, cons x l, False, []) (R, l, x, y:r) | !o <- o+1, !x <- not x -> (p, i+1, c+1, o, cons x l, y, r) (B d, l, True, r) -> (p, i+1, c+1, o, l, x, r) (B d, l, False, r) -> (p, i+d, c+1, o, l, x, r) (E d, l, True, r) -> (p, i-d, c+convention, o, l, x, r) (E d, l, False, r) -> (p, i+1, c+convention, o, l, x, r) -- helper: always compress all-0 list to [] cons False [] = [] cons x xs = x:xs -- execution: run up to 32 steps, return number of steps if it -- terminates, -1 if non-termination is detected; pass on to `run1` otherwise run0 p = go (s0 p) where go s@(_,_,i,_,_,_,_) | i >= 32 = run1 64 s | Just s <- step s = go s | otherwise = i -- execution: run up to 2^16 steps, trying harder to detect non-termination: -- we keep track of a previously seen state, and how much context the -- program looked at since seeing that state; the program loops if the -- program state and context repeats, and furthermore, if the tape head -- moved, the tape looks the same in the direction we moved in. run1 l (p, ip0, i, _, l0, x0, r0) | l > 2^16 = i | l > 2^10 && window p ip0 l0 x0 r0 = -1 | otherwise = go 0 0 (p, ip0, i, 0, l0, x0, r0) -- reset position to 0 where go ol oh s@(_,_,i,_,_,_,_) | i >= l = run1 (2*l) s | Just s@(_, _, _, o, _, _, _) <- step s , !ol <- min o ol , !oh <- max o oh = go' ol oh s | otherwise = i go' ol oh s@(_, ip, i, o, l, x, r) | ip0 /= ip || -- different state x /= x0 || -- different current cell take (-ol) l /= take (-ol) l0 || -- different left context take oh r /= take oh r0 -- different right context = go ol oh s | o == 0 -- position unchanged = -1 | o < 0, l == l0 -- moved left = -1 | o > 0, r == r0 -- moved right = -1 | otherwise = go ol oh s -- Static non-termination check based on moving window: -- For each program location, compute whether we can see a 0-bit or a 1-bit -- for ~30 positions around the current position. when moving, unknown bits -- (allowing either 0 or 1 bits) are shifted in at the end of the window. type M = M.Map Int (Word64, Word64) window :: P -> Int -> [V] -> V -> [V] -> Bool window p ip l x r = go m0 M.! sz == (0,0) where sz = A.rangeSize (A.bounds p) m0 :: M m0 = M.fromList $ [(i, (0,0)) | i <- [0..sz]] ++ [(ip, (k, complement k))] k = foldl' (\n x -> n*2 + val x) 0 (reverse (take 31 l) ++ [x] ++ take 32 (r ++ repeat False)) val False = 0 val True = 1 (a,b) .||. (c,d) = (a .|. c, b .|. d) propagate :: M -> M propagate m = foldl' (flip (uncurry (M.insertWith (.||.)))) m $ do (i, b) <- A.assocs p let (t, f) = m M.! i case p A.! i of L -> [(i+1, (bit 63 .|. (t `shiftR` 1), bit 63 .|. (f `shiftR` 1)))] R | (t, f) <- (clearBit t 32 .|. (bit 32 .&. f), clearBit f 32 .|. (bit 32 .&. t)) -> [(i+1, (bit 0 .|. (t `shiftL` 1), bit 0 .|. (f `shiftL` 1)))] B d -> [(i+1, (t, clearBit f 32)) | testBit t 32] ++ [(i+d, (clearBit t 32, f)) | testBit f 32] E d -> [(i-d, (t, clearBit f 32)) | testBit t 32] ++ [(i+1, (clearBit t 32, f)) | testBit f 32] go m | m' <- propagate m = if m == m' then m else go m' main = forM_ ref $ \(n, m) -> do putStrLn $ unwords ["---", show n, "---"] mapM_ print $ do p <- prog n let s = run0 p [(A.elems p, s) | s >= m] </pre> == Output (convention 1) == Convention 1 treats <code>]</code> as a single step that either exits the loop or jumps past the corresponding <code>[</code>. Note that the size 15 champion can be padded to obtain a 253 step size 16 champion; the fact that the program misses it is by design. <pre> --- 0 --- (,0) --- 1 --- (},1) --- 2 --- (}},2) --- 3 --- (}}},3) --- 4 --- (}}}},4) --- 5 --- (}}}}},5) (}<[}],5) (}<[<],5) --- 6 --- (}}<[<],8) --- 7 --- (}}}<[<],11) --- 8 --- (}}}}<[<],14) --- 9 --- (}}}}}<[<],17) (}}}<[}<<],17) --- 10 --- (}}}}<[}<<],22) (}}<[<<<}}],22) --- 11 --- (}}}}}<[}<<],27) (}}}<[[<]}}],27) --- 12 --- (}}}}<[[<]}}],36) --- 13 --- (}}}}}<[[<]}}],45) --- 14 --- (}}<[}<}}<[<]}],65536) (}<[}[<<]}}}<<],65536) (}<[}}<[<<]}}<],65536) (}<[}}<<<[<]}}],58) --- 15 --- (}}<[}[<<]}}}<<],65536) (}}<[}}<[<<]}}<],65536) (}<[[}}]<[<<]}}],65536) (}<[[<<]}}[}}]<],65536) (}<[[<<]}<[}}]<],65536) (}<[[}}<[<]<]}}],65536) (}<[[[<]}}<}}]<],65536) (}<[[[<<]}}}}]<],65536) (}<[}}<[<<<}]}}],252) (}<[}}<[[<]<]}}],65536) --- 16 --- (}}}}<[}<}}<[<]}],65536) (}}<<[}[<<]}}}<<],65536) (}}<<[}}<[<<]}}<],65536) (}}<[[}}]<[<<]}}],65536) (}}<[[}<]}}<[<]}],65536) (}}<[[<<]}}[}}]<],65536) (}}<[[<<]}<[}}]<],65536) (}}<[[}}<<]}[<]}],65536) (}}<[[<}<<]}[}]}],65536) (}}<[[[<<]}}}}]<],65536) (}}<[[}<}}<[<]]}],65536) (}}<[[}<}}<[<]}]],65536) (}}<[<[}[<<}]}]<],65536) (}}<[}<[]}}<[<]}],65536) (}}<[}}<<[]}[<]}],65536) (}}<[}<}}<[<][]}],65536) (}}<[}<}}<[[<]]}],65536) (}<[[<]}[}<}]}}<],65536) (}<[[<]}<[}<}]<<],65536) (}<[[<]}<[<}}]<<],65536) (}<[[}}]<[<<]}}<],65536) (}<[[}<}]}<[<<]}],65536) (}<[[}<}]}}<[<]}],65536) (}<[[<<}]}[}]}}<],65536) (}<[[[<]}}]<}}}<],65536) (}<[[}[<<]]}}}<<],65536) (}<[[<[<<]}}]<}<],65536) (}<[[}}<[<<]]}}<],65536) (}<[[}[<<]}}}]<<],65536) (}<[[<[<]}}<}}]<],65536) (}<[[<[<<]}}}}]<],101) (}<[[}[<<]}}}<<]],65536) (}<[[}}<[<<]}}<]],65536) (}<[}[<<][]}}}<<],65536) (}<[}[<<]}}}[]<<],65536) (}<[}[<<<]}}}}<<],65536) (}<[}[<<<<]}}}<<],65536) (}<[}[[<]<]}}}<<],65536) (}<[}[[<<]]}}}<<],65536) (}<[}[<[]<]}}}<<],65536) (}<[}}[]<[<<]}}<],65536) (}<[<<[<]}[}]}<}],65536) (}<[}}<[<<][]}}<],65536) (}<[}}<[<<]}[<]}],65536) (}<[}}<[<<<]}}}<],65536) (}<[}}<[<<<<]}}<],65536) (}<[}}<[[<]<]}}<],65536) (}<[}}<[[<<]]}}<],65536) (}<[}}<[<[]<]}}<],65536) (}<[}}<[<[<]<]}}],65536) (}<[<}<[[}<}]}]<],65536) (}<[}}}<[<<<]}}<],65536) </pre> == Output (convention 2, champions only) == Convention 2 treats <code>]</code> as a single step that jumps to the corresponding <code>[</code> (which then is counted as another step). <pre> --- 0 --- (,0) --- 1 --- (},1) --- 2 --- (}},2) --- 3 --- (}}},3) --- 4 --- (}}}},4) --- 5 --- (}<[}],6) (}<[<],6) --- 6 --- (}}<[<],10) --- 7 --- (}}}<[<],14) --- 8 --- (}}}}<[<],18) --- 9 --- (}}}}}<[<],22) --- 10 --- (}}}}}}<[<],26) (}}}}<[}<<],26) --- 11 --- (}}}<[[<]}}],35) --- 12 --- (}}}}<[[<]}}],47) --- 13 --- (}}}}}<[[<]}}],59) --- 14 --- (}}}}}}<[[<]}}],71) --- 15 --- (}<[}}<[<<<}]}}],295) --- 16 --- (}<[[<[<<]}}}}]<],123) (not a bug, see previous section) </pre> == Using AProVE == for more complicated programs, it is better to use [https://aprove.informatik.rwth-aachen.de/index.php/interface/v-AProVE2023/trs_wst AProVE]. it can prove complicated programs for length 17. The encoding is very simmilar; except instead of L0 and R0 we have V0, L1 and R1 we have V1, L and R become e for end of stack. letters for program position become P0 P1 P2... the bitchanger program <code>}<[<[<<]}}[}]<}<]</code> first becomes <code> [<[<<]}(})<*]</code> where <code>()</code> are do while loops, and <code>*</code> is toggle current bit. then we convert that code to this term rewriting system: <pre> (VAR X Y) (TERM P0(e,V1(e))) (RULES P0(X,V0(Y)) -> P13(X,V0(Y)) P0(X,V1(Y)) -> P1(X,V1(Y)) P0(e,Y) -> P0(V0(e),Y) P0(X,e) -> P0(X,V0(e)) P1(V0(X),Y) -> P2(X,V0(Y)) P1(V1(X),Y) -> P2(X,V1(Y)) P1(e,Y) -> P1(V0(e),Y) P1(X,e) -> P1(X,V0(e)) P2(X,V0(Y)) -> P6(X,V0(Y)) P2(X,V1(Y)) -> P3(X,V1(Y)) P2(e,Y) -> P2(V0(e),Y) P2(X,e) -> P2(X,V0(e)) P3(V0(X),Y) -> P4(X,V0(Y)) P3(V1(X),Y) -> P4(X,V1(Y)) P3(e,Y) -> P3(V0(e),Y) P3(X,e) -> P3(X,V0(e)) P4(V0(X),Y) -> P5(X,V0(Y)) P4(V1(X),Y) -> P5(X,V1(Y)) P4(e,Y) -> P4(V0(e),Y) P4(X,e) -> P4(X,V0(e)) P5(X,V0(Y)) -> P6(X,V0(Y)) P5(X,V1(Y)) -> P2(X,V1(Y)) P5(e,Y) -> P5(V0(e),Y) P5(X,e) -> P5(X,V0(e)) P6(X,V0(Y)) -> P7(V1(X),Y) P6(X,V1(Y)) -> P7(V0(X),Y) P6(e,Y) -> P6(V0(e),Y) P6(X,e) -> P6(X,V0(e)) P7(X,Y) -> P8(X,Y) P7(e,Y) -> P7(V0(e),Y) P7(X,e) -> P7(X,V0(e)) P8(X,V0(Y)) -> P9(V1(X),Y) P8(X,V1(Y)) -> P9(V0(X),Y) P8(e,Y) -> P8(V0(e),Y) P8(X,e) -> P8(X,V0(e)) P9(X,V0(Y)) -> P7(X,V0(Y)) P9(X,V1(Y)) -> P7(X,V1(Y)) P9(e,Y) -> P9(V0(e),Y) P9(X,e) -> P9(X,V0(e)) P10(V0(X),Y) -> P11(X,V0(Y)) P10(V1(X),Y) -> P11(X,V1(Y)) P10(e,Y) -> P10(V0(e),Y) P10(X,e) -> P10(X,V0(e)) P11(X,V0(Y)) -> P12(X,V1(Y)) P11(X,V1(Y)) -> P12(X,V0(Y)) P11(e,Y) -> P11(V0(e),Y) P11(X,e) -> P11(X,V0(e)) P12(X,V0(Y)) -> F P12(X,V1(Y)) -> P0(X,V1(Y)) P12(e,Y) -> P12(V0(e),Y) P12(X,e) -> P12(X,V0(e)) ) </pre> then AProVE disproves termination. == Progress towards BB(17) == This is the output of [[User:Int-e|Int-e]]'s halskell Program for length 17: for convention 2: <pre> (}<<<}<[}<}}<[<]}],65536) (}}}<<[}[<<]}}}<<],65536) (}}}<<[}}<[<<]}}<],65536) (}}}<[[}}]<[<<]}}],65537) (}}}<[[<<]}}[}}]<],65537) (}}}<[[<<]}<[}}]<],65536) (}}}<[[<}<<]}[}]}],65537) (}}}<[[}}<[<]<]}}],65536) (}}}<[[[<]}}<}}]<],65536) (}}}<[[[<<]}}}}]<],65536) (}}}<[<[}<}]}<<<}],65536) (}}}<[}}<[[<]<]}}],65536) (}}<<[<}<[}<}]}<<],65536) (}}<[[}]}<[<}<]}}],65537) (}}<[[}]}}<[<<}]}],65536) (}}<[[<]}[}<}]}}<],65536) (}}<[[<]}[}<}]<<<],65537) (}}<[[<]}<[}<}]<<],65537) (}}<[[<]}<[<}}]<<],65536) (}}<[[}}]<[<<]}}<],65536) (}}<[[}}]}<[<<}]<],65537) (}}<[[}<}]}}<[<]}],65537) (}}<[[<}<<]}[}}]}],65536) (}}<[[[<]}}]<}}}<],65536) (}}<[[[<]}}]<}<<<],65537) (}}<[[}[<<]]}}}<<],65536) (}}<[[<[<<]}}]<}<],65537) (}}<[[}}<[<<]]}}<],65537) (}}<[[}[<<]}}}]<<],65536) (}}<[[}<}}<[<]}]}],65537) (}}<[[}[<<]}}}<<]],65536) (}}<[[}}<[<<]}}<]],65537) (}}<[}[<<][]}}}<<],65536) (}}<[}[<<]}}}[]<<],65536) (}}<[}[<<<]}}}}<<],65536) (}}<[<[<}}]<<[<]}],65536) (}}<[}[<<<<]}}}<<],65536) (}}<[}[[<]<]}}}<<],65536) (}}<[}[[<<]]}}}<<],65536) (}}<[}[<[]<]}}}<<],65536) (}}<[<[[<]}}]<}<<],65536) (}}<[<[[}<}]}]<<}],65537) (}}<[<[}[<<]<]}}}],65536) (}}<[<[[[<]}}]}]<],65536) (}}<[}}[]<[<<]}}<],65536) (}}<[}}[<]<[<<]}}],65536) (}}<[}<[}]}}<[<]}],65536) (}}<[}<[<]}}<[<]}],65536) (}}<[}}<[<<][]}}<],65536) (}}<[}}<[<<<]}}}<],65536) (}}<[}}<[<<<<]}}<],65537) (}}<[}}<[[<]<]}}<],65536) (}}<[}}<[[<<]]}}<],65536) (}}<[}}<[<[]<]}}<],65536) (}}<[}}<<[}]}[<]}],65536) (}}<[}}<<[<]}[<]}],65536) (}}<[<}<<[<]}[}]}],65536) (}}<[}}}<[<<<]}}<],65536) (}}<[}}}<[[<]<<]}],65536) (}}<[}<}}<[<][}]}],65536) (}}<[}<}}<[<][<]}],65536) (}}<[}<}}<[<[<]]}],65537) (}}<[}<}}}<[<]<}}],65536) (}<[[}]<}<[<}<<]}],65536) (}<[[}]<}<<<[<]}}],65536) (}<[[}]<}<<}[<]}}],65537) (}<[[<]}[}<}]}}}<],65537) (}<[[<]}}[}<}]}}<],65536) (}<[[<]}<[}<}]}}<],65536) (}<[[<]}<[<}}]<<<],65536) (}<[[<]}}}[}]<<}<],65536) (}<[[}}][]<[<<]}}],65536) (}<[[}}]<[<<]}<}}],65536) (}<[[}}]<[<<]<}}}],65536) (}<[[}}]<[<<][]}}],65536) (}<[[}}]<[[<]<]}}],65537) (}<[[}}]<[[<<]]}}],65536) (}<[[}}]<[[<<]}]<],65536) (}<[[}}]<<<[<<]}}],65537) (}<[[}}]}}<[<<}]}],65537) (}<[[}}]}}<[<<}]<],65537) (}<[[<<][]}}[}}]<],65536) (}<[[<<][]}<[}}]<],65536) (}<[[<<]}[]<[}}]<],65536) (}<[[<<]}}[}}]<<<],65536) (}<[[<<]}}[}}][]<],65536) (}<[[<<]}<[}}]<<<],65536) (}<[[<<]}<[}}][]<],65536) (}<[[<<]}}[[}}]]<],65536) (}<[[<<]}<[[}}]]<],65536) (}<[[<<]<}}[}]}<}],65536) (}<[[<<]}}}}[}}]<],65537) (}<[[<<]}<}}[}}]<],65536) (}<[[<<]<}}}[}}]<],65536) (}<[[<<]<}}<[}}]<],65536) (}<[[}<}]<[<<]}}<],65536) (}<[[}<}]}}<[<]}}],65537) (}<[[}<}]}}}<[<]}],65537) (}<[[<}}]<}<[<]}}],65536) (}<[[<<}]}[}}]}}<],65536) (}<[[<<}]<[}}]}}<],65536) (}<[[<<}]}}[}]}}<],65536) (}<[[<<}]}<[}]}}<],65536) (}<[[<}<<]}[}]<}<],65536) (}<[[[<]<]}<[}}]<],65536) (}<[[[}}]]<[<<]}}],65537) (}<[[[<<]]}}[}}]<],65536) (}<[[[<<]]}<[}}]<],65536) (}<[[<[]<]}<[}}]<],65537) (}<[[[<]}}]<}}}}<],65536) (}<[[[<<]}]<[}}]<],65536) (}<[[<[<]}}]<}}}<],65536) (}<[[}}<[<]<][]}}],65536) (}<[[}}<[<]<]}[]}],65536) (}<[[[<]}}<}}]}}<],65536) (}<[[[<]}}<}}][]<],65537) (}<[[[<<]}}}}][]<],65536) (}<[[<}[<]}}}]<}<],65536) (}<[[[}}]<[<<]]}}],65537) (}<[[[}}<[<]]<]}}],65536) (}<[[[}}<[<]<]]}}],65536) (}<[[<[}[<]}]<]}}],65536) (}<[[}}<[<][]<]}}],65536) (}<[[}}<[[<]]<]}}],65536) (}<[[}}<[<[]]<]}}],65536) (}<[[}}<[<<<}]]}}],346) (}<[[}}<[[<]<]]}}],65536) (}<[[[<]}}<}}}<]}],65537) (}<[[[<][]}}<}}]<],65536) (}<[[[<]}[}<]}}]<],65536) (}<[[[<]}}<[]}}]<],65536) (}<[[[<<][]}}}}]<],65536) (}<[[[<<]}}[}}]]<],65536) (}<[[[<<]}<[}}]]<],65536) (}<[[[[<]]}}<}}]<],65537) (}<[[[[<<]]}}}}]<],65536) (}<[[[[<]}}<]}}]<],65536) (}<[[[}}<[<]<]}]}],65536) (}<[[[[<]}}<}}]]<],65536) (}<[[[[<<]}}}}]]<],65537) (}<[[}[<<]}}}<<]}],65536) (}<[[<[<<]}}<}}]<],65536) (}<[[<[<<<]}}}}]<],65536) (}<[[<<[<<]}}}}]<],65536) (}<[[}}<[<<]}}<]}],65537) (}<[[}}<[<<]<}}]}],65536) (}<[[}}<[[<]<]}]}],65536) (}<[[[}}]<[<<]}}]],65536) (}<[[[<<]}}[}}]<]],65537) (}<[[[<<]}<[}}]<]],65536) (}<[[[}}<[<]<]}}]],65537) (}<[[[[<]}}<}}]<]],65536) (}<[[[[<<]}}}}]<]],65536) (}<[[}}<[[<]<]}}]],65536) (}<[}[<]<}<[<<]}}],65536) (}<[<[<]}[}<}]}}<],65536) (}<[<[<]}<[}<}]<<],65537) (}<[<[<]}<[<}}]<<],65537) (}<[}[<<][}]}}}<<],65536) (}<[}[<<][<]}}}<<],65536) (}<[}[<<]}}}[}]<<],65536) (}<[}[<<]}}}[<]<<],65536) (}<[<[<<]}}[}]<}<],65536) (}<[}[}<}]}}<[<]}],65536) (}<[<[<}<]}[}]}}<],65536) (}<[}[<[}]<]}}}<<],65536) (}<[}[<[<]<]}}}<<],65536) (}<[}}[]<[[<]<]}}],65536) (}<[}}[}]<[<<]}}<],65536) (}<[}}[<]<[<<]}}<],65536) (}<[<<[<]}}[}]<}<],65536) (}<[}}[}}]<[<<]}}],65536) (}<[<<[<<]}}[}}]<],65537) (}<[<<[<<]}<[}}]<],65536) (}<[<}[}<}]<[<]}}],65536) (}<[<}[[<]}}}<}]<],65536) (}<[<}[}<}}<[<]}]],65536) (}<[}}<[<<][}]}}<],65536) (}<[}}<[<<][<]}}<],65536) (}<[}}<[<<]}[<<]}],65536) (}<[}}<[[<]<][]}}],65536) (}<[}}<[[<]<]}[]}],65536) (}<[}}<[<[}]<]}}<],65536) (}<[}}<[<[<]<]}}<],65536) (}<[<<}[[}}]}]<<}],65536) (}<[}}<[[<][]<]}}],65536) (}<[}}<[[[<]]<]}}],65536) (}<[}}<[[[<]<]]}}],65537) (}<[<<}<[}]}[}}]<],65536) (}<[<<}<[<]}[}}]<],65536) (}<[<<}<[[}<}]}]<],65536) (}<[}<}}}}<[<]<}<],65536) (}<[<}}<}}<[<]}<}],65536) </pre> and for convention 1: <pre> (}<<<}<[}<}}<[<]}],65536) (}}}<<[}[<<]}}}<<],65536) (}}}<<[}}<[<<]}}<],65536) (}}}<[[}}]<[<<]}}],65536) (}}}<[[<<]}}[}}]<],65536) (}}}<[[<<]}<[}}]<],65536) (}}}<[[<}<<]}[}]}],65536) (}}}<[[}}<[<]<]}}],65536) (}}}<[[[<]}}<}}]<],65536) (}}}<[[[<<]}}}}]<],65536) (}}}<[<[}<}]}<<<}],65536) (}}}<[}}<[[<]<]}}],65536) (}}<<[<}<[}<}]}<<],65536) (}}<[[}]}<[<}<]}}],65536) (}}<[[}]}}<[<<}]}],65536) (}}<[[<]}[}<}]}}<],65536) (}}<[[<]}[}<}]<<<],65536) (}}<[[<]}<[}<}]<<],65536) (}}<[[<]}<[<}}]<<],65536) (}}<[[}}]<[<<]}}<],65536) (}}<[[}}]}<[<<}]<],65536) (}}<[[}<}]}}<[<]}],65536) (}}<[[<}<<]}[}}]}],65536) (}}<[[[<]}}]<}}}<],65536) (}}<[[[<]}}]<}<<<],65536) (}}<[[}[<<]]}}}<<],65536) (}}<[[<[<<]}}]<}<],65536) (}}<[[}}<[<<]]}}<],65536) (}}<[[}[<<]}}}]<<],65536) (}}<[[}<}}<[<]}]}],65536) (}}<[[}[<<]}}}<<]],65536) (}}<[[}}<[<<]}}<]],65536) (}}<[}[<<][]}}}<<],65536) (}}<[}[<<]}}}[]<<],65536) (}}<[}[<<<]}}}}<<],65536) (}}<[<[<}}]<<[<]}],65536) (}}<[}[<<<<]}}}<<],65536) (}}<[}[[<]<]}}}<<],65536) (}}<[}[[<<]]}}}<<],65536) (}}<[}[<[]<]}}}<<],65536) (}}<[<[[<]}}]<}<<],65536) (}}<[<[[}<}]}]<<}],65536) (}}<[<[}[<<]<]}}}],65536) (}}<[<[[[<]}}]}]<],65536) (}}<[}}[]<[<<]}}<],65536) (}}<[}}[<]<[<<]}}],65536) (}}<[}<[}]}}<[<]}],65536) (}}<[}<[<]}}<[<]}],65536) (}}<[}}<[<<][]}}<],65536) (}}<[}}<[<<<]}}}<],65536) (}}<[}}<[<<<<]}}<],65536) (}}<[}}<[[<]<]}}<],65536) (}}<[}}<[[<<]]}}<],65536) (}}<[}}<[<[]<]}}<],65536) (}}<[}}<<[}]}[<]}],65536) (}}<[}}<<[<]}[<]}],65536) (}}<[<}<<[<]}[}]}],65536) (}}<[}}}<[<<<]}}<],65536) (}}<[}}}<[[<]<<]}],65536) (}}<[}<}}<[<][}]}],65536) (}}<[}<}}<[<][<]}],65536) (}}<[}<}}<[<[<]]}],65536) (}}<[}<}}}<[<]<}}],65536) (}<[[}]<}<[<}<<]}],65536) (}<[[}]<}<<<[<]}}],65536) (}<[[}]<}<<}[<]}}],65536) (}<[[<]}[}<}]}}}<],65536) (}<[[<]}}[}<}]}}<],65536) (}<[[<]}<[}<}]}}<],65536) (}<[[<]}<[<}}]<<<],65536) (}<[[<]}}}[}]<<}<],65536) (}<[[}}][]<[<<]}}],65536) (}<[[}}]<[<<]}<}}],65536) (}<[[}}]<[<<]<}}}],65536) (}<[[}}]<[<<][]}}],65536) (}<[[}}]<[[<]<]}}],65536) (}<[[}}]<[[<<]]}}],65536) (}<[[}}]<[[<<]}]<],65536) (}<[[}}]<<<[<<]}}],65536) (}<[[}}]}}<[<<}]}],65536) (}<[[}}]}}<[<<}]<],65536) (}<[[<<][]}}[}}]<],65536) (}<[[<<][]}<[}}]<],65536) (}<[[<<]}[]<[}}]<],65536) (}<[[<<]}}[}}]<<<],65536) (}<[[<<]}}[}}][]<],65536) (}<[[<<]}<[}}]<<<],65536) (}<[[<<]}<[}}][]<],65536) (}<[[<<]}}[[}}]]<],65536) (}<[[<<]}<[[}}]]<],65536) (}<[[<<]<}}[}]}<}],65536) (}<[[<<]}}}}[}}]<],65536) (}<[[<<]}<}}[}}]<],65536) (}<[[<<]<}}}[}}]<],65536) (}<[[<<]<}}<[}}]<],65536) (}<[[}<}]<[<<]}}<],65536) (}<[[}<}]}}<[<]}}],65536) (}<[[}<}]}}}<[<]}],65536) (}<[[<}}]<}<[<]}}],65536) (}<[[<<}]}[}}]}}<],65536) (}<[[<<}]<[}}]}}<],65536) (}<[[<<}]}}[}]}}<],65536) (}<[[<<}]}<[}]}}<],65536) (}<[[<}<<]}[}]<}<],65536) (}<[[[<]<]}<[}}]<],65536) (}<[[[}}]]<[<<]}}],65536) (}<[[[<<]]}}[}}]<],65536) (}<[[[<<]]}<[}}]<],65536) (}<[[<[]<]}<[}}]<],65536) (}<[[[<]}}]<}}}}<],65536) (}<[[[<<]}]<[}}]<],65536) (}<[[<[<]}}]<}}}<],65536) (}<[[}}<[<]<][]}}],65536) (}<[[}}<[<]<]}[]}],65536) (}<[[[<]}}<}}]}}<],65536) (}<[[[<]}}<}}][]<],65536) (}<[[[<<]}}}}][]<],65536) (}<[[<}[<]}}}]<}<],65536) (}<[[[}}]<[<<]]}}],65536) (}<[[[}}<[<]]<]}}],65536) (}<[[[}}<[<]<]]}}],65536) (}<[[<[}[<]}]<]}}],65536) (}<[[}}<[<][]<]}}],65536) (}<[[}}<[[<]]<]}}],65536) (}<[[}}<[<[]]<]}}],65536) (}<[[}}<[<<<}]]}}],286) (}<[[}}<[[<]<]]}}],65536) (}<[[[<]}}<}}}<]}],65536) (}<[[[<][]}}<}}]<],65536) (}<[[[<]}[}<]}}]<],65536) (}<[[[<]}}<[]}}]<],65536) (}<[[[<<][]}}}}]<],65536) (}<[[[<<]}}[}}]]<],65536) (}<[[[<<]}<[}}]]<],65536) (}<[[[[<]]}}<}}]<],65536) (}<[[[[<<]]}}}}]<],65536) (}<[[[[<]}}<]}}]<],65536) (}<[[[}}<[<]<]}]}],65536) (}<[[[[<]}}<}}]]<],65536) (}<[[[[<<]}}}}]]<],65536) (}<[[}[<<]}}}<<]}],65536) (}<[[<[<<]}}<}}]<],65536) (}<[[<[<<<]}}}}]<],65536) (}<[[<<[<<]}}}}]<],65536) (}<[[}}<[<<]}}<]}],65536) (}<[[}}<[<<]<}}]}],65536) (}<[[}}<[[<]<]}]}],65536) (}<[[[}}]<[<<]}}]],65536) (}<[[[<<]}}[}}]<]],65536) (}<[[[<<]}<[}}]<]],65536) (}<[[[}}<[<]<]}}]],65536) (}<[[[[<]}}<}}]<]],65536) (}<[[[[<<]}}}}]<]],65536) (}<[[}}<[[<]<]}}]],65536) (}<[}[<]<}<[<<]}}],65536) (}<[<[<]}[}<}]}}<],65536) (}<[<[<]}<[}<}]<<],65536) (}<[<[<]}<[<}}]<<],65536) (}<[}[<<][}]}}}<<],65536) (}<[}[<<][<]}}}<<],65536) (}<[}[<<]}}}[}]<<],65536) (}<[}[<<]}}}[<]<<],65536) (}<[<[<<]}}[}]<}<],65536) (}<[}[}<}]}}<[<]}],65536) (}<[<[<}<]}[}]}}<],65536) (}<[}[<[}]<]}}}<<],65536) (}<[}[<[<]<]}}}<<],65536) (}<[}}[]<[[<]<]}}],65536) (}<[}}[}]<[<<]}}<],65536) (}<[}}[<]<[<<]}}<],65536) (}<[<<[<]}}[}]<}<],65536) (}<[}}[}}]<[<<]}}],65536) (}<[<<[<<]}}[}}]<],65536) (}<[<<[<<]}<[}}]<],65536) (}<[<}[}<}]<[<]}}],65536) (}<[<}[[<]}}}<}]<],65536) (}<[<}[}<}}<[<]}]],65536) (}<[}}<[<<][}]}}<],65536) (}<[}}<[<<][<]}}<],65536) (}<[}}<[<<]}[<<]}],65536) (}<[}}<[[<]<][]}}],65536) (}<[}}<[[<]<]}[]}],65536) (}<[}}<[<[}]<]}}<],65536) (}<[}}<[<[<]<]}}<],65536) (}<[<<}[[}}]}]<<}],65536) (}<[}}<[[<][]<]}}],65536) (}<[}}<[[[<]]<]}}],65536) (}<[}}<[[<<<}]]}}],276) (}<[}}<[[[<]<]]}}],65536) (}<[<<}<[}]}[}}]<],65536) (}<[<<}<[<]}[}}]<],65536) (}<[<<}<[[}<}]}]<],65536) (}<[}<}}}}<[<]<}<],65536) (}<[<}}<}}<[<]}<}],65536) </pre> == Helping AProVE == To make AProVE verify more complicated programs; one must simplify them first. for this we will use 4 additional operations: <code>*</code>, <code>></code>, <code>(</code> and <code>)</code> Lets define what they mean; <code>*</code> toggles the current bit; <code>></code> moves right; <code>(code)</code> is a do while loop. its like a while loop but <code>code</code> always runs at least once, then checks. then we can make the following transformations: {| class="wikitable" |- ! From !! To !! Reasoning |- | <code>}<</code> || <code>*</code> || <code>*> <</code> becomes <code>*</code> because <code>><</code> cancels out |- | <code>*}</code>|| <code>></code> || <code>* *></code> becomes <code>></code> because <code>**</code> cancels out |- | <code>[[code1]code2]</code>|| <code>[(code1)code2]</code> || For the outer loop to be entered, the current bit needs to be 1. This makes it such that if the inner loop is reached it always enters (just like a do while loop) |- | <code>code[code]</code> || <code>(code)</code> || I will produce a formal proof later. |} '''NOTE: these dont take the same amount of steps, but if the transformed code halts/loops so does the original code, also vice versa.''' Initializing a starting tape also helps, <code>}}}<[[<<]}<[}}]<]</code> becomes <code>[[<<]}<[}}]<]</code> starting on <code>P0(V1(V1(e)),V1(e))</code> then we apply transformations, <code>[[<<]}<[}}]<]</code> to <code>[[<<]*[}}]<]</code> to <code>[(<<)*[}}]<]</code> We can logicaly transform it to <code>[(<<)*(}})<]</code> because at the end of <code>(<<)</code> the current bit must be 0, which gets toggled into 1 because of the <code>*</code>, which causes the <code>[]</code> to be equivalent to <code>()</code>. then we can convert it to a TRS with this python code. simply copy the program, run the script and then paste the term rewriting system. <pre> import pyperclip code = pyperclip.paste() out = "(VAR X Y)\n(TERM P0(e,e))\n(RULES\n" def findLR(i, depth): if code[i] == '[': return findLR(i + 1, depth + 1) elif code[i] == ']' and depth == 0: return i elif code[i] == ']' and depth != 0: return findLR(i + 1, depth - 1) else: return findLR(i + 1, depth) def findRL(i, depth): if code[i] == ']': return findRL(i - 1, depth + 1) elif code[i] == '[' and depth == 0: return i elif code[i] == '[' and depth != 0: return findRL(i - 1, depth - 1) else: return findRL(i - 1, depth) def findRL2(i, depth): if code[i] == ')': return findRL2(i - 1, depth + 1) elif code[i] == '(' and depth == 0: return i elif code[i] == '(' and depth != 0: return findRL2(i - 1, depth - 1) else: return findRL2(i - 1, depth) i = 0 for instr in code: if instr == '*': out += "P" + str(i) + "(X,V0(Y)) -> P" + str(i + 1) + "(X,V1(Y))\nP" + str(i) + "(X,V1(Y)) -> P" + str(i + 1) + "(X,V0(Y))\n" if instr == '}': out += "P" + str(i) + "(X,V0(Y)) -> P" + str(i + 1) + "(V1(X),Y)\nP" + str(i) + "(X,V1(Y)) -> P" + str(i + 1) + "(V0(X),Y)\n" if instr == '<': out += "P" + str(i) + "(V0(X),Y) -> P" + str(i + 1) + "(X,V0(Y))\nP" + str(i) + "(V1(X),Y) -> P" + str(i + 1) + "(X,V1(Y))\n" if instr == '>': out += "P" + str(i) + "(X,V0(Y)) -> P" + str(i + 1) + "(V0(X),Y)\nP" + str(i) + "(X,V1(Y)) -> P" + str(i + 1) + "(V1(X),Y)\n" if instr == '[': i2 = findLR(i + 1, 0) out += "P" + str(i) + "(X,V0(Y)) -> P" + str(i2 + 1) + "(X,V0(Y))\nP" + str(i) + "(X,V1(Y)) -> P" + str(i + 1) + "(X,V1(Y))\n" if instr == ']': i2 = findRL(i - 1, 0) out += "P" + str(i) + "(X,V0(Y)) -> P" + str(i + 1) + "(X,V0(Y))\nP" + str(i) + "(X,V1(Y)) -> P" + str(i2) + "(X,V1(Y))\n" if instr == ')': i2 = findRL2(i - 1, 0) out += "P" + str(i) + "(X,V0(Y)) -> P" + str(i2) + "(X,V0(Y))\nP" + str(i) + "(X,V1(Y)) -> P" + str(i2) + "(X,V1(Y))\n" if instr == '(': out += "P" + str(i) + "(X,Y) -> P" + str(i + 1) + "(X,Y)" out += "P" + str(i) + "(e,Y) -> P" + str(i) + "(V0(e),Y)\nP" + str(i) + "(X,e) -> P" + str(i) + "(X,V0(e))\n" i += 1 out += "P" + str(len(code)) + "(X,Y) -> F\n)" pyperclip.copy(out) </pre> then the TRS from <code>[(<<)*(}})<]</code> becomes: <pre> (VAR X Y) (TERM P0(e,e)) (RULES P0(X,V0(Y)) -> P12(X,V0(Y)) P0(X,V1(Y)) -> P1(X,V1(Y)) P0(e,Y) -> P0(V0(e),Y) P0(X,e) -> P0(X,V0(e)) P1(X,Y) -> P2(X,Y) P1(e,Y) -> P1(V0(e),Y) P1(X,e) -> P1(X,V0(e)) P2(V0(X),Y) -> P3(X,V0(Y)) P2(V1(X),Y) -> P3(X,V1(Y)) P2(e,Y) -> P2(V0(e),Y) P2(X,e) -> P2(X,V0(e)) P3(V0(X),Y) -> P4(X,V0(Y)) P3(V1(X),Y) -> P4(X,V1(Y)) P3(e,Y) -> P3(V0(e),Y) P3(X,e) -> P3(X,V0(e)) P4(X,V0(Y)) -> P1(X,V0(Y)) P4(X,V1(Y)) -> P1(X,V1(Y)) P4(e,Y) -> P4(V0(e),Y) P4(X,e) -> P4(X,V0(e)) P5(X,V0(Y)) -> P6(X,V1(Y)) P5(X,V1(Y)) -> P6(X,V0(Y)) P5(e,Y) -> P5(V0(e),Y) P5(X,e) -> P5(X,V0(e)) P6(X,Y) -> P7(X,Y) P6(e,Y) -> P6(V0(e),Y) P6(X,e) -> P6(X,V0(e)) P7(X,V0(Y)) -> P8(V1(X),Y) P7(X,V1(Y)) -> P8(V0(X),Y) P7(e,Y) -> P7(V0(e),Y) P7(X,e) -> P7(X,V0(e)) P8(X,V0(Y)) -> P9(V1(X),Y) P8(X,V1(Y)) -> P9(V0(X),Y) P8(e,Y) -> P8(V0(e),Y) P8(X,e) -> P8(X,V0(e)) P9(X,V0(Y)) -> P6(X,V0(Y)) P9(X,V1(Y)) -> P6(X,V1(Y)) P9(e,Y) -> P9(V0(e),Y) P9(X,e) -> P9(X,V0(e)) P10(V0(X),Y) -> P11(X,V0(Y)) P10(V1(X),Y) -> P11(X,V1(Y)) P10(e,Y) -> P10(V0(e),Y) P10(X,e) -> P10(X,V0(e)) P11(X,V0(Y)) -> P12(X,V0(Y)) P11(X,V1(Y)) -> P0(X,V1(Y)) P11(e,Y) -> P11(V0(e),Y) P11(X,e) -> P11(X,V0(e)) P12(X,Y) -> F ) </pre> Keep in mind, this assumes a empty starting tape. To start on 1 1 {1}, we need to replace <code>(TERM P0(e,e))</code> with <code>(TERM P0(V1(V1(e)),V1(e)))</code> Then run the code here: https://aprove.informatik.rwth-aachen.de/index.php/interface/v-AProVE2023/trs_wst It will then disprove termination.'