0.00/0.99 YES 0.00/0.99 0.00/0.99 Problem: 0.00/0.99 f(x) -> c() <= a() = b() 0.00/0.99 g(x, x) -> g(f(a()), f(b())) 0.00/0.99 0.00/0.99 Proof: 0.00/0.99 This system is confluent. 0.00/0.99 By \cite{GNG13}, Theorem 9. 0.00/0.99 This system is of type 3 or smaller. 0.00/0.99 This system is deterministic. 0.00/0.99 This system is weakly left-linear. 0.00/0.99 System R transformed to optimized U(R). 0.00/0.99 This system is confluent. 0.00/0.99 Call external tool: 0.00/0.99 ./csi.sh 0.00/0.99 Input: 0.00/0.99 ?1(b(), x) -> c() 0.00/0.99 f(x) -> ?1(a(), x) 0.00/0.99 g(x, x) -> g(f(a()), f(b())) 0.00/0.99 0.00/0.99 Church Rosser Transformation Processor (kb): 0.00/0.99 ?1(b(),x) -> c() 0.00/0.99 f(x) -> ?1(a(),x) 0.00/0.99 g(x,x) -> g(f(a()),f(b())) 0.00/0.99 critical peaks: joinable 0.00/0.99 Matrix Interpretation Processor: dim=2 0.00/0.99 0.00/0.99 interpretation: 0.00/0.99 [1 0] [1 0] 0.00/0.99 [g](x0, x1) = [3 1]x0 + [1 0]x1, 0.00/0.99 0.00/0.99 [0] 0.00/0.99 [a] = [0], 0.00/0.99 0.00/0.99 [1 0] 0.00/0.99 [f](x0) = [0 2]x0, 0.00/0.99 0.00/0.99 [0] 0.00/0.99 [c] = [0], 0.00/0.99 0.00/0.99 [1 2] [1 0] 0.00/0.99 [?1](x0, x1) = [0 0]x0 + [0 0]x1, 0.00/0.99 0.00/0.99 [0] 0.00/0.99 [b] = [2] 0.00/0.99 orientation: 0.00/0.99 [1 0] [4] [0] 0.00/0.99 ?1(b(),x) = [0 0]x + [0] >= [0] = c() 0.00/0.99 0.00/0.99 [1 0] [1 0] 0.00/0.99 f(x) = [0 2]x >= [0 0]x = ?1(a(),x) 0.00/0.99 0.00/0.99 [2 0] [0] 0.00/0.99 g(x,x) = [4 1]x >= [0] = g(f(a()),f(b())) 0.00/1.00 problem: 0.00/1.00 f(x) -> ?1(a(),x) 0.00/1.00 g(x,x) -> g(f(a()),f(b())) 0.00/1.00 Bounds Processor: 0.00/1.00 bound: 1 0.00/1.00 enrichment: match 0.00/1.00 automaton: 0.00/1.00 final states: {4,1} 0.00/1.00 transitions: 0.00/1.00 a1() -> 9*,3,8 0.00/1.00 f60() -> 2* 0.00/1.00 ?10(3,3) -> 7* 0.00/1.00 ?10(3,5) -> 6* 0.00/1.00 ?10(3,9) -> 7* 0.00/1.00 ?10(9,2) -> 1* 0.00/1.00 ?10(3,2) -> 1* 0.00/1.00 ?10(9,3) -> 7* 0.00/1.00 ?10(9,5) -> 6* 0.00/1.00 ?10(9,9) -> 7* 0.00/1.00 g0(7,6) -> 4* 0.00/1.00 f0(5) -> 6* 0.00/1.00 f0(9) -> 7* 0.00/1.00 f0(3) -> 7* 0.00/1.00 b0() -> 5* 0.00/1.00 ?11(8,3) -> 7* 0.00/1.00 ?11(8,5) -> 6* 0.00/1.00 ?11(8,9) -> 7* 0.00/1.00 ?11(9,3) -> 7* 0.00/1.00 ?11(9,5) -> 6* 0.00/1.00 ?11(9,9) -> 7* 0.00/1.00 problem: 0.00/1.00 0.00/1.00 Qed 0.00/1.00 0.00/1.00 EOF