let s2 be State of SCM+FSA; :: thesis: for s1 being 0 -started State of SCM+FSA
for P, Q being Instruction-Sequence of SCM+FSA
for J being really-closed parahalting Program of st J c= P holds
for n being Nat st Reloc (J,n) c= Q & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Nat holds
( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) )
let s1 be 0 -started State of SCM+FSA; :: thesis: for P, Q being Instruction-Sequence of SCM+FSA
for J being really-closed parahalting Program of st J c= P holds
for n being Nat st Reloc (J,n) c= Q & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Nat holds
( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) )
let P, Q be Instruction-Sequence of SCM+FSA; :: thesis: for J being really-closed parahalting Program of st J c= P holds
for n being Nat st Reloc (J,n) c= Q & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Nat holds
( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) )
let J be really-closed parahalting Program of ; :: thesis: ( J c= P implies for n being Nat st Reloc (J,n) c= Q & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Nat holds
( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) ) )
A1: Start-At (0,SCM+FSA) c= s1 by MEMSTR_0:29;
assume A2: J c= P ; :: thesis: for n being Nat st Reloc (J,n) c= Q & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Nat holds
( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) )
set JAt = Start-At (0,SCM+FSA);
A3: 0 in dom J by AFINSQ_1:65;
A4: IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
then A5: P . (IC s1) = P . (IC (Start-At (0,SCM+FSA))) by A1, GRFUNC_1:2
.= P . 0 by FUNCOP_1:72
.= J . 0 by A3, A2, GRFUNC_1:2 ;
A6: IC (Comput (P,s1,0)) = IC s1
.= IC (Start-At (0,SCM+FSA)) by A1, A4, GRFUNC_1:2
.= 0 by FUNCOP_1:72 ;
A7: 0 in dom J by AFINSQ_1:65;
let n be Nat; :: thesis: ( Reloc (J,n) c= Q & IC s2 = n & DataPart s1 = DataPart s2 implies for i being Nat holds
( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) ) )
assume that
A8: Reloc (J,n) c= Q and
A9: IC s2 = n and
A10: DataPart s1 = DataPart s2 ; :: thesis: for i being Nat holds
( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) )
A11: DataPart (Comput (P,s1,0)) = DataPart s2 by A10
.= DataPart (Comput (Q,s2,0)) ;
defpred S₁[ Nat] means ( (IC (Comput (P,s1,$1))) + n = IC (Comput (Q,s2,$1)) & IncAddr ((CurInstr (P,(Comput (P,s1,$1)))),n) = CurInstr (Q,(Comput (Q,s2,$1))) & DataPart (Comput (P,s1,$1)) = DataPart (Comput (Q,s2,$1)) );
A12: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
A13: Comput (P,s1,(k + 1)) = Following (P,(Comput (P,s1,k))) by EXTPRO_1:3
.= Exec ((CurInstr (P,(Comput (P,s1,k)))),(Comput (P,s1,k))) ;
reconsider l = IC (Comput (P,s1,(k + 1))) as Element of NAT ;
reconsider j = CurInstr (P,(Comput (P,s1,(k + 1)))) as Instruction of SCM+FSA ;
A14: Comput (Q,s2,(k + 1)) = Following (Q,(Comput (Q,s2,k))) by EXTPRO_1:3
.= Exec ((CurInstr (Q,(Comput (Q,s2,k)))),(Comput (Q,s2,k))) ;
IC s1 = 0 by MEMSTR_0:def 11;
then IC s1 in dom J by AFINSQ_1:65;
then A15: IC (Comput (P,s1,(k + 1))) in dom J by A2, AMISTD_1:21;
assume A16: S₁[k] ; :: thesis: S₁[k + 1]
hence (IC (Comput (P,s1,(k + 1)))) + n = IC (Comput (Q,s2,(k + 1))) by A13, A14, SCMFSA6A:8; :: thesis: ( IncAddr ((CurInstr (P,(Comput (P,s1,(k + 1))))),n) = CurInstr (Q,(Comput (Q,s2,(k + 1)))) & DataPart (Comput (P,s1,(k + 1))) = DataPart (Comput (Q,s2,(k + 1))) )
then A17: IC (Comput (Q,s2,(k + 1))) in dom (Reloc (J,n)) by A15, COMPOS_1:46;
A18: l in dom J by A15;
A19: dom P = NAT by PARTFUN1:def 2;
A20: dom Q = NAT by PARTFUN1:def 2;
j = P . (IC (Comput (P,s1,(k + 1)))) by A19, PARTFUN1:def 6
.= J . l by A15, A2, GRFUNC_1:2 ;
hence IncAddr ((CurInstr (P,(Comput (P,s1,(k + 1))))),n) = (Reloc (J,n)) . (l + n) by A18, COMPOS_1:35
.= (Reloc (J,n)) . (IC (Comput (Q,s2,(k + 1)))) by A16, A13, A14, SCMFSA6A:8
.= Q . (IC (Comput (Q,s2,(k + 1)))) by A17, A8, GRFUNC_1:2
.= CurInstr (Q,(Comput (Q,s2,(k + 1)))) by A20, PARTFUN1:def 6 ;
:: thesis: DataPart (Comput (P,s1,(k + 1))) = DataPart (Comput (Q,s2,(k + 1)))
thus DataPart (Comput (P,s1,(k + 1))) = DataPart (Comput (Q,s2,(k + 1))) by A16, A13, A14, SCMFSA6A:8; :: thesis: verum

end;

let i be Nat; :: thesis: ( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) )
0 in dom J by AFINSQ_1:65;
then A21: 0 + n in dom (Reloc (J,n)) by COMPOS_1:46;
A22: dom Q = NAT by PARTFUN1:def 2;
dom P = NAT by PARTFUN1:def 2;
then IncAddr ((CurInstr (P,(Comput (P,s1,0)))),n) = (Reloc (J,n)) . (0 + n) by A5, A7, COMPOS_1:35, PARTFUN1:def 6
.= Q . (IC (Comput (Q,s2,0))) by A9, A21, A8, GRFUNC_1:2
.= CurInstr (Q,(Comput (Q,s2,0))) by A22, PARTFUN1:def 6 ;
then A23: S₁[ 0 ] by A9, A6, A11;
for k being Nat holds S₁[k] from NAT_1:sch 2(A23, A12);
hence ( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) ) ; :: thesis: verum