let INS be Instruction of SCM ; :: thesis: for s being State of SCM
for j, k being Element of NAT st IC s = j + k holds
Exec INS,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))
let s be State of SCM ; :: thesis: for j, k being Element of NAT st IC s = j + k holds
Exec INS,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))
let j, k be Element of NAT ; :: thesis: ( IC s = j + k implies Exec INS,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k)) )
assume A1: IC s = j + k ; :: thesis: Exec INS,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))
then A2: Next ((IC s) -' k) = Next (il. j) by NAT_D:34
.= il. (j + 1) by NAT_1:39
.= (il. ((j + 1) + k)) -' k by NAT_D:34
.= (il. ((j + k) + 1)) -' k
.= (Next (IC s)) -' k by A1, NAT_1:39 ;

A3: now

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

end;

per cases ( InsCode INS = 0 or InsCode INS = 1 or InsCode INS = 2 or InsCode INS = 3 or InsCode INS = 4 or InsCode INS = 5 or InsCode INS = 6 or InsCode INS = 7 or InsCode INS = 8 ) by AMI_5:36, NAT_1:33;

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

then A4: INS = halt SCM by AMI_5:46;
A5: IncAddr (halt SCM ),k = halt SCM by Def3, AMI_5:37;
thus Exec INS,(s +* (Start-At ((IC s) -' k))) = s +* (Start-At ((IC s) -' k)) by A4, AMI_1:def 8
.= s +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k)) by A4, A5, AMI_1:def 8
.= (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k)) by A4, A5, AMI_1:def 8 ; :: thesis: verum

end;

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

then consider da, db being Data-Location such that
A6: INS = da := db by AMI_5:47;
A7: IncAddr INS,k = da := db by A6, Th5;
then A8: (Exec (IncAddr INS,k),s) . (IC SCM ) = Next (IC s) by AMI_3:8;
A9: IC (Exec INS,(s +* (Start-At ((IC s) -' k)))) = Next (IC (s +* (Start-At ((IC s) -' k)))) by A6, AMI_3:8
.= (IC (Exec (IncAddr INS,k),s)) -' k by A2, A8, AMI_1:111
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) by AMI_1:111 ;

now

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

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

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k)))) . d = (s +* (Start-At ((IC s) -' k))) . db by A6, AMI_3:8
.= s . db by AMI_5:80
.= (Exec (IncAddr INS,k),s) . d by A7, A10, AMI_3:8
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) . d by AMI_5:80 ;
:: thesis: verum

end;

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k)))) . d = (s +* (Start-At ((IC s) -' k))) . d by A6, AMI_3:8
.= s . d by AMI_5:80
.= (Exec (IncAddr INS,k),s) . d by A7, A11, AMI_3:8
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) . d by AMI_5:80 ;
:: thesis: verum

end;

end;

end;

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

end;

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

then consider da, db being Data-Location such that
A12: INS = AddTo da,db by AMI_5:48;
A13: IncAddr INS,k = AddTo da,db by A12, Th6;
then A14: (Exec (IncAddr INS,k),s) . (IC SCM ) = Next (IC s) by AMI_3:9;
A15: IC (Exec INS,(s +* (Start-At ((IC s) -' k)))) = Next (IC (s +* (Start-At ((IC s) -' k)))) by A12, AMI_3:9
.= (IC (Exec (IncAddr INS,k),s)) -' k by A2, A14, AMI_1:111
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) by AMI_1:111 ;

now

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

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

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k)))) . d = ((s +* (Start-At ((IC s) -' k))) . da) + ((s +* (Start-At ((IC s) -' k))) . db) by A12, 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 (IncAddr INS,k),s) . d by A13, A16, AMI_3:9
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) . d by AMI_5:80 ;
:: thesis: verum

end;

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k)))) . d = (s +* (Start-At ((IC s) -' k))) . d by A12, AMI_3:9
.= s . d by AMI_5:80
.= (Exec (IncAddr INS,k),s) . d by A13, A17, AMI_3:9
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) . d by AMI_5:80 ;
:: thesis: verum

end;

end;

end;

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

end;

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

then consider da, db being Data-Location such that
A18: INS = SubFrom da,db by AMI_5:49;
A19: IncAddr INS,k = SubFrom da,db by A18, Th7;
then A20: (Exec (IncAddr INS,k),s) . (IC SCM ) = Next (IC s) by AMI_3:10;
A21: IC (Exec INS,(s +* (Start-At ((IC s) -' k)))) = Next (IC (s +* (Start-At ((IC s) -' k)))) by A18, AMI_3:10
.= (IC (Exec (IncAddr INS,k),s)) -' k by A2, A20, AMI_1:111
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) by AMI_1:111 ;

now

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

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

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k)))) . d = ((s +* (Start-At ((IC s) -' k))) . da) - ((s +* (Start-At ((IC s) -' k))) . db) by A18, 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 (IncAddr INS,k),s) . d by A19, A22, AMI_3:10
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) . d by AMI_5:80 ;
:: thesis: verum

end;

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k)))) . d = (s +* (Start-At ((IC s) -' k))) . d by A18, AMI_3:10
.= s . d by AMI_5:80
.= (Exec (IncAddr INS,k),s) . d by A19, A23, AMI_3:10
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) . d by AMI_5:80 ;
:: thesis: verum

end;

end;

end;

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

end;

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

then consider da, db being Data-Location such that
A24: INS = MultBy da,db by AMI_5:50;
A25: IncAddr INS,k = MultBy da,db by A24, Th8;
then A26: (Exec (IncAddr INS,k),s) . (IC SCM ) = Next (IC s) by AMI_3:11;
A27: IC (Exec INS,(s +* (Start-At ((IC s) -' k)))) = Next (IC (s +* (Start-At ((IC s) -' k)))) by A24, AMI_3:11
.= (IC (Exec (IncAddr INS,k),s)) -' k by A2, A26, AMI_1:111
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) by AMI_1:111 ;

now

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

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

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k)))) . d = ((s +* (Start-At ((IC s) -' k))) . da) * ((s +* (Start-At ((IC s) -' k))) . db) by A24, 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 (IncAddr INS,k),s) . d by A25, A28, AMI_3:11
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) . d by AMI_5:80 ;
:: thesis: verum

end;

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k)))) . d = (s +* (Start-At ((IC s) -' k))) . d by A24, AMI_3:11
.= s . d by AMI_5:80
.= (Exec (IncAddr INS,k),s) . d by A25, A29, AMI_3:11
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) . d by AMI_5:80 ;
:: thesis: verum

end;

end;

end;

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

end;

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

then consider da, db being Data-Location such that
A30: INS = Divide da,db by AMI_5:51;
A31: IncAddr INS,k = Divide da,db by A30, Th9;

now

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

suppose A32: da <> db ; :: thesis: Exec INS,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))

A33: (Exec (IncAddr INS,k),s) . (IC SCM ) = Next (IC s) by A31, AMI_3:12;
A34: IC (Exec INS,(s +* (Start-At ((IC s) -' k)))) = Next (IC (s +* (Start-At ((IC s) -' k)))) by A30, AMI_3:12
.= (IC (Exec (IncAddr INS,k),s)) -' k by A2, A33, AMI_1:111
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) by AMI_1:111 ;

now

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

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

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k)))) . d = ((s +* (Start-At ((IC s) -' k))) . da) div ((s +* (Start-At ((IC s) -' k))) . db) by A30, A32, 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 (IncAddr INS,k),s) . d by A31, A32, A35, AMI_3:12
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) . d by AMI_5:80 ;
:: thesis: verum

end;

suppose A36: db = d ; :: thesis: (Exec INS,(s +* (Start-At ((IC s) -' k)))) . b₁ = ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) . b₁

hence (Exec INS,(s +* (Start-At ((IC s) -' k)))) . d = ((s +* (Start-At ((IC s) -' k))) . da) mod ((s +* (Start-At ((IC s) -' k))) . db) by A30, 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 (IncAddr INS,k),s) . d by A31, A36, AMI_3:12
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) . d by AMI_5:80 ;
:: thesis: verum

end;

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k)))) . d = (s +* (Start-At ((IC s) -' k))) . d by A30, AMI_3:12
.= s . d by AMI_5:80
.= (Exec (IncAddr INS,k),s) . d by A31, A37, AMI_3:12
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) . d by AMI_5:80 ;
:: thesis: verum

end;

end;

end;

hence Exec INS,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k)) by A3, A34, AMI_5:26; :: thesis: verum

end;

suppose A38: da = db ; :: thesis: Exec INS,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))

A39: (Exec (IncAddr INS,k),s) . (IC SCM ) = Next (IC s) by A31, AMI_3:12;
A40: IC (Exec INS,(s +* (Start-At ((IC s) -' k)))) = Next (IC (s +* (Start-At ((IC s) -' k)))) by A30, AMI_3:12
.= (IC (Exec (IncAddr INS,k),s)) -' k by A2, A39, AMI_1:111
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) by AMI_1:111 ;

now

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

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

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k)))) . d = ((s +* (Start-At ((IC s) -' k))) . da) mod ((s +* (Start-At ((IC s) -' k))) . db) by A30, A38, 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 (IncAddr INS,k),s) . d by A31, A38, A41, AMI_3:12
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) . d by AMI_5:80 ;
:: thesis: verum

end;

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k)))) . d = (s +* (Start-At ((IC s) -' k))) . d by A30, A38, AMI_3:12
.= s . d by AMI_5:80
.= (Exec (IncAddr INS,k),s) . d by A31, A38, A42, AMI_3:12
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) . d by AMI_5:80 ;
:: thesis: verum

end;

end;

end;

hence Exec INS,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k)) by A3, A40, AMI_5:26; :: thesis: verum

end;

end;

end;

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

end;

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

then consider loc being Instruction-Location of SCM such that
A43: INS = goto loc by AMI_5:52;
A44: IncAddr INS,k = goto (loc + k) by A43, Th10;
then A45: IC (Exec (IncAddr INS,k),s) = loc + k by AMI_3:13;
A46: IC (Exec INS,(s +* (Start-At ((IC s) -' k)))) = loc by A43, AMI_3:13
.= (IC (Exec (IncAddr INS,k),s)) -' k by A45, NAT_D:34
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) by AMI_1:111 ;

now

let d be Data-Location ; :: thesis: (Exec INS,(s +* (Start-At ((IC s) -' k)))) . d = ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) . d
thus (Exec INS,(s +* (Start-At ((IC s) -' k)))) . d = (s +* (Start-At ((IC s) -' k))) . d by A43, AMI_3:13
.= s . d by AMI_5:80
.= (Exec (IncAddr INS,k),s) . d by A44, AMI_3:13
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) . d by AMI_5:80 ; :: thesis: verum

end;

hence Exec INS,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k)) by A3, A46, AMI_5:26; :: thesis: verum

end;

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

then consider loc being Instruction-Location of SCM , da being Data-Location such that
A47: INS = da =0_goto loc by AMI_5:53;
A48: IncAddr INS,k = da =0_goto (loc + k) by A47, Th11;

A49: now

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

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

then A51: (s +* (Start-At ((IC s) -' k))) . da = 0 by AMI_5:80;
A52: IC (Exec (IncAddr INS,k),s) = loc + k by A48, A50, AMI_3:14;
IC (Exec INS,(s +* (Start-At ((IC s) -' k)))) = loc by A47, A51, AMI_3:14
.= (IC (Exec (IncAddr INS,k),s)) -' k by A52, NAT_D:34
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) by AMI_1:111 ;
hence IC (Exec INS,(s +* (Start-At ((IC s) -' k)))) = IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) ; :: thesis: verum

end;

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

then A54: (s +* (Start-At ((IC s) -' k))) . da <> 0 by AMI_5:80;
A55: (Exec (IncAddr INS,k),s) . (IC SCM ) = Next (IC s) by A48, A53, AMI_3:14;
IC (Exec INS,(s +* (Start-At ((IC s) -' k)))) = Next (IC (s +* (Start-At ((IC s) -' k)))) by A47, A54, AMI_3:14
.= (IC (Exec (IncAddr INS,k),s)) -' k by A2, A55, AMI_1:111
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) by AMI_1:111 ;
hence IC (Exec INS,(s +* (Start-At ((IC s) -' k)))) = IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) ; :: thesis: verum

end;

end;

end;

now

let d be Data-Location ; :: thesis: (Exec INS,(s +* (Start-At ((IC s) -' k)))) . d = ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) . d
thus (Exec INS,(s +* (Start-At ((IC s) -' k)))) . d = (s +* (Start-At ((IC s) -' k))) . d by A47, AMI_3:14
.= s . d by AMI_5:80
.= (Exec (IncAddr INS,k),s) . d by A48, AMI_3:14
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) . d by AMI_5:80 ; :: thesis: verum

end;

hence Exec INS,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k)) by A3, A49, AMI_5:26; :: thesis: verum

end;

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

then consider loc being Instruction-Location of SCM , da being Data-Location such that
A56: INS = da >0_goto loc by AMI_5:54;
A57: IncAddr INS,k = da >0_goto (loc + k) by A56, Th12;

A58: now

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

suppose A59: s . da > 0 ; :: thesis: IC (Exec INS,(s +* (Start-At ((IC s) -' k)))) = IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k)))

then A60: (s +* (Start-At ((IC s) -' k))) . da > 0 by AMI_5:80;
A61: IC (Exec (IncAddr INS,k),s) = loc + k by A57, A59, AMI_3:15;
IC (Exec INS,(s +* (Start-At ((IC s) -' k)))) = loc by A56, A60, AMI_3:15
.= (IC (Exec (IncAddr INS,k),s)) -' k by A61, NAT_D:34
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) by AMI_1:111 ;
hence IC (Exec INS,(s +* (Start-At ((IC s) -' k)))) = IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) ; :: thesis: verum

end;

suppose A62: s . da <= 0 ; :: thesis: IC (Exec INS,(s +* (Start-At ((IC s) -' k)))) = IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k)))

then A63: (s +* (Start-At ((IC s) -' k))) . da <= 0 by AMI_5:80;
A64: (Exec (IncAddr INS,k),s) . (IC SCM ) = Next (IC s) by A57, A62, AMI_3:15;
IC (Exec INS,(s +* (Start-At ((IC s) -' k)))) = Next (IC (s +* (Start-At ((IC s) -' k)))) by A56, A63, AMI_3:15
.= (IC (Exec (IncAddr INS,k),s)) -' k by A2, A64, AMI_1:111
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) by AMI_1:111 ;
hence IC (Exec INS,(s +* (Start-At ((IC s) -' k)))) = IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) ; :: thesis: verum

end;

end;

end;

now

let d be Data-Location ; :: thesis: (Exec INS,(s +* (Start-At ((IC s) -' k)))) . d = ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) . d
thus (Exec INS,(s +* (Start-At ((IC s) -' k)))) . d = (s +* (Start-At ((IC s) -' k))) . d by A56, AMI_3:15
.= s . d by AMI_5:80
.= (Exec (IncAddr INS,k),s) . d by A57, AMI_3:15
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))) . d by AMI_5:80 ; :: thesis: verum

end;

hence Exec INS,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k)) by A3, A58, AMI_5:26; :: thesis: verum

end;

end;