YES Termination w.r.t. Q proof of /home/cern_httpd/provide/research/cycsrs/tpdb/TPDB-d9b80194f163/SRS_Standard/Zantema_04/z001.srs

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

a(a(b(b(x)))) → b(b(b(a(a(a(x))))))

Q is empty.

(1) RFCMatchBoundsTRSProof (EQUIVALENT transformation)

Termination of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 4. This implies Q-termination of R.
The following rules were used to construct the certificate:

a(a(b(b(x)))) → b(b(b(a(a(a(x))))))

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

1, 2, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84

Node 1 is start node and node 2 is final node.

Those nodes are connected through the following edges:

  • 1 to 40 labelled b_1(0)
  • 2 to 2 labelled #_1(0)
  • 40 to 41 labelled b_1(0)
  • 41 to 42 labelled b_1(0)
  • 42 to 43 labelled a_1(0)
  • 42 to 50 labelled b_1(1)
  • 43 to 44 labelled a_1(0)
  • 43 to 45 labelled b_1(1)
  • 44 to 2 labelled a_1(0)
  • 44 to 45 labelled b_1(1)
  • 45 to 46 labelled b_1(1)
  • 46 to 47 labelled b_1(1)
  • 47 to 48 labelled a_1(1)
  • 47 to 55 labelled b_1(2)
  • 48 to 49 labelled a_1(1)
  • 48 to 45 labelled b_1(1)
  • 49 to 2 labelled a_1(1)
  • 49 to 45 labelled b_1(1)
  • 50 to 51 labelled b_1(1)
  • 51 to 52 labelled b_1(1)
  • 52 to 53 labelled a_1(1)
  • 53 to 54 labelled a_1(1)
  • 53 to 65 labelled b_1(2)
  • 54 to 46 labelled a_1(1)
  • 55 to 56 labelled b_1(2)
  • 56 to 57 labelled b_1(2)
  • 57 to 58 labelled a_1(2)
  • 58 to 59 labelled a_1(2)
  • 58 to 65 labelled b_1(2)
  • 59 to 46 labelled a_1(2)
  • 65 to 66 labelled b_1(2)
  • 66 to 67 labelled b_1(2)
  • 67 to 68 labelled a_1(2)
  • 68 to 69 labelled a_1(2)
  • 68 to 70 labelled b_1(3)
  • 69 to 55 labelled a_1(2)
  • 70 to 71 labelled b_1(3)
  • 71 to 72 labelled b_1(3)
  • 72 to 73 labelled a_1(3)
  • 72 to 80 labelled b_1(4)
  • 73 to 74 labelled a_1(3)
  • 74 to 57 labelled a_1(3)
  • 74 to 75 labelled b_1(3)
  • 75 to 76 labelled b_1(3)
  • 76 to 77 labelled b_1(3)
  • 77 to 78 labelled a_1(3)
  • 78 to 79 labelled a_1(3)
  • 79 to 66 labelled a_1(3)
  • 80 to 81 labelled b_1(4)
  • 81 to 82 labelled b_1(4)
  • 82 to 83 labelled a_1(4)
  • 83 to 84 labelled a_1(4)
  • 84 to 76 labelled a_1(4)

(2) YES