let z be natural number ; :: thesis: for N being with_non-empty_elements set
for l being Instruction-Location of STC N
for i being Element of the Instructions of (STC N) st l = z & InsCode i = 1 holds
NIC i,l = {(z + 1)}
let N be with_non-empty_elements set ; :: thesis: for l being Instruction-Location of STC N
for i being Element of the Instructions of (STC N) st l = z & InsCode i = 1 holds
NIC i,l = {(z + 1)}
let l be Instruction-Location of STC N; :: thesis: for i being Element of the Instructions of (STC N) st l = z & InsCode i = 1 holds
NIC i,l = {(z + 1)}
let i be Element of the Instructions of (STC N); :: thesis: ( l = z & InsCode i = 1 implies NIC i,l = {(z + 1)} )
assume that
A1: l = z and
A2: InsCode i = 1 ; :: thesis: NIC i,l = {(z + 1)}
set M = STC N;
set F = { (IC (Following s)) where s is State of (STC N) : ( IC s = l & s . l = i ) } ;

now

let y be set ; :: thesis: ( ( y in { (IC (Following s)) where s is State of (STC N) : ( IC s = l & s . l = i ) } implies y in {(z + 1)} ) & ( y in {(z + 1)} implies y in { (IC (Following s)) where s is State of (STC N) : ( IC s = l & s . l = i ) } ) )

hereby :: thesis: ( y in {(z + 1)} implies y in { (IC (Following s)) where s is State of (STC N) : ( IC s = l & s . l = i ) } )

assume y in { (IC (Following s)) where s is State of (STC N) : ( IC s = l & s . l = i ) } ; :: thesis: y in {(z + 1)}
then consider s being State of (STC N) such that
A3: ( y = IC (Following s) & IC s = l & s . l = i ) ;
y = succ z by A1, A2, A3, Lm4
.= z + 1 ;
hence y in {(z + 1)} by TARSKI:def 1; :: thesis: verum

end;

assume y in {(z + 1)} ; :: thesis: y in { (IC (Following s)) where s is State of (STC N) : ( IC s = l & s . l = i ) }
then A4: y = z + 1 by TARSKI:def 1
.= succ z ;
consider w being State of (STC N);
set f = NAT --> i;
A5: dom (NAT --> i) = NAT by FUNCOP_1:19;
A6: l in NAT by AMI_1:def 4;
reconsider s = w +* (NAT --> i) as State of (STC N) by Th11;
reconsider l' = l as Element of ObjectKind (IC (STC N)) by A6, AMI_1:def 11;
set u = (IC (STC N)) .--> l';
set t = s +* ((IC (STC N)) .--> l');
A7: dom ((IC (STC N)) .--> l') = {(IC (STC N))} by FUNCOP_1:19;
then IC (STC N) in dom ((IC (STC N)) .--> l') by TARSKI:def 1;
then A8: IC (s +* ((IC (STC N)) .--> l')) = ((IC (STC N)) .--> l') . (IC (STC N)) by FUNCT_4:14
.= z by A1, FUNCOP_1:87 ;
l <> IC (STC N) by AMI_1:48;
then not l in dom ((IC (STC N)) .--> l') by A7, TARSKI:def 1;
then A9: (s +* ((IC (STC N)) .--> l')) . l = s . l by FUNCT_4:12
.= (NAT --> i) . l by A5, A6, FUNCT_4:14
.= i by A6, FUNCOP_1:13 ;
then IC (Following (s +* ((IC (STC N)) .--> l'))) = succ z by A1, A2, A8, Lm4;
hence y in { (IC (Following s)) where s is State of (STC N) : ( IC s = l & s . l = i ) } by A1, A4, A8, A9; :: thesis: verum

end;

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