let P1, P2 be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s1,P1 & Start-At (0,SCM+FSA) c= s1 & Start-At (0,SCM+FSA) c= s2 & I c= P1 & I c= P2 & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
let s1, s2 be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA st I is_closed_on s1,P1 & Start-At (0,SCM+FSA) c= s1 & Start-At (0,SCM+FSA) c= s2 & I c= P1 & I c= P2 & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
let J be Program of SCM+FSA; :: thesis: ( J is_closed_on s1,P1 & Start-At (0,SCM+FSA) c= s1 & Start-At (0,SCM+FSA) c= s2 & J c= P1 & J c= P2 & DataPart s1 = DataPart s2 implies for i being Element of NAT holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) )
assume that
A1: J is_closed_on s1,P1 and
A2: Start-At (0,SCM+FSA) c= s1 and
A3: Start-At (0,SCM+FSA) c= s2 and
A4: J c= P1 and
A5: J c= P2 and
A6: DataPart s1 = DataPart s2 ; :: thesis: for i being Element of NAT holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
A7: Reloc (J,0) = J by COMPOS_1:157;
let i be Element of NAT ; :: thesis: ( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
X: IC in dom (Start-At (0,SCM+FSA)) by COMPOS_1:52;
A8: (IC (Comput (P1,s1,i))) + 0 = IC (Comput (P1,s1,i)) ;
A9: IC s2 = IC (Initialize s2) by A3, FUNCT_4:103, FUNCT_4:104
.= IC (Start-At (0,SCM+FSA)) by X, FUNCT_4:14
.= 0 by COMPOS_1:64 ;
IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),0) = CurInstr (P1,(Comput (P1,s1,i))) by COMPOS_1:91;
hence ( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) by A1, A2, A6, A8, A9, Th42, A4, A5, A7; :: thesis: verum