YES
Left Termination proof of ../tpdb/LP/SGST06/at.pl
Left Termination of the query pattern
at_in_2(a, a)
w.r.t. the given Prolog program could successfully be proven:
↳ Prolog
↳ PrologToPiTRSProof
Clauses:
at(X, fido) :- ','(at(X, mary), near(X)).
at(ta, mary).
at(jm, mary).
near(jm).
Queries:
at(a,a).
We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
at_in: (f,f) (f,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
at_in_aa(X, fido) → U1_aa(X, at_in_ag(X, mary))
at_in_ag(X, fido) → U1_ag(X, at_in_ag(X, mary))
at_in_ag(ta, mary) → at_out_ag(ta, mary)
at_in_ag(jm, mary) → at_out_ag(jm, mary)
U1_ag(X, at_out_ag(X, mary)) → U2_ag(X, near_in_g(X))
near_in_g(jm) → near_out_g(jm)
U2_ag(X, near_out_g(X)) → at_out_ag(X, fido)
U1_aa(X, at_out_ag(X, mary)) → U2_aa(X, near_in_g(X))
U2_aa(X, near_out_g(X)) → at_out_aa(X, fido)
at_in_aa(ta, mary) → at_out_aa(ta, mary)
at_in_aa(jm, mary) → at_out_aa(jm, mary)
The argument filtering Pi contains the following mapping:
at_in_aa(x1, x2) = at_in_aa
U1_aa(x1, x2) = U1_aa(x2)
at_in_ag(x1, x2) = at_in_ag(x2)
fido = fido
U1_ag(x1, x2) = U1_ag(x2)
mary = mary
at_out_ag(x1, x2) = at_out_ag(x1)
U2_ag(x1, x2) = U2_ag(x1, x2)
near_in_g(x1) = near_in_g(x1)
jm = jm
near_out_g(x1) = near_out_g
U2_aa(x1, x2) = U2_aa(x1, x2)
at_out_aa(x1, x2) = at_out_aa(x1, x2)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
Pi-finite rewrite system:
The TRS R consists of the following rules:
at_in_aa(X, fido) → U1_aa(X, at_in_ag(X, mary))
at_in_ag(X, fido) → U1_ag(X, at_in_ag(X, mary))
at_in_ag(ta, mary) → at_out_ag(ta, mary)
at_in_ag(jm, mary) → at_out_ag(jm, mary)
U1_ag(X, at_out_ag(X, mary)) → U2_ag(X, near_in_g(X))
near_in_g(jm) → near_out_g(jm)
U2_ag(X, near_out_g(X)) → at_out_ag(X, fido)
U1_aa(X, at_out_ag(X, mary)) → U2_aa(X, near_in_g(X))
U2_aa(X, near_out_g(X)) → at_out_aa(X, fido)
at_in_aa(ta, mary) → at_out_aa(ta, mary)
at_in_aa(jm, mary) → at_out_aa(jm, mary)
The argument filtering Pi contains the following mapping:
at_in_aa(x1, x2) = at_in_aa
U1_aa(x1, x2) = U1_aa(x2)
at_in_ag(x1, x2) = at_in_ag(x2)
fido = fido
U1_ag(x1, x2) = U1_ag(x2)
mary = mary
at_out_ag(x1, x2) = at_out_ag(x1)
U2_ag(x1, x2) = U2_ag(x1, x2)
near_in_g(x1) = near_in_g(x1)
jm = jm
near_out_g(x1) = near_out_g
U2_aa(x1, x2) = U2_aa(x1, x2)
at_out_aa(x1, x2) = at_out_aa(x1, x2)
Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:
AT_IN_AA(X, fido) → U1_AA(X, at_in_ag(X, mary))
AT_IN_AA(X, fido) → AT_IN_AG(X, mary)
AT_IN_AG(X, fido) → U1_AG(X, at_in_ag(X, mary))
AT_IN_AG(X, fido) → AT_IN_AG(X, mary)
U1_AG(X, at_out_ag(X, mary)) → U2_AG(X, near_in_g(X))
U1_AG(X, at_out_ag(X, mary)) → NEAR_IN_G(X)
U1_AA(X, at_out_ag(X, mary)) → U2_AA(X, near_in_g(X))
U1_AA(X, at_out_ag(X, mary)) → NEAR_IN_G(X)
The TRS R consists of the following rules:
at_in_aa(X, fido) → U1_aa(X, at_in_ag(X, mary))
at_in_ag(X, fido) → U1_ag(X, at_in_ag(X, mary))
at_in_ag(ta, mary) → at_out_ag(ta, mary)
at_in_ag(jm, mary) → at_out_ag(jm, mary)
U1_ag(X, at_out_ag(X, mary)) → U2_ag(X, near_in_g(X))
near_in_g(jm) → near_out_g(jm)
U2_ag(X, near_out_g(X)) → at_out_ag(X, fido)
U1_aa(X, at_out_ag(X, mary)) → U2_aa(X, near_in_g(X))
U2_aa(X, near_out_g(X)) → at_out_aa(X, fido)
at_in_aa(ta, mary) → at_out_aa(ta, mary)
at_in_aa(jm, mary) → at_out_aa(jm, mary)
The argument filtering Pi contains the following mapping:
at_in_aa(x1, x2) = at_in_aa
U1_aa(x1, x2) = U1_aa(x2)
at_in_ag(x1, x2) = at_in_ag(x2)
fido = fido
U1_ag(x1, x2) = U1_ag(x2)
mary = mary
at_out_ag(x1, x2) = at_out_ag(x1)
U2_ag(x1, x2) = U2_ag(x1, x2)
near_in_g(x1) = near_in_g(x1)
jm = jm
near_out_g(x1) = near_out_g
U2_aa(x1, x2) = U2_aa(x1, x2)
at_out_aa(x1, x2) = at_out_aa(x1, x2)
AT_IN_AG(x1, x2) = AT_IN_AG(x2)
U2_AG(x1, x2) = U2_AG(x1, x2)
U1_AA(x1, x2) = U1_AA(x2)
U2_AA(x1, x2) = U2_AA(x1, x2)
NEAR_IN_G(x1) = NEAR_IN_G(x1)
AT_IN_AA(x1, x2) = AT_IN_AA
U1_AG(x1, x2) = U1_AG(x2)
We have to consider all (P,R,Pi)-chains
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
Pi DP problem:
The TRS P consists of the following rules:
AT_IN_AA(X, fido) → U1_AA(X, at_in_ag(X, mary))
AT_IN_AA(X, fido) → AT_IN_AG(X, mary)
AT_IN_AG(X, fido) → U1_AG(X, at_in_ag(X, mary))
AT_IN_AG(X, fido) → AT_IN_AG(X, mary)
U1_AG(X, at_out_ag(X, mary)) → U2_AG(X, near_in_g(X))
U1_AG(X, at_out_ag(X, mary)) → NEAR_IN_G(X)
U1_AA(X, at_out_ag(X, mary)) → U2_AA(X, near_in_g(X))
U1_AA(X, at_out_ag(X, mary)) → NEAR_IN_G(X)
The TRS R consists of the following rules:
at_in_aa(X, fido) → U1_aa(X, at_in_ag(X, mary))
at_in_ag(X, fido) → U1_ag(X, at_in_ag(X, mary))
at_in_ag(ta, mary) → at_out_ag(ta, mary)
at_in_ag(jm, mary) → at_out_ag(jm, mary)
U1_ag(X, at_out_ag(X, mary)) → U2_ag(X, near_in_g(X))
near_in_g(jm) → near_out_g(jm)
U2_ag(X, near_out_g(X)) → at_out_ag(X, fido)
U1_aa(X, at_out_ag(X, mary)) → U2_aa(X, near_in_g(X))
U2_aa(X, near_out_g(X)) → at_out_aa(X, fido)
at_in_aa(ta, mary) → at_out_aa(ta, mary)
at_in_aa(jm, mary) → at_out_aa(jm, mary)
The argument filtering Pi contains the following mapping:
at_in_aa(x1, x2) = at_in_aa
U1_aa(x1, x2) = U1_aa(x2)
at_in_ag(x1, x2) = at_in_ag(x2)
fido = fido
U1_ag(x1, x2) = U1_ag(x2)
mary = mary
at_out_ag(x1, x2) = at_out_ag(x1)
U2_ag(x1, x2) = U2_ag(x1, x2)
near_in_g(x1) = near_in_g(x1)
jm = jm
near_out_g(x1) = near_out_g
U2_aa(x1, x2) = U2_aa(x1, x2)
at_out_aa(x1, x2) = at_out_aa(x1, x2)
AT_IN_AG(x1, x2) = AT_IN_AG(x2)
U2_AG(x1, x2) = U2_AG(x1, x2)
U1_AA(x1, x2) = U1_AA(x2)
U2_AA(x1, x2) = U2_AA(x1, x2)
NEAR_IN_G(x1) = NEAR_IN_G(x1)
AT_IN_AA(x1, x2) = AT_IN_AA
U1_AG(x1, x2) = U1_AG(x2)
We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 0 SCCs with 8 less nodes.