let N be non empty with_non-empty_elements set ; :: thesis: for k being Element of NAT
for p being autonomic FinPartState of (STC N)
for s1, s2 being State of (STC N) st IC in dom p & NPP p c= s1 & NPP (Relocated (p,k)) c= s2 holds
for P1, P2 being the Instructions of (STC N) -valued ManySortedSet of NAT st ProgramPart p c= P1 & Reloc ((ProgramPart p),k) c= P2 holds
for i being Element of NAT holds
( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) )
let k be Element of NAT ; :: thesis: for p being autonomic FinPartState of (STC N)
for s1, s2 being State of (STC N) st IC in dom p & NPP p c= s1 & NPP (Relocated (p,k)) c= s2 holds
for P1, P2 being the Instructions of (STC N) -valued ManySortedSet of NAT st ProgramPart p c= P1 & Reloc ((ProgramPart p),k) c= P2 holds
for i being Element of NAT holds
( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) )
let p be autonomic FinPartState of (STC N); :: thesis: for s1, s2 being State of (STC N) st IC in dom p & NPP p c= s1 & NPP (Relocated (p,k)) c= s2 holds
for P1, P2 being the Instructions of (STC N) -valued ManySortedSet of NAT st ProgramPart p c= P1 & Reloc ((ProgramPart p),k) c= P2 holds
for i being Element of NAT holds
( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) )
let s1, s2 be State of (STC N); :: thesis: ( IC in dom p & NPP p c= s1 & NPP (Relocated (p,k)) c= s2 implies for P1, P2 being the Instructions of (STC N) -valued ManySortedSet of NAT st ProgramPart p c= P1 & Reloc ((ProgramPart p),k) c= P2 holds
for i being Element of NAT holds
( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) ) )
assume that
A1: IC in dom p and
A2: NPP p c= s1 and
A3: NPP (Relocated (p,k)) c= s2 ; :: thesis: for P1, P2 being the Instructions of (STC N) -valued ManySortedSet of NAT st ProgramPart p c= P1 & Reloc ((ProgramPart p),k) c= P2 holds
for i being Element of NAT holds
( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) )
B1: IC in dom (NPP p) by A1, COMPOS_1:179;
let P1, P2 be the Instructions of (STC N) -valued ManySortedSet of NAT ; :: thesis: ( ProgramPart p c= P1 & Reloc ((ProgramPart p),k) c= P2 implies for i being Element of NAT holds
( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) ) )
assume A4: ( ProgramPart p c= P1 & Reloc ((ProgramPart p),k) c= P2 ) ; :: thesis: for i being Element of NAT holds
( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) )
set s3 = s1 +* (DataPart s2);
defpred S₁[ Element of NAT ] means ( (IC (Comput (P1,s1,$1))) + k = IC (Comput (P2,s2,$1)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,$1)))),k) = CurInstr (P2,(Comput (P2,s2,$1))) & (Comput (P1,s1,$1)) | (dom (DataPart p)) = (Comput (P2,s2,$1)) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput (P1,(s1 +* (DataPart s2)),$1)) = DataPart (Comput (P2,s2,$1)) );
A7: not p is NAT -defined by A1, COMPOS_1:19;
A8: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

proof

set DPp = DataPart p;
let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume that
A9: (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) and
A10: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) and
(Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart (Relocated (p,k)))) and
DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) ; :: thesis: S₁[i + 1]
set Cs2i1 = Comput (P2,s2,(i + 1));
set Cs3i = Comput (P1,(s1 +* (DataPart s2)),i);
set Cs2i = Comput (P2,s2,i);
set Cs3i1 = Comput (P1,(s1 +* (DataPart s2)),(i + 1));
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs1i = Comput (P1,s1,i);

A11: now

reconsider loc = IC (Comput (P1,s1,(i + 1))) as Element of NAT ;
assume A12: (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) ; :: thesis: IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1))))
reconsider kk = loc as Element of NAT ;
A13: loc in dom (ProgramPart p) by A7, Def4, A4, A2;
A14: loc + k in dom (Reloc ((ProgramPart p),k)) by A13, COMPOS_1:158;
A15: dom P2 = NAT by PARTFUN1:def 4;
dom P1 = NAT by PARTFUN1:def 4;
then CurInstr (P1,(Comput (P1,s1,(i + 1)))) = P1 . loc by PARTFUN1:def 8
.= (ProgramPart p) . loc by A13, A4, GRFUNC_1:8 ;
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = (Reloc ((ProgramPart p),k)) . (loc + k) by A13, COMPOS_1:122
.= P2 . (IC (Comput (P2,s2,(i + 1)))) by A12, A14, A4, GRFUNC_1:8
.= CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A15, PARTFUN1:def 8 ;
:: thesis: verum

end;

set I = CurInstr (P1,(Comput (P1,s1,i)));
A16: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:4
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
reconsider j = IC (Comput (P1,s1,i)) as Element of NAT ;
A17: Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:4
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
A18: the Instructions of (STC N) = {[0,0,0],[1,0,0]} by AMISTD_1:def 11;

per cases ( CurInstr (P1,(Comput (P1,s1,i))) = [0,0,0] or CurInstr (P1,(Comput (P1,s1,i))) = [1,0,0] ) by A18, TARSKI:def 2;

suppose CurInstr (P1,(Comput (P1,s1,i))) = [0,0,0] ; :: thesis: S₁[i + 1]

then A19: CurInstr (P1,(Comput (P1,s1,i))) = halt (STC N) by AMISTD_1:def 11;
thus (IC (Comput (P1,s1,(i + 1)))) + k = (IC (Comput (P1,s1,i))) + k by A17, A19, EXTPRO_1:def 3
.= IC (Comput (P2,s2,(i + 1))) by A9, A16, A19, A10, EXTPRO_1:def 3 ; :: thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A11; :: thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
thus (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) ; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
thus DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) ; :: thesis: verum

end;

suppose CurInstr (P1,(Comput (P1,s1,i))) = [1,0,0] ; :: thesis: S₁[i + 1]

then A20: InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 1 by RECDEF_2:def 1;
then A21: Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P2,s2,i))) = IncIC ((Comput (P2,s2,i)),1) by AMISTD_1:59;
thus (IC (Comput (P1,s1,(i + 1)))) + k = (succ (IC (Comput (P1,s1,i)))) + k by A17, A20, AMISTD_1:38
.= IC (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P2,s2,i)))) by A21, A9, COMPOS_1:54
.= IC (Comput (P2,s2,(i + 1))) by A16, A10, COMPOS_1:92 ; :: thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A11; :: thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
thus (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart (Relocated (p,k)))) ; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
thus DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) ; :: thesis: verum

end;

end;

end;

A22: IC in dom (Relocated (p,k)) by COMPOS_1:119;
then B22: IC in dom (NPP (Relocated (p,k))) by COMPOS_1:179;

now

thus (IC (Comput (P1,s1,0))) + k = (IC s1) + k by EXTPRO_1:3
.= (IC (NPP p)) + k by A2, B1, GRFUNC_1:8
.= (IC p) + k by B1, GRFUNC_1:8
.= IC (Relocated (p,k)) by A1, COMPOS_1:120
.= IC (NPP (Relocated (p,k))) by A22, COMPOS_1:72
.= IC s2 by A3, B22, GRFUNC_1:8
.= IC (Comput (P2,s2,0)) by EXTPRO_1:3 ; :: thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),k) = CurInstr (P2,(Comput (P2,s2,0))) & (Comput (P1,s1,0)) | (dom (DataPart p)) = (Comput (P2,s2,0)) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput (P1,(s1 +* (DataPart s2)),0)) = DataPart (Comput (P2,s2,0)) )
reconsider loc = IC (NPP p) as Element of NAT ;
A23: IC (NPP p) = IC s1 by A2, B1, GRFUNC_1:8;
then IC (NPP p) = IC (Comput (P1,s1,0)) by EXTPRO_1:3;
then A24: loc in dom (ProgramPart p) by A7, Def4, A4, A2;
A25: (IC (NPP p)) + k in dom (Reloc ((ProgramPart p),k)) by A24, COMPOS_1:158;
IC in dom (Relocated (p,k)) by COMPOS_1:119;
then B26: IC in dom (NPP (Relocated (p,k))) by COMPOS_1:179;
A27: (ProgramPart p) . (IC (NPP p)) = P1 . (IC s1) by A23, A24, A4, GRFUNC_1:8;
dom P2 = NAT by PARTFUN1:def 4;
then A28: CurInstr (P2,(Comput (P2,s2,0))) = P2 . (IC (Comput (P2,s2,0))) by PARTFUN1:def 8
.= P2 . (IC s2) by EXTPRO_1:3
.= P2 . (IC (NPP (Relocated (p,k)))) by A3, B26, GRFUNC_1:8
.= P2 . (IC (Relocated (p,k))) by B26, GRFUNC_1:8
.= P2 . ((IC p) + k) by A1, COMPOS_1:120
.= P2 . ((IC (NPP p)) + k) by A1, COMPOS_1:72
.= (Reloc ((ProgramPart p),k)) . ((IC (NPP p)) + k) by A25, A4, GRFUNC_1:8 ;
A29: dom P1 = NAT by PARTFUN1:def 4;
CurInstr (P1,(Comput (P1,s1,0))) = CurInstr (P1,s1) by EXTPRO_1:3
.= P1 . (IC s1) by A29, PARTFUN1:def 8 ;
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),k) = CurInstr (P2,(Comput (P2,s2,0))) by A28, A24, A27, COMPOS_1:122; :: thesis: ( (Comput (P1,s1,0)) | (dom (DataPart p)) = (Comput (P2,s2,0)) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput (P1,(s1 +* (DataPart s2)),0)) = DataPart (Comput (P2,s2,0)) )
thus (Comput (P1,s1,0)) | (dom (DataPart p)) = (Comput (P2,s2,0)) | (dom (DataPart (Relocated (p,k)))) ; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),0)) = DataPart (Comput (P2,s2,0))
thus DataPart (Comput (P1,(s1 +* (DataPart s2)),0)) = DataPart (Comput (P2,s2,0)) ; :: thesis: verum

end;

then A30: S₁[ 0 ] ;
thus for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A30, A8); :: thesis: verum