/*
 The function Prefix checks whether its first argument is a prefix of the second in the alphabet {'A','B'}.
 The function Concat is concatenation, done from the end of the string.
 The task of the supercompiler is to verify whether the concatenation function processing the string from the end
 does not change its first argument.
*/

/***********************************************/
/*           the input program                 */
/***********************************************/

$ENTRY Go {
	 (e.x) e.y = <Prefix (e.x) <Concat (e.x) e.y>>;
}

Prefix {
	( ) e.x = 'T';
	(t.y e.x1) t.y e.x2 = <Prefix (e.x1) e.x2>;
	('A' e.x1) 'B' e.x2 = 'F';
	('B' e.x1) 'A' e.x2 = 'F';
	(t.y e.x) = 'F';
}

Concat {
	(e.x) = e.x;
	(e.x1) e.x2 t.y = <Concat (e.x1) e.x2> t.y;
}

/*********************************************************************************/
/*                     the residual program                                      */
/*********************************************************************************/
/*
$ENTRY Go {
 (e.x1) e.x2 =  <Prefix_0 (e.x1) (e.x2) ()>;
}


Prefix_12_0 {
 () (e.x1) =  'T';
 (t.y1 e.x1) (e.x2) =  <Prefix_12_0 (e.x1) (e.x2)>;
}


Prefix_0 {
 (e.x1) () (e.x2) =  <Prefix_12_0 (e.x1) (e.x2)>;
 (e.x1) (e.x2 t.y1) (e.x3) =  <Prefix_0 (e.x1) (e.x2) (t.y1 e.x3)>;
}

*/