let N be non empty with_non-empty_elements set ; for S being non empty stored-program IC-Ins-separated definite realistic standard AMI-Struct of N
for il being Element of NAT
for i being Instruction of S st i is sequential holds
NIC (i,il) = {(succ il)}
let S be non empty stored-program IC-Ins-separated definite realistic standard AMI-Struct of N; for il being Element of NAT
for i being Instruction of S st i is sequential holds
NIC (i,il) = {(succ il)}
let il be Element of NAT ; for i being Instruction of S st i is sequential holds
NIC (i,il) = {(succ il)}
let i be Instruction of S; ( i is sequential implies NIC (i,il) = {(succ il)} )
assume A1:
for s being State of S holds (Exec (i,s)) . (IC S) = succ (IC s)
; AMISTD_1:def 16 NIC (i,il) = {(succ il)}
now let x be
set ;
( x in {(succ il)} iff x in { (IC (Exec (i,ss))) where ss is Element of product the Object-Kind of S : IC ss = il } )A2:
now reconsider il1 =
il as
Element of
ObjectKind (IC S) by COMPOS_1:def 6;
reconsider I =
i as
Element of the
Object-Kind of
S . il by COMPOS_1:def 8;
consider t being
State of
S;
assume A3:
x = succ il
;
x in { (IC (Exec (i,ss))) where ss is Element of product the Object-Kind of S : IC ss = il } reconsider f = (
(IC S),
il)
--> (
il1,
I) as
PartState of
S by COMPOS_1:37;
reconsider u =
t +* f as
Element of
product the
Object-Kind of
S by PBOOLE:155;
A4:
dom (((IC S),il) --> (il1,I)) = {(IC S),il}
by FUNCT_4:65;
then X:
il in dom (((IC S),il) --> (il1,I))
by TARSKI:def 2;
A5:
(ProgramPart u) /. il =
u . il
by COMPOS_1:38
.=
(((IC S),il) --> (il1,I)) . il
by X, FUNCT_4:14
.=
i
by FUNCT_4:66
;
IC S in dom (((IC S),il) --> (il1,I))
by A4, TARSKI:def 2;
then A6:
IC u =
(((IC S),il) --> (il1,I)) . (IC S)
by FUNCT_4:14
.=
il
by COMPOS_1:3, FUNCT_4:66
;
then
IC (Following ((ProgramPart u),u)) = succ il
by A1, A5;
hence
x in { (IC (Exec (i,ss))) where ss is Element of product the Object-Kind of S : IC ss = il }
by A3, A6, A5;
verum end; hence
(
x in {(succ il)} iff
x in { (IC (Exec (i,ss))) where ss is Element of product the Object-Kind of S : IC ss = il } )
by A2, TARSKI:def 1;
verum end;
hence
NIC (i,il) = {(succ il)}
by TARSKI:2; verum