let s1, s2 be State of SCM+FSA ; :: thesis:
let I be Program of SCM+FSA ; :: thesis:
assume A1: I +* (Start-At (insloc 0 )) c= s1 ; :: thesis:
assume A2: I is_pseudo-closed_on s1 ; :: thesis:
let n be Element of NAT ; :: thesis:
assume A3: ProgramPart (Relocated I,n) c= s2 ; :: thesis:
assume A4: IC s2 = insloc n ; :: thesis:
assume A5: DataPart s1 = DataPart s2 ; :: thesis:

hereby :: thesis:

let i be Element of NAT ; :: thesis:
assume A7: i < pseudo-LifeSpan s1,I ; :: thesis:
defpred S₁[ Element of NAT ] means ( $1 < pseudo-LifeSpan s1,I implies ( (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) ) );
A8: S₁[ 0 ]

proof

assume A9: 0 < pseudo-LifeSpan s1,I ; :: thesis:
A10: IC SCM+FSA in dom (I +* (Start-At (insloc 0 ))) by SF_MASTR:65;
IC (Computation s1,0 ) = s1 . (IC SCM+FSA ) by AMI_1:13
.= (I +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by A1, A10, GRFUNC_1:8
.= insloc 0 by SF_MASTR:66 ;
hence (IC (Computation s1,0 )) + n = IC (Computation s2,0 ) by A4, AMI_1:13; :: thesis:
A11: I c= I +* (Start-At (insloc 0 )) by SCMFSA8A:9;
then A12: dom I c= dom (I +* (Start-At (insloc 0 ))) by GRFUNC_1:8;
IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 ) = IC (s1 +* (I +* (Start-At (insloc 0 )))) by AMI_1:13
.= IC ((s1 +* I) +* (Start-At (insloc 0 ))) by FUNCT_4:15
.= insloc 0 by AMI_1:111 ;
then A13: insloc 0 in dom I by A2, A9, SCMFSA8A:def 5;
IC SCM+FSA in dom (I +* (Start-At (insloc 0 ))) by SF_MASTR:65;
then A14: s1 . (IC s1) = s1 . ((I +* (Start-At (insloc 0 ))) . (IC SCM+FSA )) by A1, GRFUNC_1:8
.= s1 . (insloc 0 ) by SF_MASTR:66
.= (I +* (Start-At (insloc 0 ))) . (insloc 0 ) by A1, A12, A13, GRFUNC_1:8
.= I . (insloc 0 ) by A11, A13, GRFUNC_1:8 ;
(insloc 0 ) + n in dom (Relocated I,n) by A13, SCMFSA_5:4;
then A15: insloc (0 + n) in dom (ProgramPart (Relocated I,n)) by AMI_1:106;
A16: insloc 0 in dom (ProgramPart I) by A13, AMI_1:105;
thus IncAddr (CurInstr (Computation s1,0 )),n = IncAddr (CurInstr s1),n by AMI_1:13
.= (Relocated I,n) . (insloc (0 + n)) by A14, A16, SCMFSA_5:7
.= (ProgramPart (Relocated I,n)) . (insloc n) by FUNCT_1:72
.= CurInstr s2 by A3, A4, A15, GRFUNC_1:8
.= CurInstr (Computation s2,0 ) by AMI_1:13 ; :: thesis:
thus DataPart (Computation s1,0 ) = DataPart s2 by A5, AMI_1:13
.= DataPart (Computation s2,0 ) by AMI_1:13 ; :: thesis:

end;

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

proof

let k be Element of NAT ; :: thesis:
assume A18: S₁[k] ; :: thesis:
assume A19: k + 1 < pseudo-LifeSpan s1,I ; :: thesis:
A20: k + 0 < k + 1 by XREAL_1:8;
A21: Computation s1,(k + 1) = Following (Computation s1,k) by AMI_1:14
.= Exec (CurInstr (Computation s1,k)),(Computation s1,k) ;
A22: Computation s2,(k + 1) = Following (Computation s2,k) by AMI_1:14
.= Exec (CurInstr (Computation s2,k)),(Computation s2,k) ;
hence A23: (IC (Computation s1,(k + 1))) + n = IC (Computation s2,(k + 1)) by A18, A19, A20, A21, SCMFSA6A:41, XXREAL_0:2; :: 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;
A25: I c= I +* (Start-At (insloc 0 )) by SCMFSA8A:9;
then A26: dom I c= dom (I +* (Start-At (insloc 0 ))) by GRFUNC_1:8;
s1 +* (I +* (Start-At (insloc 0 ))) = s1 by A1, FUNCT_4:79;
then A27: IC (Computation s1,(k + 1)) in dom I by A2, A19, SCMFSA8A:def 5;
dom (ProgramPart I) = (dom I) /\ NAT by RELAT_1:90;
then A28: l in dom (ProgramPart I) by A27, XBOOLE_0:def 4;
A29: IC (Computation s2,(k + 1)) in NAT by AMI_1:def 4;
A30: j = s1 . (IC (Computation s1,(k + 1))) by AMI_1:54
.= (I +* (Start-At (insloc 0 ))) . (IC (Computation s1,(k + 1))) by A1, A26, A27, GRFUNC_1:8
.= I . l by A25, A27, GRFUNC_1:8 ;
IC (Computation s2,(k + 1)) in dom (Relocated I,n) by A23, A27, SCMFSA_5:4;
then IC (Computation s2,(k + 1)) in (dom (Relocated I,n)) /\ NAT by A29, XBOOLE_0:def 4;
then A31: IC (Computation s2,(k + 1)) in dom (ProgramPart (Relocated I,n)) by RELAT_1:90;
thus IncAddr (CurInstr (Computation s1,(k + 1))),n = (Relocated I,n) . (l + n) by A28, A30, SCMFSA_5:7
.= (ProgramPart (Relocated I,n)) . (IC (Computation s2,(k + 1))) by A23, FUNCT_1:72
.= s2 . (IC (Computation s2,(k + 1))) by A3, A31, 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 A18, A19, A20, A21, A22, SCMFSA6A:41, XXREAL_0:2; :: thesis:

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A8, A17);
hence IncAddr (CurInstr (Computation s1,i)),n = CurInstr (Computation s2,i) by A7; :: thesis:

end;

let i be Element of NAT ; :: thesis:
assume A32: i <= pseudo-LifeSpan s1,I ; :: thesis:
defpred S₁[ Element of NAT ] means ( $1 <= pseudo-LifeSpan s1,I implies ( (IC (Computation s1,$1)) + n = IC (Computation s2,$1) & DataPart (Computation s1,$1) = DataPart (Computation s2,$1) ) );
A33: S₁[ 0 ]

proof

assume 0 <= pseudo-LifeSpan s1,I ; :: thesis:
A34: IC SCM+FSA in dom (I +* (Start-At (insloc 0 ))) by SF_MASTR:65;
IC (Computation s1,0 ) = s1 . (IC SCM+FSA ) by AMI_1:13
.= (I +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by A1, A34, GRFUNC_1:8
.= insloc 0 by SF_MASTR:66 ;
hence (IC (Computation s1,0 )) + n = IC (Computation s2,0 ) by A4, AMI_1:13; :: thesis:
thus DataPart (Computation s1,0 ) = DataPart s2 by A5, AMI_1:13
.= DataPart (Computation s2,0 ) by AMI_1:13 ; :: thesis:

end;

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

proof

let k be Element of NAT ; :: thesis:
assume A36: S₁[k] ; :: thesis:
assume A37: k + 1 <= pseudo-LifeSpan s1,I ; :: thesis:
then A38: k + 1 <= (pseudo-LifeSpan s1,I) + 1 by NAT_1:12;
A39: k < pseudo-LifeSpan s1,I by A37, NAT_1:13;
set i = CurInstr (Computation s1,k);
A40: Computation s1,(k + 1) = Following (Computation s1,k) by AMI_1:14
.= Exec (CurInstr (Computation s1,k)),(Computation s1,k) ;
A41: Computation s2,(k + 1) = Following (Computation s2,k) by AMI_1:14
.= Exec (CurInstr (Computation s2,k)),(Computation s2,k) ;
thus (IC (Computation s1,(k + 1))) + n = IC (Exec (IncAddr (CurInstr (Computation s1,k)),n),(Computation s2,k)) by A36, A38, A40, SCMFSA6A:41, XREAL_1:8
.= IC (Computation s2,(k + 1)) by A6, A39, A41 ; :: thesis:
thus DataPart (Computation s1,(k + 1)) = DataPart (Exec (IncAddr (CurInstr (Computation s1,k)),n),(Computation s2,k)) by A36, A38, A40, SCMFSA6A:41, XREAL_1:8
.= DataPart (Computation s2,(k + 1)) by A6, A39, A41 ; :: thesis:

end;

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