signature { automatic } theory
{
down (N1 []([]( down( N2 (N1:<>(N2))))));
[]<>true;
[] (down (N1 (!<>N1)))
}