begin
Lm1:
for T being InsType of {[0,{},{}]} holds JumpParts T = {0}
Lm2:
for S being non empty standard-ins homogeneous set
for I being Element of S
for x being set st x in dom (JumpPart I) holds
(product" (JumpParts (InsCode I))) . x c= NAT
Lm3:
for S being non empty standard-ins homogeneous set st S is J/A-independent holds
for I being Element of S
for x being set st x in dom (JumpPart I) holds
NAT c= (product" (JumpParts (InsCode I))) . x
Lm4:
for T being InsType of {[0,{},{}],[1,{},{}]} holds JumpParts T = {0}
registration
coherence
( {[0,{},{}],[1,{},{}]} is J/A-independent & {[0,{},{}],[1,{},{}]} is homogeneous )
end;
begin
begin
:: zero i zeby ta instrukcja to byla [0,{},{}], a wiec ma byc jedyna
:: instrukcja o kodzie 0. Wymaga to modyfikacji
:: maszyny SCMPDS, gdzie z instrukcje halt robi goto 0 (tzn. przeskok
:: o 0);