YES We show the termination of the TRS R: ack_in(|0|(),n) -> ack_out(s(n)) ack_in(s(m),|0|()) -> u11(ack_in(m,s(|0|()))) u11(ack_out(n)) -> ack_out(n) ack_in(s(m),s(n)) -> u21(ack_in(s(m),n),m) u21(ack_out(n),m) -> u22(ack_in(m,n)) u22(ack_out(n)) -> ack_out(n) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: ack_in#(s(m),|0|()) -> u11#(ack_in(m,s(|0|()))) p2: ack_in#(s(m),|0|()) -> ack_in#(m,s(|0|())) p3: ack_in#(s(m),s(n)) -> u21#(ack_in(s(m),n),m) p4: ack_in#(s(m),s(n)) -> ack_in#(s(m),n) p5: u21#(ack_out(n),m) -> u22#(ack_in(m,n)) p6: u21#(ack_out(n),m) -> ack_in#(m,n) and R consists of: r1: ack_in(|0|(),n) -> ack_out(s(n)) r2: ack_in(s(m),|0|()) -> u11(ack_in(m,s(|0|()))) r3: u11(ack_out(n)) -> ack_out(n) r4: ack_in(s(m),s(n)) -> u21(ack_in(s(m),n),m) r5: u21(ack_out(n),m) -> u22(ack_in(m,n)) r6: u22(ack_out(n)) -> ack_out(n) The estimated dependency graph contains the following SCCs: {p2, p3, p4, p6} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: ack_in#(s(m),|0|()) -> ack_in#(m,s(|0|())) p2: ack_in#(s(m),s(n)) -> ack_in#(s(m),n) p3: ack_in#(s(m),s(n)) -> u21#(ack_in(s(m),n),m) p4: u21#(ack_out(n),m) -> ack_in#(m,n) and R consists of: r1: ack_in(|0|(),n) -> ack_out(s(n)) r2: ack_in(s(m),|0|()) -> u11(ack_in(m,s(|0|()))) r3: u11(ack_out(n)) -> ack_out(n) r4: ack_in(s(m),s(n)) -> u21(ack_in(s(m),n),m) r5: u21(ack_out(n),m) -> u22(ack_in(m,n)) r6: u22(ack_out(n)) -> ack_out(n) The set of usable rules consists of r1, r2, r3, r4, r5, r6 Take the reduction pair: generalized weighted path order (>=MG, >G) base order 1: trivial reduction triple (T x T, T x T, Φ) base order 2: model-based reduction triple (=A, >=A!, >A!): finite algebra: carrier: {0,1} interpretations: ack_in#_A(0,0) = 0 ack_in#_A(0,1) = 0 ack_in#_A(1,0) = 0 ack_in#_A(1,1) = 0 s_A(0) = 0 s_A(1) = 0 |0|_A = 0 u21#_A(0,0) = 0 u21#_A(0,1) = 0 u21#_A(1,0) = 0 u21#_A(1,1) = 0 ack_in_A(0,0) = 0 ack_in_A(0,1) = 0 ack_in_A(1,0) = 1 ack_in_A(1,1) = 1 ack_out_A(0) = 0 ack_out_A(1) = 0 u11_A(0) = 0 u11_A(1) = 0 u21_A(0,0) = 0 u21_A(0,1) = 0 u21_A(1,0) = 0 u21_A(1,1) = 0 u22_A(0) = 0 u22_A(1) = 0 ack_in#!_A(0,0) = 0 ack_in#!_A(0,1) = 0 ack_in#!_A(1,0) = 0 ack_in#!_A(1,1) = 0 s!_A(0) = 1 s!_A(1) = 1 |0|!_A = 0 u21#!_A(0,0) = 0 u21#!_A(0,1) = 1 u21#!_A(1,0) = 0 u21#!_A(1,1) = 0 ack_in!_A(0,0) = 0 ack_in!_A(0,1) = 0 ack_in!_A(1,0) = 0 ack_in!_A(1,1) = 0 ack_out!_A(0) = 0 ack_out!_A(1) = 0 u11!_A(0) = 0 u11!_A(1) = 0 u21!_A(0,0) = 0 u21!_A(0,1) = 0 u21!_A(1,0) = 0 u21!_A(1,1) = 0 u22!_A(0) = 0 u22!_A(1) = 0 partial status: pi(ack_in#) = [1] pi(s) = [1] pi(|0|) = [] pi(u21#) = [2] pi(ack_in) = [] pi(ack_out) = [] pi(u11) = [] pi(u21) = [] pi(u22) = [] The following rules are removed: p3 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: ack_in#(s(m),|0|()) -> ack_in#(m,s(|0|())) p2: ack_in#(s(m),s(n)) -> ack_in#(s(m),n) p3: u21#(ack_out(n),m) -> ack_in#(m,n) and R consists of: r1: ack_in(|0|(),n) -> ack_out(s(n)) r2: ack_in(s(m),|0|()) -> u11(ack_in(m,s(|0|()))) r3: u11(ack_out(n)) -> ack_out(n) r4: ack_in(s(m),s(n)) -> u21(ack_in(s(m),n),m) r5: u21(ack_out(n),m) -> u22(ack_in(m,n)) r6: u22(ack_out(n)) -> ack_out(n) The estimated dependency graph contains the following SCCs: {p1, p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: ack_in#(s(m),|0|()) -> ack_in#(m,s(|0|())) p2: ack_in#(s(m),s(n)) -> ack_in#(s(m),n) and R consists of: r1: ack_in(|0|(),n) -> ack_out(s(n)) r2: ack_in(s(m),|0|()) -> u11(ack_in(m,s(|0|()))) r3: u11(ack_out(n)) -> ack_out(n) r4: ack_in(s(m),s(n)) -> u21(ack_in(s(m),n),m) r5: u21(ack_out(n),m) -> u22(ack_in(m,n)) r6: u22(ack_out(n)) -> ack_out(n) The set of usable rules consists of r1, r2, r3, r4, r5, r6 Take the reduction pair: generalized weighted path order (>=MG, >G) base order 1: trivial reduction triple (T x T, T x T, Φ) base order 2: model-based reduction triple (=A, >=A!, >A!): finite algebra: carrier: {0,1} interpretations: ack_in#_A(0,0) = 0 ack_in#_A(0,1) = 0 ack_in#_A(1,0) = 0 ack_in#_A(1,1) = 0 s_A(0) = 0 s_A(1) = 0 |0|_A = 0 ack_in_A(0,0) = 0 ack_in_A(0,1) = 0 ack_in_A(1,0) = 1 ack_in_A(1,1) = 0 ack_out_A(0) = 0 ack_out_A(1) = 0 u11_A(0) = 0 u11_A(1) = 0 u21_A(0,0) = 0 u21_A(0,1) = 0 u21_A(1,0) = 1 u21_A(1,1) = 0 u22_A(0) = 0 u22_A(1) = 0 ack_in#!_A(0,0) = 1 ack_in#!_A(0,1) = 0 ack_in#!_A(1,0) = 0 ack_in#!_A(1,1) = 0 s!_A(0) = 1 s!_A(1) = 0 |0|!_A = 0 ack_in!_A(0,0) = 0 ack_in!_A(0,1) = 0 ack_in!_A(1,0) = 0 ack_in!_A(1,1) = 0 ack_out!_A(0) = 0 ack_out!_A(1) = 0 u11!_A(0) = 0 u11!_A(1) = 0 u21!_A(0,0) = 0 u21!_A(0,1) = 0 u21!_A(1,0) = 0 u21!_A(1,1) = 0 u22!_A(0) = 0 u22!_A(1) = 0 partial status: pi(ack_in#) = [1, 2] pi(s) = [1] pi(|0|) = [] pi(ack_in) = [] pi(ack_out) = [] pi(u11) = [] pi(u21) = [] pi(u22) = [] The following rules are removed: p2 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: ack_in#(s(m),|0|()) -> ack_in#(m,s(|0|())) and R consists of: r1: ack_in(|0|(),n) -> ack_out(s(n)) r2: ack_in(s(m),|0|()) -> u11(ack_in(m,s(|0|()))) r3: u11(ack_out(n)) -> ack_out(n) r4: ack_in(s(m),s(n)) -> u21(ack_in(s(m),n),m) r5: u21(ack_out(n),m) -> u22(ack_in(m,n)) r6: u22(ack_out(n)) -> ack_out(n) The estimated dependency graph contains the following SCCs: (no SCCs)