let k be natural number ; :: thesis: for R being good Ring
for s being State of holds Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k))
let R be good Ring; :: thesis: for s being State of holds Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k))
let s be State of ; :: thesis: Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k))
set INS = CurInstr s;
consider m being natural number such that
A1: IC s = il. (SCM R),m by AMISTD_1:26;
A2: (IC s) + k = il. (SCM R),(m + k) by A1, AMISTD_1:def 13;
A3: Next (IC (s +* (Start-At ((IC s) + k)))) = Next ((IC s) + k) by AMI_1:111
.= il. (SCM R),((m + k) + 1) by A2, SCMRING3:67
.= il. (SCM R),((m + 1) + k)
.= (il. (SCM R),(m + 1)) + k by AMISTD_1:def 13
.= (Next (il. (SCM R),m)) + k by SCMRING3:67
.= IC ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) by A1, AMI_1:111 ;

A4: now

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

end;

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

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

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

end;

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

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

A8: now

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

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

suppose A9: da = d ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . b₁

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

end;

suppose A10: da <> d ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . b₁

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

end;

end;

end;

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

end;

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

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

A13: now

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

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

suppose A14: da = d ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . b₁

hence (Exec (CurInstr s),(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 Th20
.= (s . da) + (s . db) by Th20
.= (Exec (CurInstr s),s) . d by A12, A14, SCMRING2:14
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by Th20 ;
:: thesis: verum

end;

suppose A15: da <> d ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . b₁

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

end;

end;

end;

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

end;

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

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

A18: now

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

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

suppose A19: da = d ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . b₁

hence (Exec (CurInstr s),(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 (CurInstr s),s) . d by A17, A19, SCMRING2:15
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by Th20 ;
:: thesis: verum

end;

suppose A20: da <> d ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . b₁

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

end;

end;

end;

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

end;

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

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

A23: now

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

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

suppose A24: da = d ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . b₁

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

end;

suppose A25: da <> d ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . b₁

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

end;

end;

end;

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

end;

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

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

A28: now

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

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

suppose A29: da = d ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . b₁

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

end;

suppose A30: da <> d ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . b₁

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

end;

end;

end;

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

end;

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

then consider loc being Instruction-Location of SCM R such that
A32: CurInstr s = goto loc by SCMRING3:22;
A33: IC (Exec (CurInstr s),s) = loc by A32, SCMRING2:17;

A34: now

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

end;

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

A36: now

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

end;

IC (Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k)))) = loc + k by A35, SCMRING2:17
.= IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) by A33, AMI_1:111 ;
hence Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k)) by A36, A34, Th21; :: thesis: verum

end;

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

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

now

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

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

A40: now

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

end;

A41: now

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

end;

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

end;

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

A44: now

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

end;

A45: now

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

end;

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

end;

end;

end;

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

end;

end;