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