let k be natural number ; :: thesis: for R being good Ring
for s being State of (SCM R) 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 (SCM R) 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 (SCM R); :: 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: IncAddr (CurInstr s),k = CurInstr s by A7, AMISTD_2:29;
A9: IC (Exec (CurInstr s),s) = Next (IC s) by A7, SCMRING2:13;
A10: 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;

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 A11: 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 Th33
.= (Exec (CurInstr s),s) . d by A7, A11, SCMRING2:13
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by Th33 ;
:: thesis: verum

end;

suppose A12: 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 Th33
.= (Exec (CurInstr s),s) . d by A7, A12, SCMRING2:13
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by Th33 ;
:: 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)) by A4, A8, A9, A10, Th34; :: 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
A13: CurInstr s = AddTo da,db by SCMRING3:18;
A14: IncAddr (CurInstr s),k = CurInstr s by A13, AMISTD_2:29;
A15: IC (Exec (CurInstr s),s) = Next (IC s) by A13, SCMRING2:14;
A16: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) by A3, A13, SCMRING2:14;

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

end;

suppose A18: 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 A13, SCMRING2:14
.= s . d by Th33
.= (Exec (CurInstr s),s) . d by A13, A18, SCMRING2:14
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by Th33 ;
:: 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)) by A4, A14, A15, A16, Th34; :: 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
A19: CurInstr s = SubFrom da,db by SCMRING3:19;
A20: IncAddr (CurInstr s),k = CurInstr s by A19, AMISTD_2:29;
A21: IC (Exec (CurInstr s),s) = Next (IC s) by A19, SCMRING2:15;
A22: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) by A3, A19, SCMRING2:15;

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

end;

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))) . d by A19, SCMRING2:15
.= s . d by Th33
.= (Exec (CurInstr s),s) . d by A19, A24, SCMRING2:15
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by Th33 ;
:: 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)) by A4, A20, A21, A22, Th34; :: 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
A25: CurInstr s = MultBy da,db by SCMRING3:20;
A26: IncAddr (CurInstr s),k = CurInstr s by A25, AMISTD_2:29;
A27: IC (Exec (CurInstr s),s) = Next (IC s) by A25, SCMRING2:16;
A28: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) by A3, A25, SCMRING2:16;

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 = ((s +* (Start-At ((IC s) + k))) . da) * ((s +* (Start-At ((IC s) + k))) . db) by A25, SCMRING2:16
.= (s . da) * ((s +* (Start-At ((IC s) + k))) . db) by Th33
.= (s . da) * (s . db) by Th33
.= (Exec (CurInstr s),s) . d by A25, A29, SCMRING2:16
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by Th33 ;
:: 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 A25, SCMRING2:16
.= s . d by Th33
.= (Exec (CurInstr s),s) . d by A25, A30, SCMRING2:16
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by Th33 ;
:: 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)) by A4, A26, A27, A28, Th34; :: 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 R such that
A31: CurInstr s = da := r by SCMRING3:21;
A32: IncAddr (CurInstr s),k = CurInstr s by A31, AMISTD_2:29;
A33: IC (Exec (CurInstr s),s) = Next (IC s) by A31, SCMRING2:19;
A34: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) by A3, A31, SCMRING2:19;

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 A35: 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 A31, SCMRING2:19
.= (Exec (CurInstr s),s) . d by A31, A35, SCMRING2:19
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by Th33 ;
:: thesis: verum

end;

suppose A36: 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 A31, SCMRING2:19
.= s . d by Th33
.= (Exec (CurInstr s),s) . d by A31, A36, SCMRING2:19
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by Th33 ;
:: 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)) by A4, A32, A33, A34, Th34; :: 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
A37: CurInstr s = goto loc by SCMRING3:22;
A38: IncAddr (CurInstr s),k = goto (loc + k) by A37, SCMRING3:69;
A39: IC (Exec (CurInstr s),s) = loc by A37, SCMRING2:17;
A40: IC (Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k)))) = loc + k by A38, SCMRING2:17
.= IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) by A39, AMI_1:111 ;

A41: 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:17
.= s . d by Th33
.= (Exec (CurInstr s),s) . d by A37, SCMRING2:17
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by Th33 ; :: thesis: verum

end;

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;

hence Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k)) by A40, A41, Th34; :: 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
A42: CurInstr s = da =0_goto loc by SCMRING3:23;
A43: IncAddr (CurInstr s),k = da =0_goto (loc + k) by A42, SCMRING3:70;

now

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

suppose A44: 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))

then A45: (s +* (Start-At ((IC s) + k))) . da = 0. R by Th33;
A46: IC (Exec (CurInstr s),s) = loc by A42, A44, SCMRING2:18;
A47: IC (Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k)))) = loc + k by A43, A45, SCMRING2:18
.= IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) by A46, AMI_1:111 ;

A48: 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 A43, SCMRING2:18
.= s . d by Th33
.= (Exec (CurInstr s),s) . d by A42, SCMRING2:18
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by Th33 ; :: thesis: verum

end;

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;

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 A47, A48, Th34; :: thesis: verum

end;

suppose A49: 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))

then A50: (s +* (Start-At ((IC s) + k))) . da <> 0. R by Th33;
IC (Exec (CurInstr s),s) = Next (IC s) by A42, A49, SCMRING2:18;
then A51: 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, A43, A50, SCMRING2:18;

A52: 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 A43, SCMRING2:18
.= s . d by Th33
.= (Exec (CurInstr s),s) . d by A42, SCMRING2:18
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by Th33 ; :: thesis: verum

end;

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;

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 A51, A52, Th34; :: 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;