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 s1, s2 being State of S st NPP s1 = NPP s2 holds
NPP (Initialize s1) = NPP (Initialize s2)
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for s1, s2 being State of S st NPP s1 = NPP s2 holds
NPP (Initialize s1) = NPP (Initialize s2)
let s1, s2 be State of S; :: thesis: ( NPP s1 = NPP s2 implies NPP (Initialize s1) = NPP (Initialize s2) )
assume Z: NPP s1 = NPP s2 ; :: thesis: NPP (Initialize s1) = NPP (Initialize s2)
thus NPP (Initialize s1) = (NPP s1) +* (NPP (Start-At (0,S))) by Lm221
.= NPP (Initialize s2) by Z, Lm221 ; :: thesis: verum