(0) Obligation:
Clauses:
p(X, X, 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, X, 1) :- true.
p(X, Y, Z) :- ','(=(Z, 1), ','(=(Y, X), p(X, Y, Z))).
=(X, X).
Queries:
p(a,a,a).
(3) UndefinedPredicateHandlerProof (SOUND transformation)
Added facts for all undefined predicates [PROLOG].
(4) Obligation:
Clauses:
p(X, X, 1) :- true.
p(X, Y, Z) :- ','(=(Z, 1), ','(=(Y, X), p(X, Y, Z))).
=(X, X).
true.
Queries:
p(a,a,a).
(5) 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, X, 1) → U1_aaa(X, true_in_)
true_in_ → true_out_
U1_aaa(X, true_out_) → p_out_aaa(X, X, 1)
p_in_aaa(X, Y, Z) → 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)) → U3_aaa(X, Y, Z, =_in_aa(Y, X))
=_in_aa(X, X) → =_out_aa(X, X)
U3_aaa(X, Y, Z, =_out_aa(Y, X)) → U4_aaa(X, Y, Z, p_in_aag(X, Y, Z))
p_in_aag(X, X, 1) → U1_aag(X, true_in_)
U1_aag(X, true_out_) → p_out_aag(X, X, 1)
p_in_aag(X, Y, Z) → 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)) → U3_aag(X, Y, Z, =_in_aa(Y, X))
U3_aag(X, Y, Z, =_out_aa(Y, X)) → U4_aag(X, Y, Z, p_in_aag(X, Y, Z))
U4_aag(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aag(X, Y, Z)
U4_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) =
U1_aaa(
x2)
true_in_ =
true_in_
true_out_ =
true_out_
p_out_aaa(
x1,
x2,
x3) =
p_out_aaa(
x3)
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
U3_aaa(
x1,
x2,
x3,
x4) =
U3_aaa(
x3,
x4)
=_in_aa(
x1,
x2) =
=_in_aa
=_out_aa(
x1,
x2) =
=_out_aa
U4_aaa(
x1,
x2,
x3,
x4) =
U4_aaa(
x3,
x4)
p_in_aag(
x1,
x2,
x3) =
p_in_aag(
x3)
U1_aag(
x1,
x2) =
U1_aag(
x2)
p_out_aag(
x1,
x2,
x3) =
p_out_aag(
x3)
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)
U3_aag(
x1,
x2,
x3,
x4) =
U3_aag(
x3,
x4)
U4_aag(
x1,
x2,
x3,
x4) =
U4_aag(
x3,
x4)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(6) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
p_in_aaa(X, X, 1) → U1_aaa(X, true_in_)
true_in_ → true_out_
U1_aaa(X, true_out_) → p_out_aaa(X, X, 1)
p_in_aaa(X, Y, Z) → 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)) → U3_aaa(X, Y, Z, =_in_aa(Y, X))
=_in_aa(X, X) → =_out_aa(X, X)
U3_aaa(X, Y, Z, =_out_aa(Y, X)) → U4_aaa(X, Y, Z, p_in_aag(X, Y, Z))
p_in_aag(X, X, 1) → U1_aag(X, true_in_)
U1_aag(X, true_out_) → p_out_aag(X, X, 1)
p_in_aag(X, Y, Z) → 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)) → U3_aag(X, Y, Z, =_in_aa(Y, X))
U3_aag(X, Y, Z, =_out_aa(Y, X)) → U4_aag(X, Y, Z, p_in_aag(X, Y, Z))
U4_aag(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aag(X, Y, Z)
U4_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) =
U1_aaa(
x2)
true_in_ =
true_in_
true_out_ =
true_out_
p_out_aaa(
x1,
x2,
x3) =
p_out_aaa(
x3)
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
U3_aaa(
x1,
x2,
x3,
x4) =
U3_aaa(
x3,
x4)
=_in_aa(
x1,
x2) =
=_in_aa
=_out_aa(
x1,
x2) =
=_out_aa
U4_aaa(
x1,
x2,
x3,
x4) =
U4_aaa(
x3,
x4)
p_in_aag(
x1,
x2,
x3) =
p_in_aag(
x3)
U1_aag(
x1,
x2) =
U1_aag(
x2)
p_out_aag(
x1,
x2,
x3) =
p_out_aag(
x3)
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)
U3_aag(
x1,
x2,
x3,
x4) =
U3_aag(
x3,
x4)
U4_aag(
x1,
x2,
x3,
x4) =
U4_aag(
x3,
x4)
(7) 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, X, 1) → U1_AAA(X, true_in_)
P_IN_AAA(X, X, 1) → TRUE_IN_
P_IN_AAA(X, Y, Z) → U2_AAA(X, Y, Z, =_in_ag(Z, 1))
P_IN_AAA(X, Y, Z) → =_IN_AG(Z, 1)
U2_AAA(X, Y, Z, =_out_ag(Z, 1)) → U3_AAA(X, Y, Z, =_in_aa(Y, X))
U2_AAA(X, Y, Z, =_out_ag(Z, 1)) → =_IN_AA(Y, X)
U3_AAA(X, Y, Z, =_out_aa(Y, X)) → U4_AAA(X, Y, Z, p_in_aag(X, Y, Z))
U3_AAA(X, Y, Z, =_out_aa(Y, X)) → P_IN_AAG(X, Y, Z)
P_IN_AAG(X, X, 1) → U1_AAG(X, true_in_)
P_IN_AAG(X, X, 1) → TRUE_IN_
P_IN_AAG(X, Y, Z) → U2_AAG(X, Y, Z, =_in_gg(Z, 1))
P_IN_AAG(X, Y, Z) → =_IN_GG(Z, 1)
U2_AAG(X, Y, Z, =_out_gg(Z, 1)) → U3_AAG(X, Y, Z, =_in_aa(Y, X))
U2_AAG(X, Y, Z, =_out_gg(Z, 1)) → =_IN_AA(Y, X)
U3_AAG(X, Y, Z, =_out_aa(Y, X)) → U4_AAG(X, Y, Z, p_in_aag(X, Y, Z))
U3_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, X, 1) → U1_aaa(X, true_in_)
true_in_ → true_out_
U1_aaa(X, true_out_) → p_out_aaa(X, X, 1)
p_in_aaa(X, Y, Z) → 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)) → U3_aaa(X, Y, Z, =_in_aa(Y, X))
=_in_aa(X, X) → =_out_aa(X, X)
U3_aaa(X, Y, Z, =_out_aa(Y, X)) → U4_aaa(X, Y, Z, p_in_aag(X, Y, Z))
p_in_aag(X, X, 1) → U1_aag(X, true_in_)
U1_aag(X, true_out_) → p_out_aag(X, X, 1)
p_in_aag(X, Y, Z) → 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)) → U3_aag(X, Y, Z, =_in_aa(Y, X))
U3_aag(X, Y, Z, =_out_aa(Y, X)) → U4_aag(X, Y, Z, p_in_aag(X, Y, Z))
U4_aag(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aag(X, Y, Z)
U4_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) =
U1_aaa(
x2)
true_in_ =
true_in_
true_out_ =
true_out_
p_out_aaa(
x1,
x2,
x3) =
p_out_aaa(
x3)
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
U3_aaa(
x1,
x2,
x3,
x4) =
U3_aaa(
x3,
x4)
=_in_aa(
x1,
x2) =
=_in_aa
=_out_aa(
x1,
x2) =
=_out_aa
U4_aaa(
x1,
x2,
x3,
x4) =
U4_aaa(
x3,
x4)
p_in_aag(
x1,
x2,
x3) =
p_in_aag(
x3)
U1_aag(
x1,
x2) =
U1_aag(
x2)
p_out_aag(
x1,
x2,
x3) =
p_out_aag(
x3)
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)
U3_aag(
x1,
x2,
x3,
x4) =
U3_aag(
x3,
x4)
U4_aag(
x1,
x2,
x3,
x4) =
U4_aag(
x3,
x4)
P_IN_AAA(
x1,
x2,
x3) =
P_IN_AAA
U1_AAA(
x1,
x2) =
U1_AAA(
x2)
TRUE_IN_ =
TRUE_IN_
U2_AAA(
x1,
x2,
x3,
x4) =
U2_AAA(
x4)
=_IN_AG(
x1,
x2) =
=_IN_AG(
x2)
U3_AAA(
x1,
x2,
x3,
x4) =
U3_AAA(
x3,
x4)
=_IN_AA(
x1,
x2) =
=_IN_AA
U4_AAA(
x1,
x2,
x3,
x4) =
U4_AAA(
x3,
x4)
P_IN_AAG(
x1,
x2,
x3) =
P_IN_AAG(
x3)
U1_AAG(
x1,
x2) =
U1_AAG(
x2)
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)
We have to consider all (P,R,Pi)-chains
(8) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
P_IN_AAA(X, X, 1) → U1_AAA(X, true_in_)
P_IN_AAA(X, X, 1) → TRUE_IN_
P_IN_AAA(X, Y, Z) → U2_AAA(X, Y, Z, =_in_ag(Z, 1))
P_IN_AAA(X, Y, Z) → =_IN_AG(Z, 1)
U2_AAA(X, Y, Z, =_out_ag(Z, 1)) → U3_AAA(X, Y, Z, =_in_aa(Y, X))
U2_AAA(X, Y, Z, =_out_ag(Z, 1)) → =_IN_AA(Y, X)
U3_AAA(X, Y, Z, =_out_aa(Y, X)) → U4_AAA(X, Y, Z, p_in_aag(X, Y, Z))
U3_AAA(X, Y, Z, =_out_aa(Y, X)) → P_IN_AAG(X, Y, Z)
P_IN_AAG(X, X, 1) → U1_AAG(X, true_in_)
P_IN_AAG(X, X, 1) → TRUE_IN_
P_IN_AAG(X, Y, Z) → U2_AAG(X, Y, Z, =_in_gg(Z, 1))
P_IN_AAG(X, Y, Z) → =_IN_GG(Z, 1)
U2_AAG(X, Y, Z, =_out_gg(Z, 1)) → U3_AAG(X, Y, Z, =_in_aa(Y, X))
U2_AAG(X, Y, Z, =_out_gg(Z, 1)) → =_IN_AA(Y, X)
U3_AAG(X, Y, Z, =_out_aa(Y, X)) → U4_AAG(X, Y, Z, p_in_aag(X, Y, Z))
U3_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, X, 1) → U1_aaa(X, true_in_)
true_in_ → true_out_
U1_aaa(X, true_out_) → p_out_aaa(X, X, 1)
p_in_aaa(X, Y, Z) → 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)) → U3_aaa(X, Y, Z, =_in_aa(Y, X))
=_in_aa(X, X) → =_out_aa(X, X)
U3_aaa(X, Y, Z, =_out_aa(Y, X)) → U4_aaa(X, Y, Z, p_in_aag(X, Y, Z))
p_in_aag(X, X, 1) → U1_aag(X, true_in_)
U1_aag(X, true_out_) → p_out_aag(X, X, 1)
p_in_aag(X, Y, Z) → 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)) → U3_aag(X, Y, Z, =_in_aa(Y, X))
U3_aag(X, Y, Z, =_out_aa(Y, X)) → U4_aag(X, Y, Z, p_in_aag(X, Y, Z))
U4_aag(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aag(X, Y, Z)
U4_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) =
U1_aaa(
x2)
true_in_ =
true_in_
true_out_ =
true_out_
p_out_aaa(
x1,
x2,
x3) =
p_out_aaa(
x3)
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
U3_aaa(
x1,
x2,
x3,
x4) =
U3_aaa(
x3,
x4)
=_in_aa(
x1,
x2) =
=_in_aa
=_out_aa(
x1,
x2) =
=_out_aa
U4_aaa(
x1,
x2,
x3,
x4) =
U4_aaa(
x3,
x4)
p_in_aag(
x1,
x2,
x3) =
p_in_aag(
x3)
U1_aag(
x1,
x2) =
U1_aag(
x2)
p_out_aag(
x1,
x2,
x3) =
p_out_aag(
x3)
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)
U3_aag(
x1,
x2,
x3,
x4) =
U3_aag(
x3,
x4)
U4_aag(
x1,
x2,
x3,
x4) =
U4_aag(
x3,
x4)
P_IN_AAA(
x1,
x2,
x3) =
P_IN_AAA
U1_AAA(
x1,
x2) =
U1_AAA(
x2)
TRUE_IN_ =
TRUE_IN_
U2_AAA(
x1,
x2,
x3,
x4) =
U2_AAA(
x4)
=_IN_AG(
x1,
x2) =
=_IN_AG(
x2)
U3_AAA(
x1,
x2,
x3,
x4) =
U3_AAA(
x3,
x4)
=_IN_AA(
x1,
x2) =
=_IN_AA
U4_AAA(
x1,
x2,
x3,
x4) =
U4_AAA(
x3,
x4)
P_IN_AAG(
x1,
x2,
x3) =
P_IN_AAG(
x3)
U1_AAG(
x1,
x2) =
U1_AAG(
x2)
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)
We have to consider all (P,R,Pi)-chains
(9) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 13 less nodes.
(10) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
P_IN_AAG(X, Y, Z) → U2_AAG(X, Y, Z, =_in_gg(Z, 1))
U2_AAG(X, Y, Z, =_out_gg(Z, 1)) → U3_AAG(X, Y, Z, =_in_aa(Y, X))
U3_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, X, 1) → U1_aaa(X, true_in_)
true_in_ → true_out_
U1_aaa(X, true_out_) → p_out_aaa(X, X, 1)
p_in_aaa(X, Y, Z) → 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)) → U3_aaa(X, Y, Z, =_in_aa(Y, X))
=_in_aa(X, X) → =_out_aa(X, X)
U3_aaa(X, Y, Z, =_out_aa(Y, X)) → U4_aaa(X, Y, Z, p_in_aag(X, Y, Z))
p_in_aag(X, X, 1) → U1_aag(X, true_in_)
U1_aag(X, true_out_) → p_out_aag(X, X, 1)
p_in_aag(X, Y, Z) → 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)) → U3_aag(X, Y, Z, =_in_aa(Y, X))
U3_aag(X, Y, Z, =_out_aa(Y, X)) → U4_aag(X, Y, Z, p_in_aag(X, Y, Z))
U4_aag(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aag(X, Y, Z)
U4_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) =
U1_aaa(
x2)
true_in_ =
true_in_
true_out_ =
true_out_
p_out_aaa(
x1,
x2,
x3) =
p_out_aaa(
x3)
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
U3_aaa(
x1,
x2,
x3,
x4) =
U3_aaa(
x3,
x4)
=_in_aa(
x1,
x2) =
=_in_aa
=_out_aa(
x1,
x2) =
=_out_aa
U4_aaa(
x1,
x2,
x3,
x4) =
U4_aaa(
x3,
x4)
p_in_aag(
x1,
x2,
x3) =
p_in_aag(
x3)
U1_aag(
x1,
x2) =
U1_aag(
x2)
p_out_aag(
x1,
x2,
x3) =
p_out_aag(
x3)
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)
U3_aag(
x1,
x2,
x3,
x4) =
U3_aag(
x3,
x4)
U4_aag(
x1,
x2,
x3,
x4) =
U4_aag(
x3,
x4)
P_IN_AAG(
x1,
x2,
x3) =
P_IN_AAG(
x3)
U2_AAG(
x1,
x2,
x3,
x4) =
U2_AAG(
x3,
x4)
U3_AAG(
x1,
x2,
x3,
x4) =
U3_AAG(
x3,
x4)
We have to consider all (P,R,Pi)-chains
(11) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(12) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
P_IN_AAG(X, Y, Z) → U2_AAG(X, Y, Z, =_in_gg(Z, 1))
U2_AAG(X, Y, Z, =_out_gg(Z, 1)) → U3_AAG(X, Y, Z, =_in_aa(Y, X))
U3_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:
1 =
1
=_in_aa(
x1,
x2) =
=_in_aa
=_out_aa(
x1,
x2) =
=_out_aa
=_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)
U2_AAG(
x1,
x2,
x3,
x4) =
U2_AAG(
x3,
x4)
U3_AAG(
x1,
x2,
x3,
x4) =
U3_AAG(
x3,
x4)
We have to consider all (P,R,Pi)-chains
(13) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(14) Obligation:
Q DP problem:
The TRS P consists of the following rules:
P_IN_AAG(Z) → U2_AAG(Z, =_in_gg(Z, 1))
U2_AAG(Z, =_out_gg(Z, 1)) → U3_AAG(Z, =_in_aa)
U3_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.
(15) Rewriting (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
U2_AAG(
Z,
=_out_gg(
Z,
1)) →
U3_AAG(
Z,
=_in_aa) at position [1] we obtained the following new rules [LPAR04]:
U2_AAG(Z, =_out_gg(Z, 1)) → U3_AAG(Z, =_out_aa)
(16) Obligation:
Q DP problem:
The TRS P consists of the following rules:
P_IN_AAG(Z) → U2_AAG(Z, =_in_gg(Z, 1))
U3_AAG(Z, =_out_aa) → P_IN_AAG(Z)
U2_AAG(Z, =_out_gg(Z, 1)) → U3_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.
(17) 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.
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
P_IN_AAG(Z) → U2_AAG(Z, =_in_gg(Z, 1))
U3_AAG(Z, =_out_aa) → P_IN_AAG(Z)
U2_AAG(Z, =_out_gg(Z, 1)) → U3_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.
(19) 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
(20) Obligation:
Q DP problem:
The TRS P consists of the following rules:
P_IN_AAG(Z) → U2_AAG(Z, =_in_gg(Z, 1))
U3_AAG(Z, =_out_aa) → P_IN_AAG(Z)
U2_AAG(Z, =_out_gg(Z, 1)) → U3_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.
(21) Narrowing (SOUND transformation)
By narrowing [LPAR04] the rule
P_IN_AAG(
Z) →
U2_AAG(
Z,
=_in_gg(
Z,
1)) at position [1] we obtained the following new rules [LPAR04]:
P_IN_AAG(1) → U2_AAG(1, =_out_gg(1, 1))
(22) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_AAG(Z, =_out_aa) → P_IN_AAG(Z)
U2_AAG(Z, =_out_gg(Z, 1)) → U3_AAG(Z, =_out_aa)
P_IN_AAG(1) → U2_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.
(23) 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.
(24) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_AAG(Z, =_out_aa) → P_IN_AAG(Z)
U2_AAG(Z, =_out_gg(Z, 1)) → U3_AAG(Z, =_out_aa)
P_IN_AAG(1) → U2_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.
(25) 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)
(26) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_AAG(Z, =_out_aa) → P_IN_AAG(Z)
U2_AAG(Z, =_out_gg(Z, 1)) → U3_AAG(Z, =_out_aa)
P_IN_AAG(1) → U2_AAG(1, =_out_gg(1, 1))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(27) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U2_AAG(
Z,
=_out_gg(
Z,
1)) →
U3_AAG(
Z,
=_out_aa) we obtained the following new rules [LPAR04]:
U2_AAG(1, =_out_gg(1, 1)) → U3_AAG(1, =_out_aa)
(28) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_AAG(Z, =_out_aa) → P_IN_AAG(Z)
P_IN_AAG(1) → U2_AAG(1, =_out_gg(1, 1))
U2_AAG(1, =_out_gg(1, 1)) → U3_AAG(1, =_out_aa)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(29) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U3_AAG(
Z,
=_out_aa) →
P_IN_AAG(
Z) we obtained the following new rules [LPAR04]:
U3_AAG(1, =_out_aa) → P_IN_AAG(1)
(30) Obligation:
Q DP problem:
The TRS P consists of the following rules:
P_IN_AAG(1) → U2_AAG(1, =_out_gg(1, 1))
U2_AAG(1, =_out_gg(1, 1)) → U3_AAG(1, =_out_aa)
U3_AAG(1, =_out_aa) → P_IN_AAG(1)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(31) 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 =
U2_AAG(
1,
=_out_gg(
1,
1)) evaluates to t =
U2_AAG(
1,
=_out_gg(
1,
1))
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Matcher: [ ]
- Semiunifier: [ ]
Rewriting sequenceU2_AAG(1, =_out_gg(1, 1)) →
U3_AAG(
1,
=_out_aa)
with rule
U2_AAG(
1,
=_out_gg(
1,
1)) →
U3_AAG(
1,
=_out_aa) at position [] and matcher [ ]
U3_AAG(1, =_out_aa) →
P_IN_AAG(
1)
with rule
U3_AAG(
1,
=_out_aa) →
P_IN_AAG(
1) at position [] and matcher [ ]
P_IN_AAG(1) →
U2_AAG(
1,
=_out_gg(
1,
1))
with rule
P_IN_AAG(
1) →
U2_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.
(32) FALSE
(33) 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, X, 1) → U1_aaa(X, true_in_)
true_in_ → true_out_
U1_aaa(X, true_out_) → p_out_aaa(X, X, 1)
p_in_aaa(X, Y, Z) → 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)) → U3_aaa(X, Y, Z, =_in_aa(Y, X))
=_in_aa(X, X) → =_out_aa(X, X)
U3_aaa(X, Y, Z, =_out_aa(Y, X)) → U4_aaa(X, Y, Z, p_in_aag(X, Y, Z))
p_in_aag(X, X, 1) → U1_aag(X, true_in_)
U1_aag(X, true_out_) → p_out_aag(X, X, 1)
p_in_aag(X, Y, Z) → 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)) → U3_aag(X, Y, Z, =_in_aa(Y, X))
U3_aag(X, Y, Z, =_out_aa(Y, X)) → U4_aag(X, Y, Z, p_in_aag(X, Y, Z))
U4_aag(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aag(X, Y, Z)
U4_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) =
U1_aaa(
x2)
true_in_ =
true_in_
true_out_ =
true_out_
p_out_aaa(
x1,
x2,
x3) =
p_out_aaa(
x3)
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
U3_aaa(
x1,
x2,
x3,
x4) =
U3_aaa(
x3,
x4)
=_in_aa(
x1,
x2) =
=_in_aa
=_out_aa(
x1,
x2) =
=_out_aa
U4_aaa(
x1,
x2,
x3,
x4) =
U4_aaa(
x3,
x4)
p_in_aag(
x1,
x2,
x3) =
p_in_aag(
x3)
U1_aag(
x1,
x2) =
U1_aag(
x2)
p_out_aag(
x1,
x2,
x3) =
p_out_aag
U2_aag(
x1,
x2,
x3,
x4) =
U2_aag(
x3,
x4)
=_in_gg(
x1,
x2) =
=_in_gg(
x1,
x2)
=_out_gg(
x1,
x2) =
=_out_gg
U3_aag(
x1,
x2,
x3,
x4) =
U3_aag(
x3,
x4)
U4_aag(
x1,
x2,
x3,
x4) =
U4_aag(
x4)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(34) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
p_in_aaa(X, X, 1) → U1_aaa(X, true_in_)
true_in_ → true_out_
U1_aaa(X, true_out_) → p_out_aaa(X, X, 1)
p_in_aaa(X, Y, Z) → 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)) → U3_aaa(X, Y, Z, =_in_aa(Y, X))
=_in_aa(X, X) → =_out_aa(X, X)
U3_aaa(X, Y, Z, =_out_aa(Y, X)) → U4_aaa(X, Y, Z, p_in_aag(X, Y, Z))
p_in_aag(X, X, 1) → U1_aag(X, true_in_)
U1_aag(X, true_out_) → p_out_aag(X, X, 1)
p_in_aag(X, Y, Z) → 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)) → U3_aag(X, Y, Z, =_in_aa(Y, X))
U3_aag(X, Y, Z, =_out_aa(Y, X)) → U4_aag(X, Y, Z, p_in_aag(X, Y, Z))
U4_aag(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aag(X, Y, Z)
U4_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) =
U1_aaa(
x2)
true_in_ =
true_in_
true_out_ =
true_out_
p_out_aaa(
x1,
x2,
x3) =
p_out_aaa(
x3)
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
U3_aaa(
x1,
x2,
x3,
x4) =
U3_aaa(
x3,
x4)
=_in_aa(
x1,
x2) =
=_in_aa
=_out_aa(
x1,
x2) =
=_out_aa
U4_aaa(
x1,
x2,
x3,
x4) =
U4_aaa(
x3,
x4)
p_in_aag(
x1,
x2,
x3) =
p_in_aag(
x3)
U1_aag(
x1,
x2) =
U1_aag(
x2)
p_out_aag(
x1,
x2,
x3) =
p_out_aag
U2_aag(
x1,
x2,
x3,
x4) =
U2_aag(
x3,
x4)
=_in_gg(
x1,
x2) =
=_in_gg(
x1,
x2)
=_out_gg(
x1,
x2) =
=_out_gg
U3_aag(
x1,
x2,
x3,
x4) =
U3_aag(
x3,
x4)
U4_aag(
x1,
x2,
x3,
x4) =
U4_aag(
x4)
(35) 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, X, 1) → U1_AAA(X, true_in_)
P_IN_AAA(X, X, 1) → TRUE_IN_
P_IN_AAA(X, Y, Z) → U2_AAA(X, Y, Z, =_in_ag(Z, 1))
P_IN_AAA(X, Y, Z) → =_IN_AG(Z, 1)
U2_AAA(X, Y, Z, =_out_ag(Z, 1)) → U3_AAA(X, Y, Z, =_in_aa(Y, X))
U2_AAA(X, Y, Z, =_out_ag(Z, 1)) → =_IN_AA(Y, X)
U3_AAA(X, Y, Z, =_out_aa(Y, X)) → U4_AAA(X, Y, Z, p_in_aag(X, Y, Z))
U3_AAA(X, Y, Z, =_out_aa(Y, X)) → P_IN_AAG(X, Y, Z)
P_IN_AAG(X, X, 1) → U1_AAG(X, true_in_)
P_IN_AAG(X, X, 1) → TRUE_IN_
P_IN_AAG(X, Y, Z) → U2_AAG(X, Y, Z, =_in_gg(Z, 1))
P_IN_AAG(X, Y, Z) → =_IN_GG(Z, 1)
U2_AAG(X, Y, Z, =_out_gg(Z, 1)) → U3_AAG(X, Y, Z, =_in_aa(Y, X))
U2_AAG(X, Y, Z, =_out_gg(Z, 1)) → =_IN_AA(Y, X)
U3_AAG(X, Y, Z, =_out_aa(Y, X)) → U4_AAG(X, Y, Z, p_in_aag(X, Y, Z))
U3_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, X, 1) → U1_aaa(X, true_in_)
true_in_ → true_out_
U1_aaa(X, true_out_) → p_out_aaa(X, X, 1)
p_in_aaa(X, Y, Z) → 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)) → U3_aaa(X, Y, Z, =_in_aa(Y, X))
=_in_aa(X, X) → =_out_aa(X, X)
U3_aaa(X, Y, Z, =_out_aa(Y, X)) → U4_aaa(X, Y, Z, p_in_aag(X, Y, Z))
p_in_aag(X, X, 1) → U1_aag(X, true_in_)
U1_aag(X, true_out_) → p_out_aag(X, X, 1)
p_in_aag(X, Y, Z) → 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)) → U3_aag(X, Y, Z, =_in_aa(Y, X))
U3_aag(X, Y, Z, =_out_aa(Y, X)) → U4_aag(X, Y, Z, p_in_aag(X, Y, Z))
U4_aag(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aag(X, Y, Z)
U4_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) =
U1_aaa(
x2)
true_in_ =
true_in_
true_out_ =
true_out_
p_out_aaa(
x1,
x2,
x3) =
p_out_aaa(
x3)
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
U3_aaa(
x1,
x2,
x3,
x4) =
U3_aaa(
x3,
x4)
=_in_aa(
x1,
x2) =
=_in_aa
=_out_aa(
x1,
x2) =
=_out_aa
U4_aaa(
x1,
x2,
x3,
x4) =
U4_aaa(
x3,
x4)
p_in_aag(
x1,
x2,
x3) =
p_in_aag(
x3)
U1_aag(
x1,
x2) =
U1_aag(
x2)
p_out_aag(
x1,
x2,
x3) =
p_out_aag
U2_aag(
x1,
x2,
x3,
x4) =
U2_aag(
x3,
x4)
=_in_gg(
x1,
x2) =
=_in_gg(
x1,
x2)
=_out_gg(
x1,
x2) =
=_out_gg
U3_aag(
x1,
x2,
x3,
x4) =
U3_aag(
x3,
x4)
U4_aag(
x1,
x2,
x3,
x4) =
U4_aag(
x4)
P_IN_AAA(
x1,
x2,
x3) =
P_IN_AAA
U1_AAA(
x1,
x2) =
U1_AAA(
x2)
TRUE_IN_ =
TRUE_IN_
U2_AAA(
x1,
x2,
x3,
x4) =
U2_AAA(
x4)
=_IN_AG(
x1,
x2) =
=_IN_AG(
x2)
U3_AAA(
x1,
x2,
x3,
x4) =
U3_AAA(
x3,
x4)
=_IN_AA(
x1,
x2) =
=_IN_AA
U4_AAA(
x1,
x2,
x3,
x4) =
U4_AAA(
x3,
x4)
P_IN_AAG(
x1,
x2,
x3) =
P_IN_AAG(
x3)
U1_AAG(
x1,
x2) =
U1_AAG(
x2)
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(
x4)
We have to consider all (P,R,Pi)-chains
(36) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
P_IN_AAA(X, X, 1) → U1_AAA(X, true_in_)
P_IN_AAA(X, X, 1) → TRUE_IN_
P_IN_AAA(X, Y, Z) → U2_AAA(X, Y, Z, =_in_ag(Z, 1))
P_IN_AAA(X, Y, Z) → =_IN_AG(Z, 1)
U2_AAA(X, Y, Z, =_out_ag(Z, 1)) → U3_AAA(X, Y, Z, =_in_aa(Y, X))
U2_AAA(X, Y, Z, =_out_ag(Z, 1)) → =_IN_AA(Y, X)
U3_AAA(X, Y, Z, =_out_aa(Y, X)) → U4_AAA(X, Y, Z, p_in_aag(X, Y, Z))
U3_AAA(X, Y, Z, =_out_aa(Y, X)) → P_IN_AAG(X, Y, Z)
P_IN_AAG(X, X, 1) → U1_AAG(X, true_in_)
P_IN_AAG(X, X, 1) → TRUE_IN_
P_IN_AAG(X, Y, Z) → U2_AAG(X, Y, Z, =_in_gg(Z, 1))
P_IN_AAG(X, Y, Z) → =_IN_GG(Z, 1)
U2_AAG(X, Y, Z, =_out_gg(Z, 1)) → U3_AAG(X, Y, Z, =_in_aa(Y, X))
U2_AAG(X, Y, Z, =_out_gg(Z, 1)) → =_IN_AA(Y, X)
U3_AAG(X, Y, Z, =_out_aa(Y, X)) → U4_AAG(X, Y, Z, p_in_aag(X, Y, Z))
U3_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, X, 1) → U1_aaa(X, true_in_)
true_in_ → true_out_
U1_aaa(X, true_out_) → p_out_aaa(X, X, 1)
p_in_aaa(X, Y, Z) → 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)) → U3_aaa(X, Y, Z, =_in_aa(Y, X))
=_in_aa(X, X) → =_out_aa(X, X)
U3_aaa(X, Y, Z, =_out_aa(Y, X)) → U4_aaa(X, Y, Z, p_in_aag(X, Y, Z))
p_in_aag(X, X, 1) → U1_aag(X, true_in_)
U1_aag(X, true_out_) → p_out_aag(X, X, 1)
p_in_aag(X, Y, Z) → 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)) → U3_aag(X, Y, Z, =_in_aa(Y, X))
U3_aag(X, Y, Z, =_out_aa(Y, X)) → U4_aag(X, Y, Z, p_in_aag(X, Y, Z))
U4_aag(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aag(X, Y, Z)
U4_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) =
U1_aaa(
x2)
true_in_ =
true_in_
true_out_ =
true_out_
p_out_aaa(
x1,
x2,
x3) =
p_out_aaa(
x3)
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
U3_aaa(
x1,
x2,
x3,
x4) =
U3_aaa(
x3,
x4)
=_in_aa(
x1,
x2) =
=_in_aa
=_out_aa(
x1,
x2) =
=_out_aa
U4_aaa(
x1,
x2,
x3,
x4) =
U4_aaa(
x3,
x4)
p_in_aag(
x1,
x2,
x3) =
p_in_aag(
x3)
U1_aag(
x1,
x2) =
U1_aag(
x2)
p_out_aag(
x1,
x2,
x3) =
p_out_aag
U2_aag(
x1,
x2,
x3,
x4) =
U2_aag(
x3,
x4)
=_in_gg(
x1,
x2) =
=_in_gg(
x1,
x2)
=_out_gg(
x1,
x2) =
=_out_gg
U3_aag(
x1,
x2,
x3,
x4) =
U3_aag(
x3,
x4)
U4_aag(
x1,
x2,
x3,
x4) =
U4_aag(
x4)
P_IN_AAA(
x1,
x2,
x3) =
P_IN_AAA
U1_AAA(
x1,
x2) =
U1_AAA(
x2)
TRUE_IN_ =
TRUE_IN_
U2_AAA(
x1,
x2,
x3,
x4) =
U2_AAA(
x4)
=_IN_AG(
x1,
x2) =
=_IN_AG(
x2)
U3_AAA(
x1,
x2,
x3,
x4) =
U3_AAA(
x3,
x4)
=_IN_AA(
x1,
x2) =
=_IN_AA
U4_AAA(
x1,
x2,
x3,
x4) =
U4_AAA(
x3,
x4)
P_IN_AAG(
x1,
x2,
x3) =
P_IN_AAG(
x3)
U1_AAG(
x1,
x2) =
U1_AAG(
x2)
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(
x4)
We have to consider all (P,R,Pi)-chains
(37) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 13 less nodes.
(38) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
P_IN_AAG(X, Y, Z) → U2_AAG(X, Y, Z, =_in_gg(Z, 1))
U2_AAG(X, Y, Z, =_out_gg(Z, 1)) → U3_AAG(X, Y, Z, =_in_aa(Y, X))
U3_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, X, 1) → U1_aaa(X, true_in_)
true_in_ → true_out_
U1_aaa(X, true_out_) → p_out_aaa(X, X, 1)
p_in_aaa(X, Y, Z) → 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)) → U3_aaa(X, Y, Z, =_in_aa(Y, X))
=_in_aa(X, X) → =_out_aa(X, X)
U3_aaa(X, Y, Z, =_out_aa(Y, X)) → U4_aaa(X, Y, Z, p_in_aag(X, Y, Z))
p_in_aag(X, X, 1) → U1_aag(X, true_in_)
U1_aag(X, true_out_) → p_out_aag(X, X, 1)
p_in_aag(X, Y, Z) → 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)) → U3_aag(X, Y, Z, =_in_aa(Y, X))
U3_aag(X, Y, Z, =_out_aa(Y, X)) → U4_aag(X, Y, Z, p_in_aag(X, Y, Z))
U4_aag(X, Y, Z, p_out_aag(X, Y, Z)) → p_out_aag(X, Y, Z)
U4_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) =
U1_aaa(
x2)
true_in_ =
true_in_
true_out_ =
true_out_
p_out_aaa(
x1,
x2,
x3) =
p_out_aaa(
x3)
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
U3_aaa(
x1,
x2,
x3,
x4) =
U3_aaa(
x3,
x4)
=_in_aa(
x1,
x2) =
=_in_aa
=_out_aa(
x1,
x2) =
=_out_aa
U4_aaa(
x1,
x2,
x3,
x4) =
U4_aaa(
x3,
x4)
p_in_aag(
x1,
x2,
x3) =
p_in_aag(
x3)
U1_aag(
x1,
x2) =
U1_aag(
x2)
p_out_aag(
x1,
x2,
x3) =
p_out_aag
U2_aag(
x1,
x2,
x3,
x4) =
U2_aag(
x3,
x4)
=_in_gg(
x1,
x2) =
=_in_gg(
x1,
x2)
=_out_gg(
x1,
x2) =
=_out_gg
U3_aag(
x1,
x2,
x3,
x4) =
U3_aag(
x3,
x4)
U4_aag(
x1,
x2,
x3,
x4) =
U4_aag(
x4)
P_IN_AAG(
x1,
x2,
x3) =
P_IN_AAG(
x3)
U2_AAG(
x1,
x2,
x3,
x4) =
U2_AAG(
x3,
x4)
U3_AAG(
x1,
x2,
x3,
x4) =
U3_AAG(
x3,
x4)
We have to consider all (P,R,Pi)-chains
(39) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(40) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
P_IN_AAG(X, Y, Z) → U2_AAG(X, Y, Z, =_in_gg(Z, 1))
U2_AAG(X, Y, Z, =_out_gg(Z, 1)) → U3_AAG(X, Y, Z, =_in_aa(Y, X))
U3_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:
1 =
1
=_in_aa(
x1,
x2) =
=_in_aa
=_out_aa(
x1,
x2) =
=_out_aa
=_in_gg(
x1,
x2) =
=_in_gg(
x1,
x2)
=_out_gg(
x1,
x2) =
=_out_gg
P_IN_AAG(
x1,
x2,
x3) =
P_IN_AAG(
x3)
U2_AAG(
x1,
x2,
x3,
x4) =
U2_AAG(
x3,
x4)
U3_AAG(
x1,
x2,
x3,
x4) =
U3_AAG(
x3,
x4)
We have to consider all (P,R,Pi)-chains
(41) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(42) Obligation:
Q DP problem:
The TRS P consists of the following rules:
P_IN_AAG(Z) → U2_AAG(Z, =_in_gg(Z, 1))
U2_AAG(Z, =_out_gg) → U3_AAG(Z, =_in_aa)
U3_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.
(43) Rewriting (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
U2_AAG(
Z,
=_out_gg) →
U3_AAG(
Z,
=_in_aa) at position [1] we obtained the following new rules [LPAR04]:
U2_AAG(Z, =_out_gg) → U3_AAG(Z, =_out_aa)
(44) Obligation:
Q DP problem:
The TRS P consists of the following rules:
P_IN_AAG(Z) → U2_AAG(Z, =_in_gg(Z, 1))
U3_AAG(Z, =_out_aa) → P_IN_AAG(Z)
U2_AAG(Z, =_out_gg) → U3_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.
(45) 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.
(46) Obligation:
Q DP problem:
The TRS P consists of the following rules:
P_IN_AAG(Z) → U2_AAG(Z, =_in_gg(Z, 1))
U3_AAG(Z, =_out_aa) → P_IN_AAG(Z)
U2_AAG(Z, =_out_gg) → U3_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.
(47) 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
(48) Obligation:
Q DP problem:
The TRS P consists of the following rules:
P_IN_AAG(Z) → U2_AAG(Z, =_in_gg(Z, 1))
U3_AAG(Z, =_out_aa) → P_IN_AAG(Z)
U2_AAG(Z, =_out_gg) → U3_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.
(49) Narrowing (SOUND transformation)
By narrowing [LPAR04] the rule
P_IN_AAG(
Z) →
U2_AAG(
Z,
=_in_gg(
Z,
1)) at position [1] we obtained the following new rules [LPAR04]:
P_IN_AAG(1) → U2_AAG(1, =_out_gg)
(50) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_AAG(Z, =_out_aa) → P_IN_AAG(Z)
U2_AAG(Z, =_out_gg) → U3_AAG(Z, =_out_aa)
P_IN_AAG(1) → U2_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.
(51) 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.
(52) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_AAG(Z, =_out_aa) → P_IN_AAG(Z)
U2_AAG(Z, =_out_gg) → U3_AAG(Z, =_out_aa)
P_IN_AAG(1) → U2_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.
(53) 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)
(54) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_AAG(Z, =_out_aa) → P_IN_AAG(Z)
U2_AAG(Z, =_out_gg) → U3_AAG(Z, =_out_aa)
P_IN_AAG(1) → U2_AAG(1, =_out_gg)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(55) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U2_AAG(
Z,
=_out_gg) →
U3_AAG(
Z,
=_out_aa) we obtained the following new rules [LPAR04]:
U2_AAG(1, =_out_gg) → U3_AAG(1, =_out_aa)
(56) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_AAG(Z, =_out_aa) → P_IN_AAG(Z)
P_IN_AAG(1) → U2_AAG(1, =_out_gg)
U2_AAG(1, =_out_gg) → U3_AAG(1, =_out_aa)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(57) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U3_AAG(
Z,
=_out_aa) →
P_IN_AAG(
Z) we obtained the following new rules [LPAR04]:
U3_AAG(1, =_out_aa) → P_IN_AAG(1)
(58) Obligation:
Q DP problem:
The TRS P consists of the following rules:
P_IN_AAG(1) → U2_AAG(1, =_out_gg)
U2_AAG(1, =_out_gg) → U3_AAG(1, =_out_aa)
U3_AAG(1, =_out_aa) → P_IN_AAG(1)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(59) 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 =
U2_AAG(
1,
=_out_gg) evaluates to t =
U2_AAG(
1,
=_out_gg)
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Matcher: [ ]
- Semiunifier: [ ]
Rewriting sequenceU2_AAG(1, =_out_gg) →
U3_AAG(
1,
=_out_aa)
with rule
U2_AAG(
1,
=_out_gg) →
U3_AAG(
1,
=_out_aa) at position [] and matcher [ ]
U3_AAG(1, =_out_aa) →
P_IN_AAG(
1)
with rule
U3_AAG(
1,
=_out_aa) →
P_IN_AAG(
1) at position [] and matcher [ ]
P_IN_AAG(1) →
U2_AAG(
1,
=_out_gg)
with rule
P_IN_AAG(
1) →
U2_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.
(60) FALSE