let k be Element of NAT ; :: thesis:
let R be good Ring; :: thesis:
let s be State of (SCM R); :: thesis:
set INS = CurInstr (ProgramPart s),s;
consider m being natural number such that
A1: IC s = m ;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
A3: succ (IC (s +* (Start-At ((IC s) + k),(SCM R)))) = succ ((IC s) + k) by FUNCT_4:121
.= IC ((Exec (CurInstr (ProgramPart s),s),s) +* (Start-At ((succ (IC s)) + k),(SCM R))) by FUNCT_4:121 ;

A4: now

let d be Element of NAT ; :: thesis:
thus (Exec (CurInstr (ProgramPart s),s),(s +* (Start-At ((IC s) + k),(SCM R)))) . d = (s +* (Start-At ((IC s) + k),(SCM R))) . d by AMI_1:def 13
.= s . d by COMPOS_1:20
.= (Exec (CurInstr (ProgramPart s),s),s) . d by AMI_1:def 13
.= ((Exec (CurInstr (ProgramPart s),s),s) +* (Start-At ((succ (IC s)) + k),(SCM R))) . d by COMPOS_1:20 ; :: thesis:

end;

per cases by NAT_1:32, SCMRING3:71;

suppose InsCode (CurInstr (ProgramPart s),s) = 0 ; :: thesis:

then A5: CurInstr (ProgramPart s),s = halt (SCM R) by SCMRING3:16;
then A6: Following (ProgramPart s),s = s by AMI_1:def 8;
thus Exec (IncAddr (CurInstr (ProgramPart s),s),k),(s +* (Start-At ((IC s) + k),(SCM R))) = (Following (ProgramPart s),s) +* (Start-At ((IC (Following (ProgramPart s),s)) + k),(SCM R)) by A6, A5, AMI_1:def 8; :: thesis:

end;

suppose InsCode (CurInstr (ProgramPart s),s) = 1 ; :: thesis:

then consider da, db being Data-Location of R such that
A7: CurInstr (ProgramPart s),s = da := db by SCMRING3:17;

A8: now

let d be Data-Location of R; :: thesis:

per cases ;

suppose A9: da = d ; :: thesis:

hence (Exec (CurInstr (ProgramPart s),s),(s +* (Start-At ((IC s) + k),(SCM R)))) . d = (s +* (Start-At ((IC s) + k),(SCM R))) . db by A7, SCMRING2:13
.= s . db by Th20
.= (Exec (CurInstr (ProgramPart s),s),s) . d by A7, A9, SCMRING2:13
.= ((Exec (CurInstr (ProgramPart s),s),s) +* (Start-At ((succ (IC s)) + k),(SCM R))) . d by Th20 ;
:: thesis:

end;

suppose A10: da <> d ; :: thesis:

hence (Exec (CurInstr (ProgramPart s),s),(s +* (Start-At ((IC s) + k),(SCM R)))) . d = (s +* (Start-At ((IC s) + k),(SCM R))) . d by A7, SCMRING2:13
.= s . d by Th20
.= (Exec (CurInstr (ProgramPart s),s),s) . d by A7, A10, SCMRING2:13
.= ((Exec (CurInstr (ProgramPart s),s),s) +* (Start-At ((succ (IC s)) + k),(SCM R))) . d by Th20 ;
:: thesis:

end;

A11: ( IncAddr (CurInstr (ProgramPart s),s),k = CurInstr (ProgramPart s),s & IC (Exec (CurInstr (ProgramPart s),s),s) = succ (IC s) ) by A7, AMISTD_2:29, SCMRING2:13;
IC (Exec (CurInstr (ProgramPart s),s),(s +* (Start-At ((IC s) + k),(SCM R)))) = IC ((Exec (CurInstr (ProgramPart s),s),s) +* (Start-At ((succ (IC s)) + k),(SCM R))) by A3, A7, SCMRING2:13;
hence Exec (IncAddr (CurInstr (ProgramPart s),s),k),(s +* (Start-At ((IC s) + k),(SCM R))) = (Following (ProgramPart s),s) +* (Start-At ((IC (Following (ProgramPart s),s)) + k),(SCM R)) by A4, A11, A8, Th21; :: thesis:

end;

suppose InsCode (CurInstr (ProgramPart s),s) = 2 ; :: thesis:

then consider da, db being Data-Location of R such that
A12: CurInstr (ProgramPart s),s = AddTo da,db by SCMRING3:18;

A13: now

let d be Data-Location of R; :: thesis:

per cases ;

suppose A14: da = d ; :: thesis:

hence (Exec (CurInstr (ProgramPart s),s),(s +* (Start-At ((IC s) + k),(SCM R)))) . d = ((s +* (Start-At ((IC s) + k),(SCM R))) . da) + ((s +* (Start-At ((IC s) + k),(SCM R))) . db) by A12, SCMRING2:14
.= (s . da) + ((s +* (Start-At ((IC s) + k),(SCM R))) . db) by Th20
.= (s . da) + (s . db) by Th20
.= (Exec (CurInstr (ProgramPart s),s),s) . d by A12, A14, SCMRING2:14
.= ((Exec (CurInstr (ProgramPart s),s),s) +* (Start-At ((succ (IC s)) + k),(SCM R))) . d by Th20 ;
:: thesis:

end;

suppose A15: da <> d ; :: thesis:

hence (Exec (CurInstr (ProgramPart s),s),(s +* (Start-At ((IC s) + k),(SCM R)))) . d = (s +* (Start-At ((IC s) + k),(SCM R))) . d by A12, SCMRING2:14
.= s . d by Th20
.= (Exec (CurInstr (ProgramPart s),s),s) . d by A12, A15, SCMRING2:14
.= ((Exec (CurInstr (ProgramPart s),s),s) +* (Start-At ((succ (IC s)) + k),(SCM R))) . d by Th20 ;
:: thesis:

end;

A16: ( IncAddr (CurInstr (ProgramPart s),s),k = CurInstr (ProgramPart s),s & IC (Exec (CurInstr (ProgramPart s),s),s) = succ (IC s) ) by A12, AMISTD_2:29, SCMRING2:14;
IC (Exec (CurInstr (ProgramPart s),s),(s +* (Start-At ((IC s) + k),(SCM R)))) = IC ((Exec (CurInstr (ProgramPart s),s),s) +* (Start-At ((succ (IC s)) + k),(SCM R))) by A3, A12, SCMRING2:14;
hence Exec (IncAddr (CurInstr (ProgramPart s),s),k),(s +* (Start-At ((IC s) + k),(SCM R))) = (Following (ProgramPart s),s) +* (Start-At ((IC (Following (ProgramPart s),s)) + k),(SCM R)) by A4, A16, A13, Th21; :: thesis:

end;

suppose InsCode (CurInstr (ProgramPart s),s) = 3 ; :: thesis:

then consider da, db being Data-Location of R such that
A17: CurInstr (ProgramPart s),s = SubFrom da,db by SCMRING3:19;

A18: now

let d be Data-Location of R; :: thesis:

per cases ;

suppose A19: da = d ; :: thesis:

hence (Exec (CurInstr (ProgramPart s),s),(s +* (Start-At ((IC s) + k),(SCM R)))) . d = ((s +* (Start-At ((IC s) + k),(SCM R))) . da) - ((s +* (Start-At ((IC s) + k),(SCM R))) . db) by A17, SCMRING2:15
.= (s . da) - ((s +* (Start-At ((IC s) + k),(SCM R))) . db) by Th20
.= (s . da) - (s . db) by Th20
.= (Exec (CurInstr (ProgramPart s),s),s) . d by A17, A19, SCMRING2:15
.= ((Exec (CurInstr (ProgramPart s),s),s) +* (Start-At ((succ (IC s)) + k),(SCM R))) . d by Th20 ;
:: thesis:

end;

suppose A20: da <> d ; :: thesis:

hence (Exec (CurInstr (ProgramPart s),s),(s +* (Start-At ((IC s) + k),(SCM R)))) . d = (s +* (Start-At ((IC s) + k),(SCM R))) . d by A17, SCMRING2:15
.= s . d by Th20
.= (Exec (CurInstr (ProgramPart s),s),s) . d by A17, A20, SCMRING2:15
.= ((Exec (CurInstr (ProgramPart s),s),s) +* (Start-At ((succ (IC s)) + k),(SCM R))) . d by Th20 ;
:: thesis:

end;

A21: ( IncAddr (CurInstr (ProgramPart s),s),k = CurInstr (ProgramPart s),s & IC (Exec (CurInstr (ProgramPart s),s),s) = succ (IC s) ) by A17, AMISTD_2:29, SCMRING2:15;
IC (Exec (CurInstr (ProgramPart s),s),(s +* (Start-At ((IC s) + k),(SCM R)))) = IC ((Exec (CurInstr (ProgramPart s),s),s) +* (Start-At ((succ (IC s)) + k),(SCM R))) by A3, A17, SCMRING2:15;
hence Exec (IncAddr (CurInstr (ProgramPart s),s),k),(s +* (Start-At ((IC s) + k),(SCM R))) = (Following (ProgramPart s),s) +* (Start-At ((IC (Following (ProgramPart s),s)) + k),(SCM R)) by A4, A21, A18, Th21; :: thesis:

end;

suppose InsCode (CurInstr (ProgramPart s),s) = 4 ; :: thesis:

then consider da, db being Data-Location of R such that
A22: CurInstr (ProgramPart s),s = MultBy da,db by SCMRING3:20;

A23: now

let d be Data-Location of R; :: thesis:

per cases ;

suppose A24: da = d ; :: thesis:

hence (Exec (CurInstr (ProgramPart s),s),(s +* (Start-At ((IC s) + k),(SCM R)))) . d = ((s +* (Start-At ((IC s) + k),(SCM R))) . da) * ((s +* (Start-At ((IC s) + k),(SCM R))) . db) by A22, SCMRING2:16
.= (s . da) * ((s +* (Start-At ((IC s) + k),(SCM R))) . db) by Th20
.= (s . da) * (s . db) by Th20
.= (Exec (CurInstr (ProgramPart s),s),s) . d by A22, A24, SCMRING2:16
.= ((Exec (CurInstr (ProgramPart s),s),s) +* (Start-At ((succ (IC s)) + k),(SCM R))) . d by Th20 ;
:: thesis:

end;

suppose A25: da <> d ; :: thesis:

hence (Exec (CurInstr (ProgramPart s),s),(s +* (Start-At ((IC s) + k),(SCM R)))) . d = (s +* (Start-At ((IC s) + k),(SCM R))) . d by A22, SCMRING2:16
.= s . d by Th20
.= (Exec (CurInstr (ProgramPart s),s),s) . d by A22, A25, SCMRING2:16
.= ((Exec (CurInstr (ProgramPart s),s),s) +* (Start-At ((succ (IC s)) + k),(SCM R))) . d by Th20 ;
:: thesis:

end;

A26: ( IncAddr (CurInstr (ProgramPart s),s),k = CurInstr (ProgramPart s),s & IC (Exec (CurInstr (ProgramPart s),s),s) = succ (IC s) ) by A22, AMISTD_2:29, SCMRING2:16;
IC (Exec (CurInstr (ProgramPart s),s),(s +* (Start-At ((IC s) + k),(SCM R)))) = IC ((Exec (CurInstr (ProgramPart s),s),s) +* (Start-At ((succ (IC s)) + k),(SCM R))) by A3, A22, SCMRING2:16;
hence Exec (IncAddr (CurInstr (ProgramPart s),s),k),(s +* (Start-At ((IC s) + k),(SCM R))) = (Following (ProgramPart s),s) +* (Start-At ((IC (Following (ProgramPart s),s)) + k),(SCM R)) by A4, A26, A23, Th21; :: thesis:

end;

suppose InsCode (CurInstr (ProgramPart s),s) = 5 ; :: thesis:

then consider da being Data-Location of R, r being Element of R such that
A27: CurInstr (ProgramPart s),s = da := r by SCMRING3:21;

A28: now

let d be Data-Location of R; :: thesis:

per cases ;

suppose A29: da = d ; :: thesis:

hence (Exec (CurInstr (ProgramPart s),s),(s +* (Start-At ((IC s) + k),(SCM R)))) . d = r by A27, SCMRING2:19
.= (Exec (CurInstr (ProgramPart s),s),s) . d by A27, A29, SCMRING2:19
.= ((Exec (CurInstr (ProgramPart s),s),s) +* (Start-At ((succ (IC s)) + k),(SCM R))) . d by Th20 ;
:: thesis:

end;

suppose A30: da <> d ; :: thesis:

hence (Exec (CurInstr (ProgramPart s),s),(s +* (Start-At ((IC s) + k),(SCM R)))) . d = (s +* (Start-At ((IC s) + k),(SCM R))) . d by A27, SCMRING2:19
.= s . d by Th20
.= (Exec (CurInstr (ProgramPart s),s),s) . d by A27, A30, SCMRING2:19
.= ((Exec (CurInstr (ProgramPart s),s),s) +* (Start-At ((succ (IC s)) + k),(SCM R))) . d by Th20 ;
:: thesis:

end;

A31: ( IncAddr (CurInstr (ProgramPart s),s),k = CurInstr (ProgramPart s),s & IC (Exec (CurInstr (ProgramPart s),s),s) = succ (IC s) ) by A27, AMISTD_2:29, SCMRING2:19;
IC (Exec (CurInstr (ProgramPart s),s),(s +* (Start-At ((IC s) + k),(SCM R)))) = IC ((Exec (CurInstr (ProgramPart s),s),s) +* (Start-At ((succ (IC s)) + k),(SCM R))) by A3, A27, SCMRING2:19;
hence Exec (IncAddr (CurInstr (ProgramPart s),s),k),(s +* (Start-At ((IC s) + k),(SCM R))) = (Following (ProgramPart s),s) +* (Start-At ((IC (Following (ProgramPart s),s)) + k),(SCM R)) by A4, A31, A28, Th21; :: thesis:

end;

suppose InsCode (CurInstr (ProgramPart s),s) = 6 ; :: thesis:

then consider loc being Element of NAT such that
A32: CurInstr (ProgramPart s),s = goto loc,R by SCMRING3:22;
A33: IC (Exec (CurInstr (ProgramPart s),s),s) = loc by A32, SCMRING2:17;

A34: now

let d be Element of NAT ; :: thesis:
thus (Exec (IncAddr (CurInstr (ProgramPart s),s),k),(s +* (Start-At ((IC s) + k),(SCM R)))) . d = (s +* (Start-At ((IC s) + k),(SCM R))) . d by AMI_1:def 13
.= s . d by COMPOS_1:20
.= (Exec (CurInstr (ProgramPart s),s),s) . d by AMI_1:def 13
.= ((Exec (CurInstr (ProgramPart s),s),s) +* (Start-At ((IC (Exec (CurInstr (ProgramPart s),s),s)) + k),(SCM R))) . d by COMPOS_1:20 ; :: thesis:

end;

A35: IncAddr (CurInstr (ProgramPart s),s),k = goto (loc + k),R by A32, SCMRING3:69;

A36: now

let d be Data-Location of R; :: thesis:
thus (Exec (IncAddr (CurInstr (ProgramPart s),s),k),(s +* (Start-At ((IC s) + k),(SCM R)))) . d = (s +* (Start-At ((IC s) + k),(SCM R))) . d by A35, SCMRING2:17
.= s . d by Th20
.= (Exec (CurInstr (ProgramPart s),s),s) . d by A32, SCMRING2:17
.= ((Exec (CurInstr (ProgramPart s),s),s) +* (Start-At ((IC (Exec (CurInstr (ProgramPart s),s),s)) + k),(SCM R))) . d by Th20 ; :: thesis:

end;

set s1 = Exec (IncAddr (CurInstr (ProgramPart s),s),k),(s +* (Start-At ((IC s) + k),(SCM R)));
set s2 = (Exec (CurInstr (ProgramPart s),s),s) +* (Start-At ((IC (Exec (CurInstr (ProgramPart s),s),s)) + k),(SCM R));
IC (Exec (IncAddr (CurInstr (ProgramPart s),s),k),(s +* (Start-At ((IC s) + k),(SCM R)))) = loc + k by A35, SCMRING2:17
.= IC ((Exec (CurInstr (ProgramPart s),s),s) +* (Start-At ((IC (Exec (CurInstr (ProgramPart s),s),s)) + k),(SCM R))) by A33, FUNCT_4:121 ;
hence Exec (IncAddr (CurInstr (ProgramPart s),s),k),(s +* (Start-At ((IC s) + k),(SCM R))) = (Following (ProgramPart s),s) +* (Start-At ((IC (Following (ProgramPart s),s)) + k),(SCM R)) by A36, A34, Th21; :: thesis:

end;

suppose InsCode (CurInstr (ProgramPart s),s) = 7 ; :: thesis:

then consider da being Data-Location of R, loc being Element of NAT such that
A37: CurInstr (ProgramPart s),s = da =0_goto loc by SCMRING3:23;
A38: IncAddr (CurInstr (ProgramPart s),s),k = da =0_goto (loc + k) by A37, SCMRING3:70;

now

per cases ;

suppose A39: s . da = 0. R ; :: thesis:

A40: now

let d be Data-Location of R; :: thesis:
thus (Exec (IncAddr (CurInstr (ProgramPart s),s),k),(s +* (Start-At ((IC s) + k),(SCM R)))) . d = (s +* (Start-At ((IC s) + k),(SCM R))) . d by A38, SCMRING2:18
.= s . d by Th20
.= (Exec (CurInstr (ProgramPart s),s),s) . d by A37, SCMRING2:18
.= ((Exec (CurInstr (ProgramPart s),s),s) +* (Start-At ((IC (Exec (CurInstr (ProgramPart s),s),s)) + k),(SCM R))) . d by Th20 ; :: thesis:

end;

A41: now

end;

A42: IC (Exec (CurInstr (ProgramPart s),s),s) = loc by A37, A39, SCMRING2:18;
(s +* (Start-At ((IC s) + k),(SCM R))) . da = 0. R by A39, Th20;
then IC (Exec (IncAddr (CurInstr (ProgramPart s),s),k),(s +* (Start-At ((IC s) + k),(SCM R)))) = loc + k by A38, SCMRING2:18
.= IC ((Exec (CurInstr (ProgramPart s),s),s) +* (Start-At ((IC (Exec (CurInstr (ProgramPart s),s),s)) + k),(SCM R))) by A42, FUNCT_4:121 ;
hence Exec (IncAddr (CurInstr (ProgramPart s),s),k),(s +* (Start-At ((IC s) + k),(SCM R))) = (Exec (CurInstr (ProgramPart s),s),s) +* (Start-At ((IC (Exec (CurInstr (ProgramPart s),s),s)) + k),(SCM R)) by A40, A41, Th21; :: thesis:

end;

suppose A43: s . da <> 0. R ; :: thesis:

A44: now

end;

A45: now

let d be Data-Location of R; :: thesis:
thus (Exec (IncAddr (CurInstr (ProgramPart s),s),k),(s +* (Start-At ((IC s) + k),(SCM R)))) . d = (s +* (Start-At ((IC s) + k),(SCM R))) . d by A38, SCMRING2:18
.= s . d by Th20
.= (Exec (CurInstr (ProgramPart s),s),s) . d by A37, SCMRING2:18
.= ((Exec (CurInstr (ProgramPart s),s),s) +* (Start-At ((IC (Exec (CurInstr (ProgramPart s),s),s)) + k),(SCM R))) . d by Th20 ; :: thesis:

end;

( (s +* (Start-At ((IC s) + k),(SCM R))) . da <> 0. R & IC (Exec (CurInstr (ProgramPart s),s),s) = succ (IC s) ) by A37, A43, Th20, SCMRING2:18;
then IC (Exec (IncAddr (CurInstr (ProgramPart s),s),k),(s +* (Start-At ((IC s) + k),(SCM R)))) = IC ((Exec (CurInstr (ProgramPart s),s),s) +* (Start-At ((IC (Exec (CurInstr (ProgramPart s),s),s)) + k),(SCM R))) by A3, A38, SCMRING2:18;
hence Exec (IncAddr (CurInstr (ProgramPart s),s),k),(s +* (Start-At ((IC s) + k),(SCM R))) = (Exec (CurInstr (ProgramPart s),s),s) +* (Start-At ((IC (Exec (CurInstr (ProgramPart s),s),s)) + k),(SCM R)) by A45, A44, Th21; :: thesis:

end;

hence Exec (IncAddr (CurInstr (ProgramPart s),s),k),(s +* (Start-At ((IC s) + k),(SCM R))) = (Following (ProgramPart s),s) +* (Start-At ((IC (Following (ProgramPart s),s)) + k),(SCM R)) ; :: thesis:

end;