let N be non empty with_non-empty_elements set ; for S being non empty IC-Ins-separated 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 IC-Ins-separated 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 ) = succ (IC s)
; AMISTD_1:def 8 NIC (i,il) = {(succ il)}
now let x be
set ;
( x in {(succ il)} iff x in { (IC (Exec (i,ss))) where ss is Element of product the Object-Kind of S : IC ss = il } )A2:
now reconsider il1 =
il as
Element of
ObjectKind (IC ) by MEMSTR_0:def 3;
set I =
i;
set t = the
State of
S;
set P = the
Instruction-Sequence of
S;
assume A3:
x = succ il
;
x in { (IC (Exec (i,ss))) where ss is Element of product the Object-Kind of S : IC ss = il } reconsider u = the
State of
S +* (
(IC ),
il1) as
Element of
product the
Object-Kind of
S by CARD_3:107;
il in NAT
;
then X:
il in dom the
Instruction-Sequence of
S
by PARTFUN1:def 2;
A6:
( the Instruction-Sequence of S +* (il,i)) /. il =
( the Instruction-Sequence of S +* (il,i)) . il
by PBOOLE:143
.=
i
by X, FUNCT_7:31
;
IC in dom the
State of
S
by MEMSTR_0:2;
then A7:
IC u = il
by FUNCT_7:31;
then
IC (Following (( the Instruction-Sequence of S +* (il,i)),u)) = succ il
by A1, A6;
hence
x in { (IC (Exec (i,ss))) where ss is Element of product the Object-Kind of S : IC ss = il }
by A3, A7, A6;
verum end; hence
(
x in {(succ il)} iff
x in { (IC (Exec (i,ss))) where ss is Element of product the Object-Kind of S : IC ss = il } )
by A2, TARSKI:def 1;
verum end;
hence
NIC (i,il) = {(succ il)}
by TARSKI:1; verum