↳ PROLOG
↳ UnrequestedClauseRemoverProof
The clauses
isNat1(s1(X)) :- isNat1(X).
isNat1(00).
notEq2(s1(X), s1(Y)) :- notEq2(X, Y).
notEq2(s1(X), 00).
notEq2(00, s1(X)).
lt2(s1(X), s1(Y)) :- lt2(X, Y).
lt2(00, s1(Y)).
gt2(s1(X), s1(Y)) :- gt2(X, Y).
gt2(s1(X), 00).
le2(s1(X), s1(Y)) :- le2(X, Y).
le2(00, s1(Y)).
le2(00, 00).
even1(s1(X)) :- odd1(X).
even1(00).
odd1(s1(X)) :- even1(X).
odd1(s1(00)).
can be ignored, as they are not needed by any of the given querys.
Deleting these clauses results in the following prolog program:
add3(s1(X), Y, s1(Z)) :- add3(X, Y, Z).
add3(00, X, X).
mult3(s1(X), Y, R) :- mult3(X, Y, Z), add3(Y, Z, R).
mult3(00, Y, 00).
factorial2(s1(X), R) :- factorial2(X, Y), mult3(s1(X), Y, R).
factorial2(00, s1(00)).
↳ PROLOG
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
With regard to the inferred argument filtering the predicates were used in the following modes:
factorial2: (b,f)
mult3: (b,b,f)
add3: (b,b,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
factorial_2_in_ga2(s_11(X), R) -> if_factorial_2_in_1_ga3(X, R, factorial_2_in_ga2(X, Y))
factorial_2_in_ga2(0_0, s_11(0_0)) -> factorial_2_out_ga2(0_0, s_11(0_0))
if_factorial_2_in_1_ga3(X, R, factorial_2_out_ga2(X, Y)) -> if_factorial_2_in_2_ga4(X, R, Y, mult_3_in_gga3(s_11(X), Y, R))
mult_3_in_gga3(s_11(X), Y, R) -> if_mult_3_in_1_gga4(X, Y, R, mult_3_in_gga3(X, Y, Z))
mult_3_in_gga3(0_0, Y, 0_0) -> mult_3_out_gga3(0_0, Y, 0_0)
if_mult_3_in_1_gga4(X, Y, R, mult_3_out_gga3(X, Y, Z)) -> if_mult_3_in_2_gga5(X, Y, R, Z, add_3_in_gga3(Y, Z, R))
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_mult_3_in_2_gga5(X, Y, R, Z, add_3_out_gga3(Y, Z, R)) -> mult_3_out_gga3(s_11(X), Y, R)
if_factorial_2_in_2_ga4(X, R, Y, mult_3_out_gga3(s_11(X), Y, R)) -> factorial_2_out_ga2(s_11(X), R)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG
↳ PROLOG
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
factorial_2_in_ga2(s_11(X), R) -> if_factorial_2_in_1_ga3(X, R, factorial_2_in_ga2(X, Y))
factorial_2_in_ga2(0_0, s_11(0_0)) -> factorial_2_out_ga2(0_0, s_11(0_0))
if_factorial_2_in_1_ga3(X, R, factorial_2_out_ga2(X, Y)) -> if_factorial_2_in_2_ga4(X, R, Y, mult_3_in_gga3(s_11(X), Y, R))
mult_3_in_gga3(s_11(X), Y, R) -> if_mult_3_in_1_gga4(X, Y, R, mult_3_in_gga3(X, Y, Z))
mult_3_in_gga3(0_0, Y, 0_0) -> mult_3_out_gga3(0_0, Y, 0_0)
if_mult_3_in_1_gga4(X, Y, R, mult_3_out_gga3(X, Y, Z)) -> if_mult_3_in_2_gga5(X, Y, R, Z, add_3_in_gga3(Y, Z, R))
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_mult_3_in_2_gga5(X, Y, R, Z, add_3_out_gga3(Y, Z, R)) -> mult_3_out_gga3(s_11(X), Y, R)
if_factorial_2_in_2_ga4(X, R, Y, mult_3_out_gga3(s_11(X), Y, R)) -> factorial_2_out_ga2(s_11(X), R)
FACTORIAL_2_IN_GA2(s_11(X), R) -> IF_FACTORIAL_2_IN_1_GA3(X, R, factorial_2_in_ga2(X, Y))
FACTORIAL_2_IN_GA2(s_11(X), R) -> FACTORIAL_2_IN_GA2(X, Y)
IF_FACTORIAL_2_IN_1_GA3(X, R, factorial_2_out_ga2(X, Y)) -> IF_FACTORIAL_2_IN_2_GA4(X, R, Y, mult_3_in_gga3(s_11(X), Y, R))
IF_FACTORIAL_2_IN_1_GA3(X, R, factorial_2_out_ga2(X, Y)) -> MULT_3_IN_GGA3(s_11(X), Y, R)
MULT_3_IN_GGA3(s_11(X), Y, R) -> IF_MULT_3_IN_1_GGA4(X, Y, R, mult_3_in_gga3(X, Y, Z))
MULT_3_IN_GGA3(s_11(X), Y, R) -> MULT_3_IN_GGA3(X, Y, Z)
IF_MULT_3_IN_1_GGA4(X, Y, R, mult_3_out_gga3(X, Y, Z)) -> IF_MULT_3_IN_2_GGA5(X, Y, R, Z, add_3_in_gga3(Y, Z, R))
IF_MULT_3_IN_1_GGA4(X, Y, R, mult_3_out_gga3(X, Y, Z)) -> ADD_3_IN_GGA3(Y, Z, R)
ADD_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> IF_ADD_3_IN_1_GGA4(X, Y, Z, add_3_in_gga3(X, Y, Z))
ADD_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> ADD_3_IN_GGA3(X, Y, Z)
factorial_2_in_ga2(s_11(X), R) -> if_factorial_2_in_1_ga3(X, R, factorial_2_in_ga2(X, Y))
factorial_2_in_ga2(0_0, s_11(0_0)) -> factorial_2_out_ga2(0_0, s_11(0_0))
if_factorial_2_in_1_ga3(X, R, factorial_2_out_ga2(X, Y)) -> if_factorial_2_in_2_ga4(X, R, Y, mult_3_in_gga3(s_11(X), Y, R))
mult_3_in_gga3(s_11(X), Y, R) -> if_mult_3_in_1_gga4(X, Y, R, mult_3_in_gga3(X, Y, Z))
mult_3_in_gga3(0_0, Y, 0_0) -> mult_3_out_gga3(0_0, Y, 0_0)
if_mult_3_in_1_gga4(X, Y, R, mult_3_out_gga3(X, Y, Z)) -> if_mult_3_in_2_gga5(X, Y, R, Z, add_3_in_gga3(Y, Z, R))
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_mult_3_in_2_gga5(X, Y, R, Z, add_3_out_gga3(Y, Z, R)) -> mult_3_out_gga3(s_11(X), Y, R)
if_factorial_2_in_2_ga4(X, R, Y, mult_3_out_gga3(s_11(X), Y, R)) -> factorial_2_out_ga2(s_11(X), R)
↳ PROLOG
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
FACTORIAL_2_IN_GA2(s_11(X), R) -> IF_FACTORIAL_2_IN_1_GA3(X, R, factorial_2_in_ga2(X, Y))
FACTORIAL_2_IN_GA2(s_11(X), R) -> FACTORIAL_2_IN_GA2(X, Y)
IF_FACTORIAL_2_IN_1_GA3(X, R, factorial_2_out_ga2(X, Y)) -> IF_FACTORIAL_2_IN_2_GA4(X, R, Y, mult_3_in_gga3(s_11(X), Y, R))
IF_FACTORIAL_2_IN_1_GA3(X, R, factorial_2_out_ga2(X, Y)) -> MULT_3_IN_GGA3(s_11(X), Y, R)
MULT_3_IN_GGA3(s_11(X), Y, R) -> IF_MULT_3_IN_1_GGA4(X, Y, R, mult_3_in_gga3(X, Y, Z))
MULT_3_IN_GGA3(s_11(X), Y, R) -> MULT_3_IN_GGA3(X, Y, Z)
IF_MULT_3_IN_1_GGA4(X, Y, R, mult_3_out_gga3(X, Y, Z)) -> IF_MULT_3_IN_2_GGA5(X, Y, R, Z, add_3_in_gga3(Y, Z, R))
IF_MULT_3_IN_1_GGA4(X, Y, R, mult_3_out_gga3(X, Y, Z)) -> ADD_3_IN_GGA3(Y, Z, R)
ADD_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> IF_ADD_3_IN_1_GGA4(X, Y, Z, add_3_in_gga3(X, Y, Z))
ADD_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> ADD_3_IN_GGA3(X, Y, Z)
factorial_2_in_ga2(s_11(X), R) -> if_factorial_2_in_1_ga3(X, R, factorial_2_in_ga2(X, Y))
factorial_2_in_ga2(0_0, s_11(0_0)) -> factorial_2_out_ga2(0_0, s_11(0_0))
if_factorial_2_in_1_ga3(X, R, factorial_2_out_ga2(X, Y)) -> if_factorial_2_in_2_ga4(X, R, Y, mult_3_in_gga3(s_11(X), Y, R))
mult_3_in_gga3(s_11(X), Y, R) -> if_mult_3_in_1_gga4(X, Y, R, mult_3_in_gga3(X, Y, Z))
mult_3_in_gga3(0_0, Y, 0_0) -> mult_3_out_gga3(0_0, Y, 0_0)
if_mult_3_in_1_gga4(X, Y, R, mult_3_out_gga3(X, Y, Z)) -> if_mult_3_in_2_gga5(X, Y, R, Z, add_3_in_gga3(Y, Z, R))
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_mult_3_in_2_gga5(X, Y, R, Z, add_3_out_gga3(Y, Z, R)) -> mult_3_out_gga3(s_11(X), Y, R)
if_factorial_2_in_2_ga4(X, R, Y, mult_3_out_gga3(s_11(X), Y, R)) -> factorial_2_out_ga2(s_11(X), R)
↳ PROLOG
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
ADD_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> ADD_3_IN_GGA3(X, Y, Z)
factorial_2_in_ga2(s_11(X), R) -> if_factorial_2_in_1_ga3(X, R, factorial_2_in_ga2(X, Y))
factorial_2_in_ga2(0_0, s_11(0_0)) -> factorial_2_out_ga2(0_0, s_11(0_0))
if_factorial_2_in_1_ga3(X, R, factorial_2_out_ga2(X, Y)) -> if_factorial_2_in_2_ga4(X, R, Y, mult_3_in_gga3(s_11(X), Y, R))
mult_3_in_gga3(s_11(X), Y, R) -> if_mult_3_in_1_gga4(X, Y, R, mult_3_in_gga3(X, Y, Z))
mult_3_in_gga3(0_0, Y, 0_0) -> mult_3_out_gga3(0_0, Y, 0_0)
if_mult_3_in_1_gga4(X, Y, R, mult_3_out_gga3(X, Y, Z)) -> if_mult_3_in_2_gga5(X, Y, R, Z, add_3_in_gga3(Y, Z, R))
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_mult_3_in_2_gga5(X, Y, R, Z, add_3_out_gga3(Y, Z, R)) -> mult_3_out_gga3(s_11(X), Y, R)
if_factorial_2_in_2_ga4(X, R, Y, mult_3_out_gga3(s_11(X), Y, R)) -> factorial_2_out_ga2(s_11(X), R)
↳ PROLOG
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
ADD_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> ADD_3_IN_GGA3(X, Y, Z)
↳ PROLOG
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
↳ PiDP
ADD_3_IN_GGA2(s_11(X), Y) -> ADD_3_IN_GGA2(X, Y)
From the DPs we obtained the following set of size-change graphs:
↳ PROLOG
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
MULT_3_IN_GGA3(s_11(X), Y, R) -> MULT_3_IN_GGA3(X, Y, Z)
factorial_2_in_ga2(s_11(X), R) -> if_factorial_2_in_1_ga3(X, R, factorial_2_in_ga2(X, Y))
factorial_2_in_ga2(0_0, s_11(0_0)) -> factorial_2_out_ga2(0_0, s_11(0_0))
if_factorial_2_in_1_ga3(X, R, factorial_2_out_ga2(X, Y)) -> if_factorial_2_in_2_ga4(X, R, Y, mult_3_in_gga3(s_11(X), Y, R))
mult_3_in_gga3(s_11(X), Y, R) -> if_mult_3_in_1_gga4(X, Y, R, mult_3_in_gga3(X, Y, Z))
mult_3_in_gga3(0_0, Y, 0_0) -> mult_3_out_gga3(0_0, Y, 0_0)
if_mult_3_in_1_gga4(X, Y, R, mult_3_out_gga3(X, Y, Z)) -> if_mult_3_in_2_gga5(X, Y, R, Z, add_3_in_gga3(Y, Z, R))
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_mult_3_in_2_gga5(X, Y, R, Z, add_3_out_gga3(Y, Z, R)) -> mult_3_out_gga3(s_11(X), Y, R)
if_factorial_2_in_2_ga4(X, R, Y, mult_3_out_gga3(s_11(X), Y, R)) -> factorial_2_out_ga2(s_11(X), R)
↳ PROLOG
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
MULT_3_IN_GGA3(s_11(X), Y, R) -> MULT_3_IN_GGA3(X, Y, Z)
↳ PROLOG
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
MULT_3_IN_GGA2(s_11(X), Y) -> MULT_3_IN_GGA2(X, Y)
From the DPs we obtained the following set of size-change graphs:
↳ PROLOG
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
FACTORIAL_2_IN_GA2(s_11(X), R) -> FACTORIAL_2_IN_GA2(X, Y)
factorial_2_in_ga2(s_11(X), R) -> if_factorial_2_in_1_ga3(X, R, factorial_2_in_ga2(X, Y))
factorial_2_in_ga2(0_0, s_11(0_0)) -> factorial_2_out_ga2(0_0, s_11(0_0))
if_factorial_2_in_1_ga3(X, R, factorial_2_out_ga2(X, Y)) -> if_factorial_2_in_2_ga4(X, R, Y, mult_3_in_gga3(s_11(X), Y, R))
mult_3_in_gga3(s_11(X), Y, R) -> if_mult_3_in_1_gga4(X, Y, R, mult_3_in_gga3(X, Y, Z))
mult_3_in_gga3(0_0, Y, 0_0) -> mult_3_out_gga3(0_0, Y, 0_0)
if_mult_3_in_1_gga4(X, Y, R, mult_3_out_gga3(X, Y, Z)) -> if_mult_3_in_2_gga5(X, Y, R, Z, add_3_in_gga3(Y, Z, R))
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_mult_3_in_2_gga5(X, Y, R, Z, add_3_out_gga3(Y, Z, R)) -> mult_3_out_gga3(s_11(X), Y, R)
if_factorial_2_in_2_ga4(X, R, Y, mult_3_out_gga3(s_11(X), Y, R)) -> factorial_2_out_ga2(s_11(X), R)
↳ PROLOG
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
FACTORIAL_2_IN_GA2(s_11(X), R) -> FACTORIAL_2_IN_GA2(X, Y)
↳ PROLOG
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
FACTORIAL_2_IN_GA1(s_11(X)) -> FACTORIAL_2_IN_GA1(X)
From the DPs we obtained the following set of size-change graphs: