let P1, P2 be Instruction-Sequence of SCM+FSA; :: thesis: for s1 being 0 -started State of SCM+FSA
for s2 being State of SCM+FSA
for I being really-closed Program of SCM+FSA st I c= P1 holds
for n being Nat st Reloc (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Nat holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
let s1 be 0 -started State of SCM+FSA; :: thesis: for s2 being State of SCM+FSA
for I being really-closed Program of SCM+FSA st I c= P1 holds
for n being Nat st Reloc (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Nat holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
let s2 be State of SCM+FSA; :: thesis: for I being really-closed Program of SCM+FSA st I c= P1 holds
for n being Nat st Reloc (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Nat holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
let J be really-closed Program of SCM+FSA; :: thesis: ( J c= P1 implies for n being Nat st Reloc (J,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Nat holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) )
set JAt = Start-At (0,SCM+FSA);
A1: 0 in dom J by AFINSQ_1:65;
A2: Start-At (0,SCM+FSA) c= s1 by MEMSTR_0:29;
assume A3: J c= P1 ; :: thesis: for n being Nat st Reloc (J,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Nat holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
Start-At (0,SCM+FSA) c= s1 by A2;
then A4: Initialize s1 = s1 by FUNCT_4:98;
A5: IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
A6: P1 . (IC s1) = P1 . 0 by A4, MEMSTR_0:16
.= J . 0 by A1, A3, GRFUNC_1:2 ;
A7: IC (Comput (P1,s1,0)) = IC s1
.= IC (Start-At (0,SCM+FSA)) by A2, A5, GRFUNC_1:2
.= 0 by FUNCOP_1:72 ;
A8: 0 in dom J by AFINSQ_1:65;
let n be Nat; :: thesis: ( Reloc (J,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 implies for i being Nat holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) )
defpred S1[ Nat] means ( (IC (Comput (P1,s1,$1))) + n = IC (Comput (P2,s2,$1)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,$1)))),n) = CurInstr (P2,(Comput (P2,s2,$1))) & DataPart (Comput (P1,s1,$1)) = DataPart (Comput (P2,s2,$1)) );
assume that
A9: Reloc (J,n) c= P2 and
A10: IC s2 = n and
A11: DataPart s1 = DataPart s2 ; :: thesis: for i being Nat holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
let i be Nat; :: thesis: ( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
A12: DataPart (Comput (P1,s1,0)) = DataPart s2 by A11
.= DataPart (Comput (P2,s2,0)) ;
A13: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
A14: Comput (P1,s1,(k + 1)) = Following (P1,(Comput (P1,s1,k))) by EXTPRO_1:3;
reconsider l = IC (Comput (P1,s1,(k + 1))) as Element of NAT ;
reconsider j = CurInstr (P1,(Comput (P1,s1,(k + 1)))) as Instruction of SCM+FSA ;
A15: Comput (P2,s2,(k + 1)) = Following (P2,(Comput (P2,s2,k))) by EXTPRO_1:3;
IC s1 = 0 by MEMSTR_0:def 11;
then IC s1 in dom J by AFINSQ_1:65;
then A16: IC (Comput (P1,s1,(k + 1))) in dom J by AMISTD_1:21, A3;
assume A17: S1[k] ; :: thesis: S1[k + 1]
hence A18: (IC (Comput (P1,s1,(k + 1)))) + n = IC (Comput (P2,s2,(k + 1))) by A14, A15, SCMFSA6A:8; :: thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(k + 1))))),n) = CurInstr (P2,(Comput (P2,s2,(k + 1)))) & DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1))) )
then A19: IC (Comput (P2,s2,(k + 1))) in dom (Reloc (J,n)) by A16, COMPOS_1:46;
A20: l in dom J by A16;
j = P1 . (IC (Comput (P1,s1,(k + 1)))) by PBOOLE:143
.= J . l by A16, A3, GRFUNC_1:2 ;
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(k + 1))))),n) = (Reloc (J,n)) . (l + n) by A20, COMPOS_1:35
.= P2 . (IC (Comput (P2,s2,(k + 1)))) by A9, A18, A19, GRFUNC_1:2
.= CurInstr (P2,(Comput (P2,s2,(k + 1)))) by PBOOLE:143 ;
:: thesis: DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1)))
thus DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1))) by A17, A14, A15, SCMFSA6A:8; :: thesis: verum
end;
0 in dom J by AFINSQ_1:65;
then A21: 0 + n in dom (Reloc (J,n)) by COMPOS_1:46;
A22: P1 /. (IC s1) = P1 . (IC s1) by PBOOLE:143;
A23: P2 /. (IC s2) = P2 . (IC s2) by PBOOLE:143;
IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),n) = (Reloc (J,n)) . (0 + n) by A8, A22, A6, COMPOS_1:35
.= CurInstr (P2,(Comput (P2,s2,0))) by A9, A10, A21, A23, GRFUNC_1:2 ;
then A24: S1[ 0 ] by A10, A7, A12;
for k being Nat holds S1[k] from NAT_1:sch 2(A24, A13);
 hence ( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) ; :: thesis: verum