Jolverine Turing-completeness proof

Jolverine can be shown Turing complete by a reduction from ternary Reversible Brainfuck. We put the construction on a separate page because of the size of one of its parts.
A ternary Reversible Brainfuck program is converted to Jolverine as a series of diagonal elements concatenated with each other. The first element is the initialization; then follows the elements for the parts of the RB program in order. Loops are considerably more complicated to represent than any of the other RB instructions, and contain their inner instructions embedded within them.
Note that I/O is not needed for theoretical Turing-completeness, and may not have completely matching semantics between all esolangs involved. For best results only use input on a cell containing a zero value.
The following properties are kept for all elements other than initialization (whose job is to set them up in the first place):
*Each element takes a multiple of 7 ticks to execute. Apart from loop elements, this means each of them is a multiple of 7 long.
*Each element starts with the instruction wheel in the state
 left <--
 adddx
 input
 output
 adddy
 rot
 right
:with the top instruction (left) the current one, and with the next executed instruction to be re-inserted at the top.
*Instructions which may turn the IP will only be executed as the sixth instruction on the wheel. This ensures that the wheel sixth instructions are always at 7x7 grid positions in the larger program, thus ensuring there can be no position mismatch not fixable simply by adding a multiple of 7 non-* symbols.
*At the start of an element, the current cell of the Jolverine tape corresponds to the current RB cell. RB cells are spaced two cells apart on the Jolverine tape, with the intermediate cell being zero.
Since editing this stuff has been rather awkward, the reduction has only been tested on one program:
 [>,.]
==Reduction tables==
The following table lists the elements other than loops.
<nowiki>
initialization
==============
..*.*
 . + - > < . ,
 . = = = = = =
 * . . * * . .
 . . . . . . .
 . . . . . . *
 . . . . . . .
 . . . . . . .
 . * * . . * .
 . . . * . . *
 * * * . * * .
 . . . . . . .
 . . . . . . *
 . . . . . . .
 . . . . . . .
 . . . . . . .
 . * . * * * .
 * * * * . . .
 * . . . . . .
 . . . . . . *
 . . . . . . .
 . . . . . * .
 . . * . . * .
 . . . . * . *
 * . .
 . . .
 . . .
 . . .
 . . .
 * * .
 . . *
 .
 .
 *
 .
 .
 .
 .
 .
 .
 *
 .
 .
 .
 *
 *
 .
 .
 .
 .
 .
 .
 *
 *
 .
 .
 .
 .
 .
</nowiki>
The following shows the general structure of the large loop elements. The instructions for the loop contents are embedded at the spot marked "INSIDE LOOP". The surrounding paths must be stretched as necessary by inserting multiples of 7 non-* elements in order to fit the inside content.
(The version below has space enough for the loop [>,.] as that was what it was tested with.)
<nowiki>
 * *
 . . . .
 . * . *
 . . . .
 . . . .
 . . . .
 * . * .
 * . * .
 . * . *
 . . . .
 . . . .
 . . . .
 * . * .
 . . . .
 . * . *
 * . * .
 B . . . .
 E . * . *
 F . . . .
 O * . * .
 R . . . .
 E . . . .
 . * . *
 L . * . *
 O . * . *
 O . . . .
 P * . * .
 , * . * .
 , . . . .
 , . . . .
 . . . . .
 . . * . *
 . . . . .
 . * . * .
 . * . * .
 * . * . .
 . . . . .
 * . * . ,
 . . . . ,
 . . . . ,
 . * . * ,
 . . . . ,
 . . . . ,
 * . * . ,
 . . . . ,
 . . . . ,
 . . . . ,
 . * . * ,
 . . . . ,
 *.*......*.....**.....**......*...*..,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,.....*.*.....*.....* ,
 . . ,
 * . ,
 . . ,
 . . ,
 . . ,
 . * ,
 . . ,
 . . ,
 * . ,
 . . ,
 . . ,
 . * ,
 . . ,
 . * ,
 * . ,
 * . ,
 . . ,
 . . ,
 . . ,
 . , ,
 . , ,
 * , ,
 * , ,
 . , ,
 . , ,
 . , ,
 . , ,
 . , ,
 . , ,
 * , ,
 . , ,
 . , ,
 . , ,
 * , ,
 . , ,
 . , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 . , ,
 . , ,
 * , ,
 . , ,
 . , ,
 . , ,
 * , ,
 . , ,
 . , ,
 . , ,
 . , ,
 . , ,
 . , ,
 * , ,
 * , ,
 . , ,
 . , ,
 . . ,
 . . ,
 . . ,
 * . ,
 * . ,
 . * ,
 . . ,
 . * ,
 . . ,
 . . ,
 * . ,
 . . ,
 . . ,
 . * ,
 . . ,
 . . ,
 . . ,
 * . ,
 . . ,
 *.*......*.....**.....**......*...*..,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,.....*.*.....*.....* ,
 . . . . ,
 . * . * ,
 . . . . ,
 . . . . ,
 . . . . ,
 * . * . ,
 . . . . ,
 . . . . ,
 . * . * ,
 . . . . ,
 . . . . ,
 * . * . ,
 . . . . ,
 * . * . ,
 . * . * ,
 . * . * ,
 * . . . ,
 . . * . ,
 * . * . ,
 . . . . ,
 . . . . ,
 . * . * ,
 . * . * ,
 . . . . ,
 . . . . ,
 * . * . ,
 * . * . ,
 . . . . ,
 . . . . ,
 . * . * ,
 . . . . ,
 . . * . ,
 . . . . ,
 * * . * ,
 . . . . ,
 . * . . ,
 . . . I ,
 * . * N ,
 . . * S ,
 . . . I ,
 * . * D ,
 * . . E ,
 . * . ,
 . . . L ,
 . . . O ,
 . . . O ,
 * . . P ,
 . . * , ,
 * * , ,
 . , ,
 . , ,
 * , ,
 . , ,
 . , ,
 * , ,
 . , ,
 . , ,
 . , *
 . , *
 . , .
 . , *
 , , *
 , , *
 , , *
 , , .
 , , .
 , , .
 , , .
 , , .
 , , .
 , , *
 , , .
 , , .
 , , *
 , , .
 , , .
 , , *
 , , .
 , , .
 , , *
 , , .
 , , .
 , , .
 , , .
 , , *
 , , *
 , , .
 , , *
 , , .
 , , .
 , , .
 , , .
 , , .
 , , *
 , , .
 , , .
 , , .
 , , .
 , , .
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , ,
 , , .
 , , .
 , , .
 , , .
 , , .
 , , .
 , , *
 , * .
 , * .
 , . *
 , * .
 , * .
 , * *
 , * .
 , . *
 , . .
 , . .
 , . .
 , . .
 , . *
 , * *
 , . .
 , . .
 , * *
 , . .
 . . .
 . * .
 . . *
 . . .
 . * .
 * . .
 . . .
 . . .
 . . .
 . * *
 . * *
 . . .
 * * .
 * . .
 * . .
 . . .
 . . .
 . . *
 . * .
 * . *
 . . .
 . . .
 * . .
 . . .
 . * A
 . . F
 . . T
 . . E
 * . R
 . * 
 . * L
 . . O
 . . O
 . . P
 * . ,
 . . ,
 *.....**....*,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,.....*......***....*..*.....*.....*.* ,
 ,
</nowiki>
Category:Proofs