theorem Th64: :: SCMFSA_2:71

for l being Nat
for a being Int-Location
for s being State of SCM+FSA holds
( ( s . a > 0 implies (Exec ((a >0_goto l),s)) . (IC ) = l ) & ( s . a <= 0 implies (Exec ((a >0_goto l),s)) . (IC ) = (IC s) + 1 ) & ( for c being Int-Location holds (Exec ((a >0_goto l),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a >0_goto l),s)) . f = s . f ) )