if (ind1 < ind2) //Из Inv & ~B1 & ~B2 & B3 следует истинность: //((tower1[ind1] >= item)&&(tower1[ind2]<item))==true. //Это условие гарантирует, что последующий обмен //элементов обеспечит выполнение инварианта Inv { temp = tower1[ind1]; tower1[ind1] = tower1[ind2]; tower1[ind2] = temp; ind1++; ind2--; } //(Inv ==true) } //из условия окончания цикла следует: (S2 - пустое множество) if (ind1 == start) //В этой точке S1 и S2 - это пустые множества, -> //(S3 = tower1) |