8.35/2.78 YES 8.68/2.80 8.68/2.80 Proof: 8.68/2.80 This system is confluent. 8.68/2.80 By \cite{ALS94}, Theorem 4.1. 8.68/2.80 This system is of type 3 or smaller. 8.68/2.80 This system is strongly deterministic. 8.68/2.80 This system is quasi-decreasing. 8.68/2.80 By \cite{O02}, p. 214, Proposition 7.2.50. 8.68/2.80 This system is of type 3 or smaller. 8.68/2.80 This system is deterministic. 8.68/2.80 System R transformed to optimized U(R). 8.68/2.80 This system is terminating. 8.68/2.80 Call external tool: 8.68/2.80 ./ttt2.sh 8.68/2.80 Input: 8.68/2.80 f(c(x), c(c(y))) -> ?1(c(f(x, y)), x, y) 8.68/2.80 ?1(c(a(b)), x, y) -> a(a(x)) 8.68/2.80 f(c(c(c(x))), y) -> ?2(c(f(c(x), c(c(y)))), x, y) 8.68/2.80 ?2(c(a(a(b))), x, y) -> a(y) 8.68/2.80 h(b) -> b 8.68/2.80 h(a(a(x))) -> ?3(h(x), x) 8.68/2.80 ?3(b, x) -> a(b) 8.68/2.80 8.68/2.80 DP Processor: 8.68/2.80 DPs: 8.68/2.80 f#(c(x),c(c(y))) -> f#(x,y) 8.68/2.80 f#(c(x),c(c(y))) -> ?1#(c(f(x,y)),x,y) 8.68/2.80 f#(c(c(c(x))),y) -> f#(c(x),c(c(y))) 8.68/2.80 f#(c(c(c(x))),y) -> ?2#(c(f(c(x),c(c(y)))),x,y) 8.68/2.80 h#(a(a(x))) -> h#(x) 8.68/2.80 h#(a(a(x))) -> ?3#(h(x),x) 8.68/2.80 TRS: 8.68/2.80 f(c(x),c(c(y))) -> ?1(c(f(x,y)),x,y) 8.68/2.80 ?1(c(a(b())),x,y) -> a(a(x)) 8.68/2.80 f(c(c(c(x))),y) -> ?2(c(f(c(x),c(c(y)))),x,y) 8.68/2.80 ?2(c(a(a(b()))),x,y) -> a(y) 8.68/2.80 h(b()) -> b() 8.68/2.80 h(a(a(x))) -> ?3(h(x),x) 8.68/2.80 ?3(b(),x) -> a(b()) 8.68/2.80 TDG Processor: 8.68/2.80 DPs: 8.68/2.80 f#(c(x),c(c(y))) -> f#(x,y) 8.68/2.80 f#(c(x),c(c(y))) -> ?1#(c(f(x,y)),x,y) 8.68/2.80 f#(c(c(c(x))),y) -> f#(c(x),c(c(y))) 8.68/2.80 f#(c(c(c(x))),y) -> ?2#(c(f(c(x),c(c(y)))),x,y) 8.68/2.80 h#(a(a(x))) -> h#(x) 8.68/2.80 h#(a(a(x))) -> ?3#(h(x),x) 8.68/2.80 TRS: 8.68/2.80 f(c(x),c(c(y))) -> ?1(c(f(x,y)),x,y) 8.68/2.80 ?1(c(a(b())),x,y) -> a(a(x)) 8.68/2.80 f(c(c(c(x))),y) -> ?2(c(f(c(x),c(c(y)))),x,y) 8.68/2.80 ?2(c(a(a(b()))),x,y) -> a(y) 8.68/2.80 h(b()) -> b() 8.68/2.80 h(a(a(x))) -> ?3(h(x),x) 8.68/2.80 ?3(b(),x) -> a(b()) 8.68/2.80 graph: 8.68/2.80 h#(a(a(x))) -> h#(x) -> h#(a(a(x))) -> ?3#(h(x),x) 8.68/2.80 h#(a(a(x))) -> h#(x) -> h#(a(a(x))) -> h#(x) 8.68/2.80 f#(c(c(c(x))),y) -> f#(c(x),c(c(y))) -> 8.68/2.80 f#(c(c(c(x))),y) -> ?2#(c(f(c(x),c(c(y)))),x,y) 8.68/2.80 f#(c(c(c(x))),y) -> f#(c(x),c(c(y))) -> 8.68/2.80 f#(c(c(c(x))),y) -> f#(c(x),c(c(y))) 8.68/2.80 f#(c(c(c(x))),y) -> f#(c(x),c(c(y))) -> 8.68/2.80 f#(c(x),c(c(y))) -> ?1#(c(f(x,y)),x,y) 8.68/2.80 f#(c(c(c(x))),y) -> f#(c(x),c(c(y))) -> f#(c(x),c(c(y))) -> f#(x,y) 8.68/2.80 f#(c(x),c(c(y))) -> f#(x,y) -> 8.68/2.80 f#(c(c(c(x))),y) -> ?2#(c(f(c(x),c(c(y)))),x,y) 8.68/2.80 f#(c(x),c(c(y))) -> f#(x,y) -> f#(c(c(c(x))),y) -> f#(c(x),c(c(y))) 8.68/2.80 f#(c(x),c(c(y))) -> f#(x,y) -> 8.68/2.80 f#(c(x),c(c(y))) -> ?1#(c(f(x,y)),x,y) 8.68/2.80 f#(c(x),c(c(y))) -> f#(x,y) -> f#(c(x),c(c(y))) -> f#(x,y) 8.68/2.80 SCC Processor: 8.68/2.80 #sccs: 2 8.68/2.80 #rules: 3 8.68/2.80 #arcs: 10/36 8.68/2.80 DPs: 8.68/2.80 f#(c(c(c(x))),y) -> f#(c(x),c(c(y))) 8.68/2.80 f#(c(x),c(c(y))) -> f#(x,y) 8.68/2.80 TRS: 8.68/2.80 f(c(x),c(c(y))) -> ?1(c(f(x,y)),x,y) 8.68/2.80 ?1(c(a(b())),x,y) -> a(a(x)) 8.68/2.80 f(c(c(c(x))),y) -> ?2(c(f(c(x),c(c(y)))),x,y) 8.68/2.83 ?2(c(a(a(b()))),x,y) -> a(y) 8.68/2.83 h(b()) -> b() 8.68/2.83 h(a(a(x))) -> ?3(h(x),x) 8.68/2.83 ?3(b(),x) -> a(b()) 8.68/2.83 Subterm Criterion Processor: 8.68/2.83 simple projection: 8.68/2.83 pi(f#) = 0 8.68/2.83 problem: 8.68/2.83 DPs: 8.68/2.83 8.68/2.83 TRS: 8.68/2.83 f(c(x),c(c(y))) -> ?1(c(f(x,y)),x,y) 8.68/2.83 ?1(c(a(b())),x,y) -> a(a(x)) 8.68/2.83 f(c(c(c(x))),y) -> ?2(c(f(c(x),c(c(y)))),x,y) 8.68/2.83 ?2(c(a(a(b()))),x,y) -> a(y) 8.68/2.83 h(b()) -> b() 8.68/2.83 h(a(a(x))) -> ?3(h(x),x) 8.68/2.83 ?3(b(),x) -> a(b()) 8.68/2.83 Qed 8.68/2.83 8.68/2.83 DPs: 8.68/2.83 h#(a(a(x))) -> h#(x) 8.68/2.83 TRS: 8.68/2.83 f(c(x),c(c(y))) -> ?1(c(f(x,y)),x,y) 8.68/2.83 ?1(c(a(b())),x,y) -> a(a(x)) 8.68/2.83 f(c(c(c(x))),y) -> ?2(c(f(c(x),c(c(y)))),x,y) 8.68/2.83 ?2(c(a(a(b()))),x,y) -> a(y) 8.68/2.83 h(b()) -> b() 8.68/2.83 h(a(a(x))) -> ?3(h(x),x) 8.68/2.83 ?3(b(),x) -> a(b()) 8.68/2.83 Subterm Criterion Processor: 8.68/2.83 simple projection: 8.68/2.83 pi(h#) = 0 8.68/2.83 problem: 8.68/2.83 DPs: 8.68/2.83 8.68/2.83 TRS: 8.68/2.83 f(c(x),c(c(y))) -> ?1(c(f(x,y)),x,y) 8.68/2.83 ?1(c(a(b())),x,y) -> a(a(x)) 8.68/2.83 f(c(c(c(x))),y) -> ?2(c(f(c(x),c(c(y)))),x,y) 8.68/2.83 ?2(c(a(a(b()))),x,y) -> a(y) 8.68/2.83 h(b()) -> b() 8.68/2.83 h(a(a(x))) -> ?3(h(x),x) 8.68/2.83 ?3(b(),x) -> a(b()) 8.68/2.83 Qed 8.68/2.83 All 2 critical pairs are joinable. 8.68/2.83 Overlap: (rule1: f(c(c(c(z))), x') -> a(x') <= c(f(c(z), c(c(x')))) = c(a(a(b))), rule2: f(c(y'), c(c(z'))) -> a(a(y')) <= c(f(y', z')) = c(a(b)), pos: ε, mgu: {(y',c(c(z))), (x',c(c(z')))}) 8.68/2.83 CP: a(a(c(c(z)))) = a(c(c(z'))) <= c(f(c(z), c(c(c(c(z')))))) = c(a(a(b))), c(f(c(c(z)), z')) = c(a(b)) 8.68/2.83 This critical pair is infeasible. 8.68/2.83 This critical pair is conditional. 8.68/2.83 This critical pair has some non-trivial conditions. 8.68/2.83 Call external tool: 8.68/2.83 ./waldmeister 8.68/2.83 Input: 8.68/2.83 f(c(x), c(c(y))) -> a(a(x)) <= c(f(x, y)) = c(a(b)) 8.68/2.83 f(c(c(c(x))), y) -> a(y) <= c(f(c(x), c(c(y)))) = c(a(a(b))) 8.68/2.83 h(b) -> b 8.68/2.83 h(a(a(x))) -> a(b) <= h(x) = b 8.68/2.83 8.68/2.83 By Waldmeister. 8.68/2.83 Overlap: (rule1: f(c(z), c(c(x'))) -> a(a(z)) <= c(f(z, x')) = c(a(b)), rule2: f(c(c(c(y'))), z') -> a(z') <= c(f(c(y'), c(c(z')))) = c(a(a(b))), pos: ε, mgu: {(z,c(c(y'))), (z',c(c(x')))}) 8.68/2.83 CP: a(c(c(x'))) = a(a(c(c(y')))) <= c(f(c(c(y')), x')) = c(a(b)), c(f(c(y'), c(c(c(c(x')))))) = c(a(a(b))) 8.68/2.83 This critical pair is infeasible. 8.68/2.83 This critical pair is conditional. 8.68/2.83 This critical pair has some non-trivial conditions. 8.68/2.83 Call external tool: 8.68/2.83 ./waldmeister 8.68/2.83 Input: 8.68/2.83 f(c(x), c(c(y))) -> a(a(x)) <= c(f(x, y)) = c(a(b)) 8.68/2.83 f(c(c(c(x))), y) -> a(y) <= c(f(c(x), c(c(y)))) = c(a(a(b))) 8.68/2.83 h(b) -> b 8.68/2.83 h(a(a(x))) -> a(b) <= h(x) = b 8.68/2.83 8.68/2.83 By Waldmeister. 8.68/2.83 8.68/2.86 EOF