let P1, P2 be Instruction-Sequence of SCM+FSA; :: thesis:
let s1 be 0 -started State of SCM+FSA; :: thesis:
let s2 be State of SCM+FSA; :: thesis:
let J be Program of SCM+FSA; :: thesis:
set JAt = Start-At (0,SCM+FSA);
assume A1: J is_closed_on s1,P1 ; :: thesis:
then A2: 0 in dom J by Th39;
A3: Start-At (0,SCM+FSA) c= s1 by MEMSTR_0:29;
assume A4: J c= P1 ; :: thesis:
Start-At (0,SCM+FSA) c= s1 by A3;
then A5: Initialize s1 = s1 by FUNCT_4:98;
A6: IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
A7: P1 . (IC s1) = P1 . 0 by A5, MEMSTR_0:16
.= J . 0 by A2, A4, GRFUNC_1:2 ;
A8: P1 = P1 +* J by A4, FUNCT_4:98;
A9: IC (Comput (P1,s1,0)) = IC s1 by EXTPRO_1:2
.= IC (Start-At (0,SCM+FSA)) by A3, A6, GRFUNC_1:2
.= 0 by FUNCOP_1:72 ;
A10: 0 in dom J by A1, Th39;
let n be Element of NAT ; :: thesis:
defpred S₁[ 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
A11: Reloc (J,n) c= P2 and
A12: IC s2 = n and
A13: DataPart s1 = DataPart s2 ; :: thesis:
let i be Element of NAT ; :: thesis:
A14: DataPart (Comput (P1,s1,0)) = DataPart s2 by A13, EXTPRO_1:2
.= DataPart (Comput (P2,s2,0)) by EXTPRO_1:2 ;
A15: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis:
A16: 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 ;
A18: Comput (P2,s2,(k + 1)) = Following (P2,(Comput (P2,s2,k))) by EXTPRO_1:3;
B20: Initialize s1 = s1 by A3, FUNCT_4:98;
then A20: IC (Comput (P1,s1,(k + 1))) in dom J by A1, A8, SCMFSA7B:def 6;
assume A21: S₁[k] ; :: thesis:
hence A22: (IC (Comput (P1,s1,(k + 1)))) + n = IC (Comput (P2,s2,(k + 1))) by A16, A18, SCMFSA6A:8; :: thesis:
then A23: IC (Comput (P2,s2,(k + 1))) in dom (Reloc (J,n)) by A20, COMPOS_1:46;
A24: l in dom J by B20, A1, A8, SCMFSA7B:def 6;
j = P1 . (IC (Comput (P1,s1,(k + 1)))) by PBOOLE:143
.= J . l by A20, A4, GRFUNC_1:2 ;
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(k + 1))))),n) = (Reloc (J,n)) . (l + n) by A24, COMPOS_1:35
.= P2 . (IC (Comput (P2,s2,(k + 1)))) by A11, A22, A23, GRFUNC_1:2
.= CurInstr (P2,(Comput (P2,s2,(k + 1)))) by PBOOLE:143 ;
:: thesis:
thus DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1))) by A21, A16, A18, SCMFSA6A:8; :: thesis:

end;

0 in dom J by A1, Th39;
then A26: 0 + n in dom (Reloc (J,n)) by COMPOS_1:46;
A27: P1 /. (IC s1) = P1 . (IC s1) by PBOOLE:143;
A28: P2 /. (IC s2) = P2 . (IC s2) by PBOOLE:143;
A29: Comput (P1,s1,0) = s1 by EXTPRO_1:2;
A30: Comput (P2,s2,0) = s2 by EXTPRO_1:2;
IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),n) = (Reloc (J,n)) . (0 + n) by A10, A27, A29, A7, COMPOS_1:35
.= CurInstr (P2,(Comput (P2,s2,0))) by A30, A11, A12, A26, A28, GRFUNC_1:2 ;
then A31: S₁[ 0 ] by A12, A9, A14, EXTPRO_1:2;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A31, A15);
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: