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