MAYBE Time: 0.039284 TRS: { cond2(true(), x, y, z) -> cond1(or(gr(x, z), gr(y, z)), p x, y, z), cond2(false(), x, y, z) -> cond3(gr(y, 0()), x, y, z), gr(0(), x) -> false(), gr(s x, 0()) -> true(), gr(s x, s y) -> gr(x, y), cond1(true(), x, y, z) -> cond2(gr(x, 0()), x, y, z), or(x, true()) -> true(), or(true(), x) -> true(), or(false(), false()) -> false(), p 0() -> 0(), p s x -> x, cond3(true(), x, y, z) -> cond1(or(gr(x, z), gr(y, z)), x, p y, z), cond3(false(), x, y, z) -> cond1(or(gr(x, z), gr(y, z)), x, y, z)} DP: DP: { cond2#(true(), x, y, z) -> gr#(x, z), cond2#(true(), x, y, z) -> gr#(y, z), cond2#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), p x, y, z), cond2#(true(), x, y, z) -> or#(gr(x, z), gr(y, z)), cond2#(true(), x, y, z) -> p# x, cond2#(false(), x, y, z) -> gr#(y, 0()), cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), gr#(s x, s y) -> gr#(x, y), cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond1#(true(), x, y, z) -> gr#(x, 0()), cond3#(true(), x, y, z) -> gr#(x, z), cond3#(true(), x, y, z) -> gr#(y, z), cond3#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, p y, z), cond3#(true(), x, y, z) -> or#(gr(x, z), gr(y, z)), cond3#(true(), x, y, z) -> p# y, cond3#(false(), x, y, z) -> gr#(x, z), cond3#(false(), x, y, z) -> gr#(y, z), cond3#(false(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, y, z), cond3#(false(), x, y, z) -> or#(gr(x, z), gr(y, z))} TRS: { cond2(true(), x, y, z) -> cond1(or(gr(x, z), gr(y, z)), p x, y, z), cond2(false(), x, y, z) -> cond3(gr(y, 0()), x, y, z), gr(0(), x) -> false(), gr(s x, 0()) -> true(), gr(s x, s y) -> gr(x, y), cond1(true(), x, y, z) -> cond2(gr(x, 0()), x, y, z), or(x, true()) -> true(), or(true(), x) -> true(), or(false(), false()) -> false(), p 0() -> 0(), p s x -> x, cond3(true(), x, y, z) -> cond1(or(gr(x, z), gr(y, z)), x, p y, z), cond3(false(), x, y, z) -> cond1(or(gr(x, z), gr(y, z)), x, y, z)} UR: { gr(0(), x) -> false(), gr(s x, 0()) -> true(), gr(s x, s y) -> gr(x, y), or(x, true()) -> true(), or(true(), x) -> true(), or(false(), false()) -> false(), p 0() -> 0(), p s x -> x, a(w, v) -> w, a(w, v) -> v} EDG: {(cond2#(true(), x, y, z) -> gr#(y, z), gr#(s x, s y) -> gr#(x, y)) (cond3#(true(), x, y, z) -> gr#(y, z), gr#(s x, s y) -> gr#(x, y)) (cond3#(false(), x, y, z) -> gr#(y, z), gr#(s x, s y) -> gr#(x, y)) (cond2#(false(), x, y, z) -> gr#(y, 0()), gr#(s x, s y) -> gr#(x, y)) (cond2#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), p x, y, z), cond1#(true(), x, y, z) -> gr#(x, 0())) (cond2#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), p x, y, z), cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z)) (cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z)) (cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond2#(false(), x, y, z) -> gr#(y, 0())) (cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond2#(true(), x, y, z) -> p# x) (cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond2#(true(), x, y, z) -> or#(gr(x, z), gr(y, z))) (cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond2#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), p x, y, z)) (cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond2#(true(), x, y, z) -> gr#(y, z)) (cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond2#(true(), x, y, z) -> gr#(x, z)) (cond3#(false(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, y, z), cond1#(true(), x, y, z) -> gr#(x, 0())) (cond3#(false(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, y, z), cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z)) (gr#(s x, s y) -> gr#(x, y), gr#(s x, s y) -> gr#(x, y)) (cond3#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, p y, z), cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z)) (cond3#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, p y, z), cond1#(true(), x, y, z) -> gr#(x, 0())) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(true(), x, y, z) -> gr#(x, z)) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(true(), x, y, z) -> gr#(y, z)) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, p y, z)) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(true(), x, y, z) -> or#(gr(x, z), gr(y, z))) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(true(), x, y, z) -> p# y) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(false(), x, y, z) -> gr#(x, z)) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(false(), x, y, z) -> gr#(y, z)) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(false(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, y, z)) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(false(), x, y, z) -> or#(gr(x, z), gr(y, z))) (cond1#(true(), x, y, z) -> gr#(x, 0()), gr#(s x, s y) -> gr#(x, y)) (cond3#(false(), x, y, z) -> gr#(x, z), gr#(s x, s y) -> gr#(x, y)) (cond3#(true(), x, y, z) -> gr#(x, z), gr#(s x, s y) -> gr#(x, y)) (cond2#(true(), x, y, z) -> gr#(x, z), gr#(s x, s y) -> gr#(x, y))} EDG: {(cond2#(true(), x, y, z) -> gr#(y, z), gr#(s x, s y) -> gr#(x, y)) (cond3#(true(), x, y, z) -> gr#(y, z), gr#(s x, s y) -> gr#(x, y)) (cond3#(false(), x, y, z) -> gr#(y, z), gr#(s x, s y) -> gr#(x, y)) (cond2#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), p x, y, z), cond1#(true(), x, y, z) -> gr#(x, 0())) (cond2#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), p x, y, z), cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z)) (cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z)) (cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond2#(false(), x, y, z) -> gr#(y, 0())) (cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond2#(true(), x, y, z) -> p# x) (cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond2#(true(), x, y, z) -> or#(gr(x, z), gr(y, z))) (cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond2#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), p x, y, z)) (cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond2#(true(), x, y, z) -> gr#(y, z)) (cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond2#(true(), x, y, z) -> gr#(x, z)) (cond3#(false(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, y, z), cond1#(true(), x, y, z) -> gr#(x, 0())) (cond3#(false(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, y, z), cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z)) (gr#(s x, s y) -> gr#(x, y), gr#(s x, s y) -> gr#(x, y)) (cond3#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, p y, z), cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z)) (cond3#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, p y, z), cond1#(true(), x, y, z) -> gr#(x, 0())) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(true(), x, y, z) -> gr#(x, z)) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(true(), x, y, z) -> gr#(y, z)) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, p y, z)) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(true(), x, y, z) -> or#(gr(x, z), gr(y, z))) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(true(), x, y, z) -> p# y) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(false(), x, y, z) -> gr#(x, z)) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(false(), x, y, z) -> gr#(y, z)) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(false(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, y, z)) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(false(), x, y, z) -> or#(gr(x, z), gr(y, z))) (cond3#(false(), x, y, z) -> gr#(x, z), gr#(s x, s y) -> gr#(x, y)) (cond3#(true(), x, y, z) -> gr#(x, z), gr#(s x, s y) -> gr#(x, y)) (cond2#(true(), x, y, z) -> gr#(x, z), gr#(s x, s y) -> gr#(x, y))} EDG: {(cond2#(true(), x, y, z) -> gr#(y, z), gr#(s x, s y) -> gr#(x, y)) (cond3#(true(), x, y, z) -> gr#(y, z), gr#(s x, s y) -> gr#(x, y)) (cond3#(false(), x, y, z) -> gr#(y, z), gr#(s x, s y) -> gr#(x, y)) (cond2#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), p x, y, z), cond1#(true(), x, y, z) -> gr#(x, 0())) (cond2#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), p x, y, z), cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z)) (cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z)) (cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond2#(false(), x, y, z) -> gr#(y, 0())) (cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond2#(true(), x, y, z) -> p# x) (cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond2#(true(), x, y, z) -> or#(gr(x, z), gr(y, z))) (cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond2#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), p x, y, z)) (cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond2#(true(), x, y, z) -> gr#(y, z)) (cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond2#(true(), x, y, z) -> gr#(x, z)) (cond3#(false(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, y, z), cond1#(true(), x, y, z) -> gr#(x, 0())) (cond3#(false(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, y, z), cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z)) (gr#(s x, s y) -> gr#(x, y), gr#(s x, s y) -> gr#(x, y)) (cond3#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, p y, z), cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z)) (cond3#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, p y, z), cond1#(true(), x, y, z) -> gr#(x, 0())) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(true(), x, y, z) -> gr#(x, z)) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(true(), x, y, z) -> gr#(y, z)) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, p y, z)) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(true(), x, y, z) -> or#(gr(x, z), gr(y, z))) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(true(), x, y, z) -> p# y) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(false(), x, y, z) -> gr#(x, z)) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(false(), x, y, z) -> gr#(y, z)) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(false(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, y, z)) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(false(), x, y, z) -> or#(gr(x, z), gr(y, z))) (cond3#(false(), x, y, z) -> gr#(x, z), gr#(s x, s y) -> gr#(x, y)) (cond3#(true(), x, y, z) -> gr#(x, z), gr#(s x, s y) -> gr#(x, y)) (cond2#(true(), x, y, z) -> gr#(x, z), gr#(s x, s y) -> gr#(x, y))} EDG: {(cond2#(true(), x, y, z) -> gr#(y, z), gr#(s x, s y) -> gr#(x, y)) (cond3#(true(), x, y, z) -> gr#(y, z), gr#(s x, s y) -> gr#(x, y)) (cond3#(false(), x, y, z) -> gr#(y, z), gr#(s x, s y) -> gr#(x, y)) (cond2#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), p x, y, z), cond1#(true(), x, y, z) -> gr#(x, 0())) (cond2#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), p x, y, z), cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z)) (cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z)) (cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond2#(false(), x, y, z) -> gr#(y, 0())) (cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond2#(true(), x, y, z) -> p# x) (cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond2#(true(), x, y, z) -> or#(gr(x, z), gr(y, z))) (cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond2#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), p x, y, z)) (cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond2#(true(), x, y, z) -> gr#(y, z)) (cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond2#(true(), x, y, z) -> gr#(x, z)) (cond3#(false(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, y, z), cond1#(true(), x, y, z) -> gr#(x, 0())) (cond3#(false(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, y, z), cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z)) (gr#(s x, s y) -> gr#(x, y), gr#(s x, s y) -> gr#(x, y)) (cond3#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, p y, z), cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z)) (cond3#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, p y, z), cond1#(true(), x, y, z) -> gr#(x, 0())) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(true(), x, y, z) -> gr#(x, z)) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(true(), x, y, z) -> gr#(y, z)) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, p y, z)) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(true(), x, y, z) -> or#(gr(x, z), gr(y, z))) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(true(), x, y, z) -> p# y) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(false(), x, y, z) -> gr#(x, z)) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(false(), x, y, z) -> gr#(y, z)) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(false(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, y, z)) (cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond3#(false(), x, y, z) -> or#(gr(x, z), gr(y, z))) (cond3#(false(), x, y, z) -> gr#(x, z), gr#(s x, s y) -> gr#(x, y)) (cond3#(true(), x, y, z) -> gr#(x, z), gr#(s x, s y) -> gr#(x, y)) (cond2#(true(), x, y, z) -> gr#(x, z), gr#(s x, s y) -> gr#(x, y))} STATUS: arrows: 0.919668 SCCS (2): Scc: { cond2#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), p x, y, z), cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond3#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, p y, z), cond3#(false(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, y, z)} Scc: {gr#(s x, s y) -> gr#(x, y)} SCC (5): Strict: { cond2#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), p x, y, z), cond2#(false(), x, y, z) -> cond3#(gr(y, 0()), x, y, z), cond1#(true(), x, y, z) -> cond2#(gr(x, 0()), x, y, z), cond3#(true(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, p y, z), cond3#(false(), x, y, z) -> cond1#(or(gr(x, z), gr(y, z)), x, y, z)} Weak: { cond2(true(), x, y, z) -> cond1(or(gr(x, z), gr(y, z)), p x, y, z), cond2(false(), x, y, z) -> cond3(gr(y, 0()), x, y, z), gr(0(), x) -> false(), gr(s x, 0()) -> true(), gr(s x, s y) -> gr(x, y), cond1(true(), x, y, z) -> cond2(gr(x, 0()), x, y, z), or(x, true()) -> true(), or(true(), x) -> true(), or(false(), false()) -> false(), p 0() -> 0(), p s x -> x, cond3(true(), x, y, z) -> cond1(or(gr(x, z), gr(y, z)), x, p y, z), cond3(false(), x, y, z) -> cond1(or(gr(x, z), gr(y, z)), x, y, z)} Fail SCC (1): Strict: {gr#(s x, s y) -> gr#(x, y)} Weak: { cond2(true(), x, y, z) -> cond1(or(gr(x, z), gr(y, z)), p x, y, z), cond2(false(), x, y, z) -> cond3(gr(y, 0()), x, y, z), gr(0(), x) -> false(), gr(s x, 0()) -> true(), gr(s x, s y) -> gr(x, y), cond1(true(), x, y, z) -> cond2(gr(x, 0()), x, y, z), or(x, true()) -> true(), or(true(), x) -> true(), or(false(), false()) -> false(), p 0() -> 0(), p s x -> x, cond3(true(), x, y, z) -> cond1(or(gr(x, z), gr(y, z)), x, p y, z), cond3(false(), x, y, z) -> cond1(or(gr(x, z), gr(y, z)), x, y, z)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cond2](x0, x1, x2, x3) = x0 + 1, [cond1](x0, x1, x2, x3) = 0, [cond3](x0, x1, x2, x3) = 0, [gr](x0, x1) = 1, [or](x0, x1) = x0 + 1, [p](x0) = 0, [s](x0) = x0 + 1, [0] = 0, [true] = 1, [false] = 1, [gr#](x0, x1) = x0 Strict: gr#(s x, s y) -> gr#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: cond3(false(), x, y, z) -> cond1(or(gr(x, z), gr(y, z)), x, y, z) 0 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z cond3(true(), x, y, z) -> cond1(or(gr(x, z), gr(y, z)), x, p y, z) 0 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z p s x -> x 0 + 0x >= 1x p 0() -> 0() 0 >= 0 or(false(), false()) -> false() 2 >= 1 or(true(), x) -> true() 1 + 1x >= 1 or(x, true()) -> true() 2 + 0x >= 1 cond1(true(), x, y, z) -> cond2(gr(x, 0()), x, y, z) 0 + 0x + 0y + 0z >= 2 + 0x + 0y + 0z gr(s x, s y) -> gr(x, y) 1 + 0x + 0y >= 1 + 0x + 0y gr(s x, 0()) -> true() 1 + 0x >= 1 gr(0(), x) -> false() 1 + 0x >= 1 cond2(false(), x, y, z) -> cond3(gr(y, 0()), x, y, z) 2 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z cond2(true(), x, y, z) -> cond1(or(gr(x, z), gr(y, z)), p x, y, z) 2 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z Qed