let j, k be natural number ; :: thesis: for R being good Ring
for I being Instruction of (SCM R)
for s being State of (SCM R) st IC s = il. (SCM R),(j + k) holds
Exec I,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))
let R be good Ring; :: thesis: for I being Instruction of (SCM R)
for s being State of (SCM R) st IC s = il. (SCM R),(j + k) holds
Exec I,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))
let I be Instruction of (SCM R); :: thesis: for s being State of (SCM R) st IC s = il. (SCM R),(j + k) holds
Exec I,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))
let s be State of (SCM R); :: thesis: ( IC s = il. (SCM R),(j + k) implies Exec I,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k)) )
assume A1: IC s = il. (SCM R),(j + k) ; :: thesis: Exec I,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))
then A2: Next ((IC s) -' k) = Next (((il. (SCM R),j) + k) -' k) by AMISTD_1:def 13
.= Next (il. (SCM R),j) by AMISTD_1:61
.= il. (SCM R),(j + 1) by SCMRING3:67
.= ((il. (SCM R),(j + 1)) + k) -' k by AMISTD_1:61
.= (il. (SCM R),((j + 1) + k)) -' k by AMISTD_1:def 13
.= (il. (SCM R),((j + k) + 1)) -' k
.= (Next (IC s)) -' k by A1, SCMRING3:67 ;

A3: now

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

end;

per cases ( InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I = 4 or InsCode I = 5 or InsCode I = 6 or InsCode I = 7 ) by NAT_1:32, SCMRING3:71;

suppose InsCode I = 0 ; :: thesis: Exec I,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))

then A4: I = halt (SCM R) by SCMRING3:16;
A5: IncAddr (halt (SCM R)),k = halt (SCM R) by AMISTD_2:29;
thus Exec I,(s +* (Start-At ((IC s) -' k))) = s +* (Start-At ((IC s) -' k)) by A4, AMI_1:def 8
.= s +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k)) by A4, A5, AMI_1:def 8
.= (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k)) by A4, A5, AMI_1:def 8 ; :: thesis: verum

end;

suppose InsCode I = 1 ; :: thesis: Exec I,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))

then consider da, db being Data-Location of R such that
A6: I = da := db by SCMRING3:17;
A7: IncAddr I,k = da := db by A6, AMISTD_2:29;
then A8: (Exec (IncAddr I,k),s) . (IC (SCM R)) = Next (IC s) by SCMRING2:13;
A9: IC (Exec I,(s +* (Start-At ((IC s) -' k)))) = Next (IC (s +* (Start-At ((IC s) -' k)))) by A6, SCMRING2:13
.= (IC (Exec (IncAddr I,k),s)) -' k by A2, A8, AMI_1:111
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) by AMI_1:111 ;

now

let d be Data-Location of R; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k)))) . b₁ = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) . b₁

per cases ( da = d or da <> d ) ;

suppose A10: da = d ; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k)))) . b₁ = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) . b₁

hence (Exec I,(s +* (Start-At ((IC s) -' k)))) . d = (s +* (Start-At ((IC s) -' k))) . db by A6, SCMRING2:13
.= s . db by Th33
.= (Exec (IncAddr I,k),s) . d by A7, A10, SCMRING2:13
.= ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) . d by Th33 ;
:: thesis: verum

end;

suppose A11: da <> d ; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k)))) . b₁ = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) . b₁

hence (Exec I,(s +* (Start-At ((IC s) -' k)))) . d = (s +* (Start-At ((IC s) -' k))) . d by A6, SCMRING2:13
.= s . d by Th33
.= (Exec (IncAddr I,k),s) . d by A7, A11, SCMRING2:13
.= ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) . d by Th33 ;
:: thesis: verum

end;

end;

end;

hence Exec I,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k)) by A3, A9, Th34; :: thesis: verum

end;

suppose InsCode I = 2 ; :: thesis: Exec I,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))

then consider da, db being Data-Location of R such that
A12: I = AddTo da,db by SCMRING3:18;
A13: IncAddr I,k = AddTo da,db by A12, AMISTD_2:29;
then A14: (Exec (IncAddr I,k),s) . (IC (SCM R)) = Next (IC s) by SCMRING2:14;
A15: IC (Exec I,(s +* (Start-At ((IC s) -' k)))) = Next (IC (s +* (Start-At ((IC s) -' k)))) by A12, SCMRING2:14
.= (IC (Exec (IncAddr I,k),s)) -' k by A2, A14, AMI_1:111
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) by AMI_1:111 ;

now

let d be Data-Location of R; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k)))) . b₁ = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) . b₁

per cases ( da = d or da <> d ) ;

suppose A16: da = d ; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k)))) . b₁ = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) . b₁

hence (Exec I,(s +* (Start-At ((IC s) -' k)))) . d = ((s +* (Start-At ((IC s) -' k))) . da) + ((s +* (Start-At ((IC s) -' k))) . db) by A12, SCMRING2:14
.= (s . da) + ((s +* (Start-At ((IC s) -' k))) . db) by Th33
.= (s . da) + (s . db) by Th33
.= (Exec (IncAddr I,k),s) . d by A13, A16, SCMRING2:14
.= ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) . d by Th33 ;
:: thesis: verum

end;

suppose A17: da <> d ; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k)))) . b₁ = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) . b₁

hence (Exec I,(s +* (Start-At ((IC s) -' k)))) . d = (s +* (Start-At ((IC s) -' k))) . d by A12, SCMRING2:14
.= s . d by Th33
.= (Exec (IncAddr I,k),s) . d by A13, A17, SCMRING2:14
.= ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) . d by Th33 ;
:: thesis: verum

end;

end;

end;

hence Exec I,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k)) by A3, A15, Th34; :: thesis: verum

end;

suppose InsCode I = 3 ; :: thesis: Exec I,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))

then consider da, db being Data-Location of R such that
A18: I = SubFrom da,db by SCMRING3:19;
A19: IncAddr I,k = SubFrom da,db by A18, AMISTD_2:29;
then A20: (Exec (IncAddr I,k),s) . (IC (SCM R)) = Next (IC s) by SCMRING2:15;
A21: IC (Exec I,(s +* (Start-At ((IC s) -' k)))) = Next (IC (s +* (Start-At ((IC s) -' k)))) by A18, SCMRING2:15
.= (IC (Exec (IncAddr I,k),s)) -' k by A2, A20, AMI_1:111
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) by AMI_1:111 ;

now

let d be Data-Location of R; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k)))) . b₁ = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) . b₁

per cases ( da = d or da <> d ) ;

suppose A22: da = d ; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k)))) . b₁ = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) . b₁

hence (Exec I,(s +* (Start-At ((IC s) -' k)))) . d = ((s +* (Start-At ((IC s) -' k))) . da) - ((s +* (Start-At ((IC s) -' k))) . db) by A18, SCMRING2:15
.= (s . da) - ((s +* (Start-At ((IC s) -' k))) . db) by Th33
.= (s . da) - (s . db) by Th33
.= (Exec (IncAddr I,k),s) . d by A19, A22, SCMRING2:15
.= ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) . d by Th33 ;
:: thesis: verum

end;

suppose A23: da <> d ; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k)))) . b₁ = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) . b₁

hence (Exec I,(s +* (Start-At ((IC s) -' k)))) . d = (s +* (Start-At ((IC s) -' k))) . d by A18, SCMRING2:15
.= s . d by Th33
.= (Exec (IncAddr I,k),s) . d by A19, A23, SCMRING2:15
.= ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) . d by Th33 ;
:: thesis: verum

end;

end;

end;

hence Exec I,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k)) by A3, A21, Th34; :: thesis: verum

end;

suppose InsCode I = 4 ; :: thesis: Exec I,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))

then consider da, db being Data-Location of R such that
A24: I = MultBy da,db by SCMRING3:20;
A25: IncAddr I,k = MultBy da,db by A24, AMISTD_2:29;
then A26: (Exec (IncAddr I,k),s) . (IC (SCM R)) = Next (IC s) by SCMRING2:16;
A27: IC (Exec I,(s +* (Start-At ((IC s) -' k)))) = Next (IC (s +* (Start-At ((IC s) -' k)))) by A24, SCMRING2:16
.= (IC (Exec (IncAddr I,k),s)) -' k by A2, A26, AMI_1:111
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) by AMI_1:111 ;

now

let d be Data-Location of R; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k)))) . b₁ = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) . b₁

per cases ( da = d or da <> d ) ;

suppose A28: da = d ; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k)))) . b₁ = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) . b₁

hence (Exec I,(s +* (Start-At ((IC s) -' k)))) . d = ((s +* (Start-At ((IC s) -' k))) . da) * ((s +* (Start-At ((IC s) -' k))) . db) by A24, SCMRING2:16
.= (s . da) * ((s +* (Start-At ((IC s) -' k))) . db) by Th33
.= (s . da) * (s . db) by Th33
.= (Exec (IncAddr I,k),s) . d by A25, A28, SCMRING2:16
.= ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) . d by Th33 ;
:: thesis: verum

end;

suppose A29: da <> d ; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k)))) . b₁ = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) . b₁

hence (Exec I,(s +* (Start-At ((IC s) -' k)))) . d = (s +* (Start-At ((IC s) -' k))) . d by A24, SCMRING2:16
.= s . d by Th33
.= (Exec (IncAddr I,k),s) . d by A25, A29, SCMRING2:16
.= ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) . d by Th33 ;
:: thesis: verum

end;

end;

end;

hence Exec I,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k)) by A3, A27, Th34; :: thesis: verum

end;

suppose InsCode I = 5 ; :: thesis: Exec I,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))

then consider da being Data-Location of R, r being Element of R such that
A30: I = da := r by SCMRING3:21;
A31: IncAddr I,k = da := r by A30, AMISTD_2:29;
then A32: (Exec (IncAddr I,k),s) . (IC (SCM R)) = Next (IC s) by SCMRING2:19;
A33: IC (Exec I,(s +* (Start-At ((IC s) -' k)))) = Next (IC (s +* (Start-At ((IC s) -' k)))) by A30, SCMRING2:19
.= (IC (Exec (IncAddr I,k),s)) -' k by A2, A32, AMI_1:111
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) by AMI_1:111 ;

now

let d be Data-Location of R; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k)))) . b₁ = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) . b₁

per cases ( da = d or da <> d ) ;

suppose A34: da = d ; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k)))) . b₁ = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) . b₁

hence (Exec I,(s +* (Start-At ((IC s) -' k)))) . d = r by A30, SCMRING2:19
.= (Exec (IncAddr I,k),s) . d by A31, A34, SCMRING2:19
.= ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) . d by Th33 ;
:: thesis: verum

end;

suppose A35: da <> d ; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k)))) . b₁ = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) . b₁

hence (Exec I,(s +* (Start-At ((IC s) -' k)))) . d = (s +* (Start-At ((IC s) -' k))) . d by A30, SCMRING2:19
.= s . d by Th33
.= (Exec (IncAddr I,k),s) . d by A31, A35, SCMRING2:19
.= ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) . d by Th33 ;
:: thesis: verum

end;

end;

end;

hence Exec I,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k)) by A3, A33, Th34; :: thesis: verum

end;

suppose InsCode I = 6 ; :: thesis: Exec I,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))

then consider loc being Instruction-Location of SCM R such that
A36: I = goto loc by SCMRING3:22;
A37: IncAddr I,k = goto (loc + k) by A36, SCMRING3:69;
then A38: IC (Exec (IncAddr I,k),s) = loc + k by SCMRING2:17;
A39: IC (Exec I,(s +* (Start-At ((IC s) -' k)))) = loc by A36, SCMRING2:17
.= (IC (Exec (IncAddr I,k),s)) -' k by A38, AMISTD_1:61
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) by AMI_1:111 ;

now

let d be Data-Location of R; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k)))) . d = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) . d
thus (Exec I,(s +* (Start-At ((IC s) -' k)))) . d = (s +* (Start-At ((IC s) -' k))) . d by A36, SCMRING2:17
.= s . d by Th33
.= (Exec (IncAddr I,k),s) . d by A37, SCMRING2:17
.= ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) . d by Th33 ; :: thesis: verum

end;

hence Exec I,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k)) by A3, A39, Th34; :: thesis: verum

end;

suppose InsCode I = 7 ; :: thesis: Exec I,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))

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

A42: now

per cases ( s . da = 0. R or s . da <> 0. R ) ;

suppose A43: s . da = 0. R ; :: thesis: IC (Exec I,(s +* (Start-At ((IC s) -' k)))) = IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k)))

then A44: (s +* (Start-At ((IC s) -' k))) . da = 0. R by Th33;
A45: IC (Exec (IncAddr I,k),s) = loc + k by A41, A43, SCMRING2:18;
IC (Exec I,(s +* (Start-At ((IC s) -' k)))) = loc by A40, A44, SCMRING2:18
.= (IC (Exec (IncAddr I,k),s)) -' k by A45, AMISTD_1:61
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) by AMI_1:111 ;
hence IC (Exec I,(s +* (Start-At ((IC s) -' k)))) = IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) ; :: thesis: verum

end;

suppose A46: s . da <> 0. R ; :: thesis: IC (Exec I,(s +* (Start-At ((IC s) -' k)))) = IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k)))

then A47: (s +* (Start-At ((IC s) -' k))) . da <> 0. R by Th33;
A48: (Exec (IncAddr I,k),s) . (IC (SCM R)) = Next (IC s) by A41, A46, SCMRING2:18;
IC (Exec I,(s +* (Start-At ((IC s) -' k)))) = Next (IC (s +* (Start-At ((IC s) -' k)))) by A40, A47, SCMRING2:18
.= (IC (Exec (IncAddr I,k),s)) -' k by A2, A48, AMI_1:111
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) by AMI_1:111 ;
hence IC (Exec I,(s +* (Start-At ((IC s) -' k)))) = IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) ; :: thesis: verum

end;

end;

end;

now

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

end;

hence Exec I,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k)) by A3, A42, Th34; :: thesis: verum

end;

end;