let N be non empty with_non-empty_elements set ; :: thesis: for l being Element of NAT
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for s being State of S holds NPP (DecIC (s,l)) = DecIC ((NPP s),l)
let l be Element of NAT ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for s being State of S holds NPP (DecIC (s,l)) = DecIC ((NPP s),l)
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for s being State of S holds NPP (DecIC (s,l)) = DecIC ((NPP s),l)
let s be State of S; :: thesis: NPP (DecIC (s,l)) = DecIC ((NPP s),l)
A: IC in dom s by Lm6;
thus NPP (DecIC (s,l)) = (NPP s) +* (NPP (Start-At (((IC s) -' l),S))) by Th221
.= (NPP s) +* (Start-At (((IC s) -' l),S)) by Th212
.= (NPP s) +* (Start-At (((IC (NPP s)) -' l),S)) by A, Th72
.= DecIC ((NPP s),l) ; :: thesis: verum