let s1, s2 be State of SCM+FSA; :: thesis: for I, J being Program of SCM+FSA st DataPart s1 = DataPart s2 holds
Initialize s1 = Initialize s2
let I, J be Program of SCM+FSA; :: thesis: ( DataPart s1 = DataPart s2 implies Initialize s1 = Initialize s2 )
assume A1: DataPart s1 = DataPart s2 ; :: thesis: Initialize s1 = Initialize s2
set S2 = Initialize s2;
set S1 = Initialize s1;
IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
then A2: IC (Initialize s1) = IC (Start-At (0,SCM+FSA)) by FUNCT_4:13
.= 0 by FUNCOP_1:72 ;
IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
then A3: IC (Initialize s2) = IC (Start-At (0,SCM+FSA)) by FUNCT_4:13
.= 0 by FUNCOP_1:72 ;
DataPart (Initialize s1) = DataPart s1 by MEMSTR_0:79
.= DataPart (Initialize s2) by A1, MEMSTR_0:79 ;
hence Initialize s1 = Initialize s2 by A2, A3, MEMSTR_0:78; :: thesis: verum