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

0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇐)
↳2 Prolog
    ↳3 PrologToPiTRSProof (⇐)
        ↳4 PiTRS
        ↳5 DependencyPairsProof (⇔)
        ↳6 PiDP
        ↳7 DependencyGraphProof (⇔)
        ↳8 AND
            ↳9 PiDP
                ↳10 UsableRulesProof (⇔)
                ↳11 PiDP
                ↳12 PiDPToQDPProof (⇐)
                ↳13 QDP
                ↳14 Narrowing (⇐)
                ↳15 QDP
                ↳16 NonTerminationProof (⇔)
                ↳17 NO
            ↳18 PiDP
                ↳19 UsableRulesProof (⇔)
                ↳20 PiDP
                ↳21 PiDPToQDPProof (⇐)
                ↳22 QDP
                ↳23 Narrowing (⇐)
                ↳24 QDP
                ↳25 NonTerminationProof (⇔)
                ↳26 NO
            ↳27 PiDP
                ↳28 UsableRulesProof (⇔)
                ↳29 PiDP
                ↳30 PiDPToQDPProof (⇐)
                ↳31 QDP
                ↳32 QDPSizeChangeProof (⇔)
                ↳33 YES
    ↳34 PrologToPiTRSProof (⇐)
        ↳35 PiTRS
        ↳36 DependencyPairsProof (⇔)
        ↳37 PiDP
        ↳38 DependencyGraphProof (⇔)
        ↳39 AND
            ↳40 PiDP
                ↳41 UsableRulesProof (⇔)
                ↳42 PiDP
                ↳43 PiDPToQDPProof (⇐)
                ↳44 QDP
                ↳45 Narrowing (⇐)
                ↳46 QDP
                ↳47 NonTerminationProof (⇔)
                ↳48 NO
            ↳49 PiDP
                ↳50 UsableRulesProof (⇔)
                ↳51 PiDP
                ↳52 PiDPToQDPProof (⇐)
                ↳53 QDP
                ↳54 Narrowing (⇐)
                ↳55 QDP
                ↳56 NonTerminationProof (⇔)
                ↳57 NO
            ↳58 PiDP
                ↳59 UsableRulesProof (⇔)
                ↳60 PiDP
                ↳61 PiDPToQDPProof (⇐)
                ↳62 QDP
                ↳63 QDPSizeChangeProof (⇔)
                ↳64 YES

(0) Obligation:

Clauses:

f(0, Y, 0).
f(s(X), Y, Z) :- ','(f(X, Y, U), f(U, Y, Z)).

Queries:

f(g,a,a).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

(2) Obligation:

Clauses:

p7(0, T27, 0, 0).
p7(s(T32), T34, X47, T35) :- f23(T32, T34, X46).
p7(s(T32), T39, X47, T40) :- ','(f23(T32, T39, T38), p7(T38, T39, X47, T40)).
f23(0, T47, 0).
f23(s(T52), T54, X74) :- f23(T52, T54, X73).
f23(s(T52), T58, X74) :- ','(f23(T52, T58, T57), f23(T57, T58, X74)).
f1(0, T5, 0).
f1(s(T9), T12, T13) :- p7(T9, T12, X13, T13).

Queries:

f1(g,a,a).

(3) PrologToPiTRSProof (SOUND transformation)

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

f1_in_gaa(0, T5, 0) → f1_out_gaa(0, T5, 0)
f1_in_gaa(s(T9), T12, T13) → U7_gaa(T9, T12, T13, p7_in_gaaa(T9, T12, X13, T13))
p7_in_gaaa(0, T27, 0, 0) → p7_out_gaaa(0, T27, 0, 0)
p7_in_gaaa(s(T32), T34, X47, T35) → U1_gaaa(T32, T34, X47, T35, f23_in_gaa(T32, T34, X46))
f23_in_gaa(0, T47, 0) → f23_out_gaa(0, T47, 0)
f23_in_gaa(s(T52), T54, X74) → U4_gaa(T52, T54, X74, f23_in_gaa(T52, T54, X73))
f23_in_gaa(s(T52), T58, X74) → U5_gaa(T52, T58, X74, f23_in_gaa(T52, T58, T57))
U5_gaa(T52, T58, X74, f23_out_gaa(T52, T58, T57)) → U6_gaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
f23_in_aaa(0, T47, 0) → f23_out_aaa(0, T47, 0)
f23_in_aaa(s(T52), T54, X74) → U4_aaa(T52, T54, X74, f23_in_aaa(T52, T54, X73))
f23_in_aaa(s(T52), T58, X74) → U5_aaa(T52, T58, X74, f23_in_aaa(T52, T58, T57))
U5_aaa(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → U6_aaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
U6_aaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_aaa(s(T52), T58, X74)
U4_aaa(T52, T54, X74, f23_out_aaa(T52, T54, X73)) → f23_out_aaa(s(T52), T54, X74)
U6_gaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_gaa(s(T52), T58, X74)
U4_gaa(T52, T54, X74, f23_out_gaa(T52, T54, X73)) → f23_out_gaa(s(T52), T54, X74)
U1_gaaa(T32, T34, X47, T35, f23_out_gaa(T32, T34, X46)) → p7_out_gaaa(s(T32), T34, X47, T35)
p7_in_gaaa(s(T32), T39, X47, T40) → U2_gaaa(T32, T39, X47, T40, f23_in_gaa(T32, T39, T38))
U2_gaaa(T32, T39, X47, T40, f23_out_gaa(T32, T39, T38)) → U3_gaaa(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
p7_in_aaaa(0, T27, 0, 0) → p7_out_aaaa(0, T27, 0, 0)
p7_in_aaaa(s(T32), T34, X47, T35) → U1_aaaa(T32, T34, X47, T35, f23_in_aaa(T32, T34, X46))
U1_aaaa(T32, T34, X47, T35, f23_out_aaa(T32, T34, X46)) → p7_out_aaaa(s(T32), T34, X47, T35)
p7_in_aaaa(s(T32), T39, X47, T40) → U2_aaaa(T32, T39, X47, T40, f23_in_aaa(T32, T39, T38))
U2_aaaa(T32, T39, X47, T40, f23_out_aaa(T32, T39, T38)) → U3_aaaa(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
U3_aaaa(T32, T39, X47, T40, p7_out_aaaa(T38, T39, X47, T40)) → p7_out_aaaa(s(T32), T39, X47, T40)
U3_gaaa(T32, T39, X47, T40, p7_out_aaaa(T38, T39, X47, T40)) → p7_out_gaaa(s(T32), T39, X47, T40)
U7_gaa(T9, T12, T13, p7_out_gaaa(T9, T12, X13, T13)) → f1_out_gaa(s(T9), T12, T13)

The argument filtering Pi contains the following mapping:
f1_in_gaa(x1, x2, x3)  =  f1_in_gaa(x1)
0  =  0
f1_out_gaa(x1, x2, x3)  =  f1_out_gaa
s(x1)  =  s(x1)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x4)
p7_in_gaaa(x1, x2, x3, x4)  =  p7_in_gaaa(x1)
p7_out_gaaa(x1, x2, x3, x4)  =  p7_out_gaaa
U1_gaaa(x1, x2, x3, x4, x5)  =  U1_gaaa(x5)
f23_in_gaa(x1, x2, x3)  =  f23_in_gaa(x1)
f23_out_gaa(x1, x2, x3)  =  f23_out_gaa
U4_gaa(x1, x2, x3, x4)  =  U4_gaa(x4)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x4)
f23_in_aaa(x1, x2, x3)  =  f23_in_aaa
f23_out_aaa(x1, x2, x3)  =  f23_out_aaa(x1)
U4_aaa(x1, x2, x3, x4)  =  U4_aaa(x4)
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
U6_aaa(x1, x2, x3, x4)  =  U6_aaa(x1, x4)
U2_gaaa(x1, x2, x3, x4, x5)  =  U2_gaaa(x5)
U3_gaaa(x1, x2, x3, x4, x5)  =  U3_gaaa(x5)
p7_in_aaaa(x1, x2, x3, x4)  =  p7_in_aaaa
p7_out_aaaa(x1, x2, x3, x4)  =  p7_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5)  =  U1_aaaa(x5)
U2_aaaa(x1, x2, x3, x4, x5)  =  U2_aaaa(x5)
U3_aaaa(x1, x2, x3, x4, x5)  =  U3_aaaa(x1, x5)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

f1_in_gaa(0, T5, 0) → f1_out_gaa(0, T5, 0)
f1_in_gaa(s(T9), T12, T13) → U7_gaa(T9, T12, T13, p7_in_gaaa(T9, T12, X13, T13))
p7_in_gaaa(0, T27, 0, 0) → p7_out_gaaa(0, T27, 0, 0)
p7_in_gaaa(s(T32), T34, X47, T35) → U1_gaaa(T32, T34, X47, T35, f23_in_gaa(T32, T34, X46))
f23_in_gaa(0, T47, 0) → f23_out_gaa(0, T47, 0)
f23_in_gaa(s(T52), T54, X74) → U4_gaa(T52, T54, X74, f23_in_gaa(T52, T54, X73))
f23_in_gaa(s(T52), T58, X74) → U5_gaa(T52, T58, X74, f23_in_gaa(T52, T58, T57))
U5_gaa(T52, T58, X74, f23_out_gaa(T52, T58, T57)) → U6_gaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
f23_in_aaa(0, T47, 0) → f23_out_aaa(0, T47, 0)
f23_in_aaa(s(T52), T54, X74) → U4_aaa(T52, T54, X74, f23_in_aaa(T52, T54, X73))
f23_in_aaa(s(T52), T58, X74) → U5_aaa(T52, T58, X74, f23_in_aaa(T52, T58, T57))
U5_aaa(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → U6_aaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
U6_aaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_aaa(s(T52), T58, X74)
U4_aaa(T52, T54, X74, f23_out_aaa(T52, T54, X73)) → f23_out_aaa(s(T52), T54, X74)
U6_gaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_gaa(s(T52), T58, X74)
U4_gaa(T52, T54, X74, f23_out_gaa(T52, T54, X73)) → f23_out_gaa(s(T52), T54, X74)
U1_gaaa(T32, T34, X47, T35, f23_out_gaa(T32, T34, X46)) → p7_out_gaaa(s(T32), T34, X47, T35)
p7_in_gaaa(s(T32), T39, X47, T40) → U2_gaaa(T32, T39, X47, T40, f23_in_gaa(T32, T39, T38))
U2_gaaa(T32, T39, X47, T40, f23_out_gaa(T32, T39, T38)) → U3_gaaa(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
p7_in_aaaa(0, T27, 0, 0) → p7_out_aaaa(0, T27, 0, 0)
p7_in_aaaa(s(T32), T34, X47, T35) → U1_aaaa(T32, T34, X47, T35, f23_in_aaa(T32, T34, X46))
U1_aaaa(T32, T34, X47, T35, f23_out_aaa(T32, T34, X46)) → p7_out_aaaa(s(T32), T34, X47, T35)
p7_in_aaaa(s(T32), T39, X47, T40) → U2_aaaa(T32, T39, X47, T40, f23_in_aaa(T32, T39, T38))
U2_aaaa(T32, T39, X47, T40, f23_out_aaa(T32, T39, T38)) → U3_aaaa(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
U3_aaaa(T32, T39, X47, T40, p7_out_aaaa(T38, T39, X47, T40)) → p7_out_aaaa(s(T32), T39, X47, T40)
U3_gaaa(T32, T39, X47, T40, p7_out_aaaa(T38, T39, X47, T40)) → p7_out_gaaa(s(T32), T39, X47, T40)
U7_gaa(T9, T12, T13, p7_out_gaaa(T9, T12, X13, T13)) → f1_out_gaa(s(T9), T12, T13)

The argument filtering Pi contains the following mapping:
f1_in_gaa(x1, x2, x3)  =  f1_in_gaa(x1)
0  =  0
f1_out_gaa(x1, x2, x3)  =  f1_out_gaa
s(x1)  =  s(x1)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x4)
p7_in_gaaa(x1, x2, x3, x4)  =  p7_in_gaaa(x1)
p7_out_gaaa(x1, x2, x3, x4)  =  p7_out_gaaa
U1_gaaa(x1, x2, x3, x4, x5)  =  U1_gaaa(x5)
f23_in_gaa(x1, x2, x3)  =  f23_in_gaa(x1)
f23_out_gaa(x1, x2, x3)  =  f23_out_gaa
U4_gaa(x1, x2, x3, x4)  =  U4_gaa(x4)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x4)
f23_in_aaa(x1, x2, x3)  =  f23_in_aaa
f23_out_aaa(x1, x2, x3)  =  f23_out_aaa(x1)
U4_aaa(x1, x2, x3, x4)  =  U4_aaa(x4)
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
U6_aaa(x1, x2, x3, x4)  =  U6_aaa(x1, x4)
U2_gaaa(x1, x2, x3, x4, x5)  =  U2_gaaa(x5)
U3_gaaa(x1, x2, x3, x4, x5)  =  U3_gaaa(x5)
p7_in_aaaa(x1, x2, x3, x4)  =  p7_in_aaaa
p7_out_aaaa(x1, x2, x3, x4)  =  p7_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5)  =  U1_aaaa(x5)
U2_aaaa(x1, x2, x3, x4, x5)  =  U2_aaaa(x5)
U3_aaaa(x1, x2, x3, x4, x5)  =  U3_aaaa(x1, x5)

(5) 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:

F1_IN_GAA(s(T9), T12, T13) → U7_GAA(T9, T12, T13, p7_in_gaaa(T9, T12, X13, T13))
F1_IN_GAA(s(T9), T12, T13) → P7_IN_GAAA(T9, T12, X13, T13)
P7_IN_GAAA(s(T32), T34, X47, T35) → U1_GAAA(T32, T34, X47, T35, f23_in_gaa(T32, T34, X46))
P7_IN_GAAA(s(T32), T34, X47, T35) → F23_IN_GAA(T32, T34, X46)
F23_IN_GAA(s(T52), T54, X74) → U4_GAA(T52, T54, X74, f23_in_gaa(T52, T54, X73))
F23_IN_GAA(s(T52), T54, X74) → F23_IN_GAA(T52, T54, X73)
F23_IN_GAA(s(T52), T58, X74) → U5_GAA(T52, T58, X74, f23_in_gaa(T52, T58, T57))
U5_GAA(T52, T58, X74, f23_out_gaa(T52, T58, T57)) → U6_GAA(T52, T58, X74, f23_in_aaa(T57, T58, X74))
U5_GAA(T52, T58, X74, f23_out_gaa(T52, T58, T57)) → F23_IN_AAA(T57, T58, X74)
F23_IN_AAA(s(T52), T54, X74) → U4_AAA(T52, T54, X74, f23_in_aaa(T52, T54, X73))
F23_IN_AAA(s(T52), T54, X74) → F23_IN_AAA(T52, T54, X73)
F23_IN_AAA(s(T52), T58, X74) → U5_AAA(T52, T58, X74, f23_in_aaa(T52, T58, T57))
U5_AAA(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → U6_AAA(T52, T58, X74, f23_in_aaa(T57, T58, X74))
U5_AAA(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → F23_IN_AAA(T57, T58, X74)
P7_IN_GAAA(s(T32), T39, X47, T40) → U2_GAAA(T32, T39, X47, T40, f23_in_gaa(T32, T39, T38))
U2_GAAA(T32, T39, X47, T40, f23_out_gaa(T32, T39, T38)) → U3_GAAA(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
U2_GAAA(T32, T39, X47, T40, f23_out_gaa(T32, T39, T38)) → P7_IN_AAAA(T38, T39, X47, T40)
P7_IN_AAAA(s(T32), T34, X47, T35) → U1_AAAA(T32, T34, X47, T35, f23_in_aaa(T32, T34, X46))
P7_IN_AAAA(s(T32), T34, X47, T35) → F23_IN_AAA(T32, T34, X46)
P7_IN_AAAA(s(T32), T39, X47, T40) → U2_AAAA(T32, T39, X47, T40, f23_in_aaa(T32, T39, T38))
U2_AAAA(T32, T39, X47, T40, f23_out_aaa(T32, T39, T38)) → U3_AAAA(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
U2_AAAA(T32, T39, X47, T40, f23_out_aaa(T32, T39, T38)) → P7_IN_AAAA(T38, T39, X47, T40)

The TRS R consists of the following rules:

f1_in_gaa(0, T5, 0) → f1_out_gaa(0, T5, 0)
f1_in_gaa(s(T9), T12, T13) → U7_gaa(T9, T12, T13, p7_in_gaaa(T9, T12, X13, T13))
p7_in_gaaa(0, T27, 0, 0) → p7_out_gaaa(0, T27, 0, 0)
p7_in_gaaa(s(T32), T34, X47, T35) → U1_gaaa(T32, T34, X47, T35, f23_in_gaa(T32, T34, X46))
f23_in_gaa(0, T47, 0) → f23_out_gaa(0, T47, 0)
f23_in_gaa(s(T52), T54, X74) → U4_gaa(T52, T54, X74, f23_in_gaa(T52, T54, X73))
f23_in_gaa(s(T52), T58, X74) → U5_gaa(T52, T58, X74, f23_in_gaa(T52, T58, T57))
U5_gaa(T52, T58, X74, f23_out_gaa(T52, T58, T57)) → U6_gaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
f23_in_aaa(0, T47, 0) → f23_out_aaa(0, T47, 0)
f23_in_aaa(s(T52), T54, X74) → U4_aaa(T52, T54, X74, f23_in_aaa(T52, T54, X73))
f23_in_aaa(s(T52), T58, X74) → U5_aaa(T52, T58, X74, f23_in_aaa(T52, T58, T57))
U5_aaa(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → U6_aaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
U6_aaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_aaa(s(T52), T58, X74)
U4_aaa(T52, T54, X74, f23_out_aaa(T52, T54, X73)) → f23_out_aaa(s(T52), T54, X74)
U6_gaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_gaa(s(T52), T58, X74)
U4_gaa(T52, T54, X74, f23_out_gaa(T52, T54, X73)) → f23_out_gaa(s(T52), T54, X74)
U1_gaaa(T32, T34, X47, T35, f23_out_gaa(T32, T34, X46)) → p7_out_gaaa(s(T32), T34, X47, T35)
p7_in_gaaa(s(T32), T39, X47, T40) → U2_gaaa(T32, T39, X47, T40, f23_in_gaa(T32, T39, T38))
U2_gaaa(T32, T39, X47, T40, f23_out_gaa(T32, T39, T38)) → U3_gaaa(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
p7_in_aaaa(0, T27, 0, 0) → p7_out_aaaa(0, T27, 0, 0)
p7_in_aaaa(s(T32), T34, X47, T35) → U1_aaaa(T32, T34, X47, T35, f23_in_aaa(T32, T34, X46))
U1_aaaa(T32, T34, X47, T35, f23_out_aaa(T32, T34, X46)) → p7_out_aaaa(s(T32), T34, X47, T35)
p7_in_aaaa(s(T32), T39, X47, T40) → U2_aaaa(T32, T39, X47, T40, f23_in_aaa(T32, T39, T38))
U2_aaaa(T32, T39, X47, T40, f23_out_aaa(T32, T39, T38)) → U3_aaaa(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
U3_aaaa(T32, T39, X47, T40, p7_out_aaaa(T38, T39, X47, T40)) → p7_out_aaaa(s(T32), T39, X47, T40)
U3_gaaa(T32, T39, X47, T40, p7_out_aaaa(T38, T39, X47, T40)) → p7_out_gaaa(s(T32), T39, X47, T40)
U7_gaa(T9, T12, T13, p7_out_gaaa(T9, T12, X13, T13)) → f1_out_gaa(s(T9), T12, T13)

The argument filtering Pi contains the following mapping:
f1_in_gaa(x1, x2, x3)  =  f1_in_gaa(x1)
0  =  0
f1_out_gaa(x1, x2, x3)  =  f1_out_gaa
s(x1)  =  s(x1)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x4)
p7_in_gaaa(x1, x2, x3, x4)  =  p7_in_gaaa(x1)
p7_out_gaaa(x1, x2, x3, x4)  =  p7_out_gaaa
U1_gaaa(x1, x2, x3, x4, x5)  =  U1_gaaa(x5)
f23_in_gaa(x1, x2, x3)  =  f23_in_gaa(x1)
f23_out_gaa(x1, x2, x3)  =  f23_out_gaa
U4_gaa(x1, x2, x3, x4)  =  U4_gaa(x4)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x4)
f23_in_aaa(x1, x2, x3)  =  f23_in_aaa
f23_out_aaa(x1, x2, x3)  =  f23_out_aaa(x1)
U4_aaa(x1, x2, x3, x4)  =  U4_aaa(x4)
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
U6_aaa(x1, x2, x3, x4)  =  U6_aaa(x1, x4)
U2_gaaa(x1, x2, x3, x4, x5)  =  U2_gaaa(x5)
U3_gaaa(x1, x2, x3, x4, x5)  =  U3_gaaa(x5)
p7_in_aaaa(x1, x2, x3, x4)  =  p7_in_aaaa
p7_out_aaaa(x1, x2, x3, x4)  =  p7_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5)  =  U1_aaaa(x5)
U2_aaaa(x1, x2, x3, x4, x5)  =  U2_aaaa(x5)
U3_aaaa(x1, x2, x3, x4, x5)  =  U3_aaaa(x1, x5)
F1_IN_GAA(x1, x2, x3)  =  F1_IN_GAA(x1)
U7_GAA(x1, x2, x3, x4)  =  U7_GAA(x4)
P7_IN_GAAA(x1, x2, x3, x4)  =  P7_IN_GAAA(x1)
U1_GAAA(x1, x2, x3, x4, x5)  =  U1_GAAA(x5)
F23_IN_GAA(x1, x2, x3)  =  F23_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4)  =  U4_GAA(x4)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x4)
U6_GAA(x1, x2, x3, x4)  =  U6_GAA(x4)
F23_IN_AAA(x1, x2, x3)  =  F23_IN_AAA
U4_AAA(x1, x2, x3, x4)  =  U4_AAA(x4)
U5_AAA(x1, x2, x3, x4)  =  U5_AAA(x4)
U6_AAA(x1, x2, x3, x4)  =  U6_AAA(x1, x4)
U2_GAAA(x1, x2, x3, x4, x5)  =  U2_GAAA(x5)
U3_GAAA(x1, x2, x3, x4, x5)  =  U3_GAAA(x5)
P7_IN_AAAA(x1, x2, x3, x4)  =  P7_IN_AAAA
U1_AAAA(x1, x2, x3, x4, x5)  =  U1_AAAA(x5)
U2_AAAA(x1, x2, x3, x4, x5)  =  U2_AAAA(x5)
U3_AAAA(x1, x2, x3, x4, x5)  =  U3_AAAA(x1, x5)

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

(6) Obligation:

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

F1_IN_GAA(s(T9), T12, T13) → U7_GAA(T9, T12, T13, p7_in_gaaa(T9, T12, X13, T13))
F1_IN_GAA(s(T9), T12, T13) → P7_IN_GAAA(T9, T12, X13, T13)
P7_IN_GAAA(s(T32), T34, X47, T35) → U1_GAAA(T32, T34, X47, T35, f23_in_gaa(T32, T34, X46))
P7_IN_GAAA(s(T32), T34, X47, T35) → F23_IN_GAA(T32, T34, X46)
F23_IN_GAA(s(T52), T54, X74) → U4_GAA(T52, T54, X74, f23_in_gaa(T52, T54, X73))
F23_IN_GAA(s(T52), T54, X74) → F23_IN_GAA(T52, T54, X73)
F23_IN_GAA(s(T52), T58, X74) → U5_GAA(T52, T58, X74, f23_in_gaa(T52, T58, T57))
U5_GAA(T52, T58, X74, f23_out_gaa(T52, T58, T57)) → U6_GAA(T52, T58, X74, f23_in_aaa(T57, T58, X74))
U5_GAA(T52, T58, X74, f23_out_gaa(T52, T58, T57)) → F23_IN_AAA(T57, T58, X74)
F23_IN_AAA(s(T52), T54, X74) → U4_AAA(T52, T54, X74, f23_in_aaa(T52, T54, X73))
F23_IN_AAA(s(T52), T54, X74) → F23_IN_AAA(T52, T54, X73)
F23_IN_AAA(s(T52), T58, X74) → U5_AAA(T52, T58, X74, f23_in_aaa(T52, T58, T57))
U5_AAA(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → U6_AAA(T52, T58, X74, f23_in_aaa(T57, T58, X74))
U5_AAA(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → F23_IN_AAA(T57, T58, X74)
P7_IN_GAAA(s(T32), T39, X47, T40) → U2_GAAA(T32, T39, X47, T40, f23_in_gaa(T32, T39, T38))
U2_GAAA(T32, T39, X47, T40, f23_out_gaa(T32, T39, T38)) → U3_GAAA(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
U2_GAAA(T32, T39, X47, T40, f23_out_gaa(T32, T39, T38)) → P7_IN_AAAA(T38, T39, X47, T40)
P7_IN_AAAA(s(T32), T34, X47, T35) → U1_AAAA(T32, T34, X47, T35, f23_in_aaa(T32, T34, X46))
P7_IN_AAAA(s(T32), T34, X47, T35) → F23_IN_AAA(T32, T34, X46)
P7_IN_AAAA(s(T32), T39, X47, T40) → U2_AAAA(T32, T39, X47, T40, f23_in_aaa(T32, T39, T38))
U2_AAAA(T32, T39, X47, T40, f23_out_aaa(T32, T39, T38)) → U3_AAAA(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
U2_AAAA(T32, T39, X47, T40, f23_out_aaa(T32, T39, T38)) → P7_IN_AAAA(T38, T39, X47, T40)

The TRS R consists of the following rules:

f1_in_gaa(0, T5, 0) → f1_out_gaa(0, T5, 0)
f1_in_gaa(s(T9), T12, T13) → U7_gaa(T9, T12, T13, p7_in_gaaa(T9, T12, X13, T13))
p7_in_gaaa(0, T27, 0, 0) → p7_out_gaaa(0, T27, 0, 0)
p7_in_gaaa(s(T32), T34, X47, T35) → U1_gaaa(T32, T34, X47, T35, f23_in_gaa(T32, T34, X46))
f23_in_gaa(0, T47, 0) → f23_out_gaa(0, T47, 0)
f23_in_gaa(s(T52), T54, X74) → U4_gaa(T52, T54, X74, f23_in_gaa(T52, T54, X73))
f23_in_gaa(s(T52), T58, X74) → U5_gaa(T52, T58, X74, f23_in_gaa(T52, T58, T57))
U5_gaa(T52, T58, X74, f23_out_gaa(T52, T58, T57)) → U6_gaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
f23_in_aaa(0, T47, 0) → f23_out_aaa(0, T47, 0)
f23_in_aaa(s(T52), T54, X74) → U4_aaa(T52, T54, X74, f23_in_aaa(T52, T54, X73))
f23_in_aaa(s(T52), T58, X74) → U5_aaa(T52, T58, X74, f23_in_aaa(T52, T58, T57))
U5_aaa(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → U6_aaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
U6_aaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_aaa(s(T52), T58, X74)
U4_aaa(T52, T54, X74, f23_out_aaa(T52, T54, X73)) → f23_out_aaa(s(T52), T54, X74)
U6_gaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_gaa(s(T52), T58, X74)
U4_gaa(T52, T54, X74, f23_out_gaa(T52, T54, X73)) → f23_out_gaa(s(T52), T54, X74)
U1_gaaa(T32, T34, X47, T35, f23_out_gaa(T32, T34, X46)) → p7_out_gaaa(s(T32), T34, X47, T35)
p7_in_gaaa(s(T32), T39, X47, T40) → U2_gaaa(T32, T39, X47, T40, f23_in_gaa(T32, T39, T38))
U2_gaaa(T32, T39, X47, T40, f23_out_gaa(T32, T39, T38)) → U3_gaaa(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
p7_in_aaaa(0, T27, 0, 0) → p7_out_aaaa(0, T27, 0, 0)
p7_in_aaaa(s(T32), T34, X47, T35) → U1_aaaa(T32, T34, X47, T35, f23_in_aaa(T32, T34, X46))
U1_aaaa(T32, T34, X47, T35, f23_out_aaa(T32, T34, X46)) → p7_out_aaaa(s(T32), T34, X47, T35)
p7_in_aaaa(s(T32), T39, X47, T40) → U2_aaaa(T32, T39, X47, T40, f23_in_aaa(T32, T39, T38))
U2_aaaa(T32, T39, X47, T40, f23_out_aaa(T32, T39, T38)) → U3_aaaa(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
U3_aaaa(T32, T39, X47, T40, p7_out_aaaa(T38, T39, X47, T40)) → p7_out_aaaa(s(T32), T39, X47, T40)
U3_gaaa(T32, T39, X47, T40, p7_out_aaaa(T38, T39, X47, T40)) → p7_out_gaaa(s(T32), T39, X47, T40)
U7_gaa(T9, T12, T13, p7_out_gaaa(T9, T12, X13, T13)) → f1_out_gaa(s(T9), T12, T13)

The argument filtering Pi contains the following mapping:
f1_in_gaa(x1, x2, x3)  =  f1_in_gaa(x1)
0  =  0
f1_out_gaa(x1, x2, x3)  =  f1_out_gaa
s(x1)  =  s(x1)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x4)
p7_in_gaaa(x1, x2, x3, x4)  =  p7_in_gaaa(x1)
p7_out_gaaa(x1, x2, x3, x4)  =  p7_out_gaaa
U1_gaaa(x1, x2, x3, x4, x5)  =  U1_gaaa(x5)
f23_in_gaa(x1, x2, x3)  =  f23_in_gaa(x1)
f23_out_gaa(x1, x2, x3)  =  f23_out_gaa
U4_gaa(x1, x2, x3, x4)  =  U4_gaa(x4)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x4)
f23_in_aaa(x1, x2, x3)  =  f23_in_aaa
f23_out_aaa(x1, x2, x3)  =  f23_out_aaa(x1)
U4_aaa(x1, x2, x3, x4)  =  U4_aaa(x4)
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
U6_aaa(x1, x2, x3, x4)  =  U6_aaa(x1, x4)
U2_gaaa(x1, x2, x3, x4, x5)  =  U2_gaaa(x5)
U3_gaaa(x1, x2, x3, x4, x5)  =  U3_gaaa(x5)
p7_in_aaaa(x1, x2, x3, x4)  =  p7_in_aaaa
p7_out_aaaa(x1, x2, x3, x4)  =  p7_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5)  =  U1_aaaa(x5)
U2_aaaa(x1, x2, x3, x4, x5)  =  U2_aaaa(x5)
U3_aaaa(x1, x2, x3, x4, x5)  =  U3_aaaa(x1, x5)
F1_IN_GAA(x1, x2, x3)  =  F1_IN_GAA(x1)
U7_GAA(x1, x2, x3, x4)  =  U7_GAA(x4)
P7_IN_GAAA(x1, x2, x3, x4)  =  P7_IN_GAAA(x1)
U1_GAAA(x1, x2, x3, x4, x5)  =  U1_GAAA(x5)
F23_IN_GAA(x1, x2, x3)  =  F23_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4)  =  U4_GAA(x4)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x4)
U6_GAA(x1, x2, x3, x4)  =  U6_GAA(x4)
F23_IN_AAA(x1, x2, x3)  =  F23_IN_AAA
U4_AAA(x1, x2, x3, x4)  =  U4_AAA(x4)
U5_AAA(x1, x2, x3, x4)  =  U5_AAA(x4)
U6_AAA(x1, x2, x3, x4)  =  U6_AAA(x1, x4)
U2_GAAA(x1, x2, x3, x4, x5)  =  U2_GAAA(x5)
U3_GAAA(x1, x2, x3, x4, x5)  =  U3_GAAA(x5)
P7_IN_AAAA(x1, x2, x3, x4)  =  P7_IN_AAAA
U1_AAAA(x1, x2, x3, x4, x5)  =  U1_AAAA(x5)
U2_AAAA(x1, x2, x3, x4, x5)  =  U2_AAAA(x5)
U3_AAAA(x1, x2, x3, x4, x5)  =  U3_AAAA(x1, x5)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 16 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

F23_IN_AAA(s(T52), T58, X74) → U5_AAA(T52, T58, X74, f23_in_aaa(T52, T58, T57))
U5_AAA(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → F23_IN_AAA(T57, T58, X74)
F23_IN_AAA(s(T52), T54, X74) → F23_IN_AAA(T52, T54, X73)

The TRS R consists of the following rules:

f1_in_gaa(0, T5, 0) → f1_out_gaa(0, T5, 0)
f1_in_gaa(s(T9), T12, T13) → U7_gaa(T9, T12, T13, p7_in_gaaa(T9, T12, X13, T13))
p7_in_gaaa(0, T27, 0, 0) → p7_out_gaaa(0, T27, 0, 0)
p7_in_gaaa(s(T32), T34, X47, T35) → U1_gaaa(T32, T34, X47, T35, f23_in_gaa(T32, T34, X46))
f23_in_gaa(0, T47, 0) → f23_out_gaa(0, T47, 0)
f23_in_gaa(s(T52), T54, X74) → U4_gaa(T52, T54, X74, f23_in_gaa(T52, T54, X73))
f23_in_gaa(s(T52), T58, X74) → U5_gaa(T52, T58, X74, f23_in_gaa(T52, T58, T57))
U5_gaa(T52, T58, X74, f23_out_gaa(T52, T58, T57)) → U6_gaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
f23_in_aaa(0, T47, 0) → f23_out_aaa(0, T47, 0)
f23_in_aaa(s(T52), T54, X74) → U4_aaa(T52, T54, X74, f23_in_aaa(T52, T54, X73))
f23_in_aaa(s(T52), T58, X74) → U5_aaa(T52, T58, X74, f23_in_aaa(T52, T58, T57))
U5_aaa(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → U6_aaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
U6_aaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_aaa(s(T52), T58, X74)
U4_aaa(T52, T54, X74, f23_out_aaa(T52, T54, X73)) → f23_out_aaa(s(T52), T54, X74)
U6_gaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_gaa(s(T52), T58, X74)
U4_gaa(T52, T54, X74, f23_out_gaa(T52, T54, X73)) → f23_out_gaa(s(T52), T54, X74)
U1_gaaa(T32, T34, X47, T35, f23_out_gaa(T32, T34, X46)) → p7_out_gaaa(s(T32), T34, X47, T35)
p7_in_gaaa(s(T32), T39, X47, T40) → U2_gaaa(T32, T39, X47, T40, f23_in_gaa(T32, T39, T38))
U2_gaaa(T32, T39, X47, T40, f23_out_gaa(T32, T39, T38)) → U3_gaaa(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
p7_in_aaaa(0, T27, 0, 0) → p7_out_aaaa(0, T27, 0, 0)
p7_in_aaaa(s(T32), T34, X47, T35) → U1_aaaa(T32, T34, X47, T35, f23_in_aaa(T32, T34, X46))
U1_aaaa(T32, T34, X47, T35, f23_out_aaa(T32, T34, X46)) → p7_out_aaaa(s(T32), T34, X47, T35)
p7_in_aaaa(s(T32), T39, X47, T40) → U2_aaaa(T32, T39, X47, T40, f23_in_aaa(T32, T39, T38))
U2_aaaa(T32, T39, X47, T40, f23_out_aaa(T32, T39, T38)) → U3_aaaa(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
U3_aaaa(T32, T39, X47, T40, p7_out_aaaa(T38, T39, X47, T40)) → p7_out_aaaa(s(T32), T39, X47, T40)
U3_gaaa(T32, T39, X47, T40, p7_out_aaaa(T38, T39, X47, T40)) → p7_out_gaaa(s(T32), T39, X47, T40)
U7_gaa(T9, T12, T13, p7_out_gaaa(T9, T12, X13, T13)) → f1_out_gaa(s(T9), T12, T13)

The argument filtering Pi contains the following mapping:
f1_in_gaa(x1, x2, x3)  =  f1_in_gaa(x1)
0  =  0
f1_out_gaa(x1, x2, x3)  =  f1_out_gaa
s(x1)  =  s(x1)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x4)
p7_in_gaaa(x1, x2, x3, x4)  =  p7_in_gaaa(x1)
p7_out_gaaa(x1, x2, x3, x4)  =  p7_out_gaaa
U1_gaaa(x1, x2, x3, x4, x5)  =  U1_gaaa(x5)
f23_in_gaa(x1, x2, x3)  =  f23_in_gaa(x1)
f23_out_gaa(x1, x2, x3)  =  f23_out_gaa
U4_gaa(x1, x2, x3, x4)  =  U4_gaa(x4)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x4)
f23_in_aaa(x1, x2, x3)  =  f23_in_aaa
f23_out_aaa(x1, x2, x3)  =  f23_out_aaa(x1)
U4_aaa(x1, x2, x3, x4)  =  U4_aaa(x4)
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
U6_aaa(x1, x2, x3, x4)  =  U6_aaa(x1, x4)
U2_gaaa(x1, x2, x3, x4, x5)  =  U2_gaaa(x5)
U3_gaaa(x1, x2, x3, x4, x5)  =  U3_gaaa(x5)
p7_in_aaaa(x1, x2, x3, x4)  =  p7_in_aaaa
p7_out_aaaa(x1, x2, x3, x4)  =  p7_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5)  =  U1_aaaa(x5)
U2_aaaa(x1, x2, x3, x4, x5)  =  U2_aaaa(x5)
U3_aaaa(x1, x2, x3, x4, x5)  =  U3_aaaa(x1, x5)
F23_IN_AAA(x1, x2, x3)  =  F23_IN_AAA
U5_AAA(x1, x2, x3, x4)  =  U5_AAA(x4)

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

(10) UsableRulesProof (EQUIVALENT transformation)

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

(11) Obligation:

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

F23_IN_AAA(s(T52), T58, X74) → U5_AAA(T52, T58, X74, f23_in_aaa(T52, T58, T57))
U5_AAA(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → F23_IN_AAA(T57, T58, X74)
F23_IN_AAA(s(T52), T54, X74) → F23_IN_AAA(T52, T54, X73)

The TRS R consists of the following rules:

f23_in_aaa(0, T47, 0) → f23_out_aaa(0, T47, 0)
f23_in_aaa(s(T52), T54, X74) → U4_aaa(T52, T54, X74, f23_in_aaa(T52, T54, X73))
f23_in_aaa(s(T52), T58, X74) → U5_aaa(T52, T58, X74, f23_in_aaa(T52, T58, T57))
U4_aaa(T52, T54, X74, f23_out_aaa(T52, T54, X73)) → f23_out_aaa(s(T52), T54, X74)
U5_aaa(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → U6_aaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
U6_aaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_aaa(s(T52), T58, X74)

The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
f23_in_aaa(x1, x2, x3)  =  f23_in_aaa
f23_out_aaa(x1, x2, x3)  =  f23_out_aaa(x1)
U4_aaa(x1, x2, x3, x4)  =  U4_aaa(x4)
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
U6_aaa(x1, x2, x3, x4)  =  U6_aaa(x1, x4)
F23_IN_AAA(x1, x2, x3)  =  F23_IN_AAA
U5_AAA(x1, x2, x3, x4)  =  U5_AAA(x4)

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

(12) PiDPToQDPProof (SOUND transformation)

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

(13) Obligation:

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

F23_IN_AAA → U5_AAA(f23_in_aaa)
U5_AAA(f23_out_aaa(T52)) → F23_IN_AAA
F23_IN_AAA → F23_IN_AAA

The TRS R consists of the following rules:

f23_in_aaa → f23_out_aaa(0)
f23_in_aaa → U4_aaa(f23_in_aaa)
f23_in_aaa → U5_aaa(f23_in_aaa)
U4_aaa(f23_out_aaa(T52)) → f23_out_aaa(s(T52))
U5_aaa(f23_out_aaa(T52)) → U6_aaa(T52, f23_in_aaa)
U6_aaa(T52, f23_out_aaa(T57)) → f23_out_aaa(s(T52))

The set Q consists of the following terms:

f23_in_aaa
U4_aaa(x0)
U5_aaa(x0)
U6_aaa(x0, x1)

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

(14) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule F23_IN_AAA → U5_AAA(f23_in_aaa) at position [0] we obtained the following new rules [LPAR04]:

F23_IN_AAA → U5_AAA(f23_out_aaa(0))
F23_IN_AAA → U5_AAA(U4_aaa(f23_in_aaa))
F23_IN_AAA → U5_AAA(U5_aaa(f23_in_aaa))

(15) Obligation:

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

U5_AAA(f23_out_aaa(T52)) → F23_IN_AAA
F23_IN_AAA → F23_IN_AAA
F23_IN_AAA → U5_AAA(f23_out_aaa(0))
F23_IN_AAA → U5_AAA(U4_aaa(f23_in_aaa))
F23_IN_AAA → U5_AAA(U5_aaa(f23_in_aaa))

The TRS R consists of the following rules:

f23_in_aaa → f23_out_aaa(0)
f23_in_aaa → U4_aaa(f23_in_aaa)
f23_in_aaa → U5_aaa(f23_in_aaa)
U4_aaa(f23_out_aaa(T52)) → f23_out_aaa(s(T52))
U5_aaa(f23_out_aaa(T52)) → U6_aaa(T52, f23_in_aaa)
U6_aaa(T52, f23_out_aaa(T57)) → f23_out_aaa(s(T52))

The set Q consists of the following terms:

f23_in_aaa
U4_aaa(x0)
U5_aaa(x0)
U6_aaa(x0, x1)

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

(16) 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 = F23_IN_AAA evaluates to t =F23_IN_AAA

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 F23_IN_AAA to F23_IN_AAA.



(17) NO

(18) Obligation:

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

P7_IN_AAAA(s(T32), T39, X47, T40) → U2_AAAA(T32, T39, X47, T40, f23_in_aaa(T32, T39, T38))
U2_AAAA(T32, T39, X47, T40, f23_out_aaa(T32, T39, T38)) → P7_IN_AAAA(T38, T39, X47, T40)

The TRS R consists of the following rules:

f1_in_gaa(0, T5, 0) → f1_out_gaa(0, T5, 0)
f1_in_gaa(s(T9), T12, T13) → U7_gaa(T9, T12, T13, p7_in_gaaa(T9, T12, X13, T13))
p7_in_gaaa(0, T27, 0, 0) → p7_out_gaaa(0, T27, 0, 0)
p7_in_gaaa(s(T32), T34, X47, T35) → U1_gaaa(T32, T34, X47, T35, f23_in_gaa(T32, T34, X46))
f23_in_gaa(0, T47, 0) → f23_out_gaa(0, T47, 0)
f23_in_gaa(s(T52), T54, X74) → U4_gaa(T52, T54, X74, f23_in_gaa(T52, T54, X73))
f23_in_gaa(s(T52), T58, X74) → U5_gaa(T52, T58, X74, f23_in_gaa(T52, T58, T57))
U5_gaa(T52, T58, X74, f23_out_gaa(T52, T58, T57)) → U6_gaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
f23_in_aaa(0, T47, 0) → f23_out_aaa(0, T47, 0)
f23_in_aaa(s(T52), T54, X74) → U4_aaa(T52, T54, X74, f23_in_aaa(T52, T54, X73))
f23_in_aaa(s(T52), T58, X74) → U5_aaa(T52, T58, X74, f23_in_aaa(T52, T58, T57))
U5_aaa(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → U6_aaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
U6_aaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_aaa(s(T52), T58, X74)
U4_aaa(T52, T54, X74, f23_out_aaa(T52, T54, X73)) → f23_out_aaa(s(T52), T54, X74)
U6_gaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_gaa(s(T52), T58, X74)
U4_gaa(T52, T54, X74, f23_out_gaa(T52, T54, X73)) → f23_out_gaa(s(T52), T54, X74)
U1_gaaa(T32, T34, X47, T35, f23_out_gaa(T32, T34, X46)) → p7_out_gaaa(s(T32), T34, X47, T35)
p7_in_gaaa(s(T32), T39, X47, T40) → U2_gaaa(T32, T39, X47, T40, f23_in_gaa(T32, T39, T38))
U2_gaaa(T32, T39, X47, T40, f23_out_gaa(T32, T39, T38)) → U3_gaaa(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
p7_in_aaaa(0, T27, 0, 0) → p7_out_aaaa(0, T27, 0, 0)
p7_in_aaaa(s(T32), T34, X47, T35) → U1_aaaa(T32, T34, X47, T35, f23_in_aaa(T32, T34, X46))
U1_aaaa(T32, T34, X47, T35, f23_out_aaa(T32, T34, X46)) → p7_out_aaaa(s(T32), T34, X47, T35)
p7_in_aaaa(s(T32), T39, X47, T40) → U2_aaaa(T32, T39, X47, T40, f23_in_aaa(T32, T39, T38))
U2_aaaa(T32, T39, X47, T40, f23_out_aaa(T32, T39, T38)) → U3_aaaa(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
U3_aaaa(T32, T39, X47, T40, p7_out_aaaa(T38, T39, X47, T40)) → p7_out_aaaa(s(T32), T39, X47, T40)
U3_gaaa(T32, T39, X47, T40, p7_out_aaaa(T38, T39, X47, T40)) → p7_out_gaaa(s(T32), T39, X47, T40)
U7_gaa(T9, T12, T13, p7_out_gaaa(T9, T12, X13, T13)) → f1_out_gaa(s(T9), T12, T13)

The argument filtering Pi contains the following mapping:
f1_in_gaa(x1, x2, x3)  =  f1_in_gaa(x1)
0  =  0
f1_out_gaa(x1, x2, x3)  =  f1_out_gaa
s(x1)  =  s(x1)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x4)
p7_in_gaaa(x1, x2, x3, x4)  =  p7_in_gaaa(x1)
p7_out_gaaa(x1, x2, x3, x4)  =  p7_out_gaaa
U1_gaaa(x1, x2, x3, x4, x5)  =  U1_gaaa(x5)
f23_in_gaa(x1, x2, x3)  =  f23_in_gaa(x1)
f23_out_gaa(x1, x2, x3)  =  f23_out_gaa
U4_gaa(x1, x2, x3, x4)  =  U4_gaa(x4)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x4)
f23_in_aaa(x1, x2, x3)  =  f23_in_aaa
f23_out_aaa(x1, x2, x3)  =  f23_out_aaa(x1)
U4_aaa(x1, x2, x3, x4)  =  U4_aaa(x4)
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
U6_aaa(x1, x2, x3, x4)  =  U6_aaa(x1, x4)
U2_gaaa(x1, x2, x3, x4, x5)  =  U2_gaaa(x5)
U3_gaaa(x1, x2, x3, x4, x5)  =  U3_gaaa(x5)
p7_in_aaaa(x1, x2, x3, x4)  =  p7_in_aaaa
p7_out_aaaa(x1, x2, x3, x4)  =  p7_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5)  =  U1_aaaa(x5)
U2_aaaa(x1, x2, x3, x4, x5)  =  U2_aaaa(x5)
U3_aaaa(x1, x2, x3, x4, x5)  =  U3_aaaa(x1, x5)
P7_IN_AAAA(x1, x2, x3, x4)  =  P7_IN_AAAA
U2_AAAA(x1, x2, x3, x4, x5)  =  U2_AAAA(x5)

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

(19) UsableRulesProof (EQUIVALENT transformation)

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

(20) Obligation:

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

P7_IN_AAAA(s(T32), T39, X47, T40) → U2_AAAA(T32, T39, X47, T40, f23_in_aaa(T32, T39, T38))
U2_AAAA(T32, T39, X47, T40, f23_out_aaa(T32, T39, T38)) → P7_IN_AAAA(T38, T39, X47, T40)

The TRS R consists of the following rules:

f23_in_aaa(0, T47, 0) → f23_out_aaa(0, T47, 0)
f23_in_aaa(s(T52), T54, X74) → U4_aaa(T52, T54, X74, f23_in_aaa(T52, T54, X73))
f23_in_aaa(s(T52), T58, X74) → U5_aaa(T52, T58, X74, f23_in_aaa(T52, T58, T57))
U4_aaa(T52, T54, X74, f23_out_aaa(T52, T54, X73)) → f23_out_aaa(s(T52), T54, X74)
U5_aaa(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → U6_aaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
U6_aaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_aaa(s(T52), T58, X74)

The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
f23_in_aaa(x1, x2, x3)  =  f23_in_aaa
f23_out_aaa(x1, x2, x3)  =  f23_out_aaa(x1)
U4_aaa(x1, x2, x3, x4)  =  U4_aaa(x4)
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
U6_aaa(x1, x2, x3, x4)  =  U6_aaa(x1, x4)
P7_IN_AAAA(x1, x2, x3, x4)  =  P7_IN_AAAA
U2_AAAA(x1, x2, x3, x4, x5)  =  U2_AAAA(x5)

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

(21) PiDPToQDPProof (SOUND transformation)

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

(22) Obligation:

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

P7_IN_AAAA → U2_AAAA(f23_in_aaa)
U2_AAAA(f23_out_aaa(T32)) → P7_IN_AAAA

The TRS R consists of the following rules:

f23_in_aaa → f23_out_aaa(0)
f23_in_aaa → U4_aaa(f23_in_aaa)
f23_in_aaa → U5_aaa(f23_in_aaa)
U4_aaa(f23_out_aaa(T52)) → f23_out_aaa(s(T52))
U5_aaa(f23_out_aaa(T52)) → U6_aaa(T52, f23_in_aaa)
U6_aaa(T52, f23_out_aaa(T57)) → f23_out_aaa(s(T52))

The set Q consists of the following terms:

f23_in_aaa
U4_aaa(x0)
U5_aaa(x0)
U6_aaa(x0, x1)

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

(23) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule P7_IN_AAAA → U2_AAAA(f23_in_aaa) at position [0] we obtained the following new rules [LPAR04]:

P7_IN_AAAA → U2_AAAA(f23_out_aaa(0))
P7_IN_AAAA → U2_AAAA(U4_aaa(f23_in_aaa))
P7_IN_AAAA → U2_AAAA(U5_aaa(f23_in_aaa))

(24) Obligation:

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

U2_AAAA(f23_out_aaa(T32)) → P7_IN_AAAA
P7_IN_AAAA → U2_AAAA(f23_out_aaa(0))
P7_IN_AAAA → U2_AAAA(U4_aaa(f23_in_aaa))
P7_IN_AAAA → U2_AAAA(U5_aaa(f23_in_aaa))

The TRS R consists of the following rules:

f23_in_aaa → f23_out_aaa(0)
f23_in_aaa → U4_aaa(f23_in_aaa)
f23_in_aaa → U5_aaa(f23_in_aaa)
U4_aaa(f23_out_aaa(T52)) → f23_out_aaa(s(T52))
U5_aaa(f23_out_aaa(T52)) → U6_aaa(T52, f23_in_aaa)
U6_aaa(T52, f23_out_aaa(T57)) → f23_out_aaa(s(T52))

The set Q consists of the following terms:

f23_in_aaa
U4_aaa(x0)
U5_aaa(x0)
U6_aaa(x0, x1)

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

(25) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = P7_IN_AAAA evaluates to t =P7_IN_AAAA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Matcher: [ ]
  • Semiunifier: [ ]



Rewriting sequence

P7_IN_AAAA → U2_AAAA(f23_out_aaa(0))
with rule P7_IN_AAAA → U2_AAAA(f23_out_aaa(0)) at position [] and matcher [ ]

U2_AAAA(f23_out_aaa(0)) → P7_IN_AAAA
with rule U2_AAAA(f23_out_aaa(T32)) → P7_IN_AAAA

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.



(26) NO

(27) Obligation:

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

F23_IN_GAA(s(T52), T54, X74) → F23_IN_GAA(T52, T54, X73)

The TRS R consists of the following rules:

f1_in_gaa(0, T5, 0) → f1_out_gaa(0, T5, 0)
f1_in_gaa(s(T9), T12, T13) → U7_gaa(T9, T12, T13, p7_in_gaaa(T9, T12, X13, T13))
p7_in_gaaa(0, T27, 0, 0) → p7_out_gaaa(0, T27, 0, 0)
p7_in_gaaa(s(T32), T34, X47, T35) → U1_gaaa(T32, T34, X47, T35, f23_in_gaa(T32, T34, X46))
f23_in_gaa(0, T47, 0) → f23_out_gaa(0, T47, 0)
f23_in_gaa(s(T52), T54, X74) → U4_gaa(T52, T54, X74, f23_in_gaa(T52, T54, X73))
f23_in_gaa(s(T52), T58, X74) → U5_gaa(T52, T58, X74, f23_in_gaa(T52, T58, T57))
U5_gaa(T52, T58, X74, f23_out_gaa(T52, T58, T57)) → U6_gaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
f23_in_aaa(0, T47, 0) → f23_out_aaa(0, T47, 0)
f23_in_aaa(s(T52), T54, X74) → U4_aaa(T52, T54, X74, f23_in_aaa(T52, T54, X73))
f23_in_aaa(s(T52), T58, X74) → U5_aaa(T52, T58, X74, f23_in_aaa(T52, T58, T57))
U5_aaa(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → U6_aaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
U6_aaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_aaa(s(T52), T58, X74)
U4_aaa(T52, T54, X74, f23_out_aaa(T52, T54, X73)) → f23_out_aaa(s(T52), T54, X74)
U6_gaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_gaa(s(T52), T58, X74)
U4_gaa(T52, T54, X74, f23_out_gaa(T52, T54, X73)) → f23_out_gaa(s(T52), T54, X74)
U1_gaaa(T32, T34, X47, T35, f23_out_gaa(T32, T34, X46)) → p7_out_gaaa(s(T32), T34, X47, T35)
p7_in_gaaa(s(T32), T39, X47, T40) → U2_gaaa(T32, T39, X47, T40, f23_in_gaa(T32, T39, T38))
U2_gaaa(T32, T39, X47, T40, f23_out_gaa(T32, T39, T38)) → U3_gaaa(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
p7_in_aaaa(0, T27, 0, 0) → p7_out_aaaa(0, T27, 0, 0)
p7_in_aaaa(s(T32), T34, X47, T35) → U1_aaaa(T32, T34, X47, T35, f23_in_aaa(T32, T34, X46))
U1_aaaa(T32, T34, X47, T35, f23_out_aaa(T32, T34, X46)) → p7_out_aaaa(s(T32), T34, X47, T35)
p7_in_aaaa(s(T32), T39, X47, T40) → U2_aaaa(T32, T39, X47, T40, f23_in_aaa(T32, T39, T38))
U2_aaaa(T32, T39, X47, T40, f23_out_aaa(T32, T39, T38)) → U3_aaaa(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
U3_aaaa(T32, T39, X47, T40, p7_out_aaaa(T38, T39, X47, T40)) → p7_out_aaaa(s(T32), T39, X47, T40)
U3_gaaa(T32, T39, X47, T40, p7_out_aaaa(T38, T39, X47, T40)) → p7_out_gaaa(s(T32), T39, X47, T40)
U7_gaa(T9, T12, T13, p7_out_gaaa(T9, T12, X13, T13)) → f1_out_gaa(s(T9), T12, T13)

The argument filtering Pi contains the following mapping:
f1_in_gaa(x1, x2, x3)  =  f1_in_gaa(x1)
0  =  0
f1_out_gaa(x1, x2, x3)  =  f1_out_gaa
s(x1)  =  s(x1)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x4)
p7_in_gaaa(x1, x2, x3, x4)  =  p7_in_gaaa(x1)
p7_out_gaaa(x1, x2, x3, x4)  =  p7_out_gaaa
U1_gaaa(x1, x2, x3, x4, x5)  =  U1_gaaa(x5)
f23_in_gaa(x1, x2, x3)  =  f23_in_gaa(x1)
f23_out_gaa(x1, x2, x3)  =  f23_out_gaa
U4_gaa(x1, x2, x3, x4)  =  U4_gaa(x4)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x4)
f23_in_aaa(x1, x2, x3)  =  f23_in_aaa
f23_out_aaa(x1, x2, x3)  =  f23_out_aaa(x1)
U4_aaa(x1, x2, x3, x4)  =  U4_aaa(x4)
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
U6_aaa(x1, x2, x3, x4)  =  U6_aaa(x1, x4)
U2_gaaa(x1, x2, x3, x4, x5)  =  U2_gaaa(x5)
U3_gaaa(x1, x2, x3, x4, x5)  =  U3_gaaa(x5)
p7_in_aaaa(x1, x2, x3, x4)  =  p7_in_aaaa
p7_out_aaaa(x1, x2, x3, x4)  =  p7_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5)  =  U1_aaaa(x5)
U2_aaaa(x1, x2, x3, x4, x5)  =  U2_aaaa(x5)
U3_aaaa(x1, x2, x3, x4, x5)  =  U3_aaaa(x1, x5)
F23_IN_GAA(x1, x2, x3)  =  F23_IN_GAA(x1)

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

(28) UsableRulesProof (EQUIVALENT transformation)

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

(29) Obligation:

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

F23_IN_GAA(s(T52), T54, X74) → F23_IN_GAA(T52, T54, X73)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
F23_IN_GAA(x1, x2, x3)  =  F23_IN_GAA(x1)

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

(30) PiDPToQDPProof (SOUND transformation)

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

(31) Obligation:

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

F23_IN_GAA(s(T52)) → F23_IN_GAA(T52)

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

(32) 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:

  • F23_IN_GAA(s(T52)) → F23_IN_GAA(T52)
    The graph contains the following edges 1 > 1

(33) YES

(34) PrologToPiTRSProof (SOUND transformation)

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

f1_in_gaa(0, T5, 0) → f1_out_gaa(0, T5, 0)
f1_in_gaa(s(T9), T12, T13) → U7_gaa(T9, T12, T13, p7_in_gaaa(T9, T12, X13, T13))
p7_in_gaaa(0, T27, 0, 0) → p7_out_gaaa(0, T27, 0, 0)
p7_in_gaaa(s(T32), T34, X47, T35) → U1_gaaa(T32, T34, X47, T35, f23_in_gaa(T32, T34, X46))
f23_in_gaa(0, T47, 0) → f23_out_gaa(0, T47, 0)
f23_in_gaa(s(T52), T54, X74) → U4_gaa(T52, T54, X74, f23_in_gaa(T52, T54, X73))
f23_in_gaa(s(T52), T58, X74) → U5_gaa(T52, T58, X74, f23_in_gaa(T52, T58, T57))
U5_gaa(T52, T58, X74, f23_out_gaa(T52, T58, T57)) → U6_gaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
f23_in_aaa(0, T47, 0) → f23_out_aaa(0, T47, 0)
f23_in_aaa(s(T52), T54, X74) → U4_aaa(T52, T54, X74, f23_in_aaa(T52, T54, X73))
f23_in_aaa(s(T52), T58, X74) → U5_aaa(T52, T58, X74, f23_in_aaa(T52, T58, T57))
U5_aaa(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → U6_aaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
U6_aaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_aaa(s(T52), T58, X74)
U4_aaa(T52, T54, X74, f23_out_aaa(T52, T54, X73)) → f23_out_aaa(s(T52), T54, X74)
U6_gaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_gaa(s(T52), T58, X74)
U4_gaa(T52, T54, X74, f23_out_gaa(T52, T54, X73)) → f23_out_gaa(s(T52), T54, X74)
U1_gaaa(T32, T34, X47, T35, f23_out_gaa(T32, T34, X46)) → p7_out_gaaa(s(T32), T34, X47, T35)
p7_in_gaaa(s(T32), T39, X47, T40) → U2_gaaa(T32, T39, X47, T40, f23_in_gaa(T32, T39, T38))
U2_gaaa(T32, T39, X47, T40, f23_out_gaa(T32, T39, T38)) → U3_gaaa(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
p7_in_aaaa(0, T27, 0, 0) → p7_out_aaaa(0, T27, 0, 0)
p7_in_aaaa(s(T32), T34, X47, T35) → U1_aaaa(T32, T34, X47, T35, f23_in_aaa(T32, T34, X46))
U1_aaaa(T32, T34, X47, T35, f23_out_aaa(T32, T34, X46)) → p7_out_aaaa(s(T32), T34, X47, T35)
p7_in_aaaa(s(T32), T39, X47, T40) → U2_aaaa(T32, T39, X47, T40, f23_in_aaa(T32, T39, T38))
U2_aaaa(T32, T39, X47, T40, f23_out_aaa(T32, T39, T38)) → U3_aaaa(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
U3_aaaa(T32, T39, X47, T40, p7_out_aaaa(T38, T39, X47, T40)) → p7_out_aaaa(s(T32), T39, X47, T40)
U3_gaaa(T32, T39, X47, T40, p7_out_aaaa(T38, T39, X47, T40)) → p7_out_gaaa(s(T32), T39, X47, T40)
U7_gaa(T9, T12, T13, p7_out_gaaa(T9, T12, X13, T13)) → f1_out_gaa(s(T9), T12, T13)

The argument filtering Pi contains the following mapping:
f1_in_gaa(x1, x2, x3)  =  f1_in_gaa(x1)
0  =  0
f1_out_gaa(x1, x2, x3)  =  f1_out_gaa(x1)
s(x1)  =  s(x1)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x1, x4)
p7_in_gaaa(x1, x2, x3, x4)  =  p7_in_gaaa(x1)
p7_out_gaaa(x1, x2, x3, x4)  =  p7_out_gaaa(x1)
U1_gaaa(x1, x2, x3, x4, x5)  =  U1_gaaa(x1, x5)
f23_in_gaa(x1, x2, x3)  =  f23_in_gaa(x1)
f23_out_gaa(x1, x2, x3)  =  f23_out_gaa(x1)
U4_gaa(x1, x2, x3, x4)  =  U4_gaa(x1, x4)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x1, x4)
f23_in_aaa(x1, x2, x3)  =  f23_in_aaa
f23_out_aaa(x1, x2, x3)  =  f23_out_aaa(x1)
U4_aaa(x1, x2, x3, x4)  =  U4_aaa(x4)
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
U6_aaa(x1, x2, x3, x4)  =  U6_aaa(x1, x4)
U2_gaaa(x1, x2, x3, x4, x5)  =  U2_gaaa(x1, x5)
U3_gaaa(x1, x2, x3, x4, x5)  =  U3_gaaa(x1, x5)
p7_in_aaaa(x1, x2, x3, x4)  =  p7_in_aaaa
p7_out_aaaa(x1, x2, x3, x4)  =  p7_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5)  =  U1_aaaa(x5)
U2_aaaa(x1, x2, x3, x4, x5)  =  U2_aaaa(x5)
U3_aaaa(x1, x2, x3, x4, x5)  =  U3_aaaa(x1, x5)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(35) Obligation:

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

f1_in_gaa(0, T5, 0) → f1_out_gaa(0, T5, 0)
f1_in_gaa(s(T9), T12, T13) → U7_gaa(T9, T12, T13, p7_in_gaaa(T9, T12, X13, T13))
p7_in_gaaa(0, T27, 0, 0) → p7_out_gaaa(0, T27, 0, 0)
p7_in_gaaa(s(T32), T34, X47, T35) → U1_gaaa(T32, T34, X47, T35, f23_in_gaa(T32, T34, X46))
f23_in_gaa(0, T47, 0) → f23_out_gaa(0, T47, 0)
f23_in_gaa(s(T52), T54, X74) → U4_gaa(T52, T54, X74, f23_in_gaa(T52, T54, X73))
f23_in_gaa(s(T52), T58, X74) → U5_gaa(T52, T58, X74, f23_in_gaa(T52, T58, T57))
U5_gaa(T52, T58, X74, f23_out_gaa(T52, T58, T57)) → U6_gaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
f23_in_aaa(0, T47, 0) → f23_out_aaa(0, T47, 0)
f23_in_aaa(s(T52), T54, X74) → U4_aaa(T52, T54, X74, f23_in_aaa(T52, T54, X73))
f23_in_aaa(s(T52), T58, X74) → U5_aaa(T52, T58, X74, f23_in_aaa(T52, T58, T57))
U5_aaa(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → U6_aaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
U6_aaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_aaa(s(T52), T58, X74)
U4_aaa(T52, T54, X74, f23_out_aaa(T52, T54, X73)) → f23_out_aaa(s(T52), T54, X74)
U6_gaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_gaa(s(T52), T58, X74)
U4_gaa(T52, T54, X74, f23_out_gaa(T52, T54, X73)) → f23_out_gaa(s(T52), T54, X74)
U1_gaaa(T32, T34, X47, T35, f23_out_gaa(T32, T34, X46)) → p7_out_gaaa(s(T32), T34, X47, T35)
p7_in_gaaa(s(T32), T39, X47, T40) → U2_gaaa(T32, T39, X47, T40, f23_in_gaa(T32, T39, T38))
U2_gaaa(T32, T39, X47, T40, f23_out_gaa(T32, T39, T38)) → U3_gaaa(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
p7_in_aaaa(0, T27, 0, 0) → p7_out_aaaa(0, T27, 0, 0)
p7_in_aaaa(s(T32), T34, X47, T35) → U1_aaaa(T32, T34, X47, T35, f23_in_aaa(T32, T34, X46))
U1_aaaa(T32, T34, X47, T35, f23_out_aaa(T32, T34, X46)) → p7_out_aaaa(s(T32), T34, X47, T35)
p7_in_aaaa(s(T32), T39, X47, T40) → U2_aaaa(T32, T39, X47, T40, f23_in_aaa(T32, T39, T38))
U2_aaaa(T32, T39, X47, T40, f23_out_aaa(T32, T39, T38)) → U3_aaaa(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
U3_aaaa(T32, T39, X47, T40, p7_out_aaaa(T38, T39, X47, T40)) → p7_out_aaaa(s(T32), T39, X47, T40)
U3_gaaa(T32, T39, X47, T40, p7_out_aaaa(T38, T39, X47, T40)) → p7_out_gaaa(s(T32), T39, X47, T40)
U7_gaa(T9, T12, T13, p7_out_gaaa(T9, T12, X13, T13)) → f1_out_gaa(s(T9), T12, T13)

The argument filtering Pi contains the following mapping:
f1_in_gaa(x1, x2, x3)  =  f1_in_gaa(x1)
0  =  0
f1_out_gaa(x1, x2, x3)  =  f1_out_gaa(x1)
s(x1)  =  s(x1)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x1, x4)
p7_in_gaaa(x1, x2, x3, x4)  =  p7_in_gaaa(x1)
p7_out_gaaa(x1, x2, x3, x4)  =  p7_out_gaaa(x1)
U1_gaaa(x1, x2, x3, x4, x5)  =  U1_gaaa(x1, x5)
f23_in_gaa(x1, x2, x3)  =  f23_in_gaa(x1)
f23_out_gaa(x1, x2, x3)  =  f23_out_gaa(x1)
U4_gaa(x1, x2, x3, x4)  =  U4_gaa(x1, x4)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x1, x4)
f23_in_aaa(x1, x2, x3)  =  f23_in_aaa
f23_out_aaa(x1, x2, x3)  =  f23_out_aaa(x1)
U4_aaa(x1, x2, x3, x4)  =  U4_aaa(x4)
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
U6_aaa(x1, x2, x3, x4)  =  U6_aaa(x1, x4)
U2_gaaa(x1, x2, x3, x4, x5)  =  U2_gaaa(x1, x5)
U3_gaaa(x1, x2, x3, x4, x5)  =  U3_gaaa(x1, x5)
p7_in_aaaa(x1, x2, x3, x4)  =  p7_in_aaaa
p7_out_aaaa(x1, x2, x3, x4)  =  p7_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5)  =  U1_aaaa(x5)
U2_aaaa(x1, x2, x3, x4, x5)  =  U2_aaaa(x5)
U3_aaaa(x1, x2, x3, x4, x5)  =  U3_aaaa(x1, x5)

(36) 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:

F1_IN_GAA(s(T9), T12, T13) → U7_GAA(T9, T12, T13, p7_in_gaaa(T9, T12, X13, T13))
F1_IN_GAA(s(T9), T12, T13) → P7_IN_GAAA(T9, T12, X13, T13)
P7_IN_GAAA(s(T32), T34, X47, T35) → U1_GAAA(T32, T34, X47, T35, f23_in_gaa(T32, T34, X46))
P7_IN_GAAA(s(T32), T34, X47, T35) → F23_IN_GAA(T32, T34, X46)
F23_IN_GAA(s(T52), T54, X74) → U4_GAA(T52, T54, X74, f23_in_gaa(T52, T54, X73))
F23_IN_GAA(s(T52), T54, X74) → F23_IN_GAA(T52, T54, X73)
F23_IN_GAA(s(T52), T58, X74) → U5_GAA(T52, T58, X74, f23_in_gaa(T52, T58, T57))
U5_GAA(T52, T58, X74, f23_out_gaa(T52, T58, T57)) → U6_GAA(T52, T58, X74, f23_in_aaa(T57, T58, X74))
U5_GAA(T52, T58, X74, f23_out_gaa(T52, T58, T57)) → F23_IN_AAA(T57, T58, X74)
F23_IN_AAA(s(T52), T54, X74) → U4_AAA(T52, T54, X74, f23_in_aaa(T52, T54, X73))
F23_IN_AAA(s(T52), T54, X74) → F23_IN_AAA(T52, T54, X73)
F23_IN_AAA(s(T52), T58, X74) → U5_AAA(T52, T58, X74, f23_in_aaa(T52, T58, T57))
U5_AAA(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → U6_AAA(T52, T58, X74, f23_in_aaa(T57, T58, X74))
U5_AAA(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → F23_IN_AAA(T57, T58, X74)
P7_IN_GAAA(s(T32), T39, X47, T40) → U2_GAAA(T32, T39, X47, T40, f23_in_gaa(T32, T39, T38))
U2_GAAA(T32, T39, X47, T40, f23_out_gaa(T32, T39, T38)) → U3_GAAA(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
U2_GAAA(T32, T39, X47, T40, f23_out_gaa(T32, T39, T38)) → P7_IN_AAAA(T38, T39, X47, T40)
P7_IN_AAAA(s(T32), T34, X47, T35) → U1_AAAA(T32, T34, X47, T35, f23_in_aaa(T32, T34, X46))
P7_IN_AAAA(s(T32), T34, X47, T35) → F23_IN_AAA(T32, T34, X46)
P7_IN_AAAA(s(T32), T39, X47, T40) → U2_AAAA(T32, T39, X47, T40, f23_in_aaa(T32, T39, T38))
U2_AAAA(T32, T39, X47, T40, f23_out_aaa(T32, T39, T38)) → U3_AAAA(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
U2_AAAA(T32, T39, X47, T40, f23_out_aaa(T32, T39, T38)) → P7_IN_AAAA(T38, T39, X47, T40)

The TRS R consists of the following rules:

f1_in_gaa(0, T5, 0) → f1_out_gaa(0, T5, 0)
f1_in_gaa(s(T9), T12, T13) → U7_gaa(T9, T12, T13, p7_in_gaaa(T9, T12, X13, T13))
p7_in_gaaa(0, T27, 0, 0) → p7_out_gaaa(0, T27, 0, 0)
p7_in_gaaa(s(T32), T34, X47, T35) → U1_gaaa(T32, T34, X47, T35, f23_in_gaa(T32, T34, X46))
f23_in_gaa(0, T47, 0) → f23_out_gaa(0, T47, 0)
f23_in_gaa(s(T52), T54, X74) → U4_gaa(T52, T54, X74, f23_in_gaa(T52, T54, X73))
f23_in_gaa(s(T52), T58, X74) → U5_gaa(T52, T58, X74, f23_in_gaa(T52, T58, T57))
U5_gaa(T52, T58, X74, f23_out_gaa(T52, T58, T57)) → U6_gaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
f23_in_aaa(0, T47, 0) → f23_out_aaa(0, T47, 0)
f23_in_aaa(s(T52), T54, X74) → U4_aaa(T52, T54, X74, f23_in_aaa(T52, T54, X73))
f23_in_aaa(s(T52), T58, X74) → U5_aaa(T52, T58, X74, f23_in_aaa(T52, T58, T57))
U5_aaa(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → U6_aaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
U6_aaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_aaa(s(T52), T58, X74)
U4_aaa(T52, T54, X74, f23_out_aaa(T52, T54, X73)) → f23_out_aaa(s(T52), T54, X74)
U6_gaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_gaa(s(T52), T58, X74)
U4_gaa(T52, T54, X74, f23_out_gaa(T52, T54, X73)) → f23_out_gaa(s(T52), T54, X74)
U1_gaaa(T32, T34, X47, T35, f23_out_gaa(T32, T34, X46)) → p7_out_gaaa(s(T32), T34, X47, T35)
p7_in_gaaa(s(T32), T39, X47, T40) → U2_gaaa(T32, T39, X47, T40, f23_in_gaa(T32, T39, T38))
U2_gaaa(T32, T39, X47, T40, f23_out_gaa(T32, T39, T38)) → U3_gaaa(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
p7_in_aaaa(0, T27, 0, 0) → p7_out_aaaa(0, T27, 0, 0)
p7_in_aaaa(s(T32), T34, X47, T35) → U1_aaaa(T32, T34, X47, T35, f23_in_aaa(T32, T34, X46))
U1_aaaa(T32, T34, X47, T35, f23_out_aaa(T32, T34, X46)) → p7_out_aaaa(s(T32), T34, X47, T35)
p7_in_aaaa(s(T32), T39, X47, T40) → U2_aaaa(T32, T39, X47, T40, f23_in_aaa(T32, T39, T38))
U2_aaaa(T32, T39, X47, T40, f23_out_aaa(T32, T39, T38)) → U3_aaaa(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
U3_aaaa(T32, T39, X47, T40, p7_out_aaaa(T38, T39, X47, T40)) → p7_out_aaaa(s(T32), T39, X47, T40)
U3_gaaa(T32, T39, X47, T40, p7_out_aaaa(T38, T39, X47, T40)) → p7_out_gaaa(s(T32), T39, X47, T40)
U7_gaa(T9, T12, T13, p7_out_gaaa(T9, T12, X13, T13)) → f1_out_gaa(s(T9), T12, T13)

The argument filtering Pi contains the following mapping:
f1_in_gaa(x1, x2, x3)  =  f1_in_gaa(x1)
0  =  0
f1_out_gaa(x1, x2, x3)  =  f1_out_gaa(x1)
s(x1)  =  s(x1)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x1, x4)
p7_in_gaaa(x1, x2, x3, x4)  =  p7_in_gaaa(x1)
p7_out_gaaa(x1, x2, x3, x4)  =  p7_out_gaaa(x1)
U1_gaaa(x1, x2, x3, x4, x5)  =  U1_gaaa(x1, x5)
f23_in_gaa(x1, x2, x3)  =  f23_in_gaa(x1)
f23_out_gaa(x1, x2, x3)  =  f23_out_gaa(x1)
U4_gaa(x1, x2, x3, x4)  =  U4_gaa(x1, x4)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x1, x4)
f23_in_aaa(x1, x2, x3)  =  f23_in_aaa
f23_out_aaa(x1, x2, x3)  =  f23_out_aaa(x1)
U4_aaa(x1, x2, x3, x4)  =  U4_aaa(x4)
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
U6_aaa(x1, x2, x3, x4)  =  U6_aaa(x1, x4)
U2_gaaa(x1, x2, x3, x4, x5)  =  U2_gaaa(x1, x5)
U3_gaaa(x1, x2, x3, x4, x5)  =  U3_gaaa(x1, x5)
p7_in_aaaa(x1, x2, x3, x4)  =  p7_in_aaaa
p7_out_aaaa(x1, x2, x3, x4)  =  p7_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5)  =  U1_aaaa(x5)
U2_aaaa(x1, x2, x3, x4, x5)  =  U2_aaaa(x5)
U3_aaaa(x1, x2, x3, x4, x5)  =  U3_aaaa(x1, x5)
F1_IN_GAA(x1, x2, x3)  =  F1_IN_GAA(x1)
U7_GAA(x1, x2, x3, x4)  =  U7_GAA(x1, x4)
P7_IN_GAAA(x1, x2, x3, x4)  =  P7_IN_GAAA(x1)
U1_GAAA(x1, x2, x3, x4, x5)  =  U1_GAAA(x1, x5)
F23_IN_GAA(x1, x2, x3)  =  F23_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4)  =  U4_GAA(x1, x4)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x4)
U6_GAA(x1, x2, x3, x4)  =  U6_GAA(x1, x4)
F23_IN_AAA(x1, x2, x3)  =  F23_IN_AAA
U4_AAA(x1, x2, x3, x4)  =  U4_AAA(x4)
U5_AAA(x1, x2, x3, x4)  =  U5_AAA(x4)
U6_AAA(x1, x2, x3, x4)  =  U6_AAA(x1, x4)
U2_GAAA(x1, x2, x3, x4, x5)  =  U2_GAAA(x1, x5)
U3_GAAA(x1, x2, x3, x4, x5)  =  U3_GAAA(x1, x5)
P7_IN_AAAA(x1, x2, x3, x4)  =  P7_IN_AAAA
U1_AAAA(x1, x2, x3, x4, x5)  =  U1_AAAA(x5)
U2_AAAA(x1, x2, x3, x4, x5)  =  U2_AAAA(x5)
U3_AAAA(x1, x2, x3, x4, x5)  =  U3_AAAA(x1, x5)

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

(37) Obligation:

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

F1_IN_GAA(s(T9), T12, T13) → U7_GAA(T9, T12, T13, p7_in_gaaa(T9, T12, X13, T13))
F1_IN_GAA(s(T9), T12, T13) → P7_IN_GAAA(T9, T12, X13, T13)
P7_IN_GAAA(s(T32), T34, X47, T35) → U1_GAAA(T32, T34, X47, T35, f23_in_gaa(T32, T34, X46))
P7_IN_GAAA(s(T32), T34, X47, T35) → F23_IN_GAA(T32, T34, X46)
F23_IN_GAA(s(T52), T54, X74) → U4_GAA(T52, T54, X74, f23_in_gaa(T52, T54, X73))
F23_IN_GAA(s(T52), T54, X74) → F23_IN_GAA(T52, T54, X73)
F23_IN_GAA(s(T52), T58, X74) → U5_GAA(T52, T58, X74, f23_in_gaa(T52, T58, T57))
U5_GAA(T52, T58, X74, f23_out_gaa(T52, T58, T57)) → U6_GAA(T52, T58, X74, f23_in_aaa(T57, T58, X74))
U5_GAA(T52, T58, X74, f23_out_gaa(T52, T58, T57)) → F23_IN_AAA(T57, T58, X74)
F23_IN_AAA(s(T52), T54, X74) → U4_AAA(T52, T54, X74, f23_in_aaa(T52, T54, X73))
F23_IN_AAA(s(T52), T54, X74) → F23_IN_AAA(T52, T54, X73)
F23_IN_AAA(s(T52), T58, X74) → U5_AAA(T52, T58, X74, f23_in_aaa(T52, T58, T57))
U5_AAA(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → U6_AAA(T52, T58, X74, f23_in_aaa(T57, T58, X74))
U5_AAA(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → F23_IN_AAA(T57, T58, X74)
P7_IN_GAAA(s(T32), T39, X47, T40) → U2_GAAA(T32, T39, X47, T40, f23_in_gaa(T32, T39, T38))
U2_GAAA(T32, T39, X47, T40, f23_out_gaa(T32, T39, T38)) → U3_GAAA(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
U2_GAAA(T32, T39, X47, T40, f23_out_gaa(T32, T39, T38)) → P7_IN_AAAA(T38, T39, X47, T40)
P7_IN_AAAA(s(T32), T34, X47, T35) → U1_AAAA(T32, T34, X47, T35, f23_in_aaa(T32, T34, X46))
P7_IN_AAAA(s(T32), T34, X47, T35) → F23_IN_AAA(T32, T34, X46)
P7_IN_AAAA(s(T32), T39, X47, T40) → U2_AAAA(T32, T39, X47, T40, f23_in_aaa(T32, T39, T38))
U2_AAAA(T32, T39, X47, T40, f23_out_aaa(T32, T39, T38)) → U3_AAAA(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
U2_AAAA(T32, T39, X47, T40, f23_out_aaa(T32, T39, T38)) → P7_IN_AAAA(T38, T39, X47, T40)

The TRS R consists of the following rules:

f1_in_gaa(0, T5, 0) → f1_out_gaa(0, T5, 0)
f1_in_gaa(s(T9), T12, T13) → U7_gaa(T9, T12, T13, p7_in_gaaa(T9, T12, X13, T13))
p7_in_gaaa(0, T27, 0, 0) → p7_out_gaaa(0, T27, 0, 0)
p7_in_gaaa(s(T32), T34, X47, T35) → U1_gaaa(T32, T34, X47, T35, f23_in_gaa(T32, T34, X46))
f23_in_gaa(0, T47, 0) → f23_out_gaa(0, T47, 0)
f23_in_gaa(s(T52), T54, X74) → U4_gaa(T52, T54, X74, f23_in_gaa(T52, T54, X73))
f23_in_gaa(s(T52), T58, X74) → U5_gaa(T52, T58, X74, f23_in_gaa(T52, T58, T57))
U5_gaa(T52, T58, X74, f23_out_gaa(T52, T58, T57)) → U6_gaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
f23_in_aaa(0, T47, 0) → f23_out_aaa(0, T47, 0)
f23_in_aaa(s(T52), T54, X74) → U4_aaa(T52, T54, X74, f23_in_aaa(T52, T54, X73))
f23_in_aaa(s(T52), T58, X74) → U5_aaa(T52, T58, X74, f23_in_aaa(T52, T58, T57))
U5_aaa(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → U6_aaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
U6_aaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_aaa(s(T52), T58, X74)
U4_aaa(T52, T54, X74, f23_out_aaa(T52, T54, X73)) → f23_out_aaa(s(T52), T54, X74)
U6_gaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_gaa(s(T52), T58, X74)
U4_gaa(T52, T54, X74, f23_out_gaa(T52, T54, X73)) → f23_out_gaa(s(T52), T54, X74)
U1_gaaa(T32, T34, X47, T35, f23_out_gaa(T32, T34, X46)) → p7_out_gaaa(s(T32), T34, X47, T35)
p7_in_gaaa(s(T32), T39, X47, T40) → U2_gaaa(T32, T39, X47, T40, f23_in_gaa(T32, T39, T38))
U2_gaaa(T32, T39, X47, T40, f23_out_gaa(T32, T39, T38)) → U3_gaaa(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
p7_in_aaaa(0, T27, 0, 0) → p7_out_aaaa(0, T27, 0, 0)
p7_in_aaaa(s(T32), T34, X47, T35) → U1_aaaa(T32, T34, X47, T35, f23_in_aaa(T32, T34, X46))
U1_aaaa(T32, T34, X47, T35, f23_out_aaa(T32, T34, X46)) → p7_out_aaaa(s(T32), T34, X47, T35)
p7_in_aaaa(s(T32), T39, X47, T40) → U2_aaaa(T32, T39, X47, T40, f23_in_aaa(T32, T39, T38))
U2_aaaa(T32, T39, X47, T40, f23_out_aaa(T32, T39, T38)) → U3_aaaa(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
U3_aaaa(T32, T39, X47, T40, p7_out_aaaa(T38, T39, X47, T40)) → p7_out_aaaa(s(T32), T39, X47, T40)
U3_gaaa(T32, T39, X47, T40, p7_out_aaaa(T38, T39, X47, T40)) → p7_out_gaaa(s(T32), T39, X47, T40)
U7_gaa(T9, T12, T13, p7_out_gaaa(T9, T12, X13, T13)) → f1_out_gaa(s(T9), T12, T13)

The argument filtering Pi contains the following mapping:
f1_in_gaa(x1, x2, x3)  =  f1_in_gaa(x1)
0  =  0
f1_out_gaa(x1, x2, x3)  =  f1_out_gaa(x1)
s(x1)  =  s(x1)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x1, x4)
p7_in_gaaa(x1, x2, x3, x4)  =  p7_in_gaaa(x1)
p7_out_gaaa(x1, x2, x3, x4)  =  p7_out_gaaa(x1)
U1_gaaa(x1, x2, x3, x4, x5)  =  U1_gaaa(x1, x5)
f23_in_gaa(x1, x2, x3)  =  f23_in_gaa(x1)
f23_out_gaa(x1, x2, x3)  =  f23_out_gaa(x1)
U4_gaa(x1, x2, x3, x4)  =  U4_gaa(x1, x4)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x1, x4)
f23_in_aaa(x1, x2, x3)  =  f23_in_aaa
f23_out_aaa(x1, x2, x3)  =  f23_out_aaa(x1)
U4_aaa(x1, x2, x3, x4)  =  U4_aaa(x4)
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
U6_aaa(x1, x2, x3, x4)  =  U6_aaa(x1, x4)
U2_gaaa(x1, x2, x3, x4, x5)  =  U2_gaaa(x1, x5)
U3_gaaa(x1, x2, x3, x4, x5)  =  U3_gaaa(x1, x5)
p7_in_aaaa(x1, x2, x3, x4)  =  p7_in_aaaa
p7_out_aaaa(x1, x2, x3, x4)  =  p7_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5)  =  U1_aaaa(x5)
U2_aaaa(x1, x2, x3, x4, x5)  =  U2_aaaa(x5)
U3_aaaa(x1, x2, x3, x4, x5)  =  U3_aaaa(x1, x5)
F1_IN_GAA(x1, x2, x3)  =  F1_IN_GAA(x1)
U7_GAA(x1, x2, x3, x4)  =  U7_GAA(x1, x4)
P7_IN_GAAA(x1, x2, x3, x4)  =  P7_IN_GAAA(x1)
U1_GAAA(x1, x2, x3, x4, x5)  =  U1_GAAA(x1, x5)
F23_IN_GAA(x1, x2, x3)  =  F23_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4)  =  U4_GAA(x1, x4)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x4)
U6_GAA(x1, x2, x3, x4)  =  U6_GAA(x1, x4)
F23_IN_AAA(x1, x2, x3)  =  F23_IN_AAA
U4_AAA(x1, x2, x3, x4)  =  U4_AAA(x4)
U5_AAA(x1, x2, x3, x4)  =  U5_AAA(x4)
U6_AAA(x1, x2, x3, x4)  =  U6_AAA(x1, x4)
U2_GAAA(x1, x2, x3, x4, x5)  =  U2_GAAA(x1, x5)
U3_GAAA(x1, x2, x3, x4, x5)  =  U3_GAAA(x1, x5)
P7_IN_AAAA(x1, x2, x3, x4)  =  P7_IN_AAAA
U1_AAAA(x1, x2, x3, x4, x5)  =  U1_AAAA(x5)
U2_AAAA(x1, x2, x3, x4, x5)  =  U2_AAAA(x5)
U3_AAAA(x1, x2, x3, x4, x5)  =  U3_AAAA(x1, x5)

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

(38) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 16 less nodes.

(39) Complex Obligation (AND)

(40) Obligation:

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

F23_IN_AAA(s(T52), T58, X74) → U5_AAA(T52, T58, X74, f23_in_aaa(T52, T58, T57))
U5_AAA(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → F23_IN_AAA(T57, T58, X74)
F23_IN_AAA(s(T52), T54, X74) → F23_IN_AAA(T52, T54, X73)

The TRS R consists of the following rules:

f1_in_gaa(0, T5, 0) → f1_out_gaa(0, T5, 0)
f1_in_gaa(s(T9), T12, T13) → U7_gaa(T9, T12, T13, p7_in_gaaa(T9, T12, X13, T13))
p7_in_gaaa(0, T27, 0, 0) → p7_out_gaaa(0, T27, 0, 0)
p7_in_gaaa(s(T32), T34, X47, T35) → U1_gaaa(T32, T34, X47, T35, f23_in_gaa(T32, T34, X46))
f23_in_gaa(0, T47, 0) → f23_out_gaa(0, T47, 0)
f23_in_gaa(s(T52), T54, X74) → U4_gaa(T52, T54, X74, f23_in_gaa(T52, T54, X73))
f23_in_gaa(s(T52), T58, X74) → U5_gaa(T52, T58, X74, f23_in_gaa(T52, T58, T57))
U5_gaa(T52, T58, X74, f23_out_gaa(T52, T58, T57)) → U6_gaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
f23_in_aaa(0, T47, 0) → f23_out_aaa(0, T47, 0)
f23_in_aaa(s(T52), T54, X74) → U4_aaa(T52, T54, X74, f23_in_aaa(T52, T54, X73))
f23_in_aaa(s(T52), T58, X74) → U5_aaa(T52, T58, X74, f23_in_aaa(T52, T58, T57))
U5_aaa(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → U6_aaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
U6_aaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_aaa(s(T52), T58, X74)
U4_aaa(T52, T54, X74, f23_out_aaa(T52, T54, X73)) → f23_out_aaa(s(T52), T54, X74)
U6_gaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_gaa(s(T52), T58, X74)
U4_gaa(T52, T54, X74, f23_out_gaa(T52, T54, X73)) → f23_out_gaa(s(T52), T54, X74)
U1_gaaa(T32, T34, X47, T35, f23_out_gaa(T32, T34, X46)) → p7_out_gaaa(s(T32), T34, X47, T35)
p7_in_gaaa(s(T32), T39, X47, T40) → U2_gaaa(T32, T39, X47, T40, f23_in_gaa(T32, T39, T38))
U2_gaaa(T32, T39, X47, T40, f23_out_gaa(T32, T39, T38)) → U3_gaaa(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
p7_in_aaaa(0, T27, 0, 0) → p7_out_aaaa(0, T27, 0, 0)
p7_in_aaaa(s(T32), T34, X47, T35) → U1_aaaa(T32, T34, X47, T35, f23_in_aaa(T32, T34, X46))
U1_aaaa(T32, T34, X47, T35, f23_out_aaa(T32, T34, X46)) → p7_out_aaaa(s(T32), T34, X47, T35)
p7_in_aaaa(s(T32), T39, X47, T40) → U2_aaaa(T32, T39, X47, T40, f23_in_aaa(T32, T39, T38))
U2_aaaa(T32, T39, X47, T40, f23_out_aaa(T32, T39, T38)) → U3_aaaa(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
U3_aaaa(T32, T39, X47, T40, p7_out_aaaa(T38, T39, X47, T40)) → p7_out_aaaa(s(T32), T39, X47, T40)
U3_gaaa(T32, T39, X47, T40, p7_out_aaaa(T38, T39, X47, T40)) → p7_out_gaaa(s(T32), T39, X47, T40)
U7_gaa(T9, T12, T13, p7_out_gaaa(T9, T12, X13, T13)) → f1_out_gaa(s(T9), T12, T13)

The argument filtering Pi contains the following mapping:
f1_in_gaa(x1, x2, x3)  =  f1_in_gaa(x1)
0  =  0
f1_out_gaa(x1, x2, x3)  =  f1_out_gaa(x1)
s(x1)  =  s(x1)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x1, x4)
p7_in_gaaa(x1, x2, x3, x4)  =  p7_in_gaaa(x1)
p7_out_gaaa(x1, x2, x3, x4)  =  p7_out_gaaa(x1)
U1_gaaa(x1, x2, x3, x4, x5)  =  U1_gaaa(x1, x5)
f23_in_gaa(x1, x2, x3)  =  f23_in_gaa(x1)
f23_out_gaa(x1, x2, x3)  =  f23_out_gaa(x1)
U4_gaa(x1, x2, x3, x4)  =  U4_gaa(x1, x4)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x1, x4)
f23_in_aaa(x1, x2, x3)  =  f23_in_aaa
f23_out_aaa(x1, x2, x3)  =  f23_out_aaa(x1)
U4_aaa(x1, x2, x3, x4)  =  U4_aaa(x4)
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
U6_aaa(x1, x2, x3, x4)  =  U6_aaa(x1, x4)
U2_gaaa(x1, x2, x3, x4, x5)  =  U2_gaaa(x1, x5)
U3_gaaa(x1, x2, x3, x4, x5)  =  U3_gaaa(x1, x5)
p7_in_aaaa(x1, x2, x3, x4)  =  p7_in_aaaa
p7_out_aaaa(x1, x2, x3, x4)  =  p7_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5)  =  U1_aaaa(x5)
U2_aaaa(x1, x2, x3, x4, x5)  =  U2_aaaa(x5)
U3_aaaa(x1, x2, x3, x4, x5)  =  U3_aaaa(x1, x5)
F23_IN_AAA(x1, x2, x3)  =  F23_IN_AAA
U5_AAA(x1, x2, x3, x4)  =  U5_AAA(x4)

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

(41) UsableRulesProof (EQUIVALENT transformation)

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

(42) Obligation:

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

F23_IN_AAA(s(T52), T58, X74) → U5_AAA(T52, T58, X74, f23_in_aaa(T52, T58, T57))
U5_AAA(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → F23_IN_AAA(T57, T58, X74)
F23_IN_AAA(s(T52), T54, X74) → F23_IN_AAA(T52, T54, X73)

The TRS R consists of the following rules:

f23_in_aaa(0, T47, 0) → f23_out_aaa(0, T47, 0)
f23_in_aaa(s(T52), T54, X74) → U4_aaa(T52, T54, X74, f23_in_aaa(T52, T54, X73))
f23_in_aaa(s(T52), T58, X74) → U5_aaa(T52, T58, X74, f23_in_aaa(T52, T58, T57))
U4_aaa(T52, T54, X74, f23_out_aaa(T52, T54, X73)) → f23_out_aaa(s(T52), T54, X74)
U5_aaa(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → U6_aaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
U6_aaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_aaa(s(T52), T58, X74)

The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
f23_in_aaa(x1, x2, x3)  =  f23_in_aaa
f23_out_aaa(x1, x2, x3)  =  f23_out_aaa(x1)
U4_aaa(x1, x2, x3, x4)  =  U4_aaa(x4)
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
U6_aaa(x1, x2, x3, x4)  =  U6_aaa(x1, x4)
F23_IN_AAA(x1, x2, x3)  =  F23_IN_AAA
U5_AAA(x1, x2, x3, x4)  =  U5_AAA(x4)

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

(43) PiDPToQDPProof (SOUND transformation)

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

(44) Obligation:

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

F23_IN_AAA → U5_AAA(f23_in_aaa)
U5_AAA(f23_out_aaa(T52)) → F23_IN_AAA
F23_IN_AAA → F23_IN_AAA

The TRS R consists of the following rules:

f23_in_aaa → f23_out_aaa(0)
f23_in_aaa → U4_aaa(f23_in_aaa)
f23_in_aaa → U5_aaa(f23_in_aaa)
U4_aaa(f23_out_aaa(T52)) → f23_out_aaa(s(T52))
U5_aaa(f23_out_aaa(T52)) → U6_aaa(T52, f23_in_aaa)
U6_aaa(T52, f23_out_aaa(T57)) → f23_out_aaa(s(T52))

The set Q consists of the following terms:

f23_in_aaa
U4_aaa(x0)
U5_aaa(x0)
U6_aaa(x0, x1)

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

(45) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule F23_IN_AAA → U5_AAA(f23_in_aaa) at position [0] we obtained the following new rules [LPAR04]:

F23_IN_AAA → U5_AAA(f23_out_aaa(0))
F23_IN_AAA → U5_AAA(U4_aaa(f23_in_aaa))
F23_IN_AAA → U5_AAA(U5_aaa(f23_in_aaa))

(46) Obligation:

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

U5_AAA(f23_out_aaa(T52)) → F23_IN_AAA
F23_IN_AAA → F23_IN_AAA
F23_IN_AAA → U5_AAA(f23_out_aaa(0))
F23_IN_AAA → U5_AAA(U4_aaa(f23_in_aaa))
F23_IN_AAA → U5_AAA(U5_aaa(f23_in_aaa))

The TRS R consists of the following rules:

f23_in_aaa → f23_out_aaa(0)
f23_in_aaa → U4_aaa(f23_in_aaa)
f23_in_aaa → U5_aaa(f23_in_aaa)
U4_aaa(f23_out_aaa(T52)) → f23_out_aaa(s(T52))
U5_aaa(f23_out_aaa(T52)) → U6_aaa(T52, f23_in_aaa)
U6_aaa(T52, f23_out_aaa(T57)) → f23_out_aaa(s(T52))

The set Q consists of the following terms:

f23_in_aaa
U4_aaa(x0)
U5_aaa(x0)
U6_aaa(x0, x1)

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

(47) 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 = F23_IN_AAA evaluates to t =F23_IN_AAA

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 F23_IN_AAA to F23_IN_AAA.



(48) NO

(49) Obligation:

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

P7_IN_AAAA(s(T32), T39, X47, T40) → U2_AAAA(T32, T39, X47, T40, f23_in_aaa(T32, T39, T38))
U2_AAAA(T32, T39, X47, T40, f23_out_aaa(T32, T39, T38)) → P7_IN_AAAA(T38, T39, X47, T40)

The TRS R consists of the following rules:

f1_in_gaa(0, T5, 0) → f1_out_gaa(0, T5, 0)
f1_in_gaa(s(T9), T12, T13) → U7_gaa(T9, T12, T13, p7_in_gaaa(T9, T12, X13, T13))
p7_in_gaaa(0, T27, 0, 0) → p7_out_gaaa(0, T27, 0, 0)
p7_in_gaaa(s(T32), T34, X47, T35) → U1_gaaa(T32, T34, X47, T35, f23_in_gaa(T32, T34, X46))
f23_in_gaa(0, T47, 0) → f23_out_gaa(0, T47, 0)
f23_in_gaa(s(T52), T54, X74) → U4_gaa(T52, T54, X74, f23_in_gaa(T52, T54, X73))
f23_in_gaa(s(T52), T58, X74) → U5_gaa(T52, T58, X74, f23_in_gaa(T52, T58, T57))
U5_gaa(T52, T58, X74, f23_out_gaa(T52, T58, T57)) → U6_gaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
f23_in_aaa(0, T47, 0) → f23_out_aaa(0, T47, 0)
f23_in_aaa(s(T52), T54, X74) → U4_aaa(T52, T54, X74, f23_in_aaa(T52, T54, X73))
f23_in_aaa(s(T52), T58, X74) → U5_aaa(T52, T58, X74, f23_in_aaa(T52, T58, T57))
U5_aaa(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → U6_aaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
U6_aaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_aaa(s(T52), T58, X74)
U4_aaa(T52, T54, X74, f23_out_aaa(T52, T54, X73)) → f23_out_aaa(s(T52), T54, X74)
U6_gaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_gaa(s(T52), T58, X74)
U4_gaa(T52, T54, X74, f23_out_gaa(T52, T54, X73)) → f23_out_gaa(s(T52), T54, X74)
U1_gaaa(T32, T34, X47, T35, f23_out_gaa(T32, T34, X46)) → p7_out_gaaa(s(T32), T34, X47, T35)
p7_in_gaaa(s(T32), T39, X47, T40) → U2_gaaa(T32, T39, X47, T40, f23_in_gaa(T32, T39, T38))
U2_gaaa(T32, T39, X47, T40, f23_out_gaa(T32, T39, T38)) → U3_gaaa(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
p7_in_aaaa(0, T27, 0, 0) → p7_out_aaaa(0, T27, 0, 0)
p7_in_aaaa(s(T32), T34, X47, T35) → U1_aaaa(T32, T34, X47, T35, f23_in_aaa(T32, T34, X46))
U1_aaaa(T32, T34, X47, T35, f23_out_aaa(T32, T34, X46)) → p7_out_aaaa(s(T32), T34, X47, T35)
p7_in_aaaa(s(T32), T39, X47, T40) → U2_aaaa(T32, T39, X47, T40, f23_in_aaa(T32, T39, T38))
U2_aaaa(T32, T39, X47, T40, f23_out_aaa(T32, T39, T38)) → U3_aaaa(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
U3_aaaa(T32, T39, X47, T40, p7_out_aaaa(T38, T39, X47, T40)) → p7_out_aaaa(s(T32), T39, X47, T40)
U3_gaaa(T32, T39, X47, T40, p7_out_aaaa(T38, T39, X47, T40)) → p7_out_gaaa(s(T32), T39, X47, T40)
U7_gaa(T9, T12, T13, p7_out_gaaa(T9, T12, X13, T13)) → f1_out_gaa(s(T9), T12, T13)

The argument filtering Pi contains the following mapping:
f1_in_gaa(x1, x2, x3)  =  f1_in_gaa(x1)
0  =  0
f1_out_gaa(x1, x2, x3)  =  f1_out_gaa(x1)
s(x1)  =  s(x1)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x1, x4)
p7_in_gaaa(x1, x2, x3, x4)  =  p7_in_gaaa(x1)
p7_out_gaaa(x1, x2, x3, x4)  =  p7_out_gaaa(x1)
U1_gaaa(x1, x2, x3, x4, x5)  =  U1_gaaa(x1, x5)
f23_in_gaa(x1, x2, x3)  =  f23_in_gaa(x1)
f23_out_gaa(x1, x2, x3)  =  f23_out_gaa(x1)
U4_gaa(x1, x2, x3, x4)  =  U4_gaa(x1, x4)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x1, x4)
f23_in_aaa(x1, x2, x3)  =  f23_in_aaa
f23_out_aaa(x1, x2, x3)  =  f23_out_aaa(x1)
U4_aaa(x1, x2, x3, x4)  =  U4_aaa(x4)
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
U6_aaa(x1, x2, x3, x4)  =  U6_aaa(x1, x4)
U2_gaaa(x1, x2, x3, x4, x5)  =  U2_gaaa(x1, x5)
U3_gaaa(x1, x2, x3, x4, x5)  =  U3_gaaa(x1, x5)
p7_in_aaaa(x1, x2, x3, x4)  =  p7_in_aaaa
p7_out_aaaa(x1, x2, x3, x4)  =  p7_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5)  =  U1_aaaa(x5)
U2_aaaa(x1, x2, x3, x4, x5)  =  U2_aaaa(x5)
U3_aaaa(x1, x2, x3, x4, x5)  =  U3_aaaa(x1, x5)
P7_IN_AAAA(x1, x2, x3, x4)  =  P7_IN_AAAA
U2_AAAA(x1, x2, x3, x4, x5)  =  U2_AAAA(x5)

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

(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:

P7_IN_AAAA(s(T32), T39, X47, T40) → U2_AAAA(T32, T39, X47, T40, f23_in_aaa(T32, T39, T38))
U2_AAAA(T32, T39, X47, T40, f23_out_aaa(T32, T39, T38)) → P7_IN_AAAA(T38, T39, X47, T40)

The TRS R consists of the following rules:

f23_in_aaa(0, T47, 0) → f23_out_aaa(0, T47, 0)
f23_in_aaa(s(T52), T54, X74) → U4_aaa(T52, T54, X74, f23_in_aaa(T52, T54, X73))
f23_in_aaa(s(T52), T58, X74) → U5_aaa(T52, T58, X74, f23_in_aaa(T52, T58, T57))
U4_aaa(T52, T54, X74, f23_out_aaa(T52, T54, X73)) → f23_out_aaa(s(T52), T54, X74)
U5_aaa(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → U6_aaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
U6_aaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_aaa(s(T52), T58, X74)

The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
f23_in_aaa(x1, x2, x3)  =  f23_in_aaa
f23_out_aaa(x1, x2, x3)  =  f23_out_aaa(x1)
U4_aaa(x1, x2, x3, x4)  =  U4_aaa(x4)
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
U6_aaa(x1, x2, x3, x4)  =  U6_aaa(x1, x4)
P7_IN_AAAA(x1, x2, x3, x4)  =  P7_IN_AAAA
U2_AAAA(x1, x2, x3, x4, x5)  =  U2_AAAA(x5)

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

(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:

P7_IN_AAAA → U2_AAAA(f23_in_aaa)
U2_AAAA(f23_out_aaa(T32)) → P7_IN_AAAA

The TRS R consists of the following rules:

f23_in_aaa → f23_out_aaa(0)
f23_in_aaa → U4_aaa(f23_in_aaa)
f23_in_aaa → U5_aaa(f23_in_aaa)
U4_aaa(f23_out_aaa(T52)) → f23_out_aaa(s(T52))
U5_aaa(f23_out_aaa(T52)) → U6_aaa(T52, f23_in_aaa)
U6_aaa(T52, f23_out_aaa(T57)) → f23_out_aaa(s(T52))

The set Q consists of the following terms:

f23_in_aaa
U4_aaa(x0)
U5_aaa(x0)
U6_aaa(x0, x1)

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

(54) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule P7_IN_AAAA → U2_AAAA(f23_in_aaa) at position [0] we obtained the following new rules [LPAR04]:

P7_IN_AAAA → U2_AAAA(f23_out_aaa(0))
P7_IN_AAAA → U2_AAAA(U4_aaa(f23_in_aaa))
P7_IN_AAAA → U2_AAAA(U5_aaa(f23_in_aaa))

(55) Obligation:

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

U2_AAAA(f23_out_aaa(T32)) → P7_IN_AAAA
P7_IN_AAAA → U2_AAAA(f23_out_aaa(0))
P7_IN_AAAA → U2_AAAA(U4_aaa(f23_in_aaa))
P7_IN_AAAA → U2_AAAA(U5_aaa(f23_in_aaa))

The TRS R consists of the following rules:

f23_in_aaa → f23_out_aaa(0)
f23_in_aaa → U4_aaa(f23_in_aaa)
f23_in_aaa → U5_aaa(f23_in_aaa)
U4_aaa(f23_out_aaa(T52)) → f23_out_aaa(s(T52))
U5_aaa(f23_out_aaa(T52)) → U6_aaa(T52, f23_in_aaa)
U6_aaa(T52, f23_out_aaa(T57)) → f23_out_aaa(s(T52))

The set Q consists of the following terms:

f23_in_aaa
U4_aaa(x0)
U5_aaa(x0)
U6_aaa(x0, x1)

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

(56) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = P7_IN_AAAA evaluates to t =P7_IN_AAAA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Semiunifier: [ ]
  • Matcher: [ ]



Rewriting sequence

P7_IN_AAAA → U2_AAAA(f23_out_aaa(0))
with rule P7_IN_AAAA → U2_AAAA(f23_out_aaa(0)) at position [] and matcher [ ]

U2_AAAA(f23_out_aaa(0)) → P7_IN_AAAA
with rule U2_AAAA(f23_out_aaa(T32)) → P7_IN_AAAA

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.



(57) NO

(58) Obligation:

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

F23_IN_GAA(s(T52), T54, X74) → F23_IN_GAA(T52, T54, X73)

The TRS R consists of the following rules:

f1_in_gaa(0, T5, 0) → f1_out_gaa(0, T5, 0)
f1_in_gaa(s(T9), T12, T13) → U7_gaa(T9, T12, T13, p7_in_gaaa(T9, T12, X13, T13))
p7_in_gaaa(0, T27, 0, 0) → p7_out_gaaa(0, T27, 0, 0)
p7_in_gaaa(s(T32), T34, X47, T35) → U1_gaaa(T32, T34, X47, T35, f23_in_gaa(T32, T34, X46))
f23_in_gaa(0, T47, 0) → f23_out_gaa(0, T47, 0)
f23_in_gaa(s(T52), T54, X74) → U4_gaa(T52, T54, X74, f23_in_gaa(T52, T54, X73))
f23_in_gaa(s(T52), T58, X74) → U5_gaa(T52, T58, X74, f23_in_gaa(T52, T58, T57))
U5_gaa(T52, T58, X74, f23_out_gaa(T52, T58, T57)) → U6_gaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
f23_in_aaa(0, T47, 0) → f23_out_aaa(0, T47, 0)
f23_in_aaa(s(T52), T54, X74) → U4_aaa(T52, T54, X74, f23_in_aaa(T52, T54, X73))
f23_in_aaa(s(T52), T58, X74) → U5_aaa(T52, T58, X74, f23_in_aaa(T52, T58, T57))
U5_aaa(T52, T58, X74, f23_out_aaa(T52, T58, T57)) → U6_aaa(T52, T58, X74, f23_in_aaa(T57, T58, X74))
U6_aaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_aaa(s(T52), T58, X74)
U4_aaa(T52, T54, X74, f23_out_aaa(T52, T54, X73)) → f23_out_aaa(s(T52), T54, X74)
U6_gaa(T52, T58, X74, f23_out_aaa(T57, T58, X74)) → f23_out_gaa(s(T52), T58, X74)
U4_gaa(T52, T54, X74, f23_out_gaa(T52, T54, X73)) → f23_out_gaa(s(T52), T54, X74)
U1_gaaa(T32, T34, X47, T35, f23_out_gaa(T32, T34, X46)) → p7_out_gaaa(s(T32), T34, X47, T35)
p7_in_gaaa(s(T32), T39, X47, T40) → U2_gaaa(T32, T39, X47, T40, f23_in_gaa(T32, T39, T38))
U2_gaaa(T32, T39, X47, T40, f23_out_gaa(T32, T39, T38)) → U3_gaaa(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
p7_in_aaaa(0, T27, 0, 0) → p7_out_aaaa(0, T27, 0, 0)
p7_in_aaaa(s(T32), T34, X47, T35) → U1_aaaa(T32, T34, X47, T35, f23_in_aaa(T32, T34, X46))
U1_aaaa(T32, T34, X47, T35, f23_out_aaa(T32, T34, X46)) → p7_out_aaaa(s(T32), T34, X47, T35)
p7_in_aaaa(s(T32), T39, X47, T40) → U2_aaaa(T32, T39, X47, T40, f23_in_aaa(T32, T39, T38))
U2_aaaa(T32, T39, X47, T40, f23_out_aaa(T32, T39, T38)) → U3_aaaa(T32, T39, X47, T40, p7_in_aaaa(T38, T39, X47, T40))
U3_aaaa(T32, T39, X47, T40, p7_out_aaaa(T38, T39, X47, T40)) → p7_out_aaaa(s(T32), T39, X47, T40)
U3_gaaa(T32, T39, X47, T40, p7_out_aaaa(T38, T39, X47, T40)) → p7_out_gaaa(s(T32), T39, X47, T40)
U7_gaa(T9, T12, T13, p7_out_gaaa(T9, T12, X13, T13)) → f1_out_gaa(s(T9), T12, T13)

The argument filtering Pi contains the following mapping:
f1_in_gaa(x1, x2, x3)  =  f1_in_gaa(x1)
0  =  0
f1_out_gaa(x1, x2, x3)  =  f1_out_gaa(x1)
s(x1)  =  s(x1)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x1, x4)
p7_in_gaaa(x1, x2, x3, x4)  =  p7_in_gaaa(x1)
p7_out_gaaa(x1, x2, x3, x4)  =  p7_out_gaaa(x1)
U1_gaaa(x1, x2, x3, x4, x5)  =  U1_gaaa(x1, x5)
f23_in_gaa(x1, x2, x3)  =  f23_in_gaa(x1)
f23_out_gaa(x1, x2, x3)  =  f23_out_gaa(x1)
U4_gaa(x1, x2, x3, x4)  =  U4_gaa(x1, x4)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x1, x4)
f23_in_aaa(x1, x2, x3)  =  f23_in_aaa
f23_out_aaa(x1, x2, x3)  =  f23_out_aaa(x1)
U4_aaa(x1, x2, x3, x4)  =  U4_aaa(x4)
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
U6_aaa(x1, x2, x3, x4)  =  U6_aaa(x1, x4)
U2_gaaa(x1, x2, x3, x4, x5)  =  U2_gaaa(x1, x5)
U3_gaaa(x1, x2, x3, x4, x5)  =  U3_gaaa(x1, x5)
p7_in_aaaa(x1, x2, x3, x4)  =  p7_in_aaaa
p7_out_aaaa(x1, x2, x3, x4)  =  p7_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5)  =  U1_aaaa(x5)
U2_aaaa(x1, x2, x3, x4, x5)  =  U2_aaaa(x5)
U3_aaaa(x1, x2, x3, x4, x5)  =  U3_aaaa(x1, x5)
F23_IN_GAA(x1, x2, x3)  =  F23_IN_GAA(x1)

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

(59) UsableRulesProof (EQUIVALENT transformation)

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

(60) Obligation:

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

F23_IN_GAA(s(T52), T54, X74) → F23_IN_GAA(T52, T54, X73)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
F23_IN_GAA(x1, x2, x3)  =  F23_IN_GAA(x1)

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

(61) PiDPToQDPProof (SOUND transformation)

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

(62) Obligation:

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

F23_IN_GAA(s(T52)) → F23_IN_GAA(T52)

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

(63) 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:

  • F23_IN_GAA(s(T52)) → F23_IN_GAA(T52)
    The graph contains the following edges 1 > 1

(64) YES