(0) Obligation:
Clauses:
p(X, Y, Z) :- ','(=(X, Y), ','(=(Z, 1), !)).
p(X, Y, Z) :- ','(=(Z, 1), ','(=(Y, X), p(X, Y, Z))).
=(X, X).
Queries:
p(a,a,a).
(1) CutEliminatorProof (SOUND transformation)
Eliminated all cuts by simply ignoring them[PROLOG].
(2) Obligation:
Clauses:
p(X, Y, Z) :- ','(=(X, Y), =(Z, 1)).
p(X, Y, Z) :- ','(=(Z, 1), ','(=(Y, X), p(X, Y, Z))).
=(X, X).
Queries:
p(a,a,a).
(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:
p_in: (f,f,f) (f,f,b)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
p_in_aaa(X, Y, Z) → U1_aaa(X, Y, Z, =_in_aa(X, Y))
=_in_aa(X, X) → =_out_aa(X, X)
U1_aaa(X, Y, Z, =_out_aa(X, Y)) → U2_aaa(X, Y, Z, =_in_ag(Z, 1))
=_in_ag(X, X) → =_out_ag(X, X)
U2_aaa(X, Y, Z, =_out_ag(Z, 1)) → p_out_aaa(X, Y, Z)
p_in_aaa(X, Y, Z) → U3_aaa(X, Y, Z, =_in_ag(Z, 1))
U3_aaa(X, Y, Z, =_out_ag(Z, 1)) → U4_aaa(X, Y, Z, =_in_aa(Y, X))
U4_aaa(X, Y, Z, =_out_aa(Y, X)) → U5_aaa(X, Y, Z, p_in_aag(X, Y, Z))
p_in_aag(X, Y, Z) → U1_aag(X, Y, Z, =_in_aa(X, Y))
U1_aag(X, Y, Z, =_out_aa(X, Y)) → U2_aag(X, Y, Z, =_in_gg(Z, 1))
=_in_gg(X, X) → =_out_gg(X, X)
U2_aag(X, Y, Z, =_out_gg(Z, 1)) → p_out_aag(X, Y, Z)
p_in_aag(X, Y, Z) → U3_aag(X, Y, Z, =_in_gg(Z, 1))
U3_aag(X, Y, Z, =_out_gg(Z, 1)) → U4_aag(X, Y, Z, =_in_aa(Y, X))
U4_aag(X, Y, Z, =_out_aa(Y, X)) → U5_aag(X, Y, Z, p_in_aag(X, Y, Z))
U5_aag(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aag(X, Y, Z)
U5_aaa(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aaa(X, Y, Z)
The argument filtering Pi contains the following mapping:
p_in_aaa(
x1,
x2,
x3) =
p_in_aaa
U1_aaa(
x1,
x2,
x3,
x4) =
U1_aaa(
x4)
=_in_aa(
x1,
x2) =
=_in_aa
=_out_aa(
x1,
x2) =
=_out_aa
U2_aaa(
x1,
x2,
x3,
x4) =
U2_aaa(
x4)
=_in_ag(
x1,
x2) =
=_in_ag(
x2)
=_out_ag(
x1,
x2) =
=_out_ag(
x1)
1 =
1
p_out_aaa(
x1,
x2,
x3) =
p_out_aaa(
x3)
U3_aaa(
x1,
x2,
x3,
x4) =
U3_aaa(
x4)
U4_aaa(
x1,
x2,
x3,
x4) =
U4_aaa(
x3,
x4)
U5_aaa(
x1,
x2,
x3,
x4) =
U5_aaa(
x3,
x4)
p_in_aag(
x1,
x2,
x3) =
p_in_aag(
x3)
U1_aag(
x1,
x2,
x3,
x4) =
U1_aag(
x3,
x4)
U2_aag(
x1,
x2,
x3,
x4) =
U2_aag(
x4)
=_in_gg(
x1,
x2) =
=_in_gg(
x1,
x2)
=_out_gg(
x1,
x2) =
=_out_gg
p_out_aag(
x1,
x2,
x3) =
p_out_aag
U3_aag(
x1,
x2,
x3,
x4) =
U3_aag(
x3,
x4)
U4_aag(
x1,
x2,
x3,
x4) =
U4_aag(
x3,
x4)
U5_aag(
x1,
x2,
x3,
x4) =
U5_aag(
x4)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(4) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
p_in_aaa(X, Y, Z) → U1_aaa(X, Y, Z, =_in_aa(X, Y))
=_in_aa(X, X) → =_out_aa(X, X)
U1_aaa(X, Y, Z, =_out_aa(X, Y)) → U2_aaa(X, Y, Z, =_in_ag(Z, 1))
=_in_ag(X, X) → =_out_ag(X, X)
U2_aaa(X, Y, Z, =_out_ag(Z, 1)) → p_out_aaa(X, Y, Z)
p_in_aaa(X, Y, Z) → U3_aaa(X, Y, Z, =_in_ag(Z, 1))
U3_aaa(X, Y, Z, =_out_ag(Z, 1)) → U4_aaa(X, Y, Z, =_in_aa(Y, X))
U4_aaa(X, Y, Z, =_out_aa(Y, X)) → U5_aaa(X, Y, Z, p_in_aag(X, Y, Z))
p_in_aag(X, Y, Z) → U1_aag(X, Y, Z, =_in_aa(X, Y))
U1_aag(X, Y, Z, =_out_aa(X, Y)) → U2_aag(X, Y, Z, =_in_gg(Z, 1))
=_in_gg(X, X) → =_out_gg(X, X)
U2_aag(X, Y, Z, =_out_gg(Z, 1)) → p_out_aag(X, Y, Z)
p_in_aag(X, Y, Z) → U3_aag(X, Y, Z, =_in_gg(Z, 1))
U3_aag(X, Y, Z, =_out_gg(Z, 1)) → U4_aag(X, Y, Z, =_in_aa(Y, X))
U4_aag(X, Y, Z, =_out_aa(Y, X)) → U5_aag(X, Y, Z, p_in_aag(X, Y, Z))
U5_aag(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aag(X, Y, Z)
U5_aaa(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aaa(X, Y, Z)
The argument filtering Pi contains the following mapping:
p_in_aaa(
x1,
x2,
x3) =
p_in_aaa
U1_aaa(
x1,
x2,
x3,
x4) =
U1_aaa(
x4)
=_in_aa(
x1,
x2) =
=_in_aa
=_out_aa(
x1,
x2) =
=_out_aa
U2_aaa(
x1,
x2,
x3,
x4) =
U2_aaa(
x4)
=_in_ag(
x1,
x2) =
=_in_ag(
x2)
=_out_ag(
x1,
x2) =
=_out_ag(
x1)
1 =
1
p_out_aaa(
x1,
x2,
x3) =
p_out_aaa(
x3)
U3_aaa(
x1,
x2,
x3,
x4) =
U3_aaa(
x4)
U4_aaa(
x1,
x2,
x3,
x4) =
U4_aaa(
x3,
x4)
U5_aaa(
x1,
x2,
x3,
x4) =
U5_aaa(
x3,
x4)
p_in_aag(
x1,
x2,
x3) =
p_in_aag(
x3)
U1_aag(
x1,
x2,
x3,
x4) =
U1_aag(
x3,
x4)
U2_aag(
x1,
x2,
x3,
x4) =
U2_aag(
x4)
=_in_gg(
x1,
x2) =
=_in_gg(
x1,
x2)
=_out_gg(
x1,
x2) =
=_out_gg
p_out_aag(
x1,
x2,
x3) =
p_out_aag
U3_aag(
x1,
x2,
x3,
x4) =
U3_aag(
x3,
x4)
U4_aag(
x1,
x2,
x3,
x4) =
U4_aag(
x3,
x4)
U5_aag(
x1,
x2,
x3,
x4) =
U5_aag(
x4)
(5) 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:
P_IN_AAA(X, Y, Z) → U1_AAA(X, Y, Z, =_in_aa(X, Y))
P_IN_AAA(X, Y, Z) → =_IN_AA(X, Y)
U1_AAA(X, Y, Z, =_out_aa(X, Y)) → U2_AAA(X, Y, Z, =_in_ag(Z, 1))
U1_AAA(X, Y, Z, =_out_aa(X, Y)) → =_IN_AG(Z, 1)
P_IN_AAA(X, Y, Z) → U3_AAA(X, Y, Z, =_in_ag(Z, 1))
P_IN_AAA(X, Y, Z) → =_IN_AG(Z, 1)
U3_AAA(X, Y, Z, =_out_ag(Z, 1)) → U4_AAA(X, Y, Z, =_in_aa(Y, X))
U3_AAA(X, Y, Z, =_out_ag(Z, 1)) → =_IN_AA(Y, X)
U4_AAA(X, Y, Z, =_out_aa(Y, X)) → U5_AAA(X, Y, Z, p_in_aag(X, Y, Z))
U4_AAA(X, Y, Z, =_out_aa(Y, X)) → P_IN_AAG(X, Y, Z)
P_IN_AAG(X, Y, Z) → U1_AAG(X, Y, Z, =_in_aa(X, Y))
P_IN_AAG(X, Y, Z) → =_IN_AA(X, Y)
U1_AAG(X, Y, Z, =_out_aa(X, Y)) → U2_AAG(X, Y, Z, =_in_gg(Z, 1))
U1_AAG(X, Y, Z, =_out_aa(X, Y)) → =_IN_GG(Z, 1)
P_IN_AAG(X, Y, Z) → U3_AAG(X, Y, Z, =_in_gg(Z, 1))
P_IN_AAG(X, Y, Z) → =_IN_GG(Z, 1)
U3_AAG(X, Y, Z, =_out_gg(Z, 1)) → U4_AAG(X, Y, Z, =_in_aa(Y, X))
U3_AAG(X, Y, Z, =_out_gg(Z, 1)) → =_IN_AA(Y, X)
U4_AAG(X, Y, Z, =_out_aa(Y, X)) → U5_AAG(X, Y, Z, p_in_aag(X, Y, Z))
U4_AAG(X, Y, Z, =_out_aa(Y, X)) → P_IN_AAG(X, Y, Z)
The TRS R consists of the following rules:
p_in_aaa(X, Y, Z) → U1_aaa(X, Y, Z, =_in_aa(X, Y))
=_in_aa(X, X) → =_out_aa(X, X)
U1_aaa(X, Y, Z, =_out_aa(X, Y)) → U2_aaa(X, Y, Z, =_in_ag(Z, 1))
=_in_ag(X, X) → =_out_ag(X, X)
U2_aaa(X, Y, Z, =_out_ag(Z, 1)) → p_out_aaa(X, Y, Z)
p_in_aaa(X, Y, Z) → U3_aaa(X, Y, Z, =_in_ag(Z, 1))
U3_aaa(X, Y, Z, =_out_ag(Z, 1)) → U4_aaa(X, Y, Z, =_in_aa(Y, X))
U4_aaa(X, Y, Z, =_out_aa(Y, X)) → U5_aaa(X, Y, Z, p_in_aag(X, Y, Z))
p_in_aag(X, Y, Z) → U1_aag(X, Y, Z, =_in_aa(X, Y))
U1_aag(X, Y, Z, =_out_aa(X, Y)) → U2_aag(X, Y, Z, =_in_gg(Z, 1))
=_in_gg(X, X) → =_out_gg(X, X)
U2_aag(X, Y, Z, =_out_gg(Z, 1)) → p_out_aag(X, Y, Z)
p_in_aag(X, Y, Z) → U3_aag(X, Y, Z, =_in_gg(Z, 1))
U3_aag(X, Y, Z, =_out_gg(Z, 1)) → U4_aag(X, Y, Z, =_in_aa(Y, X))
U4_aag(X, Y, Z, =_out_aa(Y, X)) → U5_aag(X, Y, Z, p_in_aag(X, Y, Z))
U5_aag(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aag(X, Y, Z)
U5_aaa(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aaa(X, Y, Z)
The argument filtering Pi contains the following mapping:
p_in_aaa(
x1,
x2,
x3) =
p_in_aaa
U1_aaa(
x1,
x2,
x3,
x4) =
U1_aaa(
x4)
=_in_aa(
x1,
x2) =
=_in_aa
=_out_aa(
x1,
x2) =
=_out_aa
U2_aaa(
x1,
x2,
x3,
x4) =
U2_aaa(
x4)
=_in_ag(
x1,
x2) =
=_in_ag(
x2)
=_out_ag(
x1,
x2) =
=_out_ag(
x1)
1 =
1
p_out_aaa(
x1,
x2,
x3) =
p_out_aaa(
x3)
U3_aaa(
x1,
x2,
x3,
x4) =
U3_aaa(
x4)
U4_aaa(
x1,
x2,
x3,
x4) =
U4_aaa(
x3,
x4)
U5_aaa(
x1,
x2,
x3,
x4) =
U5_aaa(
x3,
x4)
p_in_aag(
x1,
x2,
x3) =
p_in_aag(
x3)
U1_aag(
x1,
x2,
x3,
x4) =
U1_aag(
x3,
x4)
U2_aag(
x1,
x2,
x3,
x4) =
U2_aag(
x4)
=_in_gg(
x1,
x2) =
=_in_gg(
x1,
x2)
=_out_gg(
x1,
x2) =
=_out_gg
p_out_aag(
x1,
x2,
x3) =
p_out_aag
U3_aag(
x1,
x2,
x3,
x4) =
U3_aag(
x3,
x4)
U4_aag(
x1,
x2,
x3,
x4) =
U4_aag(
x3,
x4)
U5_aag(
x1,
x2,
x3,
x4) =
U5_aag(
x4)
P_IN_AAA(
x1,
x2,
x3) =
P_IN_AAA
U1_AAA(
x1,
x2,
x3,
x4) =
U1_AAA(
x4)
=_IN_AA(
x1,
x2) =
=_IN_AA
U2_AAA(
x1,
x2,
x3,
x4) =
U2_AAA(
x4)
=_IN_AG(
x1,
x2) =
=_IN_AG(
x2)
U3_AAA(
x1,
x2,
x3,
x4) =
U3_AAA(
x4)
U4_AAA(
x1,
x2,
x3,
x4) =
U4_AAA(
x3,
x4)
U5_AAA(
x1,
x2,
x3,
x4) =
U5_AAA(
x3,
x4)
P_IN_AAG(
x1,
x2,
x3) =
P_IN_AAG(
x3)
U1_AAG(
x1,
x2,
x3,
x4) =
U1_AAG(
x3,
x4)
U2_AAG(
x1,
x2,
x3,
x4) =
U2_AAG(
x4)
=_IN_GG(
x1,
x2) =
=_IN_GG(
x1,
x2)
U3_AAG(
x1,
x2,
x3,
x4) =
U3_AAG(
x3,
x4)
U4_AAG(
x1,
x2,
x3,
x4) =
U4_AAG(
x3,
x4)
U5_AAG(
x1,
x2,
x3,
x4) =
U5_AAG(
x4)
We have to consider all (P,R,Pi)-chains
(6) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
P_IN_AAA(X, Y, Z) → U1_AAA(X, Y, Z, =_in_aa(X, Y))
P_IN_AAA(X, Y, Z) → =_IN_AA(X, Y)
U1_AAA(X, Y, Z, =_out_aa(X, Y)) → U2_AAA(X, Y, Z, =_in_ag(Z, 1))
U1_AAA(X, Y, Z, =_out_aa(X, Y)) → =_IN_AG(Z, 1)
P_IN_AAA(X, Y, Z) → U3_AAA(X, Y, Z, =_in_ag(Z, 1))
P_IN_AAA(X, Y, Z) → =_IN_AG(Z, 1)
U3_AAA(X, Y, Z, =_out_ag(Z, 1)) → U4_AAA(X, Y, Z, =_in_aa(Y, X))
U3_AAA(X, Y, Z, =_out_ag(Z, 1)) → =_IN_AA(Y, X)
U4_AAA(X, Y, Z, =_out_aa(Y, X)) → U5_AAA(X, Y, Z, p_in_aag(X, Y, Z))
U4_AAA(X, Y, Z, =_out_aa(Y, X)) → P_IN_AAG(X, Y, Z)
P_IN_AAG(X, Y, Z) → U1_AAG(X, Y, Z, =_in_aa(X, Y))
P_IN_AAG(X, Y, Z) → =_IN_AA(X, Y)
U1_AAG(X, Y, Z, =_out_aa(X, Y)) → U2_AAG(X, Y, Z, =_in_gg(Z, 1))
U1_AAG(X, Y, Z, =_out_aa(X, Y)) → =_IN_GG(Z, 1)
P_IN_AAG(X, Y, Z) → U3_AAG(X, Y, Z, =_in_gg(Z, 1))
P_IN_AAG(X, Y, Z) → =_IN_GG(Z, 1)
U3_AAG(X, Y, Z, =_out_gg(Z, 1)) → U4_AAG(X, Y, Z, =_in_aa(Y, X))
U3_AAG(X, Y, Z, =_out_gg(Z, 1)) → =_IN_AA(Y, X)
U4_AAG(X, Y, Z, =_out_aa(Y, X)) → U5_AAG(X, Y, Z, p_in_aag(X, Y, Z))
U4_AAG(X, Y, Z, =_out_aa(Y, X)) → P_IN_AAG(X, Y, Z)
The TRS R consists of the following rules:
p_in_aaa(X, Y, Z) → U1_aaa(X, Y, Z, =_in_aa(X, Y))
=_in_aa(X, X) → =_out_aa(X, X)
U1_aaa(X, Y, Z, =_out_aa(X, Y)) → U2_aaa(X, Y, Z, =_in_ag(Z, 1))
=_in_ag(X, X) → =_out_ag(X, X)
U2_aaa(X, Y, Z, =_out_ag(Z, 1)) → p_out_aaa(X, Y, Z)
p_in_aaa(X, Y, Z) → U3_aaa(X, Y, Z, =_in_ag(Z, 1))
U3_aaa(X, Y, Z, =_out_ag(Z, 1)) → U4_aaa(X, Y, Z, =_in_aa(Y, X))
U4_aaa(X, Y, Z, =_out_aa(Y, X)) → U5_aaa(X, Y, Z, p_in_aag(X, Y, Z))
p_in_aag(X, Y, Z) → U1_aag(X, Y, Z, =_in_aa(X, Y))
U1_aag(X, Y, Z, =_out_aa(X, Y)) → U2_aag(X, Y, Z, =_in_gg(Z, 1))
=_in_gg(X, X) → =_out_gg(X, X)
U2_aag(X, Y, Z, =_out_gg(Z, 1)) → p_out_aag(X, Y, Z)
p_in_aag(X, Y, Z) → U3_aag(X, Y, Z, =_in_gg(Z, 1))
U3_aag(X, Y, Z, =_out_gg(Z, 1)) → U4_aag(X, Y, Z, =_in_aa(Y, X))
U4_aag(X, Y, Z, =_out_aa(Y, X)) → U5_aag(X, Y, Z, p_in_aag(X, Y, Z))
U5_aag(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aag(X, Y, Z)
U5_aaa(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aaa(X, Y, Z)
The argument filtering Pi contains the following mapping:
p_in_aaa(
x1,
x2,
x3) =
p_in_aaa
U1_aaa(
x1,
x2,
x3,
x4) =
U1_aaa(
x4)
=_in_aa(
x1,
x2) =
=_in_aa
=_out_aa(
x1,
x2) =
=_out_aa
U2_aaa(
x1,
x2,
x3,
x4) =
U2_aaa(
x4)
=_in_ag(
x1,
x2) =
=_in_ag(
x2)
=_out_ag(
x1,
x2) =
=_out_ag(
x1)
1 =
1
p_out_aaa(
x1,
x2,
x3) =
p_out_aaa(
x3)
U3_aaa(
x1,
x2,
x3,
x4) =
U3_aaa(
x4)
U4_aaa(
x1,
x2,
x3,
x4) =
U4_aaa(
x3,
x4)
U5_aaa(
x1,
x2,
x3,
x4) =
U5_aaa(
x3,
x4)
p_in_aag(
x1,
x2,
x3) =
p_in_aag(
x3)
U1_aag(
x1,
x2,
x3,
x4) =
U1_aag(
x3,
x4)
U2_aag(
x1,
x2,
x3,
x4) =
U2_aag(
x4)
=_in_gg(
x1,
x2) =
=_in_gg(
x1,
x2)
=_out_gg(
x1,
x2) =
=_out_gg
p_out_aag(
x1,
x2,
x3) =
p_out_aag
U3_aag(
x1,
x2,
x3,
x4) =
U3_aag(
x3,
x4)
U4_aag(
x1,
x2,
x3,
x4) =
U4_aag(
x3,
x4)
U5_aag(
x1,
x2,
x3,
x4) =
U5_aag(
x4)
P_IN_AAA(
x1,
x2,
x3) =
P_IN_AAA
U1_AAA(
x1,
x2,
x3,
x4) =
U1_AAA(
x4)
=_IN_AA(
x1,
x2) =
=_IN_AA
U2_AAA(
x1,
x2,
x3,
x4) =
U2_AAA(
x4)
=_IN_AG(
x1,
x2) =
=_IN_AG(
x2)
U3_AAA(
x1,
x2,
x3,
x4) =
U3_AAA(
x4)
U4_AAA(
x1,
x2,
x3,
x4) =
U4_AAA(
x3,
x4)
U5_AAA(
x1,
x2,
x3,
x4) =
U5_AAA(
x3,
x4)
P_IN_AAG(
x1,
x2,
x3) =
P_IN_AAG(
x3)
U1_AAG(
x1,
x2,
x3,
x4) =
U1_AAG(
x3,
x4)
U2_AAG(
x1,
x2,
x3,
x4) =
U2_AAG(
x4)
=_IN_GG(
x1,
x2) =
=_IN_GG(
x1,
x2)
U3_AAG(
x1,
x2,
x3,
x4) =
U3_AAG(
x3,
x4)
U4_AAG(
x1,
x2,
x3,
x4) =
U4_AAG(
x3,
x4)
U5_AAG(
x1,
x2,
x3,
x4) =
U5_AAG(
x4)
We have to consider all (P,R,Pi)-chains
(7) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 17 less nodes.
(8) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
P_IN_AAG(X, Y, Z) → U3_AAG(X, Y, Z, =_in_gg(Z, 1))
U3_AAG(X, Y, Z, =_out_gg(Z, 1)) → U4_AAG(X, Y, Z, =_in_aa(Y, X))
U4_AAG(X, Y, Z, =_out_aa(Y, X)) → P_IN_AAG(X, Y, Z)
The TRS R consists of the following rules:
p_in_aaa(X, Y, Z) → U1_aaa(X, Y, Z, =_in_aa(X, Y))
=_in_aa(X, X) → =_out_aa(X, X)
U1_aaa(X, Y, Z, =_out_aa(X, Y)) → U2_aaa(X, Y, Z, =_in_ag(Z, 1))
=_in_ag(X, X) → =_out_ag(X, X)
U2_aaa(X, Y, Z, =_out_ag(Z, 1)) → p_out_aaa(X, Y, Z)
p_in_aaa(X, Y, Z) → U3_aaa(X, Y, Z, =_in_ag(Z, 1))
U3_aaa(X, Y, Z, =_out_ag(Z, 1)) → U4_aaa(X, Y, Z, =_in_aa(Y, X))
U4_aaa(X, Y, Z, =_out_aa(Y, X)) → U5_aaa(X, Y, Z, p_in_aag(X, Y, Z))
p_in_aag(X, Y, Z) → U1_aag(X, Y, Z, =_in_aa(X, Y))
U1_aag(X, Y, Z, =_out_aa(X, Y)) → U2_aag(X, Y, Z, =_in_gg(Z, 1))
=_in_gg(X, X) → =_out_gg(X, X)
U2_aag(X, Y, Z, =_out_gg(Z, 1)) → p_out_aag(X, Y, Z)
p_in_aag(X, Y, Z) → U3_aag(X, Y, Z, =_in_gg(Z, 1))
U3_aag(X, Y, Z, =_out_gg(Z, 1)) → U4_aag(X, Y, Z, =_in_aa(Y, X))
U4_aag(X, Y, Z, =_out_aa(Y, X)) → U5_aag(X, Y, Z, p_in_aag(X, Y, Z))
U5_aag(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aag(X, Y, Z)
U5_aaa(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aaa(X, Y, Z)
The argument filtering Pi contains the following mapping:
p_in_aaa(
x1,
x2,
x3) =
p_in_aaa
U1_aaa(
x1,
x2,
x3,
x4) =
U1_aaa(
x4)
=_in_aa(
x1,
x2) =
=_in_aa
=_out_aa(
x1,
x2) =
=_out_aa
U2_aaa(
x1,
x2,
x3,
x4) =
U2_aaa(
x4)
=_in_ag(
x1,
x2) =
=_in_ag(
x2)
=_out_ag(
x1,
x2) =
=_out_ag(
x1)
1 =
1
p_out_aaa(
x1,
x2,
x3) =
p_out_aaa(
x3)
U3_aaa(
x1,
x2,
x3,
x4) =
U3_aaa(
x4)
U4_aaa(
x1,
x2,
x3,
x4) =
U4_aaa(
x3,
x4)
U5_aaa(
x1,
x2,
x3,
x4) =
U5_aaa(
x3,
x4)
p_in_aag(
x1,
x2,
x3) =
p_in_aag(
x3)
U1_aag(
x1,
x2,
x3,
x4) =
U1_aag(
x3,
x4)
U2_aag(
x1,
x2,
x3,
x4) =
U2_aag(
x4)
=_in_gg(
x1,
x2) =
=_in_gg(
x1,
x2)
=_out_gg(
x1,
x2) =
=_out_gg
p_out_aag(
x1,
x2,
x3) =
p_out_aag
U3_aag(
x1,
x2,
x3,
x4) =
U3_aag(
x3,
x4)
U4_aag(
x1,
x2,
x3,
x4) =
U4_aag(
x3,
x4)
U5_aag(
x1,
x2,
x3,
x4) =
U5_aag(
x4)
P_IN_AAG(
x1,
x2,
x3) =
P_IN_AAG(
x3)
U3_AAG(
x1,
x2,
x3,
x4) =
U3_AAG(
x3,
x4)
U4_AAG(
x1,
x2,
x3,
x4) =
U4_AAG(
x3,
x4)
We have to consider all (P,R,Pi)-chains
(9) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(10) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
P_IN_AAG(X, Y, Z) → U3_AAG(X, Y, Z, =_in_gg(Z, 1))
U3_AAG(X, Y, Z, =_out_gg(Z, 1)) → U4_AAG(X, Y, Z, =_in_aa(Y, X))
U4_AAG(X, Y, Z, =_out_aa(Y, X)) → P_IN_AAG(X, Y, Z)
The TRS R consists of the following rules:
=_in_gg(X, X) → =_out_gg(X, X)
=_in_aa(X, X) → =_out_aa(X, X)
The argument filtering Pi contains the following mapping:
=_in_aa(
x1,
x2) =
=_in_aa
=_out_aa(
x1,
x2) =
=_out_aa
1 =
1
=_in_gg(
x1,
x2) =
=_in_gg(
x1,
x2)
=_out_gg(
x1,
x2) =
=_out_gg
P_IN_AAG(
x1,
x2,
x3) =
P_IN_AAG(
x3)
U3_AAG(
x1,
x2,
x3,
x4) =
U3_AAG(
x3,
x4)
U4_AAG(
x1,
x2,
x3,
x4) =
U4_AAG(
x3,
x4)
We have to consider all (P,R,Pi)-chains
(11) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(12) Obligation:
Q DP problem:
The TRS P consists of the following rules:
P_IN_AAG(Z) → U3_AAG(Z, =_in_gg(Z, 1))
U3_AAG(Z, =_out_gg) → U4_AAG(Z, =_in_aa)
U4_AAG(Z, =_out_aa) → P_IN_AAG(Z)
The TRS R consists of the following rules:
=_in_gg(X, X) → =_out_gg
=_in_aa → =_out_aa
The set Q consists of the following terms:
=_in_gg(x0, x1)
=_in_aa
We have to consider all (P,Q,R)-chains.
(13) Rewriting (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
U3_AAG(
Z,
=_out_gg) →
U4_AAG(
Z,
=_in_aa) at position [1] we obtained the following new rules [LPAR04]:
U3_AAG(Z, =_out_gg) → U4_AAG(Z, =_out_aa)
(14) Obligation:
Q DP problem:
The TRS P consists of the following rules:
P_IN_AAG(Z) → U3_AAG(Z, =_in_gg(Z, 1))
U4_AAG(Z, =_out_aa) → P_IN_AAG(Z)
U3_AAG(Z, =_out_gg) → U4_AAG(Z, =_out_aa)
The TRS R consists of the following rules:
=_in_gg(X, X) → =_out_gg
=_in_aa → =_out_aa
The set Q consists of the following terms:
=_in_gg(x0, x1)
=_in_aa
We have to consider all (P,Q,R)-chains.
(15) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(16) Obligation:
Q DP problem:
The TRS P consists of the following rules:
P_IN_AAG(Z) → U3_AAG(Z, =_in_gg(Z, 1))
U4_AAG(Z, =_out_aa) → P_IN_AAG(Z)
U3_AAG(Z, =_out_gg) → U4_AAG(Z, =_out_aa)
The TRS R consists of the following rules:
=_in_gg(X, X) → =_out_gg
The set Q consists of the following terms:
=_in_gg(x0, x1)
=_in_aa
We have to consider all (P,Q,R)-chains.
(17) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
=_in_aa
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
P_IN_AAG(Z) → U3_AAG(Z, =_in_gg(Z, 1))
U4_AAG(Z, =_out_aa) → P_IN_AAG(Z)
U3_AAG(Z, =_out_gg) → U4_AAG(Z, =_out_aa)
The TRS R consists of the following rules:
=_in_gg(X, X) → =_out_gg
The set Q consists of the following terms:
=_in_gg(x0, x1)
We have to consider all (P,Q,R)-chains.
(19) Narrowing (SOUND transformation)
By narrowing [LPAR04] the rule
P_IN_AAG(
Z) →
U3_AAG(
Z,
=_in_gg(
Z,
1)) at position [1] we obtained the following new rules [LPAR04]:
P_IN_AAG(1) → U3_AAG(1, =_out_gg)
(20) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_AAG(Z, =_out_aa) → P_IN_AAG(Z)
U3_AAG(Z, =_out_gg) → U4_AAG(Z, =_out_aa)
P_IN_AAG(1) → U3_AAG(1, =_out_gg)
The TRS R consists of the following rules:
=_in_gg(X, X) → =_out_gg
The set Q consists of the following terms:
=_in_gg(x0, x1)
We have to consider all (P,Q,R)-chains.
(21) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(22) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_AAG(Z, =_out_aa) → P_IN_AAG(Z)
U3_AAG(Z, =_out_gg) → U4_AAG(Z, =_out_aa)
P_IN_AAG(1) → U3_AAG(1, =_out_gg)
R is empty.
The set Q consists of the following terms:
=_in_gg(x0, x1)
We have to consider all (P,Q,R)-chains.
(23) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
=_in_gg(x0, x1)
(24) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_AAG(Z, =_out_aa) → P_IN_AAG(Z)
U3_AAG(Z, =_out_gg) → U4_AAG(Z, =_out_aa)
P_IN_AAG(1) → U3_AAG(1, =_out_gg)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(25) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U3_AAG(
Z,
=_out_gg) →
U4_AAG(
Z,
=_out_aa) we obtained the following new rules [LPAR04]:
U3_AAG(1, =_out_gg) → U4_AAG(1, =_out_aa)
(26) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_AAG(Z, =_out_aa) → P_IN_AAG(Z)
P_IN_AAG(1) → U3_AAG(1, =_out_gg)
U3_AAG(1, =_out_gg) → U4_AAG(1, =_out_aa)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(27) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U4_AAG(
Z,
=_out_aa) →
P_IN_AAG(
Z) we obtained the following new rules [LPAR04]:
U4_AAG(1, =_out_aa) → P_IN_AAG(1)
(28) Obligation:
Q DP problem:
The TRS P consists of the following rules:
P_IN_AAG(1) → U3_AAG(1, =_out_gg)
U3_AAG(1, =_out_gg) → U4_AAG(1, =_out_aa)
U4_AAG(1, =_out_aa) → P_IN_AAG(1)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(29) NonTerminationProof (EQUIVALENT transformation)
We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:
s =
U3_AAG(
1,
=_out_gg) evaluates to t =
U3_AAG(
1,
=_out_gg)
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Semiunifier: [ ]
- Matcher: [ ]
Rewriting sequenceU3_AAG(1, =_out_gg) →
U4_AAG(
1,
=_out_aa)
with rule
U3_AAG(
1,
=_out_gg) →
U4_AAG(
1,
=_out_aa) at position [] and matcher [ ]
U4_AAG(1, =_out_aa) →
P_IN_AAG(
1)
with rule
U4_AAG(
1,
=_out_aa) →
P_IN_AAG(
1) at position [] and matcher [ ]
P_IN_AAG(1) →
U3_AAG(
1,
=_out_gg)
with rule
P_IN_AAG(
1) →
U3_AAG(
1,
=_out_gg)
Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence
All these steps are and every following step will be a correct step w.r.t to Q.
(30) FALSE
(31) PrologToPiTRSProof (SOUND transformation)
We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
p_in: (f,f,f) (f,f,b)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
p_in_aaa(X, Y, Z) → U1_aaa(X, Y, Z, =_in_aa(X, Y))
=_in_aa(X, X) → =_out_aa(X, X)
U1_aaa(X, Y, Z, =_out_aa(X, Y)) → U2_aaa(X, Y, Z, =_in_ag(Z, 1))
=_in_ag(X, X) → =_out_ag(X, X)
U2_aaa(X, Y, Z, =_out_ag(Z, 1)) → p_out_aaa(X, Y, Z)
p_in_aaa(X, Y, Z) → U3_aaa(X, Y, Z, =_in_ag(Z, 1))
U3_aaa(X, Y, Z, =_out_ag(Z, 1)) → U4_aaa(X, Y, Z, =_in_aa(Y, X))
U4_aaa(X, Y, Z, =_out_aa(Y, X)) → U5_aaa(X, Y, Z, p_in_aag(X, Y, Z))
p_in_aag(X, Y, Z) → U1_aag(X, Y, Z, =_in_aa(X, Y))
U1_aag(X, Y, Z, =_out_aa(X, Y)) → U2_aag(X, Y, Z, =_in_gg(Z, 1))
=_in_gg(X, X) → =_out_gg(X, X)
U2_aag(X, Y, Z, =_out_gg(Z, 1)) → p_out_aag(X, Y, Z)
p_in_aag(X, Y, Z) → U3_aag(X, Y, Z, =_in_gg(Z, 1))
U3_aag(X, Y, Z, =_out_gg(Z, 1)) → U4_aag(X, Y, Z, =_in_aa(Y, X))
U4_aag(X, Y, Z, =_out_aa(Y, X)) → U5_aag(X, Y, Z, p_in_aag(X, Y, Z))
U5_aag(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aag(X, Y, Z)
U5_aaa(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aaa(X, Y, Z)
The argument filtering Pi contains the following mapping:
p_in_aaa(
x1,
x2,
x3) =
p_in_aaa
U1_aaa(
x1,
x2,
x3,
x4) =
U1_aaa(
x4)
=_in_aa(
x1,
x2) =
=_in_aa
=_out_aa(
x1,
x2) =
=_out_aa
U2_aaa(
x1,
x2,
x3,
x4) =
U2_aaa(
x4)
=_in_ag(
x1,
x2) =
=_in_ag(
x2)
=_out_ag(
x1,
x2) =
=_out_ag(
x1,
x2)
1 =
1
p_out_aaa(
x1,
x2,
x3) =
p_out_aaa(
x3)
U3_aaa(
x1,
x2,
x3,
x4) =
U3_aaa(
x4)
U4_aaa(
x1,
x2,
x3,
x4) =
U4_aaa(
x3,
x4)
U5_aaa(
x1,
x2,
x3,
x4) =
U5_aaa(
x3,
x4)
p_in_aag(
x1,
x2,
x3) =
p_in_aag(
x3)
U1_aag(
x1,
x2,
x3,
x4) =
U1_aag(
x3,
x4)
U2_aag(
x1,
x2,
x3,
x4) =
U2_aag(
x3,
x4)
=_in_gg(
x1,
x2) =
=_in_gg(
x1,
x2)
=_out_gg(
x1,
x2) =
=_out_gg(
x1,
x2)
p_out_aag(
x1,
x2,
x3) =
p_out_aag(
x3)
U3_aag(
x1,
x2,
x3,
x4) =
U3_aag(
x3,
x4)
U4_aag(
x1,
x2,
x3,
x4) =
U4_aag(
x3,
x4)
U5_aag(
x1,
x2,
x3,
x4) =
U5_aag(
x3,
x4)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(32) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
p_in_aaa(X, Y, Z) → U1_aaa(X, Y, Z, =_in_aa(X, Y))
=_in_aa(X, X) → =_out_aa(X, X)
U1_aaa(X, Y, Z, =_out_aa(X, Y)) → U2_aaa(X, Y, Z, =_in_ag(Z, 1))
=_in_ag(X, X) → =_out_ag(X, X)
U2_aaa(X, Y, Z, =_out_ag(Z, 1)) → p_out_aaa(X, Y, Z)
p_in_aaa(X, Y, Z) → U3_aaa(X, Y, Z, =_in_ag(Z, 1))
U3_aaa(X, Y, Z, =_out_ag(Z, 1)) → U4_aaa(X, Y, Z, =_in_aa(Y, X))
U4_aaa(X, Y, Z, =_out_aa(Y, X)) → U5_aaa(X, Y, Z, p_in_aag(X, Y, Z))
p_in_aag(X, Y, Z) → U1_aag(X, Y, Z, =_in_aa(X, Y))
U1_aag(X, Y, Z, =_out_aa(X, Y)) → U2_aag(X, Y, Z, =_in_gg(Z, 1))
=_in_gg(X, X) → =_out_gg(X, X)
U2_aag(X, Y, Z, =_out_gg(Z, 1)) → p_out_aag(X, Y, Z)
p_in_aag(X, Y, Z) → U3_aag(X, Y, Z, =_in_gg(Z, 1))
U3_aag(X, Y, Z, =_out_gg(Z, 1)) → U4_aag(X, Y, Z, =_in_aa(Y, X))
U4_aag(X, Y, Z, =_out_aa(Y, X)) → U5_aag(X, Y, Z, p_in_aag(X, Y, Z))
U5_aag(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aag(X, Y, Z)
U5_aaa(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aaa(X, Y, Z)
The argument filtering Pi contains the following mapping:
p_in_aaa(
x1,
x2,
x3) =
p_in_aaa
U1_aaa(
x1,
x2,
x3,
x4) =
U1_aaa(
x4)
=_in_aa(
x1,
x2) =
=_in_aa
=_out_aa(
x1,
x2) =
=_out_aa
U2_aaa(
x1,
x2,
x3,
x4) =
U2_aaa(
x4)
=_in_ag(
x1,
x2) =
=_in_ag(
x2)
=_out_ag(
x1,
x2) =
=_out_ag(
x1,
x2)
1 =
1
p_out_aaa(
x1,
x2,
x3) =
p_out_aaa(
x3)
U3_aaa(
x1,
x2,
x3,
x4) =
U3_aaa(
x4)
U4_aaa(
x1,
x2,
x3,
x4) =
U4_aaa(
x3,
x4)
U5_aaa(
x1,
x2,
x3,
x4) =
U5_aaa(
x3,
x4)
p_in_aag(
x1,
x2,
x3) =
p_in_aag(
x3)
U1_aag(
x1,
x2,
x3,
x4) =
U1_aag(
x3,
x4)
U2_aag(
x1,
x2,
x3,
x4) =
U2_aag(
x3,
x4)
=_in_gg(
x1,
x2) =
=_in_gg(
x1,
x2)
=_out_gg(
x1,
x2) =
=_out_gg(
x1,
x2)
p_out_aag(
x1,
x2,
x3) =
p_out_aag(
x3)
U3_aag(
x1,
x2,
x3,
x4) =
U3_aag(
x3,
x4)
U4_aag(
x1,
x2,
x3,
x4) =
U4_aag(
x3,
x4)
U5_aag(
x1,
x2,
x3,
x4) =
U5_aag(
x3,
x4)
(33) 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:
P_IN_AAA(X, Y, Z) → U1_AAA(X, Y, Z, =_in_aa(X, Y))
P_IN_AAA(X, Y, Z) → =_IN_AA(X, Y)
U1_AAA(X, Y, Z, =_out_aa(X, Y)) → U2_AAA(X, Y, Z, =_in_ag(Z, 1))
U1_AAA(X, Y, Z, =_out_aa(X, Y)) → =_IN_AG(Z, 1)
P_IN_AAA(X, Y, Z) → U3_AAA(X, Y, Z, =_in_ag(Z, 1))
P_IN_AAA(X, Y, Z) → =_IN_AG(Z, 1)
U3_AAA(X, Y, Z, =_out_ag(Z, 1)) → U4_AAA(X, Y, Z, =_in_aa(Y, X))
U3_AAA(X, Y, Z, =_out_ag(Z, 1)) → =_IN_AA(Y, X)
U4_AAA(X, Y, Z, =_out_aa(Y, X)) → U5_AAA(X, Y, Z, p_in_aag(X, Y, Z))
U4_AAA(X, Y, Z, =_out_aa(Y, X)) → P_IN_AAG(X, Y, Z)
P_IN_AAG(X, Y, Z) → U1_AAG(X, Y, Z, =_in_aa(X, Y))
P_IN_AAG(X, Y, Z) → =_IN_AA(X, Y)
U1_AAG(X, Y, Z, =_out_aa(X, Y)) → U2_AAG(X, Y, Z, =_in_gg(Z, 1))
U1_AAG(X, Y, Z, =_out_aa(X, Y)) → =_IN_GG(Z, 1)
P_IN_AAG(X, Y, Z) → U3_AAG(X, Y, Z, =_in_gg(Z, 1))
P_IN_AAG(X, Y, Z) → =_IN_GG(Z, 1)
U3_AAG(X, Y, Z, =_out_gg(Z, 1)) → U4_AAG(X, Y, Z, =_in_aa(Y, X))
U3_AAG(X, Y, Z, =_out_gg(Z, 1)) → =_IN_AA(Y, X)
U4_AAG(X, Y, Z, =_out_aa(Y, X)) → U5_AAG(X, Y, Z, p_in_aag(X, Y, Z))
U4_AAG(X, Y, Z, =_out_aa(Y, X)) → P_IN_AAG(X, Y, Z)
The TRS R consists of the following rules:
p_in_aaa(X, Y, Z) → U1_aaa(X, Y, Z, =_in_aa(X, Y))
=_in_aa(X, X) → =_out_aa(X, X)
U1_aaa(X, Y, Z, =_out_aa(X, Y)) → U2_aaa(X, Y, Z, =_in_ag(Z, 1))
=_in_ag(X, X) → =_out_ag(X, X)
U2_aaa(X, Y, Z, =_out_ag(Z, 1)) → p_out_aaa(X, Y, Z)
p_in_aaa(X, Y, Z) → U3_aaa(X, Y, Z, =_in_ag(Z, 1))
U3_aaa(X, Y, Z, =_out_ag(Z, 1)) → U4_aaa(X, Y, Z, =_in_aa(Y, X))
U4_aaa(X, Y, Z, =_out_aa(Y, X)) → U5_aaa(X, Y, Z, p_in_aag(X, Y, Z))
p_in_aag(X, Y, Z) → U1_aag(X, Y, Z, =_in_aa(X, Y))
U1_aag(X, Y, Z, =_out_aa(X, Y)) → U2_aag(X, Y, Z, =_in_gg(Z, 1))
=_in_gg(X, X) → =_out_gg(X, X)
U2_aag(X, Y, Z, =_out_gg(Z, 1)) → p_out_aag(X, Y, Z)
p_in_aag(X, Y, Z) → U3_aag(X, Y, Z, =_in_gg(Z, 1))
U3_aag(X, Y, Z, =_out_gg(Z, 1)) → U4_aag(X, Y, Z, =_in_aa(Y, X))
U4_aag(X, Y, Z, =_out_aa(Y, X)) → U5_aag(X, Y, Z, p_in_aag(X, Y, Z))
U5_aag(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aag(X, Y, Z)
U5_aaa(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aaa(X, Y, Z)
The argument filtering Pi contains the following mapping:
p_in_aaa(
x1,
x2,
x3) =
p_in_aaa
U1_aaa(
x1,
x2,
x3,
x4) =
U1_aaa(
x4)
=_in_aa(
x1,
x2) =
=_in_aa
=_out_aa(
x1,
x2) =
=_out_aa
U2_aaa(
x1,
x2,
x3,
x4) =
U2_aaa(
x4)
=_in_ag(
x1,
x2) =
=_in_ag(
x2)
=_out_ag(
x1,
x2) =
=_out_ag(
x1,
x2)
1 =
1
p_out_aaa(
x1,
x2,
x3) =
p_out_aaa(
x3)
U3_aaa(
x1,
x2,
x3,
x4) =
U3_aaa(
x4)
U4_aaa(
x1,
x2,
x3,
x4) =
U4_aaa(
x3,
x4)
U5_aaa(
x1,
x2,
x3,
x4) =
U5_aaa(
x3,
x4)
p_in_aag(
x1,
x2,
x3) =
p_in_aag(
x3)
U1_aag(
x1,
x2,
x3,
x4) =
U1_aag(
x3,
x4)
U2_aag(
x1,
x2,
x3,
x4) =
U2_aag(
x3,
x4)
=_in_gg(
x1,
x2) =
=_in_gg(
x1,
x2)
=_out_gg(
x1,
x2) =
=_out_gg(
x1,
x2)
p_out_aag(
x1,
x2,
x3) =
p_out_aag(
x3)
U3_aag(
x1,
x2,
x3,
x4) =
U3_aag(
x3,
x4)
U4_aag(
x1,
x2,
x3,
x4) =
U4_aag(
x3,
x4)
U5_aag(
x1,
x2,
x3,
x4) =
U5_aag(
x3,
x4)
P_IN_AAA(
x1,
x2,
x3) =
P_IN_AAA
U1_AAA(
x1,
x2,
x3,
x4) =
U1_AAA(
x4)
=_IN_AA(
x1,
x2) =
=_IN_AA
U2_AAA(
x1,
x2,
x3,
x4) =
U2_AAA(
x4)
=_IN_AG(
x1,
x2) =
=_IN_AG(
x2)
U3_AAA(
x1,
x2,
x3,
x4) =
U3_AAA(
x4)
U4_AAA(
x1,
x2,
x3,
x4) =
U4_AAA(
x3,
x4)
U5_AAA(
x1,
x2,
x3,
x4) =
U5_AAA(
x3,
x4)
P_IN_AAG(
x1,
x2,
x3) =
P_IN_AAG(
x3)
U1_AAG(
x1,
x2,
x3,
x4) =
U1_AAG(
x3,
x4)
U2_AAG(
x1,
x2,
x3,
x4) =
U2_AAG(
x3,
x4)
=_IN_GG(
x1,
x2) =
=_IN_GG(
x1,
x2)
U3_AAG(
x1,
x2,
x3,
x4) =
U3_AAG(
x3,
x4)
U4_AAG(
x1,
x2,
x3,
x4) =
U4_AAG(
x3,
x4)
U5_AAG(
x1,
x2,
x3,
x4) =
U5_AAG(
x3,
x4)
We have to consider all (P,R,Pi)-chains
(34) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
P_IN_AAA(X, Y, Z) → U1_AAA(X, Y, Z, =_in_aa(X, Y))
P_IN_AAA(X, Y, Z) → =_IN_AA(X, Y)
U1_AAA(X, Y, Z, =_out_aa(X, Y)) → U2_AAA(X, Y, Z, =_in_ag(Z, 1))
U1_AAA(X, Y, Z, =_out_aa(X, Y)) → =_IN_AG(Z, 1)
P_IN_AAA(X, Y, Z) → U3_AAA(X, Y, Z, =_in_ag(Z, 1))
P_IN_AAA(X, Y, Z) → =_IN_AG(Z, 1)
U3_AAA(X, Y, Z, =_out_ag(Z, 1)) → U4_AAA(X, Y, Z, =_in_aa(Y, X))
U3_AAA(X, Y, Z, =_out_ag(Z, 1)) → =_IN_AA(Y, X)
U4_AAA(X, Y, Z, =_out_aa(Y, X)) → U5_AAA(X, Y, Z, p_in_aag(X, Y, Z))
U4_AAA(X, Y, Z, =_out_aa(Y, X)) → P_IN_AAG(X, Y, Z)
P_IN_AAG(X, Y, Z) → U1_AAG(X, Y, Z, =_in_aa(X, Y))
P_IN_AAG(X, Y, Z) → =_IN_AA(X, Y)
U1_AAG(X, Y, Z, =_out_aa(X, Y)) → U2_AAG(X, Y, Z, =_in_gg(Z, 1))
U1_AAG(X, Y, Z, =_out_aa(X, Y)) → =_IN_GG(Z, 1)
P_IN_AAG(X, Y, Z) → U3_AAG(X, Y, Z, =_in_gg(Z, 1))
P_IN_AAG(X, Y, Z) → =_IN_GG(Z, 1)
U3_AAG(X, Y, Z, =_out_gg(Z, 1)) → U4_AAG(X, Y, Z, =_in_aa(Y, X))
U3_AAG(X, Y, Z, =_out_gg(Z, 1)) → =_IN_AA(Y, X)
U4_AAG(X, Y, Z, =_out_aa(Y, X)) → U5_AAG(X, Y, Z, p_in_aag(X, Y, Z))
U4_AAG(X, Y, Z, =_out_aa(Y, X)) → P_IN_AAG(X, Y, Z)
The TRS R consists of the following rules:
p_in_aaa(X, Y, Z) → U1_aaa(X, Y, Z, =_in_aa(X, Y))
=_in_aa(X, X) → =_out_aa(X, X)
U1_aaa(X, Y, Z, =_out_aa(X, Y)) → U2_aaa(X, Y, Z, =_in_ag(Z, 1))
=_in_ag(X, X) → =_out_ag(X, X)
U2_aaa(X, Y, Z, =_out_ag(Z, 1)) → p_out_aaa(X, Y, Z)
p_in_aaa(X, Y, Z) → U3_aaa(X, Y, Z, =_in_ag(Z, 1))
U3_aaa(X, Y, Z, =_out_ag(Z, 1)) → U4_aaa(X, Y, Z, =_in_aa(Y, X))
U4_aaa(X, Y, Z, =_out_aa(Y, X)) → U5_aaa(X, Y, Z, p_in_aag(X, Y, Z))
p_in_aag(X, Y, Z) → U1_aag(X, Y, Z, =_in_aa(X, Y))
U1_aag(X, Y, Z, =_out_aa(X, Y)) → U2_aag(X, Y, Z, =_in_gg(Z, 1))
=_in_gg(X, X) → =_out_gg(X, X)
U2_aag(X, Y, Z, =_out_gg(Z, 1)) → p_out_aag(X, Y, Z)
p_in_aag(X, Y, Z) → U3_aag(X, Y, Z, =_in_gg(Z, 1))
U3_aag(X, Y, Z, =_out_gg(Z, 1)) → U4_aag(X, Y, Z, =_in_aa(Y, X))
U4_aag(X, Y, Z, =_out_aa(Y, X)) → U5_aag(X, Y, Z, p_in_aag(X, Y, Z))
U5_aag(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aag(X, Y, Z)
U5_aaa(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aaa(X, Y, Z)
The argument filtering Pi contains the following mapping:
p_in_aaa(
x1,
x2,
x3) =
p_in_aaa
U1_aaa(
x1,
x2,
x3,
x4) =
U1_aaa(
x4)
=_in_aa(
x1,
x2) =
=_in_aa
=_out_aa(
x1,
x2) =
=_out_aa
U2_aaa(
x1,
x2,
x3,
x4) =
U2_aaa(
x4)
=_in_ag(
x1,
x2) =
=_in_ag(
x2)
=_out_ag(
x1,
x2) =
=_out_ag(
x1,
x2)
1 =
1
p_out_aaa(
x1,
x2,
x3) =
p_out_aaa(
x3)
U3_aaa(
x1,
x2,
x3,
x4) =
U3_aaa(
x4)
U4_aaa(
x1,
x2,
x3,
x4) =
U4_aaa(
x3,
x4)
U5_aaa(
x1,
x2,
x3,
x4) =
U5_aaa(
x3,
x4)
p_in_aag(
x1,
x2,
x3) =
p_in_aag(
x3)
U1_aag(
x1,
x2,
x3,
x4) =
U1_aag(
x3,
x4)
U2_aag(
x1,
x2,
x3,
x4) =
U2_aag(
x3,
x4)
=_in_gg(
x1,
x2) =
=_in_gg(
x1,
x2)
=_out_gg(
x1,
x2) =
=_out_gg(
x1,
x2)
p_out_aag(
x1,
x2,
x3) =
p_out_aag(
x3)
U3_aag(
x1,
x2,
x3,
x4) =
U3_aag(
x3,
x4)
U4_aag(
x1,
x2,
x3,
x4) =
U4_aag(
x3,
x4)
U5_aag(
x1,
x2,
x3,
x4) =
U5_aag(
x3,
x4)
P_IN_AAA(
x1,
x2,
x3) =
P_IN_AAA
U1_AAA(
x1,
x2,
x3,
x4) =
U1_AAA(
x4)
=_IN_AA(
x1,
x2) =
=_IN_AA
U2_AAA(
x1,
x2,
x3,
x4) =
U2_AAA(
x4)
=_IN_AG(
x1,
x2) =
=_IN_AG(
x2)
U3_AAA(
x1,
x2,
x3,
x4) =
U3_AAA(
x4)
U4_AAA(
x1,
x2,
x3,
x4) =
U4_AAA(
x3,
x4)
U5_AAA(
x1,
x2,
x3,
x4) =
U5_AAA(
x3,
x4)
P_IN_AAG(
x1,
x2,
x3) =
P_IN_AAG(
x3)
U1_AAG(
x1,
x2,
x3,
x4) =
U1_AAG(
x3,
x4)
U2_AAG(
x1,
x2,
x3,
x4) =
U2_AAG(
x3,
x4)
=_IN_GG(
x1,
x2) =
=_IN_GG(
x1,
x2)
U3_AAG(
x1,
x2,
x3,
x4) =
U3_AAG(
x3,
x4)
U4_AAG(
x1,
x2,
x3,
x4) =
U4_AAG(
x3,
x4)
U5_AAG(
x1,
x2,
x3,
x4) =
U5_AAG(
x3,
x4)
We have to consider all (P,R,Pi)-chains
(35) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 17 less nodes.
(36) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
P_IN_AAG(X, Y, Z) → U3_AAG(X, Y, Z, =_in_gg(Z, 1))
U3_AAG(X, Y, Z, =_out_gg(Z, 1)) → U4_AAG(X, Y, Z, =_in_aa(Y, X))
U4_AAG(X, Y, Z, =_out_aa(Y, X)) → P_IN_AAG(X, Y, Z)
The TRS R consists of the following rules:
p_in_aaa(X, Y, Z) → U1_aaa(X, Y, Z, =_in_aa(X, Y))
=_in_aa(X, X) → =_out_aa(X, X)
U1_aaa(X, Y, Z, =_out_aa(X, Y)) → U2_aaa(X, Y, Z, =_in_ag(Z, 1))
=_in_ag(X, X) → =_out_ag(X, X)
U2_aaa(X, Y, Z, =_out_ag(Z, 1)) → p_out_aaa(X, Y, Z)
p_in_aaa(X, Y, Z) → U3_aaa(X, Y, Z, =_in_ag(Z, 1))
U3_aaa(X, Y, Z, =_out_ag(Z, 1)) → U4_aaa(X, Y, Z, =_in_aa(Y, X))
U4_aaa(X, Y, Z, =_out_aa(Y, X)) → U5_aaa(X, Y, Z, p_in_aag(X, Y, Z))
p_in_aag(X, Y, Z) → U1_aag(X, Y, Z, =_in_aa(X, Y))
U1_aag(X, Y, Z, =_out_aa(X, Y)) → U2_aag(X, Y, Z, =_in_gg(Z, 1))
=_in_gg(X, X) → =_out_gg(X, X)
U2_aag(X, Y, Z, =_out_gg(Z, 1)) → p_out_aag(X, Y, Z)
p_in_aag(X, Y, Z) → U3_aag(X, Y, Z, =_in_gg(Z, 1))
U3_aag(X, Y, Z, =_out_gg(Z, 1)) → U4_aag(X, Y, Z, =_in_aa(Y, X))
U4_aag(X, Y, Z, =_out_aa(Y, X)) → U5_aag(X, Y, Z, p_in_aag(X, Y, Z))
U5_aag(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aag(X, Y, Z)
U5_aaa(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aaa(X, Y, Z)
The argument filtering Pi contains the following mapping:
p_in_aaa(
x1,
x2,
x3) =
p_in_aaa
U1_aaa(
x1,
x2,
x3,
x4) =
U1_aaa(
x4)
=_in_aa(
x1,
x2) =
=_in_aa
=_out_aa(
x1,
x2) =
=_out_aa
U2_aaa(
x1,
x2,
x3,
x4) =
U2_aaa(
x4)
=_in_ag(
x1,
x2) =
=_in_ag(
x2)
=_out_ag(
x1,
x2) =
=_out_ag(
x1,
x2)
1 =
1
p_out_aaa(
x1,
x2,
x3) =
p_out_aaa(
x3)
U3_aaa(
x1,
x2,
x3,
x4) =
U3_aaa(
x4)
U4_aaa(
x1,
x2,
x3,
x4) =
U4_aaa(
x3,
x4)
U5_aaa(
x1,
x2,
x3,
x4) =
U5_aaa(
x3,
x4)
p_in_aag(
x1,
x2,
x3) =
p_in_aag(
x3)
U1_aag(
x1,
x2,
x3,
x4) =
U1_aag(
x3,
x4)
U2_aag(
x1,
x2,
x3,
x4) =
U2_aag(
x3,
x4)
=_in_gg(
x1,
x2) =
=_in_gg(
x1,
x2)
=_out_gg(
x1,
x2) =
=_out_gg(
x1,
x2)
p_out_aag(
x1,
x2,
x3) =
p_out_aag(
x3)
U3_aag(
x1,
x2,
x3,
x4) =
U3_aag(
x3,
x4)
U4_aag(
x1,
x2,
x3,
x4) =
U4_aag(
x3,
x4)
U5_aag(
x1,
x2,
x3,
x4) =
U5_aag(
x3,
x4)
P_IN_AAG(
x1,
x2,
x3) =
P_IN_AAG(
x3)
U3_AAG(
x1,
x2,
x3,
x4) =
U3_AAG(
x3,
x4)
U4_AAG(
x1,
x2,
x3,
x4) =
U4_AAG(
x3,
x4)
We have to consider all (P,R,Pi)-chains
(37) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(38) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
P_IN_AAG(X, Y, Z) → U3_AAG(X, Y, Z, =_in_gg(Z, 1))
U3_AAG(X, Y, Z, =_out_gg(Z, 1)) → U4_AAG(X, Y, Z, =_in_aa(Y, X))
U4_AAG(X, Y, Z, =_out_aa(Y, X)) → P_IN_AAG(X, Y, Z)
The TRS R consists of the following rules:
=_in_gg(X, X) → =_out_gg(X, X)
=_in_aa(X, X) → =_out_aa(X, X)
The argument filtering Pi contains the following mapping:
=_in_aa(
x1,
x2) =
=_in_aa
=_out_aa(
x1,
x2) =
=_out_aa
1 =
1
=_in_gg(
x1,
x2) =
=_in_gg(
x1,
x2)
=_out_gg(
x1,
x2) =
=_out_gg(
x1,
x2)
P_IN_AAG(
x1,
x2,
x3) =
P_IN_AAG(
x3)
U3_AAG(
x1,
x2,
x3,
x4) =
U3_AAG(
x3,
x4)
U4_AAG(
x1,
x2,
x3,
x4) =
U4_AAG(
x3,
x4)
We have to consider all (P,R,Pi)-chains
(39) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(40) Obligation:
Q DP problem:
The TRS P consists of the following rules:
P_IN_AAG(Z) → U3_AAG(Z, =_in_gg(Z, 1))
U3_AAG(Z, =_out_gg(Z, 1)) → U4_AAG(Z, =_in_aa)
U4_AAG(Z, =_out_aa) → P_IN_AAG(Z)
The TRS R consists of the following rules:
=_in_gg(X, X) → =_out_gg(X, X)
=_in_aa → =_out_aa
The set Q consists of the following terms:
=_in_gg(x0, x1)
=_in_aa
We have to consider all (P,Q,R)-chains.
(41) Rewriting (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
U3_AAG(
Z,
=_out_gg(
Z,
1)) →
U4_AAG(
Z,
=_in_aa) at position [1] we obtained the following new rules [LPAR04]:
U3_AAG(Z, =_out_gg(Z, 1)) → U4_AAG(Z, =_out_aa)
(42) Obligation:
Q DP problem:
The TRS P consists of the following rules:
P_IN_AAG(Z) → U3_AAG(Z, =_in_gg(Z, 1))
U4_AAG(Z, =_out_aa) → P_IN_AAG(Z)
U3_AAG(Z, =_out_gg(Z, 1)) → U4_AAG(Z, =_out_aa)
The TRS R consists of the following rules:
=_in_gg(X, X) → =_out_gg(X, X)
=_in_aa → =_out_aa
The set Q consists of the following terms:
=_in_gg(x0, x1)
=_in_aa
We have to consider all (P,Q,R)-chains.
(43) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(44) Obligation:
Q DP problem:
The TRS P consists of the following rules:
P_IN_AAG(Z) → U3_AAG(Z, =_in_gg(Z, 1))
U4_AAG(Z, =_out_aa) → P_IN_AAG(Z)
U3_AAG(Z, =_out_gg(Z, 1)) → U4_AAG(Z, =_out_aa)
The TRS R consists of the following rules:
=_in_gg(X, X) → =_out_gg(X, X)
The set Q consists of the following terms:
=_in_gg(x0, x1)
=_in_aa
We have to consider all (P,Q,R)-chains.
(45) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
=_in_aa
(46) Obligation:
Q DP problem:
The TRS P consists of the following rules:
P_IN_AAG(Z) → U3_AAG(Z, =_in_gg(Z, 1))
U4_AAG(Z, =_out_aa) → P_IN_AAG(Z)
U3_AAG(Z, =_out_gg(Z, 1)) → U4_AAG(Z, =_out_aa)
The TRS R consists of the following rules:
=_in_gg(X, X) → =_out_gg(X, X)
The set Q consists of the following terms:
=_in_gg(x0, x1)
We have to consider all (P,Q,R)-chains.
(47) Narrowing (SOUND transformation)
By narrowing [LPAR04] the rule
P_IN_AAG(
Z) →
U3_AAG(
Z,
=_in_gg(
Z,
1)) at position [1] we obtained the following new rules [LPAR04]:
P_IN_AAG(1) → U3_AAG(1, =_out_gg(1, 1))
(48) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_AAG(Z, =_out_aa) → P_IN_AAG(Z)
U3_AAG(Z, =_out_gg(Z, 1)) → U4_AAG(Z, =_out_aa)
P_IN_AAG(1) → U3_AAG(1, =_out_gg(1, 1))
The TRS R consists of the following rules:
=_in_gg(X, X) → =_out_gg(X, X)
The set Q consists of the following terms:
=_in_gg(x0, x1)
We have to consider all (P,Q,R)-chains.
(49) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(50) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_AAG(Z, =_out_aa) → P_IN_AAG(Z)
U3_AAG(Z, =_out_gg(Z, 1)) → U4_AAG(Z, =_out_aa)
P_IN_AAG(1) → U3_AAG(1, =_out_gg(1, 1))
R is empty.
The set Q consists of the following terms:
=_in_gg(x0, x1)
We have to consider all (P,Q,R)-chains.
(51) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
=_in_gg(x0, x1)
(52) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_AAG(Z, =_out_aa) → P_IN_AAG(Z)
U3_AAG(Z, =_out_gg(Z, 1)) → U4_AAG(Z, =_out_aa)
P_IN_AAG(1) → U3_AAG(1, =_out_gg(1, 1))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(53) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U3_AAG(
Z,
=_out_gg(
Z,
1)) →
U4_AAG(
Z,
=_out_aa) we obtained the following new rules [LPAR04]:
U3_AAG(1, =_out_gg(1, 1)) → U4_AAG(1, =_out_aa)
(54) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_AAG(Z, =_out_aa) → P_IN_AAG(Z)
P_IN_AAG(1) → U3_AAG(1, =_out_gg(1, 1))
U3_AAG(1, =_out_gg(1, 1)) → U4_AAG(1, =_out_aa)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(55) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U4_AAG(
Z,
=_out_aa) →
P_IN_AAG(
Z) we obtained the following new rules [LPAR04]:
U4_AAG(1, =_out_aa) → P_IN_AAG(1)
(56) Obligation:
Q DP problem:
The TRS P consists of the following rules:
P_IN_AAG(1) → U3_AAG(1, =_out_gg(1, 1))
U3_AAG(1, =_out_gg(1, 1)) → U4_AAG(1, =_out_aa)
U4_AAG(1, =_out_aa) → P_IN_AAG(1)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(57) NonTerminationProof (EQUIVALENT transformation)
We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:
s =
U3_AAG(
1,
=_out_gg(
1,
1)) evaluates to t =
U3_AAG(
1,
=_out_gg(
1,
1))
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Matcher: [ ]
- Semiunifier: [ ]
Rewriting sequenceU3_AAG(1, =_out_gg(1, 1)) →
U4_AAG(
1,
=_out_aa)
with rule
U3_AAG(
1,
=_out_gg(
1,
1)) →
U4_AAG(
1,
=_out_aa) at position [] and matcher [ ]
U4_AAG(1, =_out_aa) →
P_IN_AAG(
1)
with rule
U4_AAG(
1,
=_out_aa) →
P_IN_AAG(
1) at position [] and matcher [ ]
P_IN_AAG(1) →
U3_AAG(
1,
=_out_gg(
1,
1))
with rule
P_IN_AAG(
1) →
U3_AAG(
1,
=_out_gg(
1,
1))
Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence
All these steps are and every following step will be a correct step w.r.t to Q.
(58) FALSE