signature { automatic } theory
{
p1 v <><><><>p1 v down(N1 <>(N1:[]p1));
A !p1
}