let z be Nat; :: thesis: for N being with_zero set
for l being Element of 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 Element of 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 Element of 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 } ) )

reconsider f = NAT --> i as Instruction-Sequence of (STC N) ;
reconsider l9 = l as Element of Values (IC ) by MEMSTR_0:def 6;
reconsider w = the l -started State of (STC N) as Element of product (the_Values_of (STC N)) by CARD_3:107;
set u = (IC ) .--> l9;
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 = w +* ((IC ) .--> l9) as Element of product (the_Values_of (STC N)) by CARD_3:107;

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, Lm2;
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 A4: y = z + 1 by TARSKI:def 1;
IC in dom ((IC ) .--> l9) by TARSKI:def 1;
then A5: IC t = ((IC ) .--> l9) . (IC ) by FUNCT_4:13
.= z by A1, FUNCOP_1:72 ;
then IC (Exec (i,t)) = z + 1 by A2, Lm2;
hence y in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of (STC N)) : IC ss = l } by A1, A4, A5; :: thesis: verum

end;

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