let j, k be Element of NAT ; :: thesis:
let R be good Ring; :: thesis:
let I be Instruction of (SCM R); :: thesis:
let s be State of (SCM R); :: thesis:

A1: now

let d be Element of NAT ; :: thesis:
thus (Exec (I,(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 ((IncAddr (I,k)),s)) . d by AMI_1:def 13
.= ((Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R)))) . d by COMPOS_1:20 ; :: thesis:

end;

assume A2: IC s = j + k ; :: thesis:
then A3: succ ((IC s) -' k) = succ j by NAT_D:34
.= ((j + 1) + k) -' k by NAT_D:34
.= (succ (IC s)) -' k by A2 ;

per cases by NAT_1:32, SCMRING3:71;

suppose InsCode I = 0 ; :: thesis:

then A4: I = halt (SCM R) by SCMRING3:16;
hence Exec (I,(s +* (Start-At (((IC s) -' k),(SCM R))))) = s +* (Start-At (((IC s) -' k),(SCM R))) by EXTPRO_1:def 3
.= s +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R))) by A4, EXTPRO_1:def 3
.= (Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R))) by A4, EXTPRO_1:def 3 ;
:: thesis:

end;

suppose InsCode I = 1 ; :: thesis:

then consider da, db being Data-Location of R such that
A5: I = da := db by SCMRING3:17;
A6: IncAddr (I,k) = da := db by A5, COMPOS_1:92;
then A7: (Exec ((IncAddr (I,k)),s)) . (IC (SCM R)) = succ (IC s) by SCMRING2:13;

A8: now

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

per cases ;

suppose A9: da = d ; :: thesis:

hence (Exec (I,(s +* (Start-At (((IC s) -' k),(SCM R)))))) . d = (s +* (Start-At (((IC s) -' k),(SCM R)))) . db by A5, SCMRING2:13
.= s . db by Th20
.= (Exec ((IncAddr (I,k)),s)) . d by A6, A9, SCMRING2:13
.= ((Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R)))) . d by Th20 ;
:: thesis:

end;

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

hence (Exec (I,(s +* (Start-At (((IC s) -' k),(SCM R)))))) . d = (s +* (Start-At (((IC s) -' k),(SCM R)))) . d by A5, SCMRING2:13
.= s . d by Th20
.= (Exec ((IncAddr (I,k)),s)) . d by A6, A10, SCMRING2:13
.= ((Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R)))) . d by Th20 ;
:: thesis:

end;

IC (Exec (I,(s +* (Start-At (((IC s) -' k),(SCM R)))))) = succ (IC (s +* (Start-At (((IC s) -' k),(SCM R))))) by A5, SCMRING2:13
.= (IC (Exec ((IncAddr (I,k)),s))) -' k by A3, A7, FUNCT_4:121
.= IC ((Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R)))) by FUNCT_4:121 ;
hence Exec (I,(s +* (Start-At (((IC s) -' k),(SCM R))))) = (Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R))) by A1, A8, Th21; :: thesis:

end;

suppose InsCode I = 2 ; :: thesis:

then consider da, db being Data-Location of R such that
A11: I = AddTo (da,db) by SCMRING3:18;
A12: IncAddr (I,k) = AddTo (da,db) by A11, COMPOS_1:92;
then A13: (Exec ((IncAddr (I,k)),s)) . (IC (SCM R)) = succ (IC s) by SCMRING2:14;

A14: now

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

per cases ;

suppose A15: da = d ; :: thesis:

hence (Exec (I,(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 A11, SCMRING2:14
.= (s . da) + ((s +* (Start-At (((IC s) -' k),(SCM R)))) . db) by Th20
.= (s . da) + (s . db) by Th20
.= (Exec ((IncAddr (I,k)),s)) . d by A12, A15, SCMRING2:14
.= ((Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R)))) . d by Th20 ;
:: thesis:

end;

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

hence (Exec (I,(s +* (Start-At (((IC s) -' k),(SCM R)))))) . d = (s +* (Start-At (((IC s) -' k),(SCM R)))) . d by A11, SCMRING2:14
.= s . d by Th20
.= (Exec ((IncAddr (I,k)),s)) . d by A12, A16, SCMRING2:14
.= ((Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R)))) . d by Th20 ;
:: thesis:

end;

IC (Exec (I,(s +* (Start-At (((IC s) -' k),(SCM R)))))) = succ (IC (s +* (Start-At (((IC s) -' k),(SCM R))))) by A11, SCMRING2:14
.= (IC (Exec ((IncAddr (I,k)),s))) -' k by A3, A13, FUNCT_4:121
.= IC ((Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R)))) by FUNCT_4:121 ;
hence Exec (I,(s +* (Start-At (((IC s) -' k),(SCM R))))) = (Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R))) by A1, A14, Th21; :: thesis:

end;

suppose InsCode I = 3 ; :: thesis:

then consider da, db being Data-Location of R such that
A17: I = SubFrom (da,db) by SCMRING3:19;
A18: IncAddr (I,k) = SubFrom (da,db) by A17, COMPOS_1:92;
then A19: (Exec ((IncAddr (I,k)),s)) . (IC (SCM R)) = succ (IC s) by SCMRING2:15;

A20: now

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

per cases ;

suppose A21: da = d ; :: thesis:

hence (Exec (I,(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 ((IncAddr (I,k)),s)) . d by A18, A21, SCMRING2:15
.= ((Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R)))) . d by Th20 ;
:: thesis:

end;

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

hence (Exec (I,(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 ((IncAddr (I,k)),s)) . d by A18, A22, SCMRING2:15
.= ((Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R)))) . d by Th20 ;
:: thesis:

end;

IC (Exec (I,(s +* (Start-At (((IC s) -' k),(SCM R)))))) = succ (IC (s +* (Start-At (((IC s) -' k),(SCM R))))) by A17, SCMRING2:15
.= (IC (Exec ((IncAddr (I,k)),s))) -' k by A3, A19, FUNCT_4:121
.= IC ((Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R)))) by FUNCT_4:121 ;
hence Exec (I,(s +* (Start-At (((IC s) -' k),(SCM R))))) = (Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R))) by A1, A20, Th21; :: thesis:

end;

suppose InsCode I = 4 ; :: thesis:

then consider da, db being Data-Location of R such that
A23: I = MultBy (da,db) by SCMRING3:20;
A24: IncAddr (I,k) = MultBy (da,db) by A23, COMPOS_1:92;
then A25: (Exec ((IncAddr (I,k)),s)) . (IC (SCM R)) = succ (IC s) by SCMRING2:16;

A26: now

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

per cases ;

suppose A27: da = d ; :: thesis:

hence (Exec (I,(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 A23, SCMRING2:16
.= (s . da) * ((s +* (Start-At (((IC s) -' k),(SCM R)))) . db) by Th20
.= (s . da) * (s . db) by Th20
.= (Exec ((IncAddr (I,k)),s)) . d by A24, A27, SCMRING2:16
.= ((Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R)))) . d by Th20 ;
:: thesis:

end;

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

hence (Exec (I,(s +* (Start-At (((IC s) -' k),(SCM R)))))) . d = (s +* (Start-At (((IC s) -' k),(SCM R)))) . d by A23, SCMRING2:16
.= s . d by Th20
.= (Exec ((IncAddr (I,k)),s)) . d by A24, A28, SCMRING2:16
.= ((Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R)))) . d by Th20 ;
:: thesis:

end;

IC (Exec (I,(s +* (Start-At (((IC s) -' k),(SCM R)))))) = succ (IC (s +* (Start-At (((IC s) -' k),(SCM R))))) by A23, SCMRING2:16
.= (IC (Exec ((IncAddr (I,k)),s))) -' k by A3, A25, FUNCT_4:121
.= IC ((Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R)))) by FUNCT_4:121 ;
hence Exec (I,(s +* (Start-At (((IC s) -' k),(SCM R))))) = (Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R))) by A1, A26, Th21; :: thesis:

end;

suppose InsCode I = 5 ; :: thesis:

then consider da being Data-Location of R, r being Element of R such that
A29: I = da := r by SCMRING3:21;
A30: IncAddr (I,k) = da := r by A29, COMPOS_1:92;
then A31: (Exec ((IncAddr (I,k)),s)) . (IC (SCM R)) = succ (IC s) by SCMRING2:19;

A32: now

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

per cases ;

suppose A33: da = d ; :: thesis:

hence (Exec (I,(s +* (Start-At (((IC s) -' k),(SCM R)))))) . d = r by A29, SCMRING2:19
.= (Exec ((IncAddr (I,k)),s)) . d by A30, A33, SCMRING2:19
.= ((Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R)))) . d by Th20 ;
:: thesis:

end;

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

hence (Exec (I,(s +* (Start-At (((IC s) -' k),(SCM R)))))) . d = (s +* (Start-At (((IC s) -' k),(SCM R)))) . d by A29, SCMRING2:19
.= s . d by Th20
.= (Exec ((IncAddr (I,k)),s)) . d by A30, A34, SCMRING2:19
.= ((Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R)))) . d by Th20 ;
:: thesis:

end;

IC (Exec (I,(s +* (Start-At (((IC s) -' k),(SCM R)))))) = succ (IC (s +* (Start-At (((IC s) -' k),(SCM R))))) by A29, SCMRING2:19
.= (IC (Exec ((IncAddr (I,k)),s))) -' k by A3, A31, FUNCT_4:121
.= IC ((Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R)))) by FUNCT_4:121 ;
hence Exec (I,(s +* (Start-At (((IC s) -' k),(SCM R))))) = (Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R))) by A1, A32, Th21; :: thesis:

end;

suppose InsCode I = 6 ; :: thesis:

then consider loc being Element of NAT such that
A35: I = goto (loc,R) by SCMRING3:22;
A36: IncAddr (I,k) = goto ((loc + k),R) by A35, SCMRING3:69;
then A37: IC (Exec ((IncAddr (I,k)),s)) = loc + k by SCMRING2:17;

A38: now

let d be Data-Location of R; :: thesis:
thus (Exec (I,(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 ((IncAddr (I,k)),s)) . d by A36, SCMRING2:17
.= ((Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R)))) . d by Th20 ; :: thesis:

end;

IC (Exec (I,(s +* (Start-At (((IC s) -' k),(SCM R)))))) = loc by A35, SCMRING2:17
.= (IC (Exec ((IncAddr (I,k)),s))) -' k by A37, NAT_D:34
.= IC ((Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R)))) by FUNCT_4:121 ;
hence Exec (I,(s +* (Start-At (((IC s) -' k),(SCM R))))) = (Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R))) by A1, A38, Th21; :: thesis:

end;

suppose InsCode I = 7 ; :: thesis:

then consider da being Data-Location of R, loc being Element of NAT such that
A39: I = da =0_goto loc by SCMRING3:23;
A40: IncAddr (I,k) = da =0_goto (loc + k) by A39, SCMRING3:70;

A41: now

per cases ;

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

then A43: IC (Exec ((IncAddr (I,k)),s)) = loc + k by A40, SCMRING2:18;
(s +* (Start-At (((IC s) -' k),(SCM R)))) . da = 0. R by A42, Th20;
then IC (Exec (I,(s +* (Start-At (((IC s) -' k),(SCM R)))))) = loc by A39, SCMRING2:18
.= (IC (Exec ((IncAddr (I,k)),s))) -' k by A43, NAT_D:34
.= IC ((Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R)))) by FUNCT_4:121 ;
hence IC (Exec (I,(s +* (Start-At (((IC s) -' k),(SCM R)))))) = IC ((Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R)))) ; :: thesis:

end;

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

then A45: (Exec ((IncAddr (I,k)),s)) . (IC (SCM R)) = succ (IC s) by A40, SCMRING2:18;
(s +* (Start-At (((IC s) -' k),(SCM R)))) . da <> 0. R by A44, Th20;
then IC (Exec (I,(s +* (Start-At (((IC s) -' k),(SCM R)))))) = succ (IC (s +* (Start-At (((IC s) -' k),(SCM R))))) by A39, SCMRING2:18
.= (IC (Exec ((IncAddr (I,k)),s))) -' k by A3, A45, FUNCT_4:121
.= IC ((Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R)))) by FUNCT_4:121 ;
hence IC (Exec (I,(s +* (Start-At (((IC s) -' k),(SCM R)))))) = IC ((Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R)))) ; :: thesis:

end;

now

let d be Data-Location of R; :: thesis:
thus (Exec (I,(s +* (Start-At (((IC s) -' k),(SCM R)))))) . d = (s +* (Start-At (((IC s) -' k),(SCM R)))) . d by A39, SCMRING2:18
.= s . d by Th20
.= (Exec ((IncAddr (I,k)),s)) . d by A40, SCMRING2:18
.= ((Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R)))) . d by Th20 ; :: thesis:

end;

hence Exec (I,(s +* (Start-At (((IC s) -' k),(SCM R))))) = (Exec ((IncAddr (I,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (I,k)),s))) -' k),(SCM R))) by A1, A41, Th21; :: thesis:

end;