begin
begin
begin
begin
begin
Lm2:
for S being COM-Struct holds (card (Stop S)) -' 1 = 0
Lm3:
for S being COM-Struct holds LastLoc (Stop S) = 0
Lm4:
for k being Nat holds - 1 < k
;
Lm5:
for k being Nat
for a, b, c being Element of NAT st 1 <= a & 2 <= b & not k < a - 1 & not ( a <= k & k <= (a + b) - 3 ) & not k = (a + b) - 2 & not (a + b) - 2 < k holds
k = a - 1
begin
begin
begin
begin
begin
:: halt SCM-Instr, zamiast halt SCM, zreszta wyrzucenie jej
:: spowodowaloby problemy z typowaniem.