NO

Problem:
 0(x) -> 1(x)
 0(0(x)) -> 0(x)
 3(4(5(x))) -> 4(3(5(x)))
 2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2(2(2(2(2(2(2(2(2(2(x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 ->
 1(1(1(0(1(1(0(0(0(0(0(1(1(0(1(1(1(0(0(1(0(1(1(0(1(1(1(1(0(0(0(1(1(1(
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0(0(0(1(1(0(1(0(0(0(x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 0(0(1(1(1(1(0(0(0(0(0(0(0(0(1(1(0(0(1(1(0(1(1(0(1(0(0(0(1(0(0(0(1(1(
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0(0(1(0(0(1(0(0(1(0(x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 ->
 2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2(2(2(2(2(2(2(2(2(2(x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

Proof:
 sorted: (order-sorted)
 0:3(4(5(x))) -> 4(3(5(x)))
 1:0(x) -> 1(x)
   0(0(x)) -> 0(x)
   2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2(2(2(2(2(2(2(2(2(2(x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
   ->
   1(1(1(0(1(1(0(0(0(0(0(1(1(0(1(1(1(0(0(1(0(1(1(0(1(1(1(1(0(0(0(1(1(
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0(0(0(1(1(0(1(0(0(0(x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
   0(0(1(1(1(1(0(0(0(0(0(0(0(0(1(1(0(0(1(1(0(1(1(0(1(0(0(0(1(0(0(0(1(
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0(0(1(0(0(1(0(0(1(0(x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
   ->
   2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2(2(2(2(2(2(2(2(2(2(x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 -----
 sorts
   [0>1, 1>2]
 sort attachment (non-strict)
   0 : 3 -> 3
   1 : 3 -> 3
   3 : 0 -> 0
   4 : 0 -> 0
   5 : 2 -> 1
   2 : 3 -> 3
 -----
 0:3(4(5(x))) -> 4(3(5(x)))
   Church Rosser Transformation Processor:
    
    critical peaks: joinable
    Qed
 
 
 1:0(x) -> 1(x)
   0(0(x)) -> 0(x)
   2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2(2(2(2(2(2(2(2(2(2(x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
   ->
   1(1(1(0(1(1(0(0(0(0(0(1(1(0(1(1(1(0(0(1(0(1(1(0(1(1(1(1(0(0(0(1(1(
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0(0(0(1(1(0(1(0(0(0(x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
   0(0(1(1(1(1(0(0(0(0(0(0(0(0(1(1(0(0(1(1(0(1(1(0(1(0(0(0(1(0(0(0(1(
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0(0(1(0(0(1(0(0(1(0(x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
   ->
   2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2(2(2(2(2(2(2(2(2(2(x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
   Nonconfluence Processor:
    terms: 2(1(1(1(0(1(1(0(0(0(0(0(1(1(0(1(1(1(0(0(1(0(1(1(0(1(1(1(1(
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0(1(1(0(1(0(0(0(x1788))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) *<- 
    2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2
                                                                    (
                                                                    2(2(2(2(2(2(2(2(x1788)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ->* 
    1(1(1(0(1(1(0(0(0(0(0(1(1(0(1(1(1(0(0(1(0(1(1(0(1(1(1(1(0(0(0(1(1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    1
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    0
                                                                    (
                                                                    1(1(0(1(0(0(0(2(x1788)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
    Qed