YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

Begin(a(b(b(a(b(a(x0)))))))	→	Wait(Right1(x0))
Begin(b(b(a(b(a(x0))))))	→	Wait(Right2(x0))
Begin(b(a(b(a(x0)))))	→	Wait(Right3(x0))
Begin(a(b(a(x0))))	→	Wait(Right4(x0))
Begin(b(a(x0)))	→	Wait(Right5(x0))
Begin(a(x0))	→	Wait(Right6(x0))
Right1(b(End(x0)))	→	Left(a(b(a(a(b(b(a(b(b(a(End(x0))))))))))))
Right2(b(a(End(x0))))	→	Left(a(b(a(a(b(b(a(b(b(a(End(x0))))))))))))
Right3(b(a(b(End(x0)))))	→	Left(a(b(a(a(b(b(a(b(b(a(End(x0))))))))))))
Right4(b(a(b(b(End(x0))))))	→	Left(a(b(a(a(b(b(a(b(b(a(End(x0))))))))))))
Right5(b(a(b(b(a(End(x0)))))))	→	Left(a(b(a(a(b(b(a(b(b(a(End(x0))))))))))))
Right6(b(a(b(b(a(b(End(x0))))))))	→	Left(a(b(a(a(b(b(a(b(b(a(End(x0))))))))))))
Right1(b(x0))	→	Ab(Right1(x0))
Right2(b(x0))	→	Ab(Right2(x0))
Right3(b(x0))	→	Ab(Right3(x0))
Right4(b(x0))	→	Ab(Right4(x0))
Right5(b(x0))	→	Ab(Right5(x0))
Right6(b(x0))	→	Ab(Right6(x0))
Right1(a(x0))	→	Aa(Right1(x0))
Right2(a(x0))	→	Aa(Right2(x0))
Right3(a(x0))	→	Aa(Right3(x0))
Right4(a(x0))	→	Aa(Right4(x0))
Right5(a(x0))	→	Aa(Right5(x0))
Right6(a(x0))	→	Aa(Right6(x0))
Ab(Left(x0))	→	Left(b(x0))
Aa(Left(x0))	→	Left(a(x0))
Wait(Left(x0))	→	Begin(x0)
b(a(b(b(a(b(a(x0)))))))	→	a(b(a(a(b(b(a(b(b(a(x0))))))))))

Proof

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

Begin^#(a(b(b(a(b(a(x0)))))))	→	Right1^#(x0)
Begin^#(a(b(b(a(b(a(x0)))))))	→	Wait^#(Right1(x0))
Begin^#(b(b(a(b(a(x0))))))	→	Right2^#(x0)
Begin^#(b(b(a(b(a(x0))))))	→	Wait^#(Right2(x0))
Begin^#(b(a(b(a(x0)))))	→	Right3^#(x0)
Begin^#(b(a(b(a(x0)))))	→	Wait^#(Right3(x0))
Begin^#(a(b(a(x0))))	→	Right4^#(x0)
Begin^#(a(b(a(x0))))	→	Wait^#(Right4(x0))
Begin^#(b(a(x0)))	→	Right5^#(x0)
Begin^#(b(a(x0)))	→	Wait^#(Right5(x0))
Begin^#(a(x0))	→	Right6^#(x0)
Begin^#(a(x0))	→	Wait^#(Right6(x0))
Right1^#(b(End(x0)))	→	b^#(a(End(x0)))
Right1^#(b(End(x0)))	→	b^#(b(a(End(x0))))
Right1^#(b(End(x0)))	→	b^#(a(b(b(a(End(x0))))))
Right1^#(b(End(x0)))	→	b^#(b(a(b(b(a(End(x0)))))))
Right1^#(b(End(x0)))	→	b^#(a(a(b(b(a(b(b(a(End(x0))))))))))
Right2^#(b(a(End(x0))))	→	b^#(b(a(End(x0))))
Right2^#(b(a(End(x0))))	→	b^#(a(b(b(a(End(x0))))))
Right2^#(b(a(End(x0))))	→	b^#(b(a(b(b(a(End(x0)))))))
Right2^#(b(a(End(x0))))	→	b^#(a(a(b(b(a(b(b(a(End(x0))))))))))
Right3^#(b(a(b(End(x0)))))	→	b^#(a(End(x0)))
Right3^#(b(a(b(End(x0)))))	→	b^#(b(a(End(x0))))
Right3^#(b(a(b(End(x0)))))	→	b^#(a(b(b(a(End(x0))))))
Right3^#(b(a(b(End(x0)))))	→	b^#(b(a(b(b(a(End(x0)))))))
Right3^#(b(a(b(End(x0)))))	→	b^#(a(a(b(b(a(b(b(a(End(x0))))))))))
Right4^#(b(a(b(b(End(x0))))))	→	b^#(a(End(x0)))
Right4^#(b(a(b(b(End(x0))))))	→	b^#(b(a(End(x0))))
Right4^#(b(a(b(b(End(x0))))))	→	b^#(a(b(b(a(End(x0))))))
Right4^#(b(a(b(b(End(x0))))))	→	b^#(b(a(b(b(a(End(x0)))))))
Right4^#(b(a(b(b(End(x0))))))	→	b^#(a(a(b(b(a(b(b(a(End(x0))))))))))
Right5^#(b(a(b(b(a(End(x0)))))))	→	b^#(b(a(b(b(a(End(x0)))))))
Right5^#(b(a(b(b(a(End(x0)))))))	→	b^#(a(a(b(b(a(b(b(a(End(x0))))))))))
Right6^#(b(a(b(b(a(b(End(x0))))))))	→	b^#(a(End(x0)))
Right6^#(b(a(b(b(a(b(End(x0))))))))	→	b^#(b(a(End(x0))))
Right6^#(b(a(b(b(a(b(End(x0))))))))	→	b^#(a(b(b(a(End(x0))))))
Right6^#(b(a(b(b(a(b(End(x0))))))))	→	b^#(b(a(b(b(a(End(x0)))))))
Right6^#(b(a(b(b(a(b(End(x0))))))))	→	b^#(a(a(b(b(a(b(b(a(End(x0))))))))))
Right1^#(b(x0))	→	Right1^#(x0)
Right1^#(b(x0))	→	Ab^#(Right1(x0))
Right2^#(b(x0))	→	Right2^#(x0)
Right2^#(b(x0))	→	Ab^#(Right2(x0))
Right3^#(b(x0))	→	Right3^#(x0)
Right3^#(b(x0))	→	Ab^#(Right3(x0))
Right4^#(b(x0))	→	Right4^#(x0)
Right4^#(b(x0))	→	Ab^#(Right4(x0))
Right5^#(b(x0))	→	Right5^#(x0)
Right5^#(b(x0))	→	Ab^#(Right5(x0))
Right6^#(b(x0))	→	Right6^#(x0)
Right6^#(b(x0))	→	Ab^#(Right6(x0))
Right1^#(a(x0))	→	Right1^#(x0)
Right1^#(a(x0))	→	Aa^#(Right1(x0))
Right2^#(a(x0))	→	Right2^#(x0)
Right2^#(a(x0))	→	Aa^#(Right2(x0))
Right3^#(a(x0))	→	Right3^#(x0)
Right3^#(a(x0))	→	Aa^#(Right3(x0))
Right4^#(a(x0))	→	Right4^#(x0)
Right4^#(a(x0))	→	Aa^#(Right4(x0))
Right5^#(a(x0))	→	Right5^#(x0)
Right5^#(a(x0))	→	Aa^#(Right5(x0))
Right6^#(a(x0))	→	Right6^#(x0)
Right6^#(a(x0))	→	Aa^#(Right6(x0))
Ab^#(Left(x0))	→	b^#(x0)
Wait^#(Left(x0))	→	Begin^#(x0)
b^#(a(b(b(a(b(a(x0)))))))	→	b^#(b(a(x0)))
b^#(a(b(b(a(b(a(x0)))))))	→	b^#(a(b(b(a(x0)))))
b^#(a(b(b(a(b(a(x0)))))))	→	b^#(b(a(b(b(a(x0))))))
b^#(a(b(b(a(b(a(x0)))))))	→	b^#(a(a(b(b(a(b(b(a(x0)))))))))

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pairs

Wait^#(Left(x0))	→	Begin^#(x0)
Begin^#(a(b(b(a(b(a(x0)))))))	→	Wait^#(Right1(x0))
Begin^#(b(b(a(b(a(x0))))))	→	Wait^#(Right2(x0))
Begin^#(b(a(b(a(x0)))))	→	Wait^#(Right3(x0))
Begin^#(a(b(a(x0))))	→	Wait^#(Right4(x0))
Begin^#(b(a(x0)))	→	Wait^#(Right5(x0))
Begin^#(a(x0))	→	Wait^#(Right6(x0))

1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over (4 x 4)-matrices with strict dimension 1 over the naturals

[Right5(x₁)]

0	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

· x₁ +

1	0	0	0
1	0	0	0
0	0	0	0
1	0	0	0

[b(x₁)]

0	0	0
0	0	0
1	0	0
0	1	1

· x₁ +

0	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

[Right1(x₁)]

0	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

· x₁ +

1	0	0	0
1	0	0	0
0	0	0	0
1	0	0	0

[Wait^#(x₁)]

1	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

· x₁ +

0	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

[Right2(x₁)]

0	1	1
1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0	0
1	0	0	0
0	0	0	0
1	0	0	0

[End(x₁)]

0	0	0	0
0	0	1	0
0	0	0	0
0	0	0	0

· x₁ +

0	0	0	0
1	0	0	0
0	0	0	0
0	0	0	0

[a(x₁)]

0	0	1	0
0	0	0	0
0	0	0	0
0	0	1	1

· x₁ +

0	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

[Right4(x₁)]

0	0	1	1
0	0	0	1
0	0	0	0
0	0	0	1

· x₁ +

0	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

[Begin^#(x₁)]

0	0	0	1
0	0	0	0
0	0	0	0
0	0	0	0

· x₁ +

1	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

[Ab(x₁)]

0	0	0	1
0	0	0	1
0	0	1	0
0	0	0	1

· x₁ +

0	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

[Left(x₁)]

0	1	1
0	0	1
1	1	0
1	1	1

· x₁ +

1	0	0	0
0	0	0	0
0	0	0	0
1	0	0	0

[Right6(x₁)]

0	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

· x₁ +

1	0	0	0
1	0	0	0
0	0	0	0
1	0	0	0

[Aa(x₁)]

1	0	0
0	0	1
0	1	0
0	0	1

· x₁ +

0	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

[Right3(x₁)]

0	0	1	1
0	0	0	1
0	0	0	0
0	0	0	1

· x₁ +

0	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

together with the usable rules

Right1(b(End(x0)))	→	Left(a(b(a(a(b(b(a(b(b(a(End(x0))))))))))))
Right1(b(x0))	→	Ab(Right1(x0))
Right1(a(x0))	→	Aa(Right1(x0))
Ab(Left(x0))	→	Left(b(x0))
b(a(b(b(a(b(a(x0)))))))	→	a(b(a(a(b(b(a(b(b(a(x0))))))))))
Aa(Left(x0))	→	Left(a(x0))
Right2(b(a(End(x0))))	→	Left(a(b(a(a(b(b(a(b(b(a(End(x0))))))))))))
Right2(b(x0))	→	Ab(Right2(x0))
Right2(a(x0))	→	Aa(Right2(x0))
Right3(b(a(b(End(x0)))))	→	Left(a(b(a(a(b(b(a(b(b(a(End(x0))))))))))))
Right3(b(x0))	→	Ab(Right3(x0))
Right3(a(x0))	→	Aa(Right3(x0))
Right4(b(a(b(b(End(x0))))))	→	Left(a(b(a(a(b(b(a(b(b(a(End(x0))))))))))))
Right4(b(x0))	→	Ab(Right4(x0))
Right4(a(x0))	→	Aa(Right4(x0))
Right5(b(a(b(b(a(End(x0)))))))	→	Left(a(b(a(a(b(b(a(b(b(a(End(x0))))))))))))
Right5(b(x0))	→	Ab(Right5(x0))
Right5(a(x0))	→	Aa(Right5(x0))
Right6(b(a(b(b(a(b(End(x0))))))))	→	Left(a(b(a(a(b(b(a(b(b(a(End(x0))))))))))))
Right6(b(x0))	→	Ab(Right6(x0))
Right6(a(x0))	→	Aa(Right6(x0))

(w.r.t. the implicit argument filter of the reduction pair), the pairs

Wait^#(Left(x0))	→	Begin^#(x0)
Begin^#(a(b(b(a(b(a(x0)))))))	→	Wait^#(Right1(x0))
Begin^#(b(b(a(b(a(x0))))))	→	Wait^#(Right2(x0))
Begin^#(b(a(x0)))	→	Wait^#(Right5(x0))
Begin^#(a(x0))	→	Wait^#(Right6(x0))

remain.

1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over (4 x 4)-matrices with strict dimension 1 over the naturals

[Right5(x₁)]

0	0	0	0
1	0	0	0
0	0	0	1
0	0	0	0

· x₁ +

1	0	0	0
1	0	0	0
1	0	0	0
0	0	0	0

[b(x₁)]

0	0	0	0
1	0	0	1
0	0	0	0
1	0	0	1

· x₁ +

0	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

[Right1(x₁)]

0	0	0	1
0	0	0	1
0	1	0	0
0	0	0	0

· x₁ +

0	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

[Wait^#(x₁)]

1	0	0	1
0	0	0	0
0	0	0	0
0	0	0	0

· x₁ +

0	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

[Right2(x₁)]

0	0	0
1	0	1
0	1	0
0	0	0

· x₁ +

1	0	0	0
1	0	0	0
1	0	0	0
0	0	0	0

[End(x₁)]

0	0	0	0
1	0	0	1
0	0	0	0
0	0	0	0

· x₁ +

1	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

[a(x₁)]

0	0	0	0
0	1	0	0
0	0	0	0
0	0	0	1

· x₁ +

0	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

[Begin^#(x₁)]

0	0	0	1
0	0	0	0
0	0	0	0
0	0	0	0

· x₁ +

1	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

[Ab(x₁)]

1	0	1
0	0	1
0	1	0
0	0	1

· x₁ +

0	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

[Left(x₁)]

0	1	0
1	0	0
0	0	0
1	0	1

· x₁ +

1	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

[Right6(x₁)]

0	0	0	1
0	0	0	1
0	0	0	1
0	0	0	0

· x₁ +

0	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

[Aa(x₁)]

1	0	0	0
1	0	0	0
0	0	0	0
0	0	0	1

· x₁ +

0	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

together with the usable rules

Right1(b(End(x0)))	→	Left(a(b(a(a(b(b(a(b(b(a(End(x0))))))))))))
Right1(b(x0))	→	Ab(Right1(x0))
Right1(a(x0))	→	Aa(Right1(x0))
Ab(Left(x0))	→	Left(b(x0))
b(a(b(b(a(b(a(x0)))))))	→	a(b(a(a(b(b(a(b(b(a(x0))))))))))
Aa(Left(x0))	→	Left(a(x0))
Right2(b(a(End(x0))))	→	Left(a(b(a(a(b(b(a(b(b(a(End(x0))))))))))))
Right2(b(x0))	→	Ab(Right2(x0))
Right2(a(x0))	→	Aa(Right2(x0))
Right5(b(a(b(b(a(End(x0)))))))	→	Left(a(b(a(a(b(b(a(b(b(a(End(x0))))))))))))
Right5(b(x0))	→	Ab(Right5(x0))
Right5(a(x0))	→	Aa(Right5(x0))
Right6(b(a(b(b(a(b(End(x0))))))))	→	Left(a(b(a(a(b(b(a(b(b(a(End(x0))))))))))))
Right6(b(x0))	→	Ab(Right6(x0))
Right6(a(x0))	→	Aa(Right6(x0))

(w.r.t. the implicit argument filter of the reduction pair), the pairs

Wait^#(Left(x0))	→	Begin^#(x0)
Begin^#(b(b(a(b(a(x0))))))	→	Wait^#(Right2(x0))
Begin^#(b(a(x0)))	→	Wait^#(Right5(x0))

remain.

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals

[Right5(x₁)]

1	0	0
0	1	1
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[b(x₁)]

0	0	1
0	0	1
0	1	1

· x₁ +

0	0	0
0	0	0
0	0	0

[Wait^#(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Right2(x₁)]

1	0	0
0	1	1
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[End(x₁)]

0	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a(x₁)]

0	0	0
0	0	0
1	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

[Begin^#(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Ab(x₁)]

0	0	1
0	1	1
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Left(x₁)]

1	0	0
0	1	1
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[Aa(x₁)]

0	0	0
1	0	0
1	0	0

· x₁ +

0	0	0
1	0	0
0	0	0

together with the usable rules

Right2(b(a(End(x0))))	→	Left(a(b(a(a(b(b(a(b(b(a(End(x0))))))))))))
Right2(b(x0))	→	Ab(Right2(x0))
Right2(a(x0))	→	Aa(Right2(x0))
Ab(Left(x0))	→	Left(b(x0))
b(a(b(b(a(b(a(x0)))))))	→	a(b(a(a(b(b(a(b(b(a(x0))))))))))
Aa(Left(x0))	→	Left(a(x0))
Right5(b(a(b(b(a(End(x0)))))))	→	Left(a(b(a(a(b(b(a(b(b(a(End(x0))))))))))))
Right5(b(x0))	→	Ab(Right5(x0))
Right5(a(x0))	→	Aa(Right5(x0))

(w.r.t. the implicit argument filter of the reduction pair), the pairs

Wait^#(Left(x0))	→	Begin^#(x0)
Begin^#(b(a(x0)))	→	Wait^#(Right5(x0))

remain.

1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals

[Right5(x₁)]

0	0	0
1	0	0
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[b(x₁)]

0	1	0
0	1	0
0	0	1

· x₁ +

1	0	0
0	0	0
0	0	0

[Wait^#(x₁)]

0	1	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[End(x₁)]

1	0	0
0	0	0
1	0	0

· x₁ +

0	0	0
0	0	0
1	0	0

[a(x₁)]

0	0	0
1	0	0
0	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

[Begin^#(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Ab(x₁)]

0	0	0
0	0	1
0	0	1

· x₁ +

0	0	0
1	0	0
0	0	0

[Left(x₁)]

0	0	0
1	0	0
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

[Aa(x₁)]

0	0	0
0	0	0
0	1	0

· x₁ +

0	0	0
0	0	0
0	0	0

together with the usable rules

Right5(b(a(b(b(a(End(x0)))))))	→	Left(a(b(a(a(b(b(a(b(b(a(End(x0))))))))))))
Right5(b(x0))	→	Ab(Right5(x0))
Right5(a(x0))	→	Aa(Right5(x0))
Ab(Left(x0))	→	Left(b(x0))
b(a(b(b(a(b(a(x0)))))))	→	a(b(a(a(b(b(a(b(b(a(x0))))))))))
Aa(Left(x0))	→	Left(a(x0))

(w.r.t. the implicit argument filter of the reduction pair), the pair

Wait^#(Left(x0))

→

Begin^#(x0)

remains.

1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.