0.00/0.01	YES
0.00/0.01	
0.00/0.01	By left-linear and trivial overlapping.
0.00/0.01	
0.00/0.01	1: Overlap (1)-(2)--- F|-> z1.(S'@z1) --------------------------------------------------
0.00/0.01	   (1) |abs(x.F[x])|@S => F[S]
0.00/0.01	   (2) abs(x'.(S'@x')) => S'
0.00/0.01	                                      abs(x.(S'@x))@S
0.00/0.01	                                 S'@S <-(1)-/\-(2)-> S'@S
0.00/0.01	                                 ---> S'@S =OK= S'@S <---
0.00/0.01	2: Overlap (2)-(1_x)--- S|-> abs(x'.H3[x']), F'|-> z1.z2.H3[z2], S'|-> z1.z1 ----------------
0.00/0.01	   (2) abs(x.|(S@x)|) => S
0.00/0.01	   (1_x) abs(x'.F'[x,x'])@S'[x] => F'[x,S'[x]]
0.00/0.01	                                 abs(x.(abs(x'.H3[x'])@x))
0.00/0.01	                       abs(x'.H3[x']) <-(2)-/\-(1_x)-> abs(x.H3[x])
0.00/0.01	                       ---> abs(x'.H3[x']) =E= abs(x.H3[x]) <---
0.00/0.01	.
0.00/0.01	
0.00/0.01	
0.00/0.01	******** Signature ********
0.00/0.01	abs : (term -> term) -> term
0.00/0.01	app : term -> term -> term
0.00/0.01	
0.00/0.01	******** Computation rules ********
0.00/0.01	 (1)  abs(x.F[x])@S => F[S]
0.00/0.01	 (2)  abs(x.(S@x)) => S
0.00/0.01	
0.00/0.01	YES
0.00/0.01	EOF