let k be Element of NAT ; :: thesis:
let p be autonomic FinPartState of SCM+FSA ; :: thesis:
let s1, s2 be State of SCM+FSA ; :: thesis:
assume that
A1: IC SCM+FSA in dom p and
A2: p c= s1 and
A3: Relocated p,k c= s2 ; :: thesis:
set s3 = s1 +* (DataPart s2);
A5: IC SCM+FSA in dom (Relocated p,k) by Th5;
A6: DataPart p = DataPart (Relocated p,k) by Th1;
A7: DataPart p c= p by RELAT_1:88;
A8: DataPart (Relocated p,k) c= Relocated p,k by RELAT_1:88;
A9: not p is NAT -defined by A1, AMI_1:109;
A10: p c= s1 +* (DataPart s2) by A2, A3, Th10;
defpred S₁[ Element of NAT ] means ( (IC (Computation s1,$1)) + k = IC (Computation s2,$1) & IncAddr (CurInstr (Computation s1,$1)),k = CurInstr (Computation s2,$1) & (Computation s1,$1) | (dom (DataPart p)) = (Computation s2,$1) | (dom (DataPart (Relocated p,k))) & DataPart (Computation (s1 +* (DataPart s2)),$1) = DataPart (Computation s2,$1) );
reconsider ii = IC p as Element of NAT ;

now

thus (IC (Computation s1,0 )) + k = (IC s1) + k by AMI_1:13
.= (IC p) + k by A1, A2, AMI_1:97
.= IC (Relocated p,k) by Th6
.= IC s2 by A3, A5, AMI_1:97
.= IC (Computation s2,0 ) by AMI_1:13 ; :: thesis:
reconsider loc = IC p as Instruction-Location of SCM+FSA ;
A11: IC p = IC s1 by A1, A2, AMI_1:97;
then IC p = IC (Computation s1,0 ) by AMI_1:13;
then A12: loc in dom (ProgramPart p) by A2, A9, SCMFSA_3:17;
ProgramPart p c= p by RELAT_1:88;
then A13: dom (ProgramPart p) c= dom p by GRFUNC_1:8;
then A14: p . ii = s1 . (IC s1) by A2, A11, A12, GRFUNC_1:8;
A15: IncAddr (CurInstr (Computation s1,0 )),k = IncAddr (CurInstr s1),k by AMI_1:13
.= IncAddr (s1 . (IC s1)),k ;
A16: IC SCM+FSA in dom (Relocated p,k) by Th5;
A17: (IC p) + k in dom (Relocated p,k) by A12, A13, Th4;
CurInstr (Computation s2,0 ) = CurInstr s2 by AMI_1:13
.= s2 . (IC (Relocated p,k)) by A3, A16, AMI_1:97
.= s2 . ((IC p) + k) by Th6
.= (Relocated p,k) . ((IC p) + k) by A3, A17, GRFUNC_1:8 ;
hence IncAddr (CurInstr (Computation s1,0 )),k = CurInstr (Computation s2,0 ) by A12, A14, A15, Th7; :: thesis:
thus (Computation s1,0 ) | (dom (DataPart p)) = s1 | (dom (DataPart p)) by AMI_1:13
.= DataPart p by A2, A7, GRFUNC_1:64, XBOOLE_1:1
.= s2 | (dom (DataPart p)) by A3, A6, A8, GRFUNC_1:64, XBOOLE_1:1
.= (Computation s2,0 ) | (dom (DataPart (Relocated p,k))) by A6, AMI_1:13 ; :: thesis:
thus DataPart (Computation (s1 +* (DataPart s2)),0 ) = DataPart (s1 +* (DataPart s2)) by AMI_1:13
.= DataPart s2 by CARD_3:99
.= DataPart (Computation s2,0 ) by AMI_1:13 ; :: thesis:

end;

then A19: S₁[ 0 ] ;
A20: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

proof

let i be Element of NAT ; :: thesis:
assume that
A21: (IC (Computation s1,i)) + k = IC (Computation s2,i) and
A22: IncAddr (CurInstr (Computation s1,i)),k = CurInstr (Computation s2,i) and
A23: (Computation s1,i) | (dom (DataPart p)) = (Computation s2,i) | (dom (DataPart (Relocated p,k))) and
A24: DataPart (Computation (s1 +* (DataPart s2)),i) = DataPart (Computation s2,i) ; :: thesis:
set Cs1i = Computation s1,i;
set Cs2i = Computation s2,i;
set Cs3i = Computation (s1 +* (DataPart s2)),i;
set Cs1i1 = Computation s1,(i + 1);
set Cs2i1 = Computation s2,(i + 1);
set Cs3i1 = Computation (s1 +* (DataPart s2)),(i + 1);
set DPp = DataPart p;
A25: dom (DataPart p) = dom (DataPart (Relocated p,k)) by Th1;
A26: dom (Computation s1,(i + 1)) = ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT by AMI_1:79, SCMFSA_2:8;
A27: dom (Computation s2,(i + 1)) = ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT by AMI_1:79, SCMFSA_2:8;
A28: dom (Computation s1,i) = ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT by AMI_1:79, SCMFSA_2:8;
A29: dom (Computation s2,i) = ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT by AMI_1:79, SCMFSA_2:8;
dom (DataPart p) = (dom p) /\ (Int-Locations \/ FinSeq-Locations ) by RELAT_1:90, SCMFSA_2:127;
then A30: dom (DataPart p) c= {(IC SCM+FSA )} \/ (Int-Locations \/ FinSeq-Locations ) by XBOOLE_1:10, XBOOLE_1:17;
A31: dom ((Computation s1,(i + 1)) | (dom (DataPart p))) = (dom (Computation s1,(i + 1))) /\ (dom (DataPart p)) by RELAT_1:90
.= dom (DataPart p) by A26, A30, XBOOLE_1:10, XBOOLE_1:28 ;
A32: dom ((Computation s2,(i + 1)) | (dom (DataPart (Relocated p,k)))) = (dom (Computation s2,(i + 1))) /\ (dom (DataPart p)) by A25, RELAT_1:90
.= dom (DataPart p) by A27, A30, XBOOLE_1:10, XBOOLE_1:28 ;
A33: dom ((Computation s1,i) | (dom (DataPart p))) = (dom (Computation s1,i)) /\ (dom (DataPart p)) by RELAT_1:90
.= dom (DataPart p) by A28, A30, XBOOLE_1:10, XBOOLE_1:28 ;
A34: dom ((Computation s2,i) | (dom (DataPart (Relocated p,k)))) = (dom (Computation s2,i)) /\ (dom (DataPart p)) by A25, RELAT_1:90
.= dom (DataPart p) by A29, A30, XBOOLE_1:10, XBOOLE_1:28 ;
A35: dom (DataPart (Computation (s1 +* (DataPart s2)),i)) = Int-Locations \/ FinSeq-Locations by SCMFSA_2:127, SCMNORM:14;
A36: dom (DataPart (Computation s2,i)) = Int-Locations \/ FinSeq-Locations by SCMFSA_2:127, SCMNORM:14;
A37: dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) = Int-Locations \/ FinSeq-Locations by SCMFSA_2:127, SCMNORM:14;
A38: dom (DataPart (Computation s2,(i + 1))) = Int-Locations \/ FinSeq-Locations by SCMFSA_2:127, SCMNORM:14;

A39: now

let s be State of SCM+FSA ; :: thesis:
let d be Int-Location ; :: thesis:
d in Int-Locations by SCMFSA_2:9;
then d in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
hence d in dom (DataPart s) by SCMFSA_2:127, SCMNORM:14; :: thesis:

end;

A40: now

let s be State of SCM+FSA ; :: thesis:
let d be FinSeq-Location ; :: thesis:
d in FinSeq-Locations by SCMFSA_2:10;
then d in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
hence d in dom (DataPart s) by SCMFSA_2:127, SCMNORM:14; :: thesis:

end;

A41: now

let d be Int-Location ; :: thesis:
A42: ( d in dom (DataPart (Computation (s1 +* (DataPart s2)),i)) & d in dom (DataPart (Computation (s1 +* (DataPart s2)),i)) ) by A39;
hence (Computation (s1 +* (DataPart s2)),i) . d = (DataPart (Computation (s1 +* (DataPart s2)),i)) . d by FUNCT_1:70
.= (Computation s2,i) . d by A24, A42, FUNCT_1:70 ;
:: thesis:

end;

A43: now

let d be FinSeq-Location ; :: thesis:
A44: ( d in dom (DataPart (Computation (s1 +* (DataPart s2)),i)) & d in dom (DataPart (Computation (s1 +* (DataPart s2)),i)) ) by A40;
hence (Computation (s1 +* (DataPart s2)),i) . d = (DataPart (Computation (s1 +* (DataPart s2)),i)) . d by FUNCT_1:70
.= (Computation s2,i) . d by A24, A44, FUNCT_1:70 ;
:: thesis:

end;

A45: now

let x, d be set ; :: thesis:
assume that
A46: ( d = x & d in dom (DataPart p) ) and
A47: ( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) ; :: thesis:
( ((Computation s1,i) | (dom (DataPart p))) . d = (Computation s1,i) . d & ((Computation s2,i) | (dom (DataPart p))) . d = (Computation s2,i) . d ) by A25, A33, A34, A46, FUNCT_1:70;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = (Computation s2,(i + 1)) . d by A23, A25, A31, A46, A47, FUNCT_1:70
.= ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A25, A32, A46, FUNCT_1:70 ;
:: thesis:

end;

A48: now

let x, d be set ; :: thesis:
assume that
A49: ( d = x & d in dom (DataPart p) ) and
A50: (Computation s1,(i + 1)) . d = (Computation s2,(i + 1)) . d ; :: thesis:
thus ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = (Computation s2,(i + 1)) . d by A31, A49, A50, FUNCT_1:70
.= ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A25, A32, A49, FUNCT_1:70 ; :: thesis:

end;

A51: now

let x be set ; :: thesis:
assume A52: ( x in dom ((Computation (s1 +* (DataPart s2)),(i + 1)) | (Int-Locations \/ FinSeq-Locations )) & (Computation (s1 +* (DataPart s2)),(i + 1)) . x = (Computation s2,(i + 1)) . x ) ; :: thesis:
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (Computation s2,(i + 1)) . x by FUNCT_1:70, SCMFSA_2:127
.= (DataPart (Computation s2,(i + 1))) . x by A37, A38, A52, FUNCT_1:70, SCMFSA_2:127 ;
:: thesis:

end;

A53: now

let x be set ; :: thesis:
assume A54: ( x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) & (Computation (s1 +* (DataPart s2)),(i + 1)) . x = (Computation (s1 +* (DataPart s2)),i) . x & (Computation s2,(i + 1)) . x = (Computation s2,i) . x ) ; :: thesis:
then ( (DataPart (Computation (s1 +* (DataPart s2)),i)) . x = (Computation (s1 +* (DataPart s2)),i) . x & (DataPart (Computation s2,i)) . x = (Computation s2,i) . x ) by A35, A36, A37, FUNCT_1:70;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A24, A51, A54, SCMFSA_2:127; :: thesis:

end;

A55: now

assume A56: (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) ; :: thesis:
reconsider loc = IC (Computation s1,(i + 1)) as Instruction-Location of SCM+FSA ;
reconsider ii = loc as Element of NAT by ORDINAL1:def 13;
A57: ii in dom (ProgramPart p) by A2, A9, SCMFSA_3:17;
ProgramPart p c= p by RELAT_1:88;
then A58: dom (ProgramPart p) c= dom p by GRFUNC_1:8;
A59: CurInstr (Computation s1,(i + 1)) = s1 . loc by AMI_1:54
.= p . ii by A2, A57, A58, GRFUNC_1:8 ;
loc + k in dom (Relocated p,k) by A57, A58, Th4;
then (Relocated p,k) . (loc + k) = s2 . (loc + k) by A3, GRFUNC_1:8
.= (Computation s2,(i + 1)) . (loc + k) by AMI_1:54 ;
hence IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A56, A57, A59, Th7; :: thesis:

end;

A60: Computation s1,(i + 1) = Following (Computation s1,i) by AMI_1:14
.= Exec (CurInstr (Computation s1,i)),(Computation s1,i) ;
A61: Computation s2,(i + 1) = Following (Computation s2,i) by AMI_1:14
.= Exec (CurInstr (Computation s2,i)),(Computation s2,i) ;
A62: Computation (s1 +* (DataPart s2)),(i + 1) = Following (Computation (s1 +* (DataPart s2)),i) by AMI_1:14
.= Exec (CurInstr (Computation s1,i)),(Computation (s1 +* (DataPart s2)),i) by A2, A9, A10, SCMFSA_3:18 ;
reconsider j = IC (Computation s1,i) as Element of NAT by ORDINAL1:def 13;
A64: Next ((IC (Computation s1,i)) + k) = insloc ((j + k) + 1) by NAT_1:39
.= (insloc (j + 1)) + k
.= (Next (IC (Computation s1,i))) + k by NAT_1:39 ;
set I = CurInstr (Computation s1,i);
A65: InsCode (CurInstr (Computation s1,i)) <= 11 + 1 by SCMFSA_2:35;
A66: ( not InsCode (CurInstr (Computation s1,i)) <= 10 + 1 or InsCode (CurInstr (Computation s1,i)) <= 10 or InsCode (CurInstr (Computation s1,i)) = 11 ) by NAT_1:8;
A67: ( not InsCode (CurInstr (Computation s1,i)) <= 9 + 1 or InsCode (CurInstr (Computation s1,i)) <= 8 + 1 or InsCode (CurInstr (Computation s1,i)) = 10 ) by NAT_1:8;

per cases by A65, A66, A67, NAT_1:8, NAT_1:33;

suppose InsCode (CurInstr (Computation s1,i)) = 0 ; :: thesis:

then A68: CurInstr (Computation s1,i) = halt SCM+FSA by SCMFSA_2:122;
then A69: CurInstr (Computation s2,i) = halt SCM+FSA by A22, SCMFSA_4:8;
thus (IC (Computation s1,(i + 1))) + k = (IC (Computation s1,i)) + k by A60, A68, AMI_1:def 8
.= IC (Computation s2,(i + 1)) by A21, A61, A69, AMI_1:def 8 ; :: thesis:
hence IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A55; :: thesis:
A70: ( Computation s2,(i + 1) = Computation s2,i & Computation s1,(i + 1) = Computation s1,i ) by A60, A61, A68, A69, AMI_1:def 8;
hence (Computation s1,(i + 1)) | (dom (DataPart p)) = (Computation s2,(i + 1)) | (dom (DataPart (Relocated p,k))) by A23; :: thesis:
thus DataPart (Computation (s1 +* (DataPart s2)),(i + 1)) = DataPart (Computation s2,(i + 1)) by A24, A62, A68, A70, AMI_1:def 8; :: thesis:

end;

suppose InsCode (CurInstr (Computation s1,i)) = 1 ; :: thesis:

then consider da, db being Int-Location such that
A71: CurInstr (Computation s1,i) = da := db by SCMFSA_2:54;
A72: IncAddr (CurInstr (Computation s1,i)),k = da := db by A71, SCMFSA_4:9;
A73: (Exec (CurInstr (Computation s1,i)),(Computation s1,i)) . (IC SCM+FSA ) = Next (IC (Computation s1,i)) by A71, SCMFSA_2:89;
A74: (Computation (s1 +* (DataPart s2)),i) . db = (Computation s2,i) . db by A41;
thus (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A21, A22, A60, A61, A64, A72, A73, SCMFSA_2:89; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A21, A22, A55, A60, A61, A64, A72, A73, SCMFSA_2:89; :: thesis:

now

let x be set ; :: thesis:
assume A75: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
A76: dom (DataPart p) c= Int-Locations \/ FinSeq-Locations by RELAT_1:87, SCMFSA_2:127;

per cases by A31, A75, A76, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A22, A60, A61, A71, A72, SCMFSA_2:89;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A45, A75; :: thesis:

end;

suppose A77: da = x ; :: thesis:

then A78: (Computation s1,(i + 1)) . x = (Computation s1,i) . db by A60, A71, SCMFSA_2:89;
A79: (Computation s2,(i + 1)) . x = (Computation s2,i) . db by A22, A61, A72, A77, SCMFSA_2:89;
DataPart p c= p by RELAT_1:88;
then dom (DataPart p) c= dom p by GRFUNC_1:8;
then (Computation (s1 +* (DataPart s2)),i) . db = (Computation s1,i) . db by A2, A9, A10, A31, A71, A75, A77, SCMFSA_3:19;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A48, A74, A75, A78, A79; :: thesis:

end;

suppose A80: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by SCMFSA_2:11;
( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A22, A60, A61, A71, A72, A80, SCMFSA_2:89;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A45, A75; :: thesis:

end;

then (Computation s1,(i + 1)) | (dom (DataPart p)) c= (Computation s2,(i + 1)) | (dom (DataPart p)) by A25, A31, A32, GRFUNC_1:8;
hence (Computation s1,(i + 1)) | (dom (DataPart p)) = (Computation s2,(i + 1)) | (dom (DataPart (Relocated p,k))) by A25, A31, A32, GRFUNC_1:9; :: thesis:

now

let x be set ; :: thesis:
assume A81: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:

per cases by A37, A81, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider f = x as FinSeq-Location by SCMFSA_2:12;
A82: (Computation (s1 +* (DataPart s2)),(i + 1)) . f = (Computation (s1 +* (DataPart s2)),i) . f by A62, A71, SCMFSA_2:89;
(Computation s2,(i + 1)) . f = (Computation s2,i) . f by A22, A61, A72, SCMFSA_2:89;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A53, A81, A82; :: thesis:

end;

suppose A83: da = x ; :: thesis:

( (Computation s2,(i + 1)) . da = (Computation s2,i) . db & (Computation (s1 +* (DataPart s2)),(i + 1)) . da = (Computation (s1 +* (DataPart s2)),i) . db ) by A22, A61, A62, A71, A72, SCMFSA_2:89;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A41, A51, A81, A83, SCMFSA_2:127; :: thesis:

end;

suppose A84: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by SCMFSA_2:11;
A85: (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d by A62, A71, A84, SCMFSA_2:89;
(Computation s2,(i + 1)) . d = (Computation s2,i) . d by A22, A61, A72, A84, SCMFSA_2:89;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A53, A81, A85; :: thesis:

end;

then DataPart (Computation (s1 +* (DataPart s2)),(i + 1)) c= DataPart (Computation s2,(i + 1)) by A37, A38, GRFUNC_1:8;
hence DataPart (Computation (s1 +* (DataPart s2)),(i + 1)) = DataPart (Computation s2,(i + 1)) by A37, A38, GRFUNC_1:9; :: thesis:

end;

suppose InsCode (CurInstr (Computation s1,i)) = 2 ; :: thesis:

then consider da, db being Int-Location such that
A86: CurInstr (Computation s1,i) = AddTo da,db by SCMFSA_2:55;
A87: IncAddr (CurInstr (Computation s1,i)),k = AddTo da,db by A86, SCMFSA_4:10;
A88: (Exec (CurInstr (Computation s1,i)),(Computation s1,i)) . (IC SCM+FSA ) = Next (IC (Computation s1,i)) by A86, SCMFSA_2:90;
A89: (Computation (s1 +* (DataPart s2)),i) . da = (Computation s2,i) . da by A41;
A90: (Computation (s1 +* (DataPart s2)),i) . db = (Computation s2,i) . db by A41;
thus (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A21, A22, A60, A61, A64, A87, A88, SCMFSA_2:90; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A21, A22, A55, A60, A61, A64, A87, A88, SCMFSA_2:90; :: thesis:

now

let x be set ; :: thesis:
assume A91: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
A92: dom (DataPart p) c= Int-Locations \/ FinSeq-Locations by RELAT_1:87, SCMFSA_2:127;

per cases by A31, A91, A92, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A22, A60, A61, A86, A87, SCMFSA_2:90;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A45, A91; :: thesis:

end;

suppose A93: da = x ; :: thesis:

then A94: (Computation s1,(i + 1)) . x = ((Computation s1,i) . da) + ((Computation s1,i) . db) by A60, A86, SCMFSA_2:90;
DataPart p c= p by RELAT_1:88;
then A95: dom (DataPart p) c= dom p by GRFUNC_1:8;
(Computation s2,(i + 1)) . x = ((Computation s2,i) . da) + ((Computation s2,i) . db) by A22, A61, A87, A93, SCMFSA_2:90;
then (Computation s1,(i + 1)) . x = (Computation s2,(i + 1)) . x by A2, A9, A10, A31, A86, A89, A90, A91, A93, A94, A95, SCMFSA_3:20;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A48, A91; :: thesis:

end;

suppose A96: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by SCMFSA_2:11;
( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A22, A60, A61, A86, A87, A96, SCMFSA_2:90;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A45, A91; :: thesis:

end;

now

let x be set ; :: thesis:
assume A97: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:

per cases by A37, A97, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
A98: (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d by A62, A86, SCMFSA_2:90;
(Computation s2,(i + 1)) . d = (Computation s2,i) . d by A22, A61, A87, SCMFSA_2:90;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A53, A97, A98; :: thesis:

end;

suppose A99: da = x ; :: thesis:

then A100: (Computation s2,(i + 1)) . x = ((Computation s2,i) . da) + ((Computation s2,i) . db) by A22, A61, A87, SCMFSA_2:90;
(Computation (s1 +* (DataPart s2)),(i + 1)) . x = ((Computation (s1 +* (DataPart s2)),i) . da) + ((Computation (s1 +* (DataPart s2)),i) . db) by A62, A86, A99, SCMFSA_2:90;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A51, A89, A90, A97, A100, SCMFSA_2:127; :: thesis:

end;

suppose A101: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by SCMFSA_2:11;
A102: (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d by A62, A86, A101, SCMFSA_2:90;
(Computation s2,(i + 1)) . d = (Computation s2,i) . d by A22, A61, A87, A101, SCMFSA_2:90;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A53, A97, A102; :: thesis:

end;

suppose InsCode (CurInstr (Computation s1,i)) = 3 ; :: thesis:

then consider da, db being Int-Location such that
A103: CurInstr (Computation s1,i) = SubFrom da,db by SCMFSA_2:56;
A104: IncAddr (CurInstr (Computation s1,i)),k = SubFrom da,db by A103, SCMFSA_4:11;
A105: (Exec (CurInstr (Computation s1,i)),(Computation s1,i)) . (IC SCM+FSA ) = Next (IC (Computation s1,i)) by A103, SCMFSA_2:91;
A106: (Computation (s1 +* (DataPart s2)),i) . da = (Computation s2,i) . da by A41;
A107: (Computation (s1 +* (DataPart s2)),i) . db = (Computation s2,i) . db by A41;
thus (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A21, A22, A60, A61, A64, A104, A105, SCMFSA_2:91; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A21, A22, A55, A60, A61, A64, A104, A105, SCMFSA_2:91; :: thesis:

now

let x be set ; :: thesis:
assume A108: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
A109: dom (DataPart p) c= Int-Locations \/ FinSeq-Locations by RELAT_1:87, SCMFSA_2:127;

per cases by A31, A108, A109, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A22, A60, A61, A103, A104, SCMFSA_2:91;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A45, A108; :: thesis:

end;

suppose A110: da = x ; :: thesis:

then A111: (Computation s1,(i + 1)) . x = ((Computation s1,i) . da) - ((Computation s1,i) . db) by A60, A103, SCMFSA_2:91;
DataPart p c= p by RELAT_1:88;
then A112: dom (DataPart p) c= dom p by GRFUNC_1:8;
(Computation s2,(i + 1)) . x = ((Computation s2,i) . da) - ((Computation s2,i) . db) by A22, A61, A104, A110, SCMFSA_2:91;
then ((Computation s1,i) . da) - ((Computation s1,i) . db) = (Computation s2,(i + 1)) . x by A2, A9, A10, A31, A103, A106, A107, A108, A110, A112, SCMFSA_3:21;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A48, A108, A111; :: thesis:

end;

suppose A113: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by SCMFSA_2:11;
( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A22, A60, A61, A103, A104, A113, SCMFSA_2:91;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A45, A108; :: thesis:

end;

now

let x be set ; :: thesis:
assume A114: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:

per cases by A37, A114, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
A115: (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d by A62, A103, SCMFSA_2:91;
(Computation s2,(i + 1)) . d = (Computation s2,i) . d by A22, A61, A104, SCMFSA_2:91;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A53, A114, A115; :: thesis:

end;

suppose A116: da = x ; :: thesis:

then A117: (Computation s2,(i + 1)) . x = ((Computation s2,i) . da) - ((Computation s2,i) . db) by A22, A61, A104, SCMFSA_2:91;
(Computation (s1 +* (DataPart s2)),(i + 1)) . x = ((Computation (s1 +* (DataPart s2)),i) . da) - ((Computation (s1 +* (DataPart s2)),i) . db) by A62, A103, A116, SCMFSA_2:91;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A51, A106, A107, A114, A117, SCMFSA_2:127; :: thesis:

end;

suppose A118: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by SCMFSA_2:11;
A119: (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d by A62, A103, A118, SCMFSA_2:91;
(Computation s2,(i + 1)) . d = (Computation s2,i) . d by A22, A61, A104, A118, SCMFSA_2:91;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A53, A114, A119; :: thesis:

end;

suppose InsCode (CurInstr (Computation s1,i)) = 4 ; :: thesis:

then consider da, db being Int-Location such that
A120: CurInstr (Computation s1,i) = MultBy da,db by SCMFSA_2:57;
A121: IncAddr (CurInstr (Computation s1,i)),k = MultBy da,db by A120, SCMFSA_4:12;
A122: (Exec (CurInstr (Computation s1,i)),(Computation s1,i)) . (IC SCM+FSA ) = Next (IC (Computation s1,i)) by A120, SCMFSA_2:92;
A123: (Computation (s1 +* (DataPart s2)),i) . da = (Computation s2,i) . da by A41;
A124: (Computation (s1 +* (DataPart s2)),i) . db = (Computation s2,i) . db by A41;
thus (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A21, A22, A60, A61, A64, A121, A122, SCMFSA_2:92; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A21, A22, A55, A60, A61, A64, A121, A122, SCMFSA_2:92; :: thesis:

now

let x be set ; :: thesis:
assume A125: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
A126: dom (DataPart p) c= Int-Locations \/ FinSeq-Locations by RELAT_1:87, SCMFSA_2:127;

per cases by A31, A125, A126, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A22, A60, A61, A120, A121, SCMFSA_2:92;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A45, A125; :: thesis:

end;

suppose A127: da = x ; :: thesis:

then A128: (Computation s1,(i + 1)) . x = ((Computation s1,i) . da) * ((Computation s1,i) . db) by A60, A120, SCMFSA_2:92;
DataPart p c= p by RELAT_1:88;
then A129: dom (DataPart p) c= dom p by GRFUNC_1:8;
(Computation s2,(i + 1)) . x = ((Computation s2,i) . da) * ((Computation s2,i) . db) by A22, A61, A121, A127, SCMFSA_2:92;
then (Computation s1,(i + 1)) . x = (Computation s2,(i + 1)) . x by A2, A9, A10, A31, A120, A123, A124, A125, A127, A128, A129, SCMFSA_3:22;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A48, A125; :: thesis:

end;

suppose A130: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by SCMFSA_2:11;
( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A22, A60, A61, A120, A121, A130, SCMFSA_2:92;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A45, A125; :: thesis:

end;

now

let x be set ; :: thesis:
assume A131: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:

per cases by A37, A131, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
A132: (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d by A62, A120, SCMFSA_2:92;
(Computation s2,(i + 1)) . d = (Computation s2,i) . d by A22, A61, A121, SCMFSA_2:92;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A53, A131, A132; :: thesis:

end;

suppose A133: da = x ; :: thesis:

then A134: (Computation s2,(i + 1)) . x = ((Computation s2,i) . da) * ((Computation s2,i) . db) by A22, A61, A121, SCMFSA_2:92;
(Computation (s1 +* (DataPart s2)),(i + 1)) . x = ((Computation (s1 +* (DataPart s2)),i) . da) * ((Computation (s1 +* (DataPart s2)),i) . db) by A62, A120, A133, SCMFSA_2:92;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A51, A123, A124, A131, A134, SCMFSA_2:127; :: thesis:

end;

suppose A135: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by SCMFSA_2:11;
A136: (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d by A62, A120, A135, SCMFSA_2:92;
(Computation s2,(i + 1)) . d = (Computation s2,i) . d by A22, A61, A121, A135, SCMFSA_2:92;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A53, A131, A136; :: thesis:

end;

suppose InsCode (CurInstr (Computation s1,i)) = 5 ; :: thesis:

then consider da, db being Int-Location such that
A137: CurInstr (Computation s1,i) = Divide da,db by SCMFSA_2:58;
A138: IncAddr (CurInstr (Computation s1,i)),k = Divide da,db by A137, SCMFSA_4:13;
A139: (Computation (s1 +* (DataPart s2)),i) . da = (Computation s2,i) . da by A41;
A140: (Computation (s1 +* (DataPart s2)),i) . db = (Computation s2,i) . db by A41;

now

per cases ;

suppose A141: da <> db ; :: thesis:

A142: (Exec (CurInstr (Computation s1,i)),(Computation s1,i)) . (IC SCM+FSA ) = Next (IC (Computation s1,i)) by A137, SCMFSA_2:93;
hence (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A21, A22, A60, A61, A64, A138, SCMFSA_2:93; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A21, A22, A55, A60, A61, A64, A138, A142, SCMFSA_2:93; :: thesis:

now

let x be set ; :: thesis:
assume A143: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
A144: dom (DataPart p) c= Int-Locations \/ FinSeq-Locations by RELAT_1:87, SCMFSA_2:127;

per cases by A31, A143, A144, XBOOLE_0:def 3;

suppose ( db <> x & x in FinSeq-Locations ) ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A22, A60, A61, A137, A138, SCMFSA_2:93;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A45, A143; :: thesis:

end;

suppose A145: da = x ; :: thesis:

then A146: (Computation s1,(i + 1)) . x = ((Computation s1,i) . da) div ((Computation s1,i) . db) by A60, A137, A141, SCMFSA_2:93;
A147: (Computation s2,(i + 1)) . x = ((Computation s2,i) . da) div ((Computation s2,i) . db) by A22, A61, A138, A141, A145, SCMFSA_2:93;
DataPart p c= p by RELAT_1:88;
then dom (DataPart p) c= dom p by GRFUNC_1:8;
then ((Computation (s1 +* (DataPart s2)),i) . da) div ((Computation (s1 +* (DataPart s2)),i) . db) = ((Computation s1,i) . da) div ((Computation s1,i) . db) by A2, A9, A10, A31, A137, A141, A143, A145, SCMFSA_3:23;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = (Computation s2,(i + 1)) . x by A139, A140, A143, A146, A147, FUNCT_1:70
.= ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A25, A31, A32, A143, FUNCT_1:70 ;
:: thesis:

end;

suppose A148: db = x ; :: thesis:

then A149: (Computation s1,(i + 1)) . x = ((Computation s1,i) . da) mod ((Computation s1,i) . db) by A60, A137, SCMFSA_2:93;
DataPart p c= p by RELAT_1:88;
then A150: dom (DataPart p) c= dom p by GRFUNC_1:8;
(Computation s2,(i + 1)) . x = ((Computation s2,i) . da) mod ((Computation s2,i) . db) by A22, A61, A138, A148, SCMFSA_2:93;
then (Computation s1,(i + 1)) . x = (Computation s2,(i + 1)) . x by A2, A9, A10, A31, A137, A139, A140, A141, A143, A148, A149, A150, SCMFSA_3:24;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A48, A143; :: thesis:

end;

suppose A151: ( da <> x & db <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by SCMFSA_2:11;
( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A22, A60, A61, A137, A138, A151, SCMFSA_2:93;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A45, A143; :: thesis:

end;

now

let x be set ; :: thesis:
assume A152: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:

per cases by A37, A152, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
A153: (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d by A62, A137, SCMFSA_2:93;
(Computation s2,(i + 1)) . d = (Computation s2,i) . d by A22, A61, A138, SCMFSA_2:93;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A53, A152, A153; :: thesis:

end;

suppose A154: da = x ; :: thesis:

then A155: (Computation s2,(i + 1)) . x = ((Computation s2,i) . da) div ((Computation s2,i) . db) by A22, A61, A138, A141, SCMFSA_2:93;
(Computation (s1 +* (DataPart s2)),(i + 1)) . x = ((Computation (s1 +* (DataPart s2)),i) . da) div ((Computation (s1 +* (DataPart s2)),i) . db) by A62, A137, A141, A154, SCMFSA_2:93;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A51, A139, A140, A152, A155, SCMFSA_2:127; :: thesis:

end;

suppose A156: db = x ; :: thesis:

then A157: (Computation s2,(i + 1)) . x = ((Computation s2,i) . da) mod ((Computation s2,i) . db) by A22, A61, A138, SCMFSA_2:93;
(Computation (s1 +* (DataPart s2)),(i + 1)) . x = ((Computation (s1 +* (DataPart s2)),i) . da) mod ((Computation (s1 +* (DataPart s2)),i) . db) by A62, A137, A156, SCMFSA_2:93;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A51, A139, A140, A152, A157, SCMFSA_2:127; :: thesis:

end;

suppose A158: ( da <> x & db <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by SCMFSA_2:11;
A159: (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d by A62, A137, A158, SCMFSA_2:93;
(Computation s2,(i + 1)) . d = (Computation s2,i) . d by A22, A61, A138, A158, SCMFSA_2:93;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A53, A152, A159; :: thesis:

end;

suppose A160: da = db ; :: thesis:

then A161: (Exec (CurInstr (Computation s1,i)),(Computation s1,i)) . (IC SCM+FSA ) = Next (IC (Computation s1,i)) by A137, SCMFSA_2:94;
hence (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A21, A22, A60, A61, A64, A138, A160, SCMFSA_2:94; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A21, A22, A55, A60, A61, A64, A138, A160, A161, SCMFSA_2:94; :: thesis:

now

let x be set ; :: thesis:
assume A162: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
A163: dom (DataPart p) c= Int-Locations \/ FinSeq-Locations by RELAT_1:87, SCMFSA_2:127;

per cases by A31, A162, A163, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A22, A60, A61, A137, A138, A160, SCMFSA_2:94;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A45, A162; :: thesis:

end;

suppose A164: da = x ; :: thesis:

then A165: (Computation s2,(i + 1)) . x = ((Computation s2,i) . da) mod ((Computation s2,i) . db) by A22, A61, A138, A160, SCMFSA_2:94;
A166: ( ((Computation s1,i) | (dom (DataPart p))) . x = (Computation s1,i) . x & ((Computation s2,i) | (dom (DataPart p))) . x = (Computation s2,i) . x ) by A25, A31, A33, A34, A162, FUNCT_1:70;
( ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = (Computation s1,(i + 1)) . x & ((Computation s2,(i + 1)) | (dom (DataPart p))) . x = (Computation s2,(i + 1)) . x ) by A25, A31, A32, A162, FUNCT_1:70;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A23, A25, A60, A137, A160, A164, A165, A166, SCMFSA_2:94; :: thesis:

end;

suppose A167: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by SCMFSA_2:11;
( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A22, A60, A61, A137, A138, A160, A167, SCMFSA_2:94;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A45, A162; :: thesis:

end;

now

let x be set ; :: thesis:
assume A168: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:

per cases by A37, A168, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
A169: (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d by A62, A137, A160, SCMFSA_2:94;
(Computation s2,(i + 1)) . d = (Computation s2,i) . d by A22, A61, A138, A160, SCMFSA_2:94;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A53, A168, A169; :: thesis:

end;

suppose A170: da = x ; :: thesis:

then A171: (Computation s2,(i + 1)) . x = ((Computation s2,i) . da) mod ((Computation s2,i) . db) by A22, A61, A138, A160, SCMFSA_2:94;
(Computation (s1 +* (DataPart s2)),(i + 1)) . x = ((Computation (s1 +* (DataPart s2)),i) . da) mod ((Computation (s1 +* (DataPart s2)),i) . db) by A62, A137, A160, A170, SCMFSA_2:94;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A51, A139, A140, A168, A171, SCMFSA_2:127; :: thesis:

end;

suppose A172: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by SCMFSA_2:11;
A173: (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d by A62, A137, A160, A172, SCMFSA_2:94;
(Computation s2,(i + 1)) . d = (Computation s2,i) . d by A22, A61, A138, A160, A172, SCMFSA_2:94;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A53, A168, A173; :: thesis:

end;

hence S₁[i + 1] ; :: thesis:

end;

suppose InsCode (CurInstr (Computation s1,i)) = 6 ; :: thesis:

then consider loc being Instruction-Location of SCM+FSA such that
A174: CurInstr (Computation s1,i) = goto loc by SCMFSA_2:59;
A175: CurInstr (Computation s2,i) = goto (loc + k) by A22, A174, SCMFSA_4:14;
thus (IC (Computation s1,(i + 1))) + k = loc + k by A60, A174, SCMFSA_2:95
.= IC (Computation s2,(i + 1)) by A61, A175, SCMFSA_2:95 ; :: thesis:
hence IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A55; :: thesis:

now

let x be set ; :: thesis:
assume A176: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= Int-Locations \/ FinSeq-Locations by RELAT_1:87, SCMFSA_2:127;
then ( x in Int-Locations or x in FinSeq-Locations ) by A31, A176, XBOOLE_0:def 3;
then ( x is Int-Location or x is FinSeq-Location ) by SCMFSA_2:11, SCMFSA_2:12;
then ( (Computation s1,(i + 1)) . x = (Computation s1,i) . x & (Computation s2,(i + 1)) . x = (Computation s2,i) . x ) by A60, A61, A174, A175, SCMFSA_2:95;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A45, A176; :: thesis:

end;

now

let x be set ; :: thesis:
assume A177: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:
then ( x in Int-Locations or x in FinSeq-Locations ) by A37, XBOOLE_0:def 3;
then ( x is Int-Location or x is FinSeq-Location ) by SCMFSA_2:11, SCMFSA_2:12;
then ( (Computation (s1 +* (DataPart s2)),(i + 1)) . x = (Computation (s1 +* (DataPart s2)),i) . x & (Computation s2,(i + 1)) . x = (Computation s2,i) . x ) by A61, A62, A174, A175, SCMFSA_2:95;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A53, A177; :: thesis:

end;

suppose InsCode (CurInstr (Computation s1,i)) = 7 ; :: thesis:

then consider loc being Instruction-Location of SCM+FSA , da being Int-Location such that
A178: CurInstr (Computation s1,i) = da =0_goto loc by SCMFSA_2:60;
A179: CurInstr (Computation s2,i) = da =0_goto (loc + k) by A22, A178, SCMFSA_4:15;
A180: (Computation (s1 +* (DataPart s2)),i) . da = (Computation s2,i) . da by A41;

A181: now

per cases ) . da = 0 or (Computation s1,i) . da <> 0 ) ;

case (Computation s1,i) . da = 0 ; :: thesis:

hence (IC (Computation s1,(i + 1))) + k = loc + k by A60, A178, SCMFSA_2:96; :: thesis:

end;

case (Computation s1,i) . da <> 0 ; :: thesis:

hence (IC (Computation s1,(i + 1))) + k = Next (IC (Computation s2,i)) by A21, A60, A64, A178, SCMFSA_2:96; :: thesis:

end;

A182: now

per cases ) . da = 0 or (Computation s2,i) . da <> 0 ) ;

case (Computation s2,i) . da = 0 ; :: thesis:

hence IC (Computation s2,(i + 1)) = loc + k by A61, A179, SCMFSA_2:96; :: thesis:

end;

case (Computation s2,i) . da <> 0 ; :: thesis:

hence IC (Computation s2,(i + 1)) = Next (IC (Computation s2,i)) by A61, A179, SCMFSA_2:96; :: thesis:

end;

A183: now

per cases ;

suppose loc <> Next (IC (Computation s1,i)) ; :: thesis:

hence (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A2, A9, A10, A178, A180, A181, A182, SCMFSA_3:25; :: thesis:

end;

suppose loc = Next (IC (Computation s1,i)) ; :: thesis:

hence (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A21, A64, A181, A182; :: thesis:

end;

hence (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) ; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A55, A183; :: thesis:

now

let x be set ; :: thesis:
assume A184: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= Int-Locations \/ FinSeq-Locations by RELAT_1:87, SCMFSA_2:127;
then ( x in Int-Locations or x in FinSeq-Locations ) by A31, A184, XBOOLE_0:def 3;
then ( x is Int-Location or x is FinSeq-Location ) by SCMFSA_2:11, SCMFSA_2:12;
then ( (Computation s1,(i + 1)) . x = (Computation s1,i) . x & (Computation s2,(i + 1)) . x = (Computation s2,i) . x ) by A60, A61, A178, A179, SCMFSA_2:96;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A45, A184; :: thesis:

end;

now

let x be set ; :: thesis:
assume A185: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:
then ( x in Int-Locations or x in FinSeq-Locations ) by A37, XBOOLE_0:def 3;
then ( x is Int-Location or x is FinSeq-Location ) by SCMFSA_2:11, SCMFSA_2:12;
then ( (Computation (s1 +* (DataPart s2)),(i + 1)) . x = (Computation (s1 +* (DataPart s2)),i) . x & (Computation s2,(i + 1)) . x = (Computation s2,i) . x ) by A61, A62, A178, A179, SCMFSA_2:96;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A53, A185; :: thesis:

end;

suppose InsCode (CurInstr (Computation s1,i)) = 8 ; :: thesis:

then consider loc being Instruction-Location of SCM+FSA , da being Int-Location such that
A186: CurInstr (Computation s1,i) = da >0_goto loc by SCMFSA_2:61;
A187: CurInstr (Computation s2,i) = da >0_goto (loc + k) by A22, A186, SCMFSA_4:16;
A188: (Computation (s1 +* (DataPart s2)),i) . da = (Computation s2,i) . da by A41;

A189: now

per cases ) . da > 0 or (Computation s1,i) . da <= 0 ) ;

case (Computation s1,i) . da > 0 ; :: thesis:

hence (IC (Computation s1,(i + 1))) + k = loc + k by A60, A186, SCMFSA_2:97; :: thesis:

end;

case (Computation s1,i) . da <= 0 ; :: thesis:

hence (IC (Computation s1,(i + 1))) + k = Next (IC (Computation s2,i)) by A21, A60, A64, A186, SCMFSA_2:97; :: thesis:

end;

A190: now

per cases ) . da > 0 or (Computation s2,i) . da <= 0 ) ;

case (Computation s2,i) . da > 0 ; :: thesis:

hence IC (Computation s2,(i + 1)) = loc + k by A61, A187, SCMFSA_2:97; :: thesis:

end;

case (Computation s2,i) . da <= 0 ; :: thesis:

hence IC (Computation s2,(i + 1)) = Next (IC (Computation s2,i)) by A61, A187, SCMFSA_2:97; :: thesis:

end;

A191: now

per cases ;

suppose loc <> Next (IC (Computation s1,i)) ; :: thesis:

hence (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A2, A9, A10, A186, A188, A189, A190, SCMFSA_3:26; :: thesis:

end;

suppose loc = Next (IC (Computation s1,i)) ; :: thesis:

hence (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A21, A64, A189, A190; :: thesis:

end;

now

let x be set ; :: thesis:
assume A192: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= Int-Locations \/ FinSeq-Locations by RELAT_1:87, SCMFSA_2:127;
then ( x in Int-Locations or x in FinSeq-Locations ) by A31, A192, XBOOLE_0:def 3;
then ( x is Int-Location or x is FinSeq-Location ) by SCMFSA_2:11, SCMFSA_2:12;
then ( (Computation s1,(i + 1)) . x = (Computation s1,i) . x & (Computation s2,(i + 1)) . x = (Computation s2,i) . x ) by A60, A61, A186, A187, SCMFSA_2:97;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A45, A192; :: thesis:

end;

now

let x be set ; :: thesis:
assume A193: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:
then ( x in Int-Locations or x in FinSeq-Locations ) by A37, XBOOLE_0:def 3;
then ( x is Int-Location or x is FinSeq-Location ) by SCMFSA_2:11, SCMFSA_2:12;
then ( (Computation (s1 +* (DataPart s2)),(i + 1)) . x = (Computation (s1 +* (DataPart s2)),i) . x & (Computation s2,(i + 1)) . x = (Computation s2,i) . x ) by A61, A62, A186, A187, SCMFSA_2:97;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A53, A193; :: thesis:

end;

suppose InsCode (CurInstr (Computation s1,i)) = 9 ; :: thesis:

then consider db, da being Int-Location , f being FinSeq-Location such that
A194: CurInstr (Computation s1,i) = da := f,db by SCMFSA_2:62;
A195: IncAddr (CurInstr (Computation s1,i)),k = da := f,db by A194, SCMFSA_4:17;
A196: (Exec (CurInstr (Computation s1,i)),(Computation s1,i)) . (IC SCM+FSA ) = Next (IC (Computation s1,i)) by A194, SCMFSA_2:98;
A197: (Computation (s1 +* (DataPart s2)),i) . db = (Computation s2,i) . db by A41;
A198: (Computation (s1 +* (DataPart s2)),i) . f = (Computation s2,i) . f by A43;
thus (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A21, A22, A60, A61, A64, A195, A196, SCMFSA_2:98; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A21, A22, A55, A60, A61, A64, A195, A196, SCMFSA_2:98; :: thesis:

now

let x be set ; :: thesis:
assume A199: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
A200: dom (DataPart p) c= Int-Locations \/ FinSeq-Locations by RELAT_1:87, SCMFSA_2:127;

per cases by A31, A199, A200, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A22, A60, A61, A194, A195, SCMFSA_2:98;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A45, A199; :: thesis:

end;

suppose A201: da = x ; :: thesis:

then consider k1 being Element of NAT such that
A202: ( k1 = abs ((Computation s1,i) . db) & (Computation s1,(i + 1)) . x = ((Computation s1,i) . f) /. k1 ) by A60, A194, SCMFSA_2:98;
consider k2 being Element of NAT such that
A203: ( k2 = abs ((Computation s2,i) . db) & (Computation s2,(i + 1)) . x = ((Computation s2,i) . f) /. k2 ) by A22, A61, A195, A201, SCMFSA_2:98;
DataPart p c= p by RELAT_1:88;
then dom (DataPart p) c= dom p by GRFUNC_1:8;
then ((Computation (s1 +* (DataPart s2)),i) . f) /. k2 = ((Computation s1,i) . f) /. k1 by A2, A9, A10, A31, A194, A197, A199, A201, A202, A203, SCMFSA_3:27;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A48, A198, A199, A202, A203; :: thesis:

end;

suppose A204: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by SCMFSA_2:11;
( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A22, A60, A61, A194, A195, A204, SCMFSA_2:98;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A45, A199; :: thesis:

end;

now

let x be set ; :: thesis:
assume A205: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:

per cases by A37, A205, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider f = x as FinSeq-Location by SCMFSA_2:12;
A206: (Computation (s1 +* (DataPart s2)),(i + 1)) . f = (Computation (s1 +* (DataPart s2)),i) . f by A62, A194, SCMFSA_2:98;
(Computation s2,(i + 1)) . f = (Computation s2,i) . f by A22, A61, A195, SCMFSA_2:98;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A53, A205, A206; :: thesis:

end;

suppose A207: da = x ; :: thesis:

then consider k1 being Element of NAT such that
A208: ( k1 = abs ((Computation (s1 +* (DataPart s2)),i) . db) & (Computation (s1 +* (DataPart s2)),(i + 1)) . x = ((Computation (s1 +* (DataPart s2)),i) . f) /. k1 ) by A62, A194, SCMFSA_2:98;
consider k2 being Element of NAT such that
A209: ( k2 = abs ((Computation s2,i) . db) & (Computation s2,(i + 1)) . x = ((Computation s2,i) . f) /. k2 ) by A22, A61, A195, A207, SCMFSA_2:98;
thus (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A51, A197, A198, A205, A208, A209, SCMFSA_2:127; :: thesis:

end;

suppose A210: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by SCMFSA_2:11;
A211: (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d by A62, A194, A210, SCMFSA_2:98;
(Computation s2,(i + 1)) . d = (Computation s2,i) . d by A22, A61, A195, A210, SCMFSA_2:98;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A53, A205, A211; :: thesis:

end;

suppose InsCode (CurInstr (Computation s1,i)) = 10 ; :: thesis:

then consider db, da being Int-Location , f being FinSeq-Location such that
A212: CurInstr (Computation s1,i) = f,db := da by SCMFSA_2:63;
A213: IncAddr (CurInstr (Computation s1,i)),k = f,db := da by A212, SCMFSA_4:18;
A214: (Exec (CurInstr (Computation s1,i)),(Computation s1,i)) . (IC SCM+FSA ) = Next (IC (Computation s1,i)) by A212, SCMFSA_2:99;
A215: (Computation (s1 +* (DataPart s2)),i) . db = (Computation s2,i) . db by A41;
A216: (Computation (s1 +* (DataPart s2)),i) . da = (Computation s2,i) . da by A41;
A217: (Computation (s1 +* (DataPart s2)),i) . f = (Computation s2,i) . f by A43;
thus (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A21, A22, A60, A61, A64, A213, A214, SCMFSA_2:99; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A21, A22, A55, A60, A61, A64, A213, A214, SCMFSA_2:99; :: thesis:

now

let x be set ; :: thesis:
assume A218: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
A219: dom (DataPart p) c= Int-Locations \/ FinSeq-Locations by RELAT_1:87, SCMFSA_2:127;

per cases by A31, A218, A219, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis:

then reconsider d = x as Int-Location by SCMFSA_2:11;
( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A22, A60, A61, A212, A213, SCMFSA_2:99;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A45, A218; :: thesis:

end;

suppose A220: f = x ; :: thesis:

then consider k1 being Element of NAT such that
A221: ( k1 = abs ((Computation s1,i) . db) & (Computation s1,(i + 1)) . x = ((Computation s1,i) . f) +* k1,((Computation s1,i) . da) ) by A60, A212, SCMFSA_2:99;
consider k2 being Element of NAT such that
A222: ( k2 = abs ((Computation s2,i) . db) & (Computation s2,(i + 1)) . x = ((Computation s2,i) . f) +* k2,((Computation s2,i) . da) ) by A22, A61, A213, A220, SCMFSA_2:99;
DataPart p c= p by RELAT_1:88;
then dom (DataPart p) c= dom p by GRFUNC_1:8;
then ((Computation (s1 +* (DataPart s2)),i) . f) +* k2,((Computation (s1 +* (DataPart s2)),i) . da) = ((Computation s1,i) . f) +* k1,((Computation s1,i) . da) by A2, A9, A10, A31, A212, A215, A218, A220, A221, A222, SCMFSA_3:28;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A48, A216, A217, A218, A221, A222; :: thesis:

end;

suppose A223: ( f <> x & x in FinSeq-Locations ) ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A22, A60, A61, A212, A213, A223, SCMFSA_2:99;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A45, A218; :: thesis:

end;

now

let x be set ; :: thesis:
assume A224: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:

per cases by A37, A224, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis:

then reconsider f = x as Int-Location by SCMFSA_2:11;
A225: (Computation (s1 +* (DataPart s2)),(i + 1)) . f = (Computation (s1 +* (DataPart s2)),i) . f by A62, A212, SCMFSA_2:99;
(Computation s2,(i + 1)) . f = (Computation s2,i) . f by A22, A61, A213, SCMFSA_2:99;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A53, A224, A225; :: thesis:

end;

suppose A226: f = x ; :: thesis:

then consider k1 being Element of NAT such that
A227: ( k1 = abs ((Computation (s1 +* (DataPart s2)),i) . db) & (Computation (s1 +* (DataPart s2)),(i + 1)) . x = ((Computation (s1 +* (DataPart s2)),i) . f) +* k1,((Computation (s1 +* (DataPart s2)),i) . da) ) by A62, A212, SCMFSA_2:99;
consider k2 being Element of NAT such that
A228: ( k2 = abs ((Computation s2,i) . db) & (Computation s2,(i + 1)) . x = ((Computation s2,i) . f) +* k2,((Computation s2,i) . da) ) by A22, A61, A213, A226, SCMFSA_2:99;
thus (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A51, A215, A216, A217, A224, A227, A228, SCMFSA_2:127; :: thesis:

end;

suppose A229: ( f <> x & x in FinSeq-Locations ) ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
A230: (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d by A62, A212, A229, SCMFSA_2:99;
(Computation s2,(i + 1)) . d = (Computation s2,i) . d by A22, A61, A213, A229, SCMFSA_2:99;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A53, A224, A230; :: thesis:

end;

suppose InsCode (CurInstr (Computation s1,i)) = 11 ; :: thesis:

then consider da being Int-Location , f being FinSeq-Location such that
A231: CurInstr (Computation s1,i) = da :=len f by SCMFSA_2:64;
A232: IncAddr (CurInstr (Computation s1,i)),k = da :=len f by A231, SCMFSA_4:19;
A233: (Exec (CurInstr (Computation s1,i)),(Computation s1,i)) . (IC SCM+FSA ) = Next (IC (Computation s1,i)) by A231, SCMFSA_2:100;
A234: (Computation (s1 +* (DataPart s2)),i) . f = (Computation s2,i) . f by A43;
thus (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A21, A22, A60, A61, A64, A232, A233, SCMFSA_2:100; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A21, A22, A55, A60, A61, A64, A232, A233, SCMFSA_2:100; :: thesis:

now

let x be set ; :: thesis:
assume A235: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
A236: dom (DataPart p) c= Int-Locations \/ FinSeq-Locations by RELAT_1:87, SCMFSA_2:127;

per cases by A31, A235, A236, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A22, A60, A61, A231, A232, SCMFSA_2:100;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A45, A235; :: thesis:

end;

suppose A237: da = x ; :: thesis:

then A238: (Computation s1,(i + 1)) . x = len ((Computation s1,i) . f) by A60, A231, SCMFSA_2:100;
A239: (Computation s2,(i + 1)) . x = len ((Computation s2,i) . f) by A22, A61, A232, A237, SCMFSA_2:100;
DataPart p c= p by RELAT_1:88;
then dom (DataPart p) c= dom p by GRFUNC_1:8;
then len ((Computation (s1 +* (DataPart s2)),i) . f) = len ((Computation s1,i) . f) by A2, A9, A10, A31, A231, A235, A237, SCMFSA_3:29;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A48, A234, A235, A238, A239; :: thesis:

end;

suppose A240: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by SCMFSA_2:11;
( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A22, A60, A61, A231, A232, A240, SCMFSA_2:100;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A45, A235; :: thesis:

end;

now

let x be set ; :: thesis:
assume A241: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:

per cases by A37, A241, XBOOLE_0:def 3;

suppose x in FinSeq-Locations ; :: thesis:

then reconsider f = x as FinSeq-Location by SCMFSA_2:12;
A242: (Computation (s1 +* (DataPart s2)),(i + 1)) . f = (Computation (s1 +* (DataPart s2)),i) . f by A62, A231, SCMFSA_2:100;
(Computation s2,(i + 1)) . f = (Computation s2,i) . f by A22, A61, A232, SCMFSA_2:100;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A53, A241, A242; :: thesis:

end;

suppose A243: da = x ; :: thesis:

then A244: (Computation (s1 +* (DataPart s2)),(i + 1)) . x = len ((Computation (s1 +* (DataPart s2)),i) . f) by A62, A231, SCMFSA_2:100;
(Computation s2,(i + 1)) . x = len ((Computation s2,i) . f) by A22, A61, A232, A243, SCMFSA_2:100;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A51, A234, A241, A244, SCMFSA_2:127; :: thesis:

end;

suppose A245: ( da <> x & x in Int-Locations ) ; :: thesis:

then reconsider d = x as Int-Location by SCMFSA_2:11;
A246: (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d by A62, A231, A245, SCMFSA_2:100;
(Computation s2,(i + 1)) . d = (Computation s2,i) . d by A22, A61, A232, A245, SCMFSA_2:100;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A53, A241, A246; :: thesis:

end;

suppose InsCode (CurInstr (Computation s1,i)) = 12 ; :: thesis:

then consider da being Int-Location , f being FinSeq-Location such that
A247: CurInstr (Computation s1,i) = f :=<0,...,0> da by SCMFSA_2:65;
A248: IncAddr (CurInstr (Computation s1,i)),k = f :=<0,...,0> da by A247, SCMFSA_4:20;
A249: (Exec (CurInstr (Computation s1,i)),(Computation s1,i)) . (IC SCM+FSA ) = Next (IC (Computation s1,i)) by A247, SCMFSA_2:101;
A250: (Computation (s1 +* (DataPart s2)),i) . da = (Computation s2,i) . da by A41;
thus (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A21, A22, A60, A61, A64, A248, A249, SCMFSA_2:101; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A21, A22, A55, A60, A61, A64, A248, A249, SCMFSA_2:101; :: thesis:

now

let x be set ; :: thesis:
assume A251: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
A252: dom (DataPart p) c= Int-Locations \/ FinSeq-Locations by RELAT_1:87, SCMFSA_2:127;

per cases by A31, A251, A252, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis:

then reconsider d = x as Int-Location by SCMFSA_2:11;
( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A22, A60, A61, A247, A248, SCMFSA_2:101;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A45, A251; :: thesis:

end;

suppose A253: f = x ; :: thesis:

then consider k1 being Element of NAT such that
A254: ( k1 = abs ((Computation s1,i) . da) & (Computation s1,(i + 1)) . x = k1 |-> 0 ) by A60, A247, SCMFSA_2:101;
consider k2 being Element of NAT such that
A255: ( k2 = abs ((Computation s2,i) . da) & (Computation s2,(i + 1)) . x = k2 |-> 0 ) by A22, A61, A248, A253, SCMFSA_2:101;
DataPart p c= p by RELAT_1:88;
then dom (DataPart p) c= dom p by GRFUNC_1:8;
then k2 |-> 0 = k1 |-> 0 by A2, A9, A10, A31, A247, A250, A251, A253, A254, A255, SCMFSA_3:30;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A48, A251, A254, A255; :: thesis:

end;

suppose A256: ( f <> x & x in FinSeq-Locations ) ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A22, A60, A61, A247, A248, A256, SCMFSA_2:101;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A31, A45, A251; :: thesis:

end;

now

let x be set ; :: thesis:
assume A257: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:

per cases by A37, A257, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis:

then reconsider f = x as Int-Location by SCMFSA_2:11;
A258: (Computation (s1 +* (DataPart s2)),(i + 1)) . f = (Computation (s1 +* (DataPart s2)),i) . f by A62, A247, SCMFSA_2:101;
(Computation s2,(i + 1)) . f = (Computation s2,i) . f by A22, A61, A248, SCMFSA_2:101;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A53, A257, A258; :: thesis:

end;

suppose A259: f = x ; :: thesis:

then consider k1 being Element of NAT such that
A260: ( k1 = abs ((Computation (s1 +* (DataPart s2)),i) . da) & (Computation (s1 +* (DataPart s2)),(i + 1)) . x = k1 |-> 0 ) by A62, A247, SCMFSA_2:101;
consider k2 being Element of NAT such that
A261: ( k2 = abs ((Computation s2,i) . da) & (Computation s2,(i + 1)) . x = k2 |-> 0 ) by A22, A61, A248, A259, SCMFSA_2:101;
thus (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A51, A250, A257, A260, A261, SCMFSA_2:127; :: thesis:

end;

suppose A262: ( f <> x & x in FinSeq-Locations ) ; :: thesis:

then reconsider d = x as FinSeq-Location by SCMFSA_2:12;
A263: (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d by A62, A247, A262, SCMFSA_2:101;
(Computation s2,(i + 1)) . d = (Computation s2,i) . d by A22, A61, A248, A262, SCMFSA_2:101;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A53, A257, A263; :: thesis:

end;

thus for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A19, A20); :: thesis: