let l be Instruction-Location of SCM+FSA ; :: 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 SCM+FSA ) = l ) & ( s . a <> 0 implies (Exec (a =0_goto l),s) . (IC SCM+FSA ) = Next ) & ( 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 SCM+FSA ) = l ) & ( s . a <> 0 implies (Exec (a =0_goto l),s) . (IC SCM+FSA ) = Next ) & ( 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 SCM+FSA ) = l ) & ( s . a <> 0 implies (Exec (a =0_goto l),s) . (IC SCM+FSA ) = Next ) & ( 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 , La being Instruction-Location of SCM such that
A1: a = A and
A2: l = La and
A3: a =0_goto l = A =0_goto La by Def17;
reconsider S = (s | SCM-Memory ) +* (NAT --> (A =0_goto La)) as State of SCM by SCMFSA_1:18;
A4: Exec (a =0_goto l),s = (s +* (Exec (A =0_goto La),S)) +* (s | NAT ) by A3, Th75;

hereby :: thesis: ( ( s . a <> 0 implies (Exec (a =0_goto l),s) . (IC SCM+FSA ) = Next ) & ( 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 SCM+FSA ) = l
then A5: S . A = 0 by A1, Th80;
thus (Exec (a =0_goto l),s) . (IC SCM+FSA ) = (Exec (A =0_goto La),S) . (IC SCM ) by A4, Th78
.= l by A2, A5, AMI_3:14 ; :: 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 SCM+FSA ) = Next
then A6: S . A <> 0 by A1, Th80;
thus (Exec (a =0_goto l),s) . (IC SCM+FSA ) = (Exec (A =0_goto La),S) . (IC SCM ) by A4, Th78
.= Next by A6, AMI_3:14
.= Next by Th88 ; :: 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 Th25;
thus (Exec (a =0_goto l),s) . c = (Exec (A =0_goto La),S) . C by A4, Th79
.= S . C by AMI_3:14
.= s . c by Th80 ; :: thesis: verum

end;

let f be FinSeq-Location ; :: thesis: (Exec (a =0_goto l),s) . f = s . f
A7: dom (s | NAT ) = (dom s) /\ NAT by RELAT_1:90;

now

assume f in NAT ; :: thesis: contradiction
then A8: SCM+FSA-OK . f = SCM+FSA-Instr by SCMFSA_1:11;
f in SCM+FSA-Data*-Loc by Def5;
hence contradiction by A8, SCMFSA_1:12, SCMFSA_1:13; :: thesis: verum

end;

then A9: not f in dom (s | NAT ) by A7, XBOOLE_0:def 4;
A10: not f in dom (Exec (A =0_goto La),S) by Th68;
thus (Exec (a =0_goto l),s) . f = (s +* (Exec (A =0_goto La),S)) . f by A4, A9, FUNCT_4:12
.= s . f by A10, FUNCT_4:12 ; :: thesis: verum