let s1, s2 be State of SCM+FSA; :: thesis: for I, J being Program of SCM+FSA st DataPart s1 = DataPart s2 holds
NPP (Initialize s1) = NPP (Initialize s2)
let I, J be Program of SCM+FSA; :: thesis: ( DataPart s1 = DataPart s2 implies NPP (Initialize s1) = NPP (Initialize s2) )
assume A1: DataPart s1 = DataPart s2 ; :: thesis: NPP (Initialize s1) = NPP (Initialize s2)
set S2 = Initialize s2;
set S1 = Initialize s1;
IC in dom (Start-At (0,SCM+FSA)) by COMPOS_1:52;
then A2: IC (Initialize s1) = IC (Start-At (0,SCM+FSA)) by FUNCT_4:14
.= 0 by COMPOS_1:64 ;
IC in dom (Start-At (0,SCM+FSA)) by COMPOS_1:52;
then A3: IC (Initialize s2) = IC (Start-At (0,SCM+FSA)) by FUNCT_4:14
.= 0 by COMPOS_1:64 ;
DataPart (Initialize s1) = DataPart s1 by SCMFSA8A:10
.= DataPart (Initialize s2) by A1, SCMFSA8A:10 ;
hence NPP (Initialize s1) = NPP (Initialize s2) by A2, A3, SCMFSA8A:6; :: thesis: verum