let N be non empty with_non-empty_elements set ; for S being non empty stored-program IC-Ins-separated definite realistic steady-programmed standard AMI-Struct of N
for il being Element of NAT
for i being Instruction of S st i is sequential holds
NIC i,il = {(succ il)}
let S be non empty stored-program IC-Ins-separated definite realistic steady-programmed standard AMI-Struct of N; for il being Element of NAT
for i being Instruction of S st i is sequential holds
NIC i,il = {(succ il)}
let il be Element of NAT ; for i being Instruction of S st i is sequential holds
NIC i,il = {(succ il)}
let i be Instruction of S; ( i is sequential implies NIC i,il = {(succ il)} )
assume A1:
for s being State of S holds (Exec i,s) . (IC S) = succ (IC s)
; AMISTD_1:def 16 NIC i,il = {(succ il)}
now let x be
set ;
( x in {(succ il)} iff x in { (IC (Following (ProgramPart ss),ss)) where ss is Element of product the Object-Kind of S : ( IC ss = il & (ProgramPart ss) /. il = i ) } )A2:
now reconsider il1 =
il as
Element of
ObjectKind (IC S) by COMPOS_1:def 6;
reconsider I =
i as
Element of the
Object-Kind of
S . il by COMPOS_1:def 8;
consider t being
State of
S;
assume A3:
x = succ il
;
x in { (IC (Following (ProgramPart ss),ss)) where ss is Element of product the Object-Kind of S : ( IC ss = il & (ProgramPart ss) /. il = i ) } reconsider f =
(IC S),
il --> il1,
I as
PartState of
S by COMPOS_1:37;
reconsider u =
t +* f as
Element of
product the
Object-Kind of
S by PBOOLE:155;
A4:
dom ((IC S),il --> il1,I) = {(IC S),il}
by FUNCT_4:65;
then X:
il in dom ((IC S),il --> il1,I)
by TARSKI:def 2;
A5:
(ProgramPart u) /. il =
u . il
by COMPOS_1:38
.=
((IC S),il --> il1,I) . il
by X, 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 COMPOS_1:3, FUNCT_4:66
;
then
IC (Following (ProgramPart u),u) = succ il
by A1, A5;
hence
x in { (IC (Following (ProgramPart ss),ss)) where ss is Element of product the Object-Kind of S : ( IC ss = il & (ProgramPart ss) /. il = i ) }
by A3, A6, A5;
verum end; hence
(
x in {(succ il)} iff
x in { (IC (Following (ProgramPart ss),ss)) where ss is Element of product the Object-Kind of S : ( IC ss = il & (ProgramPart ss) /. il = i ) } )
by A2, TARSKI:def 1;
verum end;
hence
NIC i,il = {(succ il)}
by TARSKI:2; verum