YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

Begin(b(b(a(a(b(x0))))))	→	Wait(Right1(x0))
Begin(b(a(a(b(x0)))))	→	Wait(Right2(x0))
Begin(a(a(b(x0))))	→	Wait(Right3(x0))
Begin(a(b(x0)))	→	Wait(Right4(x0))
Begin(b(x0))	→	Wait(Right5(x0))
Right1(a(End(x0)))	→	Left(a(a(b(b(a(b(a(End(x0)))))))))
Right2(a(b(End(x0))))	→	Left(a(a(b(b(a(b(a(End(x0)))))))))
Right3(a(b(b(End(x0)))))	→	Left(a(a(b(b(a(b(a(End(x0)))))))))
Right4(a(b(b(a(End(x0))))))	→	Left(a(a(b(b(a(b(a(End(x0)))))))))
Right5(a(b(b(a(a(End(x0)))))))	→	Left(a(a(b(b(a(b(a(End(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))
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))
Aa(Left(x0))	→	Left(a(x0))
Ab(Left(x0))	→	Left(b(x0))
Wait(Left(x0))	→	Begin(x0)
a(b(b(a(a(b(x0))))))	→	a(a(b(b(a(b(a(x0)))))))

Proof

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS

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

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

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

1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pairs

End^#(a(Right1(x0)))	→	End^#(a(b(a(b(b(a(a(Left(x0)))))))))
End^#(a(a(b(b(a(Right5(x0)))))))	→	End^#(a(b(a(b(b(a(a(Left(x0)))))))))
End^#(a(b(b(a(Right4(x0))))))	→	End^#(a(b(a(b(b(a(a(Left(x0)))))))))
End^#(b(b(a(Right3(x0)))))	→	End^#(a(b(a(b(b(a(a(Left(x0)))))))))
End^#(b(a(Right2(x0))))	→	End^#(a(b(a(b(b(a(a(Left(x0)))))))))

1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight function

prec(End^#)	=	0	weight(End^#)	=	0
prec(Ab)	=	12	weight(Ab)	=	1
prec(Aa)	=	0	weight(Aa)	=	1
prec(Left)	=	0	weight(Left)	=	1
prec(Right5)	=	0	weight(Right5)	=	1
prec(Right4)	=	0	weight(Right4)	=	0
prec(Right3)	=	12	weight(Right3)	=	0
prec(Right2)	=	0	weight(Right2)	=	0
prec(Wait)	=	0	weight(Wait)	=	0
prec(Right1)	=	0	weight(Right1)	=	0
prec(Begin)	=	0	weight(Begin)	=	0
prec(a)	=	1	weight(a)	=	1
prec(b)	=	0	weight(b)	=	1

in combination with the following argument filter

π(End^#) = 1

π(Ab) = []

π(Aa) = []

π(Left) = []

π(Right5) = []

π(Right4) = 1

π(Right3) = 1

π(Right2) = 1

π(Wait) = 1

π(Right1) = 1

π(Begin) = 1

π(a) = []

π(b) = [1]

together with the usable rules

a(Right1(x0))	→	Right1(Aa(x0))
a(Right2(x0))	→	Right2(Aa(x0))
a(Right3(x0))	→	Right3(Aa(x0))
a(Right4(x0))	→	Right4(Aa(x0))
a(Right5(x0))	→	Right5(Aa(x0))

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

End^#(a(Right1(x0)))	→	End^#(a(b(a(b(b(a(a(Left(x0)))))))))
End^#(a(a(b(b(a(Right5(x0)))))))	→	End^#(a(b(a(b(b(a(a(Left(x0)))))))))
End^#(a(b(b(a(Right4(x0))))))	→	End^#(a(b(a(b(b(a(a(Left(x0)))))))))

remain.

1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pairs

End^#(a(Right1(x0)))	→	End^#(a(b(a(b(b(a(a(Left(x0)))))))))
End^#(a(a(b(b(a(Right5(x0)))))))	→	End^#(a(b(a(b(b(a(a(Left(x0)))))))))

1.1.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

[Wait(x₁)]

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

· x₁ +

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

[Right5(x₁)]

0	0	0	1
0	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

[a(x₁)]

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

· x₁ +

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

[Right1(x₁)]

0	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	0	0	1
0	0	0	0
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

[Left(x₁)]

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

· x₁ +

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

[b(x₁)]

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

· x₁ +

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

[Right4(x₁)]

0	0	0	1
0	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

[End^#(x₁)]

0	0	1	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

[Ab(x₁)]

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

· x₁ +

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

[Aa(x₁)]

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

· x₁ +

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

[Right3(x₁)]

0	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

[Begin(x₁)]

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

· x₁ +

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

together with the usable rules

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

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

End^#(a(Right1(x0)))

→

End^#(a(b(a(b(b(a(a(Left(x0)))))))))

remains.

1.1.1.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

[Wait(x₁)]

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

· x₁ +

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

[Right5(x₁)]

0	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

[a(x₁)]

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

· 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	0
1	0	0	0
0	1	1	0

· x₁ +

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

[Right2(x₁)]

0	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

[Left(x₁)]

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

· x₁ +

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

[b(x₁)]

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

· x₁ +

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

[Right4(x₁)]

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

· x₁ +

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

[End^#(x₁)]

0	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

[Ab(x₁)]

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

· x₁ +

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

[Aa(x₁)]

0	0	0	0
0	0	0	0
0	0	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	0	0
0	1	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

[Begin(x₁)]

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

· x₁ +

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

together with the usable rules

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

(w.r.t. the implicit argument filter of the reduction pair), all pairs could be removed.

1.1.1.1.1.1.1.1 P is empty

There are no pairs anymore.

π(End^#)	=	1
π(Ab)	=	[]
π(Aa)	=	[]
π(Left)	=	[]
π(Right5)	=	[]
π(Right4)	=	1
π(Right3)	=	1
π(Right2)	=	1
π(Wait)	=	1
π(Right1)	=	1
π(Begin)	=	1
π(a)	=	[]
π(b)	=	[1]