0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 0 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 25 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 PiDP
↳7 PisEmptyProof (⇔, 0 ms)
↳8 YES
mapA_in_a(.(region(belize, T9, .(T10, [])), .(region(guatemala, T10, .(T9, .(T11, .(T12, [])))), .(region(el_salvador, T11, .(T10, .(T12, []))), .(region(honduras, T12, .(T10, .(T11, .(T13, [])))), .(region(nicaragua, T13, .(T12, .(T14, []))), .(region(costa_rica, T14, .(T13, .(T15, []))), .(region(panama, T15, .(T14, [])), [])))))))) → mapA_out_a(.(region(belize, T9, .(T10, [])), .(region(guatemala, T10, .(T9, .(T11, .(T12, [])))), .(region(el_salvador, T11, .(T10, .(T12, []))), .(region(honduras, T12, .(T10, .(T11, .(T13, [])))), .(region(nicaragua, T13, .(T12, .(T14, []))), .(region(costa_rica, T14, .(T13, .(T15, []))), .(region(panama, T15, .(T14, [])), []))))))))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
mapA_in_a(.(region(belize, T9, .(T10, [])), .(region(guatemala, T10, .(T9, .(T11, .(T12, [])))), .(region(el_salvador, T11, .(T10, .(T12, []))), .(region(honduras, T12, .(T10, .(T11, .(T13, [])))), .(region(nicaragua, T13, .(T12, .(T14, []))), .(region(costa_rica, T14, .(T13, .(T15, []))), .(region(panama, T15, .(T14, [])), [])))))))) → mapA_out_a(.(region(belize, T9, .(T10, [])), .(region(guatemala, T10, .(T9, .(T11, .(T12, [])))), .(region(el_salvador, T11, .(T10, .(T12, []))), .(region(honduras, T12, .(T10, .(T11, .(T13, [])))), .(region(nicaragua, T13, .(T12, .(T14, []))), .(region(costa_rica, T14, .(T13, .(T15, []))), .(region(panama, T15, .(T14, [])), []))))))))
mapA_in_a(.(region(belize, T9, .(T10, [])), .(region(guatemala, T10, .(T9, .(T11, .(T12, [])))), .(region(el_salvador, T11, .(T10, .(T12, []))), .(region(honduras, T12, .(T10, .(T11, .(T13, [])))), .(region(nicaragua, T13, .(T12, .(T14, []))), .(region(costa_rica, T14, .(T13, .(T15, []))), .(region(panama, T15, .(T14, [])), [])))))))) → mapA_out_a(.(region(belize, T9, .(T10, [])), .(region(guatemala, T10, .(T9, .(T11, .(T12, [])))), .(region(el_salvador, T11, .(T10, .(T12, []))), .(region(honduras, T12, .(T10, .(T11, .(T13, [])))), .(region(nicaragua, T13, .(T12, .(T14, []))), .(region(costa_rica, T14, .(T13, .(T15, []))), .(region(panama, T15, .(T14, [])), []))))))))
mapA_in_a(.(region(belize, T9, .(T10, [])), .(region(guatemala, T10, .(T9, .(T11, .(T12, [])))), .(region(el_salvador, T11, .(T10, .(T12, []))), .(region(honduras, T12, .(T10, .(T11, .(T13, [])))), .(region(nicaragua, T13, .(T12, .(T14, []))), .(region(costa_rica, T14, .(T13, .(T15, []))), .(region(panama, T15, .(T14, [])), [])))))))) → mapA_out_a(.(region(belize, T9, .(T10, [])), .(region(guatemala, T10, .(T9, .(T11, .(T12, [])))), .(region(el_salvador, T11, .(T10, .(T12, []))), .(region(honduras, T12, .(T10, .(T11, .(T13, [])))), .(region(nicaragua, T13, .(T12, .(T14, []))), .(region(costa_rica, T14, .(T13, .(T15, []))), .(region(panama, T15, .(T14, [])), []))))))))