begin
A(N0 & E true)
end