let s1, s2 be State of SCM+FSA ; :: thesis:
let J be InitHalting Program of SCM+FSA ; :: thesis:
set JAt = Initialized J;
assume A1: Initialized J c= s1 ; :: thesis:
let n be Element of NAT ; :: thesis:
assume that
A2: ProgramPart (Relocated J,n) c= s2 and
A3: IC s2 = insloc n and
A4: DataPart s1 = DataPart s2 ; :: thesis:
A5: J c= Initialized J by SCMFSA6A:26;
then A6: dom J c= dom (Initialized J) by GRFUNC_1:8;
let i be Element of NAT ; :: thesis:
defpred S₁[ Element of NAT ] means ( (IC (Computation s1,$1)) + n = IC (Computation s2,$1) & IncAddr (CurInstr (Computation s1,$1)),n = CurInstr (Computation s2,$1) & DataPart (Computation s1,$1) = DataPart (Computation s2,$1) );
A7: S₁[ 0 ]

proof

A8: IC SCM+FSA in dom (Initialized J) by SCMFSA6A:24;
insloc 0 in dom J by Th11;
then (insloc 0 ) + n in dom (Relocated J,n) by SCMFSA_5:4;
then A9: insloc (0 + n) in dom (ProgramPart (Relocated J,n)) by AMI_1:106;
IC (Computation s1,0 ) = s1 . (IC SCM+FSA ) by AMI_1:13
.= (Initialized J) . (IC SCM+FSA ) by A1, A8, GRFUNC_1:8
.= insloc 0 by SCMFSA6A:46 ;
hence (IC (Computation s1,0 )) + n = IC (Computation s2,0 ) by A3, AMI_1:13; :: thesis:
A10: insloc 0 in dom J by Th11;
A11: s1 . (IC s1) = s1 . ((Initialized J) . (IC SCM+FSA )) by A1, A8, GRFUNC_1:8
.= s1 . (insloc 0 ) by SCMFSA6A:46
.= (Initialized J) . (insloc 0 ) by A1, A6, A10, GRFUNC_1:8
.= J . (insloc 0 ) by A5, A10, GRFUNC_1:8 ;
ProgramPart J = J by AMI_1:105;
then A12: insloc 0 in dom (ProgramPart J) by Th11;
thus IncAddr (CurInstr (Computation s1,0 )),n = IncAddr (CurInstr s1),n by AMI_1:13
.= (Relocated J,n) . ((insloc 0 ) + n) by A11, A12, SCMFSA_5:7
.= (ProgramPart (Relocated J,n)) . (insloc n) by FUNCT_1:72
.= CurInstr s2 by A2, A3, A9, GRFUNC_1:8
.= CurInstr (Computation s2,0 ) by AMI_1:13 ; :: thesis:
thus DataPart (Computation s1,0 ) = DataPart s2 by A4, AMI_1:13
.= DataPart (Computation s2,0 ) by AMI_1:13 ; :: thesis:

end;

A13: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A14: S₁[k] ; :: thesis:
A15: Computation s1,(k + 1) = Following (Computation s1,k) by AMI_1:14
.= Exec (CurInstr (Computation s1,k)),(Computation s1,k) ;
A16: Computation s2,(k + 1) = Following (Computation s2,k) by AMI_1:14
.= Exec (CurInstr (Computation s2,k)),(Computation s2,k) ;
hence A17: (IC (Computation s1,(k + 1))) + n = IC (Computation s2,(k + 1)) by A14, A15, SCMFSA6A:41; :: thesis:
reconsider j = CurInstr (Computation s1,(k + 1)) as Instruction of SCM+FSA ;
reconsider l = IC (Computation s1,(k + 1)) as Element of NAT by ORDINAL1:def 13;
A19: IC (Computation s1,(k + 1)) in dom J by A1, Def1;
dom (ProgramPart J) = (dom J) /\ NAT by RELAT_1:90;
then A20: l in dom (ProgramPart J) by A19, XBOOLE_0:def 4;
A21: j = s1 . (IC (Computation s1,(k + 1))) by AMI_1:54
.= (Initialized J) . (IC (Computation s1,(k + 1))) by A1, A6, A19, GRFUNC_1:8
.= J . l by A5, A19, GRFUNC_1:8 ;
A22: IC (Computation s2,(k + 1)) in NAT by AMI_1:def 4;
IC (Computation s2,(k + 1)) in dom (Relocated J,n) by A17, A19, SCMFSA_5:4;
then IC (Computation s2,(k + 1)) in (dom (Relocated J,n)) /\ NAT by A22, XBOOLE_0:def 4;
then A23: IC (Computation s2,(k + 1)) in dom (ProgramPart (Relocated J,n)) by RELAT_1:90;
thus IncAddr (CurInstr (Computation s1,(k + 1))),n = (Relocated J,n) . (l + n) by A20, A21, SCMFSA_5:7
.= (ProgramPart (Relocated J,n)) . (IC (Computation s2,(k + 1))) by A17, FUNCT_1:72
.= s2 . (IC (Computation s2,(k + 1))) by A2, A23, GRFUNC_1:8
.= CurInstr (Computation s2,(k + 1)) by AMI_1:54 ; :: thesis:
thus DataPart (Computation s1,(k + 1)) = DataPart (Computation s2,(k + 1)) by A14, A15, A16, SCMFSA6A:41; :: thesis:

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A7, A13);
hence ( (IC (Computation s1,i)) + n = IC (Computation s2,i) & IncAddr (CurInstr (Computation s1,i)),n = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) ) ; :: thesis: