↳ PROLOG
↳ UnrequestedClauseRemoverProof
The clauses
append13({}0, X, X).
append13(.2(X, Y), U, .2(X, Z)) :- append13(Y, U, Z).
append23({}0, X, X).
append23(.2(X, Y), U, .2(X, Z)) :- append23(Y, U, Z).
can be ignored, as they are not needed by any of the given querys.
Deleting these clauses results in the following prolog program:
append33({}0, X, X).
append33(.2(X, Y), U, .2(X, Z)) :- append33(Y, U, Z).
↳ PROLOG
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
With regard to the inferred argument filtering the predicates were used in the following modes:
append33: (f,f,b)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
append3_3_in_aag3([]_0, X, X) -> append3_3_out_aag3([]_0, X, X)
append3_3_in_aag3(._22(X, Y), U, ._22(X, Z)) -> if_append3_3_in_1_aag5(X, Y, U, Z, append3_3_in_aag3(Y, U, Z))
if_append3_3_in_1_aag5(X, Y, U, Z, append3_3_out_aag3(Y, U, Z)) -> append3_3_out_aag3(._22(X, Y), U, ._22(X, Z))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG
↳ PROLOG
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
append3_3_in_aag3([]_0, X, X) -> append3_3_out_aag3([]_0, X, X)
append3_3_in_aag3(._22(X, Y), U, ._22(X, Z)) -> if_append3_3_in_1_aag5(X, Y, U, Z, append3_3_in_aag3(Y, U, Z))
if_append3_3_in_1_aag5(X, Y, U, Z, append3_3_out_aag3(Y, U, Z)) -> append3_3_out_aag3(._22(X, Y), U, ._22(X, Z))
APPEND3_3_IN_AAG3(._22(X, Y), U, ._22(X, Z)) -> IF_APPEND3_3_IN_1_AAG5(X, Y, U, Z, append3_3_in_aag3(Y, U, Z))
APPEND3_3_IN_AAG3(._22(X, Y), U, ._22(X, Z)) -> APPEND3_3_IN_AAG3(Y, U, Z)
append3_3_in_aag3([]_0, X, X) -> append3_3_out_aag3([]_0, X, X)
append3_3_in_aag3(._22(X, Y), U, ._22(X, Z)) -> if_append3_3_in_1_aag5(X, Y, U, Z, append3_3_in_aag3(Y, U, Z))
if_append3_3_in_1_aag5(X, Y, U, Z, append3_3_out_aag3(Y, U, Z)) -> append3_3_out_aag3(._22(X, Y), U, ._22(X, Z))
↳ PROLOG
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
APPEND3_3_IN_AAG3(._22(X, Y), U, ._22(X, Z)) -> IF_APPEND3_3_IN_1_AAG5(X, Y, U, Z, append3_3_in_aag3(Y, U, Z))
APPEND3_3_IN_AAG3(._22(X, Y), U, ._22(X, Z)) -> APPEND3_3_IN_AAG3(Y, U, Z)
append3_3_in_aag3([]_0, X, X) -> append3_3_out_aag3([]_0, X, X)
append3_3_in_aag3(._22(X, Y), U, ._22(X, Z)) -> if_append3_3_in_1_aag5(X, Y, U, Z, append3_3_in_aag3(Y, U, Z))
if_append3_3_in_1_aag5(X, Y, U, Z, append3_3_out_aag3(Y, U, Z)) -> append3_3_out_aag3(._22(X, Y), U, ._22(X, Z))
↳ PROLOG
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
APPEND3_3_IN_AAG3(._22(X, Y), U, ._22(X, Z)) -> APPEND3_3_IN_AAG3(Y, U, Z)
append3_3_in_aag3([]_0, X, X) -> append3_3_out_aag3([]_0, X, X)
append3_3_in_aag3(._22(X, Y), U, ._22(X, Z)) -> if_append3_3_in_1_aag5(X, Y, U, Z, append3_3_in_aag3(Y, U, Z))
if_append3_3_in_1_aag5(X, Y, U, Z, append3_3_out_aag3(Y, U, Z)) -> append3_3_out_aag3(._22(X, Y), U, ._22(X, Z))
↳ PROLOG
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
APPEND3_3_IN_AAG3(._22(X, Y), U, ._22(X, Z)) -> APPEND3_3_IN_AAG3(Y, U, Z)
↳ PROLOG
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
APPEND3_3_IN_AAG1(._22(X, Z)) -> APPEND3_3_IN_AAG1(Z)
From the DPs we obtained the following set of size-change graphs: