Left Termination of the query pattern p(b,f) w.r.t. the given Prolog program could successfully be proven:
↳ PROLOG
↳ PrologToPiTRSProof
p2(X, g1(X)).
p2(X, f1(Y)) :- p2(X, g1(Y)).
With regard to the inferred argument filtering the predicates were used in the following modes:
p2: (b,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
p_2_in_ga2(X, g_11(X)) -> p_2_out_ga2(X, g_11(X))
p_2_in_ga2(X, f_11(Y)) -> if_p_2_in_1_ga3(X, Y, p_2_in_ga2(X, g_11(Y)))
if_p_2_in_1_ga3(X, Y, p_2_out_ga2(X, g_11(Y))) -> p_2_out_ga2(X, f_11(Y))
The argument filtering Pi contains the following mapping:
p_2_in_ga2(x1, x2) = p_2_in_ga1(x1)
g_11(x1) = g_11(x1)
f_11(x1) = f_11(x1)
p_2_out_ga2(x1, x2) = p_2_out_ga1(x2)
if_p_2_in_1_ga3(x1, x2, x3) = if_p_2_in_1_ga1(x3)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
Pi-finite rewrite system:
The TRS R consists of the following rules:
p_2_in_ga2(X, g_11(X)) -> p_2_out_ga2(X, g_11(X))
p_2_in_ga2(X, f_11(Y)) -> if_p_2_in_1_ga3(X, Y, p_2_in_ga2(X, g_11(Y)))
if_p_2_in_1_ga3(X, Y, p_2_out_ga2(X, g_11(Y))) -> p_2_out_ga2(X, f_11(Y))
The argument filtering Pi contains the following mapping:
p_2_in_ga2(x1, x2) = p_2_in_ga1(x1)
g_11(x1) = g_11(x1)
f_11(x1) = f_11(x1)
p_2_out_ga2(x1, x2) = p_2_out_ga1(x2)
if_p_2_in_1_ga3(x1, x2, x3) = if_p_2_in_1_ga1(x3)
Pi DP problem:
The TRS P consists of the following rules:
P_2_IN_GA2(X, f_11(Y)) -> IF_P_2_IN_1_GA3(X, Y, p_2_in_ga2(X, g_11(Y)))
P_2_IN_GA2(X, f_11(Y)) -> P_2_IN_GA2(X, g_11(Y))
The TRS R consists of the following rules:
p_2_in_ga2(X, g_11(X)) -> p_2_out_ga2(X, g_11(X))
p_2_in_ga2(X, f_11(Y)) -> if_p_2_in_1_ga3(X, Y, p_2_in_ga2(X, g_11(Y)))
if_p_2_in_1_ga3(X, Y, p_2_out_ga2(X, g_11(Y))) -> p_2_out_ga2(X, f_11(Y))
The argument filtering Pi contains the following mapping:
p_2_in_ga2(x1, x2) = p_2_in_ga1(x1)
g_11(x1) = g_11(x1)
f_11(x1) = f_11(x1)
p_2_out_ga2(x1, x2) = p_2_out_ga1(x2)
if_p_2_in_1_ga3(x1, x2, x3) = if_p_2_in_1_ga1(x3)
IF_P_2_IN_1_GA3(x1, x2, x3) = IF_P_2_IN_1_GA1(x3)
P_2_IN_GA2(x1, x2) = P_2_IN_GA1(x1)
We have to consider all (P,R,Pi)-chains
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
Pi DP problem:
The TRS P consists of the following rules:
P_2_IN_GA2(X, f_11(Y)) -> IF_P_2_IN_1_GA3(X, Y, p_2_in_ga2(X, g_11(Y)))
P_2_IN_GA2(X, f_11(Y)) -> P_2_IN_GA2(X, g_11(Y))
The TRS R consists of the following rules:
p_2_in_ga2(X, g_11(X)) -> p_2_out_ga2(X, g_11(X))
p_2_in_ga2(X, f_11(Y)) -> if_p_2_in_1_ga3(X, Y, p_2_in_ga2(X, g_11(Y)))
if_p_2_in_1_ga3(X, Y, p_2_out_ga2(X, g_11(Y))) -> p_2_out_ga2(X, f_11(Y))
The argument filtering Pi contains the following mapping:
p_2_in_ga2(x1, x2) = p_2_in_ga1(x1)
g_11(x1) = g_11(x1)
f_11(x1) = f_11(x1)
p_2_out_ga2(x1, x2) = p_2_out_ga1(x2)
if_p_2_in_1_ga3(x1, x2, x3) = if_p_2_in_1_ga1(x3)
IF_P_2_IN_1_GA3(x1, x2, x3) = IF_P_2_IN_1_GA1(x3)
P_2_IN_GA2(x1, x2) = P_2_IN_GA1(x1)
We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph contains 0 SCCs with 2 less nodes.