team-worthwhile/worthwhile — comment on commit b557a11052602dd5e0b229a0db4d801f26fab8af
File: validierung/testprogramme/bubblesort2-ext.ww line 54
By bafain:

Try both in one conjunction ` _ensures ∀ Integer i12, 0 ≤ i12 ∧ i12 < length : 0 ≤ _return[length + i12] ∧ _return[length + i12] < length`.