Examine individual changes

Abuse Filter navigation (Home | Recent filter changes | Examine past edits | Abuse log)
Jump to navigation Jump to search

This page allows you to examine the variables generated by the Abuse Filter for an individual change.

Variables generated for this change

VariableValue
Edit count of the user (user_editcount)
63
Name of the user account (user_name)
'C++DSUCKER'
Age of the user account (user_age)
4470442
Page ID (page_id)
21997
Page namespace (page_namespace)
0
Page title (without namespace) (page_title)
'BitChanger Busy beaver/Proof'
Full page title (page_prefixedtitle)
'BitChanger Busy beaver/Proof'
Action (action)
'edit'
Edit summary/reason (summary)
''
Old content model (old_content_model)
'wikitext'
New content model (new_content_model)
'wikitext'
Old page wikitext, before the edit (old_wikitext)
'= 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>'
New page wikitext, after the edit (new_wikitext)
'= 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.'
Unified diff of changes made by edit (edit_diff)
'@@ -698,2 +698,637 @@ (}<[[<[<<]}}}}]<],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. '
New page size (new_size)
37245
Old page size (old_size)
19165
Lines added in edit (added_lines)
[ 0 => '', 1 => '', 2 => '== Using AProVE ==', 3 => 'for more complicated programs, it is better to use [https://aprove.informatik.rwth-aachen.de/index.php/interface/v-AProVE2023/trs_wst AProVE].', 4 => 'it can prove complicated programs for length 17.', 5 => '', 6 => '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...', 7 => '', 8 => 'the bitchanger program <code>}<[<[<<]}}[}]<}<]</code> first becomes <code>', 9 => '[<[<<]}(})<*]</code> where <code>()</code> are do while loops, and <code>*</code> is toggle current bit.', 10 => '', 11 => 'then we convert that code to this term rewriting system:', 12 => '<pre>', 13 => '(VAR X Y)', 14 => '(TERM P0(e,V1(e)))', 15 => '(RULES', 16 => 'P0(X,V0(Y)) -> P13(X,V0(Y))', 17 => 'P0(X,V1(Y)) -> P1(X,V1(Y))', 18 => 'P0(e,Y) -> P0(V0(e),Y)', 19 => 'P0(X,e) -> P0(X,V0(e))', 20 => 'P1(V0(X),Y) -> P2(X,V0(Y))', 21 => 'P1(V1(X),Y) -> P2(X,V1(Y))', 22 => 'P1(e,Y) -> P1(V0(e),Y)', 23 => 'P1(X,e) -> P1(X,V0(e))', 24 => 'P2(X,V0(Y)) -> P6(X,V0(Y))', 25 => 'P2(X,V1(Y)) -> P3(X,V1(Y))', 26 => 'P2(e,Y) -> P2(V0(e),Y)', 27 => 'P2(X,e) -> P2(X,V0(e))', 28 => 'P3(V0(X),Y) -> P4(X,V0(Y))', 29 => 'P3(V1(X),Y) -> P4(X,V1(Y))', 30 => 'P3(e,Y) -> P3(V0(e),Y)', 31 => 'P3(X,e) -> P3(X,V0(e))', 32 => 'P4(V0(X),Y) -> P5(X,V0(Y))', 33 => 'P4(V1(X),Y) -> P5(X,V1(Y))', 34 => 'P4(e,Y) -> P4(V0(e),Y)', 35 => 'P4(X,e) -> P4(X,V0(e))', 36 => 'P5(X,V0(Y)) -> P6(X,V0(Y))', 37 => 'P5(X,V1(Y)) -> P2(X,V1(Y))', 38 => 'P5(e,Y) -> P5(V0(e),Y)', 39 => 'P5(X,e) -> P5(X,V0(e))', 40 => 'P6(X,V0(Y)) -> P7(V1(X),Y)', 41 => 'P6(X,V1(Y)) -> P7(V0(X),Y)', 42 => 'P6(e,Y) -> P6(V0(e),Y)', 43 => 'P6(X,e) -> P6(X,V0(e))', 44 => 'P7(X,Y) -> P8(X,Y)', 45 => 'P7(e,Y) -> P7(V0(e),Y)', 46 => 'P7(X,e) -> P7(X,V0(e))', 47 => 'P8(X,V0(Y)) -> P9(V1(X),Y)', 48 => 'P8(X,V1(Y)) -> P9(V0(X),Y)', 49 => 'P8(e,Y) -> P8(V0(e),Y)', 50 => 'P8(X,e) -> P8(X,V0(e))', 51 => 'P9(X,V0(Y)) -> P7(X,V0(Y))', 52 => 'P9(X,V1(Y)) -> P7(X,V1(Y))', 53 => 'P9(e,Y) -> P9(V0(e),Y)', 54 => 'P9(X,e) -> P9(X,V0(e))', 55 => 'P10(V0(X),Y) -> P11(X,V0(Y))', 56 => 'P10(V1(X),Y) -> P11(X,V1(Y))', 57 => 'P10(e,Y) -> P10(V0(e),Y)', 58 => 'P10(X,e) -> P10(X,V0(e))', 59 => 'P11(X,V0(Y)) -> P12(X,V1(Y))', 60 => 'P11(X,V1(Y)) -> P12(X,V0(Y))', 61 => 'P11(e,Y) -> P11(V0(e),Y)', 62 => 'P11(X,e) -> P11(X,V0(e))', 63 => 'P12(X,V0(Y)) -> F', 64 => 'P12(X,V1(Y)) -> P0(X,V1(Y))', 65 => 'P12(e,Y) -> P12(V0(e),Y)', 66 => 'P12(X,e) -> P12(X,V0(e))', 67 => ')', 68 => '</pre>', 69 => '', 70 => 'then AProVE disproves termination.', 71 => '', 72 => '== Progress towards BB(17) ==', 73 => 'This is the output of [[User:Int-e|Int-e]]'s halskell Program for length 17: for convention 2:', 74 => '', 75 => '<pre>', 76 => '(}<<<}<[}<}}<[<]}],65536)', 77 => '(}}}<<[}[<<]}}}<<],65536)', 78 => '(}}}<<[}}<[<<]}}<],65536)', 79 => '(}}}<[[}}]<[<<]}}],65537)', 80 => '(}}}<[[<<]}}[}}]<],65537)', 81 => '(}}}<[[<<]}<[}}]<],65536)', 82 => '(}}}<[[<}<<]}[}]}],65537)', 83 => '(}}}<[[}}<[<]<]}}],65536)', 84 => '(}}}<[[[<]}}<}}]<],65536)', 85 => '(}}}<[[[<<]}}}}]<],65536)', 86 => '(}}}<[<[}<}]}<<<}],65536)', 87 => '(}}}<[}}<[[<]<]}}],65536)', 88 => '(}}<<[<}<[}<}]}<<],65536)', 89 => '(}}<[[}]}<[<}<]}}],65537)', 90 => '(}}<[[}]}}<[<<}]}],65536)', 91 => '(}}<[[<]}[}<}]}}<],65536)', 92 => '(}}<[[<]}[}<}]<<<],65537)', 93 => '(}}<[[<]}<[}<}]<<],65537)', 94 => '(}}<[[<]}<[<}}]<<],65536)', 95 => '(}}<[[}}]<[<<]}}<],65536)', 96 => '(}}<[[}}]}<[<<}]<],65537)', 97 => '(}}<[[}<}]}}<[<]}],65537)', 98 => '(}}<[[<}<<]}[}}]}],65536)', 99 => '(}}<[[[<]}}]<}}}<],65536)', 100 => '(}}<[[[<]}}]<}<<<],65537)', 101 => '(}}<[[}[<<]]}}}<<],65536)', 102 => '(}}<[[<[<<]}}]<}<],65537)', 103 => '(}}<[[}}<[<<]]}}<],65537)', 104 => '(}}<[[}[<<]}}}]<<],65536)', 105 => '(}}<[[}<}}<[<]}]}],65537)', 106 => '(}}<[[}[<<]}}}<<]],65536)', 107 => '(}}<[[}}<[<<]}}<]],65537)', 108 => '(}}<[}[<<][]}}}<<],65536)', 109 => '(}}<[}[<<]}}}[]<<],65536)', 110 => '(}}<[}[<<<]}}}}<<],65536)', 111 => '(}}<[<[<}}]<<[<]}],65536)', 112 => '(}}<[}[<<<<]}}}<<],65536)', 113 => '(}}<[}[[<]<]}}}<<],65536)', 114 => '(}}<[}[[<<]]}}}<<],65536)', 115 => '(}}<[}[<[]<]}}}<<],65536)', 116 => '(}}<[<[[<]}}]<}<<],65536)', 117 => '(}}<[<[[}<}]}]<<}],65537)', 118 => '(}}<[<[}[<<]<]}}}],65536)', 119 => '(}}<[<[[[<]}}]}]<],65536)', 120 => '(}}<[}}[]<[<<]}}<],65536)', 121 => '(}}<[}}[<]<[<<]}}],65536)', 122 => '(}}<[}<[}]}}<[<]}],65536)', 123 => '(}}<[}<[<]}}<[<]}],65536)', 124 => '(}}<[}}<[<<][]}}<],65536)', 125 => '(}}<[}}<[<<<]}}}<],65536)', 126 => '(}}<[}}<[<<<<]}}<],65537)', 127 => '(}}<[}}<[[<]<]}}<],65536)', 128 => '(}}<[}}<[[<<]]}}<],65536)', 129 => '(}}<[}}<[<[]<]}}<],65536)', 130 => '(}}<[}}<<[}]}[<]}],65536)', 131 => '(}}<[}}<<[<]}[<]}],65536)', 132 => '(}}<[<}<<[<]}[}]}],65536)', 133 => '(}}<[}}}<[<<<]}}<],65536)', 134 => '(}}<[}}}<[[<]<<]}],65536)', 135 => '(}}<[}<}}<[<][}]}],65536)', 136 => '(}}<[}<}}<[<][<]}],65536)', 137 => '(}}<[}<}}<[<[<]]}],65537)', 138 => '(}}<[}<}}}<[<]<}}],65536)', 139 => '(}<[[}]<}<[<}<<]}],65536)', 140 => '(}<[[}]<}<<<[<]}}],65536)', 141 => '(}<[[}]<}<<}[<]}}],65537)', 142 => '(}<[[<]}[}<}]}}}<],65537)', 143 => '(}<[[<]}}[}<}]}}<],65536)', 144 => '(}<[[<]}<[}<}]}}<],65536)', 145 => '(}<[[<]}<[<}}]<<<],65536)', 146 => '(}<[[<]}}}[}]<<}<],65536)', 147 => '(}<[[}}][]<[<<]}}],65536)', 148 => '(}<[[}}]<[<<]}<}}],65536)', 149 => '(}<[[}}]<[<<]<}}}],65536)', 150 => '(}<[[}}]<[<<][]}}],65536)', 151 => '(}<[[}}]<[[<]<]}}],65537)', 152 => '(}<[[}}]<[[<<]]}}],65536)', 153 => '(}<[[}}]<[[<<]}]<],65536)', 154 => '(}<[[}}]<<<[<<]}}],65537)', 155 => '(}<[[}}]}}<[<<}]}],65537)', 156 => '(}<[[}}]}}<[<<}]<],65537)', 157 => '(}<[[<<][]}}[}}]<],65536)', 158 => '(}<[[<<][]}<[}}]<],65536)', 159 => '(}<[[<<]}[]<[}}]<],65536)', 160 => '(}<[[<<]}}[}}]<<<],65536)', 161 => '(}<[[<<]}}[}}][]<],65536)', 162 => '(}<[[<<]}<[}}]<<<],65536)', 163 => '(}<[[<<]}<[}}][]<],65536)', 164 => '(}<[[<<]}}[[}}]]<],65536)', 165 => '(}<[[<<]}<[[}}]]<],65536)', 166 => '(}<[[<<]<}}[}]}<}],65536)', 167 => '(}<[[<<]}}}}[}}]<],65537)', 168 => '(}<[[<<]}<}}[}}]<],65536)', 169 => '(}<[[<<]<}}}[}}]<],65536)', 170 => '(}<[[<<]<}}<[}}]<],65536)', 171 => '(}<[[}<}]<[<<]}}<],65536)', 172 => '(}<[[}<}]}}<[<]}}],65537)', 173 => '(}<[[}<}]}}}<[<]}],65537)', 174 => '(}<[[<}}]<}<[<]}}],65536)', 175 => '(}<[[<<}]}[}}]}}<],65536)', 176 => '(}<[[<<}]<[}}]}}<],65536)', 177 => '(}<[[<<}]}}[}]}}<],65536)', 178 => '(}<[[<<}]}<[}]}}<],65536)', 179 => '(}<[[<}<<]}[}]<}<],65536)', 180 => '(}<[[[<]<]}<[}}]<],65536)', 181 => '(}<[[[}}]]<[<<]}}],65537)', 182 => '(}<[[[<<]]}}[}}]<],65536)', 183 => '(}<[[[<<]]}<[}}]<],65536)', 184 => '(}<[[<[]<]}<[}}]<],65537)', 185 => '(}<[[[<]}}]<}}}}<],65536)', 186 => '(}<[[[<<]}]<[}}]<],65536)', 187 => '(}<[[<[<]}}]<}}}<],65536)', 188 => '(}<[[}}<[<]<][]}}],65536)', 189 => '(}<[[}}<[<]<]}[]}],65536)', 190 => '(}<[[[<]}}<}}]}}<],65536)', 191 => '(}<[[[<]}}<}}][]<],65537)', 192 => '(}<[[[<<]}}}}][]<],65536)', 193 => '(}<[[<}[<]}}}]<}<],65536)', 194 => '(}<[[[}}]<[<<]]}}],65537)', 195 => '(}<[[[}}<[<]]<]}}],65536)', 196 => '(}<[[[}}<[<]<]]}}],65536)', 197 => '(}<[[<[}[<]}]<]}}],65536)', 198 => '(}<[[}}<[<][]<]}}],65536)', 199 => '(}<[[}}<[[<]]<]}}],65536)', 200 => '(}<[[}}<[<[]]<]}}],65536)', 201 => '(}<[[}}<[<<<}]]}}],346)', 202 => '(}<[[}}<[[<]<]]}}],65536)', 203 => '(}<[[[<]}}<}}}<]}],65537)', 204 => '(}<[[[<][]}}<}}]<],65536)', 205 => '(}<[[[<]}[}<]}}]<],65536)', 206 => '(}<[[[<]}}<[]}}]<],65536)', 207 => '(}<[[[<<][]}}}}]<],65536)', 208 => '(}<[[[<<]}}[}}]]<],65536)', 209 => '(}<[[[<<]}<[}}]]<],65536)', 210 => '(}<[[[[<]]}}<}}]<],65537)', 211 => '(}<[[[[<<]]}}}}]<],65536)', 212 => '(}<[[[[<]}}<]}}]<],65536)', 213 => '(}<[[[}}<[<]<]}]}],65536)', 214 => '(}<[[[[<]}}<}}]]<],65536)', 215 => '(}<[[[[<<]}}}}]]<],65537)', 216 => '(}<[[}[<<]}}}<<]}],65536)', 217 => '(}<[[<[<<]}}<}}]<],65536)', 218 => '(}<[[<[<<<]}}}}]<],65536)', 219 => '(}<[[<<[<<]}}}}]<],65536)', 220 => '(}<[[}}<[<<]}}<]}],65537)', 221 => '(}<[[}}<[<<]<}}]}],65536)', 222 => '(}<[[}}<[[<]<]}]}],65536)', 223 => '(}<[[[}}]<[<<]}}]],65536)', 224 => '(}<[[[<<]}}[}}]<]],65537)', 225 => '(}<[[[<<]}<[}}]<]],65536)', 226 => '(}<[[[}}<[<]<]}}]],65537)', 227 => '(}<[[[[<]}}<}}]<]],65536)', 228 => '(}<[[[[<<]}}}}]<]],65536)', 229 => '(}<[[}}<[[<]<]}}]],65536)', 230 => '(}<[}[<]<}<[<<]}}],65536)', 231 => '(}<[<[<]}[}<}]}}<],65536)', 232 => '(}<[<[<]}<[}<}]<<],65537)', 233 => '(}<[<[<]}<[<}}]<<],65537)', 234 => '(}<[}[<<][}]}}}<<],65536)', 235 => '(}<[}[<<][<]}}}<<],65536)', 236 => '(}<[}[<<]}}}[}]<<],65536)', 237 => '(}<[}[<<]}}}[<]<<],65536)', 238 => '(}<[<[<<]}}[}]<}<],65536)', 239 => '(}<[}[}<}]}}<[<]}],65536)', 240 => '(}<[<[<}<]}[}]}}<],65536)', 241 => '(}<[}[<[}]<]}}}<<],65536)', 242 => '(}<[}[<[<]<]}}}<<],65536)', 243 => '(}<[}}[]<[[<]<]}}],65536)', 244 => '(}<[}}[}]<[<<]}}<],65536)', 245 => '(}<[}}[<]<[<<]}}<],65536)', 246 => '(}<[<<[<]}}[}]<}<],65536)', 247 => '(}<[}}[}}]<[<<]}}],65536)', 248 => '(}<[<<[<<]}}[}}]<],65537)', 249 => '(}<[<<[<<]}<[}}]<],65536)', 250 => '(}<[<}[}<}]<[<]}}],65536)', 251 => '(}<[<}[[<]}}}<}]<],65536)', 252 => '(}<[<}[}<}}<[<]}]],65536)', 253 => '(}<[}}<[<<][}]}}<],65536)', 254 => '(}<[}}<[<<][<]}}<],65536)', 255 => '(}<[}}<[<<]}[<<]}],65536)', 256 => '(}<[}}<[[<]<][]}}],65536)', 257 => '(}<[}}<[[<]<]}[]}],65536)', 258 => '(}<[}}<[<[}]<]}}<],65536)', 259 => '(}<[}}<[<[<]<]}}<],65536)', 260 => '(}<[<<}[[}}]}]<<}],65536)', 261 => '(}<[}}<[[<][]<]}}],65536)', 262 => '(}<[}}<[[[<]]<]}}],65536)', 263 => '(}<[}}<[[[<]<]]}}],65537)', 264 => '(}<[<<}<[}]}[}}]<],65536)', 265 => '(}<[<<}<[<]}[}}]<],65536)', 266 => '(}<[<<}<[[}<}]}]<],65536)', 267 => '(}<[}<}}}}<[<]<}<],65536)', 268 => '(}<[<}}<}}<[<]}<}],65536)', 269 => '</pre>', 270 => 'and for convention 1:', 271 => '', 272 => '<pre>', 273 => '(}<<<}<[}<}}<[<]}],65536)', 274 => '(}}}<<[}[<<]}}}<<],65536)', 275 => '(}}}<<[}}<[<<]}}<],65536)', 276 => '(}}}<[[}}]<[<<]}}],65536)', 277 => '(}}}<[[<<]}}[}}]<],65536)', 278 => '(}}}<[[<<]}<[}}]<],65536)', 279 => '(}}}<[[<}<<]}[}]}],65536)', 280 => '(}}}<[[}}<[<]<]}}],65536)', 281 => '(}}}<[[[<]}}<}}]<],65536)', 282 => '(}}}<[[[<<]}}}}]<],65536)', 283 => '(}}}<[<[}<}]}<<<}],65536)', 284 => '(}}}<[}}<[[<]<]}}],65536)', 285 => '(}}<<[<}<[}<}]}<<],65536)', 286 => '(}}<[[}]}<[<}<]}}],65536)', 287 => '(}}<[[}]}}<[<<}]}],65536)', 288 => '(}}<[[<]}[}<}]}}<],65536)', 289 => '(}}<[[<]}[}<}]<<<],65536)', 290 => '(}}<[[<]}<[}<}]<<],65536)', 291 => '(}}<[[<]}<[<}}]<<],65536)', 292 => '(}}<[[}}]<[<<]}}<],65536)', 293 => '(}}<[[}}]}<[<<}]<],65536)', 294 => '(}}<[[}<}]}}<[<]}],65536)', 295 => '(}}<[[<}<<]}[}}]}],65536)', 296 => '(}}<[[[<]}}]<}}}<],65536)', 297 => '(}}<[[[<]}}]<}<<<],65536)', 298 => '(}}<[[}[<<]]}}}<<],65536)', 299 => '(}}<[[<[<<]}}]<}<],65536)', 300 => '(}}<[[}}<[<<]]}}<],65536)', 301 => '(}}<[[}[<<]}}}]<<],65536)', 302 => '(}}<[[}<}}<[<]}]}],65536)', 303 => '(}}<[[}[<<]}}}<<]],65536)', 304 => '(}}<[[}}<[<<]}}<]],65536)', 305 => '(}}<[}[<<][]}}}<<],65536)', 306 => '(}}<[}[<<]}}}[]<<],65536)', 307 => '(}}<[}[<<<]}}}}<<],65536)', 308 => '(}}<[<[<}}]<<[<]}],65536)', 309 => '(}}<[}[<<<<]}}}<<],65536)', 310 => '(}}<[}[[<]<]}}}<<],65536)', 311 => '(}}<[}[[<<]]}}}<<],65536)', 312 => '(}}<[}[<[]<]}}}<<],65536)', 313 => '(}}<[<[[<]}}]<}<<],65536)', 314 => '(}}<[<[[}<}]}]<<}],65536)', 315 => '(}}<[<[}[<<]<]}}}],65536)', 316 => '(}}<[<[[[<]}}]}]<],65536)', 317 => '(}}<[}}[]<[<<]}}<],65536)', 318 => '(}}<[}}[<]<[<<]}}],65536)', 319 => '(}}<[}<[}]}}<[<]}],65536)', 320 => '(}}<[}<[<]}}<[<]}],65536)', 321 => '(}}<[}}<[<<][]}}<],65536)', 322 => '(}}<[}}<[<<<]}}}<],65536)', 323 => '(}}<[}}<[<<<<]}}<],65536)', 324 => '(}}<[}}<[[<]<]}}<],65536)', 325 => '(}}<[}}<[[<<]]}}<],65536)', 326 => '(}}<[}}<[<[]<]}}<],65536)', 327 => '(}}<[}}<<[}]}[<]}],65536)', 328 => '(}}<[}}<<[<]}[<]}],65536)', 329 => '(}}<[<}<<[<]}[}]}],65536)', 330 => '(}}<[}}}<[<<<]}}<],65536)', 331 => '(}}<[}}}<[[<]<<]}],65536)', 332 => '(}}<[}<}}<[<][}]}],65536)', 333 => '(}}<[}<}}<[<][<]}],65536)', 334 => '(}}<[}<}}<[<[<]]}],65536)', 335 => '(}}<[}<}}}<[<]<}}],65536)', 336 => '(}<[[}]<}<[<}<<]}],65536)', 337 => '(}<[[}]<}<<<[<]}}],65536)', 338 => '(}<[[}]<}<<}[<]}}],65536)', 339 => '(}<[[<]}[}<}]}}}<],65536)', 340 => '(}<[[<]}}[}<}]}}<],65536)', 341 => '(}<[[<]}<[}<}]}}<],65536)', 342 => '(}<[[<]}<[<}}]<<<],65536)', 343 => '(}<[[<]}}}[}]<<}<],65536)', 344 => '(}<[[}}][]<[<<]}}],65536)', 345 => '(}<[[}}]<[<<]}<}}],65536)', 346 => '(}<[[}}]<[<<]<}}}],65536)', 347 => '(}<[[}}]<[<<][]}}],65536)', 348 => '(}<[[}}]<[[<]<]}}],65536)', 349 => '(}<[[}}]<[[<<]]}}],65536)', 350 => '(}<[[}}]<[[<<]}]<],65536)', 351 => '(}<[[}}]<<<[<<]}}],65536)', 352 => '(}<[[}}]}}<[<<}]}],65536)', 353 => '(}<[[}}]}}<[<<}]<],65536)', 354 => '(}<[[<<][]}}[}}]<],65536)', 355 => '(}<[[<<][]}<[}}]<],65536)', 356 => '(}<[[<<]}[]<[}}]<],65536)', 357 => '(}<[[<<]}}[}}]<<<],65536)', 358 => '(}<[[<<]}}[}}][]<],65536)', 359 => '(}<[[<<]}<[}}]<<<],65536)', 360 => '(}<[[<<]}<[}}][]<],65536)', 361 => '(}<[[<<]}}[[}}]]<],65536)', 362 => '(}<[[<<]}<[[}}]]<],65536)', 363 => '(}<[[<<]<}}[}]}<}],65536)', 364 => '(}<[[<<]}}}}[}}]<],65536)', 365 => '(}<[[<<]}<}}[}}]<],65536)', 366 => '(}<[[<<]<}}}[}}]<],65536)', 367 => '(}<[[<<]<}}<[}}]<],65536)', 368 => '(}<[[}<}]<[<<]}}<],65536)', 369 => '(}<[[}<}]}}<[<]}}],65536)', 370 => '(}<[[}<}]}}}<[<]}],65536)', 371 => '(}<[[<}}]<}<[<]}}],65536)', 372 => '(}<[[<<}]}[}}]}}<],65536)', 373 => '(}<[[<<}]<[}}]}}<],65536)', 374 => '(}<[[<<}]}}[}]}}<],65536)', 375 => '(}<[[<<}]}<[}]}}<],65536)', 376 => '(}<[[<}<<]}[}]<}<],65536)', 377 => '(}<[[[<]<]}<[}}]<],65536)', 378 => '(}<[[[}}]]<[<<]}}],65536)', 379 => '(}<[[[<<]]}}[}}]<],65536)', 380 => '(}<[[[<<]]}<[}}]<],65536)', 381 => '(}<[[<[]<]}<[}}]<],65536)', 382 => '(}<[[[<]}}]<}}}}<],65536)', 383 => '(}<[[[<<]}]<[}}]<],65536)', 384 => '(}<[[<[<]}}]<}}}<],65536)', 385 => '(}<[[}}<[<]<][]}}],65536)', 386 => '(}<[[}}<[<]<]}[]}],65536)', 387 => '(}<[[[<]}}<}}]}}<],65536)', 388 => '(}<[[[<]}}<}}][]<],65536)', 389 => '(}<[[[<<]}}}}][]<],65536)', 390 => '(}<[[<}[<]}}}]<}<],65536)', 391 => '(}<[[[}}]<[<<]]}}],65536)', 392 => '(}<[[[}}<[<]]<]}}],65536)', 393 => '(}<[[[}}<[<]<]]}}],65536)', 394 => '(}<[[<[}[<]}]<]}}],65536)', 395 => '(}<[[}}<[<][]<]}}],65536)', 396 => '(}<[[}}<[[<]]<]}}],65536)', 397 => '(}<[[}}<[<[]]<]}}],65536)', 398 => '(}<[[}}<[<<<}]]}}],286)', 399 => '(}<[[}}<[[<]<]]}}],65536)', 400 => '(}<[[[<]}}<}}}<]}],65536)', 401 => '(}<[[[<][]}}<}}]<],65536)', 402 => '(}<[[[<]}[}<]}}]<],65536)', 403 => '(}<[[[<]}}<[]}}]<],65536)', 404 => '(}<[[[<<][]}}}}]<],65536)', 405 => '(}<[[[<<]}}[}}]]<],65536)', 406 => '(}<[[[<<]}<[}}]]<],65536)', 407 => '(}<[[[[<]]}}<}}]<],65536)', 408 => '(}<[[[[<<]]}}}}]<],65536)', 409 => '(}<[[[[<]}}<]}}]<],65536)', 410 => '(}<[[[}}<[<]<]}]}],65536)', 411 => '(}<[[[[<]}}<}}]]<],65536)', 412 => '(}<[[[[<<]}}}}]]<],65536)', 413 => '(}<[[}[<<]}}}<<]}],65536)', 414 => '(}<[[<[<<]}}<}}]<],65536)', 415 => '(}<[[<[<<<]}}}}]<],65536)', 416 => '(}<[[<<[<<]}}}}]<],65536)', 417 => '(}<[[}}<[<<]}}<]}],65536)', 418 => '(}<[[}}<[<<]<}}]}],65536)', 419 => '(}<[[}}<[[<]<]}]}],65536)', 420 => '(}<[[[}}]<[<<]}}]],65536)', 421 => '(}<[[[<<]}}[}}]<]],65536)', 422 => '(}<[[[<<]}<[}}]<]],65536)', 423 => '(}<[[[}}<[<]<]}}]],65536)', 424 => '(}<[[[[<]}}<}}]<]],65536)', 425 => '(}<[[[[<<]}}}}]<]],65536)', 426 => '(}<[[}}<[[<]<]}}]],65536)', 427 => '(}<[}[<]<}<[<<]}}],65536)', 428 => '(}<[<[<]}[}<}]}}<],65536)', 429 => '(}<[<[<]}<[}<}]<<],65536)', 430 => '(}<[<[<]}<[<}}]<<],65536)', 431 => '(}<[}[<<][}]}}}<<],65536)', 432 => '(}<[}[<<][<]}}}<<],65536)', 433 => '(}<[}[<<]}}}[}]<<],65536)', 434 => '(}<[}[<<]}}}[<]<<],65536)', 435 => '(}<[<[<<]}}[}]<}<],65536)', 436 => '(}<[}[}<}]}}<[<]}],65536)', 437 => '(}<[<[<}<]}[}]}}<],65536)', 438 => '(}<[}[<[}]<]}}}<<],65536)', 439 => '(}<[}[<[<]<]}}}<<],65536)', 440 => '(}<[}}[]<[[<]<]}}],65536)', 441 => '(}<[}}[}]<[<<]}}<],65536)', 442 => '(}<[}}[<]<[<<]}}<],65536)', 443 => '(}<[<<[<]}}[}]<}<],65536)', 444 => '(}<[}}[}}]<[<<]}}],65536)', 445 => '(}<[<<[<<]}}[}}]<],65536)', 446 => '(}<[<<[<<]}<[}}]<],65536)', 447 => '(}<[<}[}<}]<[<]}}],65536)', 448 => '(}<[<}[[<]}}}<}]<],65536)', 449 => '(}<[<}[}<}}<[<]}]],65536)', 450 => '(}<[}}<[<<][}]}}<],65536)', 451 => '(}<[}}<[<<][<]}}<],65536)', 452 => '(}<[}}<[<<]}[<<]}],65536)', 453 => '(}<[}}<[[<]<][]}}],65536)', 454 => '(}<[}}<[[<]<]}[]}],65536)', 455 => '(}<[}}<[<[}]<]}}<],65536)', 456 => '(}<[}}<[<[<]<]}}<],65536)', 457 => '(}<[<<}[[}}]}]<<}],65536)', 458 => '(}<[}}<[[<][]<]}}],65536)', 459 => '(}<[}}<[[[<]]<]}}],65536)', 460 => '(}<[}}<[[<<<}]]}}],276)', 461 => '(}<[}}<[[[<]<]]}}],65536)', 462 => '(}<[<<}<[}]}[}}]<],65536)', 463 => '(}<[<<}<[<]}[}}]<],65536)', 464 => '(}<[<<}<[[}<}]}]<],65536)', 465 => '(}<[}<}}}}<[<]<}<],65536)', 466 => '(}<[<}}<}}<[<]}<}],65536)', 467 => '</pre>', 468 => '', 469 => '== Helping AProVE ==', 470 => '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>', 471 => 'Lets define what they mean;', 472 => '', 473 => '<code>*</code> toggles the current bit;', 474 => '<code>></code> moves right;', 475 => '<code>(code)</code> is a do while loop. its like a while loop but <code>code</code> always runs at least once, then checks.', 476 => '', 477 => 'then we can make the following transformations:', 478 => '', 479 => '{| class="wikitable"', 480 => '|-', 481 => '! From !! To !! Reasoning', 482 => '|-', 483 => '| <code>}<</code> || <code>*</code> || <code>*> <</code> becomes <code>*</code> because <code>><</code> cancels out', 484 => '|-', 485 => '| <code>*}</code>|| <code>></code> || <code>* *></code> becomes <code>></code> because <code>**</code> cancels out', 486 => '|-', 487 => '| <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)', 488 => '|-', 489 => '| <code>code[code]</code> || <code>(code)</code> || I will produce a formal proof later.', 490 => '|}', 491 => '', 492 => ''''NOTE: these dont take the same amount of steps, but if the transformed code halts/loops so does the original code, also vice versa.'''', 493 => '', 494 => 'Initializing a starting tape also helps, ', 495 => '<code>}}}<[[<<]}<[}}]<]</code> becomes <code>[[<<]}<[}}]<]</code> starting on <code>P0(V1(V1(e)),V1(e))</code>', 496 => '', 497 => 'then we apply transformations,', 498 => '<code>[[<<]}<[}}]<]</code> to <code>[[<<]*[}}]<]</code> to <code>[(<<)*[}}]<]</code>', 499 => '', 500 => '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>.', 501 => '', 502 => 'then we can convert it to a TRS with this python code.', 503 => 'simply copy the program, run the script and then paste the term rewriting system.', 504 => '', 505 => '<pre>', 506 => 'import pyperclip', 507 => '', 508 => 'code = pyperclip.paste()', 509 => '', 510 => '', 511 => 'out = "(VAR X Y)\n(TERM P0(e,e))\n(RULES\n"', 512 => '', 513 => 'def findLR(i, depth):', 514 => ' if code[i] == '[':', 515 => ' return findLR(i + 1, depth + 1)', 516 => ' elif code[i] == ']' and depth == 0:', 517 => ' return i', 518 => ' elif code[i] == ']' and depth != 0:', 519 => ' return findLR(i + 1, depth - 1)', 520 => ' else:', 521 => ' return findLR(i + 1, depth)', 522 => '', 523 => 'def findRL(i, depth):', 524 => ' if code[i] == ']':', 525 => ' return findRL(i - 1, depth + 1)', 526 => ' elif code[i] == '[' and depth == 0:', 527 => ' return i', 528 => ' elif code[i] == '[' and depth != 0:', 529 => ' return findRL(i - 1, depth - 1)', 530 => ' else:', 531 => ' return findRL(i - 1, depth)', 532 => 'def findRL2(i, depth):', 533 => ' if code[i] == ')':', 534 => ' return findRL2(i - 1, depth + 1)', 535 => ' elif code[i] == '(' and depth == 0:', 536 => ' return i', 537 => ' elif code[i] == '(' and depth != 0:', 538 => ' return findRL2(i - 1, depth - 1)', 539 => ' else:', 540 => ' return findRL2(i - 1, depth)', 541 => '', 542 => '', 543 => 'i = 0', 544 => '', 545 => 'for instr in code:', 546 => ' if instr == '*':', 547 => ' 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"', 548 => ' if instr == '}':', 549 => ' 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"', 550 => ' if instr == '<':', 551 => ' 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"', 552 => ' if instr == '>':', 553 => ' 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"', 554 => ' if instr == '[':', 555 => ' i2 = findLR(i + 1, 0)', 556 => ' 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"', 557 => ' if instr == ']':', 558 => ' i2 = findRL(i - 1, 0)', 559 => ' 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"', 560 => ' if instr == ')':', 561 => ' i2 = findRL2(i - 1, 0)', 562 => ' 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"', 563 => ' if instr == '(':', 564 => ' out += "P" + str(i) + "(X,Y) -> P" + str(i + 1) + "(X,Y)"', 565 => ' out += "P" + str(i) + "(e,Y) -> P" + str(i) + "(V0(e),Y)\nP" + str(i) + "(X,e) -> P" + str(i) + "(X,V0(e))\n"', 566 => ' i += 1', 567 => '', 568 => 'out += "P" + str(len(code)) + "(X,Y) -> F\n)"', 569 => '', 570 => 'pyperclip.copy(out)', 571 => '</pre>', 572 => '', 573 => 'then the TRS from <code>[(<<)*(}})<]</code> becomes:', 574 => '', 575 => '<pre>', 576 => '(VAR X Y)', 577 => '(TERM P0(e,e))', 578 => '(RULES', 579 => 'P0(X,V0(Y)) -> P12(X,V0(Y))', 580 => 'P0(X,V1(Y)) -> P1(X,V1(Y))', 581 => 'P0(e,Y) -> P0(V0(e),Y)', 582 => 'P0(X,e) -> P0(X,V0(e))', 583 => 'P1(X,Y) -> P2(X,Y)', 584 => 'P1(e,Y) -> P1(V0(e),Y)', 585 => 'P1(X,e) -> P1(X,V0(e))', 586 => 'P2(V0(X),Y) -> P3(X,V0(Y))', 587 => 'P2(V1(X),Y) -> P3(X,V1(Y))', 588 => 'P2(e,Y) -> P2(V0(e),Y)', 589 => 'P2(X,e) -> P2(X,V0(e))', 590 => 'P3(V0(X),Y) -> P4(X,V0(Y))', 591 => 'P3(V1(X),Y) -> P4(X,V1(Y))', 592 => 'P3(e,Y) -> P3(V0(e),Y)', 593 => 'P3(X,e) -> P3(X,V0(e))', 594 => 'P4(X,V0(Y)) -> P1(X,V0(Y))', 595 => 'P4(X,V1(Y)) -> P1(X,V1(Y))', 596 => 'P4(e,Y) -> P4(V0(e),Y)', 597 => 'P4(X,e) -> P4(X,V0(e))', 598 => 'P5(X,V0(Y)) -> P6(X,V1(Y))', 599 => 'P5(X,V1(Y)) -> P6(X,V0(Y))', 600 => 'P5(e,Y) -> P5(V0(e),Y)', 601 => 'P5(X,e) -> P5(X,V0(e))', 602 => 'P6(X,Y) -> P7(X,Y)', 603 => 'P6(e,Y) -> P6(V0(e),Y)', 604 => 'P6(X,e) -> P6(X,V0(e))', 605 => 'P7(X,V0(Y)) -> P8(V1(X),Y)', 606 => 'P7(X,V1(Y)) -> P8(V0(X),Y)', 607 => 'P7(e,Y) -> P7(V0(e),Y)', 608 => 'P7(X,e) -> P7(X,V0(e))', 609 => 'P8(X,V0(Y)) -> P9(V1(X),Y)', 610 => 'P8(X,V1(Y)) -> P9(V0(X),Y)', 611 => 'P8(e,Y) -> P8(V0(e),Y)', 612 => 'P8(X,e) -> P8(X,V0(e))', 613 => 'P9(X,V0(Y)) -> P6(X,V0(Y))', 614 => 'P9(X,V1(Y)) -> P6(X,V1(Y))', 615 => 'P9(e,Y) -> P9(V0(e),Y)', 616 => 'P9(X,e) -> P9(X,V0(e))', 617 => 'P10(V0(X),Y) -> P11(X,V0(Y))', 618 => 'P10(V1(X),Y) -> P11(X,V1(Y))', 619 => 'P10(e,Y) -> P10(V0(e),Y)', 620 => 'P10(X,e) -> P10(X,V0(e))', 621 => 'P11(X,V0(Y)) -> P12(X,V0(Y))', 622 => 'P11(X,V1(Y)) -> P0(X,V1(Y))', 623 => 'P11(e,Y) -> P11(V0(e),Y)', 624 => 'P11(X,e) -> P11(X,V0(e))', 625 => 'P12(X,Y) -> F', 626 => ')', 627 => '</pre>', 628 => 'Keep in mind, this assumes a empty starting tape.', 629 => '', 630 => '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>', 631 => '', 632 => 'Then run the code here: https://aprove.informatik.rwth-aachen.de/index.php/interface/v-AProVE2023/trs_wst', 633 => '', 634 => 'It will then disprove termination.' ]
Unix timestamp of change (timestamp)
'1744451494'