---- CR(R cup S) ---- [Klein and Hirokawa, 2012] R: -(+(x,-(x))) -> 0() +(x,-(x)) -> 0() -(+(0(),0())) -> 0() +(0(),0()) -> 0() -(0()) -> 0() S: CP_S(R): -(+(+(___y640,-(___y640)),0())) -> 0() +(+(___y642,-(___y642)),0()) -> 0() -(0()) -> 0() -(+(+(0(),0()),0())) -> 0() +(+(0(),0()),0()) -> 0() -(0()) -> 0() -(+(0(),0())) -> 0() +(0(),0()) -> 0() CR(S): see below. ---- CR(R) ---- [Hirokawa and Middeldorp, 2011] R: CPS'(R): CP(R):