(0) Obligation:
Clauses:max_valued(.(Head, Tail), Max) :- max_valued(Tail, Head, Max).
max_valued([], Term, Term).
max_valued(.(Head, Tail), Term, Max) :- ','(higher_valued(Head, Term), ','(!, max_valued(Tail, Head, Max))).
max_valued(.(Head, Tail), Term, Max) :- ','(higher_valued(Term, Head), max_valued(Tail, Term, Max)).
higher_valued(X, Y) :- greater(s(X), Y).
greater(s(X1), 0).
greater(s(X), s(Y)) :- greater(X, Y).
Queries:
max_valued(g,a).
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph.
(2) Obligation:
Triples:greater25(s(T70), s(T71)) :- greater25(T70, T71).
max_valued3(.(T29, T30), T31, T33) :- higher_valued15(T29, T31).
max_valued3(.(T29, T30), T31, T33) :- ','(higher_valuedc15(T29, T31), max_valued3(T30, T29, T33)).
max_valued3(.(T84, T85), T86, T88) :- higher_valued15(T86, T84).
max_valued3(.(T84, T85), T86, T88) :- ','(higher_valuedc15(T86, T84), max_valued3(T85, T86, T88)).
higher_valued15(T57, s(T58)) :- greater25(T57, T58).
max_valued1(.(T6, T7), T9) :- max_valued3(T7, T6, T9).
Clauses:
greaterc25(s(T65), 0).
greaterc25(s(T70), s(T71)) :- greaterc25(T70, T71).
max_valuedc3([], T12, T12).
max_valuedc3(.(T29, T30), T31, T33) :- ','(higher_valuedc15(T29, T31), max_valuedc3(T30, T29, T33)).
max_valuedc3(.(T84, T85), T86, T88) :- ','(higher_valuedc15(T86, T84), max_valuedc3(T85, T86, T88)).
higher_valuedc15(T52, 0).
higher_valuedc15(T57, s(T58)) :- greaterc25(T57, T58).
Afs:
max_valued1(x1, x2) = max_valued1(x1)
(3) TriplesToPiDPProof (SOUND transformation)
We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:max_valued1_in: (b,f)
max_valued3_in: (b,b,f)
higher_valued15_in: (b,b)
greater25_in: (b,b)
higher_valuedc15_in: (b,b)
greaterc25_in: (b,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
MAX_VALUED1_IN_GA(.(T6, T7), T9) → U9_GA(T6, T7, T9, max_valued3_in_gga(T7, T6, T9))
MAX_VALUED1_IN_GA(.(T6, T7), T9) → MAX_VALUED3_IN_GGA(T7, T6, T9)
MAX_VALUED3_IN_GGA(.(T29, T30), T31, T33) → U2_GGA(T29, T30, T31, T33, higher_valued15_in_gg(T29, T31))
MAX_VALUED3_IN_GGA(.(T29, T30), T31, T33) → HIGHER_VALUED15_IN_GG(T29, T31)
HIGHER_VALUED15_IN_GG(T57, s(T58)) → U8_GG(T57, T58, greater25_in_gg(T57, T58))
HIGHER_VALUED15_IN_GG(T57, s(T58)) → GREATER25_IN_GG(T57, T58)
GREATER25_IN_GG(s(T70), s(T71)) → U1_GG(T70, T71, greater25_in_gg(T70, T71))
GREATER25_IN_GG(s(T70), s(T71)) → GREATER25_IN_GG(T70, T71)
MAX_VALUED3_IN_GGA(.(T29, T30), T31, T33) → U3_GGA(T29, T30, T31, T33, higher_valuedc15_in_gg(T29, T31))
U3_GGA(T29, T30, T31, T33, higher_valuedc15_out_gg(T29, T31)) → U4_GGA(T29, T30, T31, T33, max_valued3_in_gga(T30, T29, T33))
U3_GGA(T29, T30, T31, T33, higher_valuedc15_out_gg(T29, T31)) → MAX_VALUED3_IN_GGA(T30, T29, T33)
MAX_VALUED3_IN_GGA(.(T84, T85), T86, T88) → U5_GGA(T84, T85, T86, T88, higher_valued15_in_gg(T86, T84))
MAX_VALUED3_IN_GGA(.(T84, T85), T86, T88) → HIGHER_VALUED15_IN_GG(T86, T84)
MAX_VALUED3_IN_GGA(.(T84, T85), T86, T88) → U6_GGA(T84, T85, T86, T88, higher_valuedc15_in_gg(T86, T84))
U6_GGA(T84, T85, T86, T88, higher_valuedc15_out_gg(T86, T84)) → U7_GGA(T84, T85, T86, T88, max_valued3_in_gga(T85, T86, T88))
U6_GGA(T84, T85, T86, T88, higher_valuedc15_out_gg(T86, T84)) → MAX_VALUED3_IN_GGA(T85, T86, T88)
The TRS R consists of the following rules:
higher_valuedc15_in_gg(T52, 0) → higher_valuedc15_out_gg(T52, 0)
higher_valuedc15_in_gg(T57, s(T58)) → U16_gg(T57, T58, greaterc25_in_gg(T57, T58))
greaterc25_in_gg(s(T65), 0) → greaterc25_out_gg(s(T65), 0)
greaterc25_in_gg(s(T70), s(T71)) → U11_gg(T70, T71, greaterc25_in_gg(T70, T71))
U11_gg(T70, T71, greaterc25_out_gg(T70, T71)) → greaterc25_out_gg(s(T70), s(T71))
U16_gg(T57, T58, greaterc25_out_gg(T57, T58)) → higher_valuedc15_out_gg(T57, s(T58))
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
max_valued3_in_gga(x1, x2, x3) = max_valued3_in_gga(x1, x2)
higher_valued15_in_gg(x1, x2) = higher_valued15_in_gg(x1, x2)
s(x1) = s(x1)
greater25_in_gg(x1, x2) = greater25_in_gg(x1, x2)
higher_valuedc15_in_gg(x1, x2) = higher_valuedc15_in_gg(x1, x2)
0 = 0
higher_valuedc15_out_gg(x1, x2) = higher_valuedc15_out_gg(x1, x2)
U16_gg(x1, x2, x3) = U16_gg(x1, x2, x3)
greaterc25_in_gg(x1, x2) = greaterc25_in_gg(x1, x2)
greaterc25_out_gg(x1, x2) = greaterc25_out_gg(x1, x2)
U11_gg(x1, x2, x3) = U11_gg(x1, x2, x3)
MAX_VALUED1_IN_GA(x1, x2) = MAX_VALUED1_IN_GA(x1)
U9_GA(x1, x2, x3, x4) = U9_GA(x1, x2, x4)
MAX_VALUED3_IN_GGA(x1, x2, x3) = MAX_VALUED3_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4, x5) = U2_GGA(x1, x2, x3, x5)
HIGHER_VALUED15_IN_GG(x1, x2) = HIGHER_VALUED15_IN_GG(x1, x2)
U8_GG(x1, x2, x3) = U8_GG(x1, x2, x3)
GREATER25_IN_GG(x1, x2) = GREATER25_IN_GG(x1, x2)
U1_GG(x1, x2, x3) = U1_GG(x1, x2, x3)
U3_GGA(x1, x2, x3, x4, x5) = U3_GGA(x1, x2, x3, x5)
U4_GGA(x1, x2, x3, x4, x5) = U4_GGA(x1, x2, x3, x5)
U5_GGA(x1, x2, x3, x4, x5) = U5_GGA(x1, x2, x3, x5)
U6_GGA(x1, x2, x3, x4, x5) = U6_GGA(x1, x2, x3, x5)
U7_GGA(x1, x2, x3, x4, x5) = U7_GGA(x1, x2, x3, x5)
We have to consider all (P,R,Pi)-chains
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
(4) Obligation:
Pi DP problem:The TRS P consists of the following rules:
MAX_VALUED1_IN_GA(.(T6, T7), T9) → U9_GA(T6, T7, T9, max_valued3_in_gga(T7, T6, T9))
MAX_VALUED1_IN_GA(.(T6, T7), T9) → MAX_VALUED3_IN_GGA(T7, T6, T9)
MAX_VALUED3_IN_GGA(.(T29, T30), T31, T33) → U2_GGA(T29, T30, T31, T33, higher_valued15_in_gg(T29, T31))
MAX_VALUED3_IN_GGA(.(T29, T30), T31, T33) → HIGHER_VALUED15_IN_GG(T29, T31)
HIGHER_VALUED15_IN_GG(T57, s(T58)) → U8_GG(T57, T58, greater25_in_gg(T57, T58))
HIGHER_VALUED15_IN_GG(T57, s(T58)) → GREATER25_IN_GG(T57, T58)
GREATER25_IN_GG(s(T70), s(T71)) → U1_GG(T70, T71, greater25_in_gg(T70, T71))
GREATER25_IN_GG(s(T70), s(T71)) → GREATER25_IN_GG(T70, T71)
MAX_VALUED3_IN_GGA(.(T29, T30), T31, T33) → U3_GGA(T29, T30, T31, T33, higher_valuedc15_in_gg(T29, T31))
U3_GGA(T29, T30, T31, T33, higher_valuedc15_out_gg(T29, T31)) → U4_GGA(T29, T30, T31, T33, max_valued3_in_gga(T30, T29, T33))
U3_GGA(T29, T30, T31, T33, higher_valuedc15_out_gg(T29, T31)) → MAX_VALUED3_IN_GGA(T30, T29, T33)
MAX_VALUED3_IN_GGA(.(T84, T85), T86, T88) → U5_GGA(T84, T85, T86, T88, higher_valued15_in_gg(T86, T84))
MAX_VALUED3_IN_GGA(.(T84, T85), T86, T88) → HIGHER_VALUED15_IN_GG(T86, T84)
MAX_VALUED3_IN_GGA(.(T84, T85), T86, T88) → U6_GGA(T84, T85, T86, T88, higher_valuedc15_in_gg(T86, T84))
U6_GGA(T84, T85, T86, T88, higher_valuedc15_out_gg(T86, T84)) → U7_GGA(T84, T85, T86, T88, max_valued3_in_gga(T85, T86, T88))
U6_GGA(T84, T85, T86, T88, higher_valuedc15_out_gg(T86, T84)) → MAX_VALUED3_IN_GGA(T85, T86, T88)
The TRS R consists of the following rules:
higher_valuedc15_in_gg(T52, 0) → higher_valuedc15_out_gg(T52, 0)
higher_valuedc15_in_gg(T57, s(T58)) → U16_gg(T57, T58, greaterc25_in_gg(T57, T58))
greaterc25_in_gg(s(T65), 0) → greaterc25_out_gg(s(T65), 0)
greaterc25_in_gg(s(T70), s(T71)) → U11_gg(T70, T71, greaterc25_in_gg(T70, T71))
U11_gg(T70, T71, greaterc25_out_gg(T70, T71)) → greaterc25_out_gg(s(T70), s(T71))
U16_gg(T57, T58, greaterc25_out_gg(T57, T58)) → higher_valuedc15_out_gg(T57, s(T58))
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
max_valued3_in_gga(x1, x2, x3) = max_valued3_in_gga(x1, x2)
higher_valued15_in_gg(x1, x2) = higher_valued15_in_gg(x1, x2)
s(x1) = s(x1)
greater25_in_gg(x1, x2) = greater25_in_gg(x1, x2)
higher_valuedc15_in_gg(x1, x2) = higher_valuedc15_in_gg(x1, x2)
0 = 0
higher_valuedc15_out_gg(x1, x2) = higher_valuedc15_out_gg(x1, x2)
U16_gg(x1, x2, x3) = U16_gg(x1, x2, x3)
greaterc25_in_gg(x1, x2) = greaterc25_in_gg(x1, x2)
greaterc25_out_gg(x1, x2) = greaterc25_out_gg(x1, x2)
U11_gg(x1, x2, x3) = U11_gg(x1, x2, x3)
MAX_VALUED1_IN_GA(x1, x2) = MAX_VALUED1_IN_GA(x1)
U9_GA(x1, x2, x3, x4) = U9_GA(x1, x2, x4)
MAX_VALUED3_IN_GGA(x1, x2, x3) = MAX_VALUED3_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4, x5) = U2_GGA(x1, x2, x3, x5)
HIGHER_VALUED15_IN_GG(x1, x2) = HIGHER_VALUED15_IN_GG(x1, x2)
U8_GG(x1, x2, x3) = U8_GG(x1, x2, x3)
GREATER25_IN_GG(x1, x2) = GREATER25_IN_GG(x1, x2)
U1_GG(x1, x2, x3) = U1_GG(x1, x2, x3)
U3_GGA(x1, x2, x3, x4, x5) = U3_GGA(x1, x2, x3, x5)
U4_GGA(x1, x2, x3, x4, x5) = U4_GGA(x1, x2, x3, x5)
U5_GGA(x1, x2, x3, x4, x5) = U5_GGA(x1, x2, x3, x5)
U6_GGA(x1, x2, x3, x4, x5) = U6_GGA(x1, x2, x3, x5)
U7_GGA(x1, x2, x3, x4, x5) = U7_GGA(x1, x2, x3, x5)
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 11 less nodes.(6) Complex Obligation (AND)
(7) Obligation:
Pi DP problem:The TRS P consists of the following rules:
GREATER25_IN_GG(s(T70), s(T71)) → GREATER25_IN_GG(T70, T71)
The TRS R consists of the following rules:
higher_valuedc15_in_gg(T52, 0) → higher_valuedc15_out_gg(T52, 0)
higher_valuedc15_in_gg(T57, s(T58)) → U16_gg(T57, T58, greaterc25_in_gg(T57, T58))
greaterc25_in_gg(s(T65), 0) → greaterc25_out_gg(s(T65), 0)
greaterc25_in_gg(s(T70), s(T71)) → U11_gg(T70, T71, greaterc25_in_gg(T70, T71))
U11_gg(T70, T71, greaterc25_out_gg(T70, T71)) → greaterc25_out_gg(s(T70), s(T71))
U16_gg(T57, T58, greaterc25_out_gg(T57, T58)) → higher_valuedc15_out_gg(T57, s(T58))
Pi is empty.
We have to consider all (P,R,Pi)-chains
(8) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.(9) Obligation:
Pi DP problem:The TRS P consists of the following rules:
GREATER25_IN_GG(s(T70), s(T71)) → GREATER25_IN_GG(T70, T71)
R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
(10) PiDPToQDPProof (EQUIVALENT transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(11) Obligation:
Q DP problem:The TRS P consists of the following rules:
GREATER25_IN_GG(s(T70), s(T71)) → GREATER25_IN_GG(T70, T71)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(12) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.From the DPs we obtained the following set of size-change graphs:
- GREATER25_IN_GG(s(T70), s(T71)) → GREATER25_IN_GG(T70, T71)
The graph contains the following edges 1 > 1, 2 > 2
(13) YES
(14) Obligation:
Pi DP problem:The TRS P consists of the following rules:
MAX_VALUED3_IN_GGA(.(T29, T30), T31, T33) → U3_GGA(T29, T30, T31, T33, higher_valuedc15_in_gg(T29, T31))
U3_GGA(T29, T30, T31, T33, higher_valuedc15_out_gg(T29, T31)) → MAX_VALUED3_IN_GGA(T30, T29, T33)
MAX_VALUED3_IN_GGA(.(T84, T85), T86, T88) → U6_GGA(T84, T85, T86, T88, higher_valuedc15_in_gg(T86, T84))
U6_GGA(T84, T85, T86, T88, higher_valuedc15_out_gg(T86, T84)) → MAX_VALUED3_IN_GGA(T85, T86, T88)
The TRS R consists of the following rules:
higher_valuedc15_in_gg(T52, 0) → higher_valuedc15_out_gg(T52, 0)
higher_valuedc15_in_gg(T57, s(T58)) → U16_gg(T57, T58, greaterc25_in_gg(T57, T58))
greaterc25_in_gg(s(T65), 0) → greaterc25_out_gg(s(T65), 0)
greaterc25_in_gg(s(T70), s(T71)) → U11_gg(T70, T71, greaterc25_in_gg(T70, T71))
U11_gg(T70, T71, greaterc25_out_gg(T70, T71)) → greaterc25_out_gg(s(T70), s(T71))
U16_gg(T57, T58, greaterc25_out_gg(T57, T58)) → higher_valuedc15_out_gg(T57, s(T58))
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
s(x1) = s(x1)
higher_valuedc15_in_gg(x1, x2) = higher_valuedc15_in_gg(x1, x2)
0 = 0
higher_valuedc15_out_gg(x1, x2) = higher_valuedc15_out_gg(x1, x2)
U16_gg(x1, x2, x3) = U16_gg(x1, x2, x3)
greaterc25_in_gg(x1, x2) = greaterc25_in_gg(x1, x2)
greaterc25_out_gg(x1, x2) = greaterc25_out_gg(x1, x2)
U11_gg(x1, x2, x3) = U11_gg(x1, x2, x3)
MAX_VALUED3_IN_GGA(x1, x2, x3) = MAX_VALUED3_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4, x5) = U3_GGA(x1, x2, x3, x5)
U6_GGA(x1, x2, x3, x4, x5) = U6_GGA(x1, x2, x3, x5)
We have to consider all (P,R,Pi)-chains
(15) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(16) Obligation:
Q DP problem:The TRS P consists of the following rules:
MAX_VALUED3_IN_GGA(.(T29, T30), T31) → U3_GGA(T29, T30, T31, higher_valuedc15_in_gg(T29, T31))
U3_GGA(T29, T30, T31, higher_valuedc15_out_gg(T29, T31)) → MAX_VALUED3_IN_GGA(T30, T29)
MAX_VALUED3_IN_GGA(.(T84, T85), T86) → U6_GGA(T84, T85, T86, higher_valuedc15_in_gg(T86, T84))
U6_GGA(T84, T85, T86, higher_valuedc15_out_gg(T86, T84)) → MAX_VALUED3_IN_GGA(T85, T86)
The TRS R consists of the following rules:
higher_valuedc15_in_gg(T52, 0) → higher_valuedc15_out_gg(T52, 0)
higher_valuedc15_in_gg(T57, s(T58)) → U16_gg(T57, T58, greaterc25_in_gg(T57, T58))
greaterc25_in_gg(s(T65), 0) → greaterc25_out_gg(s(T65), 0)
greaterc25_in_gg(s(T70), s(T71)) → U11_gg(T70, T71, greaterc25_in_gg(T70, T71))
U11_gg(T70, T71, greaterc25_out_gg(T70, T71)) → greaterc25_out_gg(s(T70), s(T71))
U16_gg(T57, T58, greaterc25_out_gg(T57, T58)) → higher_valuedc15_out_gg(T57, s(T58))
The set Q consists of the following terms:
higher_valuedc15_in_gg(x0, x1)
greaterc25_in_gg(x0, x1)
U11_gg(x0, x1, x2)
U16_gg(x0, x1, x2)
We have to consider all (P,Q,R)-chains.
(17) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.From the DPs we obtained the following set of size-change graphs:
- U3_GGA(T29, T30, T31, higher_valuedc15_out_gg(T29, T31)) → MAX_VALUED3_IN_GGA(T30, T29)
The graph contains the following edges 2 >= 1, 1 >= 2, 4 > 2 - U6_GGA(T84, T85, T86, higher_valuedc15_out_gg(T86, T84)) → MAX_VALUED3_IN_GGA(T85, T86)
The graph contains the following edges 2 >= 1, 3 >= 2, 4 > 2 - MAX_VALUED3_IN_GGA(.(T29, T30), T31) → U3_GGA(T29, T30, T31, higher_valuedc15_in_gg(T29, T31))
The graph contains the following edges 1 > 1, 1 > 2, 2 >= 3 - MAX_VALUED3_IN_GGA(.(T84, T85), T86) → U6_GGA(T84, T85, T86, higher_valuedc15_in_gg(T86, T84))
The graph contains the following edges 1 > 1, 1 > 2, 2 >= 3