WORST_CASE(Omega(n^1),?) proof of /export/starexec/sandbox/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 9992 ms] (2) CpxRelTRS (3) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (4) TRS for Loop Detection (5) DecreasingLoopProof [LOWER BOUND(ID), 0 ms] (6) BEST (7) proven lower bound (8) LowerBoundPropagationProof [FINISHED, 0 ms] (9) BOUNDS(n^1, INF) (10) TRS for Loop Detection ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: EQ(0, 0) -> c EQ(0, s(z0)) -> c1 EQ(s(z0), 0) -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) OR(true, z0) -> c4 OR(false, z0) -> c5 UNION(empty, z0) -> c6 UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3)) ISEMPTY(empty) -> c8 ISEMPTY(edge(z0, z1, z2)) -> c9 FROM(edge(z0, z1, z2)) -> c10 TO(edge(z0, z1, z2)) -> c11 REST(edge(z0, z1, z2)) -> c12 REST(empty) -> c13 REACH(z0, z1, z2, z3) -> c14(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, z1)) REACH(z0, z1, z2, z3) -> c15(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), ISEMPTY(z2)) REACH(z0, z1, z2, z3) -> c16(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, from(z2)), FROM(z2)) REACH(z0, z1, z2, z3) -> c17(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z1, to(z2)), TO(z2)) IF1(true, z0, z1, z2, z3, z4, z5, z6) -> c18 IF1(false, z0, z1, z2, z3, z4, z5, z6) -> c19(IF2(z0, z1, z2, z3, z4, z5, z6)) IF2(true, z0, z1, z2, z3, z4, z5) -> c20 IF2(false, z0, z1, z2, z3, z4, z5) -> c21(IF3(z0, z1, z2, z3, z4, z5)) IF3(false, z0, z1, z2, z3, z4) -> c22(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), REST(z3)) IF3(false, z0, z1, z2, z3, z4) -> c23(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), FROM(z3)) IF3(false, z0, z1, z2, z3, z4) -> c24(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), TO(z3)) IF3(true, z0, z1, z2, z3, z4) -> c25(IF4(z0, z1, z2, z3, z4)) IF4(true, z0, z1, z2, z3) -> c26 IF4(false, z0, z1, z2, z3) -> c27(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(z0, z1, rest(z2), z3), REST(z2)) IF4(false, z0, z1, z2, z3) -> c28(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), TO(z2)) IF4(false, z0, z1, z2, z3) -> c29(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), UNION(rest(z2), z3), REST(z2)) The (relative) TRS S consists of the following rules: eq(0, 0) -> true eq(0, s(z0)) -> false eq(s(z0), 0) -> false eq(s(z0), s(z1)) -> eq(z0, z1) or(true, z0) -> true or(false, z0) -> z0 union(empty, z0) -> z0 union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3)) isEmpty(empty) -> true isEmpty(edge(z0, z1, z2)) -> false from(edge(z0, z1, z2)) -> z0 to(edge(z0, z1, z2)) -> z1 rest(edge(z0, z1, z2)) -> z2 rest(empty) -> empty reach(z0, z1, z2, z3) -> if1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3) if1(true, z0, z1, z2, z3, z4, z5, z6) -> true if1(false, z0, z1, z2, z3, z4, z5, z6) -> if2(z0, z1, z2, z3, z4, z5, z6) if2(true, z0, z1, z2, z3, z4, z5) -> false if2(false, z0, z1, z2, z3, z4, z5) -> if3(z0, z1, z2, z3, z4, z5) if3(false, z0, z1, z2, z3, z4) -> reach(z1, z2, rest(z3), edge(from(z3), to(z3), z4)) if3(true, z0, z1, z2, z3, z4) -> if4(z0, z1, z2, z3, z4) if4(true, z0, z1, z2, z3) -> true if4(false, z0, z1, z2, z3) -> or(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)) Rewrite Strategy: INNERMOST ---------------------------------------- (1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID)) proved innermost termination of relative rules ---------------------------------------- (2) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: EQ(0, 0) -> c EQ(0, s(z0)) -> c1 EQ(s(z0), 0) -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) OR(true, z0) -> c4 OR(false, z0) -> c5 UNION(empty, z0) -> c6 UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3)) ISEMPTY(empty) -> c8 ISEMPTY(edge(z0, z1, z2)) -> c9 FROM(edge(z0, z1, z2)) -> c10 TO(edge(z0, z1, z2)) -> c11 REST(edge(z0, z1, z2)) -> c12 REST(empty) -> c13 REACH(z0, z1, z2, z3) -> c14(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, z1)) REACH(z0, z1, z2, z3) -> c15(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), ISEMPTY(z2)) REACH(z0, z1, z2, z3) -> c16(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, from(z2)), FROM(z2)) REACH(z0, z1, z2, z3) -> c17(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z1, to(z2)), TO(z2)) IF1(true, z0, z1, z2, z3, z4, z5, z6) -> c18 IF1(false, z0, z1, z2, z3, z4, z5, z6) -> c19(IF2(z0, z1, z2, z3, z4, z5, z6)) IF2(true, z0, z1, z2, z3, z4, z5) -> c20 IF2(false, z0, z1, z2, z3, z4, z5) -> c21(IF3(z0, z1, z2, z3, z4, z5)) IF3(false, z0, z1, z2, z3, z4) -> c22(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), REST(z3)) IF3(false, z0, z1, z2, z3, z4) -> c23(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), FROM(z3)) IF3(false, z0, z1, z2, z3, z4) -> c24(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), TO(z3)) IF3(true, z0, z1, z2, z3, z4) -> c25(IF4(z0, z1, z2, z3, z4)) IF4(true, z0, z1, z2, z3) -> c26 IF4(false, z0, z1, z2, z3) -> c27(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(z0, z1, rest(z2), z3), REST(z2)) IF4(false, z0, z1, z2, z3) -> c28(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), TO(z2)) IF4(false, z0, z1, z2, z3) -> c29(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), UNION(rest(z2), z3), REST(z2)) The (relative) TRS S consists of the following rules: eq(0, 0) -> true eq(0, s(z0)) -> false eq(s(z0), 0) -> false eq(s(z0), s(z1)) -> eq(z0, z1) or(true, z0) -> true or(false, z0) -> z0 union(empty, z0) -> z0 union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3)) isEmpty(empty) -> true isEmpty(edge(z0, z1, z2)) -> false from(edge(z0, z1, z2)) -> z0 to(edge(z0, z1, z2)) -> z1 rest(edge(z0, z1, z2)) -> z2 rest(empty) -> empty reach(z0, z1, z2, z3) -> if1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3) if1(true, z0, z1, z2, z3, z4, z5, z6) -> true if1(false, z0, z1, z2, z3, z4, z5, z6) -> if2(z0, z1, z2, z3, z4, z5, z6) if2(true, z0, z1, z2, z3, z4, z5) -> false if2(false, z0, z1, z2, z3, z4, z5) -> if3(z0, z1, z2, z3, z4, z5) if3(false, z0, z1, z2, z3, z4) -> reach(z1, z2, rest(z3), edge(from(z3), to(z3), z4)) if3(true, z0, z1, z2, z3, z4) -> if4(z0, z1, z2, z3, z4) if4(true, z0, z1, z2, z3) -> true if4(false, z0, z1, z2, z3) -> or(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)) Rewrite Strategy: INNERMOST ---------------------------------------- (3) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (4) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: EQ(0, 0) -> c EQ(0, s(z0)) -> c1 EQ(s(z0), 0) -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) OR(true, z0) -> c4 OR(false, z0) -> c5 UNION(empty, z0) -> c6 UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3)) ISEMPTY(empty) -> c8 ISEMPTY(edge(z0, z1, z2)) -> c9 FROM(edge(z0, z1, z2)) -> c10 TO(edge(z0, z1, z2)) -> c11 REST(edge(z0, z1, z2)) -> c12 REST(empty) -> c13 REACH(z0, z1, z2, z3) -> c14(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, z1)) REACH(z0, z1, z2, z3) -> c15(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), ISEMPTY(z2)) REACH(z0, z1, z2, z3) -> c16(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, from(z2)), FROM(z2)) REACH(z0, z1, z2, z3) -> c17(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z1, to(z2)), TO(z2)) IF1(true, z0, z1, z2, z3, z4, z5, z6) -> c18 IF1(false, z0, z1, z2, z3, z4, z5, z6) -> c19(IF2(z0, z1, z2, z3, z4, z5, z6)) IF2(true, z0, z1, z2, z3, z4, z5) -> c20 IF2(false, z0, z1, z2, z3, z4, z5) -> c21(IF3(z0, z1, z2, z3, z4, z5)) IF3(false, z0, z1, z2, z3, z4) -> c22(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), REST(z3)) IF3(false, z0, z1, z2, z3, z4) -> c23(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), FROM(z3)) IF3(false, z0, z1, z2, z3, z4) -> c24(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), TO(z3)) IF3(true, z0, z1, z2, z3, z4) -> c25(IF4(z0, z1, z2, z3, z4)) IF4(true, z0, z1, z2, z3) -> c26 IF4(false, z0, z1, z2, z3) -> c27(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(z0, z1, rest(z2), z3), REST(z2)) IF4(false, z0, z1, z2, z3) -> c28(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), TO(z2)) IF4(false, z0, z1, z2, z3) -> c29(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), UNION(rest(z2), z3), REST(z2)) The (relative) TRS S consists of the following rules: eq(0, 0) -> true eq(0, s(z0)) -> false eq(s(z0), 0) -> false eq(s(z0), s(z1)) -> eq(z0, z1) or(true, z0) -> true or(false, z0) -> z0 union(empty, z0) -> z0 union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3)) isEmpty(empty) -> true isEmpty(edge(z0, z1, z2)) -> false from(edge(z0, z1, z2)) -> z0 to(edge(z0, z1, z2)) -> z1 rest(edge(z0, z1, z2)) -> z2 rest(empty) -> empty reach(z0, z1, z2, z3) -> if1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3) if1(true, z0, z1, z2, z3, z4, z5, z6) -> true if1(false, z0, z1, z2, z3, z4, z5, z6) -> if2(z0, z1, z2, z3, z4, z5, z6) if2(true, z0, z1, z2, z3, z4, z5) -> false if2(false, z0, z1, z2, z3, z4, z5) -> if3(z0, z1, z2, z3, z4, z5) if3(false, z0, z1, z2, z3, z4) -> reach(z1, z2, rest(z3), edge(from(z3), to(z3), z4)) if3(true, z0, z1, z2, z3, z4) -> if4(z0, z1, z2, z3, z4) if4(true, z0, z1, z2, z3) -> true if4(false, z0, z1, z2, z3) -> or(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)) Rewrite Strategy: INNERMOST ---------------------------------------- (5) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence EQ(s(z0), s(z1)) ->^+ c3(EQ(z0, z1)) gives rise to a decreasing loop by considering the right hand sides subterm at position [0]. The pumping substitution is [z0 / s(z0), z1 / s(z1)]. The result substitution is [ ]. ---------------------------------------- (6) Complex Obligation (BEST) ---------------------------------------- (7) Obligation: Proved the lower bound n^1 for the following obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: EQ(0, 0) -> c EQ(0, s(z0)) -> c1 EQ(s(z0), 0) -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) OR(true, z0) -> c4 OR(false, z0) -> c5 UNION(empty, z0) -> c6 UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3)) ISEMPTY(empty) -> c8 ISEMPTY(edge(z0, z1, z2)) -> c9 FROM(edge(z0, z1, z2)) -> c10 TO(edge(z0, z1, z2)) -> c11 REST(edge(z0, z1, z2)) -> c12 REST(empty) -> c13 REACH(z0, z1, z2, z3) -> c14(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, z1)) REACH(z0, z1, z2, z3) -> c15(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), ISEMPTY(z2)) REACH(z0, z1, z2, z3) -> c16(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, from(z2)), FROM(z2)) REACH(z0, z1, z2, z3) -> c17(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z1, to(z2)), TO(z2)) IF1(true, z0, z1, z2, z3, z4, z5, z6) -> c18 IF1(false, z0, z1, z2, z3, z4, z5, z6) -> c19(IF2(z0, z1, z2, z3, z4, z5, z6)) IF2(true, z0, z1, z2, z3, z4, z5) -> c20 IF2(false, z0, z1, z2, z3, z4, z5) -> c21(IF3(z0, z1, z2, z3, z4, z5)) IF3(false, z0, z1, z2, z3, z4) -> c22(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), REST(z3)) IF3(false, z0, z1, z2, z3, z4) -> c23(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), FROM(z3)) IF3(false, z0, z1, z2, z3, z4) -> c24(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), TO(z3)) IF3(true, z0, z1, z2, z3, z4) -> c25(IF4(z0, z1, z2, z3, z4)) IF4(true, z0, z1, z2, z3) -> c26 IF4(false, z0, z1, z2, z3) -> c27(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(z0, z1, rest(z2), z3), REST(z2)) IF4(false, z0, z1, z2, z3) -> c28(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), TO(z2)) IF4(false, z0, z1, z2, z3) -> c29(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), UNION(rest(z2), z3), REST(z2)) The (relative) TRS S consists of the following rules: eq(0, 0) -> true eq(0, s(z0)) -> false eq(s(z0), 0) -> false eq(s(z0), s(z1)) -> eq(z0, z1) or(true, z0) -> true or(false, z0) -> z0 union(empty, z0) -> z0 union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3)) isEmpty(empty) -> true isEmpty(edge(z0, z1, z2)) -> false from(edge(z0, z1, z2)) -> z0 to(edge(z0, z1, z2)) -> z1 rest(edge(z0, z1, z2)) -> z2 rest(empty) -> empty reach(z0, z1, z2, z3) -> if1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3) if1(true, z0, z1, z2, z3, z4, z5, z6) -> true if1(false, z0, z1, z2, z3, z4, z5, z6) -> if2(z0, z1, z2, z3, z4, z5, z6) if2(true, z0, z1, z2, z3, z4, z5) -> false if2(false, z0, z1, z2, z3, z4, z5) -> if3(z0, z1, z2, z3, z4, z5) if3(false, z0, z1, z2, z3, z4) -> reach(z1, z2, rest(z3), edge(from(z3), to(z3), z4)) if3(true, z0, z1, z2, z3, z4) -> if4(z0, z1, z2, z3, z4) if4(true, z0, z1, z2, z3) -> true if4(false, z0, z1, z2, z3) -> or(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)) Rewrite Strategy: INNERMOST ---------------------------------------- (8) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (9) BOUNDS(n^1, INF) ---------------------------------------- (10) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: EQ(0, 0) -> c EQ(0, s(z0)) -> c1 EQ(s(z0), 0) -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) OR(true, z0) -> c4 OR(false, z0) -> c5 UNION(empty, z0) -> c6 UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3)) ISEMPTY(empty) -> c8 ISEMPTY(edge(z0, z1, z2)) -> c9 FROM(edge(z0, z1, z2)) -> c10 TO(edge(z0, z1, z2)) -> c11 REST(edge(z0, z1, z2)) -> c12 REST(empty) -> c13 REACH(z0, z1, z2, z3) -> c14(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, z1)) REACH(z0, z1, z2, z3) -> c15(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), ISEMPTY(z2)) REACH(z0, z1, z2, z3) -> c16(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, from(z2)), FROM(z2)) REACH(z0, z1, z2, z3) -> c17(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z1, to(z2)), TO(z2)) IF1(true, z0, z1, z2, z3, z4, z5, z6) -> c18 IF1(false, z0, z1, z2, z3, z4, z5, z6) -> c19(IF2(z0, z1, z2, z3, z4, z5, z6)) IF2(true, z0, z1, z2, z3, z4, z5) -> c20 IF2(false, z0, z1, z2, z3, z4, z5) -> c21(IF3(z0, z1, z2, z3, z4, z5)) IF3(false, z0, z1, z2, z3, z4) -> c22(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), REST(z3)) IF3(false, z0, z1, z2, z3, z4) -> c23(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), FROM(z3)) IF3(false, z0, z1, z2, z3, z4) -> c24(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), TO(z3)) IF3(true, z0, z1, z2, z3, z4) -> c25(IF4(z0, z1, z2, z3, z4)) IF4(true, z0, z1, z2, z3) -> c26 IF4(false, z0, z1, z2, z3) -> c27(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(z0, z1, rest(z2), z3), REST(z2)) IF4(false, z0, z1, z2, z3) -> c28(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), TO(z2)) IF4(false, z0, z1, z2, z3) -> c29(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), UNION(rest(z2), z3), REST(z2)) The (relative) TRS S consists of the following rules: eq(0, 0) -> true eq(0, s(z0)) -> false eq(s(z0), 0) -> false eq(s(z0), s(z1)) -> eq(z0, z1) or(true, z0) -> true or(false, z0) -> z0 union(empty, z0) -> z0 union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3)) isEmpty(empty) -> true isEmpty(edge(z0, z1, z2)) -> false from(edge(z0, z1, z2)) -> z0 to(edge(z0, z1, z2)) -> z1 rest(edge(z0, z1, z2)) -> z2 rest(empty) -> empty reach(z0, z1, z2, z3) -> if1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3) if1(true, z0, z1, z2, z3, z4, z5, z6) -> true if1(false, z0, z1, z2, z3, z4, z5, z6) -> if2(z0, z1, z2, z3, z4, z5, z6) if2(true, z0, z1, z2, z3, z4, z5) -> false if2(false, z0, z1, z2, z3, z4, z5) -> if3(z0, z1, z2, z3, z4, z5) if3(false, z0, z1, z2, z3, z4) -> reach(z1, z2, rest(z3), edge(from(z3), to(z3), z4)) if3(true, z0, z1, z2, z3, z4) -> if4(z0, z1, z2, z3, z4) if4(true, z0, z1, z2, z3) -> true if4(false, z0, z1, z2, z3) -> or(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)) Rewrite Strategy: INNERMOST