let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for s being State of S
for k being Element of NAT
for x being Instruction of S holds NPP (s +* (k,x)) = NPP s
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for s being State of S
for k being Element of NAT
for x being Instruction of S holds NPP (s +* (k,x)) = NPP s
let s be State of S; :: thesis: for k being Element of NAT
for x being Instruction of S holds NPP (s +* (k,x)) = NPP s
let k be Element of NAT ; :: thesis: for x being Instruction of S holds NPP (s +* (k,x)) = NPP s
let x be Instruction of S; :: thesis: NPP (s +* (k,x)) = NPP s
k in dom s by Th23;
hence NPP (s +* (k,x)) = NPP (s +* (k .--> x)) by FUNCT_7:def 3
.= (NPP s) +* (NPP (k .--> x)) by Th221
.= (NPP s) +* {}
.= NPP s by FUNCT_4:22 ;
:: thesis: verum