::theorem :: COMPOS_1:23
:: for S being COM-Struct,
:: F, G being initial non empty finite preProgram of S
:: holds (F ';' G).LastLoc F = IncAddr(G,card F -' 1).0;
::theorem :: COMPOS_1:24
:: for S being COM-Struct,
:: F, G being initial non empty finite preProgram of S,
:: f being Nat st f < card F - 1
:: holds IncAddr(F,card F -' 1).f = IncAddr(F ';' G, card F -' 1).f;
:: Zeby moc mowic o tym, ze Reloc(I,k) jest closed
:: trzebaby ten atrybut zdefiniowac ogolniej
:: ale wtedy trzeba wykorzystac fakt, ze sekwencyjnie
:: przejscie nie moze sie cofac. Czyli maszyna
:: musi byc standard.
:: Potrzeba nam wiec raczej to, ze tak psedomakroinstrukcja
:: jest "contigious" a niekoniecznie "initial"
:: Definicje moze bez trudu zrobic ogolniejsza.