YES(?,O(1)) * Step 1: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. start(A,B) -> f0(A,B) True (1,1) 1. f0(A,B) -> f0(A,A) [A >= 1 && B = 0] (?,1) 2. f0(A,B) -> f0(A,A) [0 >= 1 + A && B = 0] (?,1) Signature: {(f0,2);(start,2)} Flow Graph: [0->{1,2},1->{1,2},2->{1,2}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,1),(1,2),(2,1),(2,2)] * Step 2: TrivialSCCs WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. start(A,B) -> f0(A,B) True (1,1) 1. f0(A,B) -> f0(A,A) [A >= 1 && B = 0] (?,1) 2. f0(A,B) -> f0(A,A) [0 >= 1 + A && B = 0] (?,1) Signature: {(f0,2);(start,2)} Flow Graph: [0->{1,2},1->{},2->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 3: KnowledgePropagation WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. start(A,B) -> f0(A,B) True (1,1) 1. f0(A,B) -> f0(A,A) [A >= 1 && B = 0] (1,1) 2. f0(A,B) -> f0(A,A) [0 >= 1 + A && B = 0] (1,1) Signature: {(f0,2);(start,2)} Flow Graph: [0->{1,2},1->{},2->{}] + Applied Processor: KnowledgePropagation + Details: The problem is already solved. YES(?,O(1))