NO * Step 1: FromIts NO + Considered Problem: Rules: 0. f4(A,B) -> f5(A,B) [B >= 0 && 0 >= 1 + A] (?,1) 1. f4(A,B) -> f5(A,B) [B >= 0 && A >= 1] (?,1) 2. f0(A,B) -> f4(C,0) True (1,1) 3. f5(A,B) -> f4(C,1 + B) [B >= 0 && 3 >= B] (?,1) 4. f5(A,B) -> f4(C,1 + B) [B >= 0 && B >= 5] (?,1) 5. f5(A,B) -> f4(C,1) [B >= 0 && B = 4] (?,1) 6. f4(A,B) -> f12(0,B) [B >= 0 && A = 0] (?,1) Signature: {(f0,2);(f12,2);(f4,2);(f5,2)} Flow Graph: [0->{3,4,5},1->{3,4,5},2->{0,1,6},3->{0,1,6},4->{0,1,6},5->{0,1,6},6->{}] + Applied Processor: FromIts + Details: () * Step 2: CloseWith NO + Considered Problem: Rules: f4(A,B) -> f5(A,B) [B >= 0 && 0 >= 1 + A] f4(A,B) -> f5(A,B) [B >= 0 && A >= 1] f0(A,B) -> f4(C,0) True f5(A,B) -> f4(C,1 + B) [B >= 0 && 3 >= B] f5(A,B) -> f4(C,1 + B) [B >= 0 && B >= 5] f5(A,B) -> f4(C,1) [B >= 0 && B = 4] f4(A,B) -> f12(0,B) [B >= 0 && A = 0] Signature: {(f0,2);(f12,2);(f4,2);(f5,2)} Rule Graph: [0->{3,4,5},1->{3,4,5},2->{0,1,6},3->{0,1,6},4->{0,1,6},5->{0,1,6},6->{}] + Applied Processor: CloseWith False + Details: () NO