property := #witness EFpmax (loc[T4] = T4end_ok, e2e);