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 } ;

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 } ) )

hence
NIC (i,l) = {(z + 1)}
by TARSKI:2; :: thesis: verum( ( 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;

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;

then A5: y = z + 1 by TARSKI:def 1;

IC in dom ((IC ) .--> l9) by 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 A2, 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; :: thesis: verum

end;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;

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;

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 {(z + 1)}
; :: thesis: 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;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

then A5: y = z + 1 by TARSKI:def 1;

IC in dom ((IC ) .--> l9) by 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 A2, 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; :: thesis: verum