let z be Nat; :: thesis: for N being with_zero set
for l being Nat
for i being Element of the InstructionsF of (STC N) st l = z & InsCode i = 1 holds
NIC (i,l) = {(z + 1)}
let N be with_zero set ; :: thesis: for l being Nat
for i being Element of the InstructionsF of (STC N) st l = z & InsCode i = 1 holds
NIC (i,l) = {(z + 1)}
let l be Nat; :: thesis: for i being Element of the InstructionsF of (STC N) st l = z & InsCode i = 1 holds
NIC (i,l) = {(z + 1)}
let i be Element of the InstructionsF 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 (Exec (i,ss))) where ss is Element of product (the_Values_of (STC N)) : IC ss = l } ;

now :: thesis: for y being object holds
( ( y in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of (STC N)) : IC ss = l } implies y in {(z + 1)} ) & ( y in {(z + 1)} implies y in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of (STC N)) : IC ss = l } ) )

set f = NAT --> i;
set w = the State of (STC N);
reconsider ll = l as Element of NAT by ORDINAL1:def 12;
reconsider l9 = ll as Element of Values (IC ) by MEMSTR_0:def 6;
set u = (IC ) .--> l9;
A3: dom ((IC ) .--> l9) = {(IC )} by FUNCOP_1:13;
let y be object ; :: thesis: ( ( y in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of (STC N)) : IC ss = l } implies y in {(z + 1)} ) & ( y in {(z + 1)} implies y in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of (STC N)) : IC ss = l } ) )
reconsider t = the State of (STC N) +* ((IC ) .--> l9) as Element of product (the_Values_of (STC N)) by CARD_3:107;
A4: (NAT --> i) /. ll = i by FUNCOP_1:7;

hereby :: thesis: ( y in {(z + 1)} implies y in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of (STC N)) : IC ss = l } )

assume y in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of (STC N)) : IC ss = l } ; :: thesis: y in {(z + 1)}
then ex s being Element of product (the_Values_of (STC N)) st
( y = IC (Exec (i,s)) & IC s = l ) ;
then y = z + 1 by A1, A2, Lm3;
hence y in {(z + 1)} by TARSKI:def 1; :: thesis: verum

end;

assume y in {(z + 1)} ; :: thesis: y in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of (STC N)) : IC ss = l }
then A5: y = z + 1 by TARSKI:def 1;
IC in dom ((IC ) .--> l9) by A3, TARSKI:def 1;
then A6: IC t = ((IC ) .--> l9) . (IC ) by FUNCT_4:13
.= z by A1, FUNCOP_1:72 ;
then IC (Following ((NAT --> i),t)) = z + 1 by A1, A2, A4, Lm3;
hence y in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of (STC N)) : IC ss = l } by A1, A5, A6, A4; :: thesis: verum

end;

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