let k be Element of NAT ; :: 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;
reconsider m = IC s as Element of NAT by ORDINAL1:def 13;
A1: Next (IC (s +* (Start-At ((IC s) + k)))) = Next (il. (m + k)) by AMI_1:111
.= il. ((m + k) + 1) by NAT_1:39
.= (il. (m + 1)) + k
.= (Next (IC s)) + k by NAT_1:39
.= IC ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) by AMI_1:111 ;

A2: now

let d be Instruction-Location of SCM ; :: 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 or InsCode (CurInstr s) = 8 ) by AMI_5:36, NAT_1:33;

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 A3: CurInstr s = halt SCM by AMI_5:46;
then A4: Following s = s by AMI_1:def 8;
thus Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = Exec (halt SCM ),(s +* (Start-At ((IC s) + k))) by A3, Def3, AMI_5:37
.= (Following s) +* (Start-At ((IC (Following s)) + k)) by A4, 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 such that
A5: CurInstr s = da := db by AMI_5:47;

A6: now

let d be Data-Location ; :: 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 A7: 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 A5, AMI_3:8
.= s . db by AMI_5:80
.= (Exec (CurInstr s),s) . d by A5, A7, AMI_3:8
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by AMI_5:80 ;
:: thesis: verum

end;

suppose A8: 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 A5, AMI_3:8
.= s . d by AMI_5:80
.= (Exec (CurInstr s),s) . d by A5, A8, AMI_3:8
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by AMI_5:80 ;
:: thesis: verum

end;

end;

end;

A9: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) by A1, A5, AMI_3:8;
( IncAddr (CurInstr s),k = CurInstr s & IC (Exec (CurInstr s),s) = Next (IC s) ) by A5, Th5, AMI_3:8;
hence Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k)) by A2, A9, A6, AMI_5:26; :: 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 such that
A10: CurInstr s = AddTo da,db by AMI_5:48;

A11: now

let d be Data-Location ; :: 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 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))) . da) + ((s +* (Start-At ((IC s) + k))) . db) by A10, AMI_3:9
.= (s . da) + ((s +* (Start-At ((IC s) + k))) . db) by AMI_5:80
.= (s . da) + (s . db) by AMI_5:80
.= (Exec (CurInstr s),s) . d by A10, A12, AMI_3:9
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by AMI_5:80 ;
:: thesis: verum

end;

suppose A13: 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 A10, AMI_3:9
.= s . d by AMI_5:80
.= (Exec (CurInstr s),s) . d by A10, A13, AMI_3:9
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by AMI_5:80 ;
:: thesis: verum

end;

end;

end;

A14: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) by A1, A10, AMI_3:9;
( IncAddr (CurInstr s),k = CurInstr s & IC (Exec (CurInstr s),s) = Next (IC s) ) by A10, Th6, AMI_3:9;
hence Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k)) by A2, A14, A11, AMI_5:26; :: 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 such that
A15: CurInstr s = SubFrom da,db by AMI_5:49;

A16: now

let d be Data-Location ; :: 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 A15, AMI_3:10
.= (s . da) - ((s +* (Start-At ((IC s) + k))) . db) by AMI_5:80
.= (s . da) - (s . db) by AMI_5:80
.= (Exec (CurInstr s),s) . d by A15, A17, AMI_3:10
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by AMI_5:80 ;
:: 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 A15, AMI_3:10
.= s . d by AMI_5:80
.= (Exec (CurInstr s),s) . d by A15, A18, AMI_3:10
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by AMI_5:80 ;
:: thesis: verum

end;

end;

end;

A19: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) by A1, A15, AMI_3:10;
( IncAddr (CurInstr s),k = CurInstr s & IC (Exec (CurInstr s),s) = Next (IC s) ) by A15, Th7, AMI_3:10;
hence Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k)) by A2, A19, A16, AMI_5:26; :: 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 such that
A20: CurInstr s = MultBy da,db by AMI_5:50;

A21: now

let d be Data-Location ; :: 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 A22: 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 A20, AMI_3:11
.= (s . da) * ((s +* (Start-At ((IC s) + k))) . db) by AMI_5:80
.= (s . da) * (s . db) by AMI_5:80
.= (Exec (CurInstr s),s) . d by A20, A22, AMI_3:11
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by AMI_5:80 ;
:: thesis: verum

end;

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))) . d by A20, AMI_3:11
.= s . d by AMI_5:80
.= (Exec (CurInstr s),s) . d by A20, A23, AMI_3:11
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by AMI_5:80 ;
:: thesis: verum

end;

end;

end;

A24: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) by A1, A20, AMI_3:11;
( IncAddr (CurInstr s),k = CurInstr s & IC (Exec (CurInstr s),s) = Next (IC s) ) by A20, Th8, AMI_3:11;
hence Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k)) by A2, A24, A21, AMI_5:26; :: 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, db being Data-Location such that
A25: CurInstr s = Divide da,db by AMI_5:51;

A26: now

let d be Data-Location ; :: 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 <> db or da = db ) ;

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

hereby :: thesis: verum

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

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

hence (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . d = ((s +* (Start-At ((IC s) + k))) . da) div ((s +* (Start-At ((IC s) + k))) . db) by A25, A27, AMI_3:12
.= (s . da) div ((s +* (Start-At ((IC s) + k))) . db) by AMI_5:80
.= (s . da) div (s . db) by AMI_5:80
.= (Exec (CurInstr s),s) . d by A25, A27, A28, AMI_3:12
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by AMI_5:80 ;
:: thesis: verum

end;

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

hence (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . d = ((s +* (Start-At ((IC s) + k))) . da) mod ((s +* (Start-At ((IC s) + k))) . db) by A25, AMI_3:12
.= (s . da) mod ((s +* (Start-At ((IC s) + k))) . db) by AMI_5:80
.= (s . da) mod (s . db) by AMI_5:80
.= (Exec (CurInstr s),s) . d by A25, A29, AMI_3:12
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by AMI_5:80 ;
:: thesis: verum

end;

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

hence (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . d = (s +* (Start-At ((IC s) + k))) . d by A25, AMI_3:12
.= s . d by AMI_5:80
.= (Exec (CurInstr s),s) . d by A25, A30, AMI_3:12
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by AMI_5:80 ;
:: thesis: verum

end;

end;

end;

end;

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

hereby :: thesis: verum

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

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

hence (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . d = ((s +* (Start-At ((IC s) + k))) . da) mod ((s +* (Start-At ((IC s) + k))) . da) by A25, A31, AMI_3:12
.= (s . da) mod ((s +* (Start-At ((IC s) + k))) . da) by AMI_5:80
.= (s . da) mod (s . da) by AMI_5:80
.= (Exec (CurInstr s),s) . d by A25, A31, A32, AMI_3:12
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by AMI_5:80 ;
:: thesis: verum

end;

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

hence (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . d = (s +* (Start-At ((IC s) + k))) . d by A25, A31, AMI_3:12
.= s . d by AMI_5:80
.= (Exec (CurInstr s),s) . d by A25, A31, A33, AMI_3:12
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by AMI_5:80 ;
:: thesis: verum

end;

end;

end;

end;

end;

end;

A34: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) by A1, A25, AMI_3:12;
( IncAddr (CurInstr s),k = CurInstr s & IC (Exec (CurInstr s),s) = Next (IC s) ) by A25, Th9, AMI_3:12;
hence Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k)) by A2, A34, A26, AMI_5:26; :: 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 such that
A35: CurInstr s = goto loc by AMI_5:52;
A36: IC (Exec (CurInstr s),s) = loc by A35, AMI_3:13;

A37: now

let d be Instruction-Location of SCM ; :: 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;

A38: IncAddr (CurInstr s),k = goto (loc + k) by A35, Th10;

A39: now

let d be Data-Location ; :: 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, AMI_3:13
.= s . d by AMI_5:80
.= (Exec (CurInstr s),s) . d by A35, AMI_3:13
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by AMI_5:80 ; :: thesis: verum

end;

IC (Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k)))) = loc + k by A38, AMI_3:13
.= IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) by A36, AMI_1:111 ;
hence Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k)) by A39, A37, AMI_5:26; :: 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 loc being Instruction-Location of SCM , da being Data-Location such that
A40: CurInstr s = da =0_goto loc by AMI_5:53;
A41: IncAddr (CurInstr s),k = da =0_goto (loc + k) by A40, Th11;

now

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

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

A43: now

let d be Data-Location ; :: 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 A41, AMI_3:14
.= s . d by AMI_5:80
.= (Exec (CurInstr s),s) . d by A40, AMI_3:14
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by AMI_5:80 ; :: thesis: verum

end;

A44: now

let d be Instruction-Location of SCM ; :: 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: IC (Exec (CurInstr s),s) = loc by A40, A42, AMI_3:14;
(s +* (Start-At ((IC s) + k))) . da = 0 by A42, AMI_5:80;
then IC (Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k)))) = loc + k by A41, AMI_3:14
.= IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) by A45, 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 A43, A44, AMI_5:26; :: thesis: verum

end;

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

A47: now

let d be Instruction-Location of SCM ; :: 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;

A48: now

let d be Data-Location ; :: 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 A41, AMI_3:14
.= s . d by AMI_5:80
.= (Exec (CurInstr s),s) . d by A40, AMI_3:14
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by AMI_5:80 ; :: thesis: verum

end;

( (s +* (Start-At ((IC s) + k))) . da <> 0 & IC (Exec (CurInstr s),s) = Next (IC s) ) by A40, A46, AMI_3:14, AMI_5:80;
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 A1, A41, AMI_3:14;
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 A48, A47, AMI_5:26; :: 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;

suppose InsCode (CurInstr s) = 8 ; :: 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 , da being Data-Location such that
A49: CurInstr s = da >0_goto loc by AMI_5:54;

now

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

suppose A50: s . da > 0 ; :: thesis: Exec (da >0_goto (loc + k)),(s +* (Start-At ((IC s) + k))) = (Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))

A51: now

let d be Data-Location ; :: thesis: (Exec (da >0_goto (loc + k)),(s +* (Start-At ((IC s) + k)))) . d = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d
thus (Exec (da >0_goto (loc + k)),(s +* (Start-At ((IC s) + k)))) . d = (s +* (Start-At ((IC s) + k))) . d by AMI_3:15
.= s . d by AMI_5:80
.= (Exec (CurInstr s),s) . d by A49, AMI_3:15
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by AMI_5:80 ; :: thesis: verum

end;

A52: now

let d be Instruction-Location of SCM ; :: thesis: (Exec (da >0_goto (loc + k)),(s +* (Start-At ((IC s) + k)))) . d = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d
thus (Exec (da >0_goto (loc + 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;

A53: IC (Exec (CurInstr s),s) = loc by A49, A50, AMI_3:15;
(s +* (Start-At ((IC s) + k))) . da > 0 by A50, AMI_5:80;
then IC (Exec (da >0_goto (loc + k)),(s +* (Start-At ((IC s) + k)))) = loc + k by AMI_3:15
.= IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) by A53, AMI_1:111 ;
hence Exec (da >0_goto (loc + k)),(s +* (Start-At ((IC s) + k))) = (Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k)) by A51, A52, AMI_5:26; :: thesis: verum

end;

suppose A54: s . da <= 0 ; :: thesis: Exec (da >0_goto (loc + k)),(s +* (Start-At ((IC s) + k))) = (Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))

A55: now

let d be Instruction-Location of SCM ; :: thesis: (Exec (da >0_goto (loc + k)),(s +* (Start-At ((IC s) + k)))) . d = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d
thus (Exec (da >0_goto (loc + 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;

A56: now

let d be Data-Location ; :: thesis: (Exec (da >0_goto (loc + k)),(s +* (Start-At ((IC s) + k)))) . d = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d
thus (Exec (da >0_goto (loc + k)),(s +* (Start-At ((IC s) + k)))) . d = (s +* (Start-At ((IC s) + k))) . d by AMI_3:15
.= s . d by AMI_5:80
.= (Exec (CurInstr s),s) . d by A49, AMI_3:15
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by AMI_5:80 ; :: thesis: verum

end;

( (s +* (Start-At ((IC s) + k))) . da <= 0 & IC (Exec (CurInstr s),s) = Next (IC s) ) by A49, A54, AMI_3:15, AMI_5:80;
then IC (Exec (da >0_goto (loc + k)),(s +* (Start-At ((IC s) + k)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) by A1, AMI_3:15;
hence Exec (da >0_goto (loc + k)),(s +* (Start-At ((IC s) + k))) = (Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k)) by A56, A55, AMI_5:26; :: 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 A49, Th12; :: thesis: verum

end;

end;