let N be non empty with_non-empty_elements set ; :: thesis: 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 halting holds
NIC (i,il) = {il}
let S be non empty stored-program IC-Ins-separated definite realistic AMI-Struct of N; :: thesis: for il being Element of NAT
for i being Instruction of S st i is halting holds
NIC (i,il) = {il}
let il be Element of 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 set ; :: 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 Object-Kind 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;

reconsider f = ((IC ),il) --> (il,i) as PartState of S by COMPOS_1:37;
set s = the State of S;
let n be set ; :: according to TARSKI:def 3 :: thesis: ( not n in {il} or n in NIC (i,il) )
assume A2: n in {il} ; :: thesis: n in NIC (i,il)
set a = the State of S +* f;
A3: dom f = {(IC ),il} by FUNCT_4:65;
then IC in dom f by TARSKI:def 2;
then A4: ( the State of S +* f) . (IC ) = f . (IC ) by FUNCT_4:14
.= il by COMPOS_1:3, FUNCT_4:66 ;
A5: il in dom f by A3, TARSKI:def 2;
(ProgramPart ( the State of S +* f)) /. (IC ( the State of S +* f)) = ( the State of S +* f) . (IC ( the State of S +* f)) by COMPOS_1:38
.= f . il by A4, A5, FUNCT_4:14
.= i by FUNCT_4:66 ;
then IC (Following ((ProgramPart ( the State of S +* f)),( the State of S +* f))) = ( the State of S +* f) . (IC ) by A1
.= n by A2, A4, TARSKI:def 1 ;
hence n in NIC (i,il) by Lm1; :: thesis: verum