(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)).

Query: h(g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

(2) Obligation:

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

hA_in_g(c(s(T8), T9)) → U1_g(T8, T9, pB_in_gg(T8, T9))
pB_in_gg(T8, T9) → U4_gg(T8, T9, fC_in_gg(T8, T9))
fC_in_gg(s(T18), T19) → U2_gg(T18, T19, fC_in_gg(T18, s(T19)))
U2_gg(T18, T19, fC_out_gg(T18, s(T19))) → fC_out_gg(s(T18), T19)
U4_gg(T8, T9, fC_out_gg(T8, T9)) → U5_gg(T8, T9, gD_in_gg(T8, T9))
gD_in_gg(T28, s(T29)) → U3_gg(T28, T29, gD_in_gg(s(T28), T29))
U3_gg(T28, T29, gD_out_gg(s(T28), T29)) → gD_out_gg(T28, s(T29))
U5_gg(T8, T9, gD_out_gg(T8, T9)) → pB_out_gg(T8, T9)
U1_g(T8, T9, pB_out_gg(T8, T9)) → hA_out_g(c(s(T8), T9))

Pi is empty.

(3) DependencyPairsProof (EQUIVALENT transformation)

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

HA_IN_G(c(s(T8), T9)) → U1_G(T8, T9, pB_in_gg(T8, T9))
HA_IN_G(c(s(T8), T9)) → PB_IN_GG(T8, T9)
PB_IN_GG(T8, T9) → U4_GG(T8, T9, fC_in_gg(T8, T9))
PB_IN_GG(T8, T9) → FC_IN_GG(T8, T9)
FC_IN_GG(s(T18), T19) → U2_GG(T18, T19, fC_in_gg(T18, s(T19)))
FC_IN_GG(s(T18), T19) → FC_IN_GG(T18, s(T19))
U4_GG(T8, T9, fC_out_gg(T8, T9)) → U5_GG(T8, T9, gD_in_gg(T8, T9))
U4_GG(T8, T9, fC_out_gg(T8, T9)) → GD_IN_GG(T8, T9)
GD_IN_GG(T28, s(T29)) → U3_GG(T28, T29, gD_in_gg(s(T28), T29))
GD_IN_GG(T28, s(T29)) → GD_IN_GG(s(T28), T29)

The TRS R consists of the following rules:

hA_in_g(c(s(T8), T9)) → U1_g(T8, T9, pB_in_gg(T8, T9))
pB_in_gg(T8, T9) → U4_gg(T8, T9, fC_in_gg(T8, T9))
fC_in_gg(s(T18), T19) → U2_gg(T18, T19, fC_in_gg(T18, s(T19)))
U2_gg(T18, T19, fC_out_gg(T18, s(T19))) → fC_out_gg(s(T18), T19)
U4_gg(T8, T9, fC_out_gg(T8, T9)) → U5_gg(T8, T9, gD_in_gg(T8, T9))
gD_in_gg(T28, s(T29)) → U3_gg(T28, T29, gD_in_gg(s(T28), T29))
U3_gg(T28, T29, gD_out_gg(s(T28), T29)) → gD_out_gg(T28, s(T29))
U5_gg(T8, T9, gD_out_gg(T8, T9)) → pB_out_gg(T8, T9)
U1_g(T8, T9, pB_out_gg(T8, T9)) → hA_out_g(c(s(T8), T9))

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

(4) Obligation:

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

HA_IN_G(c(s(T8), T9)) → U1_G(T8, T9, pB_in_gg(T8, T9))
HA_IN_G(c(s(T8), T9)) → PB_IN_GG(T8, T9)
PB_IN_GG(T8, T9) → U4_GG(T8, T9, fC_in_gg(T8, T9))
PB_IN_GG(T8, T9) → FC_IN_GG(T8, T9)
FC_IN_GG(s(T18), T19) → U2_GG(T18, T19, fC_in_gg(T18, s(T19)))
FC_IN_GG(s(T18), T19) → FC_IN_GG(T18, s(T19))
U4_GG(T8, T9, fC_out_gg(T8, T9)) → U5_GG(T8, T9, gD_in_gg(T8, T9))
U4_GG(T8, T9, fC_out_gg(T8, T9)) → GD_IN_GG(T8, T9)
GD_IN_GG(T28, s(T29)) → U3_GG(T28, T29, gD_in_gg(s(T28), T29))
GD_IN_GG(T28, s(T29)) → GD_IN_GG(s(T28), T29)

The TRS R consists of the following rules:

hA_in_g(c(s(T8), T9)) → U1_g(T8, T9, pB_in_gg(T8, T9))
pB_in_gg(T8, T9) → U4_gg(T8, T9, fC_in_gg(T8, T9))
fC_in_gg(s(T18), T19) → U2_gg(T18, T19, fC_in_gg(T18, s(T19)))
U2_gg(T18, T19, fC_out_gg(T18, s(T19))) → fC_out_gg(s(T18), T19)
U4_gg(T8, T9, fC_out_gg(T8, T9)) → U5_gg(T8, T9, gD_in_gg(T8, T9))
gD_in_gg(T28, s(T29)) → U3_gg(T28, T29, gD_in_gg(s(T28), T29))
U3_gg(T28, T29, gD_out_gg(s(T28), T29)) → gD_out_gg(T28, s(T29))
U5_gg(T8, T9, gD_out_gg(T8, T9)) → pB_out_gg(T8, T9)
U1_g(T8, T9, pB_out_gg(T8, T9)) → hA_out_g(c(s(T8), T9))

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

GD_IN_GG(T28, s(T29)) → GD_IN_GG(s(T28), T29)

The TRS R consists of the following rules:

hA_in_g(c(s(T8), T9)) → U1_g(T8, T9, pB_in_gg(T8, T9))
pB_in_gg(T8, T9) → U4_gg(T8, T9, fC_in_gg(T8, T9))
fC_in_gg(s(T18), T19) → U2_gg(T18, T19, fC_in_gg(T18, s(T19)))
U2_gg(T18, T19, fC_out_gg(T18, s(T19))) → fC_out_gg(s(T18), T19)
U4_gg(T8, T9, fC_out_gg(T8, T9)) → U5_gg(T8, T9, gD_in_gg(T8, T9))
gD_in_gg(T28, s(T29)) → U3_gg(T28, T29, gD_in_gg(s(T28), T29))
U3_gg(T28, T29, gD_out_gg(s(T28), T29)) → gD_out_gg(T28, s(T29))
U5_gg(T8, T9, gD_out_gg(T8, T9)) → pB_out_gg(T8, T9)
U1_g(T8, T9, pB_out_gg(T8, T9)) → hA_out_g(c(s(T8), T9))

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

GD_IN_GG(T28, s(T29)) → GD_IN_GG(s(T28), T29)

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

(10) PiDPToQDPProof (EQUIVALENT transformation)

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

(11) Obligation:

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

GD_IN_GG(T28, s(T29)) → GD_IN_GG(s(T28), T29)

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

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

(13) YES

(14) Obligation:

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

FC_IN_GG(s(T18), T19) → FC_IN_GG(T18, s(T19))

The TRS R consists of the following rules:

hA_in_g(c(s(T8), T9)) → U1_g(T8, T9, pB_in_gg(T8, T9))
pB_in_gg(T8, T9) → U4_gg(T8, T9, fC_in_gg(T8, T9))
fC_in_gg(s(T18), T19) → U2_gg(T18, T19, fC_in_gg(T18, s(T19)))
U2_gg(T18, T19, fC_out_gg(T18, s(T19))) → fC_out_gg(s(T18), T19)
U4_gg(T8, T9, fC_out_gg(T8, T9)) → U5_gg(T8, T9, gD_in_gg(T8, T9))
gD_in_gg(T28, s(T29)) → U3_gg(T28, T29, gD_in_gg(s(T28), T29))
U3_gg(T28, T29, gD_out_gg(s(T28), T29)) → gD_out_gg(T28, s(T29))
U5_gg(T8, T9, gD_out_gg(T8, T9)) → pB_out_gg(T8, T9)
U1_g(T8, T9, pB_out_gg(T8, T9)) → hA_out_g(c(s(T8), T9))

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

FC_IN_GG(s(T18), T19) → FC_IN_GG(T18, s(T19))

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

(17) PiDPToQDPProof (EQUIVALENT transformation)

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

(18) Obligation:

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

FC_IN_GG(s(T18), T19) → FC_IN_GG(T18, s(T19))

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

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

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

(20) YES