let j, k be natural number ; :: thesis: for R being good Ring
for I being Instruction of
for s being State of 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
for s being State of 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 ; :: thesis: for s being State of 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 ; :: 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)) )

A1: 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;

assume A2: 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 A3: 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 A2, SCMRING3:67 ;

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;
hence Exec I,(s +* (Start-At ((IC s) -' k))) = s +* (Start-At ((IC s) -' k)) by AMI_1:def 8
.= s +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k)) by A4, AMISTD_2:29, AMI_1:def 8
.= (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k)) by A4, AMISTD_2:29, 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
A5: I = da := db by SCMRING3:17;
A6: IncAddr I,k = da := db by A5, AMISTD_2:29;
then A7: (Exec (IncAddr I,k),s) . (IC (SCM R)) = Next (IC s) by SCMRING2:13;

A8: 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 A9: 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 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))) . d by Th20 ;
:: thesis: verum

end;

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))) . 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))) . d by Th20 ;
:: thesis: verum

end;

end;

end;

IC (Exec I,(s +* (Start-At ((IC s) -' k)))) = Next (IC (s +* (Start-At ((IC s) -' k)))) by A5, SCMRING2:13
.= (IC (Exec (IncAddr I,k),s)) -' k by A3, A7, AMI_1:111
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) by AMI_1:111 ;
hence Exec I,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k)) by A1, A8, Th21; :: 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
A11: I = AddTo da,db by SCMRING3:18;
A12: IncAddr I,k = AddTo da,db by A11, AMISTD_2:29;
then A13: (Exec (IncAddr I,k),s) . (IC (SCM R)) = Next (IC s) by SCMRING2:14;

A14: 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 A15: 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 A11, SCMRING2:14
.= (s . da) + ((s +* (Start-At ((IC s) -' k))) . 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))) . d by Th20 ;
:: thesis: verum

end;

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))) . 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))) . d by Th20 ;
:: thesis: verum

end;

end;

end;

IC (Exec I,(s +* (Start-At ((IC s) -' k)))) = Next (IC (s +* (Start-At ((IC s) -' k)))) by A11, SCMRING2:14
.= (IC (Exec (IncAddr I,k),s)) -' k by A3, A13, AMI_1:111
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) by AMI_1:111 ;
hence Exec I,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k)) by A1, A14, Th21; :: 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
A17: I = SubFrom da,db by SCMRING3:19;
A18: IncAddr I,k = SubFrom da,db by A17, AMISTD_2:29;
then A19: (Exec (IncAddr I,k),s) . (IC (SCM R)) = Next (IC s) by SCMRING2:15;

A20: 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 A21: 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 A17, SCMRING2:15
.= (s . da) - ((s +* (Start-At ((IC s) -' k))) . 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))) . d by Th20 ;
:: thesis: verum

end;

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))) . 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))) . d by Th20 ;
:: thesis: verum

end;

end;

end;

IC (Exec I,(s +* (Start-At ((IC s) -' k)))) = Next (IC (s +* (Start-At ((IC s) -' k)))) by A17, SCMRING2:15
.= (IC (Exec (IncAddr I,k),s)) -' k by A3, A19, AMI_1:111
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) by AMI_1:111 ;
hence Exec I,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k)) by A1, A20, Th21; :: 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
A23: I = MultBy da,db by SCMRING3:20;
A24: IncAddr I,k = MultBy da,db by A23, AMISTD_2:29;
then A25: (Exec (IncAddr I,k),s) . (IC (SCM R)) = Next (IC s) by SCMRING2:16;

A26: 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 A27: 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 A23, SCMRING2:16
.= (s . da) * ((s +* (Start-At ((IC s) -' k))) . 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))) . d by Th20 ;
:: thesis: verum

end;

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))) . 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))) . d by Th20 ;
:: thesis: verum

end;

end;

end;

IC (Exec I,(s +* (Start-At ((IC s) -' k)))) = Next (IC (s +* (Start-At ((IC s) -' k)))) by A23, SCMRING2:16
.= (IC (Exec (IncAddr I,k),s)) -' k by A3, A25, AMI_1:111
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) by AMI_1:111 ;
hence Exec I,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k)) by A1, A26, Th21; :: 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 such that
A29: I = da := r by SCMRING3:21;
A30: IncAddr I,k = da := r by A29, AMISTD_2:29;
then A31: (Exec (IncAddr I,k),s) . (IC (SCM R)) = Next (IC s) by SCMRING2:19;

A32: 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 A33: 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 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))) . d by Th20 ;
:: thesis: verum

end;

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 = (s +* (Start-At ((IC s) -' k))) . 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))) . d by Th20 ;
:: thesis: verum

end;

end;

end;

IC (Exec I,(s +* (Start-At ((IC s) -' k)))) = Next (IC (s +* (Start-At ((IC s) -' k)))) by A29, SCMRING2:19
.= (IC (Exec (IncAddr I,k),s)) -' k by A3, A31, AMI_1:111
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) by AMI_1:111 ;
hence Exec I,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k)) by A1, A32, Th21; :: 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
A35: I = goto loc by SCMRING3:22;
A36: IncAddr I,k = goto (loc + k) 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: (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 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))) . d by Th20 ; :: thesis: verum

end;

IC (Exec I,(s +* (Start-At ((IC s) -' k)))) = loc by A35, SCMRING2:17
.= (IC (Exec (IncAddr I,k),s)) -' k by A37, AMISTD_1:61
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))) by AMI_1:111 ;
hence Exec I,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k)) by A1, A38, Th21; :: 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
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 ( s . da = 0. R or s . da <> 0. R ) ;

suppose A42: 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 A43: IC (Exec (IncAddr I,k),s) = loc + k by A40, SCMRING2:18;
(s +* (Start-At ((IC s) -' k))) . da = 0. R by A42, Th20;
then IC (Exec I,(s +* (Start-At ((IC s) -' k)))) = loc by A39, SCMRING2:18
.= (IC (Exec (IncAddr I,k),s)) -' k by A43, 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 A44: 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 A45: (Exec (IncAddr I,k),s) . (IC (SCM R)) = Next (IC s) by A40, SCMRING2:18;
(s +* (Start-At ((IC s) -' k))) . da <> 0. R by A44, Th20;
then IC (Exec I,(s +* (Start-At ((IC s) -' k)))) = Next (IC (s +* (Start-At ((IC s) -' k)))) by A39, SCMRING2:18
.= (IC (Exec (IncAddr I,k),s)) -' k by A3, A45, 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 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))) . d by Th20 ; :: 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 A1, A41, Th21; :: thesis: verum

end;

end;