let k be Element of NAT ; :: thesis:
let p be autonomic FinPartState of ; :: thesis:
let s1, s2 be State of ; :: thesis:
assume that
A1: IC SCM in dom p and
A2: p c= s1 and
A3: Relocated p,k c= s2 ; :: thesis:
set s3 = s1 +* (DataPart s2);
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) );
A4: not p is NAT -defined by A1, AMI_1:109;
A5: p c= s1 +* (DataPart s2) by A2, A3, Th30;

now

set DPp = DataPart p;
let i be Element of NAT ; :: thesis:
assume that
A6: (IC (Computation s1,i)) + k = IC (Computation s2,i) and
A7: IncAddr (CurInstr (Computation s1,i)),k = CurInstr (Computation s2,i) and
A8: (Computation s1,i) | (dom (DataPart p)) = (Computation s2,i) | (dom (DataPart (Relocated p,k))) and
A9: DataPart (Computation (s1 +* (DataPart s2)),i) = DataPart (Computation s2,i) ; :: thesis:
set Cs2i1 = Computation s2,(i + 1);
set Cs3i = Computation (s1 +* (DataPart s2)),i;
set Cs2i = Computation s2,i;
A10: dom (Computation s2,(i + 1)) = ({(IC SCM )} \/ SCM-Data-Loc ) \/ NAT by AMI_1:79, AMI_5:23;
set Cs3i1 = Computation (s1 +* (DataPart s2)),(i + 1);
A11: dom (DataPart (Computation s2,i)) = SCM-Data-Loc by AMI_3:72, SCMNORM:14;
A12: dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) = SCM-Data-Loc by AMI_3:72, SCMNORM:14;
A13: dom (DataPart (Computation s2,(i + 1))) = SCM-Data-Loc by AMI_3:72, SCMNORM:14;

A14: now

let x be set ; :: thesis:
assume that
A15: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) and
A16: (Computation (s1 +* (DataPart s2)),(i + 1)) . x = (Computation s2,(i + 1)) . x ; :: thesis:
thus (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (Computation s2,(i + 1)) . x by A15, A16, FUNCT_1:70
.= (DataPart (Computation s2,(i + 1))) . x by A12, A13, A15, FUNCT_1:70 ; :: thesis:

end;

A17: dom (DataPart (Computation (s1 +* (DataPart s2)),i)) = SCM-Data-Loc by AMI_3:72, SCMNORM:14;

A18: now

let x be set ; :: thesis:
assume that
A19: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) and
A20: ( (Computation (s1 +* (DataPart s2)),(i + 1)) . x = (Computation (s1 +* (DataPart s2)),i) . x & (Computation s2,(i + 1)) . x = (Computation s2,i) . x ) ; :: thesis:
(DataPart (Computation (s1 +* (DataPart s2)),i)) . x = (Computation (s1 +* (DataPart s2)),i) . x by A17, A12, A19, FUNCT_1:70;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A9, A11, A12, A14, A19, A20, FUNCT_1:70; :: thesis:

end;

A21: now

let s be State of ; :: thesis:
let d be Data-Location ; :: thesis:
d in SCM-Data-Loc by AMI_3:def 2;
hence d in dom (DataPart s) by AMI_3:72, SCMNORM:14; :: thesis:

end;

A22: now

let d be Data-Location ; :: thesis:
A23: d in dom (DataPart (Computation (s1 +* (DataPart s2)),i)) by A21;
hence (Computation (s1 +* (DataPart s2)),i) . d = (DataPart (Computation (s1 +* (DataPart s2)),i)) . d by FUNCT_1:70
.= (Computation s2,i) . d by A9, A23, FUNCT_1:70 ;
:: thesis:

end;

set Cs1i1 = Computation s1,(i + 1);
set Cs1i = Computation s1,i;
A24: dom (Computation s1,(i + 1)) = ({(IC SCM )} \/ SCM-Data-Loc ) \/ NAT by AMI_1:79, AMI_5:23;
dom (DataPart p) = (dom p) /\ SCM-Data-Loc by AMI_3:72, RELAT_1:90;
then A25: dom (DataPart p) c= {(IC SCM )} \/ SCM-Data-Loc by XBOOLE_1:10, XBOOLE_1:17;
A26: dom ((Computation s1,(i + 1)) | (dom (DataPart p))) = (dom (Computation s1,(i + 1))) /\ (dom (DataPart p)) by RELAT_1:90
.= dom (DataPart p) by A24, A25, XBOOLE_1:10, XBOOLE_1:28 ;

A27: now

reconsider loc = IC (Computation s1,(i + 1)) as Instruction-Location of SCM ;
assume A28: (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) ; :: thesis:
reconsider kk = loc as Element of NAT by ORDINAL1:def 13;
A29: loc in dom (ProgramPart p) by A2, A4, AMI_5:86;
ProgramPart p c= p by RELAT_1:88;
then A30: dom (ProgramPart p) c= dom p by GRFUNC_1:8;
then loc + k in dom (Relocated p,k) by A29, Th24;
then A31: (Relocated p,k) . (loc + k) = s2 . (loc + k) by A3, GRFUNC_1:8
.= (Computation s2,(i + 1)) . (kk + k) by AMI_1:54 ;
CurInstr (Computation s1,(i + 1)) = s1 . loc by AMI_1:54
.= p . loc by A2, A29, A30, GRFUNC_1:8 ;
hence IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A28, A29, A31, Th27; :: thesis:

end;

set I = CurInstr (Computation s1,i);
A32: Computation s2,(i + 1) = Following (Computation s2,i) by AMI_1:14
.= Exec (CurInstr (Computation s2,i)),(Computation s2,i) ;
A33: dom (Computation s2,i) = ({(IC SCM )} \/ SCM-Data-Loc ) \/ NAT by AMI_1:79, AMI_5:23;
A34: dom (Computation s1,i) = ({(IC SCM )} \/ SCM-Data-Loc ) \/ NAT by AMI_1:79, AMI_5:23;
A35: dom ((Computation s1,i) | (dom (DataPart p))) = (dom (Computation s1,i)) /\ (dom (DataPart p)) by RELAT_1:90
.= dom (DataPart p) by A34, A25, XBOOLE_1:10, XBOOLE_1:28 ;
A36: 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, A4, A5, AMI_5:87 ;
A37: dom (DataPart p) = dom (DataPart (Relocated p,k)) by Th21;
then A38: dom ((Computation s2,(i + 1)) | (dom (DataPart (Relocated p,k)))) = (dom (Computation s2,(i + 1))) /\ (dom (DataPart p)) by RELAT_1:90
.= dom (DataPart p) by A10, A25, XBOOLE_1:10, XBOOLE_1:28 ;

A39: now

let x be set ; :: thesis:
let d be Data-Location ; :: thesis:
assume that
A40: ( d = x & d in dom (DataPart p) ) and
A41: (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 A26, A40, A41, FUNCT_1:70
.= ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A37, A38, A40, FUNCT_1:70 ; :: thesis:

end;

A42: dom ((Computation s2,i) | (dom (DataPart (Relocated p,k)))) = (dom (Computation s2,i)) /\ (dom (DataPart p)) by A37, RELAT_1:90
.= dom (DataPart p) by A33, A25, XBOOLE_1:10, XBOOLE_1:28 ;

A43: now

let x be set ; :: thesis:
let d be Data-Location ; :: thesis:
assume that
A44: d = x and
A45: d in dom (DataPart p) and
A46: ( (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 A37, A35, A42, A45, FUNCT_1:70;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = (Computation s2,(i + 1)) . d by A8, A37, A26, A44, A45, A46, FUNCT_1:70
.= ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A37, A38, A44, A45, FUNCT_1:70 ;
:: thesis:

end;

reconsider j = IC (Computation s1,i) as Element of NAT by ORDINAL1:def 13;
A47: Computation s1,(i + 1) = Following (Computation s1,i) by AMI_1:14
.= Exec (CurInstr (Computation s1,i)),(Computation s1,i) ;
A48: Next ((IC (Computation s1,i)) + k) = il. ((j + k) + 1) by NAT_1:39
.= (il. (j + 1)) + k
.= (Next (IC (Computation s1,i))) + k by NAT_1:39 ;

per cases by AMI_5:36, NAT_1:33;

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

then A49: CurInstr (Computation s1,i) = halt SCM by AMI_5:46;
then A50: CurInstr (Computation s2,i) = halt SCM by A7, Def3, AMI_5:37;
thus (IC (Computation s1,(i + 1))) + k = (IC (Computation s1,i)) + k by A47, A49, AMI_1:def 8
.= IC (Computation s2,(i + 1)) by A6, A32, A50, AMI_1:def 8 ; :: thesis:
hence IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A27; :: thesis:
A51: Computation s2,(i + 1) = Computation s2,i by A32, A50, AMI_1:def 8;
hence (Computation s1,(i + 1)) | (dom (DataPart p)) = (Computation s2,(i + 1)) | (dom (DataPart (Relocated p,k))) by A8, A47, A49, AMI_1:def 8; :: thesis:
thus DataPart (Computation (s1 +* (DataPart s2)),(i + 1)) = DataPart (Computation s2,(i + 1)) by A9, A36, A49, A51, AMI_1:def 8; :: thesis:

end;

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

then consider da, db being Data-Location such that
A52: CurInstr (Computation s1,i) = da := db by AMI_5:47;
A53: IncAddr (CurInstr (Computation s1,i)),k = da := db by A52, Th5;
A54: (Exec (CurInstr (Computation s1,i)),(Computation s1,i)) . (IC SCM ) = Next (IC (Computation s1,i)) by A52, AMI_3:8;
hence (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A6, A7, A47, A32, A48, A53, AMI_3:8; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A6, A7, A27, A47, A32, A48, A53, A54, AMI_3:8; :: thesis:
A55: (Computation (s1 +* (DataPart s2)),i) . db = (Computation s2,i) . db by A22;

now

DataPart p c= p by RELAT_1:88;
then A56: dom (DataPart p) c= dom p by GRFUNC_1:8;
let x be set ; :: thesis:
assume A57: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= SCM-Data-Loc by AMI_3:72, RELAT_1:87;
then x in SCM-Data-Loc by A26, A57;
then reconsider d = x as Data-Location by AMI_3:def 2;

per cases ;

suppose A58: da = d ; :: thesis:

then ( (Computation s1,(i + 1)) . d = (Computation s1,i) . db & (Computation s2,(i + 1)) . d = (Computation s2,i) . db ) by A7, A47, A32, A52, A53, AMI_3:8;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A2, A4, A5, A26, A39, A52, A55, A57, A56, A58, AMI_5:88; :: thesis:

end;

suppose da <> d ; :: thesis:

then ( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A7, A47, A32, A52, A53, AMI_3:8;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A26, A43, A57; :: thesis:

end;

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

now

let x be set ; :: thesis:
assume A59: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:
then reconsider d = x as Data-Location by A12, AMI_3:def 2;

per cases ;

suppose da = d ; :: thesis:

then ( (Computation s2,(i + 1)) . d = (Computation s2,i) . db & (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . db ) by A7, A32, A36, A52, A53, AMI_3:8;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A22, A14, A59; :: thesis:

end;

suppose da <> d ; :: thesis:

then ( (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A7, A32, A36, A52, A53, AMI_3:8;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A18, A59; :: thesis:

end;

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

end;

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

then consider da, db being Data-Location such that
A60: CurInstr (Computation s1,i) = AddTo da,db by AMI_5:48;
A61: IncAddr (CurInstr (Computation s1,i)),k = AddTo da,db by A60, Th6;
A62: (Exec (CurInstr (Computation s1,i)),(Computation s1,i)) . (IC SCM ) = Next (IC (Computation s1,i)) by A60, AMI_3:9;
hence (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A6, A7, A47, A32, A48, A61, AMI_3:9; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A6, A7, A27, A47, A32, A48, A61, A62, AMI_3:9; :: thesis:
A63: ( (Computation (s1 +* (DataPart s2)),i) . da = (Computation s2,i) . da & (Computation (s1 +* (DataPart s2)),i) . db = (Computation s2,i) . db ) by A22;

now

DataPart p c= p by RELAT_1:88;
then A64: dom (DataPart p) c= dom p by GRFUNC_1:8;
let x be set ; :: thesis:
assume A65: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= SCM-Data-Loc by AMI_3:72, RELAT_1:87;
then x in SCM-Data-Loc by A26, A65;
then reconsider d = x as Data-Location by AMI_3:def 2;

per cases ;

suppose A66: da = d ; :: thesis:

then ( (Computation s1,(i + 1)) . d = ((Computation s1,i) . da) + ((Computation s1,i) . db) & (Computation s2,(i + 1)) . d = ((Computation s2,i) . da) + ((Computation s2,i) . db) ) by A7, A47, A32, A60, A61, AMI_3:9;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A2, A4, A5, A26, A39, A60, A63, A65, A64, A66, AMI_5:89; :: thesis:

end;

suppose da <> d ; :: thesis:

then ( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A7, A47, A32, A60, A61, AMI_3:9;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A26, A43, A65; :: thesis:

end;

now

let x be set ; :: thesis:
assume A67: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:
then reconsider d = x as Data-Location by A12, AMI_3:def 2;

per cases ;

suppose da = d ; :: thesis:

then ( (Computation s2,(i + 1)) . d = ((Computation s2,i) . da) + ((Computation s2,i) . db) & (Computation (s1 +* (DataPart s2)),(i + 1)) . d = ((Computation (s1 +* (DataPart s2)),i) . da) + ((Computation (s1 +* (DataPart s2)),i) . db) ) by A7, A32, A36, A60, A61, AMI_3:9;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A14, A63, A67; :: thesis:

end;

suppose da <> d ; :: thesis:

then ( (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A7, A32, A36, A60, A61, AMI_3:9;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A18, A67; :: thesis:

end;

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

then consider da, db being Data-Location such that
A68: CurInstr (Computation s1,i) = SubFrom da,db by AMI_5:49;
A69: IncAddr (CurInstr (Computation s1,i)),k = SubFrom da,db by A68, Th7;
A70: (Exec (CurInstr (Computation s1,i)),(Computation s1,i)) . (IC SCM ) = Next (IC (Computation s1,i)) by A68, AMI_3:10;
hence (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A6, A7, A47, A32, A48, A69, AMI_3:10; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A6, A7, A27, A47, A32, A48, A69, A70, AMI_3:10; :: thesis:
A71: ( (Computation (s1 +* (DataPart s2)),i) . da = (Computation s2,i) . da & (Computation (s1 +* (DataPart s2)),i) . db = (Computation s2,i) . db ) by A22;

now

DataPart p c= p by RELAT_1:88;
then A72: dom (DataPart p) c= dom p by GRFUNC_1:8;
let x be set ; :: thesis:
assume A73: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= SCM-Data-Loc by AMI_3:72, RELAT_1:87;
then x in SCM-Data-Loc by A26, A73;
then reconsider d = x as Data-Location by AMI_3:def 2;

per cases ;

suppose A74: da = d ; :: thesis:

then ( (Computation s1,(i + 1)) . d = ((Computation s1,i) . da) - ((Computation s1,i) . db) & (Computation s2,(i + 1)) . d = ((Computation s2,i) . da) - ((Computation s2,i) . db) ) by A7, A47, A32, A68, A69, AMI_3:10;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A2, A4, A5, A26, A39, A68, A71, A73, A72, A74, AMI_5:90; :: thesis:

end;

suppose da <> d ; :: thesis:

then ( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A7, A47, A32, A68, A69, AMI_3:10;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A26, A43, A73; :: thesis:

end;

now

let x be set ; :: thesis:
assume A75: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:
then reconsider d = x as Data-Location by A12, AMI_3:def 2;

per cases ;

suppose da = d ; :: thesis:

then ( (Computation s2,(i + 1)) . d = ((Computation s2,i) . da) - ((Computation s2,i) . db) & (Computation (s1 +* (DataPart s2)),(i + 1)) . d = ((Computation (s1 +* (DataPart s2)),i) . da) - ((Computation (s1 +* (DataPart s2)),i) . db) ) by A7, A32, A36, A68, A69, AMI_3:10;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A14, A71, A75; :: thesis:

end;

suppose da <> d ; :: thesis:

then ( (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A7, A32, A36, A68, A69, AMI_3:10;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A18, A75; :: thesis:

end;

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

then consider da, db being Data-Location such that
A76: CurInstr (Computation s1,i) = MultBy da,db by AMI_5:50;
A77: IncAddr (CurInstr (Computation s1,i)),k = MultBy da,db by A76, Th8;
A78: (Exec (CurInstr (Computation s1,i)),(Computation s1,i)) . (IC SCM ) = Next (IC (Computation s1,i)) by A76, AMI_3:11;
hence (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A6, A7, A47, A32, A48, A77, AMI_3:11; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A6, A7, A27, A47, A32, A48, A77, A78, AMI_3:11; :: thesis:
A79: ( (Computation (s1 +* (DataPart s2)),i) . da = (Computation s2,i) . da & (Computation (s1 +* (DataPart s2)),i) . db = (Computation s2,i) . db ) by A22;

now

DataPart p c= p by RELAT_1:88;
then A80: dom (DataPart p) c= dom p by GRFUNC_1:8;
let x be set ; :: thesis:
assume A81: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= SCM-Data-Loc by AMI_3:72, RELAT_1:87;
then x in SCM-Data-Loc by A26, A81;
then reconsider d = x as Data-Location by AMI_3:def 2;

per cases ;

suppose A82: da = d ; :: thesis:

then ( (Computation s1,(i + 1)) . d = ((Computation s1,i) . da) * ((Computation s1,i) . db) & (Computation s2,(i + 1)) . d = ((Computation s2,i) . da) * ((Computation s2,i) . db) ) by A7, A47, A32, A76, A77, AMI_3:11;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A2, A4, A5, A26, A39, A76, A79, A81, A80, A82, AMI_5:91; :: thesis:

end;

suppose da <> d ; :: thesis:

then ( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A7, A47, A32, A76, A77, AMI_3:11;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A26, A43, A81; :: thesis:

end;

now

let x be set ; :: thesis:
assume A83: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:
then reconsider d = x as Data-Location by A12, AMI_3:def 2;

per cases ;

suppose da = d ; :: thesis:

then ( (Computation s2,(i + 1)) . d = ((Computation s2,i) . da) * ((Computation s2,i) . db) & (Computation (s1 +* (DataPart s2)),(i + 1)) . d = ((Computation (s1 +* (DataPart s2)),i) . da) * ((Computation (s1 +* (DataPart s2)),i) . db) ) by A7, A32, A36, A76, A77, AMI_3:11;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A14, A79, A83; :: thesis:

end;

suppose da <> d ; :: thesis:

then ( (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A7, A32, A36, A76, A77, AMI_3:11;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A18, A83; :: thesis:

end;

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

then consider da, db being Data-Location such that
A84: CurInstr (Computation s1,i) = Divide da,db by AMI_5:51;
A85: IncAddr (CurInstr (Computation s1,i)),k = Divide da,db by A84, Th9;
A86: ( (Computation (s1 +* (DataPart s2)),i) . da = (Computation s2,i) . da & (Computation (s1 +* (DataPart s2)),i) . db = (Computation s2,i) . db ) by A22;

now

per cases ;

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

A88: (Exec (CurInstr (Computation s1,i)),(Computation s1,i)) . (IC SCM ) = Next (IC (Computation s1,i)) by A84, AMI_3:12;
hence (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A6, A7, A47, A32, A48, A85, AMI_3:12; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A6, A7, A27, A47, A32, A48, A85, A88, AMI_3:12; :: thesis:

now

DataPart p c= p by RELAT_1:88;
then A89: dom (DataPart p) c= dom p by GRFUNC_1:8;
let x be set ; :: thesis:
assume A90: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= SCM-Data-Loc by AMI_3:72, RELAT_1:87;
then x in SCM-Data-Loc by A26, A90;
then reconsider d = x as Data-Location by AMI_3:def 2;

per cases ;

suppose A91: da = d ; :: thesis:

then A92: ( (Computation s1,(i + 1)) . d = ((Computation s1,i) . da) div ((Computation s1,i) . db) & (Computation s2,(i + 1)) . d = ((Computation s2,i) . da) div ((Computation s2,i) . db) ) by A7, A47, A32, A84, A85, A87, AMI_3:12;
((Computation (s1 +* (DataPart s2)),i) . da) div ((Computation (s1 +* (DataPart s2)),i) . db) = ((Computation s1,i) . da) div ((Computation s1,i) . db) by A2, A4, A5, A26, A84, A87, A90, A89, A91, AMI_5:92;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = (Computation s2,(i + 1)) . d by A86, A90, A92, FUNCT_1:70
.= ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A37, A26, A38, A90, FUNCT_1:70 ;
:: thesis:

end;

suppose A93: db = d ; :: thesis:

then ( (Computation s1,(i + 1)) . d = ((Computation s1,i) . da) mod ((Computation s1,i) . db) & (Computation s2,(i + 1)) . d = ((Computation s2,i) . da) mod ((Computation s2,i) . db) ) by A7, A47, A32, A84, A85, AMI_3:12;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A2, A4, A5, A26, A39, A84, A86, A90, A89, A93, AMI_5:93; :: thesis:

end;

suppose ( da <> d & db <> d ) ; :: thesis:

then ( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A7, A47, A32, A84, A85, AMI_3:12;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A26, A43, A90; :: thesis:

end;

now

let x be set ; :: thesis:
assume A94: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:
then reconsider d = x as Data-Location by A12, AMI_3:def 2;

per cases ;

suppose da = d ; :: thesis:

then ( (Computation s2,(i + 1)) . d = ((Computation s2,i) . da) div ((Computation s2,i) . db) & (Computation (s1 +* (DataPart s2)),(i + 1)) . d = ((Computation (s1 +* (DataPart s2)),i) . da) div ((Computation (s1 +* (DataPart s2)),i) . db) ) by A7, A32, A36, A84, A85, A87, AMI_3:12;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A14, A86, A94; :: thesis:

end;

suppose db = d ; :: thesis:

then ( (Computation s2,(i + 1)) . d = ((Computation s2,i) . da) mod ((Computation s2,i) . db) & (Computation (s1 +* (DataPart s2)),(i + 1)) . d = ((Computation (s1 +* (DataPart s2)),i) . da) mod ((Computation (s1 +* (DataPart s2)),i) . db) ) by A7, A32, A36, A84, A85, AMI_3:12;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A14, A86, A94; :: thesis:

end;

suppose ( da <> d & db <> d ) ; :: thesis:

then ( (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A7, A32, A36, A84, A85, AMI_3:12;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A18, A94; :: thesis:

end;

suppose A95: da = db ; :: thesis:

A96: (Exec (CurInstr (Computation s1,i)),(Computation s1,i)) . (IC SCM ) = Next (IC (Computation s1,i)) by A84, AMI_3:12;
hence (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A6, A7, A47, A32, A48, A85, AMI_3:12; :: thesis:
thus IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A6, A7, A27, A47, A32, A48, A85, A96, AMI_3:12; :: thesis:

now

let x be set ; :: thesis:
assume A97: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= SCM-Data-Loc by AMI_3:72, RELAT_1:87;
then x in SCM-Data-Loc by A26, A97;
then reconsider d = x as Data-Location by AMI_3:def 2;

per cases ;

suppose A98: da = d ; :: thesis:

A99: ( ((Computation s1,i) | (dom (DataPart p))) . d = (Computation s1,i) . d & ((Computation s2,i) | (dom (DataPart p))) . d = (Computation s2,i) . d ) by A37, A26, A35, A42, A97, FUNCT_1:70;
A100: ( ((Computation s1,(i + 1)) | (dom (DataPart p))) . d = (Computation s1,(i + 1)) . d & ((Computation s2,(i + 1)) | (dom (DataPart p))) . d = (Computation s2,(i + 1)) . d ) by A37, A26, A38, A97, FUNCT_1:70;
(Computation s2,(i + 1)) . d = ((Computation s2,i) . da) mod ((Computation s2,i) . db) by A7, A32, A85, A95, A98, AMI_3:12;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A8, A37, A47, A84, A95, A98, A99, A100, AMI_3:12; :: thesis:

end;

suppose da <> d ; :: thesis:

then ( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A7, A47, A32, A84, A85, A95, AMI_3:12;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A26, A43, A97; :: thesis:

end;

now

let x be set ; :: thesis:
assume A101: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:
then reconsider d = x as Data-Location by A12, AMI_3:def 2;

per cases ;

suppose da = d ; :: thesis:

then ( (Computation s2,(i + 1)) . d = ((Computation s2,i) . da) mod ((Computation s2,i) . db) & (Computation (s1 +* (DataPart s2)),(i + 1)) . d = ((Computation (s1 +* (DataPart s2)),i) . da) mod ((Computation (s1 +* (DataPart s2)),i) . db) ) by A7, A32, A36, A84, A85, A95, AMI_3:12;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A14, A86, A101; :: thesis:

end;

suppose da <> d ; :: thesis:

then ( (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A7, A32, A36, A84, A85, A95, AMI_3:12;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A18, A101; :: thesis:

end;

hence ( (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) & IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) & (Computation s1,(i + 1)) | (dom (DataPart p)) = (Computation s2,(i + 1)) | (dom (DataPart (Relocated p,k))) & DataPart (Computation (s1 +* (DataPart s2)),(i + 1)) = DataPart (Computation s2,(i + 1)) ) ; :: thesis:

end;

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

then consider loc being Instruction-Location of SCM such that
A102: CurInstr (Computation s1,i) = goto loc by AMI_5:52;
A103: CurInstr (Computation s2,i) = goto (loc + k) by A7, A102, Th10;
thus (IC (Computation s1,(i + 1))) + k = loc + k by A47, A102, AMI_3:13
.= IC (Computation s2,(i + 1)) by A32, A103, AMI_3:13 ; :: thesis:
hence IncAddr (CurInstr (Computation s1,(i + 1))),k = CurInstr (Computation s2,(i + 1)) by A27; :: thesis:

now

let x be set ; :: thesis:
assume A104: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= SCM-Data-Loc by AMI_3:72, RELAT_1:87;
then x in SCM-Data-Loc by A26, A104;
then reconsider d = x as Data-Location by AMI_3:def 2;
( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A47, A32, A102, A103, AMI_3:13;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A26, A43, A104; :: thesis:

end;

now

let x be set ; :: thesis:
assume A105: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:
then reconsider d = x as Data-Location by A12, AMI_3:def 2;
( (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A32, A36, A102, A103, AMI_3:13;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A18, A105; :: thesis:

end;

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

then consider loc being Instruction-Location of SCM , da being Data-Location such that
A106: CurInstr (Computation s1,i) = da =0_goto loc by AMI_5:53;

A107: 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 A47, A106, AMI_3:14; :: thesis:

end;

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

hence (IC (Computation s1,(i + 1))) + k = Next (IC (Computation s2,i)) by A6, A47, A48, A106, AMI_3:14; :: thesis:

end;

A108: CurInstr (Computation s2,i) = da =0_goto (loc + k) by A7, A106, Th11;

A109: 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 A32, A108, AMI_3:14; :: thesis:

end;

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

hence IC (Computation s2,(i + 1)) = Next (IC (Computation s2,i)) by A32, A108, AMI_3:14; :: thesis:

end;

A110: (Computation (s1 +* (DataPart s2)),i) . da = (Computation s2,i) . da by A22;

A111: 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, A4, A5, A106, A110, A107, A109, AMI_5:94; :: thesis:

end;

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

hence (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A6, A48, A107, A109; :: 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 A27, A111; :: thesis:

now

let x be set ; :: thesis:
assume A112: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= SCM-Data-Loc by AMI_3:72, RELAT_1:87;
then x in SCM-Data-Loc by A26, A112;
then reconsider d = x as Data-Location by AMI_3:def 2;
( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A47, A32, A106, A108, AMI_3:14;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A26, A43, A112; :: thesis:

end;

now

let x be set ; :: thesis:
assume A113: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:
then reconsider d = x as Data-Location by A12, AMI_3:def 2;
( (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A32, A36, A106, A108, AMI_3:14;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A18, A113; :: thesis:

end;

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

then consider loc being Instruction-Location of SCM , da being Data-Location such that
A114: CurInstr (Computation s1,i) = da >0_goto loc by AMI_5:54;

A115: 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 A47, A114, AMI_3:15; :: thesis:

end;

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

hence (IC (Computation s1,(i + 1))) + k = Next (IC (Computation s2,i)) by A6, A47, A48, A114, AMI_3:15; :: thesis:

end;

A116: CurInstr (Computation s2,i) = da >0_goto (loc + k) by A7, A114, Th12;

A117: 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 A32, A116, AMI_3:15; :: thesis:

end;

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

hence IC (Computation s2,(i + 1)) = Next (IC (Computation s2,i)) by A32, A116, AMI_3:15; :: thesis:

end;

A118: (Computation (s1 +* (DataPart s2)),i) . da = (Computation s2,i) . da by A22;

A119: 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, A4, A5, A114, A118, A115, A117, AMI_5:95; :: thesis:

end;

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

hence (IC (Computation s1,(i + 1))) + k = IC (Computation s2,(i + 1)) by A6, A48, A115, A117; :: 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 A27, A119; :: thesis:

now

let x be set ; :: thesis:
assume A120: x in dom ((Computation s1,(i + 1)) | (dom (DataPart p))) ; :: thesis:
dom (DataPart p) c= SCM-Data-Loc by AMI_3:72, RELAT_1:87;
then x in SCM-Data-Loc by A26, A120;
then reconsider d = x as Data-Location by AMI_3:def 2;
( (Computation s1,(i + 1)) . d = (Computation s1,i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A47, A32, A114, A116, AMI_3:15;
hence ((Computation s1,(i + 1)) | (dom (DataPart p))) . x = ((Computation s2,(i + 1)) | (dom (DataPart p))) . x by A26, A43, A120; :: thesis:

end;

now

let x be set ; :: thesis:
assume A121: x in dom (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) ; :: thesis:
then reconsider d = x as Data-Location by A12, AMI_3:def 2;
( (Computation (s1 +* (DataPart s2)),(i + 1)) . d = (Computation (s1 +* (DataPart s2)),i) . d & (Computation s2,(i + 1)) . d = (Computation s2,i) . d ) by A32, A36, A114, A116, AMI_3:15;
hence (DataPart (Computation (s1 +* (DataPart s2)),(i + 1))) . x = (DataPart (Computation s2,(i + 1))) . x by A18, A121; :: thesis:

end;

then A122: for i being Element of NAT st S₁[i] holds
S₁[i + 1] ;
A123: DataPart p c= p by RELAT_1:88;
A124: DataPart (Relocated p,k) c= Relocated p,k by RELAT_1:88;
A125: DataPart p = DataPart (Relocated p,k) by Th21;
A126: IC SCM in dom (Relocated p,k) by Th25;

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 Th26
.= IC s2 by A3, A126, AMI_1:97
.= IC (Computation s2,0 ) by AMI_1:13 ; :: thesis:
reconsider loc = IC p as Element of NAT by ORDINAL1:def 13;
A127: IncAddr (CurInstr (Computation s1,0 )),k = IncAddr (CurInstr s1),k by AMI_1:13
.= IncAddr (s1 . (IC s1)),k ;
A128: IC p = IC s1 by A1, A2, AMI_1:97;
then IC p = IC (Computation s1,0 ) by AMI_1:13;
then A129: loc in dom (ProgramPart p) by A2, A4, AMI_5:86;
ProgramPart p c= p by RELAT_1:88;
then A130: dom (ProgramPart p) c= dom p by GRFUNC_1:8;
then A131: (IC p) + k in dom (Relocated p,k) by A129, Th24;
A132: IC SCM in dom (Relocated p,k) by Th25;
A133: p . (IC p) = s1 . (IC s1) by A2, A128, A129, A130, GRFUNC_1:8;
CurInstr (Computation s2,0 ) = CurInstr s2 by AMI_1:13
.= s2 . (IC (Relocated p,k)) by A3, A132, AMI_1:97
.= s2 . ((IC p) + k) by Th26
.= (Relocated p,k) . ((IC p) + k) by A3, A131, GRFUNC_1:8 ;
hence IncAddr (CurInstr (Computation s1,0 )),k = CurInstr (Computation s2,0 ) by A129, A133, A127, Th27; :: thesis:
A134: dom (DataPart s2) = SCM-Data-Loc by AMI_3:72, SCMNORM:14;
thus (Computation s1,0 ) | (dom (DataPart p)) = s1 | (dom (DataPart p)) by AMI_1:13
.= DataPart p by A2, A123, GRFUNC_1:64, XBOOLE_1:1
.= s2 | (dom (DataPart p)) by A3, A125, A124, GRFUNC_1:64, XBOOLE_1:1
.= (Computation s2,0 ) | (dom (DataPart (Relocated p,k))) by A125, AMI_1:13 ; :: thesis:
thus DataPart (Computation (s1 +* (DataPart s2)),0 ) = DataPart (s1 +* (DataPart s2)) by AMI_1:13
.= DataPart s2 by A134, AMI_3:72, FUNCT_4:24
.= DataPart (Computation s2,0 ) by AMI_1:13 ; :: thesis:

end;

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