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.
' |
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.'
] |