let P1, P2 be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st Start-At (0,SCM+FSA) c= s1 & I is_closed_on s1,P1 & I c= P1 holds
for n being Element of NAT st IC s2 = n & DataPart s1 = DataPart s2 & Reloc (I,n) c= P2 holds
for i being Element of 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 s1, s2 be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA st Start-At (0,SCM+FSA) c= s1 & I is_closed_on s1,P1 & I c= P1 holds
for n being Element of NAT st IC s2 = n & DataPart s1 = DataPart s2 & Reloc (I,n) c= P2 holds
for i being Element of 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 I be Program of SCM+FSA; :: thesis: ( Start-At (0,SCM+FSA) c= s1 & I is_closed_on s1,P1 & I c= P1 implies for n being Element of NAT st IC s2 = n & DataPart s1 = DataPart s2 & Reloc (I,n) c= P2 holds
for i being Element of 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 A1: Start-At (0,SCM+FSA) c= s1 ; :: thesis: ( not I is_closed_on s1,P1 or not I c= P1 or for n being Element of NAT st IC s2 = n & DataPart s1 = DataPart s2 & Reloc (I,n) c= P2 holds
for i being Element of 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 A2: I is_closed_on s1,P1 ; :: thesis: ( not I c= P1 or for n being Element of NAT st IC s2 = n & DataPart s1 = DataPart s2 & Reloc (I,n) c= P2 holds
for i being Element of 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 A4: I c= P1 ; :: thesis: for n being Element of NAT st IC s2 = n & DataPart s1 = DataPart s2 & Reloc (I,n) c= P2 holds
for i being Element of 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 Element of NAT ; :: thesis: ( IC s2 = n & DataPart s1 = DataPart s2 & Reloc (I,n) c= P2 implies for i being Element of 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)) ) )
B5: IC in dom (Start-At (0,SCM+FSA)) by COMPOS_1:52;
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)) );
A6: IC (Comput (P1,s1,0)) = IC s1 by EXTPRO_1:3
.= IC (Start-At (0,SCM+FSA)) by A1, B5, GRFUNC_1:8
.= 0 by COMPOS_1:64 ;
assume A7: IC s2 = n ; :: thesis: ( not DataPart s1 = DataPart s2 or not Reloc (I,n) c= P2 or for i being Element of 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)) ) )
A8: 0 in dom I by A2, Th3;
then A9: 0 + n in dom (Reloc (I,n)) by COMPOS_1:158;
IC in dom (Start-At (0,SCM+FSA)) by COMPOS_1:52;
then A10: P1 . (IC s1) = P1 . (IC (Start-At (0,SCM+FSA))) by A1, GRFUNC_1:8
.= P1 . 0 by COMPOS_1:64
.= I . 0 by A8, A4, GRFUNC_1:8 ;
assume DataPart s1 = DataPart s2 ; :: thesis: ( not Reloc (I,n) c= P2 or for i being Element of 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)) ) )
then A11: DataPart (Comput (P1,s1,0)) = DataPart s2 by EXTPRO_1:3
.= DataPart (Comput (P2,s2,0)) by EXTPRO_1:3 ;
assume A12: Reloc (I,n) c= P2 ; :: thesis: for i being Element of 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 i be Element of 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)) )
A13: P2 /. (IC s2) = P2 . (IC s2) by PBOOLE:158;
A14: CurInstr (P1,s1) = I . 0 by A10, PBOOLE:158;
IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),n) = IncAddr ((CurInstr (P1,s1)),n) by EXTPRO_1:3
.= (Reloc (I,n)) . (0 + n) by A14, A8, COMPOS_1:122
.= CurInstr (P2,s2) by A7, A9, A13, A12, GRFUNC_1:8
.= CurInstr (P2,(Comput (P2,s2,0))) by EXTPRO_1:3 ;
then A15: S₁[ 0 ] by A7, A6, A11, EXTPRO_1:3;
A16: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
A17: Comput (P1,s1,(k + 1)) = Following (P1,(Comput (P1,s1,k))) by EXTPRO_1:4
.= 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 ;
A18: Comput (P2,s2,(k + 1)) = Following (P2,(Comput (P2,s2,k))) by EXTPRO_1:4
.= Exec ((CurInstr (P2,(Comput (P2,s2,k)))),(Comput (P2,s2,k))) ;
A19: Initialize s1 = s1 by A1, FUNCT_4:104;
A20: P1 = P1 +* I by A4, FUNCT_4:104;
then A21: IC (Comput (P1,s1,(k + 1))) in dom I by A2, A19, SCMFSA7B:def 7;
assume A22: S₁[k] ; :: thesis: S₁[k + 1]
hence A23: (IC (Comput (P1,s1,(k + 1)))) + n = IC (Comput (P2,s2,(k + 1))) by A17, A18, SCMFSA6A:41; :: 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 A24: IC (Comput (P2,s2,(k + 1))) in dom (Reloc (I,n)) by A21, COMPOS_1:158;
A25: l in dom I by A19, A2, A20, SCMFSA7B:def 7;
j = P1 . (IC (Comput (P1,s1,(k + 1)))) by PBOOLE:158
.= I . l by A21, A4, GRFUNC_1:8 ;
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(k + 1))))),n) = (Reloc (I,n)) . (l + n) by A25, COMPOS_1:122
.= P2 . (IC (Comput (P2,s2,(k + 1)))) by A24, A23, A12, GRFUNC_1:8
.= CurInstr (P2,(Comput (P2,s2,(k + 1)))) by PBOOLE:158 ;
:: 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 A22, A17, A18, SCMFSA6A:41; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A15, A16);
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