let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic standard AMI-Struct of NAT ,N
for il being Instruction-Location of S
for i being Instruction of S st i is sequential holds
NIC i,il = {(NextLoc il)}
let S be non empty stored-program IC-Ins-separated definite realistic standard AMI-Struct of NAT ,N; :: thesis: for il being Instruction-Location of S
for i being Instruction of S st i is sequential holds
NIC i,il = {(NextLoc il)}
let il be Instruction-Location of S; :: thesis: for i being Instruction of S st i is sequential holds
NIC i,il = {(NextLoc il)}
let i be Instruction of S; :: thesis: ( i is sequential implies NIC i,il = {(NextLoc il)} )
assume A1:
for s being State of S holds (Exec i,s) . (IC S) = NextLoc (IC s)
; :: according to AMISTD_1:def 16 :: thesis: NIC i,il = {(NextLoc il)}
now let x be
set ;
:: thesis: ( x in {(NextLoc il)} iff x in { (IC (Following s)) where s is State of S : ( IC s = il & s . il = i ) } )A2:
now assume A3:
x = NextLoc il
;
:: thesis: x in { (IC (Following s)) where s is State of S : ( IC s = il & s . il = i ) } consider t being
State of
S;
il in NAT
by AMI_1:def 4;
then reconsider il1 =
il as
Element of
ObjectKind (IC S) by AMI_1:def 11;
reconsider I =
i as
Element of
ObjectKind il by AMI_1:def 14;
reconsider u =
t +* ((IC S),il --> il1,I) as
State of
S ;
A4:
dom ((IC S),il --> il1,I) = {(IC S),il}
by FUNCT_4:65;
then A5:
IC S in dom ((IC S),il --> il1,I)
by TARSKI:def 2;
A7:
IC u =
((IC S),il --> il1,I) . (IC S)
by A5, FUNCT_4:14
.=
il
by AMI_1:48, FUNCT_4:66
;
il in dom ((IC S),il --> il1,I)
by A4, TARSKI:def 2;
then A8:
u . il =
((IC S),il --> il1,I) . il
by FUNCT_4:14
.=
i
by FUNCT_4:66
;
then
IC (Following u) = NextLoc il
by A1, A7;
hence
x in { (IC (Following s)) where s is State of S : ( IC s = il & s . il = i ) }
by A3, A7, A8;
:: thesis: verum end; hence
(
x in {(NextLoc il)} iff
x in { (IC (Following s)) where s is State of S : ( IC s = il & s . il = i ) } )
by A2, TARSKI:def 1;
:: thesis: verum end;
hence
NIC i,il = {(NextLoc il)}
by TARSKI:2; :: thesis: verum