YES
0 QTRS
↳1 DependencyPairsProof (⇔, 0 ms)
↳2 QDP
↳3 TransformationProof (⇔, 0 ms)
↳4 QDP
↳5 TransformationProof (⇔, 0 ms)
↳6 QDP
↳7 SemLabProof (⇒, 462 ms)
↳8 QDP
↳9 DependencyGraphProof (⇔, 0 ms)
↳10 QDP
↳11 QDPOrderProof (⇔, 81 ms)
↳12 QDP
↳13 DependencyGraphProof (⇔, 0 ms)
↳14 AND
↳15 QDP
↳16 QDPOrderProof (⇔, 0 ms)
↳17 QDP
↳18 DependencyGraphProof (⇔, 0 ms)
↳19 QDP
↳20 QDPOrderProof (⇔, 0 ms)
↳21 QDP
↳22 DependencyGraphProof (⇔, 0 ms)
↳23 QDP
↳24 QDPOrderProof (⇔, 21 ms)
↳25 QDP
↳26 PisEmptyProof (⇔, 0 ms)
↳27 YES
↳28 QDP
↳29 QDPOrderProof (⇔, 0 ms)
↳30 QDP
↳31 DependencyGraphProof (⇔, 0 ms)
↳32 QDP
↳33 QDPOrderProof (⇔, 0 ms)
↳34 QDP
↳35 DependencyGraphProof (⇔, 0 ms)
↳36 QDP
↳37 QDPOrderProof (⇔, 9 ms)
↳38 QDP
↳39 DependencyGraphProof (⇔, 0 ms)
↳40 TRUE
f(f(x, y, a), z, w) → f(z, w, f(y, x, z))
F(f(x, y, a), z, w) → F(z, w, f(y, x, z))
F(f(x, y, a), z, w) → F(y, x, z)
f(f(x, y, a), z, w) → f(z, w, f(y, x, z))
F(f(x0, x1, a), f(y_0, y_1, a), x3) → F(f(y_0, y_1, a), x3, f(x1, x0, f(y_0, y_1, a))) → F(f(x0, x1, a), f(y_0, y_1, a), x3) → F(f(y_0, y_1, a), x3, f(x1, x0, f(y_0, y_1, a)))
F(f(x, y, a), z, w) → F(y, x, z)
F(f(x0, x1, a), f(y_0, y_1, a), x3) → F(f(y_0, y_1, a), x3, f(x1, x0, f(y_0, y_1, a)))
f(f(x, y, a), z, w) → f(z, w, f(y, x, z))
F(f(x0, f(y_0, y_1, a), a), x2, x3) → F(f(y_0, y_1, a), x0, x2) → F(f(x0, f(y_0, y_1, a), a), x2, x3) → F(f(y_0, y_1, a), x0, x2)
F(f(f(y_2, y_3, a), f(y_0, y_1, a), a), x2, x3) → F(f(y_0, y_1, a), f(y_2, y_3, a), x2) → F(f(f(y_2, y_3, a), f(y_0, y_1, a), a), x2, x3) → F(f(y_0, y_1, a), f(y_2, y_3, a), x2)
F(f(x0, x1, a), f(y_0, y_1, a), x3) → F(f(y_0, y_1, a), x3, f(x1, x0, f(y_0, y_1, a)))
F(f(x0, f(y_0, y_1, a), a), x2, x3) → F(f(y_0, y_1, a), x0, x2)
F(f(f(y_2, y_3, a), f(y_0, y_1, a), a), x2, x3) → F(f(y_0, y_1, a), f(y_2, y_3, a), x2)
f(f(x, y, a), z, w) → f(z, w, f(y, x, z))
F.0-0-0(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-1(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-0(f.0-0-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-1-1(y_0, y_1, a.)))
F.0-0-1(f.0-0-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) → F.0-1-0(f.0-1-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-1-1(y_0, y_1, a.)))
F.0-0-0(f.0-0-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.1-0-1(y_0, y_1, a.)))
F.0-0-1(f.0-0-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.1-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.1-0-1(y_0, y_1, a.)))
F.0-0-0(f.0-0-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.1-1-1(y_0, y_1, a.)))
F.0-0-1(f.0-0-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) → F.0-1-0(f.1-1-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.1-1-1(y_0, y_1, a.)))
F.0-0-0(f.0-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-1(f.0-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-0(f.0-1-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-1-1(y_0, y_1, a.)))
F.0-0-1(f.0-1-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) → F.0-1-0(f.0-1-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-1-1(y_0, y_1, a.)))
F.0-0-0(f.0-1-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.1-0-1(y_0, y_1, a.)))
F.0-0-1(f.0-1-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.1-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.1-0-1(y_0, y_1, a.)))
F.0-0-0(f.0-1-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.1-1-1(y_0, y_1, a.)))
F.0-0-1(f.0-1-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) → F.0-1-0(f.1-1-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.1-1-1(y_0, y_1, a.)))
F.0-0-0(f.1-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-1(f.1-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-0(f.1-0-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.0-1-1(y_0, y_1, a.)))
F.0-0-1(f.1-0-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) → F.0-1-0(f.0-1-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.0-1-1(y_0, y_1, a.)))
F.0-0-0(f.1-0-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.1-0-1(y_0, y_1, a.)))
F.0-0-1(f.1-0-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.1-0-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.1-0-1(y_0, y_1, a.)))
F.0-0-0(f.1-0-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.1-1-1(y_0, y_1, a.)))
F.0-0-1(f.1-0-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) → F.0-1-0(f.1-1-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.1-1-1(y_0, y_1, a.)))
F.0-0-0(f.1-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-1(f.1-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-0(f.1-1-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-1-1(y_0, y_1, a.)))
F.0-0-1(f.1-1-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) → F.0-1-0(f.0-1-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-1-1(y_0, y_1, a.)))
F.0-0-0(f.1-1-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.1-0-1(y_0, y_1, a.)))
F.0-0-1(f.1-1-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.1-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.1-0-1(y_0, y_1, a.)))
F.0-0-0(f.1-1-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.1-1-1(y_0, y_1, a.)))
F.0-0-1(f.1-1-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) → F.0-1-0(f.1-1-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.1-1-1(y_0, y_1, a.)))
F.0-0-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-1-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-1-1(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), x0, x2)
F.0-1-0(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-1-1(y_0, y_1, a.), x0, x2)
F.0-1-1(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-1-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.0-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.0-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), x0, x2)
F.0-1-0(f.0-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), x0, x2)
F.0-1-1(f.0-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x0, x2)
F.0-1-0(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), x0, x2)
F.0-1-1(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.1-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.1-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-1-0(f.1-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-1(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-1-1(f.1-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-1(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.1-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-0(f.0-1-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.1-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-0(f.0-1-1(y_0, y_1, a.), x0, x2)
F.0-1-0(f.1-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-1(f.0-1-1(y_0, y_1, a.), x0, x2)
F.0-1-1(f.1-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-1(f.0-1-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.1-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-0(f.1-0-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.1-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-0(f.1-0-1(y_0, y_1, a.), x0, x2)
F.0-1-0(f.1-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-1(f.1-0-1(y_0, y_1, a.), x0, x2)
F.0-1-1(f.1-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-1(f.1-0-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.1-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-0(f.1-1-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.1-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-0(f.1-1-1(y_0, y_1, a.), x0, x2)
F.0-1-0(f.1-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-1(f.1-1-1(y_0, y_1, a.), x0, x2)
F.0-1-1(f.1-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-1(f.1-1-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
f.0-0-0(f.0-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-0-0(y, x, z))
f.0-0-1(f.0-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-0-0(y, x, z))
f.0-1-0(f.0-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-0-1(y, x, z))
f.0-1-1(f.0-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-0-1(y, x, z))
f.0-0-0(f.0-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-0-0(y, x, z))
f.0-0-1(f.0-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-0-0(y, x, z))
f.0-1-0(f.0-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-0-1(y, x, z))
f.0-1-1(f.0-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-0-1(y, x, z))
f.0-0-0(f.1-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-1-0(y, x, z))
f.0-0-1(f.1-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-1-0(y, x, z))
f.0-1-0(f.1-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-1-1(y, x, z))
f.0-1-1(f.1-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-1-1(y, x, z))
f.0-0-0(f.1-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-1-0(y, x, z))
f.0-0-1(f.1-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-1-0(y, x, z))
f.0-1-0(f.1-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-1-1(y, x, z))
f.0-1-1(f.1-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-1-1(y, x, z))
F.0-0-0(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-0(f.0-0-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-1-1(y_0, y_1, a.)))
F.0-0-0(f.0-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-0(f.0-0-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.1-0-1(y_0, y_1, a.)))
F.0-0-0(f.1-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-0(f.0-0-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.1-1-1(y_0, y_1, a.)))
F.0-0-0(f.1-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.0-1-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-1-1(y_0, y_1, a.)))
F.0-0-0(f.0-1-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.1-0-1(y_0, y_1, a.)))
F.0-0-0(f.1-0-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.0-1-1(y_0, y_1, a.)))
F.0-0-0(f.0-1-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.1-1-1(y_0, y_1, a.)))
F.0-0-0(f.1-1-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-1-1(y_0, y_1, a.)))
F.0-0-0(f.1-1-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.1-0-1(y_0, y_1, a.)))
F.0-0-0(f.1-0-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.1-0-1(y_0, y_1, a.)))
F.0-0-0(f.1-0-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.1-1-1(y_0, y_1, a.)))
F.0-0-0(f.1-1-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.1-1-1(y_0, y_1, a.)))
F.0-0-0(f.1-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-1-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-1-0(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-1-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.0-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-1-0(f.0-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.1-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-1-0(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.1-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.0-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.1-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-0(f.1-0-1(y_0, y_1, a.), x0, x2)
F.0-1-0(f.1-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-1(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-1-1(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.0-0-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.1-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.1-0-1(y_0, y_1, a.)))
F.0-1-0(f.1-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-1(f.1-0-1(y_0, y_1, a.), x0, x2)
F.0-1-1(f.1-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-1(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-1-1(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-1-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.0-1-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.1-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.1-0-1(y_0, y_1, a.)))
F.0-1-1(f.0-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.1-0-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.1-0-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.1-0-1(y_0, y_1, a.)))
F.0-0-1(f.1-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-1(f.1-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-0(f.1-0-1(y_0, y_1, a.), x0, x2)
F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.0-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-1(f.1-1-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.1-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.1-0-1(y_0, y_1, a.)))
F.0-1-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), x0, x2)
F.0-1-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-1-1(f.1-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-1(f.1-0-1(y_0, y_1, a.), x0, x2)
f.0-0-0(f.0-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-0-0(y, x, z))
f.0-0-1(f.0-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-0-0(y, x, z))
f.0-1-0(f.0-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-0-1(y, x, z))
f.0-1-1(f.0-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-0-1(y, x, z))
f.0-0-0(f.0-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-0-0(y, x, z))
f.0-0-1(f.0-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-0-0(y, x, z))
f.0-1-0(f.0-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-0-1(y, x, z))
f.0-1-1(f.0-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-0-1(y, x, z))
f.0-0-0(f.1-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-1-0(y, x, z))
f.0-0-1(f.1-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-1-0(y, x, z))
f.0-1-0(f.1-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-1-1(y, x, z))
f.0-1-1(f.1-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-1-1(y, x, z))
f.0-0-0(f.1-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-1-0(y, x, z))
f.0-0-1(f.1-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-1-0(y, x, z))
f.0-1-0(f.1-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-1-1(y, x, z))
f.0-1-1(f.1-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-1-1(y, x, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F.0-0-0(f.1-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-0(f.1-0-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.0-1-1(y_0, y_1, a.)))
F.0-0-0(f.1-0-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.1-0-1(y_0, y_1, a.)))
F.0-0-0(f.1-0-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.1-1-1(y_0, y_1, a.)))
F.0-0-0(f.1-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.1-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-0(f.1-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-0(f.1-0-1(y_0, y_1, a.), x0, x2)
F.0-1-0(f.1-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-1(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-1-0(f.1-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-1(f.1-0-1(y_0, y_1, a.), x0, x2)
F.0-1-1(f.1-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-1(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.1-0-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.1-0-1(y_0, y_1, a.), x3, f.0-1-0(x1, x0, f.1-0-1(y_0, y_1, a.)))
F.0-0-1(f.1-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.1-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-0(f.1-0-1(y_0, y_1, a.), x0, x2)
F.0-1-1(f.1-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-1-1(f.1-0-1(y_0, y_1, a.), x0, x2)
POL(F.0-0-0(x1, x2, x3)) = 1 + x1 + x2 + x3
POL(F.0-0-1(x1, x2, x3)) = 1 + x1 + x2
POL(F.0-1-0(x1, x2, x3)) = 1 + x1 + x3
POL(F.0-1-1(x1, x2, x3)) = 1 + x1
POL(a.) = 0
POL(f.0-0-0(x1, x2, x3)) = 0
POL(f.0-0-1(x1, x2, x3)) = x1 + x2
POL(f.0-1-0(x1, x2, x3)) = 0
POL(f.0-1-1(x1, x2, x3)) = x3
POL(f.1-0-0(x1, x2, x3)) = 0
POL(f.1-0-1(x1, x2, x3)) = 1 + x2
POL(f.1-1-0(x1, x2, x3)) = 0
POL(f.1-1-1(x1, x2, x3)) = x3
f.0-0-1(f.0-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-0-0(y, x, z))
f.0-0-1(f.0-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-0-0(y, x, z))
f.0-0-1(f.1-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-1-0(y, x, z))
f.0-0-1(f.1-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-1-0(y, x, z))
f.0-0-0(f.0-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-0-0(y, x, z))
f.0-0-0(f.0-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-0-0(y, x, z))
f.0-0-0(f.1-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-1-0(y, x, z))
f.0-0-0(f.1-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-1-0(y, x, z))
f.0-1-1(f.0-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-0-1(y, x, z))
f.0-1-1(f.0-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-0-1(y, x, z))
f.0-1-1(f.1-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-1-1(y, x, z))
f.0-1-1(f.1-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-1-1(y, x, z))
f.0-1-0(f.0-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-0-1(y, x, z))
f.0-1-0(f.0-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-0-1(y, x, z))
f.0-1-0(f.1-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-1-1(y, x, z))
f.0-1-0(f.1-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-1-1(y, x, z))
F.0-0-0(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-0(f.0-0-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-1-1(y_0, y_1, a.)))
F.0-0-0(f.0-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-0(f.0-0-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.1-0-1(y_0, y_1, a.)))
F.0-0-0(f.0-0-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.1-1-1(y_0, y_1, a.)))
F.0-0-0(f.1-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.0-1-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-1-1(y_0, y_1, a.)))
F.0-0-0(f.0-1-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.1-0-1(y_0, y_1, a.)))
F.0-0-0(f.0-1-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.1-1-1(y_0, y_1, a.)))
F.0-0-0(f.1-1-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-1-1(y_0, y_1, a.)))
F.0-0-0(f.1-1-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.1-0-1(y_0, y_1, a.)))
F.0-0-0(f.1-1-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.1-1-1(y_0, y_1, a.)))
F.0-1-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-1-0(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-1-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.0-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-1-0(f.0-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), x0, x2)
F.0-1-0(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.1-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.0-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), x0, x2)
F.0-1-1(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.0-0-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.1-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.1-0-1(y_0, y_1, a.)))
F.0-1-1(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-1-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.0-1-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.1-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.1-0-1(y_0, y_1, a.)))
F.0-1-1(f.0-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), x0, x2)
F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.0-0-1(x0, f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-0-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-1(f.1-1-1(x0, x1, a.), f.1-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.1-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.1-0-1(y_0, y_1, a.)))
F.0-1-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), x0, x2)
F.0-1-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-1-1(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
f.0-0-0(f.0-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-0-0(y, x, z))
f.0-0-1(f.0-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-0-0(y, x, z))
f.0-1-0(f.0-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-0-1(y, x, z))
f.0-1-1(f.0-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-0-1(y, x, z))
f.0-0-0(f.0-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-0-0(y, x, z))
f.0-0-1(f.0-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-0-0(y, x, z))
f.0-1-0(f.0-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-0-1(y, x, z))
f.0-1-1(f.0-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-0-1(y, x, z))
f.0-0-0(f.1-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-1-0(y, x, z))
f.0-0-1(f.1-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-1-0(y, x, z))
f.0-1-0(f.1-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-1-1(y, x, z))
f.0-1-1(f.1-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-1-1(y, x, z))
f.0-0-0(f.1-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-1-0(y, x, z))
f.0-0-1(f.1-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-1-0(y, x, z))
f.0-1-0(f.1-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-1-1(y, x, z))
f.0-1-1(f.1-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-1-1(y, x, z))
F.0-0-0(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-0(f.0-0-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-1-1(y_0, y_1, a.)))
F.0-0-0(f.0-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-0(f.0-0-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.1-1-1(y_0, y_1, a.)))
F.0-0-0(f.1-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.0-1-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-1-1(y_0, y_1, a.)))
F.0-0-0(f.0-1-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.1-1-1(y_0, y_1, a.)))
F.0-0-0(f.1-1-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-1-1(y_0, y_1, a.)))
F.0-0-0(f.1-1-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.1-1-1(y_0, y_1, a.)))
F.0-0-0(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
f.0-0-0(f.0-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-0-0(y, x, z))
f.0-0-1(f.0-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-0-0(y, x, z))
f.0-1-0(f.0-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-0-1(y, x, z))
f.0-1-1(f.0-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-0-1(y, x, z))
f.0-0-0(f.0-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-0-0(y, x, z))
f.0-0-1(f.0-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-0-0(y, x, z))
f.0-1-0(f.0-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-0-1(y, x, z))
f.0-1-1(f.0-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-0-1(y, x, z))
f.0-0-0(f.1-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-1-0(y, x, z))
f.0-0-1(f.1-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-1-0(y, x, z))
f.0-1-0(f.1-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-1-1(y, x, z))
f.0-1-1(f.1-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-1-1(y, x, z))
f.0-0-0(f.1-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-1-0(y, x, z))
f.0-0-1(f.1-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-1-0(y, x, z))
f.0-1-0(f.1-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-1-1(y, x, z))
f.0-1-1(f.1-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-1-1(y, x, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F.0-0-0(f.0-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-0(f.0-1-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-1-1(y_0, y_1, a.)))
F.0-0-0(f.0-1-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.1-1-1(y_0, y_1, a.)))
POL(F.0-0-0(x1, x2, x3)) = x1 + x2 + x3
POL(a.) = 1
POL(f.0-0-0(x1, x2, x3)) = 0
POL(f.0-0-1(x1, x2, x3)) = x1 + x2
POL(f.0-1-0(x1, x2, x3)) = 0
POL(f.0-1-1(x1, x2, x3)) = 1 + x3
POL(f.1-0-0(x1, x2, x3)) = 0
POL(f.1-0-1(x1, x2, x3)) = 1 + x3
POL(f.1-1-0(x1, x2, x3)) = 0
POL(f.1-1-1(x1, x2, x3)) = 0
f.0-0-1(f.0-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-0-0(y, x, z))
f.0-0-1(f.0-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-0-0(y, x, z))
f.0-0-1(f.1-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-1-0(y, x, z))
f.0-0-1(f.1-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-1-0(y, x, z))
f.0-0-0(f.0-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-0-0(y, x, z))
f.0-0-0(f.0-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-0-0(y, x, z))
f.0-0-0(f.1-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-1-0(y, x, z))
f.0-0-0(f.1-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-1-0(y, x, z))
f.0-1-1(f.0-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-0-1(y, x, z))
f.0-1-1(f.0-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-0-1(y, x, z))
f.0-1-1(f.1-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-1-1(y, x, z))
f.0-1-1(f.1-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-1-1(y, x, z))
f.0-1-0(f.0-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-0-1(y, x, z))
f.0-1-0(f.1-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-1-1(y, x, z))
f.0-1-0(f.0-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-0-1(y, x, z))
f.0-1-0(f.1-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-1-1(y, x, z))
F.0-0-0(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-0(f.0-0-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-1-1(y_0, y_1, a.)))
F.0-0-0(f.0-0-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.1-1-1(y_0, y_1, a.)))
F.0-0-0(f.1-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.1-1-1(x0, x1, a.), f.0-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-1-1(y_0, y_1, a.)))
F.0-0-0(f.1-1-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.1-1-1(y_0, y_1, a.)))
F.0-0-0(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
f.0-0-0(f.0-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-0-0(y, x, z))
f.0-0-1(f.0-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-0-0(y, x, z))
f.0-1-0(f.0-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-0-1(y, x, z))
f.0-1-1(f.0-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-0-1(y, x, z))
f.0-0-0(f.0-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-0-0(y, x, z))
f.0-0-1(f.0-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-0-0(y, x, z))
f.0-1-0(f.0-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-0-1(y, x, z))
f.0-1-1(f.0-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-0-1(y, x, z))
f.0-0-0(f.1-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-1-0(y, x, z))
f.0-0-1(f.1-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-1-0(y, x, z))
f.0-1-0(f.1-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-1-1(y, x, z))
f.0-1-1(f.1-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-1-1(y, x, z))
f.0-0-0(f.1-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-1-0(y, x, z))
f.0-0-1(f.1-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-1-0(y, x, z))
f.0-1-0(f.1-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-1-1(y, x, z))
f.0-1-1(f.1-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-1-1(y, x, z))
F.0-0-0(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-0(f.0-0-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.1-1-1(y_0, y_1, a.)))
F.0-0-0(f.1-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.1-1-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.1-1-1(y_0, y_1, a.)))
F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
f.0-0-0(f.0-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-0-0(y, x, z))
f.0-0-1(f.0-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-0-0(y, x, z))
f.0-1-0(f.0-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-0-1(y, x, z))
f.0-1-1(f.0-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-0-1(y, x, z))
f.0-0-0(f.0-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-0-0(y, x, z))
f.0-0-1(f.0-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-0-0(y, x, z))
f.0-1-0(f.0-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-0-1(y, x, z))
f.0-1-1(f.0-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-0-1(y, x, z))
f.0-0-0(f.1-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-1-0(y, x, z))
f.0-0-1(f.1-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-1-0(y, x, z))
f.0-1-0(f.1-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-1-1(y, x, z))
f.0-1-1(f.1-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-1-1(y, x, z))
f.0-0-0(f.1-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-1-0(y, x, z))
f.0-0-1(f.1-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-1-0(y, x, z))
f.0-1-0(f.1-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-1-1(y, x, z))
f.0-1-1(f.1-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-1-1(y, x, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F.0-0-0(f.1-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-0(f.1-1-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.1-1-1(y_0, y_1, a.)))
POL(F.0-0-0(x1, x2, x3)) = x1 + x2 + x3
POL(a.) = 1
POL(f.0-0-0(x1, x2, x3)) = 0
POL(f.0-0-1(x1, x2, x3)) = x1 + x2
POL(f.0-1-0(x1, x2, x3)) = 0
POL(f.0-1-1(x1, x2, x3)) = 0
POL(f.1-0-0(x1, x2, x3)) = 0
POL(f.1-0-1(x1, x2, x3)) = 0
POL(f.1-1-0(x1, x2, x3)) = 0
POL(f.1-1-1(x1, x2, x3)) = x3
f.0-0-1(f.0-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-0-0(y, x, z))
f.0-0-1(f.0-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-0-0(y, x, z))
f.0-0-1(f.1-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-1-0(y, x, z))
f.0-0-1(f.1-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-1-0(y, x, z))
f.0-0-0(f.0-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-0-0(y, x, z))
f.0-0-0(f.0-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-0-0(y, x, z))
f.0-0-0(f.1-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-1-0(y, x, z))
f.0-0-0(f.1-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-1-0(y, x, z))
f.0-1-1(f.0-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-0-1(y, x, z))
f.0-1-1(f.0-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-0-1(y, x, z))
f.0-1-1(f.1-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-1-1(y, x, z))
f.0-1-1(f.1-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-1-1(y, x, z))
f.0-1-0(f.0-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-0-1(y, x, z))
f.0-1-0(f.1-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-1-1(y, x, z))
f.0-1-0(f.0-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-0-1(y, x, z))
f.0-1-0(f.1-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-1-1(y, x, z))
F.0-0-0(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-0(f.0-0-1(x0, x1, a.), f.1-1-1(y_0, y_1, a.), x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.1-1-1(y_0, y_1, a.)))
F.0-0-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.1-1-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
f.0-0-0(f.0-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-0-0(y, x, z))
f.0-0-1(f.0-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-0-0(y, x, z))
f.0-1-0(f.0-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-0-1(y, x, z))
f.0-1-1(f.0-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-0-1(y, x, z))
f.0-0-0(f.0-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-0-0(y, x, z))
f.0-0-1(f.0-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-0-0(y, x, z))
f.0-1-0(f.0-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-0-1(y, x, z))
f.0-1-1(f.0-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-0-1(y, x, z))
f.0-0-0(f.1-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-1-0(y, x, z))
f.0-0-1(f.1-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-1-0(y, x, z))
f.0-1-0(f.1-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-1-1(y, x, z))
f.0-1-1(f.1-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-1-1(y, x, z))
f.0-0-0(f.1-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-1-0(y, x, z))
f.0-0-1(f.1-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-1-0(y, x, z))
f.0-1-0(f.1-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-1-1(y, x, z))
f.0-1-1(f.1-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-1-1(y, x, z))
F.0-0-0(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
f.0-0-0(f.0-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-0-0(y, x, z))
f.0-0-1(f.0-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-0-0(y, x, z))
f.0-1-0(f.0-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-0-1(y, x, z))
f.0-1-1(f.0-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-0-1(y, x, z))
f.0-0-0(f.0-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-0-0(y, x, z))
f.0-0-1(f.0-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-0-0(y, x, z))
f.0-1-0(f.0-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-0-1(y, x, z))
f.0-1-1(f.0-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-0-1(y, x, z))
f.0-0-0(f.1-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-1-0(y, x, z))
f.0-0-1(f.1-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-1-0(y, x, z))
f.0-1-0(f.1-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-1-1(y, x, z))
f.0-1-1(f.1-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-1-1(y, x, z))
f.0-0-0(f.1-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-1-0(y, x, z))
f.0-0-1(f.1-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-1-0(y, x, z))
f.0-1-0(f.1-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-1-1(y, x, z))
f.0-1-1(f.1-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-1-1(y, x, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F.0-0-0(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-0-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.0-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.0-1-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-0-1(y_2, y_3, a.), x2)
F.0-0-0(f.0-0-1(f.1-1-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-0(f.0-0-1(y_0, y_1, a.), f.1-1-1(y_2, y_3, a.), x2)
POL(F.0-0-0(x1, x2, x3)) = x1 + x2 + x3
POL(a.) = 1
POL(f.0-0-0(x1, x2, x3)) = 0
POL(f.0-0-1(x1, x2, x3)) = 1 + x1 + x2 + x3
POL(f.0-1-0(x1, x2, x3)) = 0
POL(f.0-1-1(x1, x2, x3)) = 1 + x1 + x3
POL(f.1-0-0(x1, x2, x3)) = 0
POL(f.1-0-1(x1, x2, x3)) = 0
POL(f.1-1-0(x1, x2, x3)) = 0
POL(f.1-1-1(x1, x2, x3)) = 0
f.0-0-1(f.0-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-0-0(y, x, z))
f.0-0-1(f.0-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-0-0(y, x, z))
f.0-0-1(f.1-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-1-0(y, x, z))
f.0-0-1(f.1-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-1-0(y, x, z))
f.0-0-0(f.0-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-0-0(y, x, z))
f.0-0-0(f.0-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-0-0(y, x, z))
f.0-0-0(f.1-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-1-0(y, x, z))
f.0-0-0(f.1-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-1-0(y, x, z))
f.0-1-1(f.0-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-0-1(y, x, z))
f.0-1-1(f.0-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-0-1(y, x, z))
f.0-1-1(f.1-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-1-1(y, x, z))
f.0-1-1(f.1-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-1-1(y, x, z))
f.0-1-0(f.0-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-0-1(y, x, z))
f.0-1-0(f.1-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-1-1(y, x, z))
f.0-1-0(f.0-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-0-1(y, x, z))
f.0-1-0(f.1-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-1-1(y, x, z))
f.0-0-0(f.0-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-0-0(y, x, z))
f.0-0-1(f.0-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-0-0(y, x, z))
f.0-1-0(f.0-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-0-1(y, x, z))
f.0-1-1(f.0-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-0-1(y, x, z))
f.0-0-0(f.0-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-0-0(y, x, z))
f.0-0-1(f.0-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-0-0(y, x, z))
f.0-1-0(f.0-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-0-1(y, x, z))
f.0-1-1(f.0-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-0-1(y, x, z))
f.0-0-0(f.1-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-1-0(y, x, z))
f.0-0-1(f.1-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-1-0(y, x, z))
f.0-1-0(f.1-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-1-1(y, x, z))
f.0-1-1(f.1-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-1-1(y, x, z))
f.0-0-0(f.1-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-1-0(y, x, z))
f.0-0-1(f.1-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-1-0(y, x, z))
f.0-1-0(f.1-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-1-1(y, x, z))
f.0-1-1(f.1-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-1-1(y, x, z))
F.0-0-1(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-1-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-1-0(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-1-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.0-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-1-0(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.1-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
f.0-0-0(f.0-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-0-0(y, x, z))
f.0-0-1(f.0-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-0-0(y, x, z))
f.0-1-0(f.0-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-0-1(y, x, z))
f.0-1-1(f.0-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-0-1(y, x, z))
f.0-0-0(f.0-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-0-0(y, x, z))
f.0-0-1(f.0-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-0-0(y, x, z))
f.0-1-0(f.0-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-0-1(y, x, z))
f.0-1-1(f.0-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-0-1(y, x, z))
f.0-0-0(f.1-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-1-0(y, x, z))
f.0-0-1(f.1-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-1-0(y, x, z))
f.0-1-0(f.1-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-1-1(y, x, z))
f.0-1-1(f.1-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-1-1(y, x, z))
f.0-0-0(f.1-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-1-0(y, x, z))
f.0-0-1(f.1-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-1-0(y, x, z))
f.0-1-0(f.1-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-1-1(y, x, z))
f.0-1-1(f.1-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-1-1(y, x, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F.0-0-1(f.0-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.1-0-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
POL(F.0-0-1(x1, x2, x3)) = 1 + x1 + x2
POL(F.0-1-0(x1, x2, x3)) = 1 + x1 + x3
POL(a.) = 1
POL(f.0-0-0(x1, x2, x3)) = 0
POL(f.0-0-1(x1, x2, x3)) = x1 + x2
POL(f.0-1-0(x1, x2, x3)) = x3
POL(f.0-1-1(x1, x2, x3)) = x3
POL(f.1-0-0(x1, x2, x3)) = 0
POL(f.1-0-1(x1, x2, x3)) = 0
POL(f.1-1-0(x1, x2, x3)) = 0
POL(f.1-1-1(x1, x2, x3)) = 0
f.0-0-1(f.0-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-0-0(y, x, z))
f.0-0-1(f.0-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-0-0(y, x, z))
f.0-0-1(f.1-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-1-0(y, x, z))
f.0-0-1(f.1-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-1-0(y, x, z))
f.0-0-0(f.0-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-0-0(y, x, z))
f.0-0-0(f.0-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-0-0(y, x, z))
f.0-0-0(f.1-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-1-0(y, x, z))
f.0-0-0(f.1-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-1-0(y, x, z))
f.0-1-1(f.0-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-0-1(y, x, z))
f.0-1-1(f.0-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-0-1(y, x, z))
f.0-1-1(f.1-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-1-1(y, x, z))
f.0-1-1(f.1-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-1-1(y, x, z))
f.0-1-0(f.0-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-0-1(y, x, z))
f.0-1-0(f.1-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-1-1(y, x, z))
f.0-1-0(f.0-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-0-1(y, x, z))
f.0-1-0(f.1-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-1-1(y, x, z))
F.0-0-1(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-1-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-1-0(f.0-0-1(x0, f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-1-1(y_0, y_1, a.), x0, x2)
F.0-1-0(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.1-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
f.0-0-0(f.0-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-0-0(y, x, z))
f.0-0-1(f.0-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-0-0(y, x, z))
f.0-1-0(f.0-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-0-1(y, x, z))
f.0-1-1(f.0-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-0-1(y, x, z))
f.0-0-0(f.0-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-0-0(y, x, z))
f.0-0-1(f.0-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-0-0(y, x, z))
f.0-1-0(f.0-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-0-1(y, x, z))
f.0-1-1(f.0-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-0-1(y, x, z))
f.0-0-0(f.1-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-1-0(y, x, z))
f.0-0-1(f.1-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-1-0(y, x, z))
f.0-1-0(f.1-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-1-1(y, x, z))
f.0-1-1(f.1-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-1-1(y, x, z))
f.0-0-0(f.1-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-1-0(y, x, z))
f.0-0-1(f.1-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-1-0(y, x, z))
f.0-1-0(f.1-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-1-1(y, x, z))
f.0-1-1(f.1-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-1-1(y, x, z))
F.0-1-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-1-0(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.1-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
f.0-0-0(f.0-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-0-0(y, x, z))
f.0-0-1(f.0-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-0-0(y, x, z))
f.0-1-0(f.0-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-0-1(y, x, z))
f.0-1-1(f.0-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-0-1(y, x, z))
f.0-0-0(f.0-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-0-0(y, x, z))
f.0-0-1(f.0-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-0-0(y, x, z))
f.0-1-0(f.0-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-0-1(y, x, z))
f.0-1-1(f.0-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-0-1(y, x, z))
f.0-0-0(f.1-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-1-0(y, x, z))
f.0-0-1(f.1-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-1-0(y, x, z))
f.0-1-0(f.1-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-1-1(y, x, z))
f.0-1-1(f.1-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-1-1(y, x, z))
f.0-0-0(f.1-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-1-0(y, x, z))
f.0-0-1(f.1-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-1-0(y, x, z))
f.0-1-0(f.1-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-1-1(y, x, z))
f.0-1-1(f.1-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-1-1(y, x, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F.0-1-0(f.0-0-1(x0, f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), x0, x2)
F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.1-1-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.1-1-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
POL(F.0-0-1(x1, x2, x3)) = 1 + x2
POL(F.0-1-0(x1, x2, x3)) = 1 + x1 + x3
POL(a.) = 1
POL(f.0-0-0(x1, x2, x3)) = 0
POL(f.0-0-1(x1, x2, x3)) = x1 + x2
POL(f.0-1-0(x1, x2, x3)) = 0
POL(f.0-1-1(x1, x2, x3)) = 0
POL(f.1-0-0(x1, x2, x3)) = 0
POL(f.1-0-1(x1, x2, x3)) = 0
POL(f.1-1-0(x1, x2, x3)) = 0
POL(f.1-1-1(x1, x2, x3)) = x3
f.0-0-1(f.0-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-0-0(y, x, z))
f.0-0-1(f.0-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-0-0(y, x, z))
f.0-0-1(f.1-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-1-0(y, x, z))
f.0-0-1(f.1-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-1-0(y, x, z))
f.0-0-0(f.0-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-0-0(y, x, z))
f.0-0-0(f.0-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-0-0(y, x, z))
f.0-0-0(f.1-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-1-0(y, x, z))
f.0-0-0(f.1-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-1-0(y, x, z))
f.0-1-0(f.0-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-0-1(y, x, z))
f.0-1-0(f.1-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-1-1(y, x, z))
f.0-1-0(f.0-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-0-1(y, x, z))
f.0-1-0(f.1-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-1-1(y, x, z))
f.0-1-1(f.0-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-0-1(y, x, z))
f.0-1-1(f.1-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-1-1(y, x, z))
F.0-1-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-0-1(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-0-1(f.1-1-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.1-1-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
f.0-0-0(f.0-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-0-0(y, x, z))
f.0-0-1(f.0-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-0-0(y, x, z))
f.0-1-0(f.0-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-0-1(y, x, z))
f.0-1-1(f.0-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-0-1(y, x, z))
f.0-0-0(f.0-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-0-0(y, x, z))
f.0-0-1(f.0-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-0-0(y, x, z))
f.0-1-0(f.0-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-0-1(y, x, z))
f.0-1-1(f.0-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-0-1(y, x, z))
f.0-0-0(f.1-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-1-0(y, x, z))
f.0-0-1(f.1-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-1-0(y, x, z))
f.0-1-0(f.1-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-1-1(y, x, z))
f.0-1-1(f.1-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-1-1(y, x, z))
f.0-0-0(f.1-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-1-0(y, x, z))
f.0-0-1(f.1-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-1-0(y, x, z))
f.0-1-0(f.1-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-1-1(y, x, z))
f.0-1-1(f.1-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-1-1(y, x, z))
F.0-0-1(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
F.0-1-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
f.0-0-0(f.0-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-0-0(y, x, z))
f.0-0-1(f.0-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-0-0(y, x, z))
f.0-1-0(f.0-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-0-1(y, x, z))
f.0-1-1(f.0-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-0-1(y, x, z))
f.0-0-0(f.0-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-0-0(y, x, z))
f.0-0-1(f.0-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-0-0(y, x, z))
f.0-1-0(f.0-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-0-1(y, x, z))
f.0-1-1(f.0-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-0-1(y, x, z))
f.0-0-0(f.1-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-1-0(y, x, z))
f.0-0-1(f.1-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-1-0(y, x, z))
f.0-1-0(f.1-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-1-1(y, x, z))
f.0-1-1(f.1-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-1-1(y, x, z))
f.0-0-0(f.1-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-1-0(y, x, z))
f.0-0-1(f.1-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-1-0(y, x, z))
f.0-1-0(f.1-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-1-1(y, x, z))
f.0-1-1(f.1-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-1-1(y, x, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F.0-0-1(f.0-0-1(x0, x1, a.), f.0-0-1(y_0, y_1, a.), x3) → F.0-1-0(f.0-0-1(y_0, y_1, a.), x3, f.0-0-0(x1, x0, f.0-0-1(y_0, y_1, a.)))
POL(F.0-0-1(x1, x2, x3)) = 1 + x1 + x2
POL(F.0-1-0(x1, x2, x3)) = x1
POL(a.) = 0
POL(f.0-0-0(x1, x2, x3)) = 0
POL(f.0-0-1(x1, x2, x3)) = 1 + x1 + x2 + x3
POL(f.0-1-0(x1, x2, x3)) = 0
POL(f.0-1-1(x1, x2, x3)) = 0
POL(f.1-0-0(x1, x2, x3)) = 0
POL(f.1-0-1(x1, x2, x3)) = x2
POL(f.1-1-0(x1, x2, x3)) = 0
POL(f.1-1-1(x1, x2, x3)) = 0
f.0-0-1(f.0-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-0-0(y, x, z))
f.0-0-1(f.0-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-0-0(y, x, z))
f.0-0-1(f.1-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-1-0(y, x, z))
f.0-0-1(f.1-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-1-0(y, x, z))
f.0-0-0(f.0-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-0-0(y, x, z))
f.0-0-0(f.0-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-0-0(y, x, z))
f.0-0-0(f.1-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-1-0(y, x, z))
f.0-0-0(f.1-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-1-0(y, x, z))
f.0-1-0(f.0-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-0-1(y, x, z))
f.0-1-0(f.1-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-1-1(y, x, z))
f.0-1-0(f.0-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-0-1(y, x, z))
f.0-1-0(f.1-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-1-1(y, x, z))
f.0-1-1(f.0-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-0-1(y, x, z))
f.0-1-1(f.1-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-1-1(y, x, z))
F.0-1-0(f.0-0-1(x0, f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), x0, x2)
F.0-1-0(f.0-0-1(f.0-0-1(y_2, y_3, a.), f.0-0-1(y_0, y_1, a.), a.), x2, x3) → F.0-0-1(f.0-0-1(y_0, y_1, a.), f.0-0-1(y_2, y_3, a.), x2)
f.0-0-0(f.0-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-0-0(y, x, z))
f.0-0-1(f.0-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-0-0(y, x, z))
f.0-1-0(f.0-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-0-1(y, x, z))
f.0-1-1(f.0-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-0-1(y, x, z))
f.0-0-0(f.0-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-0-0(y, x, z))
f.0-0-1(f.0-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-0-0(y, x, z))
f.0-1-0(f.0-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-0-1(y, x, z))
f.0-1-1(f.0-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-0-1(y, x, z))
f.0-0-0(f.1-0-1(x, y, a.), z, w) → f.0-0-0(z, w, f.0-1-0(y, x, z))
f.0-0-1(f.1-0-1(x, y, a.), z, w) → f.0-1-0(z, w, f.0-1-0(y, x, z))
f.0-1-0(f.1-0-1(x, y, a.), z, w) → f.1-0-0(z, w, f.0-1-1(y, x, z))
f.0-1-1(f.1-0-1(x, y, a.), z, w) → f.1-1-0(z, w, f.0-1-1(y, x, z))
f.0-0-0(f.1-1-1(x, y, a.), z, w) → f.0-0-0(z, w, f.1-1-0(y, x, z))
f.0-0-1(f.1-1-1(x, y, a.), z, w) → f.0-1-0(z, w, f.1-1-0(y, x, z))
f.0-1-0(f.1-1-1(x, y, a.), z, w) → f.1-0-0(z, w, f.1-1-1(y, x, z))
f.0-1-1(f.1-1-1(x, y, a.), z, w) → f.1-1-0(z, w, f.1-1-1(y, x, z))