let s1, s2 be State of SCM+FSA; :: thesis: for p1, p2 being Instruction-Sequence of SCM+FSA
for J being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s1 & J c= p1 holds
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)) )
let p1, p2 be Instruction-Sequence of SCM+FSA; :: thesis: for J being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s1 & J c= p1 holds
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)) )
let J be really-closed InitHalting Program of SCM+FSA; :: thesis: ( Initialize ((intloc 0) .--> 1) c= s1 & 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)) ) )
assume that
A1: Initialize ((intloc 0) .--> 1) c= s1 and
A2: 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)) )
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)) ) )
assume that
A3: Reloc (J,n) c= p2 and
A4: IC s2 = n and
A5: 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)) )
A6: DataPart (Comput (p1,s1,0)) = DataPart s2 by A5
.= DataPart (Comput (p2,s2,0)) ;
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)) );
A7: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
A8: Comput (p1,s1,(k + 1)) = Following (p1,(Comput (p1,s1,k))) by EXTPRO_1:3
.= Exec ((CurInstr (p1,(Comput (p1,s1,k)))),(Comput (p1,s1,k))) ;
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 ;
A9: Comput (p2,s2,(k + 1)) = Following (p2,(Comput (p2,s2,k))) by EXTPRO_1:3
.= Exec ((CurInstr (p2,(Comput (p2,s2,k)))),(Comput (p2,s2,k))) ;
IC s1 = 0 by A1, MEMSTR_0:47;
then IC s1 in dom J by AFINSQ_1:65;
then A10: IC (Comput (p1,s1,(k + 1))) in dom J by A2, AMISTD_1:21;
assume A11: S₁[k] ; :: thesis: S₁[k + 1]
hence (IC (Comput (p1,s1,(k + 1)))) + n = IC (Comput (p2,s2,(k + 1))) by A8, A9, 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 A12: IC (Comput (p2,s2,(k + 1))) in dom (Reloc (J,n)) by A10, COMPOS_1:46;
A13: l in dom J by A10;
j = p1 . (IC (Comput (p1,s1,(k + 1)))) by PBOOLE:143
.= J . l by A10, A2, GRFUNC_1:2 ;
hence IncAddr ((CurInstr (p1,(Comput (p1,s1,(k + 1))))),n) = (Reloc (J,n)) . (l + n) by A13, COMPOS_1:35
.= (Reloc (J,n)) . (IC (Comput (p2,s2,(k + 1)))) by A11, A8, A9, SCMFSA6A:8
.= p2 . (IC (Comput (p2,s2,(k + 1)))) by A12, A3, 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 A11, A8, A9, SCMFSA6A:8; :: thesis: verum

end;

A14: 0 in dom J by AFINSQ_1:65;
A15: 0 in dom J by AFINSQ_1:65;
A16: IC in dom (Initialize ((intloc 0) .--> 1)) by MEMSTR_0:48;
then A17: p1 . (IC s1) = p1 . (IC (Initialize ((intloc 0) .--> 1))) by A1, GRFUNC_1:2
.= J . 0 by A15, A2, Lm1, GRFUNC_1:2 ;
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)) )
0 in dom J by AFINSQ_1:65;
then A18: 0 + n in dom (Reloc (J,n)) by COMPOS_1:46;
A19: IC (Comput (p1,s1,0)) = s1 . (IC )
.= 0 by Lm1, A1, A16, GRFUNC_1:2 ;
A20: p2 /. (IC s2) = p2 . (IC s2) by PBOOLE:143;
A21: p1 /. (IC s1) = p1 . (IC s1) by PBOOLE:143;
IncAddr ((CurInstr (p1,(Comput (p1,s1,0)))),n) = IncAddr ((CurInstr (p1,s1)),n)
.= (Reloc (J,n)) . (0 + n) by A17, A14, A21, COMPOS_1:35
.= CurInstr (p2,s2) by A4, A18, A20, A3, GRFUNC_1:2
.= CurInstr (p2,(Comput (p2,s2,0))) ;
then A22: S₁[ 0 ] by A4, A19, A6;
for k being Nat holds S₁[k] from NAT_1:sch 2(A22, A7);
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