patience: version with fully proved invariant, but still main property remains to prove