YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

0(1(0(1(x0)))) → 0(2(3(1(x0))))
2(1(4(0(1(x0))))) → 3(0(0(1(x0))))
2(3(3(3(1(x0))))) → 1(1(3(1(x0))))
4(1(2(3(4(x0))))) → 1(5(3(0(x0))))
5(3(2(4(4(x0))))) → 0(1(3(0(x0))))
5(5(0(4(3(3(x0)))))) → 0(3(2(1(3(x0)))))
5(0(3(1(4(1(0(1(0(x0))))))))) → 2(2(4(1(3(2(2(3(0(x0)))))))))
5(5(5(4(4(0(4(0(2(1(x0)))))))))) → 5(4(5(4(0(5(0(4(0(3(x0))))))))))
2(2(2(0(3(3(2(0(4(5(0(x0))))))))))) → 0(4(0(0(0(0(2(5(1(x0)))))))))
1(0(2(0(3(5(1(4(5(2(4(4(x0)))))))))))) → 1(0(1(0(3(2(3(2(1(0(3(3(x0))))))))))))
4(0(4(2(3(5(0(1(4(4(5(0(x0)))))))))))) → 3(5(0(2(5(1(2(5(1(4(1(x0)))))))))))
4(1(0(2(3(5(4(1(4(4(1(1(x0)))))))))))) → 2(5(4(4(5(5(1(2(4(4(2(x0)))))))))))
2(0(0(5(5(0(2(2(2(3(4(1(4(x0))))))))))))) → 3(3(3(3(1(3(1(4(1(4(5(4(3(x0)))))))))))))
4(5(1(3(0(0(3(5(2(1(2(5(2(x0))))))))))))) → 4(5(0(3(5(3(5(5(3(5(4(0(4(x0)))))))))))))
2(1(4(5(5(0(2(4(0(5(4(4(1(4(x0)))))))))))))) → 0(0(2(1(4(3(2(5(3(2(5(2(1(x0)))))))))))))
3(1(3(5(4(1(1(4(5(1(1(3(5(1(x0)))))))))))))) → 3(2(1(2(4(3(5(1(5(5(1(3(4(x0)))))))))))))
4(4(5(3(0(2(0(0(0(3(5(0(2(1(x0)))))))))))))) → 2(2(0(4(1(0(0(1(4(2(4(1(3(5(x0))))))))))))))
5(0(5(4(4(4(4(2(5(1(2(3(3(1(1(x0))))))))))))))) → 1(3(0(5(3(1(3(1(0(3(3(1(0(3(x0))))))))))))))
5(3(5(5(4(0(2(2(4(3(2(2(1(4(1(x0))))))))))))))) → 5(1(4(2(3(5(4(0(4(4(2(1(0(0(x0))))))))))))))
5(5(2(1(3(3(2(5(0(1(0(5(0(5(0(x0))))))))))))))) → 2(3(5(0(2(4(1(0(5(4(3(0(5(0(x0))))))))))))))
2(1(2(3(2(1(2(5(5(5(0(0(3(2(1(1(x0)))))))))))))))) → 4(4(1(1(3(3(1(4(2(1(3(0(3(2(3(x0)))))))))))))))
3(3(3(1(4(2(0(0(3(0(1(1(3(4(1(2(x0)))))))))))))))) → 3(0(4(1(5(0(5(3(5(0(4(4(3(0(4(x0)))))))))))))))
2(1(1(3(5(4(0(1(4(2(5(1(4(5(4(5(1(x0))))))))))))))))) → 2(3(3(3(3(2(1(4(5(5(2(2(4(4(4(3(0(x0)))))))))))))))))
5(0(2(4(4(4(4(3(1(2(2(2(2(2(2(5(2(x0))))))))))))))))) → 5(4(0(4(4(3(5(5(4(3(0(5(5(5(0(0(x0))))))))))))))))
2(5(5(1(0(4(4(1(4(0(5(1(1(5(0(0(1(4(x0)))))))))))))))))) → 3(3(1(0(0(1(1(1(2(1(2(0(2(4(4(3(5(0(x0))))))))))))))))))
0(0(1(1(4(5(3(2(5(3(4(4(3(0(5(4(4(4(2(x0))))))))))))))))))) → 0(0(4(5(1(4(1(5(3(0(4(0(3(3(4(0(4(0(4(x0)))))))))))))))))))
1(4(1(4(1(5(2(4(4(3(3(4(5(4(4(1(2(0(2(3(x0)))))))))))))))))))) → 1(2(1(5(0(1(0(4(4(4(2(5(0(1(5(1(1(4(3(3(x0))))))))))))))))))))
2(1(0(0(4(2(5(5(1(3(3(4(3(3(5(5(3(3(5(2(x0)))))))))))))))))))) → 4(4(3(3(5(0(4(2(2(1(1(3(1(5(2(5(2(4(5(x0)))))))))))))))))))
4(2(4(2(4(5(4(5(2(1(5(3(1(0(2(5(2(1(4(2(4(x0))))))))))))))))))))) → 1(5(3(1(5(0(5(2(0(5(4(3(5(2(1(2(5(4(3(2(1(x0)))))))))))))))))))))
5(0(2(1(0(3(4(3(4(1(5(3(3(3(4(2(0(5(5(3(5(x0))))))))))))))))))))) → 3(5(1(1(0(5(4(5(2(1(5(0(4(4(4(3(4(4(1(5(x0))))))))))))))))))))

Proof

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
1(0(1(0(x0)))) → 1(3(2(0(x0))))
1(0(4(1(2(x0))))) → 1(0(0(3(x0))))
1(3(3(3(2(x0))))) → 1(3(1(1(x0))))
4(3(2(1(4(x0))))) → 0(3(5(1(x0))))
4(4(2(3(5(x0))))) → 0(3(1(0(x0))))
3(3(4(0(5(5(x0)))))) → 3(1(2(3(0(x0)))))
0(1(0(1(4(1(3(0(5(x0))))))))) → 0(3(2(2(3(1(4(2(2(x0)))))))))
1(2(0(4(0(4(4(5(5(5(x0)))))))))) → 3(0(4(0(5(0(4(5(4(5(x0))))))))))
0(5(4(0(2(3(3(0(2(2(2(x0))))))))))) → 1(5(2(0(0(0(0(4(0(x0)))))))))
4(4(2(5(4(1(5(3(0(2(0(1(x0)))))))))))) → 3(3(0(1(2(3(2(3(0(1(0(1(x0))))))))))))
0(5(4(4(1(0(5(3(2(4(0(4(x0)))))))))))) → 1(4(1(5(2(1(5(2(0(5(3(x0)))))))))))
1(1(4(4(1(4(5(3(2(0(1(4(x0)))))))))))) → 2(4(4(2(1(5(5(4(4(5(2(x0)))))))))))
4(1(4(3(2(2(2(0(5(5(0(0(2(x0))))))))))))) → 3(4(5(4(1(4(1(3(1(3(3(3(3(x0)))))))))))))
2(5(2(1(2(5(3(0(0(3(1(5(4(x0))))))))))))) → 4(0(4(5(3(5(5(3(5(3(0(5(4(x0)))))))))))))
4(1(4(4(5(0(4(2(0(5(5(4(1(2(x0)))))))))))))) → 1(2(5(2(3(5(2(3(4(1(2(0(0(x0)))))))))))))
1(5(3(1(1(5(4(1(1(4(5(3(1(3(x0)))))))))))))) → 4(3(1(5(5(1(5(3(4(2(1(2(3(x0)))))))))))))
1(2(0(5(3(0(0(0(2(0(3(5(4(4(x0)))))))))))))) → 5(3(1(4(2(4(1(0(0(1(4(0(2(2(x0))))))))))))))
1(1(3(3(2(1(5(2(4(4(4(4(5(0(5(x0))))))))))))))) → 3(0(1(3(3(0(1(3(1(3(5(0(3(1(x0))))))))))))))
1(4(1(2(2(3(4(2(2(0(4(5(5(3(5(x0))))))))))))))) → 0(0(1(2(4(4(0(4(5(3(2(4(1(5(x0))))))))))))))
0(5(0(5(0(1(0(5(2(3(3(1(2(5(5(x0))))))))))))))) → 0(5(0(3(4(5(0(1(4(2(0(5(3(2(x0))))))))))))))
1(1(2(3(0(0(5(5(5(2(1(2(3(2(1(2(x0)))))))))))))))) → 3(2(3(0(3(1(2(4(1(3(3(1(1(4(4(x0)))))))))))))))
2(1(4(3(1(1(0(3(0(0(2(4(1(3(3(3(x0)))))))))))))))) → 4(0(3(4(4(0(5(3(5(0(5(1(4(0(3(x0)))))))))))))))
1(5(4(5(4(1(5(2(4(1(0(4(5(3(1(1(2(x0))))))))))))))))) → 0(3(4(4(4(2(2(5(5(4(1(2(3(3(3(3(2(x0)))))))))))))))))
2(5(2(2(2(2(2(2(1(3(4(4(4(4(2(0(5(x0))))))))))))))))) → 0(0(5(5(5(0(3(4(5(5(3(4(4(0(4(5(x0))))))))))))))))
4(1(0(0(5(1(1(5(0(4(1(4(4(0(1(5(5(2(x0)))))))))))))))))) → 0(5(3(4(4(2(0(2(1(2(1(1(1(0(0(1(3(3(x0))))))))))))))))))
2(4(4(4(5(0(3(4(4(3(5(2(3(5(4(1(1(0(0(x0))))))))))))))))))) → 4(0(4(0(4(3(3(0(4(0(3(5(1(4(1(5(4(0(0(x0)))))))))))))))))))
3(2(0(2(1(4(4(5(4(3(3(4(4(2(5(1(4(1(4(1(x0)))))))))))))))))))) → 3(3(4(1(1(5(1(0(5(2(4(4(4(0(1(0(5(1(2(1(x0))))))))))))))))))))
2(5(3(3(5(5(3(3(4(3(3(1(5(5(2(4(0(0(1(2(x0)))))))))))))))))))) → 5(4(2(5(2(5(1(3(1(1(2(2(4(0(5(3(3(4(4(x0)))))))))))))))))))
4(2(4(1(2(5(2(0(1(3(5(1(2(5(4(5(4(2(4(2(4(x0))))))))))))))))))))) → 1(2(3(4(5(2(1(2(5(3(4(5(0(2(5(0(5(1(3(5(1(x0)))))))))))))))))))))
5(3(5(5(0(2(4(3(3(3(5(1(4(3(4(3(0(1(2(0(5(x0))))))))))))))))))))) → 5(1(4(4(3(4(4(4(0(5(1(2(5(4(5(0(1(1(5(3(x0))))))))))))))))))))

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
1#(0(1(0(x0)))) → 2#(0(x0))
1#(0(1(0(x0)))) → 3#(2(0(x0)))
1#(0(1(0(x0)))) → 1#(3(2(0(x0))))
1#(0(4(1(2(x0))))) → 3#(x0)
1#(0(4(1(2(x0))))) → 0#(3(x0))
1#(0(4(1(2(x0))))) → 0#(0(3(x0)))
1#(0(4(1(2(x0))))) → 1#(0(0(3(x0))))
1#(3(3(3(2(x0))))) → 1#(x0)
1#(3(3(3(2(x0))))) → 1#(1(x0))
1#(3(3(3(2(x0))))) → 3#(1(1(x0)))
1#(3(3(3(2(x0))))) → 1#(3(1(1(x0))))
4#(3(2(1(4(x0))))) → 1#(x0)
4#(3(2(1(4(x0))))) → 5#(1(x0))
4#(3(2(1(4(x0))))) → 3#(5(1(x0)))
4#(3(2(1(4(x0))))) → 0#(3(5(1(x0))))
4#(4(2(3(5(x0))))) → 0#(x0)
4#(4(2(3(5(x0))))) → 1#(0(x0))
4#(4(2(3(5(x0))))) → 3#(1(0(x0)))
4#(4(2(3(5(x0))))) → 0#(3(1(0(x0))))
3#(3(4(0(5(5(x0)))))) → 0#(x0)
3#(3(4(0(5(5(x0)))))) → 3#(0(x0))
3#(3(4(0(5(5(x0)))))) → 2#(3(0(x0)))
3#(3(4(0(5(5(x0)))))) → 1#(2(3(0(x0))))
3#(3(4(0(5(5(x0)))))) → 3#(1(2(3(0(x0)))))
0#(1(0(1(4(1(3(0(5(x0))))))))) → 2#(x0)
0#(1(0(1(4(1(3(0(5(x0))))))))) → 2#(2(x0))
0#(1(0(1(4(1(3(0(5(x0))))))))) → 4#(2(2(x0)))
0#(1(0(1(4(1(3(0(5(x0))))))))) → 1#(4(2(2(x0))))
0#(1(0(1(4(1(3(0(5(x0))))))))) → 3#(1(4(2(2(x0)))))
0#(1(0(1(4(1(3(0(5(x0))))))))) → 2#(3(1(4(2(2(x0))))))
0#(1(0(1(4(1(3(0(5(x0))))))))) → 2#(2(3(1(4(2(2(x0)))))))
0#(1(0(1(4(1(3(0(5(x0))))))))) → 3#(2(2(3(1(4(2(2(x0))))))))
0#(1(0(1(4(1(3(0(5(x0))))))))) → 0#(3(2(2(3(1(4(2(2(x0)))))))))
1#(2(0(4(0(4(4(5(5(5(x0)))))))))) → 4#(5(x0))
1#(2(0(4(0(4(4(5(5(5(x0)))))))))) → 5#(4(5(x0)))
1#(2(0(4(0(4(4(5(5(5(x0)))))))))) → 4#(5(4(5(x0))))
1#(2(0(4(0(4(4(5(5(5(x0)))))))))) → 0#(4(5(4(5(x0)))))
1#(2(0(4(0(4(4(5(5(5(x0)))))))))) → 5#(0(4(5(4(5(x0))))))
1#(2(0(4(0(4(4(5(5(5(x0)))))))))) → 0#(5(0(4(5(4(5(x0)))))))
1#(2(0(4(0(4(4(5(5(5(x0)))))))))) → 4#(0(5(0(4(5(4(5(x0))))))))
1#(2(0(4(0(4(4(5(5(5(x0)))))))))) → 0#(4(0(5(0(4(5(4(5(x0)))))))))
1#(2(0(4(0(4(4(5(5(5(x0)))))))))) → 3#(0(4(0(5(0(4(5(4(5(x0))))))))))
0#(5(4(0(2(3(3(0(2(2(2(x0))))))))))) → 0#(x0)
0#(5(4(0(2(3(3(0(2(2(2(x0))))))))))) → 4#(0(x0))
0#(5(4(0(2(3(3(0(2(2(2(x0))))))))))) → 0#(4(0(x0)))
0#(5(4(0(2(3(3(0(2(2(2(x0))))))))))) → 0#(0(4(0(x0))))
0#(5(4(0(2(3(3(0(2(2(2(x0))))))))))) → 0#(0(0(4(0(x0)))))
0#(5(4(0(2(3(3(0(2(2(2(x0))))))))))) → 0#(0(0(0(4(0(x0))))))
0#(5(4(0(2(3(3(0(2(2(2(x0))))))))))) → 2#(0(0(0(0(4(0(x0)))))))
0#(5(4(0(2(3(3(0(2(2(2(x0))))))))))) → 5#(2(0(0(0(0(4(0(x0))))))))
0#(5(4(0(2(3(3(0(2(2(2(x0))))))))))) → 1#(5(2(0(0(0(0(4(0(x0)))))))))
4#(4(2(5(4(1(5(3(0(2(0(1(x0)))))))))))) → 1#(0(1(x0)))
4#(4(2(5(4(1(5(3(0(2(0(1(x0)))))))))))) → 0#(1(0(1(x0))))
4#(4(2(5(4(1(5(3(0(2(0(1(x0)))))))))))) → 3#(0(1(0(1(x0)))))
4#(4(2(5(4(1(5(3(0(2(0(1(x0)))))))))))) → 2#(3(0(1(0(1(x0))))))
4#(4(2(5(4(1(5(3(0(2(0(1(x0)))))))))))) → 3#(2(3(0(1(0(1(x0)))))))
4#(4(2(5(4(1(5(3(0(2(0(1(x0)))))))))))) → 2#(3(2(3(0(1(0(1(x0))))))))
4#(4(2(5(4(1(5(3(0(2(0(1(x0)))))))))))) → 1#(2(3(2(3(0(1(0(1(x0)))))))))
4#(4(2(5(4(1(5(3(0(2(0(1(x0)))))))))))) → 0#(1(2(3(2(3(0(1(0(1(x0))))))))))
4#(4(2(5(4(1(5(3(0(2(0(1(x0)))))))))))) → 3#(0(1(2(3(2(3(0(1(0(1(x0)))))))))))
4#(4(2(5(4(1(5(3(0(2(0(1(x0)))))))))))) → 3#(3(0(1(2(3(2(3(0(1(0(1(x0))))))))))))
0#(5(4(4(1(0(5(3(2(4(0(4(x0)))))))))))) → 3#(x0)
0#(5(4(4(1(0(5(3(2(4(0(4(x0)))))))))))) → 5#(3(x0))
0#(5(4(4(1(0(5(3(2(4(0(4(x0)))))))))))) → 0#(5(3(x0)))
0#(5(4(4(1(0(5(3(2(4(0(4(x0)))))))))))) → 2#(0(5(3(x0))))
0#(5(4(4(1(0(5(3(2(4(0(4(x0)))))))))))) → 5#(2(0(5(3(x0)))))
0#(5(4(4(1(0(5(3(2(4(0(4(x0)))))))))))) → 1#(5(2(0(5(3(x0))))))
0#(5(4(4(1(0(5(3(2(4(0(4(x0)))))))))))) → 2#(1(5(2(0(5(3(x0)))))))
0#(5(4(4(1(0(5(3(2(4(0(4(x0)))))))))))) → 5#(2(1(5(2(0(5(3(x0))))))))
0#(5(4(4(1(0(5(3(2(4(0(4(x0)))))))))))) → 1#(5(2(1(5(2(0(5(3(x0)))))))))
0#(5(4(4(1(0(5(3(2(4(0(4(x0)))))))))))) → 4#(1(5(2(1(5(2(0(5(3(x0))))))))))
0#(5(4(4(1(0(5(3(2(4(0(4(x0)))))))))))) → 1#(4(1(5(2(1(5(2(0(5(3(x0)))))))))))
1#(1(4(4(1(4(5(3(2(0(1(4(x0)))))))))))) → 2#(x0)
1#(1(4(4(1(4(5(3(2(0(1(4(x0)))))))))))) → 5#(2(x0))
1#(1(4(4(1(4(5(3(2(0(1(4(x0)))))))))))) → 4#(5(2(x0)))
1#(1(4(4(1(4(5(3(2(0(1(4(x0)))))))))))) → 4#(4(5(2(x0))))
1#(1(4(4(1(4(5(3(2(0(1(4(x0)))))))))))) → 5#(4(4(5(2(x0)))))
1#(1(4(4(1(4(5(3(2(0(1(4(x0)))))))))))) → 5#(5(4(4(5(2(x0))))))
1#(1(4(4(1(4(5(3(2(0(1(4(x0)))))))))))) → 1#(5(5(4(4(5(2(x0)))))))
1#(1(4(4(1(4(5(3(2(0(1(4(x0)))))))))))) → 2#(1(5(5(4(4(5(2(x0))))))))
1#(1(4(4(1(4(5(3(2(0(1(4(x0)))))))))))) → 4#(2(1(5(5(4(4(5(2(x0)))))))))
1#(1(4(4(1(4(5(3(2(0(1(4(x0)))))))))))) → 4#(4(2(1(5(5(4(4(5(2(x0))))))))))
1#(1(4(4(1(4(5(3(2(0(1(4(x0)))))))))))) → 2#(4(4(2(1(5(5(4(4(5(2(x0)))))))))))
4#(1(4(3(2(2(2(0(5(5(0(0(2(x0))))))))))))) → 3#(x0)
4#(1(4(3(2(2(2(0(5(5(0(0(2(x0))))))))))))) → 3#(3(x0))
4#(1(4(3(2(2(2(0(5(5(0(0(2(x0))))))))))))) → 3#(3(3(x0)))
4#(1(4(3(2(2(2(0(5(5(0(0(2(x0))))))))))))) → 3#(3(3(3(x0))))
4#(1(4(3(2(2(2(0(5(5(0(0(2(x0))))))))))))) → 1#(3(3(3(3(x0)))))
4#(1(4(3(2(2(2(0(5(5(0(0(2(x0))))))))))))) → 3#(1(3(3(3(3(x0))))))
4#(1(4(3(2(2(2(0(5(5(0(0(2(x0))))))))))))) → 1#(3(1(3(3(3(3(x0)))))))
4#(1(4(3(2(2(2(0(5(5(0(0(2(x0))))))))))))) → 4#(1(3(1(3(3(3(3(x0))))))))
4#(1(4(3(2(2(2(0(5(5(0(0(2(x0))))))))))))) → 1#(4(1(3(1(3(3(3(3(x0)))))))))
4#(1(4(3(2(2(2(0(5(5(0(0(2(x0))))))))))))) → 4#(1(4(1(3(1(3(3(3(3(x0))))))))))
4#(1(4(3(2(2(2(0(5(5(0(0(2(x0))))))))))))) → 5#(4(1(4(1(3(1(3(3(3(3(x0)))))))))))
4#(1(4(3(2(2(2(0(5(5(0(0(2(x0))))))))))))) → 4#(5(4(1(4(1(3(1(3(3(3(3(x0))))))))))))
4#(1(4(3(2(2(2(0(5(5(0(0(2(x0))))))))))))) → 3#(4(5(4(1(4(1(3(1(3(3(3(3(x0)))))))))))))
2#(5(2(1(2(5(3(0(0(3(1(5(4(x0))))))))))))) → 0#(5(4(x0)))
2#(5(2(1(2(5(3(0(0(3(1(5(4(x0))))))))))))) → 3#(0(5(4(x0))))
2#(5(2(1(2(5(3(0(0(3(1(5(4(x0))))))))))))) → 5#(3(0(5(4(x0)))))
2#(5(2(1(2(5(3(0(0(3(1(5(4(x0))))))))))))) → 3#(5(3(0(5(4(x0))))))
2#(5(2(1(2(5(3(0(0(3(1(5(4(x0))))))))))))) → 5#(3(5(3(0(5(4(x0)))))))
2#(5(2(1(2(5(3(0(0(3(1(5(4(x0))))))))))))) → 5#(5(3(5(3(0(5(4(x0))))))))
2#(5(2(1(2(5(3(0(0(3(1(5(4(x0))))))))))))) → 3#(5(5(3(5(3(0(5(4(x0)))))))))
2#(5(2(1(2(5(3(0(0(3(1(5(4(x0))))))))))))) → 5#(3(5(5(3(5(3(0(5(4(x0))))))))))
2#(5(2(1(2(5(3(0(0(3(1(5(4(x0))))))))))))) → 4#(5(3(5(5(3(5(3(0(5(4(x0)))))))))))
2#(5(2(1(2(5(3(0(0(3(1(5(4(x0))))))))))))) → 0#(4(5(3(5(5(3(5(3(0(5(4(x0))))))))))))
2#(5(2(1(2(5(3(0(0(3(1(5(4(x0))))))))))))) → 4#(0(4(5(3(5(5(3(5(3(0(5(4(x0)))))))))))))
4#(1(4(4(5(0(4(2(0(5(5(4(1(2(x0)))))))))))))) → 0#(x0)
4#(1(4(4(5(0(4(2(0(5(5(4(1(2(x0)))))))))))))) → 0#(0(x0))
4#(1(4(4(5(0(4(2(0(5(5(4(1(2(x0)))))))))))))) → 2#(0(0(x0)))
4#(1(4(4(5(0(4(2(0(5(5(4(1(2(x0)))))))))))))) → 1#(2(0(0(x0))))
4#(1(4(4(5(0(4(2(0(5(5(4(1(2(x0)))))))))))))) → 4#(1(2(0(0(x0)))))
4#(1(4(4(5(0(4(2(0(5(5(4(1(2(x0)))))))))))))) → 3#(4(1(2(0(0(x0))))))
4#(1(4(4(5(0(4(2(0(5(5(4(1(2(x0)))))))))))))) → 2#(3(4(1(2(0(0(x0)))))))
4#(1(4(4(5(0(4(2(0(5(5(4(1(2(x0)))))))))))))) → 5#(2(3(4(1(2(0(0(x0))))))))
4#(1(4(4(5(0(4(2(0(5(5(4(1(2(x0)))))))))))))) → 3#(5(2(3(4(1(2(0(0(x0)))))))))
4#(1(4(4(5(0(4(2(0(5(5(4(1(2(x0)))))))))))))) → 2#(3(5(2(3(4(1(2(0(0(x0))))))))))
4#(1(4(4(5(0(4(2(0(5(5(4(1(2(x0)))))))))))))) → 5#(2(3(5(2(3(4(1(2(0(0(x0)))))))))))
4#(1(4(4(5(0(4(2(0(5(5(4(1(2(x0)))))))))))))) → 2#(5(2(3(5(2(3(4(1(2(0(0(x0))))))))))))
4#(1(4(4(5(0(4(2(0(5(5(4(1(2(x0)))))))))))))) → 1#(2(5(2(3(5(2(3(4(1(2(0(0(x0)))))))))))))
1#(5(3(1(1(5(4(1(1(4(5(3(1(3(x0)))))))))))))) → 2#(3(x0))
1#(5(3(1(1(5(4(1(1(4(5(3(1(3(x0)))))))))))))) → 1#(2(3(x0)))
1#(5(3(1(1(5(4(1(1(4(5(3(1(3(x0)))))))))))))) → 2#(1(2(3(x0))))
1#(5(3(1(1(5(4(1(1(4(5(3(1(3(x0)))))))))))))) → 4#(2(1(2(3(x0)))))
1#(5(3(1(1(5(4(1(1(4(5(3(1(3(x0)))))))))))))) → 3#(4(2(1(2(3(x0))))))
1#(5(3(1(1(5(4(1(1(4(5(3(1(3(x0)))))))))))))) → 5#(3(4(2(1(2(3(x0)))))))
1#(5(3(1(1(5(4(1(1(4(5(3(1(3(x0)))))))))))))) → 1#(5(3(4(2(1(2(3(x0))))))))
1#(5(3(1(1(5(4(1(1(4(5(3(1(3(x0)))))))))))))) → 5#(1(5(3(4(2(1(2(3(x0)))))))))
1#(5(3(1(1(5(4(1(1(4(5(3(1(3(x0)))))))))))))) → 5#(5(1(5(3(4(2(1(2(3(x0))))))))))
1#(5(3(1(1(5(4(1(1(4(5(3(1(3(x0)))))))))))))) → 1#(5(5(1(5(3(4(2(1(2(3(x0)))))))))))
1#(5(3(1(1(5(4(1(1(4(5(3(1(3(x0)))))))))))))) → 3#(1(5(5(1(5(3(4(2(1(2(3(x0))))))))))))
1#(5(3(1(1(5(4(1(1(4(5(3(1(3(x0)))))))))))))) → 4#(3(1(5(5(1(5(3(4(2(1(2(3(x0)))))))))))))
1#(2(0(5(3(0(0(0(2(0(3(5(4(4(x0)))))))))))))) → 2#(x0)
1#(2(0(5(3(0(0(0(2(0(3(5(4(4(x0)))))))))))))) → 2#(2(x0))
1#(2(0(5(3(0(0(0(2(0(3(5(4(4(x0)))))))))))))) → 0#(2(2(x0)))
1#(2(0(5(3(0(0(0(2(0(3(5(4(4(x0)))))))))))))) → 4#(0(2(2(x0))))
1#(2(0(5(3(0(0(0(2(0(3(5(4(4(x0)))))))))))))) → 1#(4(0(2(2(x0)))))
1#(2(0(5(3(0(0(0(2(0(3(5(4(4(x0)))))))))))))) → 0#(1(4(0(2(2(x0))))))
1#(2(0(5(3(0(0(0(2(0(3(5(4(4(x0)))))))))))))) → 0#(0(1(4(0(2(2(x0)))))))
1#(2(0(5(3(0(0(0(2(0(3(5(4(4(x0)))))))))))))) → 1#(0(0(1(4(0(2(2(x0))))))))
1#(2(0(5(3(0(0(0(2(0(3(5(4(4(x0)))))))))))))) → 4#(1(0(0(1(4(0(2(2(x0)))))))))
1#(2(0(5(3(0(0(0(2(0(3(5(4(4(x0)))))))))))))) → 2#(4(1(0(0(1(4(0(2(2(x0))))))))))
1#(2(0(5(3(0(0(0(2(0(3(5(4(4(x0)))))))))))))) → 4#(2(4(1(0(0(1(4(0(2(2(x0)))))))))))
1#(2(0(5(3(0(0(0(2(0(3(5(4(4(x0)))))))))))))) → 1#(4(2(4(1(0(0(1(4(0(2(2(x0))))))))))))
1#(2(0(5(3(0(0(0(2(0(3(5(4(4(x0)))))))))))))) → 3#(1(4(2(4(1(0(0(1(4(0(2(2(x0)))))))))))))
1#(2(0(5(3(0(0(0(2(0(3(5(4(4(x0)))))))))))))) → 5#(3(1(4(2(4(1(0(0(1(4(0(2(2(x0))))))))))))))
1#(1(3(3(2(1(5(2(4(4(4(4(5(0(5(x0))))))))))))))) → 1#(x0)
1#(1(3(3(2(1(5(2(4(4(4(4(5(0(5(x0))))))))))))))) → 3#(1(x0))
1#(1(3(3(2(1(5(2(4(4(4(4(5(0(5(x0))))))))))))))) → 0#(3(1(x0)))
1#(1(3(3(2(1(5(2(4(4(4(4(5(0(5(x0))))))))))))))) → 5#(0(3(1(x0))))
1#(1(3(3(2(1(5(2(4(4(4(4(5(0(5(x0))))))))))))))) → 3#(5(0(3(1(x0)))))
1#(1(3(3(2(1(5(2(4(4(4(4(5(0(5(x0))))))))))))))) → 1#(3(5(0(3(1(x0))))))
1#(1(3(3(2(1(5(2(4(4(4(4(5(0(5(x0))))))))))))))) → 3#(1(3(5(0(3(1(x0)))))))
1#(1(3(3(2(1(5(2(4(4(4(4(5(0(5(x0))))))))))))))) → 1#(3(1(3(5(0(3(1(x0))))))))
1#(1(3(3(2(1(5(2(4(4(4(4(5(0(5(x0))))))))))))))) → 0#(1(3(1(3(5(0(3(1(x0)))))))))
1#(1(3(3(2(1(5(2(4(4(4(4(5(0(5(x0))))))))))))))) → 3#(0(1(3(1(3(5(0(3(1(x0))))))))))
1#(1(3(3(2(1(5(2(4(4(4(4(5(0(5(x0))))))))))))))) → 3#(3(0(1(3(1(3(5(0(3(1(x0)))))))))))
1#(1(3(3(2(1(5(2(4(4(4(4(5(0(5(x0))))))))))))))) → 1#(3(3(0(1(3(1(3(5(0(3(1(x0))))))))))))
1#(1(3(3(2(1(5(2(4(4(4(4(5(0(5(x0))))))))))))))) → 0#(1(3(3(0(1(3(1(3(5(0(3(1(x0)))))))))))))
1#(1(3(3(2(1(5(2(4(4(4(4(5(0(5(x0))))))))))))))) → 3#(0(1(3(3(0(1(3(1(3(5(0(3(1(x0))))))))))))))
1#(4(1(2(2(3(4(2(2(0(4(5(5(3(5(x0))))))))))))))) → 1#(5(x0))
1#(4(1(2(2(3(4(2(2(0(4(5(5(3(5(x0))))))))))))))) → 4#(1(5(x0)))
1#(4(1(2(2(3(4(2(2(0(4(5(5(3(5(x0))))))))))))))) → 2#(4(1(5(x0))))
1#(4(1(2(2(3(4(2(2(0(4(5(5(3(5(x0))))))))))))))) → 3#(2(4(1(5(x0)))))
1#(4(1(2(2(3(4(2(2(0(4(5(5(3(5(x0))))))))))))))) → 5#(3(2(4(1(5(x0))))))
1#(4(1(2(2(3(4(2(2(0(4(5(5(3(5(x0))))))))))))))) → 4#(5(3(2(4(1(5(x0)))))))
1#(4(1(2(2(3(4(2(2(0(4(5(5(3(5(x0))))))))))))))) → 0#(4(5(3(2(4(1(5(x0))))))))
1#(4(1(2(2(3(4(2(2(0(4(5(5(3(5(x0))))))))))))))) → 4#(0(4(5(3(2(4(1(5(x0)))))))))
1#(4(1(2(2(3(4(2(2(0(4(5(5(3(5(x0))))))))))))))) → 4#(4(0(4(5(3(2(4(1(5(x0))))))))))
1#(4(1(2(2(3(4(2(2(0(4(5(5(3(5(x0))))))))))))))) → 2#(4(4(0(4(5(3(2(4(1(5(x0)))))))))))
1#(4(1(2(2(3(4(2(2(0(4(5(5(3(5(x0))))))))))))))) → 1#(2(4(4(0(4(5(3(2(4(1(5(x0))))))))))))
1#(4(1(2(2(3(4(2(2(0(4(5(5(3(5(x0))))))))))))))) → 0#(1(2(4(4(0(4(5(3(2(4(1(5(x0)))))))))))))
1#(4(1(2(2(3(4(2(2(0(4(5(5(3(5(x0))))))))))))))) → 0#(0(1(2(4(4(0(4(5(3(2(4(1(5(x0))))))))))))))
0#(5(0(5(0(1(0(5(2(3(3(1(2(5(5(x0))))))))))))))) → 2#(x0)
0#(5(0(5(0(1(0(5(2(3(3(1(2(5(5(x0))))))))))))))) → 3#(2(x0))
0#(5(0(5(0(1(0(5(2(3(3(1(2(5(5(x0))))))))))))))) → 5#(3(2(x0)))
0#(5(0(5(0(1(0(5(2(3(3(1(2(5(5(x0))))))))))))))) → 0#(5(3(2(x0))))
0#(5(0(5(0(1(0(5(2(3(3(1(2(5(5(x0))))))))))))))) → 2#(0(5(3(2(x0)))))
0#(5(0(5(0(1(0(5(2(3(3(1(2(5(5(x0))))))))))))))) → 4#(2(0(5(3(2(x0))))))
0#(5(0(5(0(1(0(5(2(3(3(1(2(5(5(x0))))))))))))))) → 1#(4(2(0(5(3(2(x0)))))))
0#(5(0(5(0(1(0(5(2(3(3(1(2(5(5(x0))))))))))))))) → 0#(1(4(2(0(5(3(2(x0))))))))
0#(5(0(5(0(1(0(5(2(3(3(1(2(5(5(x0))))))))))))))) → 5#(0(1(4(2(0(5(3(2(x0)))))))))
0#(5(0(5(0(1(0(5(2(3(3(1(2(5(5(x0))))))))))))))) → 4#(5(0(1(4(2(0(5(3(2(x0))))))))))
0#(5(0(5(0(1(0(5(2(3(3(1(2(5(5(x0))))))))))))))) → 3#(4(5(0(1(4(2(0(5(3(2(x0)))))))))))
0#(5(0(5(0(1(0(5(2(3(3(1(2(5(5(x0))))))))))))))) → 0#(3(4(5(0(1(4(2(0(5(3(2(x0))))))))))))
0#(5(0(5(0(1(0(5(2(3(3(1(2(5(5(x0))))))))))))))) → 5#(0(3(4(5(0(1(4(2(0(5(3(2(x0)))))))))))))
0#(5(0(5(0(1(0(5(2(3(3(1(2(5(5(x0))))))))))))))) → 0#(5(0(3(4(5(0(1(4(2(0(5(3(2(x0))))))))))))))
1#(1(2(3(0(0(5(5(5(2(1(2(3(2(1(2(x0)))))))))))))))) → 4#(x0)
1#(1(2(3(0(0(5(5(5(2(1(2(3(2(1(2(x0)))))))))))))))) → 4#(4(x0))
1#(1(2(3(0(0(5(5(5(2(1(2(3(2(1(2(x0)))))))))))))))) → 1#(4(4(x0)))
1#(1(2(3(0(0(5(5(5(2(1(2(3(2(1(2(x0)))))))))))))))) → 1#(1(4(4(x0))))
1#(1(2(3(0(0(5(5(5(2(1(2(3(2(1(2(x0)))))))))))))))) → 3#(1(1(4(4(x0)))))
1#(1(2(3(0(0(5(5(5(2(1(2(3(2(1(2(x0)))))))))))))))) → 3#(3(1(1(4(4(x0))))))
1#(1(2(3(0(0(5(5(5(2(1(2(3(2(1(2(x0)))))))))))))))) → 1#(3(3(1(1(4(4(x0)))))))
1#(1(2(3(0(0(5(5(5(2(1(2(3(2(1(2(x0)))))))))))))))) → 4#(1(3(3(1(1(4(4(x0))))))))
1#(1(2(3(0(0(5(5(5(2(1(2(3(2(1(2(x0)))))))))))))))) → 2#(4(1(3(3(1(1(4(4(x0)))))))))
1#(1(2(3(0(0(5(5(5(2(1(2(3(2(1(2(x0)))))))))))))))) → 1#(2(4(1(3(3(1(1(4(4(x0))))))))))
1#(1(2(3(0(0(5(5(5(2(1(2(3(2(1(2(x0)))))))))))))))) → 3#(1(2(4(1(3(3(1(1(4(4(x0)))))))))))
1#(1(2(3(0(0(5(5(5(2(1(2(3(2(1(2(x0)))))))))))))))) → 0#(3(1(2(4(1(3(3(1(1(4(4(x0))))))))))))
1#(1(2(3(0(0(5(5(5(2(1(2(3(2(1(2(x0)))))))))))))))) → 3#(0(3(1(2(4(1(3(3(1(1(4(4(x0)))))))))))))
1#(1(2(3(0(0(5(5(5(2(1(2(3(2(1(2(x0)))))))))))))))) → 2#(3(0(3(1(2(4(1(3(3(1(1(4(4(x0))))))))))))))
1#(1(2(3(0(0(5(5(5(2(1(2(3(2(1(2(x0)))))))))))))))) → 3#(2(3(0(3(1(2(4(1(3(3(1(1(4(4(x0)))))))))))))))
2#(1(4(3(1(1(0(3(0(0(2(4(1(3(3(3(x0)))))))))))))))) → 0#(3(x0))
2#(1(4(3(1(1(0(3(0(0(2(4(1(3(3(3(x0)))))))))))))))) → 4#(0(3(x0)))
2#(1(4(3(1(1(0(3(0(0(2(4(1(3(3(3(x0)))))))))))))))) → 1#(4(0(3(x0))))
2#(1(4(3(1(1(0(3(0(0(2(4(1(3(3(3(x0)))))))))))))))) → 5#(1(4(0(3(x0)))))
2#(1(4(3(1(1(0(3(0(0(2(4(1(3(3(3(x0)))))))))))))))) → 0#(5(1(4(0(3(x0))))))
2#(1(4(3(1(1(0(3(0(0(2(4(1(3(3(3(x0)))))))))))))))) → 5#(0(5(1(4(0(3(x0)))))))
2#(1(4(3(1(1(0(3(0(0(2(4(1(3(3(3(x0)))))))))))))))) → 3#(5(0(5(1(4(0(3(x0))))))))
2#(1(4(3(1(1(0(3(0(0(2(4(1(3(3(3(x0)))))))))))))))) → 5#(3(5(0(5(1(4(0(3(x0)))))))))
2#(1(4(3(1(1(0(3(0(0(2(4(1(3(3(3(x0)))))))))))))))) → 0#(5(3(5(0(5(1(4(0(3(x0))))))))))
2#(1(4(3(1(1(0(3(0(0(2(4(1(3(3(3(x0)))))))))))))))) → 4#(0(5(3(5(0(5(1(4(0(3(x0)))))))))))
2#(1(4(3(1(1(0(3(0(0(2(4(1(3(3(3(x0)))))))))))))))) → 4#(4(0(5(3(5(0(5(1(4(0(3(x0))))))))))))
2#(1(4(3(1(1(0(3(0(0(2(4(1(3(3(3(x0)))))))))))))))) → 3#(4(4(0(5(3(5(0(5(1(4(0(3(x0)))))))))))))
2#(1(4(3(1(1(0(3(0(0(2(4(1(3(3(3(x0)))))))))))))))) → 0#(3(4(4(0(5(3(5(0(5(1(4(0(3(x0))))))))))))))
2#(1(4(3(1(1(0(3(0(0(2(4(1(3(3(3(x0)))))))))))))))) → 4#(0(3(4(4(0(5(3(5(0(5(1(4(0(3(x0)))))))))))))))
1#(5(4(5(4(1(5(2(4(1(0(4(5(3(1(1(2(x0))))))))))))))))) → 3#(2(x0))
1#(5(4(5(4(1(5(2(4(1(0(4(5(3(1(1(2(x0))))))))))))))))) → 3#(3(2(x0)))
1#(5(4(5(4(1(5(2(4(1(0(4(5(3(1(1(2(x0))))))))))))))))) → 3#(3(3(2(x0))))
1#(5(4(5(4(1(5(2(4(1(0(4(5(3(1(1(2(x0))))))))))))))))) → 3#(3(3(3(2(x0)))))
1#(5(4(5(4(1(5(2(4(1(0(4(5(3(1(1(2(x0))))))))))))))))) → 2#(3(3(3(3(2(x0))))))
1#(5(4(5(4(1(5(2(4(1(0(4(5(3(1(1(2(x0))))))))))))))))) → 1#(2(3(3(3(3(2(x0)))))))
1#(5(4(5(4(1(5(2(4(1(0(4(5(3(1(1(2(x0))))))))))))))))) → 4#(1(2(3(3(3(3(2(x0))))))))
1#(5(4(5(4(1(5(2(4(1(0(4(5(3(1(1(2(x0))))))))))))))))) → 5#(4(1(2(3(3(3(3(2(x0)))))))))
1#(5(4(5(4(1(5(2(4(1(0(4(5(3(1(1(2(x0))))))))))))))))) → 5#(5(4(1(2(3(3(3(3(2(x0))))))))))
1#(5(4(5(4(1(5(2(4(1(0(4(5(3(1(1(2(x0))))))))))))))))) → 2#(5(5(4(1(2(3(3(3(3(2(x0)))))))))))
1#(5(4(5(4(1(5(2(4(1(0(4(5(3(1(1(2(x0))))))))))))))))) → 2#(2(5(5(4(1(2(3(3(3(3(2(x0))))))))))))
1#(5(4(5(4(1(5(2(4(1(0(4(5(3(1(1(2(x0))))))))))))))))) → 4#(2(2(5(5(4(1(2(3(3(3(3(2(x0)))))))))))))
1#(5(4(5(4(1(5(2(4(1(0(4(5(3(1(1(2(x0))))))))))))))))) → 4#(4(2(2(5(5(4(1(2(3(3(3(3(2(x0))))))))))))))
1#(5(4(5(4(1(5(2(4(1(0(4(5(3(1(1(2(x0))))))))))))))))) → 4#(4(4(2(2(5(5(4(1(2(3(3(3(3(2(x0)))))))))))))))
1#(5(4(5(4(1(5(2(4(1(0(4(5(3(1(1(2(x0))))))))))))))))) → 3#(4(4(4(2(2(5(5(4(1(2(3(3(3(3(2(x0))))))))))))))))
1#(5(4(5(4(1(5(2(4(1(0(4(5(3(1(1(2(x0))))))))))))))))) → 0#(3(4(4(4(2(2(5(5(4(1(2(3(3(3(3(2(x0)))))))))))))))))
2#(5(2(2(2(2(2(2(1(3(4(4(4(4(2(0(5(x0))))))))))))))))) → 4#(5(x0))
2#(5(2(2(2(2(2(2(1(3(4(4(4(4(2(0(5(x0))))))))))))))))) → 0#(4(5(x0)))
2#(5(2(2(2(2(2(2(1(3(4(4(4(4(2(0(5(x0))))))))))))))))) → 4#(0(4(5(x0))))
2#(5(2(2(2(2(2(2(1(3(4(4(4(4(2(0(5(x0))))))))))))))))) → 4#(4(0(4(5(x0)))))
2#(5(2(2(2(2(2(2(1(3(4(4(4(4(2(0(5(x0))))))))))))))))) → 3#(4(4(0(4(5(x0))))))
2#(5(2(2(2(2(2(2(1(3(4(4(4(4(2(0(5(x0))))))))))))))))) → 5#(3(4(4(0(4(5(x0)))))))
2#(5(2(2(2(2(2(2(1(3(4(4(4(4(2(0(5(x0))))))))))))))))) → 5#(5(3(4(4(0(4(5(x0))))))))
2#(5(2(2(2(2(2(2(1(3(4(4(4(4(2(0(5(x0))))))))))))))))) → 4#(5(5(3(4(4(0(4(5(x0)))))))))
2#(5(2(2(2(2(2(2(1(3(4(4(4(4(2(0(5(x0))))))))))))))))) → 3#(4(5(5(3(4(4(0(4(5(x0))))))))))
2#(5(2(2(2(2(2(2(1(3(4(4(4(4(2(0(5(x0))))))))))))))))) → 0#(3(4(5(5(3(4(4(0(4(5(x0)))))))))))
2#(5(2(2(2(2(2(2(1(3(4(4(4(4(2(0(5(x0))))))))))))))))) → 5#(0(3(4(5(5(3(4(4(0(4(5(x0))))))))))))
2#(5(2(2(2(2(2(2(1(3(4(4(4(4(2(0(5(x0))))))))))))))))) → 5#(5(0(3(4(5(5(3(4(4(0(4(5(x0)))))))))))))
2#(5(2(2(2(2(2(2(1(3(4(4(4(4(2(0(5(x0))))))))))))))))) → 5#(5(5(0(3(4(5(5(3(4(4(0(4(5(x0))))))))))))))
2#(5(2(2(2(2(2(2(1(3(4(4(4(4(2(0(5(x0))))))))))))))))) → 0#(5(5(5(0(3(4(5(5(3(4(4(0(4(5(x0)))))))))))))))
2#(5(2(2(2(2(2(2(1(3(4(4(4(4(2(0(5(x0))))))))))))))))) → 0#(0(5(5(5(0(3(4(5(5(3(4(4(0(4(5(x0))))))))))))))))
4#(1(0(0(5(1(1(5(0(4(1(4(4(0(1(5(5(2(x0)))))))))))))))))) → 3#(x0)
4#(1(0(0(5(1(1(5(0(4(1(4(4(0(1(5(5(2(x0)))))))))))))))))) → 3#(3(x0))
4#(1(0(0(5(1(1(5(0(4(1(4(4(0(1(5(5(2(x0)))))))))))))))))) → 1#(3(3(x0)))
4#(1(0(0(5(1(1(5(0(4(1(4(4(0(1(5(5(2(x0)))))))))))))))))) → 0#(1(3(3(x0))))
4#(1(0(0(5(1(1(5(0(4(1(4(4(0(1(5(5(2(x0)))))))))))))))))) → 0#(0(1(3(3(x0)))))
4#(1(0(0(5(1(1(5(0(4(1(4(4(0(1(5(5(2(x0)))))))))))))))))) → 1#(0(0(1(3(3(x0))))))
4#(1(0(0(5(1(1(5(0(4(1(4(4(0(1(5(5(2(x0)))))))))))))))))) → 1#(1(0(0(1(3(3(x0)))))))
4#(1(0(0(5(1(1(5(0(4(1(4(4(0(1(5(5(2(x0)))))))))))))))))) → 1#(1(1(0(0(1(3(3(x0))))))))
4#(1(0(0(5(1(1(5(0(4(1(4(4(0(1(5(5(2(x0)))))))))))))))))) → 2#(1(1(1(0(0(1(3(3(x0)))))))))
4#(1(0(0(5(1(1(5(0(4(1(4(4(0(1(5(5(2(x0)))))))))))))))))) → 1#(2(1(1(1(0(0(1(3(3(x0))))))))))
4#(1(0(0(5(1(1(5(0(4(1(4(4(0(1(5(5(2(x0)))))))))))))))))) → 2#(1(2(1(1(1(0(0(1(3(3(x0)))))))))))
4#(1(0(0(5(1(1(5(0(4(1(4(4(0(1(5(5(2(x0)))))))))))))))))) → 0#(2(1(2(1(1(1(0(0(1(3(3(x0))))))))))))
4#(1(0(0(5(1(1(5(0(4(1(4(4(0(1(5(5(2(x0)))))))))))))))))) → 2#(0(2(1(2(1(1(1(0(0(1(3(3(x0)))))))))))))
4#(1(0(0(5(1(1(5(0(4(1(4(4(0(1(5(5(2(x0)))))))))))))))))) → 4#(2(0(2(1(2(1(1(1(0(0(1(3(3(x0))))))))))))))
4#(1(0(0(5(1(1(5(0(4(1(4(4(0(1(5(5(2(x0)))))))))))))))))) → 4#(4(2(0(2(1(2(1(1(1(0(0(1(3(3(x0)))))))))))))))
4#(1(0(0(5(1(1(5(0(4(1(4(4(0(1(5(5(2(x0)))))))))))))))))) → 3#(4(4(2(0(2(1(2(1(1(1(0(0(1(3(3(x0))))))))))))))))
4#(1(0(0(5(1(1(5(0(4(1(4(4(0(1(5(5(2(x0)))))))))))))))))) → 5#(3(4(4(2(0(2(1(2(1(1(1(0(0(1(3(3(x0)))))))))))))))))
4#(1(0(0(5(1(1(5(0(4(1(4(4(0(1(5(5(2(x0)))))))))))))))))) → 0#(5(3(4(4(2(0(2(1(2(1(1(1(0(0(1(3(3(x0))))))))))))))))))
2#(4(4(4(5(0(3(4(4(3(5(2(3(5(4(1(1(0(0(x0))))))))))))))))))) → 4#(0(0(x0)))
2#(4(4(4(5(0(3(4(4(3(5(2(3(5(4(1(1(0(0(x0))))))))))))))))))) → 5#(4(0(0(x0))))
2#(4(4(4(5(0(3(4(4(3(5(2(3(5(4(1(1(0(0(x0))))))))))))))))))) → 1#(5(4(0(0(x0)))))
2#(4(4(4(5(0(3(4(4(3(5(2(3(5(4(1(1(0(0(x0))))))))))))))))))) → 4#(1(5(4(0(0(x0))))))
2#(4(4(4(5(0(3(4(4(3(5(2(3(5(4(1(1(0(0(x0))))))))))))))))))) → 1#(4(1(5(4(0(0(x0)))))))
2#(4(4(4(5(0(3(4(4(3(5(2(3(5(4(1(1(0(0(x0))))))))))))))))))) → 5#(1(4(1(5(4(0(0(x0))))))))
2#(4(4(4(5(0(3(4(4(3(5(2(3(5(4(1(1(0(0(x0))))))))))))))))))) → 3#(5(1(4(1(5(4(0(0(x0)))))))))
2#(4(4(4(5(0(3(4(4(3(5(2(3(5(4(1(1(0(0(x0))))))))))))))))))) → 0#(3(5(1(4(1(5(4(0(0(x0))))))))))
2#(4(4(4(5(0(3(4(4(3(5(2(3(5(4(1(1(0(0(x0))))))))))))))))))) → 4#(0(3(5(1(4(1(5(4(0(0(x0)))))))))))
2#(4(4(4(5(0(3(4(4(3(5(2(3(5(4(1(1(0(0(x0))))))))))))))))))) → 0#(4(0(3(5(1(4(1(5(4(0(0(x0))))))))))))
2#(4(4(4(5(0(3(4(4(3(5(2(3(5(4(1(1(0(0(x0))))))))))))))))))) → 3#(0(4(0(3(5(1(4(1(5(4(0(0(x0)))))))))))))
2#(4(4(4(5(0(3(4(4(3(5(2(3(5(4(1(1(0(0(x0))))))))))))))))))) → 3#(3(0(4(0(3(5(1(4(1(5(4(0(0(x0))))))))))))))
2#(4(4(4(5(0(3(4(4(3(5(2(3(5(4(1(1(0(0(x0))))))))))))))))))) → 4#(3(3(0(4(0(3(5(1(4(1(5(4(0(0(x0)))))))))))))))
2#(4(4(4(5(0(3(4(4(3(5(2(3(5(4(1(1(0(0(x0))))))))))))))))))) → 0#(4(3(3(0(4(0(3(5(1(4(1(5(4(0(0(x0))))))))))))))))
2#(4(4(4(5(0(3(4(4(3(5(2(3(5(4(1(1(0(0(x0))))))))))))))))))) → 4#(0(4(3(3(0(4(0(3(5(1(4(1(5(4(0(0(x0)))))))))))))))))
2#(4(4(4(5(0(3(4(4(3(5(2(3(5(4(1(1(0(0(x0))))))))))))))))))) → 0#(4(0(4(3(3(0(4(0(3(5(1(4(1(5(4(0(0(x0))))))))))))))))))
2#(4(4(4(5(0(3(4(4(3(5(2(3(5(4(1(1(0(0(x0))))))))))))))))))) → 4#(0(4(0(4(3(3(0(4(0(3(5(1(4(1(5(4(0(0(x0)))))))))))))))))))
3#(2(0(2(1(4(4(5(4(3(3(4(4(2(5(1(4(1(4(1(x0)))))))))))))))))))) → 2#(1(x0))
3#(2(0(2(1(4(4(5(4(3(3(4(4(2(5(1(4(1(4(1(x0)))))))))))))))))))) → 1#(2(1(x0)))
3#(2(0(2(1(4(4(5(4(3(3(4(4(2(5(1(4(1(4(1(x0)))))))))))))))))))) → 5#(1(2(1(x0))))
3#(2(0(2(1(4(4(5(4(3(3(4(4(2(5(1(4(1(4(1(x0)))))))))))))))))))) → 0#(5(1(2(1(x0)))))
3#(2(0(2(1(4(4(5(4(3(3(4(4(2(5(1(4(1(4(1(x0)))))))))))))))))))) → 1#(0(5(1(2(1(x0))))))
3#(2(0(2(1(4(4(5(4(3(3(4(4(2(5(1(4(1(4(1(x0)))))))))))))))))))) → 0#(1(0(5(1(2(1(x0)))))))
3#(2(0(2(1(4(4(5(4(3(3(4(4(2(5(1(4(1(4(1(x0)))))))))))))))))))) → 4#(0(1(0(5(1(2(1(x0))))))))
3#(2(0(2(1(4(4(5(4(3(3(4(4(2(5(1(4(1(4(1(x0)))))))))))))))))))) → 4#(4(0(1(0(5(1(2(1(x0)))))))))
3#(2(0(2(1(4(4(5(4(3(3(4(4(2(5(1(4(1(4(1(x0)))))))))))))))))))) → 4#(4(4(0(1(0(5(1(2(1(x0))))))))))
3#(2(0(2(1(4(4(5(4(3(3(4(4(2(5(1(4(1(4(1(x0)))))))))))))))))))) → 2#(4(4(4(0(1(0(5(1(2(1(x0)))))))))))
3#(2(0(2(1(4(4(5(4(3(3(4(4(2(5(1(4(1(4(1(x0)))))))))))))))))))) → 5#(2(4(4(4(0(1(0(5(1(2(1(x0))))))))))))
3#(2(0(2(1(4(4(5(4(3(3(4(4(2(5(1(4(1(4(1(x0)))))))))))))))))))) → 0#(5(2(4(4(4(0(1(0(5(1(2(1(x0)))))))))))))
3#(2(0(2(1(4(4(5(4(3(3(4(4(2(5(1(4(1(4(1(x0)))))))))))))))))))) → 1#(0(5(2(4(4(4(0(1(0(5(1(2(1(x0))))))))))))))
3#(2(0(2(1(4(4(5(4(3(3(4(4(2(5(1(4(1(4(1(x0)))))))))))))))))))) → 5#(1(0(5(2(4(4(4(0(1(0(5(1(2(1(x0)))))))))))))))
3#(2(0(2(1(4(4(5(4(3(3(4(4(2(5(1(4(1(4(1(x0)))))))))))))))))))) → 1#(5(1(0(5(2(4(4(4(0(1(0(5(1(2(1(x0))))))))))))))))
3#(2(0(2(1(4(4(5(4(3(3(4(4(2(5(1(4(1(4(1(x0)))))))))))))))))))) → 1#(1(5(1(0(5(2(4(4(4(0(1(0(5(1(2(1(x0)))))))))))))))))
3#(2(0(2(1(4(4(5(4(3(3(4(4(2(5(1(4(1(4(1(x0)))))))))))))))))))) → 4#(1(1(5(1(0(5(2(4(4(4(0(1(0(5(1(2(1(x0))))))))))))))))))
3#(2(0(2(1(4(4(5(4(3(3(4(4(2(5(1(4(1(4(1(x0)))))))))))))))))))) → 3#(4(1(1(5(1(0(5(2(4(4(4(0(1(0(5(1(2(1(x0)))))))))))))))))))
3#(2(0(2(1(4(4(5(4(3(3(4(4(2(5(1(4(1(4(1(x0)))))))))))))))))))) → 3#(3(4(1(1(5(1(0(5(2(4(4(4(0(1(0(5(1(2(1(x0))))))))))))))))))))
2#(5(3(3(5(5(3(3(4(3(3(1(5(5(2(4(0(0(1(2(x0)))))))))))))))))))) → 4#(x0)
2#(5(3(3(5(5(3(3(4(3(3(1(5(5(2(4(0(0(1(2(x0)))))))))))))))))))) → 4#(4(x0))
2#(5(3(3(5(5(3(3(4(3(3(1(5(5(2(4(0(0(1(2(x0)))))))))))))))))))) → 3#(4(4(x0)))
2#(5(3(3(5(5(3(3(4(3(3(1(5(5(2(4(0(0(1(2(x0)))))))))))))))))))) → 3#(3(4(4(x0))))
2#(5(3(3(5(5(3(3(4(3(3(1(5(5(2(4(0(0(1(2(x0)))))))))))))))))))) → 5#(3(3(4(4(x0)))))
2#(5(3(3(5(5(3(3(4(3(3(1(5(5(2(4(0(0(1(2(x0)))))))))))))))))))) → 0#(5(3(3(4(4(x0))))))
2#(5(3(3(5(5(3(3(4(3(3(1(5(5(2(4(0(0(1(2(x0)))))))))))))))))))) → 4#(0(5(3(3(4(4(x0)))))))
2#(5(3(3(5(5(3(3(4(3(3(1(5(5(2(4(0(0(1(2(x0)))))))))))))))))))) → 2#(4(0(5(3(3(4(4(x0))))))))
2#(5(3(3(5(5(3(3(4(3(3(1(5(5(2(4(0(0(1(2(x0)))))))))))))))))))) → 2#(2(4(0(5(3(3(4(4(x0)))))))))
2#(5(3(3(5(5(3(3(4(3(3(1(5(5(2(4(0(0(1(2(x0)))))))))))))))))))) → 1#(2(2(4(0(5(3(3(4(4(x0))))))))))
2#(5(3(3(5(5(3(3(4(3(3(1(5(5(2(4(0(0(1(2(x0)))))))))))))))))))) → 1#(1(2(2(4(0(5(3(3(4(4(x0)))))))))))
2#(5(3(3(5(5(3(3(4(3(3(1(5(5(2(4(0(0(1(2(x0)))))))))))))))))))) → 3#(1(1(2(2(4(0(5(3(3(4(4(x0))))))))))))
2#(5(3(3(5(5(3(3(4(3(3(1(5(5(2(4(0(0(1(2(x0)))))))))))))))))))) → 1#(3(1(1(2(2(4(0(5(3(3(4(4(x0)))))))))))))
2#(5(3(3(5(5(3(3(4(3(3(1(5(5(2(4(0(0(1(2(x0)))))))))))))))))))) → 5#(1(3(1(1(2(2(4(0(5(3(3(4(4(x0))))))))))))))
2#(5(3(3(5(5(3(3(4(3(3(1(5(5(2(4(0(0(1(2(x0)))))))))))))))))))) → 2#(5(1(3(1(1(2(2(4(0(5(3(3(4(4(x0)))))))))))))))
2#(5(3(3(5(5(3(3(4(3(3(1(5(5(2(4(0(0(1(2(x0)))))))))))))))))))) → 5#(2(5(1(3(1(1(2(2(4(0(5(3(3(4(4(x0))))))))))))))))
2#(5(3(3(5(5(3(3(4(3(3(1(5(5(2(4(0(0(1(2(x0)))))))))))))))))))) → 2#(5(2(5(1(3(1(1(2(2(4(0(5(3(3(4(4(x0)))))))))))))))))
2#(5(3(3(5(5(3(3(4(3(3(1(5(5(2(4(0(0(1(2(x0)))))))))))))))))))) → 4#(2(5(2(5(1(3(1(1(2(2(4(0(5(3(3(4(4(x0))))))))))))))))))
2#(5(3(3(5(5(3(3(4(3(3(1(5(5(2(4(0(0(1(2(x0)))))))))))))))))))) → 5#(4(2(5(2(5(1(3(1(1(2(2(4(0(5(3(3(4(4(x0)))))))))))))))))))
4#(2(4(1(2(5(2(0(1(3(5(1(2(5(4(5(4(2(4(2(4(x0))))))))))))))))))))) → 1#(x0)
4#(2(4(1(2(5(2(0(1(3(5(1(2(5(4(5(4(2(4(2(4(x0))))))))))))))))))))) → 5#(1(x0))
4#(2(4(1(2(5(2(0(1(3(5(1(2(5(4(5(4(2(4(2(4(x0))))))))))))))))))))) → 3#(5(1(x0)))
4#(2(4(1(2(5(2(0(1(3(5(1(2(5(4(5(4(2(4(2(4(x0))))))))))))))))))))) → 1#(3(5(1(x0))))
4#(2(4(1(2(5(2(0(1(3(5(1(2(5(4(5(4(2(4(2(4(x0))))))))))))))))))))) → 5#(1(3(5(1(x0)))))
4#(2(4(1(2(5(2(0(1(3(5(1(2(5(4(5(4(2(4(2(4(x0))))))))))))))))))))) → 0#(5(1(3(5(1(x0))))))
4#(2(4(1(2(5(2(0(1(3(5(1(2(5(4(5(4(2(4(2(4(x0))))))))))))))))))))) → 5#(0(5(1(3(5(1(x0)))))))
4#(2(4(1(2(5(2(0(1(3(5(1(2(5(4(5(4(2(4(2(4(x0))))))))))))))))))))) → 2#(5(0(5(1(3(5(1(x0))))))))
4#(2(4(1(2(5(2(0(1(3(5(1(2(5(4(5(4(2(4(2(4(x0))))))))))))))))))))) → 0#(2(5(0(5(1(3(5(1(x0)))))))))
4#(2(4(1(2(5(2(0(1(3(5(1(2(5(4(5(4(2(4(2(4(x0))))))))))))))))))))) → 5#(0(2(5(0(5(1(3(5(1(x0))))))))))
4#(2(4(1(2(5(2(0(1(3(5(1(2(5(4(5(4(2(4(2(4(x0))))))))))))))))))))) → 4#(5(0(2(5(0(5(1(3(5(1(x0)))))))))))
4#(2(4(1(2(5(2(0(1(3(5(1(2(5(4(5(4(2(4(2(4(x0))))))))))))))))))))) → 3#(4(5(0(2(5(0(5(1(3(5(1(x0))))))))))))
4#(2(4(1(2(5(2(0(1(3(5(1(2(5(4(5(4(2(4(2(4(x0))))))))))))))))))))) → 5#(3(4(5(0(2(5(0(5(1(3(5(1(x0)))))))))))))
4#(2(4(1(2(5(2(0(1(3(5(1(2(5(4(5(4(2(4(2(4(x0))))))))))))))))))))) → 2#(5(3(4(5(0(2(5(0(5(1(3(5(1(x0))))))))))))))
4#(2(4(1(2(5(2(0(1(3(5(1(2(5(4(5(4(2(4(2(4(x0))))))))))))))))))))) → 1#(2(5(3(4(5(0(2(5(0(5(1(3(5(1(x0)))))))))))))))
4#(2(4(1(2(5(2(0(1(3(5(1(2(5(4(5(4(2(4(2(4(x0))))))))))))))))))))) → 2#(1(2(5(3(4(5(0(2(5(0(5(1(3(5(1(x0))))))))))))))))
4#(2(4(1(2(5(2(0(1(3(5(1(2(5(4(5(4(2(4(2(4(x0))))))))))))))))))))) → 5#(2(1(2(5(3(4(5(0(2(5(0(5(1(3(5(1(x0)))))))))))))))))
4#(2(4(1(2(5(2(0(1(3(5(1(2(5(4(5(4(2(4(2(4(x0))))))))))))))))))))) → 4#(5(2(1(2(5(3(4(5(0(2(5(0(5(1(3(5(1(x0))))))))))))))))))
4#(2(4(1(2(5(2(0(1(3(5(1(2(5(4(5(4(2(4(2(4(x0))))))))))))))))))))) → 3#(4(5(2(1(2(5(3(4(5(0(2(5(0(5(1(3(5(1(x0)))))))))))))))))))
4#(2(4(1(2(5(2(0(1(3(5(1(2(5(4(5(4(2(4(2(4(x0))))))))))))))))))))) → 2#(3(4(5(2(1(2(5(3(4(5(0(2(5(0(5(1(3(5(1(x0))))))))))))))))))))
4#(2(4(1(2(5(2(0(1(3(5(1(2(5(4(5(4(2(4(2(4(x0))))))))))))))))))))) → 1#(2(3(4(5(2(1(2(5(3(4(5(0(2(5(0(5(1(3(5(1(x0)))))))))))))))))))))
5#(3(5(5(0(2(4(3(3(3(5(1(4(3(4(3(0(1(2(0(5(x0))))))))))))))))))))) → 3#(x0)
5#(3(5(5(0(2(4(3(3(3(5(1(4(3(4(3(0(1(2(0(5(x0))))))))))))))))))))) → 5#(3(x0))
5#(3(5(5(0(2(4(3(3(3(5(1(4(3(4(3(0(1(2(0(5(x0))))))))))))))))))))) → 1#(5(3(x0)))
5#(3(5(5(0(2(4(3(3(3(5(1(4(3(4(3(0(1(2(0(5(x0))))))))))))))))))))) → 1#(1(5(3(x0))))
5#(3(5(5(0(2(4(3(3(3(5(1(4(3(4(3(0(1(2(0(5(x0))))))))))))))))))))) → 0#(1(1(5(3(x0)))))
5#(3(5(5(0(2(4(3(3(3(5(1(4(3(4(3(0(1(2(0(5(x0))))))))))))))))))))) → 5#(0(1(1(5(3(x0))))))
5#(3(5(5(0(2(4(3(3(3(5(1(4(3(4(3(0(1(2(0(5(x0))))))))))))))))))))) → 4#(5(0(1(1(5(3(x0)))))))
5#(3(5(5(0(2(4(3(3(3(5(1(4(3(4(3(0(1(2(0(5(x0))))))))))))))))))))) → 5#(4(5(0(1(1(5(3(x0))))))))
5#(3(5(5(0(2(4(3(3(3(5(1(4(3(4(3(0(1(2(0(5(x0))))))))))))))))))))) → 2#(5(4(5(0(1(1(5(3(x0)))))))))
5#(3(5(5(0(2(4(3(3(3(5(1(4(3(4(3(0(1(2(0(5(x0))))))))))))))))))))) → 1#(2(5(4(5(0(1(1(5(3(x0))))))))))
5#(3(5(5(0(2(4(3(3(3(5(1(4(3(4(3(0(1(2(0(5(x0))))))))))))))))))))) → 5#(1(2(5(4(5(0(1(1(5(3(x0)))))))))))
5#(3(5(5(0(2(4(3(3(3(5(1(4(3(4(3(0(1(2(0(5(x0))))))))))))))))))))) → 0#(5(1(2(5(4(5(0(1(1(5(3(x0))))))))))))
5#(3(5(5(0(2(4(3(3(3(5(1(4(3(4(3(0(1(2(0(5(x0))))))))))))))))))))) → 4#(0(5(1(2(5(4(5(0(1(1(5(3(x0)))))))))))))
5#(3(5(5(0(2(4(3(3(3(5(1(4(3(4(3(0(1(2(0(5(x0))))))))))))))))))))) → 4#(4(0(5(1(2(5(4(5(0(1(1(5(3(x0))))))))))))))
5#(3(5(5(0(2(4(3(3(3(5(1(4(3(4(3(0(1(2(0(5(x0))))))))))))))))))))) → 4#(4(4(0(5(1(2(5(4(5(0(1(1(5(3(x0)))))))))))))))
5#(3(5(5(0(2(4(3(3(3(5(1(4(3(4(3(0(1(2(0(5(x0))))))))))))))))))))) → 3#(4(4(4(0(5(1(2(5(4(5(0(1(1(5(3(x0))))))))))))))))
5#(3(5(5(0(2(4(3(3(3(5(1(4(3(4(3(0(1(2(0(5(x0))))))))))))))))))))) → 4#(3(4(4(4(0(5(1(2(5(4(5(0(1(1(5(3(x0)))))))))))))))))
5#(3(5(5(0(2(4(3(3(3(5(1(4(3(4(3(0(1(2(0(5(x0))))))))))))))))))))) → 4#(4(3(4(4(4(0(5(1(2(5(4(5(0(1(1(5(3(x0))))))))))))))))))
5#(3(5(5(0(2(4(3(3(3(5(1(4(3(4(3(0(1(2(0(5(x0))))))))))))))))))))) → 1#(4(4(3(4(4(4(0(5(1(2(5(4(5(0(1(1(5(3(x0)))))))))))))))))))
5#(3(5(5(0(2(4(3(3(3(5(1(4(3(4(3(0(1(2(0(5(x0))))))))))))))))))))) → 5#(1(4(4(3(4(4(4(0(5(1(2(5(4(5(0(1(1(5(3(x0))))))))))))))))))))

1.1.1 Reduction Pair Processor

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight function
prec(5#) = 0 weight(5#) = 1
prec(4#) = 2 weight(4#) = 1
prec(0#) = 7 weight(0#) = 0
prec(3#) = 0 weight(3#) = 1
prec(2#) = 4 weight(2#) = 1
prec(1#) = 1 weight(1#) = 1
prec(5) = 0 weight(5) = 1
prec(4) = 4 weight(4) = 1
prec(2) = 6 weight(2) = 1
prec(3) = 0 weight(3) = 1
prec(0) = 2 weight(0) = 1
prec(1) = 3 weight(1) = 1
all pairs could be removed.

1.1.1.1 P is empty

There are no pairs anymore.