let k be Element of NAT ; :: thesis: for s being State of SCM+FSA holds Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k))
let s be State of SCM+FSA ; :: 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;
A3: Next (IC (s +* (Start-At ((IC s) + k)))) = Next (insloc (m + k)) by AMI_1:111
.= insloc ((m + k) + 1) by NAT_1:39
.= insloc ((m + 1) + k)
.= (insloc (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 ;

A4: now

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

A5: InsCode (CurInstr s) <= 11 + 1 by SCMFSA_2:35;
A6: ( not InsCode (CurInstr s) <= 10 + 1 or InsCode (CurInstr s) <= 10 or InsCode (CurInstr s) = 11 ) by NAT_1:8;
A7: ( not InsCode (CurInstr s) <= 9 + 1 or InsCode (CurInstr s) <= 8 + 1 or InsCode (CurInstr s) = 10 ) by NAT_1:8;

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 or InsCode (CurInstr s) = 9 or InsCode (CurInstr s) = 10 or InsCode (CurInstr s) = 11 or InsCode (CurInstr s) = 12 ) by A5, A6, A7, NAT_1:8, NAT_1:33;

suppose A8: 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 A9: CurInstr s = halt SCM+FSA by SCMFSA_2:122;
A10: Following s = Exec (halt SCM+FSA ),s by A8, SCMFSA_2:122
.= s by AMI_1:def 8 ;
thus Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = Exec (halt SCM+FSA ),(s +* (Start-At ((IC s) + k))) by A9, Th8
.= (Following s) +* (Start-At ((IC (Following s)) + k)) by A10, 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 Int-Location such that
A11: CurInstr s = da := db by SCMFSA_2:54;
A12: IncAddr (CurInstr s),k = CurInstr s by A11, Th9;
A13: IC (Exec (CurInstr s),s) = Next (IC s) by A11, SCMFSA_2:89;
A14: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) by A3, A11, SCMFSA_2:89;

A15: now

let d be FinSeq-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 A11, A12, SCMFSA_2:89
.= s . d by SCMFSA_3:12
.= (Exec (CurInstr s),s) . d by A11, SCMFSA_2:89
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by SCMFSA_3:12 ; :: thesis: verum

end;

now

let d be Int-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 A16: 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 A11, SCMFSA_2:89
.= s . db by SCMFSA_3:11
.= (Exec (CurInstr s),s) . d by A11, A16, SCMFSA_2:89
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

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))) . d by A11, SCMFSA_2:89
.= s . d by SCMFSA_3:11
.= (Exec (CurInstr s),s) . d by A11, A17, SCMFSA_2:89
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

end;

end;

hence Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k)) by A4, A12, A13, A14, A15, SCMFSA_2:86; :: 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 Int-Location such that
A18: CurInstr s = AddTo da,db by SCMFSA_2:55;
A19: IncAddr (CurInstr s),k = CurInstr s by A18, Th10;
A20: IC (Exec (CurInstr s),s) = Next (IC s) by A18, SCMFSA_2:90;
A21: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) by A3, A18, SCMFSA_2:90;

A22: now

let d be FinSeq-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 A18, A19, SCMFSA_2:90
.= s . d by SCMFSA_3:12
.= (Exec (CurInstr s),s) . d by A18, SCMFSA_2:90
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by SCMFSA_3:12 ; :: thesis: verum

end;

now

let d be Int-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 A23: da = d ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . b₁

hence (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . d = ((s +* (Start-At ((IC s) + k))) . da) + ((s +* (Start-At ((IC s) + k))) . db) by A18, SCMFSA_2:90
.= (s . da) + ((s +* (Start-At ((IC s) + k))) . db) by SCMFSA_3:11
.= (s . da) + (s . db) by SCMFSA_3:11
.= (Exec (CurInstr s),s) . d by A18, A23, SCMFSA_2:90
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

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

hence (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . d = (s +* (Start-At ((IC s) + k))) . d by A18, SCMFSA_2:90
.= s . d by SCMFSA_3:11
.= (Exec (CurInstr s),s) . d by A18, A24, SCMFSA_2:90
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

end;

end;

hence Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k)) by A4, A19, A20, A21, A22, SCMFSA_2:86; :: 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 Int-Location such that
A25: CurInstr s = SubFrom da,db by SCMFSA_2:56;
A26: IncAddr (CurInstr s),k = CurInstr s by A25, Th11;
A27: IC (Exec (CurInstr s),s) = Next (IC s) by A25, SCMFSA_2:91;
A28: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) by A3, A25, SCMFSA_2:91;

A29: now

let d be FinSeq-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 A25, A26, SCMFSA_2:91
.= s . d by SCMFSA_3:12
.= (Exec (CurInstr s),s) . d by A25, SCMFSA_2:91
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by SCMFSA_3:12 ; :: thesis: verum

end;

now

let d be Int-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 A30: da = d ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . b₁

hence (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . d = ((s +* (Start-At ((IC s) + k))) . da) - ((s +* (Start-At ((IC s) + k))) . db) by A25, SCMFSA_2:91
.= (s . da) - ((s +* (Start-At ((IC s) + k))) . db) by SCMFSA_3:11
.= (s . da) - (s . db) by SCMFSA_3:11
.= (Exec (CurInstr s),s) . d by A25, A30, SCMFSA_2:91
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

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

hence (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . d = (s +* (Start-At ((IC s) + k))) . d by A25, SCMFSA_2:91
.= s . d by SCMFSA_3:11
.= (Exec (CurInstr s),s) . d by A25, A31, SCMFSA_2:91
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

end;

end;

hence Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k)) by A4, A26, A27, A28, A29, SCMFSA_2:86; :: 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 Int-Location such that
A32: CurInstr s = MultBy da,db by SCMFSA_2:57;
A33: IncAddr (CurInstr s),k = CurInstr s by A32, Th12;
A34: IC (Exec (CurInstr s),s) = Next (IC s) by A32, SCMFSA_2:92;
A35: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) by A3, A32, SCMFSA_2:92;

A36: now

let d be FinSeq-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 A32, A33, SCMFSA_2:92
.= s . d by SCMFSA_3:12
.= (Exec (CurInstr s),s) . d by A32, SCMFSA_2:92
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by SCMFSA_3:12 ; :: thesis: verum

end;

now

let d be Int-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 A37: 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 A32, SCMFSA_2:92
.= (s . da) * ((s +* (Start-At ((IC s) + k))) . db) by SCMFSA_3:11
.= (s . da) * (s . db) by SCMFSA_3:11
.= (Exec (CurInstr s),s) . d by A32, A37, SCMFSA_2:92
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

suppose A38: 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 A32, SCMFSA_2:92
.= s . d by SCMFSA_3:11
.= (Exec (CurInstr s),s) . d by A32, A38, SCMFSA_2:92
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

end;

end;

hence Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k)) by A4, A33, A34, A35, A36, SCMFSA_2:86; :: 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 Int-Location such that
A39: CurInstr s = Divide da,db by SCMFSA_2:58;
A40: IncAddr (CurInstr s),k = CurInstr s by A39, Th13;
A41: IC (Exec (CurInstr s),s) = Next (IC s) by A39, SCMFSA_2:93;
A42: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) by A3, A39, SCMFSA_2:93;

A43: now

let d be FinSeq-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 A39, A40, SCMFSA_2:93
.= s . d by SCMFSA_3:12
.= (Exec (CurInstr s),s) . d by A39, SCMFSA_2:93
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by SCMFSA_3:12 ; :: thesis: verum

end;

now

let d be Int-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 A44: 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 A45: 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 A39, A44, SCMFSA_2:93
.= (s . da) div ((s +* (Start-At ((IC s) + k))) . db) by SCMFSA_3:11
.= (s . da) div (s . db) by SCMFSA_3:11
.= (Exec (CurInstr s),s) . d by A39, A44, A45, SCMFSA_2:93
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

suppose A46: 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 A39, SCMFSA_2:93
.= (s . da) mod ((s +* (Start-At ((IC s) + k))) . db) by SCMFSA_3:11
.= (s . da) mod (s . db) by SCMFSA_3:11
.= (Exec (CurInstr s),s) . d by A39, A46, SCMFSA_2:93
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

suppose A47: ( 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 A39, SCMFSA_2:93
.= s . d by SCMFSA_3:11
.= (Exec (CurInstr s),s) . d by A39, A47, SCMFSA_2:93
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

end;

end;

end;

suppose A48: 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 A49: 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 A39, A48, SCMFSA_2:94
.= (s . da) mod ((s +* (Start-At ((IC s) + k))) . da) by SCMFSA_3:11
.= (s . da) mod (s . da) by SCMFSA_3:11
.= (Exec (CurInstr s),s) . d by A39, A48, A49, SCMFSA_2:94
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

suppose A50: 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 A39, A48, SCMFSA_2:94
.= s . d by SCMFSA_3:11
.= (Exec (CurInstr s),s) . d by A39, A48, A50, SCMFSA_2:94
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

end;

end;

end;

end;

end;

hence Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k)) by A4, A40, A41, A42, A43, SCMFSA_2:86; :: 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+FSA such that
A51: CurInstr s = goto loc by SCMFSA_2:59;
A52: IncAddr (CurInstr s),k = goto (loc + k) by A51, Th14;
A53: IC (Exec (CurInstr s),s) = loc by A51, SCMFSA_2:95;
A54: IC (Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k)))) = loc + k by A52, SCMFSA_2:95
.= IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) by A53, AMI_1:111 ;

A55: now

let d be Int-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 A52, SCMFSA_2:95
.= s . d by SCMFSA_3:11
.= (Exec (CurInstr s),s) . d by A51, SCMFSA_2:95
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by SCMFSA_3:11 ; :: thesis: verum

end;

A56: now

let d be FinSeq-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 A52, SCMFSA_2:95
.= s . d by SCMFSA_3:12
.= (Exec (CurInstr s),s) . d by A51, SCMFSA_2:95
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by SCMFSA_3:12 ; :: thesis: verum

end;

now

let d be Instruction-Location of SCM+FSA ; :: thesis: (Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k)))) . d = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d
thus (Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k)))) . d = (s +* (Start-At ((IC s) + k))) . d by AMI_1:def 13
.= s . d by AMI_1:112
.= (Exec (CurInstr s),s) . d by AMI_1:def 13
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by AMI_1:112 ; :: thesis: verum

end;

hence Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k)) by A54, A55, A56, SCMFSA_2:86; :: 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+FSA , da being Int-Location such that
A57: CurInstr s = da =0_goto loc by SCMFSA_2:60;
A58: IncAddr (CurInstr s),k = da =0_goto (loc + k) by A57, Th15;

now

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

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

then A60: (s +* (Start-At ((IC s) + k))) . da = 0 by SCMFSA_3:11;
A61: IC (Exec (CurInstr s),s) = loc by A57, A59, SCMFSA_2:96;
A62: IC (Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k)))) = loc + k by A58, A60, SCMFSA_2:96
.= IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) by A61, AMI_1:111 ;

A63: now

let d be FinSeq-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 A58, SCMFSA_2:96
.= s . d by SCMFSA_3:12
.= (Exec (CurInstr s),s) . d by A57, SCMFSA_2:96
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by SCMFSA_3:12 ; :: thesis: verum

end;

A64: now

let d be Int-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 A58, SCMFSA_2:96
.= s . d by SCMFSA_3:11
.= (Exec (CurInstr s),s) . d by A57, SCMFSA_2:96
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by SCMFSA_3:11 ; :: thesis: verum

end;

now

let d be Instruction-Location of SCM+FSA ; :: thesis: (Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k)))) . d = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d
thus (Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k)))) . d = (s +* (Start-At ((IC s) + k))) . d by AMI_1:def 13
.= s . d by AMI_1:112
.= (Exec (CurInstr s),s) . d by AMI_1:def 13
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by AMI_1:112 ; :: thesis: verum

end;

hence Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k)) by A62, A63, A64, SCMFSA_2:86; :: thesis: verum

end;

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

then A66: (s +* (Start-At ((IC s) + k))) . da <> 0 by SCMFSA_3:11;
IC (Exec (CurInstr s),s) = Next (IC s) by A57, A65, SCMFSA_2:96;
then A67: IC (Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) by A3, A58, A66, SCMFSA_2:96;

A68: now

let d be FinSeq-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 A58, SCMFSA_2:96
.= s . d by SCMFSA_3:12
.= (Exec (CurInstr s),s) . d by A57, SCMFSA_2:96
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by SCMFSA_3:12 ; :: thesis: verum

end;

A69: now

let d be Int-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 A58, SCMFSA_2:96
.= s . d by SCMFSA_3:11
.= (Exec (CurInstr s),s) . d by A57, SCMFSA_2:96
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by SCMFSA_3:11 ; :: thesis: verum

end;

now

let d be Instruction-Location of SCM+FSA ; :: thesis: (Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k)))) . d = ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d
thus (Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k)))) . d = (s +* (Start-At ((IC s) + k))) . d by AMI_1:def 13
.= s . d by AMI_1:112
.= (Exec (CurInstr s),s) . d by AMI_1:def 13
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by AMI_1:112 ; :: thesis: verum

end;

hence Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k)) by A67, A68, A69, SCMFSA_2:86; :: 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+FSA , da being Int-Location such that
A70: CurInstr s = da >0_goto loc by SCMFSA_2:61;

now

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

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

then A72: (s +* (Start-At ((IC s) + k))) . da > 0 by SCMFSA_3:11;
A73: IC (Exec (CurInstr s),s) = loc by A70, A71, SCMFSA_2:97;
A74: IC (Exec (da >0_goto (loc + k)),(s +* (Start-At ((IC s) + k)))) = loc + k by A72, SCMFSA_2:97
.= IC ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) by A73, AMI_1:111 ;

A75: now

let d be FinSeq-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 SCMFSA_2:97
.= s . d by SCMFSA_3:12
.= (Exec (CurInstr s),s) . d by A70, SCMFSA_2:97
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by SCMFSA_3:12 ; :: thesis: verum

end;

A76: now

let d be Int-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 SCMFSA_2:97
.= s . d by SCMFSA_3:11
.= (Exec (CurInstr s),s) . d by A70, SCMFSA_2:97
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by SCMFSA_3:11 ; :: thesis: verum

end;

now

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

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 A74, A75, A76, SCMFSA_2:86; :: thesis: verum

end;

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

then A78: (s +* (Start-At ((IC s) + k))) . da <= 0 by SCMFSA_3:11;
IC (Exec (CurInstr s),s) = Next (IC s) by A70, A77, SCMFSA_2:97;
then A79: 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 A3, A78, SCMFSA_2:97;

A80: now

let d be FinSeq-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 SCMFSA_2:97
.= s . d by SCMFSA_3:12
.= (Exec (CurInstr s),s) . d by A70, SCMFSA_2:97
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by SCMFSA_3:12 ; :: thesis: verum

end;

A81: now

let d be Int-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 SCMFSA_2:97
.= s . d by SCMFSA_3:11
.= (Exec (CurInstr s),s) . d by A70, SCMFSA_2:97
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by SCMFSA_3:11 ; :: thesis: verum

end;

now

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

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 A79, A80, A81, SCMFSA_2:86; :: 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 A70, Th16; :: thesis: verum

end;

suppose InsCode (CurInstr s) = 9 ; :: thesis: Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k))

then consider db, da being Int-Location , f being FinSeq-Location such that
A82: CurInstr s = da := f,db by SCMFSA_2:62;
A83: IncAddr (CurInstr s),k = CurInstr s by A82, Th17;
A84: IC (Exec (CurInstr s),s) = Next (IC s) by A82, SCMFSA_2:98;
A85: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) by A3, A82, SCMFSA_2:98;

A86: now

let d be FinSeq-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 A82, A83, SCMFSA_2:98
.= s . d by SCMFSA_3:12
.= (Exec (CurInstr s),s) . d by A82, SCMFSA_2:98
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by SCMFSA_3:12 ; :: thesis: verum

end;

now

let d be Int-Location ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . b₁
consider m being Element of NAT such that
A87: m = abs (s . db) and
A88: (Exec (CurInstr s),s) . da = (s . f) /. m by A82, SCMFSA_2:98;
consider m' being Element of NAT such that
A89: m' = abs ((s +* (Start-At ((IC s) + k))) . db) and
A90: (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . da = ((s +* (Start-At ((IC s) + k))) . f) /. m' by A82, SCMFSA_2:98;

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

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

(s +* (Start-At ((IC s) + k))) . db = s . db by SCMFSA_3:11;
hence (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . d = (s . f) /. m by A87, A89, A90, A91, SCMFSA_3:12
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by A88, A91, SCMFSA_3:11 ;
:: thesis: verum

end;

suppose A92: 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 A82, SCMFSA_2:98
.= s . d by SCMFSA_3:11
.= (Exec (CurInstr s),s) . d by A82, A92, SCMFSA_2:98
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

end;

end;

hence Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k)) by A4, A83, A84, A85, A86, SCMFSA_2:86; :: thesis: verum

end;

suppose InsCode (CurInstr s) = 10 ; :: thesis: Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k))

then consider db, da being Int-Location , f being FinSeq-Location such that
A93: CurInstr s = f,db := da by SCMFSA_2:63;
A94: IncAddr (CurInstr s),k = CurInstr s by A93, Th18;
A95: IC (Exec (CurInstr s),s) = Next (IC s) by A93, SCMFSA_2:99;
A96: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) by A3, A93, SCMFSA_2:99;

A97: now

let d be Int-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 A93, A94, SCMFSA_2:99
.= s . d by SCMFSA_3:11
.= (Exec (CurInstr s),s) . d by A93, SCMFSA_2:99
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by SCMFSA_3:11 ; :: thesis: verum

end;

now

let g be FinSeq-Location ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . b₁
consider m being Element of NAT such that
A98: m = abs (s . db) and
A99: (Exec (CurInstr s),s) . f = (s . f) +* m,(s . da) by A93, SCMFSA_2:99;
consider m' being Element of NAT such that
A100: m' = abs ((s +* (Start-At ((IC s) + k))) . db) and
A101: (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . f = ((s +* (Start-At ((IC s) + k))) . f) +* m',((s +* (Start-At ((IC s) + k))) . da) by A93, SCMFSA_2:99;

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

suppose A102: f = g ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . b₁

A103: (s +* (Start-At ((IC s) + k))) . f = s . f by SCMFSA_3:12;
(s +* (Start-At ((IC s) + k))) . db = s . db by SCMFSA_3:11;
hence (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . g = (s . f) +* m,(s . da) by A98, A100, A101, A102, A103, SCMFSA_3:11
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . g by A99, A102, SCMFSA_3:12 ;
:: thesis: verum

end;

suppose A104: f <> g ; :: 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)))) . g = (s +* (Start-At ((IC s) + k))) . g by A93, SCMFSA_2:99
.= s . g by SCMFSA_3:12
.= (Exec (CurInstr s),s) . g by A93, A104, SCMFSA_2:99
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . g by SCMFSA_3:12 ;
:: thesis: verum

end;

end;

end;

hence Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k)) by A4, A94, A95, A96, A97, SCMFSA_2:86; :: thesis: verum

end;

suppose InsCode (CurInstr s) = 11 ; :: thesis: Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k))

then consider da being Int-Location , f being FinSeq-Location such that
A105: CurInstr s = da :=len f by SCMFSA_2:64;
A106: IncAddr (CurInstr s),k = CurInstr s by A105, Th19;
A107: IC (Exec (CurInstr s),s) = Next (IC s) by A105, SCMFSA_2:100;
A108: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) by A3, A105, SCMFSA_2:100;

A109: now

let d be FinSeq-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 A105, A106, SCMFSA_2:100
.= s . d by SCMFSA_3:12
.= (Exec (CurInstr s),s) . d by A105, SCMFSA_2:100
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by SCMFSA_3:12 ; :: thesis: verum

end;

now

let d be Int-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 A110: 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 = len ((s +* (Start-At ((IC s) + k))) . f) by A105, SCMFSA_2:100
.= len (s . f) by SCMFSA_3:12
.= (Exec (CurInstr s),s) . d by A105, A110, SCMFSA_2:100
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

suppose A111: 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 A105, SCMFSA_2:100
.= s . d by SCMFSA_3:11
.= (Exec (CurInstr s),s) . d by A105, A111, SCMFSA_2:100
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

end;

end;

hence Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k)) by A4, A106, A107, A108, A109, SCMFSA_2:86; :: thesis: verum

end;

suppose InsCode (CurInstr s) = 12 ; :: thesis: Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k))

then consider da being Int-Location , f being FinSeq-Location such that
A112: CurInstr s = f :=<0,...,0> da by SCMFSA_2:65;
A113: IncAddr (CurInstr s),k = CurInstr s by A112, Th20;
A114: IC (Exec (CurInstr s),s) = Next (IC s) by A112, SCMFSA_2:101;
A115: IC (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) = IC ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) by A3, A112, SCMFSA_2:101;

A116: now

let d be Int-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 A112, A113, SCMFSA_2:101
.= s . d by SCMFSA_3:11
.= (Exec (CurInstr s),s) . d by A112, SCMFSA_2:101
.= ((Exec (CurInstr s),s) +* (Start-At ((IC (Exec (CurInstr s),s)) + k))) . d by SCMFSA_3:11 ; :: thesis: verum

end;

now

let g be FinSeq-Location ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . b₁
consider m being Element of NAT such that
A117: m = abs (s . da) and
A118: (Exec (CurInstr s),s) . f = m |-> 0 by A112, SCMFSA_2:101;
consider m' being Element of NAT such that
A119: m' = abs ((s +* (Start-At ((IC s) + k))) . da) and
A120: (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . f = m' |-> 0 by A112, SCMFSA_2:101;

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

suppose A121: f = g ; :: thesis: (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . b₁ = ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . b₁

(s +* (Start-At ((IC s) + k))) . da = s . da by SCMFSA_3:11;
hence (Exec (CurInstr s),(s +* (Start-At ((IC s) + k)))) . g = ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . g by A117, A118, A119, A120, A121, SCMFSA_3:12; :: thesis: verum

end;

suppose A122: f <> g ; :: 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)))) . g = (s +* (Start-At ((IC s) + k))) . g by A112, SCMFSA_2:101
.= s . g by SCMFSA_3:12
.= (Exec (CurInstr s),s) . g by A112, A122, SCMFSA_2:101
.= ((Exec (CurInstr s),s) +* (Start-At ((Next (IC s)) + k))) . g by SCMFSA_3:12 ;
:: thesis: verum

end;

end;

end;

hence Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k)) by A4, A113, A114, A115, A116, SCMFSA_2:86; :: thesis: verum

end;

end;