let s1, s2 be State of SCM+FSA; :: thesis: for J being parahalting Program of SCM+FSA st J +* (Start-At (0,SCM+FSA)) c= s1 holds
for n being Element of NAT st ProgramPart (Relocated (J,n)) c= s2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),n) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) )
let J be parahalting Program of SCM+FSA; :: thesis: ( J +* (Start-At (0,SCM+FSA)) c= s1 implies for n being Element of NAT st ProgramPart (Relocated (J,n)) c= s2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),n) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) ) )
assume A1: J +* (Start-At (0,SCM+FSA)) c= s1 ; :: thesis: for n being Element of NAT st ProgramPart (Relocated (J,n)) c= s2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),n) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) )
set JAt = J +* (Start-At (0,SCM+FSA));
A2: 0 in dom J by AFINSQ_1:69;
dom J misses dom (Start-At (0,SCM+FSA)) by COMPOS_1:140;
then A3: J c= J +* (Start-At (0,SCM+FSA)) by FUNCT_4:33;
then A4: dom J c= dom (J +* (Start-At (0,SCM+FSA))) by GRFUNC_1:8;
A5: IC SCM+FSA in dom (J +* (Start-At (0,SCM+FSA))) by COMPOS_1:141;
then A6: s1 . (IC s1) = s1 . (IC (J +* (Start-At (0,SCM+FSA)))) by A1, GRFUNC_1:8
.= s1 . 0 by COMPOS_1:142
.= (J +* (Start-At (0,SCM+FSA))) . 0 by A1, A4, A2, GRFUNC_1:8
.= J . 0 by A3, A2, GRFUNC_1:8 ;
A7: IC (Comput ((ProgramPart s1),s1,0)) = IC s1 by EXTPRO_1:3
.= IC (J +* (Start-At (0,SCM+FSA))) by A1, A5, GRFUNC_1:8
.= 0 by COMPOS_1:142 ;
ProgramPart J = J by RELAT_1:209;
then A8: 0 in dom (ProgramPart J) by AFINSQ_1:69;
let n be Element of NAT ; :: thesis: ( ProgramPart (Relocated (J,n)) c= s2 & IC s2 = n & DataPart s1 = DataPart s2 implies for i being Element of NAT holds
( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),n) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) ) )
assume that
A9: ProgramPart (Relocated (J,n)) c= s2 and
A10: IC s2 = n and
A11: DataPart s1 = DataPart s2 ; :: thesis: for i being Element of NAT holds
( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),n) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) )
A12: DataPart (Comput ((ProgramPart s1),s1,0)) = DataPart s2 by A11, EXTPRO_1:3
.= DataPart (Comput ((ProgramPart s2),s2,0)) by EXTPRO_1:3 ;
defpred S₁[ Nat] means ( (IC (Comput ((ProgramPart s1),s1,$1))) + n = IC (Comput ((ProgramPart s2),s2,$1)) & IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,$1))),(Comput ((ProgramPart s1),s1,$1)))),n) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,$1))),(Comput ((ProgramPart s2),s2,$1))) & DataPart (Comput ((ProgramPart s1),s1,$1)) = DataPart (Comput ((ProgramPart s2),s2,$1)) );
A13: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

dom J misses dom (Start-At (0,SCM+FSA)) by COMPOS_1:140;
then A14: J c= J +* (Start-At (0,SCM+FSA)) by FUNCT_4:33;
then A15: dom J c= dom (J +* (Start-At (0,SCM+FSA))) by GRFUNC_1:8;
let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
T: ProgramPart s1 = ProgramPart (Comput ((ProgramPart s1),s1,k)) by AMI_1:123;
A16: Comput ((ProgramPart s1),s1,(k + 1)) = Following ((ProgramPart s1),(Comput ((ProgramPart s1),s1,k))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,k))),(Comput ((ProgramPart s1),s1,k)))),(Comput ((ProgramPart s1),s1,k))) by T ;
reconsider l = IC (Comput ((ProgramPart s1),s1,(k + 1))) as Element of NAT ;
reconsider j = CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(k + 1)))),(Comput ((ProgramPart s1),s1,(k + 1)))) as Instruction of SCM+FSA ;
T: ProgramPart s2 = ProgramPart (Comput ((ProgramPart s2),s2,k)) by AMI_1:123;
A17: Comput ((ProgramPart s2),s2,(k + 1)) = Following ((ProgramPart s2),(Comput ((ProgramPart s2),s2,k))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,k))),(Comput ((ProgramPart s2),s2,k)))),(Comput ((ProgramPart s2),s2,k))) by T ;
A18: IC (Comput ((ProgramPart s1),s1,(k + 1))) in dom J by A1, Def2;
assume A19: S₁[k] ; :: thesis: S₁[k + 1]
hence A20: (IC (Comput ((ProgramPart s1),s1,(k + 1)))) + n = IC (Comput ((ProgramPart s2),s2,(k + 1))) by A16, A17, SCMFSA6A:41; :: thesis: ( IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(k + 1)))),(Comput ((ProgramPart s1),s1,(k + 1))))),n) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,(k + 1)))),(Comput ((ProgramPart s2),s2,(k + 1)))) & DataPart (Comput ((ProgramPart s1),s1,(k + 1))) = DataPart (Comput ((ProgramPart s2),s2,(k + 1))) )
then ( IC (Comput ((ProgramPart s2),s2,(k + 1))) in NAT & IC (Comput ((ProgramPart s2),s2,(k + 1))) in dom (Relocated (J,n)) ) by A18, COMPOS_1:118;
then IC (Comput ((ProgramPart s2),s2,(k + 1))) in (dom (Relocated (J,n))) /\ NAT by XBOOLE_0:def 4;
then A21: IC (Comput ((ProgramPart s2),s2,(k + 1))) in dom (ProgramPart (Relocated (J,n))) by RELAT_1:90;
dom (ProgramPart J) = (dom J) /\ NAT by RELAT_1:90;
then A22: l in dom (ProgramPart J) by A18, XBOOLE_0:def 4;
Y: (ProgramPart (Comput ((ProgramPart s1),s1,(k + 1)))) /. (IC (Comput ((ProgramPart s1),s1,(k + 1)))) = (Comput ((ProgramPart s1),s1,(k + 1))) . (IC (Comput ((ProgramPart s1),s1,(k + 1)))) by COMPOS_1:38;
Z: (ProgramPart (Comput ((ProgramPart s2),s2,(k + 1)))) /. (IC (Comput ((ProgramPart s2),s2,(k + 1)))) = (Comput ((ProgramPart s2),s2,(k + 1))) . (IC (Comput ((ProgramPart s2),s2,(k + 1)))) by COMPOS_1:38;
j = s1 . (IC (Comput ((ProgramPart s1),s1,(k + 1)))) by Y, AMI_1:54
.= (J +* (Start-At (0,SCM+FSA))) . (IC (Comput ((ProgramPart s1),s1,(k + 1)))) by A1, A15, A18, GRFUNC_1:8
.= J . l by A14, A18, GRFUNC_1:8 ;
hence IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(k + 1)))),(Comput ((ProgramPart s1),s1,(k + 1))))),n) = (Relocated (J,n)) . (l + n) by A22, COMPOS_1:122
.= (ProgramPart (Relocated (J,n))) . (IC (Comput ((ProgramPart s2),s2,(k + 1)))) by A20, FUNCT_1:72
.= s2 . (IC (Comput ((ProgramPart s2),s2,(k + 1)))) by A9, A21, GRFUNC_1:8
.= CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,(k + 1)))),(Comput ((ProgramPart s2),s2,(k + 1)))) by Z, AMI_1:54 ;
:: thesis: DataPart (Comput ((ProgramPart s1),s1,(k + 1))) = DataPart (Comput ((ProgramPart s2),s2,(k + 1)))
thus DataPart (Comput ((ProgramPart s1),s1,(k + 1))) = DataPart (Comput ((ProgramPart s2),s2,(k + 1))) by A19, A16, A17, SCMFSA6A:41; :: thesis: verum

end;

let i be Element of NAT ; :: thesis: ( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),n) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) )
0 in dom J by AFINSQ_1:69;
then 0 + n in dom (Relocated (J,n)) by COMPOS_1:118;
then A23: 0 + n in dom (ProgramPart (Relocated (J,n))) by COMPOS_1:16;
u: Comput ((ProgramPart s1),s1,0) = s1 by EXTPRO_1:3;
v: Comput ((ProgramPart s2),s2,0) = s2 by EXTPRO_1:3;
Z: (ProgramPart s1) /. (IC s1) = s1 . (IC s1) by COMPOS_1:38;
V: (ProgramPart s2) /. (IC s2) = s2 . (IC s2) by COMPOS_1:38;
IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,0))),(Comput ((ProgramPart s1),s1,0)))),n) = IncAddr ((CurInstr ((ProgramPart s1),s1)),n) by u
.= (Relocated (J,n)) . (0 + n) by A6, A8, Z, COMPOS_1:122
.= (ProgramPart (Relocated (J,n))) . n by FUNCT_1:72
.= CurInstr ((ProgramPart s2),s2) by A9, A10, A23, V, GRFUNC_1:8
.= CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,0))),(Comput ((ProgramPart s2),s2,0))) by v ;
then A24: S₁[ 0 ] by A10, A7, A12, EXTPRO_1:3;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A24, A13);
hence ( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),n) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) ) ; :: thesis: verum