let N be non empty with_non-empty_elements set ; for S being non empty stored-program IC-Ins-separated definite realistic 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 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 16 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 COMPOS_1:def 6;
reconsider I =
i as
Element of the
Object-Kind of
S . il by COMPOS_1:def 8;
set t = the
State of
S;
set P = the the
Instructions of
S -valued ManySortedSet of
NAT ;
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 PBOOLE:155;
il in NAT
;
then X:
il in dom the the
Instructions of
S -valued ManySortedSet of
NAT
by PARTFUN1:def 4;
A6:
( the the Instructions of S -valued ManySortedSet of NAT +* (il,i)) /. il =
( the the Instructions of S -valued ManySortedSet of NAT +* (il,i)) . il
by PBOOLE:158
.=
i
by X, FUNCT_7:33
;
IC in dom the
State of
S
by COMPOS_1:9;
then A7:
IC u = il
by FUNCT_7:33;
then
IC (Following (( the the Instructions of S -valued ManySortedSet of NAT +* (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:2; verum