Left Termination of the query pattern h_in_1(g) w.r.t. the given Prolog program could successfully be proven:

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 QDPSizeChangeProof (⇔)
        ↳15 YES
    ↳16 PiDP
        ↳17 UsableRulesProof (⇔)
        ↳18 PiDP
        ↳19 PiDPToQDPProof (⇔)
        ↳20 QDP
        ↳21 QDPSizeChangeProof (⇔)
        ↳22 YES

(0) Obligation:

Clauses:

f(c(s(X), Y)) :- f(c(X, s(Y))).
g(c(X, s(Y))) :- g(c(s(X), Y)).
h(X) :- ','(f(X), g(X)).

Queries:

h(g).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

(2) Obligation:

Clauses:

f7(s(T18), T19) :- f7(T18, s(T19)).
g8(T28, s(T29)) :- g8(s(T28), T29).
h1(c(s(T8), T9)) :- f7(T8, T9).
h1(c(s(T8), T9)) :- ','(f7(T8, T9), g8(T8, T9)).

Queries:

h1(g).

(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:
h1_in: (b)
f7_in: (b,b)
g8_in: (b,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

h1_in_g(c(s(T8), T9)) → U3_g(T8, T9, f7_in_gg(T8, T9))
f7_in_gg(s(T18), T19) → U1_gg(T18, T19, f7_in_gg(T18, s(T19)))
U1_gg(T18, T19, f7_out_gg(T18, s(T19))) → f7_out_gg(s(T18), T19)
U3_g(T8, T9, f7_out_gg(T8, T9)) → h1_out_g(c(s(T8), T9))
U3_g(T8, T9, f7_out_gg(T8, T9)) → U4_g(T8, T9, g8_in_gg(T8, T9))
g8_in_gg(T28, s(T29)) → U2_gg(T28, T29, g8_in_gg(s(T28), T29))
U2_gg(T28, T29, g8_out_gg(s(T28), T29)) → g8_out_gg(T28, s(T29))
U4_g(T8, T9, g8_out_gg(T8, T9)) → h1_out_g(c(s(T8), T9))

The argument filtering Pi contains the following mapping:
h1_in_g(x1)  =  h1_in_g(x1)
c(x1, x2)  =  c(x1, x2)
s(x1)  =  s(x1)
U3_g(x1, x2, x3)  =  U3_g(x1, x2, x3)
f7_in_gg(x1, x2)  =  f7_in_gg(x1, x2)
U1_gg(x1, x2, x3)  =  U1_gg(x3)
f7_out_gg(x1, x2)  =  f7_out_gg
h1_out_g(x1)  =  h1_out_g
U4_g(x1, x2, x3)  =  U4_g(x3)
g8_in_gg(x1, x2)  =  g8_in_gg(x1, x2)
U2_gg(x1, x2, x3)  =  U2_gg(x3)
g8_out_gg(x1, x2)  =  g8_out_gg

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

h1_in_g(c(s(T8), T9)) → U3_g(T8, T9, f7_in_gg(T8, T9))
f7_in_gg(s(T18), T19) → U1_gg(T18, T19, f7_in_gg(T18, s(T19)))
U1_gg(T18, T19, f7_out_gg(T18, s(T19))) → f7_out_gg(s(T18), T19)
U3_g(T8, T9, f7_out_gg(T8, T9)) → h1_out_g(c(s(T8), T9))
U3_g(T8, T9, f7_out_gg(T8, T9)) → U4_g(T8, T9, g8_in_gg(T8, T9))
g8_in_gg(T28, s(T29)) → U2_gg(T28, T29, g8_in_gg(s(T28), T29))
U2_gg(T28, T29, g8_out_gg(s(T28), T29)) → g8_out_gg(T28, s(T29))
U4_g(T8, T9, g8_out_gg(T8, T9)) → h1_out_g(c(s(T8), T9))

The argument filtering Pi contains the following mapping:
h1_in_g(x1)  =  h1_in_g(x1)
c(x1, x2)  =  c(x1, x2)
s(x1)  =  s(x1)
U3_g(x1, x2, x3)  =  U3_g(x1, x2, x3)
f7_in_gg(x1, x2)  =  f7_in_gg(x1, x2)
U1_gg(x1, x2, x3)  =  U1_gg(x3)
f7_out_gg(x1, x2)  =  f7_out_gg
h1_out_g(x1)  =  h1_out_g
U4_g(x1, x2, x3)  =  U4_g(x3)
g8_in_gg(x1, x2)  =  g8_in_gg(x1, x2)
U2_gg(x1, x2, x3)  =  U2_gg(x3)
g8_out_gg(x1, x2)  =  g8_out_gg

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

H1_IN_G(c(s(T8), T9)) → U3_G(T8, T9, f7_in_gg(T8, T9))
H1_IN_G(c(s(T8), T9)) → F7_IN_GG(T8, T9)
F7_IN_GG(s(T18), T19) → U1_GG(T18, T19, f7_in_gg(T18, s(T19)))
F7_IN_GG(s(T18), T19) → F7_IN_GG(T18, s(T19))
U3_G(T8, T9, f7_out_gg(T8, T9)) → U4_G(T8, T9, g8_in_gg(T8, T9))
U3_G(T8, T9, f7_out_gg(T8, T9)) → G8_IN_GG(T8, T9)
G8_IN_GG(T28, s(T29)) → U2_GG(T28, T29, g8_in_gg(s(T28), T29))
G8_IN_GG(T28, s(T29)) → G8_IN_GG(s(T28), T29)

The TRS R consists of the following rules:

h1_in_g(c(s(T8), T9)) → U3_g(T8, T9, f7_in_gg(T8, T9))
f7_in_gg(s(T18), T19) → U1_gg(T18, T19, f7_in_gg(T18, s(T19)))
U1_gg(T18, T19, f7_out_gg(T18, s(T19))) → f7_out_gg(s(T18), T19)
U3_g(T8, T9, f7_out_gg(T8, T9)) → h1_out_g(c(s(T8), T9))
U3_g(T8, T9, f7_out_gg(T8, T9)) → U4_g(T8, T9, g8_in_gg(T8, T9))
g8_in_gg(T28, s(T29)) → U2_gg(T28, T29, g8_in_gg(s(T28), T29))
U2_gg(T28, T29, g8_out_gg(s(T28), T29)) → g8_out_gg(T28, s(T29))
U4_g(T8, T9, g8_out_gg(T8, T9)) → h1_out_g(c(s(T8), T9))

The argument filtering Pi contains the following mapping:
h1_in_g(x1)  =  h1_in_g(x1)
c(x1, x2)  =  c(x1, x2)
s(x1)  =  s(x1)
U3_g(x1, x2, x3)  =  U3_g(x1, x2, x3)
f7_in_gg(x1, x2)  =  f7_in_gg(x1, x2)
U1_gg(x1, x2, x3)  =  U1_gg(x3)
f7_out_gg(x1, x2)  =  f7_out_gg
h1_out_g(x1)  =  h1_out_g
U4_g(x1, x2, x3)  =  U4_g(x3)
g8_in_gg(x1, x2)  =  g8_in_gg(x1, x2)
U2_gg(x1, x2, x3)  =  U2_gg(x3)
g8_out_gg(x1, x2)  =  g8_out_gg
H1_IN_G(x1)  =  H1_IN_G(x1)
U3_G(x1, x2, x3)  =  U3_G(x1, x2, x3)
F7_IN_GG(x1, x2)  =  F7_IN_GG(x1, x2)
U1_GG(x1, x2, x3)  =  U1_GG(x3)
U4_G(x1, x2, x3)  =  U4_G(x3)
G8_IN_GG(x1, x2)  =  G8_IN_GG(x1, x2)
U2_GG(x1, x2, x3)  =  U2_GG(x3)

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

(6) Obligation:

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

H1_IN_G(c(s(T8), T9)) → U3_G(T8, T9, f7_in_gg(T8, T9))
H1_IN_G(c(s(T8), T9)) → F7_IN_GG(T8, T9)
F7_IN_GG(s(T18), T19) → U1_GG(T18, T19, f7_in_gg(T18, s(T19)))
F7_IN_GG(s(T18), T19) → F7_IN_GG(T18, s(T19))
U3_G(T8, T9, f7_out_gg(T8, T9)) → U4_G(T8, T9, g8_in_gg(T8, T9))
U3_G(T8, T9, f7_out_gg(T8, T9)) → G8_IN_GG(T8, T9)
G8_IN_GG(T28, s(T29)) → U2_GG(T28, T29, g8_in_gg(s(T28), T29))
G8_IN_GG(T28, s(T29)) → G8_IN_GG(s(T28), T29)

The TRS R consists of the following rules:

h1_in_g(c(s(T8), T9)) → U3_g(T8, T9, f7_in_gg(T8, T9))
f7_in_gg(s(T18), T19) → U1_gg(T18, T19, f7_in_gg(T18, s(T19)))
U1_gg(T18, T19, f7_out_gg(T18, s(T19))) → f7_out_gg(s(T18), T19)
U3_g(T8, T9, f7_out_gg(T8, T9)) → h1_out_g(c(s(T8), T9))
U3_g(T8, T9, f7_out_gg(T8, T9)) → U4_g(T8, T9, g8_in_gg(T8, T9))
g8_in_gg(T28, s(T29)) → U2_gg(T28, T29, g8_in_gg(s(T28), T29))
U2_gg(T28, T29, g8_out_gg(s(T28), T29)) → g8_out_gg(T28, s(T29))
U4_g(T8, T9, g8_out_gg(T8, T9)) → h1_out_g(c(s(T8), T9))

The argument filtering Pi contains the following mapping:
h1_in_g(x1)  =  h1_in_g(x1)
c(x1, x2)  =  c(x1, x2)
s(x1)  =  s(x1)
U3_g(x1, x2, x3)  =  U3_g(x1, x2, x3)
f7_in_gg(x1, x2)  =  f7_in_gg(x1, x2)
U1_gg(x1, x2, x3)  =  U1_gg(x3)
f7_out_gg(x1, x2)  =  f7_out_gg
h1_out_g(x1)  =  h1_out_g
U4_g(x1, x2, x3)  =  U4_g(x3)
g8_in_gg(x1, x2)  =  g8_in_gg(x1, x2)
U2_gg(x1, x2, x3)  =  U2_gg(x3)
g8_out_gg(x1, x2)  =  g8_out_gg
H1_IN_G(x1)  =  H1_IN_G(x1)
U3_G(x1, x2, x3)  =  U3_G(x1, x2, x3)
F7_IN_GG(x1, x2)  =  F7_IN_GG(x1, x2)
U1_GG(x1, x2, x3)  =  U1_GG(x3)
U4_G(x1, x2, x3)  =  U4_G(x3)
G8_IN_GG(x1, x2)  =  G8_IN_GG(x1, x2)
U2_GG(x1, x2, x3)  =  U2_GG(x3)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 6 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

G8_IN_GG(T28, s(T29)) → G8_IN_GG(s(T28), T29)

The TRS R consists of the following rules:

h1_in_g(c(s(T8), T9)) → U3_g(T8, T9, f7_in_gg(T8, T9))
f7_in_gg(s(T18), T19) → U1_gg(T18, T19, f7_in_gg(T18, s(T19)))
U1_gg(T18, T19, f7_out_gg(T18, s(T19))) → f7_out_gg(s(T18), T19)
U3_g(T8, T9, f7_out_gg(T8, T9)) → h1_out_g(c(s(T8), T9))
U3_g(T8, T9, f7_out_gg(T8, T9)) → U4_g(T8, T9, g8_in_gg(T8, T9))
g8_in_gg(T28, s(T29)) → U2_gg(T28, T29, g8_in_gg(s(T28), T29))
U2_gg(T28, T29, g8_out_gg(s(T28), T29)) → g8_out_gg(T28, s(T29))
U4_g(T8, T9, g8_out_gg(T8, T9)) → h1_out_g(c(s(T8), T9))

The argument filtering Pi contains the following mapping:
h1_in_g(x1)  =  h1_in_g(x1)
c(x1, x2)  =  c(x1, x2)
s(x1)  =  s(x1)
U3_g(x1, x2, x3)  =  U3_g(x1, x2, x3)
f7_in_gg(x1, x2)  =  f7_in_gg(x1, x2)
U1_gg(x1, x2, x3)  =  U1_gg(x3)
f7_out_gg(x1, x2)  =  f7_out_gg
h1_out_g(x1)  =  h1_out_g
U4_g(x1, x2, x3)  =  U4_g(x3)
g8_in_gg(x1, x2)  =  g8_in_gg(x1, x2)
U2_gg(x1, x2, x3)  =  U2_gg(x3)
g8_out_gg(x1, x2)  =  g8_out_gg
G8_IN_GG(x1, x2)  =  G8_IN_GG(x1, x2)

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:

G8_IN_GG(T28, s(T29)) → G8_IN_GG(s(T28), T29)

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

(12) PiDPToQDPProof (EQUIVALENT 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:

G8_IN_GG(T28, s(T29)) → G8_IN_GG(s(T28), T29)

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

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

  • G8_IN_GG(T28, s(T29)) → G8_IN_GG(s(T28), T29)
    The graph contains the following edges 2 > 2

(15) YES

(16) Obligation:

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

F7_IN_GG(s(T18), T19) → F7_IN_GG(T18, s(T19))

The TRS R consists of the following rules:

h1_in_g(c(s(T8), T9)) → U3_g(T8, T9, f7_in_gg(T8, T9))
f7_in_gg(s(T18), T19) → U1_gg(T18, T19, f7_in_gg(T18, s(T19)))
U1_gg(T18, T19, f7_out_gg(T18, s(T19))) → f7_out_gg(s(T18), T19)
U3_g(T8, T9, f7_out_gg(T8, T9)) → h1_out_g(c(s(T8), T9))
U3_g(T8, T9, f7_out_gg(T8, T9)) → U4_g(T8, T9, g8_in_gg(T8, T9))
g8_in_gg(T28, s(T29)) → U2_gg(T28, T29, g8_in_gg(s(T28), T29))
U2_gg(T28, T29, g8_out_gg(s(T28), T29)) → g8_out_gg(T28, s(T29))
U4_g(T8, T9, g8_out_gg(T8, T9)) → h1_out_g(c(s(T8), T9))

The argument filtering Pi contains the following mapping:
h1_in_g(x1)  =  h1_in_g(x1)
c(x1, x2)  =  c(x1, x2)
s(x1)  =  s(x1)
U3_g(x1, x2, x3)  =  U3_g(x1, x2, x3)
f7_in_gg(x1, x2)  =  f7_in_gg(x1, x2)
U1_gg(x1, x2, x3)  =  U1_gg(x3)
f7_out_gg(x1, x2)  =  f7_out_gg
h1_out_g(x1)  =  h1_out_g
U4_g(x1, x2, x3)  =  U4_g(x3)
g8_in_gg(x1, x2)  =  g8_in_gg(x1, x2)
U2_gg(x1, x2, x3)  =  U2_gg(x3)
g8_out_gg(x1, x2)  =  g8_out_gg
F7_IN_GG(x1, x2)  =  F7_IN_GG(x1, x2)

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

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

F7_IN_GG(s(T18), T19) → F7_IN_GG(T18, s(T19))

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

(19) PiDPToQDPProof (EQUIVALENT transformation)

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

(20) Obligation:

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

F7_IN_GG(s(T18), T19) → F7_IN_GG(T18, s(T19))

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

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

  • F7_IN_GG(s(T18), T19) → F7_IN_GG(T18, s(T19))
    The graph contains the following edges 1 > 1

(22) YES