Certification Problem

Input (TPDB SRS_Standard/Waldmann_06_SRS/sym-6)

The rewrite relation of the following TRS is considered.

c(c(c(c(x1)))) → b(b(b(b(x1)))) (1)
b(b(x1)) → x1 (2)
b(b(x1)) → c(b(c(x1))) (3)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by matchbox @ termCOMP 2023)

1 Closure Under Flat Contexts

Using the flat contexts

{c(☐), b(☐)}

We obtain the transformed TRS
c(c(c(c(c(x1))))) → c(b(b(b(b(x1))))) (4)
c(b(b(x1))) → c(x1) (5)
c(b(b(x1))) → c(c(b(c(x1)))) (6)
b(c(c(c(c(x1))))) → b(b(b(b(b(x1))))) (7)
b(b(b(x1))) → b(x1) (8)
b(b(b(x1))) → b(c(b(c(x1)))) (9)

1.1 Semantic Labeling

The following interpretations form a model of the rules.

As carrier we take the set {0,1}. Symbols are labeled by the interpretation of their arguments using the interpretations (modulo 2):

[c(x1)] = 2x1 + 0
[b(x1)] = 2x1 + 1

We obtain the labeled TRS
c0(c0(c0(c0(c0(x1))))) → c1(b1(b1(b1(b0(x1))))) (10)
c0(c0(c0(c0(c1(x1))))) → c1(b1(b1(b1(b1(x1))))) (11)
b0(c0(c0(c0(c0(x1))))) → b1(b1(b1(b1(b0(x1))))) (12)
b0(c0(c0(c0(c1(x1))))) → b1(b1(b1(b1(b1(x1))))) (13)
c1(b1(b0(x1))) → c0(x1) (14)
c1(b1(b1(x1))) → c1(x1) (15)
b1(b1(b0(x1))) → b0(x1) (16)
b1(b1(b1(x1))) → b1(x1) (17)
c1(b1(b0(x1))) → c0(c1(b0(c0(x1)))) (18)
c1(b1(b1(x1))) → c0(c1(b0(c1(x1)))) (19)
b1(b1(b0(x1))) → b0(c1(b0(c0(x1)))) (20)
b1(b1(b1(x1))) → b0(c1(b0(c1(x1)))) (21)

1.1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
c0(c0(c0(c0(c0(x1))))) → b0(b1(b1(b1(c1(x1))))) (22)
c1(c0(c0(c0(c0(x1))))) → b1(b1(b1(b1(c1(x1))))) (23)
c0(c0(c0(c0(b0(x1))))) → b0(b1(b1(b1(b1(x1))))) (24)
c1(c0(c0(c0(b0(x1))))) → b1(b1(b1(b1(b1(x1))))) (25)
b0(b1(c1(x1))) → c0(x1) (26)
b1(b1(c1(x1))) → c1(x1) (27)
b0(b1(b1(x1))) → b0(x1) (28)
b1(b1(b1(x1))) → b1(x1) (17)
b0(b1(c1(x1))) → c0(b0(c1(c0(x1)))) (29)
b1(b1(c1(x1))) → c1(b0(c1(c0(x1)))) (30)
b0(b1(b1(x1))) → c0(b0(c1(b0(x1)))) (31)
b1(b1(b1(x1))) → c1(b0(c1(b0(x1)))) (32)

1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
c0#(c0(c0(c0(c0(x1))))) → c1#(x1) (33)
c0#(c0(c0(c0(c0(x1))))) → b0#(b1(b1(b1(c1(x1))))) (34)
c0#(c0(c0(c0(c0(x1))))) → b1#(c1(x1)) (35)
c0#(c0(c0(c0(c0(x1))))) → b1#(b1(c1(x1))) (36)
c0#(c0(c0(c0(c0(x1))))) → b1#(b1(b1(c1(x1)))) (37)
c0#(c0(c0(c0(b0(x1))))) → b0#(b1(b1(b1(b1(x1))))) (38)
c0#(c0(c0(c0(b0(x1))))) → b1#(x1) (39)
c0#(c0(c0(c0(b0(x1))))) → b1#(b1(x1)) (40)
c0#(c0(c0(c0(b0(x1))))) → b1#(b1(b1(x1))) (41)
c0#(c0(c0(c0(b0(x1))))) → b1#(b1(b1(b1(x1)))) (42)
c1#(c0(c0(c0(c0(x1))))) → c1#(x1) (43)
c1#(c0(c0(c0(c0(x1))))) → b1#(c1(x1)) (44)
c1#(c0(c0(c0(c0(x1))))) → b1#(b1(c1(x1))) (45)
c1#(c0(c0(c0(c0(x1))))) → b1#(b1(b1(c1(x1)))) (46)
c1#(c0(c0(c0(c0(x1))))) → b1#(b1(b1(b1(c1(x1))))) (47)
c1#(c0(c0(c0(b0(x1))))) → b1#(x1) (48)
c1#(c0(c0(c0(b0(x1))))) → b1#(b1(x1)) (49)
c1#(c0(c0(c0(b0(x1))))) → b1#(b1(b1(x1))) (50)
c1#(c0(c0(c0(b0(x1))))) → b1#(b1(b1(b1(x1)))) (51)
c1#(c0(c0(c0(b0(x1))))) → b1#(b1(b1(b1(b1(x1))))) (52)
b0#(b1(c1(x1))) → c0#(x1) (53)
b0#(b1(c1(x1))) → c0#(b0(c1(c0(x1)))) (54)
b0#(b1(c1(x1))) → c1#(c0(x1)) (55)
b0#(b1(c1(x1))) → b0#(c1(c0(x1))) (56)
b0#(b1(b1(x1))) → c0#(b0(c1(b0(x1)))) (57)
b0#(b1(b1(x1))) → c1#(b0(x1)) (58)
b0#(b1(b1(x1))) → b0#(x1) (59)
b0#(b1(b1(x1))) → b0#(c1(b0(x1))) (60)
b1#(b1(c1(x1))) → c0#(x1) (61)
b1#(b1(c1(x1))) → c1#(c0(x1)) (62)
b1#(b1(c1(x1))) → c1#(b0(c1(c0(x1)))) (63)
b1#(b1(c1(x1))) → b0#(c1(c0(x1))) (64)
b1#(b1(b1(x1))) → c1#(b0(x1)) (65)
b1#(b1(b1(x1))) → c1#(b0(c1(b0(x1)))) (66)
b1#(b1(b1(x1))) → b0#(x1) (67)
b1#(b1(b1(x1))) → b0#(c1(b0(x1))) (68)

1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.