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 halting holds
NIC (i,il) = {il}
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 halting holds
NIC (i,il) = {il}
let il be Nat; :: thesis: for i being Instruction of S st i is halting holds
NIC (i,il) = {il}
let i be Instruction of S; :: thesis: ( i is halting implies NIC (i,il) = {il} )
assume A1: for s being State of S holds Exec (i,s) = s ; :: according to EXTPRO_1:def 3 :: thesis: NIC (i,il) = {il}

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {il} c= NIC (i,il)

let n be object ; :: thesis: ( n in NIC (i,il) implies n in {il} )
assume n in NIC (i,il) ; :: thesis: n in {il}
then ex s being Element of product (the_Values_of S) st
( n = IC (Exec (i,s)) & IC s = il ) ;
then n = il by A1;
hence n in {il} by TARSKI:def 1; :: thesis: verum

end;

set s = the State of S;
set P = the Instruction-Sequence of S;
let n be object ; :: according to TARSKI:def 3 :: thesis: ( not n in {il} or n in NIC (i,il) )
assume n in {il} ; :: thesis: n in NIC (i,il)
then A2: n = il by TARSKI:def 1;
il in NAT by ORDINAL1:def 12;
then A3: il in dom the Instruction-Sequence of S by PARTFUN1:def 2;
A4: IC in dom the State of S by MEMSTR_0:2;
then IC ( the State of S +* ((IC ),il)) = il by FUNCT_7:31;
then CurInstr (( the Instruction-Sequence of S +* (il,i)),( the State of S +* ((IC ),il))) = ( the Instruction-Sequence of S +* (il,i)) . il by PBOOLE:143
.= i by A3, FUNCT_7:31 ;
then IC (Following (( the Instruction-Sequence of S +* (il,i)),( the State of S +* ((IC ),il)))) = IC ( the State of S +* ((IC ),il)) by A1
.= n by A2, A4, FUNCT_7:31 ;
hence n in NIC (i,il) by Lm1; :: thesis: verum