(0) Obligation:

Clauses:

even(0) :- !.
even(N) :- ','(p(N, P), odd(P)).
odd(s(0)) :- !.
odd(s(N)) :- even(P).
p(0, 0).
p(s(X), X).

Queries:

even(g).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

(2) Obligation:

Clauses:

even1(0).
even1(s(s(0))).
even1(s(s(T4))).

Queries:

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

even1_in_g(0) → even1_out_g(0)
even1_in_g(s(s(0))) → even1_out_g(s(s(0)))
even1_in_g(s(s(T4))) → even1_out_g(s(s(T4)))

The argument filtering Pi contains the following mapping:
even1_in_g(x1)  =  even1_in_g(x1)
0  =  0
even1_out_g(x1)  =  even1_out_g
s(x1)  =  s(x1)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

even1_in_g(0) → even1_out_g(0)
even1_in_g(s(s(0))) → even1_out_g(s(s(0)))
even1_in_g(s(s(T4))) → even1_out_g(s(s(T4)))

The argument filtering Pi contains the following mapping:
even1_in_g(x1)  =  even1_in_g(x1)
0  =  0
even1_out_g(x1)  =  even1_out_g
s(x1)  =  s(x1)

(5) DependencyPairsProof (EQUIVALENT transformation)

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

even1_in_g(0) → even1_out_g(0)
even1_in_g(s(s(0))) → even1_out_g(s(s(0)))
even1_in_g(s(s(T4))) → even1_out_g(s(s(T4)))

The argument filtering Pi contains the following mapping:
even1_in_g(x1)  =  even1_in_g(x1)
0  =  0
even1_out_g(x1)  =  even1_out_g
s(x1)  =  s(x1)

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

(6) Obligation:

Pi DP problem:
P is empty.
The TRS R consists of the following rules:

even1_in_g(0) → even1_out_g(0)
even1_in_g(s(s(0))) → even1_out_g(s(s(0)))
even1_in_g(s(s(T4))) → even1_out_g(s(s(T4)))

The argument filtering Pi contains the following mapping:
even1_in_g(x1)  =  even1_in_g(x1)
0  =  0
even1_out_g(x1)  =  even1_out_g
s(x1)  =  s(x1)

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

(7) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,R,Pi) chain.

(8) TRUE