for P being Instruction-Sequence of SCM+FSA st Bubble-Sort-Algorithm c= P holds
for f being FinSeq-Location
for k being Nat st k < 53 holds
Bubble-Sort-Algorithm . k = P . k