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),SCM )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM )
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),SCM )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM )
let j, k be Element of NAT ; :: thesis: ( IC s = j + k implies Exec INS,(s +* (Start-At ((IC s) -' k),SCM )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM ) )

A1: now

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

end;

assume A2: IC s = j + k ; :: thesis: Exec INS,(s +* (Start-At ((IC s) -' k),SCM )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM )
then A3: succ ((IC s) -' k) = succ j by NAT_D:34
.= j + 1 by NAT_1:39
.= ((j + 1) + k) -' k by NAT_D:34
.= ((j + k) + 1) -' k
.= (succ (IC s)) -' k by A2, NAT_1:39 ;

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 A4: InsCode INS = 0 ; :: thesis: Exec INS,(s +* (Start-At ((IC s) -' k),SCM )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM )

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

end;

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

then consider da, db being Data-Location such that
A7: INS = da := db by AMI_5:47;
A8: IncAddr INS,k = da := db by A7, Th5;
then A9: (Exec (IncAddr INS,k),s) . (IC SCM ) = succ (IC s) by AMI_3:8;

A10: now

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

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

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

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

end;

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

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

end;

end;

end;

IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM ))) = succ (IC (s +* (Start-At ((IC s) -' k),SCM ))) by A7, AMI_3:8
.= (IC (Exec (IncAddr INS,k),s)) -' k by A3, A9, AMI_1:111
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM )) by AMI_1:111 ;
hence Exec INS,(s +* (Start-At ((IC s) -' k),SCM )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM ) by A1, A10, AMI_5:26; :: thesis: verum

end;

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

then consider da, db being Data-Location such that
A13: INS = AddTo da,db by AMI_5:48;
A14: IncAddr INS,k = AddTo da,db by A13, Th6;
then A15: (Exec (IncAddr INS,k),s) . (IC SCM ) = succ (IC s) by AMI_3:9;

A16: now

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

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

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

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

end;

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

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

end;

end;

end;

IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM ))) = succ (IC (s +* (Start-At ((IC s) -' k),SCM ))) by A13, AMI_3:9
.= (IC (Exec (IncAddr INS,k),s)) -' k by A3, A15, AMI_1:111
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM )) by AMI_1:111 ;
hence Exec INS,(s +* (Start-At ((IC s) -' k),SCM )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM ) by A1, A16, AMI_5:26; :: thesis: verum

end;

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

then consider da, db being Data-Location such that
A19: INS = SubFrom da,db by AMI_5:49;
A20: IncAddr INS,k = SubFrom da,db by A19, Th7;
then A21: (Exec (IncAddr INS,k),s) . (IC SCM ) = succ (IC s) by AMI_3:10;

A22: now

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

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

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

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

end;

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

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

end;

end;

end;

IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM ))) = succ (IC (s +* (Start-At ((IC s) -' k),SCM ))) by A19, AMI_3:10
.= (IC (Exec (IncAddr INS,k),s)) -' k by A3, A21, AMI_1:111
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM )) by AMI_1:111 ;
hence Exec INS,(s +* (Start-At ((IC s) -' k),SCM )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM ) by A1, A22, AMI_5:26; :: thesis: verum

end;

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

then consider da, db being Data-Location such that
A25: INS = MultBy da,db by AMI_5:50;
A26: IncAddr INS,k = MultBy da,db by A25, Th8;
then A27: (Exec (IncAddr INS,k),s) . (IC SCM ) = succ (IC s) by AMI_3:11;

A28: now

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

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

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

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

end;

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

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

end;

end;

end;

IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM ))) = succ (IC (s +* (Start-At ((IC s) -' k),SCM ))) by A25, AMI_3:11
.= (IC (Exec (IncAddr INS,k),s)) -' k by A3, A27, AMI_1:111
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM )) by AMI_1:111 ;
hence Exec INS,(s +* (Start-At ((IC s) -' k),SCM )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM ) by A1, A28, AMI_5:26; :: thesis: verum

end;

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

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

now

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

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

A34: now

let d be Data-Location ; :: thesis: (Exec INS,(s +* (Start-At ((IC s) -' k),SCM ))) . b₁ = ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM )) . 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),SCM ))) . b₁ = ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM )) . b₁

hence (Exec INS,(s +* (Start-At ((IC s) -' k),SCM ))) . d = ((s +* (Start-At ((IC s) -' k),SCM )) . da) div ((s +* (Start-At ((IC s) -' k),SCM )) . db) by A31, A33, AMI_3:12
.= (s . da) div ((s +* (Start-At ((IC s) -' k),SCM )) . db) by AMI_5:80
.= (s . da) div (s . db) by AMI_5:80
.= (Exec (IncAddr INS,k),s) . d by A32, A33, A35, AMI_3:12
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM )) . d by AMI_5:80 ;
:: thesis: verum

end;

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k),SCM ))) . d = ((s +* (Start-At ((IC s) -' k),SCM )) . da) mod ((s +* (Start-At ((IC s) -' k),SCM )) . db) by A31, AMI_3:12
.= (s . da) mod ((s +* (Start-At ((IC s) -' k),SCM )) . db) by AMI_5:80
.= (s . da) mod (s . db) by AMI_5:80
.= (Exec (IncAddr INS,k),s) . d by A32, A36, AMI_3:12
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM )) . d by AMI_5:80 ;
:: thesis: verum

end;

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

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

end;

end;

end;

A38: (Exec (IncAddr INS,k),s) . (IC SCM ) = succ (IC s) by A32, AMI_3:12;
IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM ))) = succ (IC (s +* (Start-At ((IC s) -' k),SCM ))) by A31, AMI_3:12
.= (IC (Exec (IncAddr INS,k),s)) -' k by A3, A38, AMI_1:111
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM )) by AMI_1:111 ;
hence Exec INS,(s +* (Start-At ((IC s) -' k),SCM )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM ) by A1, A34, AMI_5:26; :: thesis: verum

end;

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

A40: now

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

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

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k),SCM ))) . d = ((s +* (Start-At ((IC s) -' k),SCM )) . da) mod ((s +* (Start-At ((IC s) -' k),SCM )) . db) by A31, A39, AMI_3:12
.= (s . da) mod ((s +* (Start-At ((IC s) -' k),SCM )) . db) by AMI_5:80
.= (s . da) mod (s . db) by AMI_5:80
.= (Exec (IncAddr INS,k),s) . d by A32, A39, A41, AMI_3:12
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM )) . d by AMI_5:80 ;
:: thesis: verum

end;

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

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

end;

end;

end;

A43: (Exec (IncAddr INS,k),s) . (IC SCM ) = succ (IC s) by A32, AMI_3:12;
IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM ))) = succ (IC (s +* (Start-At ((IC s) -' k),SCM ))) by A31, AMI_3:12
.= (IC (Exec (IncAddr INS,k),s)) -' k by A3, A43, AMI_1:111
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM )) by AMI_1:111 ;
hence Exec INS,(s +* (Start-At ((IC s) -' k),SCM )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM ) by A1, A40, AMI_5:26; :: thesis: verum

end;

end;

end;

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

end;

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

then consider loc being Element of NAT such that
A44: INS = SCM-goto loc by AMI_5:52;
A45: IncAddr INS,k = SCM-goto (loc + k) by A44, Th10;
then A46: IC (Exec (IncAddr INS,k),s) = loc + k by AMI_3:13;

A47: now

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

end;

IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM ))) = loc by A44, AMI_3:13
.= (IC (Exec (IncAddr INS,k),s)) -' k by A46, NAT_D:34
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM )) by AMI_1:111 ;
hence Exec INS,(s +* (Start-At ((IC s) -' k),SCM )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM ) by A1, A47, AMI_5:26; :: thesis: verum

end;

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

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

A50: now

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

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

then A52: IC (Exec (IncAddr INS,k),s) = loc + k by A49, AMI_3:14;
(s +* (Start-At ((IC s) -' k),SCM )) . da = 0 by A51, AMI_5:80;
then IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM ))) = loc by A48, 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),SCM )) by AMI_1:111 ;
hence IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM ))) = IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM )) ; :: thesis: verum

end;

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

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

end;

end;

end;

now

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

end;

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

end;

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

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

A57: now

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

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

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

end;

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

then A61: (Exec (IncAddr INS,k),s) . (IC SCM ) = succ (IC s) by A56, AMI_3:15;
(s +* (Start-At ((IC s) -' k),SCM )) . da <= 0 by A60, AMI_5:80;
then IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM ))) = succ (IC (s +* (Start-At ((IC s) -' k),SCM ))) by A55, AMI_3:15
.= (IC (Exec (IncAddr INS,k),s)) -' k by A3, A61, AMI_1:111
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM )) by AMI_1:111 ;
hence IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM ))) = IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM )) ; :: thesis: verum

end;

end;

end;

now

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

end;

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

end;

end;