theorem :: SCPISORT:15

for n, p0 being Nat st p0 >= 7 holds
insert-sort (n,p0) is parahalting