Left Termination proof of /tmp/tmpqD3vpD/ackermann-ioi.pl

Left Termination of the query pattern ackermann_in_3(g, a, g) w.r.t. the given Prolog program could not be shown:

0 Prolog

  ↳1 PrologToPiTRSProof (⇐)

    ↳2 PiTRS

    ↳3 DependencyPairsProof (⇔)

    ↳4 PiDP

    ↳5 DependencyGraphProof (⇔)

    ↳6 AND

      ↳7 PiDP

        ↳8 UsableRulesProof (⇔)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇐)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔)

        ↳13 TRUE

      ↳14 PiDP

        ↳15 UsableRulesProof (⇔)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇐)

        ↳18 QDP

        ↳19 QDPOrderProof (⇔)

        ↳20 QDP

        ↳21 DependencyGraphProof (⇔)

        ↳22 QDP

        ↳23 UsableRulesProof (⇔)

        ↳24 QDP

        ↳25 QReductionProof (⇔)

        ↳26 QDP

        ↳27 NonTerminationProof (⇔)

        ↳28 FALSE

      ↳29 PiDP

        ↳30 UsableRulesProof (⇔)

        ↳31 PiDP

        ↳32 PiDPToQDPProof (⇐)

        ↳33 QDP

        ↳34 QDPSizeChangeProof (⇔)

        ↳35 TRUE

      ↳36 PiDP

        ↳37 UsableRulesProof (⇔)

        ↳38 PiDP

        ↳39 PiDPToQDPProof (⇐)

        ↳40 QDP

        ↳41 QDPSizeChangeProof (⇔)

        ↳42 TRUE

  ↳43 PrologToPiTRSProof (⇐)

    ↳44 PiTRS

    ↳45 DependencyPairsProof (⇔)

    ↳46 PiDP

    ↳47 DependencyGraphProof (⇔)

    ↳48 AND

      ↳49 PiDP

        ↳50 UsableRulesProof (⇔)

        ↳51 PiDP

        ↳52 PiDPToQDPProof (⇐)

        ↳53 QDP

        ↳54 QDPSizeChangeProof (⇔)

        ↳55 TRUE

      ↳56 PiDP

        ↳57 UsableRulesProof (⇔)

        ↳58 PiDP

        ↳59 PiDPToQDPProof (⇐)

        ↳60 QDP

        ↳61 QDPOrderProof (⇔)

        ↳62 QDP

        ↳63 DependencyGraphProof (⇔)

        ↳64 QDP

        ↳65 UsableRulesProof (⇔)

        ↳66 QDP

        ↳67 QReductionProof (⇔)

        ↳68 QDP

        ↳69 NonTerminationProof (⇔)

        ↳70 FALSE

      ↳71 PiDP

        ↳72 UsableRulesProof (⇔)

        ↳73 PiDP

        ↳74 PiDPToQDPProof (⇐)

        ↳75 QDP

        ↳76 QDPSizeChangeProof (⇔)

        ↳77 TRUE

      ↳78 PiDP

        ↳79 UsableRulesProof (⇔)

        ↳80 PiDP

        ↳81 PiDPToQDPProof (⇐)

        ↳82 QDP

        ↳83 QDPSizeChangeProof (⇔)

        ↳84 TRUE

(0) Obligation:

Clauses:

ackermann(0, N, s(N)).
ackermann(s(M), 0, Val) :- ackermann(M, s(0), Val).
ackermann(s(M), s(N), Val) :- ','(ackermann(s(M), N, Val1), ackermann(M, Val1, Val)).

Queries:

ackermann(g,a,g).

(1) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
ackermann_in: (b,f,b) (b,b,b) (b,b,f) (b,f,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(2) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAG(s(M), 0, Val) → U1_GAG(M, Val, ackermann_in_ggg(M, s(0), Val))
ACKERMANN_IN_GAG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)
ACKERMANN_IN_GGG(s(M), 0, Val) → U1_GGG(M, Val, ackermann_in_ggg(M, s(0), Val))
ACKERMANN_IN_GGG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)
ACKERMANN_IN_GGG(s(M), s(N), Val) → U2_GGG(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ACKERMANN_IN_GGG(s(M), s(N), Val) → ACKERMANN_IN_GGA(s(M), N, Val1)
ACKERMANN_IN_GGA(s(M), 0, Val) → U1_GGA(M, Val, ackermann_in_gga(M, s(0), Val))
ACKERMANN_IN_GGA(s(M), 0, Val) → ACKERMANN_IN_GGA(M, s(0), Val)
ACKERMANN_IN_GGA(s(M), s(N), Val) → U2_GGA(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ACKERMANN_IN_GGA(s(M), s(N), Val) → ACKERMANN_IN_GGA(s(M), N, Val1)
U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_GGA(M, N, Val, ackermann_in_gga(M, Val1, Val))
U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGA(M, Val1, Val)
U2_GGG(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_GGG(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U2_GGG(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGG(M, Val1, Val)
ACKERMANN_IN_GAG(s(M), s(N), Val) → U2_GAG(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_GAG(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
ACKERMANN_IN_GAA(s(M), 0, Val) → U1_GAA(M, Val, ackermann_in_gga(M, s(0), Val))
ACKERMANN_IN_GAA(s(M), 0, Val) → ACKERMANN_IN_GGA(M, s(0), Val)
ACKERMANN_IN_GAA(s(M), s(N), Val) → U2_GAA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_GAA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_GAA(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAA(M, Val1, Val)
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_GAG(M, N, Val, ackermann_in_gag(M, Val1, Val))
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAG(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

The argument filtering Pi contains the following mapping:
ackermann_in_gag(x1, x2, x3) = ackermann_in_gag(x1, x3)
0 = 0
s(x1) = s(x1)
ackermann_out_gag(x1, x2, x3) = ackermann_out_gag(x1, x3)
U1_gag(x1, x2, x3) = U1_gag(x1, x2, x3)
ackermann_in_ggg(x1, x2, x3) = ackermann_in_ggg(x1, x2, x3)
ackermann_out_ggg(x1, x2, x3) = ackermann_out_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3) = U1_ggg(x1, x2, x3)
U2_ggg(x1, x2, x3, x4) = U2_ggg(x1, x2, x3, x4)
ackermann_in_gga(x1, x2, x3) = ackermann_in_gga(x1, x2)
ackermann_out_gga(x1, x2, x3) = ackermann_out_gga(x1, x2, x3)
U1_gga(x1, x2, x3) = U1_gga(x1, x3)
U2_gga(x1, x2, x3, x4) = U2_gga(x1, x2, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x1, x2, x4)
U3_ggg(x1, x2, x3, x4) = U3_ggg(x1, x2, x3, x4)
U2_gag(x1, x2, x3, x4) = U2_gag(x1, x3, x4)
ackermann_in_gaa(x1, x2, x3) = ackermann_in_gaa(x1)
ackermann_out_gaa(x1, x2, x3) = ackermann_out_gaa(x1)
U1_gaa(x1, x2, x3) = U1_gaa(x1, x3)
U2_gaa(x1, x2, x3, x4) = U2_gaa(x1, x4)
U3_gaa(x1, x2, x3, x4) = U3_gaa(x1, x4)
U3_gag(x1, x2, x3, x4) = U3_gag(x1, x3, x4)
ACKERMANN_IN_GAG(x1, x2, x3) = ACKERMANN_IN_GAG(x1, x3)
U1_GAG(x1, x2, x3) = U1_GAG(x1, x2, x3)
ACKERMANN_IN_GGG(x1, x2, x3) = ACKERMANN_IN_GGG(x1, x2, x3)
U1_GGG(x1, x2, x3) = U1_GGG(x1, x2, x3)
U2_GGG(x1, x2, x3, x4) = U2_GGG(x1, x2, x3, x4)
ACKERMANN_IN_GGA(x1, x2, x3) = ACKERMANN_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3) = U1_GGA(x1, x3)
U2_GGA(x1, x2, x3, x4) = U2_GGA(x1, x2, x4)
U3_GGA(x1, x2, x3, x4) = U3_GGA(x1, x2, x4)
U3_GGG(x1, x2, x3, x4) = U3_GGG(x1, x2, x3, x4)
U2_GAG(x1, x2, x3, x4) = U2_GAG(x1, x3, x4)
ACKERMANN_IN_GAA(x1, x2, x3) = ACKERMANN_IN_GAA(x1)
U1_GAA(x1, x2, x3) = U1_GAA(x1, x3)
U2_GAA(x1, x2, x3, x4) = U2_GAA(x1, x4)
U3_GAA(x1, x2, x3, x4) = U3_GAA(x1, x4)
U3_GAG(x1, x2, x3, x4) = U3_GAG(x1, x3, x4)

We have to consider all (P,R,Pi)-chains

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAG(s(M), 0, Val) → U1_GAG(M, Val, ackermann_in_ggg(M, s(0), Val))
ACKERMANN_IN_GAG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)
ACKERMANN_IN_GGG(s(M), 0, Val) → U1_GGG(M, Val, ackermann_in_ggg(M, s(0), Val))
ACKERMANN_IN_GGG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)
ACKERMANN_IN_GGG(s(M), s(N), Val) → U2_GGG(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ACKERMANN_IN_GGG(s(M), s(N), Val) → ACKERMANN_IN_GGA(s(M), N, Val1)
ACKERMANN_IN_GGA(s(M), 0, Val) → U1_GGA(M, Val, ackermann_in_gga(M, s(0), Val))
ACKERMANN_IN_GGA(s(M), 0, Val) → ACKERMANN_IN_GGA(M, s(0), Val)
ACKERMANN_IN_GGA(s(M), s(N), Val) → U2_GGA(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ACKERMANN_IN_GGA(s(M), s(N), Val) → ACKERMANN_IN_GGA(s(M), N, Val1)
U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_GGA(M, N, Val, ackermann_in_gga(M, Val1, Val))
U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGA(M, Val1, Val)
U2_GGG(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_GGG(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U2_GGG(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGG(M, Val1, Val)
ACKERMANN_IN_GAG(s(M), s(N), Val) → U2_GAG(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_GAG(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
ACKERMANN_IN_GAA(s(M), 0, Val) → U1_GAA(M, Val, ackermann_in_gga(M, s(0), Val))
ACKERMANN_IN_GAA(s(M), 0, Val) → ACKERMANN_IN_GGA(M, s(0), Val)
ACKERMANN_IN_GAA(s(M), s(N), Val) → U2_GAA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_GAA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_GAA(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAA(M, Val1, Val)
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_GAG(M, N, Val, ackermann_in_gag(M, Val1, Val))
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAG(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 12 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GGA(s(M), 0, Val) → ACKERMANN_IN_GGA(M, s(0), Val)
ACKERMANN_IN_GGA(s(M), s(N), Val) → U2_GGA(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGA(M, Val1, Val)
ACKERMANN_IN_GGA(s(M), s(N), Val) → ACKERMANN_IN_GGA(s(M), N, Val1)

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GGA(s(M), 0, Val) → ACKERMANN_IN_GGA(M, s(0), Val)
ACKERMANN_IN_GGA(s(M), s(N), Val) → U2_GGA(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGA(M, Val1, Val)
ACKERMANN_IN_GGA(s(M), s(N), Val) → ACKERMANN_IN_GGA(s(M), N, Val1)

The TRS R consists of the following rules:

ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GGA(s(M), 0) → ACKERMANN_IN_GGA(M, s(0))
ACKERMANN_IN_GGA(s(M), s(N)) → U2_GGA(M, N, ackermann_in_gga(s(M), N))
U2_GGA(M, N, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGA(M, Val1)
ACKERMANN_IN_GGA(s(M), s(N)) → ACKERMANN_IN_GGA(s(M), N)

The TRS R consists of the following rules:

ackermann_in_gga(s(M), 0) → U1_gga(M, ackermann_in_gga(M, s(0)))
ackermann_in_gga(s(M), s(N)) → U2_gga(M, N, ackermann_in_gga(s(M), N))
U1_gga(M, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_gga(M, N, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, ackermann_in_gga(M, Val1))
ackermann_in_gga(0, N) → ackermann_out_gga(0, N, s(N))
U3_gga(M, N, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)

The set Q consists of the following terms:

ackermann_in_gga(x0, x1)
U1_gga(x0, x1)
U2_gga(x0, x1, x2)
U3_gga(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

ACKERMANN_IN_GGA(s(M), s(N)) → ACKERMANN_IN_GGA(s(M), N)
The graph contains the following edges 1 >= 1, 2 > 2
ACKERMANN_IN_GGA(s(M), s(N)) → U2_GGA(M, N, ackermann_in_gga(s(M), N))
The graph contains the following edges 1 > 1, 2 > 2
U2_GGA(M, N, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGA(M, Val1)
The graph contains the following edges 1 >= 1, 3 > 1, 3 > 2
ACKERMANN_IN_GGA(s(M), 0) → ACKERMANN_IN_GGA(M, s(0))
The graph contains the following edges 1 > 1

(13) TRUE

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M), s(N), Val) → U2_GAA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAA(M, Val1, Val)
ACKERMANN_IN_GAA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M), s(N), Val) → U2_GAA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAA(M, Val1, Val)
ACKERMANN_IN_GAA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)

The TRS R consists of the following rules:

ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)

The argument filtering Pi contains the following mapping:
0 = 0
s(x1) = s(x1)
ackermann_in_gga(x1, x2, x3) = ackermann_in_gga(x1, x2)
ackermann_out_gga(x1, x2, x3) = ackermann_out_gga(x1, x2, x3)
U1_gga(x1, x2, x3) = U1_gga(x1, x3)
U2_gga(x1, x2, x3, x4) = U2_gga(x1, x2, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x1, x2, x4)
ackermann_in_gaa(x1, x2, x3) = ackermann_in_gaa(x1)
ackermann_out_gaa(x1, x2, x3) = ackermann_out_gaa(x1)
U1_gaa(x1, x2, x3) = U1_gaa(x1, x3)
U2_gaa(x1, x2, x3, x4) = U2_gaa(x1, x4)
U3_gaa(x1, x2, x3, x4) = U3_gaa(x1, x4)
ACKERMANN_IN_GAA(x1, x2, x3) = ACKERMANN_IN_GAA(x1)
U2_GAA(x1, x2, x3, x4) = U2_GAA(x1, x4)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M)) → U2_GAA(M, ackermann_in_gaa(s(M)))
U2_GAA(M, ackermann_out_gaa(s(M))) → ACKERMANN_IN_GAA(M)
ACKERMANN_IN_GAA(s(M)) → ACKERMANN_IN_GAA(s(M))

The TRS R consists of the following rules:

ackermann_in_gaa(s(M)) → U1_gaa(M, ackermann_in_gga(M, s(0)))
ackermann_in_gaa(s(M)) → U2_gaa(M, ackermann_in_gaa(s(M)))
U1_gaa(M, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M))
U2_gaa(M, ackermann_out_gaa(s(M))) → U3_gaa(M, ackermann_in_gaa(M))
ackermann_in_gga(0, N) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), s(N)) → U2_gga(M, N, ackermann_in_gga(s(M), N))
U3_gaa(M, ackermann_out_gaa(M)) → ackermann_out_gaa(s(M))
U2_gga(M, N, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, ackermann_in_gga(M, Val1))
ackermann_in_gaa(0) → ackermann_out_gaa(0)
ackermann_in_gga(s(M), 0) → U1_gga(M, ackermann_in_gga(M, s(0)))
U3_gga(M, N, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0, x1)
U2_gaa(x0, x1)
ackermann_in_gga(x0, x1)
U3_gaa(x0, x1)
U2_gga(x0, x1, x2)
U3_gga(x0, x1, x2)
U1_gga(x0, x1)

We have to consider all (P,Q,R)-chains.

(19) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

U2_GAA(M, ackermann_out_gaa(s(M))) → ACKERMANN_IN_GAA(M)

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(ACKERMANN_IN_GAA(x₁)) = 0 +
[ 1, 1 ]

· x₁

POL(s(x₁)) =
/ 0 \

\ 1 /

+
/ 0 1 \

\ 1 1 /

· x₁

POL(U2_GAA(x₁, x₂)) = 1 +
[ 1, 1 ]

· x₁ +
[ 0, 0 ]

· x₂

POL(ackermann_in_gaa(x₁)) =
/ 0 \

\ 0 /

+
/ 0 0 \

\ 1 0 /

· x₁

POL(ackermann_out_gaa(x₁)) =
/ 0 \

\ 1 /

+
/ 0 1 \

\ 0 0 /

· x₁

POL(U1_gaa(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 0 /

· x₁ +
/ 0 0 \

\ 0 0 /

· x₂

POL(ackermann_in_gga(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 1 1 /

· x₁ +
/ 1 1 \

\ 0 1 /

· x₂

POL(0) =
/ 1 \

\ 0 /

POL(U2_gaa(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁ +
/ 0 1 \

\ 0 0 /

· x₂

POL(U3_gaa(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 0 1 \

\ 0 0 /

· x₁ +
/ 0 0 \

\ 0 0 /

· x₂

POL(ackermann_out_gga(x₁, x₂, x₃)) =
/ 0 \

\ 0 /

+
/ 0 0 \

\ 1 1 /

· x₁ +
/ 1 0 \

\ 0 0 /

· x₂ +
/ 0 0 \

\ 0 1 /

· x₃

POL(U2_gga(x₁, x₂, x₃)) =
/ 0 \

\ 0 /

+
/ 0 0 \

\ 0 0 /

· x₁ +
/ 0 1 \

\ 1 1 /

· x₂ +
/ 0 0 \

\ 1 0 /

· x₃

POL(U1_gga(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 0 0 \

\ 0 0 /

· x₁ +
/ 1 0 \

\ 1 0 /

· x₂

POL(U3_gga(x₁, x₂, x₃)) =
/ 1 \

\ 1 /

+
/ 0 0 \

\ 0 1 /

· x₁ +
/ 1 0 \

\ 1 0 /

· x₂ +
/ 1 1 \

\ 1 0 /

· x₃

The following usable rules [FROCOS05] were oriented: none

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M)) → U2_GAA(M, ackermann_in_gaa(s(M)))
ACKERMANN_IN_GAA(s(M)) → ACKERMANN_IN_GAA(s(M))

The TRS R consists of the following rules:

ackermann_in_gaa(s(M)) → U1_gaa(M, ackermann_in_gga(M, s(0)))
ackermann_in_gaa(s(M)) → U2_gaa(M, ackermann_in_gaa(s(M)))
U1_gaa(M, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M))
U2_gaa(M, ackermann_out_gaa(s(M))) → U3_gaa(M, ackermann_in_gaa(M))
ackermann_in_gga(0, N) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), s(N)) → U2_gga(M, N, ackermann_in_gga(s(M), N))
U3_gaa(M, ackermann_out_gaa(M)) → ackermann_out_gaa(s(M))
U2_gga(M, N, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, ackermann_in_gga(M, Val1))
ackermann_in_gaa(0) → ackermann_out_gaa(0)
ackermann_in_gga(s(M), 0) → U1_gga(M, ackermann_in_gga(M, s(0)))
U3_gga(M, N, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0, x1)
U2_gaa(x0, x1)
ackermann_in_gga(x0, x1)
U3_gaa(x0, x1)
U2_gga(x0, x1, x2)
U3_gga(x0, x1, x2)
U1_gga(x0, x1)

We have to consider all (P,Q,R)-chains.

(21) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(22) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M)) → ACKERMANN_IN_GAA(s(M))

The TRS R consists of the following rules:

ackermann_in_gaa(s(M)) → U1_gaa(M, ackermann_in_gga(M, s(0)))
ackermann_in_gaa(s(M)) → U2_gaa(M, ackermann_in_gaa(s(M)))
U1_gaa(M, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M))
U2_gaa(M, ackermann_out_gaa(s(M))) → U3_gaa(M, ackermann_in_gaa(M))
ackermann_in_gga(0, N) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), s(N)) → U2_gga(M, N, ackermann_in_gga(s(M), N))
U3_gaa(M, ackermann_out_gaa(M)) → ackermann_out_gaa(s(M))
U2_gga(M, N, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, ackermann_in_gga(M, Val1))
ackermann_in_gaa(0) → ackermann_out_gaa(0)
ackermann_in_gga(s(M), 0) → U1_gga(M, ackermann_in_gga(M, s(0)))
U3_gga(M, N, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0, x1)
U2_gaa(x0, x1)
ackermann_in_gga(x0, x1)
U3_gaa(x0, x1)
U2_gga(x0, x1, x2)
U3_gga(x0, x1, x2)
U1_gga(x0, x1)

We have to consider all (P,Q,R)-chains.

(23) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(24) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M)) → ACKERMANN_IN_GAA(s(M))

R is empty.
The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0, x1)
U2_gaa(x0, x1)
ackermann_in_gga(x0, x1)
U3_gaa(x0, x1)
U2_gga(x0, x1, x2)
U3_gga(x0, x1, x2)
U1_gga(x0, x1)

We have to consider all (P,Q,R)-chains.

(25) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

ackermann_in_gaa(x0)
U1_gaa(x0, x1)
U2_gaa(x0, x1)
ackermann_in_gga(x0, x1)
U3_gaa(x0, x1)
U2_gga(x0, x1, x2)
U3_gga(x0, x1, x2)
U1_gga(x0, x1)

(26) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M)) → ACKERMANN_IN_GAA(s(M))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(27) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = ACKERMANN_IN_GAA(s(M)) evaluates to t =ACKERMANN_IN_GAA(s(M))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Matcher: [ ]
Semiunifier: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from ACKERMANN_IN_GAA(s(M)) to ACKERMANN_IN_GAA(s(M)).

(28) FALSE

(29) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GGG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)
ACKERMANN_IN_GGG(s(M), s(N), Val) → U2_GGG(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_GGG(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGG(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

(30) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(31) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GGG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)
ACKERMANN_IN_GGG(s(M), s(N), Val) → U2_GGG(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_GGG(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGG(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)

(32) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(33) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GGG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)
ACKERMANN_IN_GGG(s(M), s(N), Val) → U2_GGG(M, N, Val, ackermann_in_gga(s(M), N))
U2_GGG(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGG(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_in_gga(s(M), 0) → U1_gga(M, ackermann_in_gga(M, s(0)))
ackermann_in_gga(s(M), s(N)) → U2_gga(M, N, ackermann_in_gga(s(M), N))
U1_gga(M, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_gga(M, N, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, ackermann_in_gga(M, Val1))
ackermann_in_gga(0, N) → ackermann_out_gga(0, N, s(N))
U3_gga(M, N, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)

The set Q consists of the following terms:

ackermann_in_gga(x0, x1)
U1_gga(x0, x1)
U2_gga(x0, x1, x2)
U3_gga(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(34) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

ACKERMANN_IN_GGG(s(M), s(N), Val) → U2_GGG(M, N, Val, ackermann_in_gga(s(M), N))
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
U2_GGG(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGG(M, Val1, Val)
The graph contains the following edges 1 >= 1, 4 > 1, 4 > 2, 3 >= 3
ACKERMANN_IN_GGG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)
The graph contains the following edges 1 > 1, 3 >= 3

(35) TRUE

(36) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAG(s(M), s(N), Val) → U2_GAG(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAG(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

(37) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(38) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAG(s(M), s(N), Val) → U2_GAG(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAG(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)

The argument filtering Pi contains the following mapping:
0 = 0
s(x1) = s(x1)
ackermann_in_gga(x1, x2, x3) = ackermann_in_gga(x1, x2)
ackermann_out_gga(x1, x2, x3) = ackermann_out_gga(x1, x2, x3)
U1_gga(x1, x2, x3) = U1_gga(x1, x3)
U2_gga(x1, x2, x3, x4) = U2_gga(x1, x2, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x1, x2, x4)
ackermann_in_gaa(x1, x2, x3) = ackermann_in_gaa(x1)
ackermann_out_gaa(x1, x2, x3) = ackermann_out_gaa(x1)
U1_gaa(x1, x2, x3) = U1_gaa(x1, x3)
U2_gaa(x1, x2, x3, x4) = U2_gaa(x1, x4)
U3_gaa(x1, x2, x3, x4) = U3_gaa(x1, x4)
ACKERMANN_IN_GAG(x1, x2, x3) = ACKERMANN_IN_GAG(x1, x3)
U2_GAG(x1, x2, x3, x4) = U2_GAG(x1, x3, x4)

We have to consider all (P,R,Pi)-chains

(39) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(40) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAG(s(M), Val) → U2_GAG(M, Val, ackermann_in_gaa(s(M)))
U2_GAG(M, Val, ackermann_out_gaa(s(M))) → ACKERMANN_IN_GAG(M, Val)

The TRS R consists of the following rules:

ackermann_in_gaa(s(M)) → U1_gaa(M, ackermann_in_gga(M, s(0)))
ackermann_in_gaa(s(M)) → U2_gaa(M, ackermann_in_gaa(s(M)))
U1_gaa(M, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M))
U2_gaa(M, ackermann_out_gaa(s(M))) → U3_gaa(M, ackermann_in_gaa(M))
ackermann_in_gga(0, N) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), s(N)) → U2_gga(M, N, ackermann_in_gga(s(M), N))
U3_gaa(M, ackermann_out_gaa(M)) → ackermann_out_gaa(s(M))
U2_gga(M, N, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, ackermann_in_gga(M, Val1))
ackermann_in_gaa(0) → ackermann_out_gaa(0)
ackermann_in_gga(s(M), 0) → U1_gga(M, ackermann_in_gga(M, s(0)))
U3_gga(M, N, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0, x1)
U2_gaa(x0, x1)
ackermann_in_gga(x0, x1)
U3_gaa(x0, x1)
U2_gga(x0, x1, x2)
U3_gga(x0, x1, x2)
U1_gga(x0, x1)

We have to consider all (P,Q,R)-chains.

(41) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

U2_GAG(M, Val, ackermann_out_gaa(s(M))) → ACKERMANN_IN_GAG(M, Val)
The graph contains the following edges 1 >= 1, 3 > 1, 2 >= 2
ACKERMANN_IN_GAG(s(M), Val) → U2_GAG(M, Val, ackermann_in_gaa(s(M)))
The graph contains the following edges 1 > 1, 2 >= 2

(42) TRUE

(43) PrologToPiTRSProof (SOUND transformation)

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(44) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

(45) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAG(s(M), 0, Val) → U1_GAG(M, Val, ackermann_in_ggg(M, s(0), Val))
ACKERMANN_IN_GAG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)
ACKERMANN_IN_GGG(s(M), 0, Val) → U1_GGG(M, Val, ackermann_in_ggg(M, s(0), Val))
ACKERMANN_IN_GGG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)
ACKERMANN_IN_GGG(s(M), s(N), Val) → U2_GGG(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ACKERMANN_IN_GGG(s(M), s(N), Val) → ACKERMANN_IN_GGA(s(M), N, Val1)
ACKERMANN_IN_GGA(s(M), 0, Val) → U1_GGA(M, Val, ackermann_in_gga(M, s(0), Val))
ACKERMANN_IN_GGA(s(M), 0, Val) → ACKERMANN_IN_GGA(M, s(0), Val)
ACKERMANN_IN_GGA(s(M), s(N), Val) → U2_GGA(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ACKERMANN_IN_GGA(s(M), s(N), Val) → ACKERMANN_IN_GGA(s(M), N, Val1)
U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_GGA(M, N, Val, ackermann_in_gga(M, Val1, Val))
U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGA(M, Val1, Val)
U2_GGG(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_GGG(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U2_GGG(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGG(M, Val1, Val)
ACKERMANN_IN_GAG(s(M), s(N), Val) → U2_GAG(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_GAG(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
ACKERMANN_IN_GAA(s(M), 0, Val) → U1_GAA(M, Val, ackermann_in_gga(M, s(0), Val))
ACKERMANN_IN_GAA(s(M), 0, Val) → ACKERMANN_IN_GGA(M, s(0), Val)
ACKERMANN_IN_GAA(s(M), s(N), Val) → U2_GAA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_GAA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_GAA(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAA(M, Val1, Val)
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_GAG(M, N, Val, ackermann_in_gag(M, Val1, Val))
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAG(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

The argument filtering Pi contains the following mapping:
ackermann_in_gag(x1, x2, x3) = ackermann_in_gag(x1, x3)
0 = 0
s(x1) = s(x1)
ackermann_out_gag(x1, x2, x3) = ackermann_out_gag
U1_gag(x1, x2, x3) = U1_gag(x3)
ackermann_in_ggg(x1, x2, x3) = ackermann_in_ggg(x1, x2, x3)
ackermann_out_ggg(x1, x2, x3) = ackermann_out_ggg
U1_ggg(x1, x2, x3) = U1_ggg(x3)
U2_ggg(x1, x2, x3, x4) = U2_ggg(x1, x3, x4)
ackermann_in_gga(x1, x2, x3) = ackermann_in_gga(x1, x2)
ackermann_out_gga(x1, x2, x3) = ackermann_out_gga(x3)
U1_gga(x1, x2, x3) = U1_gga(x3)
U2_gga(x1, x2, x3, x4) = U2_gga(x1, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x4)
U3_ggg(x1, x2, x3, x4) = U3_ggg(x4)
U2_gag(x1, x2, x3, x4) = U2_gag(x1, x3, x4)
ackermann_in_gaa(x1, x2, x3) = ackermann_in_gaa(x1)
ackermann_out_gaa(x1, x2, x3) = ackermann_out_gaa
U1_gaa(x1, x2, x3) = U1_gaa(x3)
U2_gaa(x1, x2, x3, x4) = U2_gaa(x1, x4)
U3_gaa(x1, x2, x3, x4) = U3_gaa(x4)
U3_gag(x1, x2, x3, x4) = U3_gag(x4)
ACKERMANN_IN_GAG(x1, x2, x3) = ACKERMANN_IN_GAG(x1, x3)
U1_GAG(x1, x2, x3) = U1_GAG(x3)
ACKERMANN_IN_GGG(x1, x2, x3) = ACKERMANN_IN_GGG(x1, x2, x3)
U1_GGG(x1, x2, x3) = U1_GGG(x3)
U2_GGG(x1, x2, x3, x4) = U2_GGG(x1, x3, x4)
ACKERMANN_IN_GGA(x1, x2, x3) = ACKERMANN_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3) = U1_GGA(x3)
U2_GGA(x1, x2, x3, x4) = U2_GGA(x1, x4)
U3_GGA(x1, x2, x3, x4) = U3_GGA(x4)
U3_GGG(x1, x2, x3, x4) = U3_GGG(x4)
U2_GAG(x1, x2, x3, x4) = U2_GAG(x1, x3, x4)
ACKERMANN_IN_GAA(x1, x2, x3) = ACKERMANN_IN_GAA(x1)
U1_GAA(x1, x2, x3) = U1_GAA(x3)
U2_GAA(x1, x2, x3, x4) = U2_GAA(x1, x4)
U3_GAA(x1, x2, x3, x4) = U3_GAA(x4)
U3_GAG(x1, x2, x3, x4) = U3_GAG(x4)

We have to consider all (P,R,Pi)-chains

(46) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAG(s(M), 0, Val) → U1_GAG(M, Val, ackermann_in_ggg(M, s(0), Val))
ACKERMANN_IN_GAG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)
ACKERMANN_IN_GGG(s(M), 0, Val) → U1_GGG(M, Val, ackermann_in_ggg(M, s(0), Val))
ACKERMANN_IN_GGG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)
ACKERMANN_IN_GGG(s(M), s(N), Val) → U2_GGG(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ACKERMANN_IN_GGG(s(M), s(N), Val) → ACKERMANN_IN_GGA(s(M), N, Val1)
ACKERMANN_IN_GGA(s(M), 0, Val) → U1_GGA(M, Val, ackermann_in_gga(M, s(0), Val))
ACKERMANN_IN_GGA(s(M), 0, Val) → ACKERMANN_IN_GGA(M, s(0), Val)
ACKERMANN_IN_GGA(s(M), s(N), Val) → U2_GGA(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ACKERMANN_IN_GGA(s(M), s(N), Val) → ACKERMANN_IN_GGA(s(M), N, Val1)
U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_GGA(M, N, Val, ackermann_in_gga(M, Val1, Val))
U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGA(M, Val1, Val)
U2_GGG(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_GGG(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U2_GGG(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGG(M, Val1, Val)
ACKERMANN_IN_GAG(s(M), s(N), Val) → U2_GAG(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_GAG(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
ACKERMANN_IN_GAA(s(M), 0, Val) → U1_GAA(M, Val, ackermann_in_gga(M, s(0), Val))
ACKERMANN_IN_GAA(s(M), 0, Val) → ACKERMANN_IN_GGA(M, s(0), Val)
ACKERMANN_IN_GAA(s(M), s(N), Val) → U2_GAA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ACKERMANN_IN_GAA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_GAA(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAA(M, Val1, Val)
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_GAG(M, N, Val, ackermann_in_gag(M, Val1, Val))
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAG(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

The argument filtering Pi contains the following mapping:
ackermann_in_gag(x1, x2, x3) = ackermann_in_gag(x1, x3)
0 = 0
s(x1) = s(x1)
ackermann_out_gag(x1, x2, x3) = ackermann_out_gag
U1_gag(x1, x2, x3) = U1_gag(x3)
ackermann_in_ggg(x1, x2, x3) = ackermann_in_ggg(x1, x2, x3)
ackermann_out_ggg(x1, x2, x3) = ackermann_out_ggg
U1_ggg(x1, x2, x3) = U1_ggg(x3)
U2_ggg(x1, x2, x3, x4) = U2_ggg(x1, x3, x4)
ackermann_in_gga(x1, x2, x3) = ackermann_in_gga(x1, x2)
ackermann_out_gga(x1, x2, x3) = ackermann_out_gga(x3)
U1_gga(x1, x2, x3) = U1_gga(x3)
U2_gga(x1, x2, x3, x4) = U2_gga(x1, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x4)
U3_ggg(x1, x2, x3, x4) = U3_ggg(x4)
U2_gag(x1, x2, x3, x4) = U2_gag(x1, x3, x4)
ackermann_in_gaa(x1, x2, x3) = ackermann_in_gaa(x1)
ackermann_out_gaa(x1, x2, x3) = ackermann_out_gaa
U1_gaa(x1, x2, x3) = U1_gaa(x3)
U2_gaa(x1, x2, x3, x4) = U2_gaa(x1, x4)
U3_gaa(x1, x2, x3, x4) = U3_gaa(x4)
U3_gag(x1, x2, x3, x4) = U3_gag(x4)
ACKERMANN_IN_GAG(x1, x2, x3) = ACKERMANN_IN_GAG(x1, x3)
U1_GAG(x1, x2, x3) = U1_GAG(x3)
ACKERMANN_IN_GGG(x1, x2, x3) = ACKERMANN_IN_GGG(x1, x2, x3)
U1_GGG(x1, x2, x3) = U1_GGG(x3)
U2_GGG(x1, x2, x3, x4) = U2_GGG(x1, x3, x4)
ACKERMANN_IN_GGA(x1, x2, x3) = ACKERMANN_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3) = U1_GGA(x3)
U2_GGA(x1, x2, x3, x4) = U2_GGA(x1, x4)
U3_GGA(x1, x2, x3, x4) = U3_GGA(x4)
U3_GGG(x1, x2, x3, x4) = U3_GGG(x4)
U2_GAG(x1, x2, x3, x4) = U2_GAG(x1, x3, x4)
ACKERMANN_IN_GAA(x1, x2, x3) = ACKERMANN_IN_GAA(x1)
U1_GAA(x1, x2, x3) = U1_GAA(x3)
U2_GAA(x1, x2, x3, x4) = U2_GAA(x1, x4)
U3_GAA(x1, x2, x3, x4) = U3_GAA(x4)
U3_GAG(x1, x2, x3, x4) = U3_GAG(x4)

We have to consider all (P,R,Pi)-chains

(47) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 12 less nodes.

(48) Complex Obligation (AND)

(49) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GGA(s(M), 0, Val) → ACKERMANN_IN_GGA(M, s(0), Val)
ACKERMANN_IN_GGA(s(M), s(N), Val) → U2_GGA(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGA(M, Val1, Val)
ACKERMANN_IN_GGA(s(M), s(N), Val) → ACKERMANN_IN_GGA(s(M), N, Val1)

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

(50) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(51) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GGA(s(M), 0, Val) → ACKERMANN_IN_GGA(M, s(0), Val)
ACKERMANN_IN_GGA(s(M), s(N), Val) → U2_GGA(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_GGA(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGA(M, Val1, Val)
ACKERMANN_IN_GGA(s(M), s(N), Val) → ACKERMANN_IN_GGA(s(M), N, Val1)

The TRS R consists of the following rules:

ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)

(52) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(53) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GGA(s(M), 0) → ACKERMANN_IN_GGA(M, s(0))
ACKERMANN_IN_GGA(s(M), s(N)) → U2_GGA(M, ackermann_in_gga(s(M), N))
U2_GGA(M, ackermann_out_gga(Val1)) → ACKERMANN_IN_GGA(M, Val1)
ACKERMANN_IN_GGA(s(M), s(N)) → ACKERMANN_IN_GGA(s(M), N)

The TRS R consists of the following rules:

ackermann_in_gga(s(M), 0) → U1_gga(ackermann_in_gga(M, s(0)))
ackermann_in_gga(s(M), s(N)) → U2_gga(M, ackermann_in_gga(s(M), N))
U1_gga(ackermann_out_gga(Val)) → ackermann_out_gga(Val)
U2_gga(M, ackermann_out_gga(Val1)) → U3_gga(ackermann_in_gga(M, Val1))
ackermann_in_gga(0, N) → ackermann_out_gga(s(N))
U3_gga(ackermann_out_gga(Val)) → ackermann_out_gga(Val)

The set Q consists of the following terms:

ackermann_in_gga(x0, x1)
U1_gga(x0)
U2_gga(x0, x1)
U3_gga(x0)

We have to consider all (P,Q,R)-chains.

(54) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

ACKERMANN_IN_GGA(s(M), s(N)) → ACKERMANN_IN_GGA(s(M), N)
The graph contains the following edges 1 >= 1, 2 > 2
ACKERMANN_IN_GGA(s(M), s(N)) → U2_GGA(M, ackermann_in_gga(s(M), N))
The graph contains the following edges 1 > 1
U2_GGA(M, ackermann_out_gga(Val1)) → ACKERMANN_IN_GGA(M, Val1)
The graph contains the following edges 1 >= 1, 2 > 2
ACKERMANN_IN_GGA(s(M), 0) → ACKERMANN_IN_GGA(M, s(0))
The graph contains the following edges 1 > 1

(55) TRUE

(56) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M), s(N), Val) → U2_GAA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAA(M, Val1, Val)
ACKERMANN_IN_GAA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

(57) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(58) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M), s(N), Val) → U2_GAA(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_GAA(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAA(M, Val1, Val)
ACKERMANN_IN_GAA(s(M), s(N), Val) → ACKERMANN_IN_GAA(s(M), N, Val1)

The TRS R consists of the following rules:

ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)

The argument filtering Pi contains the following mapping:
0 = 0
s(x1) = s(x1)
ackermann_in_gga(x1, x2, x3) = ackermann_in_gga(x1, x2)
ackermann_out_gga(x1, x2, x3) = ackermann_out_gga(x3)
U1_gga(x1, x2, x3) = U1_gga(x3)
U2_gga(x1, x2, x3, x4) = U2_gga(x1, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x4)
ackermann_in_gaa(x1, x2, x3) = ackermann_in_gaa(x1)
ackermann_out_gaa(x1, x2, x3) = ackermann_out_gaa
U1_gaa(x1, x2, x3) = U1_gaa(x3)
U2_gaa(x1, x2, x3, x4) = U2_gaa(x1, x4)
U3_gaa(x1, x2, x3, x4) = U3_gaa(x4)
ACKERMANN_IN_GAA(x1, x2, x3) = ACKERMANN_IN_GAA(x1)
U2_GAA(x1, x2, x3, x4) = U2_GAA(x1, x4)

We have to consider all (P,R,Pi)-chains

(59) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(60) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M)) → U2_GAA(M, ackermann_in_gaa(s(M)))
U2_GAA(M, ackermann_out_gaa) → ACKERMANN_IN_GAA(M)
ACKERMANN_IN_GAA(s(M)) → ACKERMANN_IN_GAA(s(M))

The TRS R consists of the following rules:

ackermann_in_gaa(s(M)) → U1_gaa(ackermann_in_gga(M, s(0)))
ackermann_in_gaa(s(M)) → U2_gaa(M, ackermann_in_gaa(s(M)))
U1_gaa(ackermann_out_gga(Val)) → ackermann_out_gaa
U2_gaa(M, ackermann_out_gaa) → U3_gaa(ackermann_in_gaa(M))
ackermann_in_gga(0, N) → ackermann_out_gga(s(N))
ackermann_in_gga(s(M), s(N)) → U2_gga(M, ackermann_in_gga(s(M), N))
U3_gaa(ackermann_out_gaa) → ackermann_out_gaa
U2_gga(M, ackermann_out_gga(Val1)) → U3_gga(ackermann_in_gga(M, Val1))
ackermann_in_gaa(0) → ackermann_out_gaa
ackermann_in_gga(s(M), 0) → U1_gga(ackermann_in_gga(M, s(0)))
U3_gga(ackermann_out_gga(Val)) → ackermann_out_gga(Val)
U1_gga(ackermann_out_gga(Val)) → ackermann_out_gga(Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0, x1)
ackermann_in_gga(x0, x1)
U3_gaa(x0)
U2_gga(x0, x1)
U3_gga(x0)
U1_gga(x0)

We have to consider all (P,Q,R)-chains.

(61) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

ACKERMANN_IN_GAA(s(M)) → U2_GAA(M, ackermann_in_gaa(s(M)))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0
POL(ACKERMANN_IN_GAA(x₁)) = x₁
POL(U1_gaa(x₁)) = 0
POL(U1_gga(x₁)) = 0
POL(U2_GAA(x₁, x₂)) = x₁
POL(U2_gaa(x₁, x₂)) = 0
POL(U2_gga(x₁, x₂)) = 0
POL(U3_gaa(x₁)) = 0
POL(U3_gga(x₁)) = 0
POL(ackermann_in_gaa(x₁)) = 0
POL(ackermann_in_gga(x₁, x₂)) = 0
POL(ackermann_out_gaa) = 0
POL(ackermann_out_gga(x₁)) = 0
POL(s(x₁)) = 1 + x₁

The following usable rules [FROCOS05] were oriented: none

(62) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U2_GAA(M, ackermann_out_gaa) → ACKERMANN_IN_GAA(M)
ACKERMANN_IN_GAA(s(M)) → ACKERMANN_IN_GAA(s(M))

The TRS R consists of the following rules:

ackermann_in_gaa(s(M)) → U1_gaa(ackermann_in_gga(M, s(0)))
ackermann_in_gaa(s(M)) → U2_gaa(M, ackermann_in_gaa(s(M)))
U1_gaa(ackermann_out_gga(Val)) → ackermann_out_gaa
U2_gaa(M, ackermann_out_gaa) → U3_gaa(ackermann_in_gaa(M))
ackermann_in_gga(0, N) → ackermann_out_gga(s(N))
ackermann_in_gga(s(M), s(N)) → U2_gga(M, ackermann_in_gga(s(M), N))
U3_gaa(ackermann_out_gaa) → ackermann_out_gaa
U2_gga(M, ackermann_out_gga(Val1)) → U3_gga(ackermann_in_gga(M, Val1))
ackermann_in_gaa(0) → ackermann_out_gaa
ackermann_in_gga(s(M), 0) → U1_gga(ackermann_in_gga(M, s(0)))
U3_gga(ackermann_out_gga(Val)) → ackermann_out_gga(Val)
U1_gga(ackermann_out_gga(Val)) → ackermann_out_gga(Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0, x1)
ackermann_in_gga(x0, x1)
U3_gaa(x0)
U2_gga(x0, x1)
U3_gga(x0)
U1_gga(x0)

We have to consider all (P,Q,R)-chains.

(63) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(64) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M)) → ACKERMANN_IN_GAA(s(M))

The TRS R consists of the following rules:

ackermann_in_gaa(s(M)) → U1_gaa(ackermann_in_gga(M, s(0)))
ackermann_in_gaa(s(M)) → U2_gaa(M, ackermann_in_gaa(s(M)))
U1_gaa(ackermann_out_gga(Val)) → ackermann_out_gaa
U2_gaa(M, ackermann_out_gaa) → U3_gaa(ackermann_in_gaa(M))
ackermann_in_gga(0, N) → ackermann_out_gga(s(N))
ackermann_in_gga(s(M), s(N)) → U2_gga(M, ackermann_in_gga(s(M), N))
U3_gaa(ackermann_out_gaa) → ackermann_out_gaa
U2_gga(M, ackermann_out_gga(Val1)) → U3_gga(ackermann_in_gga(M, Val1))
ackermann_in_gaa(0) → ackermann_out_gaa
ackermann_in_gga(s(M), 0) → U1_gga(ackermann_in_gga(M, s(0)))
U3_gga(ackermann_out_gga(Val)) → ackermann_out_gga(Val)
U1_gga(ackermann_out_gga(Val)) → ackermann_out_gga(Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0, x1)
ackermann_in_gga(x0, x1)
U3_gaa(x0)
U2_gga(x0, x1)
U3_gga(x0)
U1_gga(x0)

We have to consider all (P,Q,R)-chains.

(65) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(66) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M)) → ACKERMANN_IN_GAA(s(M))

R is empty.
The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0, x1)
ackermann_in_gga(x0, x1)
U3_gaa(x0)
U2_gga(x0, x1)
U3_gga(x0)
U1_gga(x0)

We have to consider all (P,Q,R)-chains.

(67) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0, x1)
ackermann_in_gga(x0, x1)
U3_gaa(x0)
U2_gga(x0, x1)
U3_gga(x0)
U1_gga(x0)

(68) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAA(s(M)) → ACKERMANN_IN_GAA(s(M))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(69) NonTerminationProof (EQUIVALENT transformation)

Matcher: [ ]
Semiunifier: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from ACKERMANN_IN_GAA(s(M)) to ACKERMANN_IN_GAA(s(M)).

(70) FALSE

(71) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GGG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)
ACKERMANN_IN_GGG(s(M), s(N), Val) → U2_GGG(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_GGG(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGG(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

(72) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(73) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GGG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)
ACKERMANN_IN_GGG(s(M), s(N), Val) → U2_GGG(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_GGG(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → ACKERMANN_IN_GGG(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)

(74) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(75) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GGG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)
ACKERMANN_IN_GGG(s(M), s(N), Val) → U2_GGG(M, Val, ackermann_in_gga(s(M), N))
U2_GGG(M, Val, ackermann_out_gga(Val1)) → ACKERMANN_IN_GGG(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_in_gga(s(M), 0) → U1_gga(ackermann_in_gga(M, s(0)))
ackermann_in_gga(s(M), s(N)) → U2_gga(M, ackermann_in_gga(s(M), N))
U1_gga(ackermann_out_gga(Val)) → ackermann_out_gga(Val)
U2_gga(M, ackermann_out_gga(Val1)) → U3_gga(ackermann_in_gga(M, Val1))
ackermann_in_gga(0, N) → ackermann_out_gga(s(N))
U3_gga(ackermann_out_gga(Val)) → ackermann_out_gga(Val)

The set Q consists of the following terms:

ackermann_in_gga(x0, x1)
U1_gga(x0)
U2_gga(x0, x1)
U3_gga(x0)

We have to consider all (P,Q,R)-chains.

(76) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

ACKERMANN_IN_GGG(s(M), s(N), Val) → U2_GGG(M, Val, ackermann_in_gga(s(M), N))
The graph contains the following edges 1 > 1, 3 >= 2
U2_GGG(M, Val, ackermann_out_gga(Val1)) → ACKERMANN_IN_GGG(M, Val1, Val)
The graph contains the following edges 1 >= 1, 3 > 2, 2 >= 3
ACKERMANN_IN_GGG(s(M), 0, Val) → ACKERMANN_IN_GGG(M, s(0), Val)
The graph contains the following edges 1 > 1, 3 >= 3

(77) TRUE

(78) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAG(s(M), s(N), Val) → U2_GAG(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAG(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_in_gag(0, N, s(N)) → ackermann_out_gag(0, N, s(N))
ackermann_in_gag(s(M), 0, Val) → U1_gag(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(0, N, s(N)) → ackermann_out_ggg(0, N, s(N))
ackermann_in_ggg(s(M), 0, Val) → U1_ggg(M, Val, ackermann_in_ggg(M, s(0), Val))
ackermann_in_ggg(s(M), s(N), Val) → U2_ggg(M, N, Val, ackermann_in_gga(s(M), N, Val1))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)
U2_ggg(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_ggg(M, N, Val, ackermann_in_ggg(M, Val1, Val))
U3_ggg(M, N, Val, ackermann_out_ggg(M, Val1, Val)) → ackermann_out_ggg(s(M), s(N), Val)
U1_ggg(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_ggg(s(M), 0, Val)
U1_gag(M, Val, ackermann_out_ggg(M, s(0), Val)) → ackermann_out_gag(s(M), 0, Val)
ackermann_in_gag(s(M), s(N), Val) → U2_gag(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gag(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gag(M, N, Val, ackermann_in_gag(M, Val1, Val))
U3_gag(M, N, Val, ackermann_out_gag(M, Val1, Val)) → ackermann_out_gag(s(M), s(N), Val)

(79) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(80) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAG(s(M), s(N), Val) → U2_GAG(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U2_GAG(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → ACKERMANN_IN_GAG(M, Val1, Val)

The TRS R consists of the following rules:

ackermann_in_gaa(s(M), 0, Val) → U1_gaa(M, Val, ackermann_in_gga(M, s(0), Val))
ackermann_in_gaa(s(M), s(N), Val) → U2_gaa(M, N, Val, ackermann_in_gaa(s(M), N, Val1))
U1_gaa(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gaa(s(M), 0, Val)
U2_gaa(M, N, Val, ackermann_out_gaa(s(M), N, Val1)) → U3_gaa(M, N, Val, ackermann_in_gaa(M, Val1, Val))
ackermann_in_gga(0, N, s(N)) → ackermann_out_gga(0, N, s(N))
ackermann_in_gga(s(M), s(N), Val) → U2_gga(M, N, Val, ackermann_in_gga(s(M), N, Val1))
U3_gaa(M, N, Val, ackermann_out_gaa(M, Val1, Val)) → ackermann_out_gaa(s(M), s(N), Val)
U2_gga(M, N, Val, ackermann_out_gga(s(M), N, Val1)) → U3_gga(M, N, Val, ackermann_in_gga(M, Val1, Val))
ackermann_in_gaa(0, N, s(N)) → ackermann_out_gaa(0, N, s(N))
ackermann_in_gga(s(M), 0, Val) → U1_gga(M, Val, ackermann_in_gga(M, s(0), Val))
U3_gga(M, N, Val, ackermann_out_gga(M, Val1, Val)) → ackermann_out_gga(s(M), s(N), Val)
U1_gga(M, Val, ackermann_out_gga(M, s(0), Val)) → ackermann_out_gga(s(M), 0, Val)

The argument filtering Pi contains the following mapping:
0 = 0
s(x1) = s(x1)
ackermann_in_gga(x1, x2, x3) = ackermann_in_gga(x1, x2)
ackermann_out_gga(x1, x2, x3) = ackermann_out_gga(x3)
U1_gga(x1, x2, x3) = U1_gga(x3)
U2_gga(x1, x2, x3, x4) = U2_gga(x1, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x4)
ackermann_in_gaa(x1, x2, x3) = ackermann_in_gaa(x1)
ackermann_out_gaa(x1, x2, x3) = ackermann_out_gaa
U1_gaa(x1, x2, x3) = U1_gaa(x3)
U2_gaa(x1, x2, x3, x4) = U2_gaa(x1, x4)
U3_gaa(x1, x2, x3, x4) = U3_gaa(x4)
ACKERMANN_IN_GAG(x1, x2, x3) = ACKERMANN_IN_GAG(x1, x3)
U2_GAG(x1, x2, x3, x4) = U2_GAG(x1, x3, x4)

We have to consider all (P,R,Pi)-chains

(81) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(82) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACKERMANN_IN_GAG(s(M), Val) → U2_GAG(M, Val, ackermann_in_gaa(s(M)))
U2_GAG(M, Val, ackermann_out_gaa) → ACKERMANN_IN_GAG(M, Val)

The TRS R consists of the following rules:

ackermann_in_gaa(s(M)) → U1_gaa(ackermann_in_gga(M, s(0)))
ackermann_in_gaa(s(M)) → U2_gaa(M, ackermann_in_gaa(s(M)))
U1_gaa(ackermann_out_gga(Val)) → ackermann_out_gaa
U2_gaa(M, ackermann_out_gaa) → U3_gaa(ackermann_in_gaa(M))
ackermann_in_gga(0, N) → ackermann_out_gga(s(N))
ackermann_in_gga(s(M), s(N)) → U2_gga(M, ackermann_in_gga(s(M), N))
U3_gaa(ackermann_out_gaa) → ackermann_out_gaa
U2_gga(M, ackermann_out_gga(Val1)) → U3_gga(ackermann_in_gga(M, Val1))
ackermann_in_gaa(0) → ackermann_out_gaa
ackermann_in_gga(s(M), 0) → U1_gga(ackermann_in_gga(M, s(0)))
U3_gga(ackermann_out_gga(Val)) → ackermann_out_gga(Val)
U1_gga(ackermann_out_gga(Val)) → ackermann_out_gga(Val)

The set Q consists of the following terms:

ackermann_in_gaa(x0)
U1_gaa(x0)
U2_gaa(x0, x1)
ackermann_in_gga(x0, x1)
U3_gaa(x0)
U2_gga(x0, x1)
U3_gga(x0)
U1_gga(x0)

We have to consider all (P,Q,R)-chains.

(83) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

U2_GAG(M, Val, ackermann_out_gaa) → ACKERMANN_IN_GAG(M, Val)
The graph contains the following edges 1 >= 1, 2 >= 2
ACKERMANN_IN_GAG(s(M), Val) → U2_GAG(M, Val, ackermann_in_gaa(s(M)))
The graph contains the following edges 1 > 1, 2 >= 2