let z be natural number ; for N being non empty with_non-empty_elements set
for l being Element of NAT
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 non empty with_non-empty_elements set ; for l being Element of NAT
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 Element of NAT ; 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); ( l = z & InsCode i = 1 implies NIC (i,l) = {(z + 1)} )
assume that
A1:
l = z
and
A2:
InsCode i = 1
; NIC (i,l) = {(z + 1)}
set M = STC N;
set F = { (IC (Exec (i,ss))) where ss is Element of product the Object-Kind of (STC N) : IC ss = l } ;
now reconsider f =
NAT --> i as
Instruction-Sequence of
(STC N) ;
reconsider l9 =
l as
Element of
ObjectKind (IC ) by MEMSTR_0:def 3;
reconsider w = the
l -started State of
(STC N) as
Element of
product the
Object-Kind of
(STC N) by CARD_3:107;
set u =
(IC ) .--> l9;
A3:
dom ((IC ) .--> l9) = {(IC )}
by FUNCOP_1:13;
let y be
set ;
( ( y in { (IC (Exec (i,ss))) where ss is Element of product the Object-Kind 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 Object-Kind of (STC N) : IC ss = l } ) )reconsider t =
w +* ((IC ) .--> l9) as
Element of
product the
Object-Kind of
(STC N) by CARD_3:107;
assume
y in {(z + 1)}
;
y in { (IC (Exec (i,ss))) where ss is Element of product the Object-Kind of (STC N) : IC ss = l } then A7:
y = succ z
by TARSKI:def 1;
IC in dom ((IC ) .--> l9)
by A3, TARSKI:def 1;
then A8:
IC t =
((IC ) .--> l9) . (IC )
by FUNCT_4:13
.=
z
by A1, FUNCOP_1:72
;
then
IC (Exec (i,t)) = succ z
by A2, Lm2;
hence
y in { (IC (Exec (i,ss))) where ss is Element of product the Object-Kind of (STC N) : IC ss = l }
by A1, A7, A8;
verum end;
hence
NIC (i,l) = {(z + 1)}
by TARSKI:1; verum