0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 56 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 0 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 PiDP
↳7 UsableRulesProof (⇔, 0 ms)
↳8 PiDP
↳9 PiDPToQDPProof (⇔, 4 ms)
↳10 QDP
↳11 QDPSizeChangeProof (⇔, 0 ms)
↳12 YES
evenA_in_g(0) → evenA_out_g(0)
evenA_in_g(s(s(0))) → evenA_out_g(s(s(0)))
evenA_in_g(s(s(s(s(0))))) → evenA_out_g(s(s(s(s(0)))))
evenA_in_g(s(s(s(s(T6))))) → U1_g(T6, evenA_in_g(s(s(T6))))
U1_g(T6, evenA_out_g(s(s(T6)))) → evenA_out_g(s(s(s(s(T6)))))
EVENA_IN_G(s(s(s(s(T6))))) → U1_G(T6, evenA_in_g(s(s(T6))))
EVENA_IN_G(s(s(s(s(T6))))) → EVENA_IN_G(s(s(T6)))
evenA_in_g(0) → evenA_out_g(0)
evenA_in_g(s(s(0))) → evenA_out_g(s(s(0)))
evenA_in_g(s(s(s(s(0))))) → evenA_out_g(s(s(s(s(0)))))
evenA_in_g(s(s(s(s(T6))))) → U1_g(T6, evenA_in_g(s(s(T6))))
U1_g(T6, evenA_out_g(s(s(T6)))) → evenA_out_g(s(s(s(s(T6)))))
EVENA_IN_G(s(s(s(s(T6))))) → U1_G(T6, evenA_in_g(s(s(T6))))
EVENA_IN_G(s(s(s(s(T6))))) → EVENA_IN_G(s(s(T6)))
evenA_in_g(0) → evenA_out_g(0)
evenA_in_g(s(s(0))) → evenA_out_g(s(s(0)))
evenA_in_g(s(s(s(s(0))))) → evenA_out_g(s(s(s(s(0)))))
evenA_in_g(s(s(s(s(T6))))) → U1_g(T6, evenA_in_g(s(s(T6))))
U1_g(T6, evenA_out_g(s(s(T6)))) → evenA_out_g(s(s(s(s(T6)))))
EVENA_IN_G(s(s(s(s(T6))))) → EVENA_IN_G(s(s(T6)))
evenA_in_g(0) → evenA_out_g(0)
evenA_in_g(s(s(0))) → evenA_out_g(s(s(0)))
evenA_in_g(s(s(s(s(0))))) → evenA_out_g(s(s(s(s(0)))))
evenA_in_g(s(s(s(s(T6))))) → U1_g(T6, evenA_in_g(s(s(T6))))
U1_g(T6, evenA_out_g(s(s(T6)))) → evenA_out_g(s(s(s(s(T6)))))
EVENA_IN_G(s(s(s(s(T6))))) → EVENA_IN_G(s(s(T6)))
EVENA_IN_G(s(s(s(s(T6))))) → EVENA_IN_G(s(s(T6)))
From the DPs we obtained the following set of size-change graphs: