let l be Nat; :: thesis: 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 ) )
let a be Int-Location; :: thesis: 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 ) )
let s be State of SCM+FSA; :: thesis: ( ( 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 ) )
consider A being Data-Location such that
A1: a = A and
A2: a >0_goto l = A >0_goto l by Def13;
reconsider S = s | SCM-Memory as State of SCM by Th42;
A3: Exec ((a >0_goto l),s) = s +* (Exec ((A >0_goto l),S)) by A2, Th44;
hereby :: thesis: ( ( 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 ) )
assume s . a > 0 ; :: thesis: (Exec ((a >0_goto l),s)) . (IC ) = l
then A4: S . A > 0 by A1, Th48;
thus (Exec ((a >0_goto l),s)) . (IC ) = (Exec ((A >0_goto l),S)) . (IC ) by A3, Th46
.= l by A4, AMI_3:9 ; :: thesis: verum
end;
hereby :: thesis: ( ( 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 ) )
assume s . a <= 0 ; :: thesis: (Exec ((a >0_goto l),s)) . (IC ) = (IC s) + 1
then A5: S . A <= 0 by A1, Th48;
thus (Exec ((a >0_goto l),s)) . (IC ) = (Exec ((A >0_goto l),S)) . (IC ) by A3, Th46
.= (IC S) + 1 by A5, AMI_3:9
.= (IC s) + 1 by Th55 ; :: thesis: verum
end;
hereby :: thesis: for f being FinSeq-Location holds (Exec ((a >0_goto l),s)) . f = s . f
let c be Int-Location; :: thesis: (Exec ((a >0_goto l),s)) . c = s . c
reconsider C = c as Data-Location by Th5;
thus (Exec ((a >0_goto l),s)) . c = (Exec ((A >0_goto l),S)) . C by A3, Th47
.= S . C by AMI_3:9
.= s . c by Th48 ; :: thesis: verum
end;
let f be FinSeq-Location ; :: thesis: (Exec ((a >0_goto l),s)) . f = s . f
A6: not f in dom (Exec ((A >0_goto l),S)) by Th37;
thus (Exec ((a >0_goto l),s)) . f = s . f by A3, A6, FUNCT_4:11; :: thesis: verum