let INS be Instruction of SCM+FSA ; :: thesis: for s being State of SCM+FSA
for p being FinPartState of SCM+FSA
for i, j, k being Element of NAT st IC s = j + k holds
Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )
let s be State of SCM+FSA ; :: thesis: for p being FinPartState of SCM+FSA
for i, j, k being Element of NAT st IC s = j + k holds
Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )
let p be FinPartState of SCM+FSA ; :: thesis: for i, j, k being Element of NAT st IC s = j + k holds
Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )
let i, j, k be Element of NAT ; :: thesis: ( IC s = j + k implies Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA ) )

A1: now

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

end;

A2: ( not InsCode INS <= 9 + 1 or InsCode INS <= 8 + 1 or InsCode INS = 10 ) by NAT_1:8;
A3: ( not InsCode INS <= 10 + 1 or InsCode INS <= 10 or InsCode INS = 11 ) by NAT_1:8;
A4: InsCode INS <= 11 + 1 by SCMFSA_2:35;
assume A5: IC s = j + k ; :: thesis: Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )
then A6: succ ((IC s) -' k) = succ ((j + k) -' k)
.= succ j by NAT_D:34
.= j + 1 by NAT_1:39
.= ((j + 1) + k) -' k by NAT_D:34
.= ((j + 1) + k) -' k
.= ((j + k) + 1) -' k
.= (succ (IC s)) -' k by A5, 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 or InsCode INS = 9 or InsCode INS = 10 or InsCode INS = 11 or InsCode INS = 12 ) by A4, A3, A2, NAT_1:8, NAT_1:33;

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

A8: IncAddr (halt SCM+FSA ),k = halt SCM+FSA by Th8;
A9: INS = halt SCM+FSA by A7, SCMFSA_2:122;
hence Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA )) = s +* (Start-At ((IC s) -' k),SCM+FSA ) by AMI_1:def 8
.= s +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA ) by A9, A8, AMI_1:def 8
.= (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA ) by A9, A8, AMI_1:def 8 ;
:: thesis: verum

end;

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

then consider da, db being Int-Location such that
A10: INS = da := db by SCMFSA_2:54;
A11: IncAddr INS,k = da := db by A10, Th9;

A12: now

let d be FinSeq-Location ; :: thesis: (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d
thus (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) -' k),SCM+FSA )) . d by A10, SCMFSA_2:89
.= s . d by SCMFSA_3:12
.= (Exec (IncAddr INS,k),s) . d by A11, SCMFSA_2:89
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:12 ; :: thesis: verum

end;

A13: now

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

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

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) -' k),SCM+FSA )) . db by A10, SCMFSA_2:89
.= s . db by SCMFSA_3:11
.= (Exec (IncAddr INS,k),s) . d by A11, A14, SCMFSA_2:89
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) -' k),SCM+FSA )) . d by A10, SCMFSA_2:89
.= s . d by SCMFSA_3:11
.= (Exec (IncAddr INS,k),s) . d by A11, A15, SCMFSA_2:89
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

end;

end;

IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) = succ (IC (s +* (Start-At ((IC s) -' k),SCM+FSA ))) by A10, SCMFSA_2:89
.= (succ (IC s)) -' k by A6, FUNCT_4:121
.= (IC (Exec (IncAddr INS,k),s)) -' k by A11, SCMFSA_2:89
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) by FUNCT_4:121 ;
hence Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA ) by A1, A12, A13, SCMFSA_2:86; :: thesis: verum

end;

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

then consider da, db being Int-Location such that
A16: INS = AddTo da,db by SCMFSA_2:55;
A17: IncAddr INS,k = AddTo da,db by A16, Th10;

A18: now

let d be FinSeq-Location ; :: thesis: (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d
thus (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) -' k),SCM+FSA )) . d by A16, SCMFSA_2:90
.= s . d by SCMFSA_3:12
.= (Exec (IncAddr INS,k),s) . d by A17, SCMFSA_2:90
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:12 ; :: thesis: verum

end;

A19: now

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

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

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = ((s +* (Start-At ((IC s) -' k),SCM+FSA )) . da) + ((s +* (Start-At ((IC s) -' k),SCM+FSA )) . db) by A16, SCMFSA_2:90
.= (s . da) + ((s +* (Start-At ((IC s) -' k),SCM+FSA )) . db) by SCMFSA_3:11
.= (s . da) + (s . db) by SCMFSA_3:11
.= (Exec (IncAddr INS,k),s) . d by A17, A20, SCMFSA_2:90
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) -' k),SCM+FSA )) . d by A16, SCMFSA_2:90
.= s . d by SCMFSA_3:11
.= (Exec (IncAddr INS,k),s) . d by A17, A21, SCMFSA_2:90
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

end;

end;

IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) = succ (IC (s +* (Start-At ((IC s) -' k),SCM+FSA ))) by A16, SCMFSA_2:90
.= (succ (IC s)) -' k by A6, FUNCT_4:121
.= (IC (Exec (IncAddr INS,k),s)) -' k by A17, SCMFSA_2:90
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) by FUNCT_4:121 ;
hence Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA ) by A1, A18, A19, SCMFSA_2:86; :: thesis: verum

end;

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

then consider da, db being Int-Location such that
A22: INS = SubFrom da,db by SCMFSA_2:56;
A23: IncAddr INS,k = SubFrom da,db by A22, Th11;

A24: now

let d be FinSeq-Location ; :: thesis: (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d
thus (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) -' k),SCM+FSA )) . d by A22, SCMFSA_2:91
.= s . d by SCMFSA_3:12
.= (Exec (IncAddr INS,k),s) . d by A23, SCMFSA_2:91
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:12 ; :: thesis: verum

end;

A25: now

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

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

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = ((s +* (Start-At ((IC s) -' k),SCM+FSA )) . da) - ((s +* (Start-At ((IC s) -' k),SCM+FSA )) . db) by A22, SCMFSA_2:91
.= (s . da) - ((s +* (Start-At ((IC s) -' k),SCM+FSA )) . db) by SCMFSA_3:11
.= (s . da) - (s . db) by SCMFSA_3:11
.= (Exec (IncAddr INS,k),s) . d by A23, A26, SCMFSA_2:91
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) -' k),SCM+FSA )) . d by A22, SCMFSA_2:91
.= s . d by SCMFSA_3:11
.= (Exec (IncAddr INS,k),s) . d by A23, A27, SCMFSA_2:91
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

end;

end;

IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) = succ (IC (s +* (Start-At ((IC s) -' k),SCM+FSA ))) by A22, SCMFSA_2:91
.= (succ (IC s)) -' k by A6, FUNCT_4:121
.= (IC (Exec (IncAddr INS,k),s)) -' k by A23, SCMFSA_2:91
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) by FUNCT_4:121 ;
hence Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA ) by A1, A24, A25, SCMFSA_2:86; :: thesis: verum

end;

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

then consider da, db being Int-Location such that
A28: INS = MultBy da,db by SCMFSA_2:57;
A29: IncAddr INS,k = MultBy da,db by A28, Th12;

A30: now

let d be FinSeq-Location ; :: thesis: (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d
thus (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) -' k),SCM+FSA )) . d by A28, SCMFSA_2:92
.= s . d by SCMFSA_3:12
.= (Exec (IncAddr INS,k),s) . d by A29, SCMFSA_2:92
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:12 ; :: thesis: verum

end;

A31: now

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

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

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = ((s +* (Start-At ((IC s) -' k),SCM+FSA )) . da) * ((s +* (Start-At ((IC s) -' k),SCM+FSA )) . db) by A28, SCMFSA_2:92
.= (s . da) * ((s +* (Start-At ((IC s) -' k),SCM+FSA )) . db) by SCMFSA_3:11
.= (s . da) * (s . db) by SCMFSA_3:11
.= (Exec (IncAddr INS,k),s) . d by A29, A32, SCMFSA_2:92
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) -' k),SCM+FSA )) . d by A28, SCMFSA_2:92
.= s . d by SCMFSA_3:11
.= (Exec (IncAddr INS,k),s) . d by A29, A33, SCMFSA_2:92
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

end;

end;

IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) = succ (IC (s +* (Start-At ((IC s) -' k),SCM+FSA ))) by A28, SCMFSA_2:92
.= (succ (IC s)) -' k by A6, FUNCT_4:121
.= (IC (Exec (IncAddr INS,k),s)) -' k by A29, SCMFSA_2:92
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) by FUNCT_4:121 ;
hence Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA ) by A1, A30, A31, SCMFSA_2:86; :: thesis: verum

end;

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

then consider da, db being Int-Location such that
A34: INS = Divide da,db by SCMFSA_2:58;
A35: IncAddr INS,k = Divide da,db by A34, Th13;

now

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

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

A37: now

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

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

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = ((s +* (Start-At ((IC s) -' k),SCM+FSA )) . da) div ((s +* (Start-At ((IC s) -' k),SCM+FSA )) . db) by A34, A36, SCMFSA_2:93
.= (s . da) div ((s +* (Start-At ((IC s) -' k),SCM+FSA )) . db) by SCMFSA_3:11
.= (s . da) div (s . db) by SCMFSA_3:11
.= (Exec (IncAddr INS,k),s) . d by A35, A36, A38, SCMFSA_2:93
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = ((s +* (Start-At ((IC s) -' k),SCM+FSA )) . da) mod ((s +* (Start-At ((IC s) -' k),SCM+FSA )) . db) by A34, SCMFSA_2:93
.= (s . da) mod ((s +* (Start-At ((IC s) -' k),SCM+FSA )) . db) by SCMFSA_3:11
.= (s . da) mod (s . db) by SCMFSA_3:11
.= (Exec (IncAddr INS,k),s) . d by A35, A39, SCMFSA_2:93
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) -' k),SCM+FSA )) . d by A34, SCMFSA_2:93
.= s . d by SCMFSA_3:11
.= (Exec (IncAddr INS,k),s) . d by A35, A40, SCMFSA_2:93
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

end;

end;

A41: now

let d be FinSeq-Location ; :: thesis: (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d
thus (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) -' k),SCM+FSA )) . d by A34, SCMFSA_2:93
.= s . d by SCMFSA_3:12
.= (Exec (IncAddr INS,k),s) . d by A35, SCMFSA_2:93
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:12 ; :: thesis: verum

end;

IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) = succ (IC (s +* (Start-At ((IC s) -' k),SCM+FSA ))) by A34, SCMFSA_2:93
.= (succ (IC s)) -' k by A6, FUNCT_4:121
.= (IC (Exec (IncAddr INS,k),s)) -' k by A35, SCMFSA_2:93
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) by FUNCT_4:121 ;
hence Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA ) by A1, A41, A37, SCMFSA_2:86; :: thesis: verum

end;

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

A43: now

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

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

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = ((s +* (Start-At ((IC s) -' k),SCM+FSA )) . da) mod ((s +* (Start-At ((IC s) -' k),SCM+FSA )) . db) by A34, A42, SCMFSA_2:94
.= (s . da) mod ((s +* (Start-At ((IC s) -' k),SCM+FSA )) . db) by SCMFSA_3:11
.= (s . da) mod (s . db) by SCMFSA_3:11
.= (Exec (IncAddr INS,k),s) . d by A35, A42, A44, SCMFSA_2:94
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) -' k),SCM+FSA )) . d by A34, A42, SCMFSA_2:94
.= s . d by SCMFSA_3:11
.= (Exec (IncAddr INS,k),s) . d by A35, A42, A45, SCMFSA_2:94
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

end;

end;

A46: now

let d be FinSeq-Location ; :: thesis: (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d
thus (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) -' k),SCM+FSA )) . d by A34, A42, SCMFSA_2:94
.= s . d by SCMFSA_3:12
.= (Exec (IncAddr INS,k),s) . d by A35, A42, SCMFSA_2:94
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:12 ; :: thesis: verum

end;

IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) = succ (IC (s +* (Start-At ((IC s) -' k),SCM+FSA ))) by A34, A42, SCMFSA_2:94
.= (succ (IC s)) -' k by A6, FUNCT_4:121
.= (IC (Exec (IncAddr INS,k),s)) -' k by A35, A42, SCMFSA_2:94
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) by FUNCT_4:121 ;
hence Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA ) by A1, A46, A43, SCMFSA_2:86; :: thesis: verum

end;

end;

end;

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

end;

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

then consider loc being Element of NAT such that
A47: INS = goto loc by SCMFSA_2:59;
A48: IncAddr INS,k = goto (loc + k) by A47, Th14;
then A49: IC (Exec (IncAddr INS,k),s) = loc + k by SCMFSA_2:95;

A50: now

let d be Int-Location ; :: thesis: (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d
thus (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) -' k),SCM+FSA )) . d by A47, SCMFSA_2:95
.= s . d by SCMFSA_3:11
.= (Exec (IncAddr INS,k),s) . d by A48, SCMFSA_2:95
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:11 ; :: thesis: verum

end;

A51: now

let d be FinSeq-Location ; :: thesis: (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d
thus (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) -' k),SCM+FSA )) . d by A47, SCMFSA_2:95
.= s . d by SCMFSA_3:12
.= (Exec (IncAddr INS,k),s) . d by A48, SCMFSA_2:95
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:12 ; :: thesis: verum

end;

IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) = loc by A47, SCMFSA_2:95
.= (IC (Exec (IncAddr INS,k),s)) -' k by A49, NAT_D:34
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) by FUNCT_4:121 ;
hence Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA ) by A1, A51, A50, SCMFSA_2:86; :: thesis: verum

end;

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

then consider loc being Element of NAT , da being Int-Location such that
A52: INS = da =0_goto loc by SCMFSA_2:60;
A53: IncAddr INS,k = da =0_goto (loc + k) by A52, Th15;

A54: now

let d be Int-Location ; :: thesis: (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d
thus (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) -' k),SCM+FSA )) . d by A52, SCMFSA_2:96
.= s . d by SCMFSA_3:11
.= (Exec (IncAddr INS,k),s) . d by A53, SCMFSA_2:96
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:11 ; :: thesis: verum

end;

A55: now

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

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

then A57: IC (Exec (IncAddr INS,k),s) = loc + k by A53, SCMFSA_2:96;
(s +* (Start-At ((IC s) -' k),SCM+FSA )) . da = 0 by A56, SCMFSA_3:11;
then IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) = loc by A52, SCMFSA_2:96
.= (IC (Exec (IncAddr INS,k),s)) -' k by A57, NAT_D:34
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) by FUNCT_4:121 ;
hence IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) = IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) ; :: thesis: verum

end;

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

then (s +* (Start-At ((IC s) -' k),SCM+FSA )) . da <> 0 by SCMFSA_3:11;
then IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) = succ (IC (s +* (Start-At ((IC s) -' k),SCM+FSA ))) by A52, SCMFSA_2:96
.= (succ (IC s)) -' k by A6, FUNCT_4:121
.= (IC (Exec (IncAddr INS,k),s)) -' k by A53, A58, SCMFSA_2:96
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) by FUNCT_4:121 ;
hence IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) = IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) ; :: thesis: verum

end;

end;

end;

now

let d be FinSeq-Location ; :: thesis: (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d
thus (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) -' k),SCM+FSA )) . d by A52, SCMFSA_2:96
.= s . d by SCMFSA_3:12
.= (Exec (IncAddr INS,k),s) . d by A53, SCMFSA_2:96
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:12 ; :: thesis: verum

end;

hence Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA ) by A1, A55, A54, SCMFSA_2:86; :: thesis: verum

end;

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

then consider loc being Element of NAT , da being Int-Location such that
A59: INS = da >0_goto loc by SCMFSA_2:61;
A60: IncAddr INS,k = da >0_goto (loc + k) by A59, Th16;

A61: now

let d be Int-Location ; :: thesis: (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d
thus (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) -' k),SCM+FSA )) . d by A59, SCMFSA_2:97
.= s . d by SCMFSA_3:11
.= (Exec (IncAddr INS,k),s) . d by A60, SCMFSA_2:97
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:11 ; :: thesis: verum

end;

A62: now

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

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

then A64: IC (Exec (IncAddr INS,k),s) = loc + k by A60, SCMFSA_2:97;
(s +* (Start-At ((IC s) -' k),SCM+FSA )) . da > 0 by A63, SCMFSA_3:11;
then IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) = loc by A59, SCMFSA_2:97
.= (IC (Exec (IncAddr INS,k),s)) -' k by A64, NAT_D:34
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) by FUNCT_4:121 ;
hence IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) = IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) ; :: thesis: verum

end;

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

then (s +* (Start-At ((IC s) -' k),SCM+FSA )) . da <= 0 by SCMFSA_3:11;
then IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) = succ (IC (s +* (Start-At ((IC s) -' k),SCM+FSA ))) by A59, SCMFSA_2:97
.= (succ (IC s)) -' k by A6, FUNCT_4:121
.= (IC (Exec (IncAddr INS,k),s)) -' k by A60, A65, SCMFSA_2:97
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) by FUNCT_4:121 ;
hence IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) = IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) ; :: thesis: verum

end;

end;

end;

now

let d be FinSeq-Location ; :: thesis: (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d
thus (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) -' k),SCM+FSA )) . d by A59, SCMFSA_2:97
.= s . d by SCMFSA_3:12
.= (Exec (IncAddr INS,k),s) . d by A60, SCMFSA_2:97
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:12 ; :: thesis: verum

end;

hence Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA ) by A1, A62, A61, SCMFSA_2:86; :: thesis: verum

end;

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

then consider db, da being Int-Location , f being FinSeq-Location such that
A66: INS = da := f,db by SCMFSA_2:62;
A67: IncAddr INS,k = da := f,db by A66, Th17;

A68: now

let d be FinSeq-Location ; :: thesis: (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d
thus (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) -' k),SCM+FSA )) . d by A66, SCMFSA_2:98
.= s . d by SCMFSA_3:12
.= (Exec (IncAddr INS,k),s) . d by A67, SCMFSA_2:98
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:12 ; :: thesis: verum

end;

A69: now

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

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

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

consider m being Element of NAT such that
A71: m = abs (s . db) and
A72: (Exec (IncAddr INS,k),s) . da = (s . f) /. m by A67, SCMFSA_2:98;
( ex m9 being Element of NAT st
( m9 = abs ((s +* (Start-At ((IC s) -' k),SCM+FSA )) . db) & (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . da = ((s +* (Start-At ((IC s) -' k),SCM+FSA )) . f) /. m9 ) & (s +* (Start-At ((IC s) -' k),SCM+FSA )) . db = s . db ) by A66, SCMFSA_2:98, SCMFSA_3:11;
hence (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s . f) /. m by A70, A71, SCMFSA_3:12
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by A70, A72, SCMFSA_3:11 ;
:: thesis: verum

end;

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) -' k),SCM+FSA )) . d by A66, SCMFSA_2:98
.= s . d by SCMFSA_3:11
.= (Exec (IncAddr INS,k),s) . d by A67, A73, SCMFSA_2:98
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

end;

end;

IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) = succ (IC (s +* (Start-At ((IC s) -' k),SCM+FSA ))) by A66, SCMFSA_2:98
.= (succ (IC s)) -' k by A6, FUNCT_4:121
.= (IC (Exec (IncAddr INS,k),s)) -' k by A67, SCMFSA_2:98
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) by FUNCT_4:121 ;
hence Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA ) by A1, A68, A69, SCMFSA_2:86; :: thesis: verum

end;

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

then consider db, da being Int-Location , f being FinSeq-Location such that
A74: INS = f,db := da by SCMFSA_2:63;
A75: IncAddr INS,k = f,db := da by A74, Th18;

A76: now

let d be Int-Location ; :: thesis: (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d
thus (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) -' k),SCM+FSA )) . d by A74, SCMFSA_2:99
.= s . d by SCMFSA_3:11
.= (Exec (IncAddr INS,k),s) . d by A75, SCMFSA_2:99
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:11 ; :: thesis: verum

end;

A77: now

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

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

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

A79: (s +* (Start-At ((IC s) -' k),SCM+FSA )) . db = s . db by SCMFSA_3:11;
consider m being Element of NAT such that
A80: m = abs (s . db) and
A81: (Exec (IncAddr INS,k),s) . f = (s . f) +* m,(s . da) by A75, SCMFSA_2:99;
( ex m9 being Element of NAT st
( m9 = abs ((s +* (Start-At ((IC s) -' k),SCM+FSA )) . db) & (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . f = ((s +* (Start-At ((IC s) -' k),SCM+FSA )) . f) +* m9,((s +* (Start-At ((IC s) -' k),SCM+FSA )) . da) ) & (s +* (Start-At ((IC s) -' k),SCM+FSA )) . da = s . da ) by A74, SCMFSA_2:99, SCMFSA_3:11;
hence (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s . f) +* m,(s . da) by A78, A80, A79, SCMFSA_3:12
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by A78, A81, SCMFSA_3:12 ;
:: thesis: verum

end;

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) -' k),SCM+FSA )) . d by A74, SCMFSA_2:99
.= s . d by SCMFSA_3:12
.= (Exec (IncAddr INS,k),s) . d by A75, A82, SCMFSA_2:99
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:12 ;
:: thesis: verum

end;

end;

end;

IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) = succ (IC (s +* (Start-At ((IC s) -' k),SCM+FSA ))) by A74, SCMFSA_2:99
.= (succ (IC s)) -' k by A6, FUNCT_4:121
.= (IC (Exec (IncAddr INS,k),s)) -' k by A75, SCMFSA_2:99
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) by FUNCT_4:121 ;
hence Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA ) by A1, A76, A77, SCMFSA_2:86; :: thesis: verum

end;

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

then consider da being Int-Location , f being FinSeq-Location such that
A83: INS = da :=len f by SCMFSA_2:64;
A84: IncAddr INS,k = da :=len f by A83, Th19;

A85: now

let d be FinSeq-Location ; :: thesis: (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d
thus (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) -' k),SCM+FSA )) . d by A83, SCMFSA_2:100
.= s . d by SCMFSA_3:12
.= (Exec (IncAddr INS,k),s) . d by A84, SCMFSA_2:100
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:12 ; :: thesis: verum

end;

A86: now

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

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

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = len ((s +* (Start-At ((IC s) -' k),SCM+FSA )) . f) by A83, SCMFSA_2:100
.= len (s . f) by SCMFSA_3:12
.= (Exec (IncAddr INS,k),s) . d by A84, A87, SCMFSA_2:100
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) -' k),SCM+FSA )) . d by A83, SCMFSA_2:100
.= s . d by SCMFSA_3:11
.= (Exec (IncAddr INS,k),s) . d by A84, A88, SCMFSA_2:100
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

end;

end;

IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) = succ (IC (s +* (Start-At ((IC s) -' k),SCM+FSA ))) by A83, SCMFSA_2:100
.= (succ (IC s)) -' k by A6, FUNCT_4:121
.= (IC (Exec (IncAddr INS,k),s)) -' k by A84, SCMFSA_2:100
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) by FUNCT_4:121 ;
hence Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA ) by A1, A85, A86, SCMFSA_2:86; :: thesis: verum

end;

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

then consider da being Int-Location , f being FinSeq-Location such that
A89: INS = f :=<0,...,0> da by SCMFSA_2:65;
A90: IncAddr INS,k = f :=<0,...,0> da by A89, Th20;

A91: now

let d be Int-Location ; :: thesis: (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d
thus (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) -' k),SCM+FSA )) . d by A89, SCMFSA_2:101
.= s . d by SCMFSA_3:11
.= (Exec (IncAddr INS,k),s) . d by A90, SCMFSA_2:101
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:11 ; :: thesis: verum

end;

A92: now

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

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

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

A94: (s +* (Start-At ((IC s) -' k),SCM+FSA )) . da = s . da by SCMFSA_3:11;
( ex m being Element of NAT st
( m = abs (s . da) & (Exec (IncAddr INS,k),s) . f = m |-> 0 ) & ex m9 being Element of NAT st
( m9 = abs ((s +* (Start-At ((IC s) -' k),SCM+FSA )) . da) & (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . f = m9 |-> 0 ) ) by A89, A90, SCMFSA_2:101;
hence (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by A93, A94, SCMFSA_3:12; :: thesis: verum

end;

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

hence (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) -' k),SCM+FSA )) . d by A89, SCMFSA_2:101
.= s . d by SCMFSA_3:12
.= (Exec (IncAddr INS,k),s) . d by A90, A95, SCMFSA_2:101
.= ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) . d by SCMFSA_3:12 ;
:: thesis: verum

end;

end;

end;

IC (Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA ))) = succ (IC (s +* (Start-At ((IC s) -' k),SCM+FSA ))) by A89, SCMFSA_2:101
.= (succ (IC s)) -' k by A6, FUNCT_4:121
.= (IC (Exec (IncAddr INS,k),s)) -' k by A90, SCMFSA_2:101
.= IC ((Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA )) by FUNCT_4:121 ;
hence Exec INS,(s +* (Start-At ((IC s) -' k),SCM+FSA )) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k),SCM+FSA ) by A1, A91, A92, SCMFSA_2:86; :: thesis: verum

end;

end;