let R be good Ring; :: thesis: for l being Element of NAT
for i being Instruction of (SCM R) st ( for s being State of (SCM R) st IC s = l & s . l = i holds
(Exec i,s) . (IC (SCM R)) = succ (IC s) ) holds
NIC i,l = {(succ l)}
let l be Element of NAT ; :: thesis: for i being Instruction of (SCM R) st ( for s being State of (SCM R) st IC s = l & s . l = i holds
(Exec i,s) . (IC (SCM R)) = succ (IC s) ) holds
NIC i,l = {(succ l)}
let i be Instruction of (SCM R); :: thesis: ( ( for s being State of (SCM R) st IC s = l & s . l = i holds
(Exec i,s) . (IC (SCM R)) = succ (IC s) ) implies NIC i,l = {(succ l)} )
consider t being State of (SCM R);
reconsider I = i as Element of the Object-Kind of (SCM R) . l by AMI_1:def 14;
assume A1: for s being State of (SCM R) st IC s = l & s . l = i holds
(Exec i,s) . (IC (SCM R)) = succ (IC s) ; :: thesis: NIC i,l = {(succ l)}

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

let x be set ; :: thesis: ( x in NIC i,l implies x in {(succ l)} )
assume x in NIC i,l ; :: thesis: x in {(succ l)}
then consider s being Element of product the Object-Kind of (SCM R) such that
W: ( x = IC (Following (ProgramPart s),s) & IC s = l & (ProgramPart s) /. l = i ) ;
(ProgramPart s) /. l = s . l by AMI_1:150;
then x = succ l by A1, W;
hence x in {(succ l)} by TARSKI:def 1; :: thesis: verum

end;

reconsider il1 = l as Element of ObjectKind (IC (SCM R)) by AMI_1:def 11;
reconsider p = (IC (SCM R)),l --> il1,I as PartState of (SCM R) by AMI_1:149;
reconsider u = t +* p as Element of product the Object-Kind of (SCM R) by PBOOLE:155;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(succ l)} or x in NIC i,l )
X: (ProgramPart u) /. l = u . l by AMI_1:150;
assume x in {(succ l)} ; :: thesis: x in NIC i,l
then A2: x = succ l by TARSKI:def 1;
A3: ( IC u = l & u . l = i ) by AMI_1:133;
then IC (Following (ProgramPart u),u) = succ l by A1, X;
hence x in NIC i,l by A2, A3, X; :: thesis: verum