0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇐)
↳2 Prolog
↳3 PrologToPiTRSProof (⇐)
↳4 PiTRS
↳5 DependencyPairsProof (⇔)
↳6 PiDP
↳7 DependencyGraphProof (⇔)
↳8 PiDP
↳9 UsableRulesProof (⇔)
↳10 PiDP
↳11 PiDPToQDPProof (⇐)
↳12 QDP
↳13 QDPSizeChangeProof (⇔)
↳14 TRUE
rev1_in_ga([], []) → rev1_out_ga([], [])
rev1_in_ga(.(T18, []), .(T18, [])) → rev1_out_ga(.(T18, []), .(T18, []))
rev1_in_ga(.(T32, .(T31, [])), .(T31, .(T32, []))) → rev1_out_ga(.(T32, .(T31, [])), .(T31, .(T32, [])))
rev1_in_ga(.(T49, .(T48, .(T47, []))), .(T47, .(T48, .(T49, [])))) → rev1_out_ga(.(T49, .(T48, .(T47, []))), .(T47, .(T48, .(T49, []))))
rev1_in_ga(.(T69, .(T68, .(T67, .(T66, [])))), .(T66, .(T67, .(T68, .(T69, []))))) → rev1_out_ga(.(T69, .(T68, .(T67, .(T66, [])))), .(T66, .(T67, .(T68, .(T69, [])))))
rev1_in_ga(.(T92, .(T91, .(T90, .(T89, .(T88, []))))), .(T88, .(T89, .(T90, .(T91, .(T92, [])))))) → rev1_out_ga(.(T92, .(T91, .(T90, .(T89, .(T88, []))))), .(T88, .(T89, .(T90, .(T91, .(T92, []))))))
rev1_in_ga(.(T118, .(T117, .(T116, .(T115, .(T114, .(T113, [])))))), .(T113, .(T114, .(T115, .(T116, .(T117, .(T118, []))))))) → rev1_out_ga(.(T118, .(T117, .(T116, .(T115, .(T114, .(T113, [])))))), .(T113, .(T114, .(T115, .(T116, .(T117, .(T118, [])))))))
rev1_in_ga(.(T125, .(T124, .(T123, .(T122, .(T121, .(T120, .(T130, []))))))), .(T138, T139)) → rev1_out_ga(.(T125, .(T124, .(T123, .(T122, .(T121, .(T120, .(T130, []))))))), .(T138, T139))
rev1_in_ga(.(T125, .(T124, .(T123, .(T122, .(T121, .(T120, .(T130, .(T147, T148)))))))), T144) → U2_ga(T125, T124, T123, T122, T121, T120, T130, T147, T148, T144, rev116_in_gaaa(T148, T147, .(T141, T142), T144))
rev116_in_gaaa([], T138, T139, .(T138, T139)) → rev116_out_gaaa([], T138, T139, .(T138, T139))
rev116_in_gaaa(.(T147, T148), T141, T142, T144) → U1_gaaa(T147, T148, T141, T142, T144, rev116_in_gaaa(T148, T147, .(T141, T142), T144))
U1_gaaa(T147, T148, T141, T142, T144, rev116_out_gaaa(T148, T147, .(T141, T142), T144)) → rev116_out_gaaa(.(T147, T148), T141, T142, T144)
U2_ga(T125, T124, T123, T122, T121, T120, T130, T147, T148, T144, rev116_out_gaaa(T148, T147, .(T141, T142), T144)) → rev1_out_ga(.(T125, .(T124, .(T123, .(T122, .(T121, .(T120, .(T130, .(T147, T148)))))))), T144)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
rev1_in_ga([], []) → rev1_out_ga([], [])
rev1_in_ga(.(T18, []), .(T18, [])) → rev1_out_ga(.(T18, []), .(T18, []))
rev1_in_ga(.(T32, .(T31, [])), .(T31, .(T32, []))) → rev1_out_ga(.(T32, .(T31, [])), .(T31, .(T32, [])))
rev1_in_ga(.(T49, .(T48, .(T47, []))), .(T47, .(T48, .(T49, [])))) → rev1_out_ga(.(T49, .(T48, .(T47, []))), .(T47, .(T48, .(T49, []))))
rev1_in_ga(.(T69, .(T68, .(T67, .(T66, [])))), .(T66, .(T67, .(T68, .(T69, []))))) → rev1_out_ga(.(T69, .(T68, .(T67, .(T66, [])))), .(T66, .(T67, .(T68, .(T69, [])))))
rev1_in_ga(.(T92, .(T91, .(T90, .(T89, .(T88, []))))), .(T88, .(T89, .(T90, .(T91, .(T92, [])))))) → rev1_out_ga(.(T92, .(T91, .(T90, .(T89, .(T88, []))))), .(T88, .(T89, .(T90, .(T91, .(T92, []))))))
rev1_in_ga(.(T118, .(T117, .(T116, .(T115, .(T114, .(T113, [])))))), .(T113, .(T114, .(T115, .(T116, .(T117, .(T118, []))))))) → rev1_out_ga(.(T118, .(T117, .(T116, .(T115, .(T114, .(T113, [])))))), .(T113, .(T114, .(T115, .(T116, .(T117, .(T118, [])))))))
rev1_in_ga(.(T125, .(T124, .(T123, .(T122, .(T121, .(T120, .(T130, []))))))), .(T138, T139)) → rev1_out_ga(.(T125, .(T124, .(T123, .(T122, .(T121, .(T120, .(T130, []))))))), .(T138, T139))
rev1_in_ga(.(T125, .(T124, .(T123, .(T122, .(T121, .(T120, .(T130, .(T147, T148)))))))), T144) → U2_ga(T125, T124, T123, T122, T121, T120, T130, T147, T148, T144, rev116_in_gaaa(T148, T147, .(T141, T142), T144))
rev116_in_gaaa([], T138, T139, .(T138, T139)) → rev116_out_gaaa([], T138, T139, .(T138, T139))
rev116_in_gaaa(.(T147, T148), T141, T142, T144) → U1_gaaa(T147, T148, T141, T142, T144, rev116_in_gaaa(T148, T147, .(T141, T142), T144))
U1_gaaa(T147, T148, T141, T142, T144, rev116_out_gaaa(T148, T147, .(T141, T142), T144)) → rev116_out_gaaa(.(T147, T148), T141, T142, T144)
U2_ga(T125, T124, T123, T122, T121, T120, T130, T147, T148, T144, rev116_out_gaaa(T148, T147, .(T141, T142), T144)) → rev1_out_ga(.(T125, .(T124, .(T123, .(T122, .(T121, .(T120, .(T130, .(T147, T148)))))))), T144)
REV1_IN_GA(.(T125, .(T124, .(T123, .(T122, .(T121, .(T120, .(T130, .(T147, T148)))))))), T144) → U2_GA(T125, T124, T123, T122, T121, T120, T130, T147, T148, T144, rev116_in_gaaa(T148, T147, .(T141, T142), T144))
REV1_IN_GA(.(T125, .(T124, .(T123, .(T122, .(T121, .(T120, .(T130, .(T147, T148)))))))), T144) → REV116_IN_GAAA(T148, T147, .(T141, T142), T144)
REV116_IN_GAAA(.(T147, T148), T141, T142, T144) → U1_GAAA(T147, T148, T141, T142, T144, rev116_in_gaaa(T148, T147, .(T141, T142), T144))
REV116_IN_GAAA(.(T147, T148), T141, T142, T144) → REV116_IN_GAAA(T148, T147, .(T141, T142), T144)
rev1_in_ga([], []) → rev1_out_ga([], [])
rev1_in_ga(.(T18, []), .(T18, [])) → rev1_out_ga(.(T18, []), .(T18, []))
rev1_in_ga(.(T32, .(T31, [])), .(T31, .(T32, []))) → rev1_out_ga(.(T32, .(T31, [])), .(T31, .(T32, [])))
rev1_in_ga(.(T49, .(T48, .(T47, []))), .(T47, .(T48, .(T49, [])))) → rev1_out_ga(.(T49, .(T48, .(T47, []))), .(T47, .(T48, .(T49, []))))
rev1_in_ga(.(T69, .(T68, .(T67, .(T66, [])))), .(T66, .(T67, .(T68, .(T69, []))))) → rev1_out_ga(.(T69, .(T68, .(T67, .(T66, [])))), .(T66, .(T67, .(T68, .(T69, [])))))
rev1_in_ga(.(T92, .(T91, .(T90, .(T89, .(T88, []))))), .(T88, .(T89, .(T90, .(T91, .(T92, [])))))) → rev1_out_ga(.(T92, .(T91, .(T90, .(T89, .(T88, []))))), .(T88, .(T89, .(T90, .(T91, .(T92, []))))))
rev1_in_ga(.(T118, .(T117, .(T116, .(T115, .(T114, .(T113, [])))))), .(T113, .(T114, .(T115, .(T116, .(T117, .(T118, []))))))) → rev1_out_ga(.(T118, .(T117, .(T116, .(T115, .(T114, .(T113, [])))))), .(T113, .(T114, .(T115, .(T116, .(T117, .(T118, [])))))))
rev1_in_ga(.(T125, .(T124, .(T123, .(T122, .(T121, .(T120, .(T130, []))))))), .(T138, T139)) → rev1_out_ga(.(T125, .(T124, .(T123, .(T122, .(T121, .(T120, .(T130, []))))))), .(T138, T139))
rev1_in_ga(.(T125, .(T124, .(T123, .(T122, .(T121, .(T120, .(T130, .(T147, T148)))))))), T144) → U2_ga(T125, T124, T123, T122, T121, T120, T130, T147, T148, T144, rev116_in_gaaa(T148, T147, .(T141, T142), T144))
rev116_in_gaaa([], T138, T139, .(T138, T139)) → rev116_out_gaaa([], T138, T139, .(T138, T139))
rev116_in_gaaa(.(T147, T148), T141, T142, T144) → U1_gaaa(T147, T148, T141, T142, T144, rev116_in_gaaa(T148, T147, .(T141, T142), T144))
U1_gaaa(T147, T148, T141, T142, T144, rev116_out_gaaa(T148, T147, .(T141, T142), T144)) → rev116_out_gaaa(.(T147, T148), T141, T142, T144)
U2_ga(T125, T124, T123, T122, T121, T120, T130, T147, T148, T144, rev116_out_gaaa(T148, T147, .(T141, T142), T144)) → rev1_out_ga(.(T125, .(T124, .(T123, .(T122, .(T121, .(T120, .(T130, .(T147, T148)))))))), T144)
REV1_IN_GA(.(T125, .(T124, .(T123, .(T122, .(T121, .(T120, .(T130, .(T147, T148)))))))), T144) → U2_GA(T125, T124, T123, T122, T121, T120, T130, T147, T148, T144, rev116_in_gaaa(T148, T147, .(T141, T142), T144))
REV1_IN_GA(.(T125, .(T124, .(T123, .(T122, .(T121, .(T120, .(T130, .(T147, T148)))))))), T144) → REV116_IN_GAAA(T148, T147, .(T141, T142), T144)
REV116_IN_GAAA(.(T147, T148), T141, T142, T144) → U1_GAAA(T147, T148, T141, T142, T144, rev116_in_gaaa(T148, T147, .(T141, T142), T144))
REV116_IN_GAAA(.(T147, T148), T141, T142, T144) → REV116_IN_GAAA(T148, T147, .(T141, T142), T144)
rev1_in_ga([], []) → rev1_out_ga([], [])
rev1_in_ga(.(T18, []), .(T18, [])) → rev1_out_ga(.(T18, []), .(T18, []))
rev1_in_ga(.(T32, .(T31, [])), .(T31, .(T32, []))) → rev1_out_ga(.(T32, .(T31, [])), .(T31, .(T32, [])))
rev1_in_ga(.(T49, .(T48, .(T47, []))), .(T47, .(T48, .(T49, [])))) → rev1_out_ga(.(T49, .(T48, .(T47, []))), .(T47, .(T48, .(T49, []))))
rev1_in_ga(.(T69, .(T68, .(T67, .(T66, [])))), .(T66, .(T67, .(T68, .(T69, []))))) → rev1_out_ga(.(T69, .(T68, .(T67, .(T66, [])))), .(T66, .(T67, .(T68, .(T69, [])))))
rev1_in_ga(.(T92, .(T91, .(T90, .(T89, .(T88, []))))), .(T88, .(T89, .(T90, .(T91, .(T92, [])))))) → rev1_out_ga(.(T92, .(T91, .(T90, .(T89, .(T88, []))))), .(T88, .(T89, .(T90, .(T91, .(T92, []))))))
rev1_in_ga(.(T118, .(T117, .(T116, .(T115, .(T114, .(T113, [])))))), .(T113, .(T114, .(T115, .(T116, .(T117, .(T118, []))))))) → rev1_out_ga(.(T118, .(T117, .(T116, .(T115, .(T114, .(T113, [])))))), .(T113, .(T114, .(T115, .(T116, .(T117, .(T118, [])))))))
rev1_in_ga(.(T125, .(T124, .(T123, .(T122, .(T121, .(T120, .(T130, []))))))), .(T138, T139)) → rev1_out_ga(.(T125, .(T124, .(T123, .(T122, .(T121, .(T120, .(T130, []))))))), .(T138, T139))
rev1_in_ga(.(T125, .(T124, .(T123, .(T122, .(T121, .(T120, .(T130, .(T147, T148)))))))), T144) → U2_ga(T125, T124, T123, T122, T121, T120, T130, T147, T148, T144, rev116_in_gaaa(T148, T147, .(T141, T142), T144))
rev116_in_gaaa([], T138, T139, .(T138, T139)) → rev116_out_gaaa([], T138, T139, .(T138, T139))
rev116_in_gaaa(.(T147, T148), T141, T142, T144) → U1_gaaa(T147, T148, T141, T142, T144, rev116_in_gaaa(T148, T147, .(T141, T142), T144))
U1_gaaa(T147, T148, T141, T142, T144, rev116_out_gaaa(T148, T147, .(T141, T142), T144)) → rev116_out_gaaa(.(T147, T148), T141, T142, T144)
U2_ga(T125, T124, T123, T122, T121, T120, T130, T147, T148, T144, rev116_out_gaaa(T148, T147, .(T141, T142), T144)) → rev1_out_ga(.(T125, .(T124, .(T123, .(T122, .(T121, .(T120, .(T130, .(T147, T148)))))))), T144)
REV116_IN_GAAA(.(T147, T148), T141, T142, T144) → REV116_IN_GAAA(T148, T147, .(T141, T142), T144)
rev1_in_ga([], []) → rev1_out_ga([], [])
rev1_in_ga(.(T18, []), .(T18, [])) → rev1_out_ga(.(T18, []), .(T18, []))
rev1_in_ga(.(T32, .(T31, [])), .(T31, .(T32, []))) → rev1_out_ga(.(T32, .(T31, [])), .(T31, .(T32, [])))
rev1_in_ga(.(T49, .(T48, .(T47, []))), .(T47, .(T48, .(T49, [])))) → rev1_out_ga(.(T49, .(T48, .(T47, []))), .(T47, .(T48, .(T49, []))))
rev1_in_ga(.(T69, .(T68, .(T67, .(T66, [])))), .(T66, .(T67, .(T68, .(T69, []))))) → rev1_out_ga(.(T69, .(T68, .(T67, .(T66, [])))), .(T66, .(T67, .(T68, .(T69, [])))))
rev1_in_ga(.(T92, .(T91, .(T90, .(T89, .(T88, []))))), .(T88, .(T89, .(T90, .(T91, .(T92, [])))))) → rev1_out_ga(.(T92, .(T91, .(T90, .(T89, .(T88, []))))), .(T88, .(T89, .(T90, .(T91, .(T92, []))))))
rev1_in_ga(.(T118, .(T117, .(T116, .(T115, .(T114, .(T113, [])))))), .(T113, .(T114, .(T115, .(T116, .(T117, .(T118, []))))))) → rev1_out_ga(.(T118, .(T117, .(T116, .(T115, .(T114, .(T113, [])))))), .(T113, .(T114, .(T115, .(T116, .(T117, .(T118, [])))))))
rev1_in_ga(.(T125, .(T124, .(T123, .(T122, .(T121, .(T120, .(T130, []))))))), .(T138, T139)) → rev1_out_ga(.(T125, .(T124, .(T123, .(T122, .(T121, .(T120, .(T130, []))))))), .(T138, T139))
rev1_in_ga(.(T125, .(T124, .(T123, .(T122, .(T121, .(T120, .(T130, .(T147, T148)))))))), T144) → U2_ga(T125, T124, T123, T122, T121, T120, T130, T147, T148, T144, rev116_in_gaaa(T148, T147, .(T141, T142), T144))
rev116_in_gaaa([], T138, T139, .(T138, T139)) → rev116_out_gaaa([], T138, T139, .(T138, T139))
rev116_in_gaaa(.(T147, T148), T141, T142, T144) → U1_gaaa(T147, T148, T141, T142, T144, rev116_in_gaaa(T148, T147, .(T141, T142), T144))
U1_gaaa(T147, T148, T141, T142, T144, rev116_out_gaaa(T148, T147, .(T141, T142), T144)) → rev116_out_gaaa(.(T147, T148), T141, T142, T144)
U2_ga(T125, T124, T123, T122, T121, T120, T130, T147, T148, T144, rev116_out_gaaa(T148, T147, .(T141, T142), T144)) → rev1_out_ga(.(T125, .(T124, .(T123, .(T122, .(T121, .(T120, .(T130, .(T147, T148)))))))), T144)
REV116_IN_GAAA(.(T147, T148), T141, T142, T144) → REV116_IN_GAAA(T148, T147, .(T141, T142), T144)
REV116_IN_GAAA(.(T148)) → REV116_IN_GAAA(T148)
From the DPs we obtained the following set of size-change graphs: