let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for il being Nat
for i being Instruction of S st i is sequential holds
NIC (i,il) = {(il + 1)}
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; :: thesis: for il being Nat
for i being Instruction of S st i is sequential holds
NIC (i,il) = {(il + 1)}
let il be Nat; :: thesis: for i being Instruction of S st i is sequential holds
NIC (i,il) = {(il + 1)}
let i be Instruction of S; :: thesis: ( i is sequential implies NIC (i,il) = {(il + 1)} )
assume A1: for s being State of S holds (Exec (i,s)) . (IC ) = (IC s) + 1 ; :: according to AMISTD_1:def 8 :: thesis: NIC (i,il) = {(il + 1)}

now :: thesis: for x being object holds
( x in {(il + 1)} iff x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il } )

let x be object ; :: thesis: ( x in {(il + 1)} iff x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il } )

A2: now :: thesis: ( x = il + 1 implies x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il } )

reconsider ll = il as Element of NAT by ORDINAL1:def 12;
reconsider il1 = ll as Element of Values (IC ) by MEMSTR_0:def 6;
set I = i;
set t = the State of S;
set P = the Instruction-Sequence of S;
assume A3: x = il + 1 ; :: thesis: x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il }
reconsider u = the State of S +* ((IC ),il1) as Element of product (the_Values_of S) by CARD_3:107;
ll in NAT ;
then A4: il in dom the Instruction-Sequence of S by PARTFUN1:def 2;
A5: ( the Instruction-Sequence of S +* (il,i)) /. ll = ( the Instruction-Sequence of S +* (il,i)) . ll by PBOOLE:143
.= i by A4, FUNCT_7:31 ;
IC in dom the State of S by MEMSTR_0:2;
then A6: IC u = il by FUNCT_7:31;
then IC (Following (( the Instruction-Sequence of S +* (il,i)),u)) = il + 1 by A1, A5;
hence x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il } by A3, A6, A5; :: thesis: verum

end;

now :: thesis: ( x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il } implies x = il + 1 )

assume x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il } ; :: thesis: x = il + 1
then ex s being Element of product (the_Values_of S) st
( x = IC (Exec (i,s)) & IC s = il ) ;
hence x = il + 1 by A1; :: thesis: verum

end;

hence ( x in {(il + 1)} iff x in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = il } ) by A2, TARSKI:def 1; :: thesis: verum

end;

hence NIC (i,il) = {(il + 1)} by TARSKI:2; :: thesis: verum