let k be Element of NAT ; :: thesis: for p being the Instructions of SCM+FSA -valued Function
for s being State of SCM+FSA holds Exec (IncAddr (CurInstr p,s),k),(s +* (Start-At ((IC s) + k),SCM+FSA )) = (Following p,s) +* (Start-At ((IC (Following p,s)) + k),SCM+FSA )
let p be the Instructions of SCM+FSA -valued Function; :: thesis: for s being State of SCM+FSA holds Exec (IncAddr (CurInstr p,s),k),(s +* (Start-At ((IC s) + k),SCM+FSA )) = (Following p,s) +* (Start-At ((IC (Following p,s)) + k),SCM+FSA )
let s be State of SCM+FSA ; :: thesis: Exec (IncAddr (CurInstr p,s),k),(s +* (Start-At ((IC s) + k),SCM+FSA )) = (Following p,s) +* (Start-At ((IC (Following p,s)) + k),SCM+FSA )
set INS = CurInstr p,s;
reconsider m = IC s as Element of NAT ;
A1: succ (IC (s +* (Start-At ((IC s) + k),SCM+FSA ))) = succ (m + k) by FUNCT_4:121
.= (m + k) + 1 by NAT_1:39
.= (m + 1) + k
.= (succ (IC s)) + k by NAT_1:39
.= IC ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) by FUNCT_4:121 ;
A2: ( not InsCode (CurInstr p,s) <= 9 + 1 or InsCode (CurInstr p,s) <= 8 + 1 or InsCode (CurInstr p,s) = 10 ) by NAT_1:8;
A3: ( not InsCode (CurInstr p,s) <= 10 + 1 or InsCode (CurInstr p,s) <= 10 or InsCode (CurInstr p,s) = 11 ) by NAT_1:8;
A4: InsCode (CurInstr p,s) <= 11 + 1 by SCMFSA_2:35;

A5: now

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

end;

per cases ( InsCode (CurInstr p,s) = 0 or InsCode (CurInstr p,s) = 1 or InsCode (CurInstr p,s) = 2 or InsCode (CurInstr p,s) = 3 or InsCode (CurInstr p,s) = 4 or InsCode (CurInstr p,s) = 5 or InsCode (CurInstr p,s) = 6 or InsCode (CurInstr p,s) = 7 or InsCode (CurInstr p,s) = 8 or InsCode (CurInstr p,s) = 9 or InsCode (CurInstr p,s) = 10 or InsCode (CurInstr p,s) = 11 or InsCode (CurInstr p,s) = 12 ) by A4, A3, A2, NAT_1:8, NAT_1:33;

suppose A6: InsCode (CurInstr p,s) = 0 ; :: thesis: Exec (IncAddr (CurInstr p,s),k),(s +* (Start-At ((IC s) + k),SCM+FSA )) = (Following p,s) +* (Start-At ((IC (Following p,s)) + k),SCM+FSA )

then A7: Following p,s = Exec (halt SCM+FSA ),s by SCMFSA_2:122
.= s by AMI_1:def 8 ;
CurInstr p,s = halt SCM+FSA by A6, SCMFSA_2:122;
hence Exec (IncAddr (CurInstr p,s),k),(s +* (Start-At ((IC s) + k),SCM+FSA )) = Exec (halt SCM+FSA ),(s +* (Start-At ((IC s) + k),SCM+FSA )) by Th8
.= (Following p,s) +* (Start-At ((IC (Following p,s)) + k),SCM+FSA ) by A7, AMI_1:def 8 ;
:: thesis: verum

end;

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

then consider da, db being Int-Location such that
A8: CurInstr p,s = da := db by SCMFSA_2:54;
A9: IncAddr (CurInstr p,s),k = CurInstr p,s by A8, Th9;

A10: now

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

end;

A11: now

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

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

suppose A12: da = d ; :: thesis: (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . b₁ = ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . b₁

hence (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) + k),SCM+FSA )) . db by A8, SCMFSA_2:89
.= s . db by SCMFSA_3:11
.= (Exec (CurInstr p,s),s) . d by A8, A12, SCMFSA_2:89
.= ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

suppose A13: da <> d ; :: thesis: (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . b₁ = ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . b₁

hence (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) + k),SCM+FSA )) . d by A8, SCMFSA_2:89
.= s . d by SCMFSA_3:11
.= (Exec (CurInstr p,s),s) . d by A8, A13, SCMFSA_2:89
.= ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

end;

end;

( IC (Exec (CurInstr p,s),s) = succ (IC s) & IC (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) = IC ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) ) by A1, A8, SCMFSA_2:89;
hence Exec (IncAddr (CurInstr p,s),k),(s +* (Start-At ((IC s) + k),SCM+FSA )) = (Following p,s) +* (Start-At ((IC (Following p,s)) + k),SCM+FSA ) by A5, A9, A10, A11, SCMFSA_2:86; :: thesis: verum

end;

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

then consider da, db being Int-Location such that
A14: CurInstr p,s = AddTo da,db by SCMFSA_2:55;
A15: IncAddr (CurInstr p,s),k = CurInstr p,s by A14, Th10;

A16: now

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

end;

A17: now

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

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

suppose A18: da = d ; :: thesis: (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . b₁ = ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . b₁

hence (Exec (CurInstr p,s),(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 A14, 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 (CurInstr p,s),s) . d by A14, A18, SCMFSA_2:90
.= ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

suppose A19: da <> d ; :: thesis: (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . b₁ = ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . b₁

hence (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) + k),SCM+FSA )) . d by A14, SCMFSA_2:90
.= s . d by SCMFSA_3:11
.= (Exec (CurInstr p,s),s) . d by A14, A19, SCMFSA_2:90
.= ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

end;

end;

( IC (Exec (CurInstr p,s),s) = succ (IC s) & IC (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) = IC ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) ) by A1, A14, SCMFSA_2:90;
hence Exec (IncAddr (CurInstr p,s),k),(s +* (Start-At ((IC s) + k),SCM+FSA )) = (Following p,s) +* (Start-At ((IC (Following p,s)) + k),SCM+FSA ) by A5, A15, A16, A17, SCMFSA_2:86; :: thesis: verum

end;

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

then consider da, db being Int-Location such that
A20: CurInstr p,s = SubFrom da,db by SCMFSA_2:56;
A21: IncAddr (CurInstr p,s),k = CurInstr p,s by A20, Th11;

A22: now

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

end;

A23: now

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

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

suppose A24: da = d ; :: thesis: (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . b₁ = ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . b₁

hence (Exec (CurInstr p,s),(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 A20, 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 (CurInstr p,s),s) . d by A20, A24, SCMFSA_2:91
.= ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

suppose A25: da <> d ; :: thesis: (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . b₁ = ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . b₁

hence (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) + k),SCM+FSA )) . d by A20, SCMFSA_2:91
.= s . d by SCMFSA_3:11
.= (Exec (CurInstr p,s),s) . d by A20, A25, SCMFSA_2:91
.= ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

end;

end;

( IC (Exec (CurInstr p,s),s) = succ (IC s) & IC (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) = IC ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) ) by A1, A20, SCMFSA_2:91;
hence Exec (IncAddr (CurInstr p,s),k),(s +* (Start-At ((IC s) + k),SCM+FSA )) = (Following p,s) +* (Start-At ((IC (Following p,s)) + k),SCM+FSA ) by A5, A21, A22, A23, SCMFSA_2:86; :: thesis: verum

end;

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

then consider da, db being Int-Location such that
A26: CurInstr p,s = MultBy da,db by SCMFSA_2:57;
A27: IncAddr (CurInstr p,s),k = CurInstr p,s by A26, Th12;

A28: now

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

end;

A29: now

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

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

suppose A30: da = d ; :: thesis: (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . b₁ = ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . b₁

hence (Exec (CurInstr p,s),(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 A26, 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 (CurInstr p,s),s) . d by A26, A30, SCMFSA_2:92
.= ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

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

hence (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) + k),SCM+FSA )) . d by A26, SCMFSA_2:92
.= s . d by SCMFSA_3:11
.= (Exec (CurInstr p,s),s) . d by A26, A31, SCMFSA_2:92
.= ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

end;

end;

( IC (Exec (CurInstr p,s),s) = succ (IC s) & IC (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) = IC ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) ) by A1, A26, SCMFSA_2:92;
hence Exec (IncAddr (CurInstr p,s),k),(s +* (Start-At ((IC s) + k),SCM+FSA )) = (Following p,s) +* (Start-At ((IC (Following p,s)) + k),SCM+FSA ) by A5, A27, A28, A29, SCMFSA_2:86; :: thesis: verum

end;

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

then consider da, db being Int-Location such that
A32: CurInstr p,s = Divide da,db by SCMFSA_2:58;
A33: IncAddr (CurInstr p,s),k = CurInstr p,s by A32, Th13;

A34: now

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

end;

A35: now

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

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

suppose A36: da <> db ; :: thesis: (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . b₁ = ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . b₁

hereby :: thesis: verum

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

suppose A37: da = d ; :: thesis: (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . d = ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . d

hence (Exec (CurInstr p,s),(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 A32, 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 (CurInstr p,s),s) . d by A32, A36, A37, SCMFSA_2:93
.= ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

suppose A38: db = d ; :: thesis: (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . d = ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . d

hence (Exec (CurInstr p,s),(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 A32, 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 (CurInstr p,s),s) . d by A32, A38, SCMFSA_2:93
.= ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

suppose A39: ( da <> d & db <> d ) ; :: thesis: (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . d = ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . d

hence (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) + k),SCM+FSA )) . d by A32, SCMFSA_2:93
.= s . d by SCMFSA_3:11
.= (Exec (CurInstr p,s),s) . d by A32, A39, SCMFSA_2:93
.= ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

end;

end;

end;

suppose A40: da = db ; :: thesis: (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . b₁ = ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . b₁

hereby :: thesis: verum

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

suppose A41: da = d ; :: thesis: (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . d = ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . d

hence (Exec (CurInstr p,s),(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 )) . da) by A32, A40, SCMFSA_2:94
.= (s . da) mod ((s +* (Start-At ((IC s) + k),SCM+FSA )) . da) by SCMFSA_3:11
.= (s . da) mod (s . da) by SCMFSA_3:11
.= (Exec (CurInstr p,s),s) . d by A32, A40, A41, SCMFSA_2:94
.= ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

suppose A42: da <> d ; :: thesis: (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . d = ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . d

hence (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) + k),SCM+FSA )) . d by A32, A40, SCMFSA_2:94
.= s . d by SCMFSA_3:11
.= (Exec (CurInstr p,s),s) . d by A32, A40, A42, SCMFSA_2:94
.= ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

end;

end;

end;

end;

end;

( IC (Exec (CurInstr p,s),s) = succ (IC s) & IC (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) = IC ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) ) by A1, A32, SCMFSA_2:93;
hence Exec (IncAddr (CurInstr p,s),k),(s +* (Start-At ((IC s) + k),SCM+FSA )) = (Following p,s) +* (Start-At ((IC (Following p,s)) + k),SCM+FSA ) by A5, A33, A34, A35, SCMFSA_2:86; :: thesis: verum

end;

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

then consider loc being Element of NAT such that
A43: CurInstr p,s = goto loc by SCMFSA_2:59;
A44: IncAddr (CurInstr p,s),k = goto (loc + k) by A43, Th14;

A45: now

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

end;

A46: IC (Exec (CurInstr p,s),s) = loc by A43, SCMFSA_2:95;

A47: now

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

end;

A48: now

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

end;

IC (Exec (IncAddr (CurInstr p,s),k),(s +* (Start-At ((IC s) + k),SCM+FSA ))) = loc + k by A44, SCMFSA_2:95
.= IC ((Exec (CurInstr p,s),s) +* (Start-At ((IC (Exec (CurInstr p,s),s)) + k),SCM+FSA )) by A46, FUNCT_4:121 ;
hence Exec (IncAddr (CurInstr p,s),k),(s +* (Start-At ((IC s) + k),SCM+FSA )) = (Following p,s) +* (Start-At ((IC (Following p,s)) + k),SCM+FSA ) by A45, A48, A47, SCMFSA_2:86; :: thesis: verum

end;

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

then consider loc being Element of NAT , da being Int-Location such that
A49: CurInstr p,s = da =0_goto loc by SCMFSA_2:60;
A50: IncAddr (CurInstr p,s),k = da =0_goto (loc + k) by A49, Th15;

now

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

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

A52: now

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

end;

A53: now

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

end;

A54: IC (Exec (CurInstr p,s),s) = loc by A49, A51, SCMFSA_2:96;

A55: now

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

end;

(s +* (Start-At ((IC s) + k),SCM+FSA )) . da = 0 by A51, SCMFSA_3:11;
then IC (Exec (IncAddr (CurInstr p,s),k),(s +* (Start-At ((IC s) + k),SCM+FSA ))) = loc + k by A50, SCMFSA_2:96
.= IC ((Exec (CurInstr p,s),s) +* (Start-At ((IC (Exec (CurInstr p,s),s)) + k),SCM+FSA )) by A54, FUNCT_4:121 ;
hence Exec (IncAddr (CurInstr p,s),k),(s +* (Start-At ((IC s) + k),SCM+FSA )) = (Exec (CurInstr p,s),s) +* (Start-At ((IC (Exec (CurInstr p,s),s)) + k),SCM+FSA ) by A53, A52, A55, SCMFSA_2:86; :: thesis: verum

end;

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

A57: now

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

end;

A58: now

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

end;

A59: now

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

end;

( (s +* (Start-At ((IC s) + k),SCM+FSA )) . da <> 0 & IC (Exec (CurInstr p,s),s) = succ (IC s) ) by A49, A56, SCMFSA_2:96, SCMFSA_3:11;
then IC (Exec (IncAddr (CurInstr p,s),k),(s +* (Start-At ((IC s) + k),SCM+FSA ))) = IC ((Exec (CurInstr p,s),s) +* (Start-At ((IC (Exec (CurInstr p,s),s)) + k),SCM+FSA )) by A1, A50, SCMFSA_2:96;
hence Exec (IncAddr (CurInstr p,s),k),(s +* (Start-At ((IC s) + k),SCM+FSA )) = (Exec (CurInstr p,s),s) +* (Start-At ((IC (Exec (CurInstr p,s),s)) + k),SCM+FSA ) by A59, A58, A57, SCMFSA_2:86; :: thesis: verum

end;

end;

end;

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

end;

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

then consider loc being Element of NAT , da being Int-Location such that
A60: CurInstr p,s = da >0_goto loc by SCMFSA_2:61;

now

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

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

A62: now

let d be Int-Location ; :: thesis: (Exec (da >0_goto (loc + k)),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . d = ((Exec (CurInstr p,s),s) +* (Start-At ((IC (Exec (CurInstr p,s),s)) + k),SCM+FSA )) . d
thus (Exec (da >0_goto (loc + k)),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) + k),SCM+FSA )) . d by SCMFSA_2:97
.= s . d by SCMFSA_3:11
.= (Exec (CurInstr p,s),s) . d by A60, SCMFSA_2:97
.= ((Exec (CurInstr p,s),s) +* (Start-At ((IC (Exec (CurInstr p,s),s)) + k),SCM+FSA )) . d by SCMFSA_3:11 ; :: thesis: verum

end;

A63: now

let d be FinSeq-Location ; :: thesis: (Exec (da >0_goto (loc + k)),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . d = ((Exec (CurInstr p,s),s) +* (Start-At ((IC (Exec (CurInstr p,s),s)) + k),SCM+FSA )) . d
thus (Exec (da >0_goto (loc + k)),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) + k),SCM+FSA )) . d by SCMFSA_2:97
.= s . d by SCMFSA_3:12
.= (Exec (CurInstr p,s),s) . d by A60, SCMFSA_2:97
.= ((Exec (CurInstr p,s),s) +* (Start-At ((IC (Exec (CurInstr p,s),s)) + k),SCM+FSA )) . d by SCMFSA_3:12 ; :: thesis: verum

end;

A64: IC (Exec (CurInstr p,s),s) = loc by A60, A61, SCMFSA_2:97;

A65: now

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

end;

(s +* (Start-At ((IC s) + k),SCM+FSA )) . da > 0 by A61, SCMFSA_3:11;
then IC (Exec (da >0_goto (loc + k)),(s +* (Start-At ((IC s) + k),SCM+FSA ))) = loc + k by SCMFSA_2:97
.= IC ((Exec (CurInstr p,s),s) +* (Start-At ((IC (Exec (CurInstr p,s),s)) + k),SCM+FSA )) by A64, FUNCT_4:121 ;
hence Exec (da >0_goto (loc + k)),(s +* (Start-At ((IC s) + k),SCM+FSA )) = (Exec (CurInstr p,s),s) +* (Start-At ((IC (Exec (CurInstr p,s),s)) + k),SCM+FSA ) by A63, A62, A65, SCMFSA_2:86; :: thesis: verum

end;

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

A67: now

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

end;

A68: now

let d be Int-Location ; :: thesis: (Exec (da >0_goto (loc + k)),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . d = ((Exec (CurInstr p,s),s) +* (Start-At ((IC (Exec (CurInstr p,s),s)) + k),SCM+FSA )) . d
thus (Exec (da >0_goto (loc + k)),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) + k),SCM+FSA )) . d by SCMFSA_2:97
.= s . d by SCMFSA_3:11
.= (Exec (CurInstr p,s),s) . d by A60, SCMFSA_2:97
.= ((Exec (CurInstr p,s),s) +* (Start-At ((IC (Exec (CurInstr p,s),s)) + k),SCM+FSA )) . d by SCMFSA_3:11 ; :: thesis: verum

end;

A69: now

let d be FinSeq-Location ; :: thesis: (Exec (da >0_goto (loc + k)),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . d = ((Exec (CurInstr p,s),s) +* (Start-At ((IC (Exec (CurInstr p,s),s)) + k),SCM+FSA )) . d
thus (Exec (da >0_goto (loc + k)),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) + k),SCM+FSA )) . d by SCMFSA_2:97
.= s . d by SCMFSA_3:12
.= (Exec (CurInstr p,s),s) . d by A60, SCMFSA_2:97
.= ((Exec (CurInstr p,s),s) +* (Start-At ((IC (Exec (CurInstr p,s),s)) + k),SCM+FSA )) . d by SCMFSA_3:12 ; :: thesis: verum

end;

( (s +* (Start-At ((IC s) + k),SCM+FSA )) . da <= 0 & IC (Exec (CurInstr p,s),s) = succ (IC s) ) by A60, A66, SCMFSA_2:97, SCMFSA_3:11;
then IC (Exec (da >0_goto (loc + k)),(s +* (Start-At ((IC s) + k),SCM+FSA ))) = IC ((Exec (CurInstr p,s),s) +* (Start-At ((IC (Exec (CurInstr p,s),s)) + k),SCM+FSA )) by A1, SCMFSA_2:97;
hence Exec (da >0_goto (loc + k)),(s +* (Start-At ((IC s) + k),SCM+FSA )) = (Exec (CurInstr p,s),s) +* (Start-At ((IC (Exec (CurInstr p,s),s)) + k),SCM+FSA ) by A69, A68, A67, SCMFSA_2:86; :: thesis: verum

end;

end;

end;

hence Exec (IncAddr (CurInstr p,s),k),(s +* (Start-At ((IC s) + k),SCM+FSA )) = (Following p,s) +* (Start-At ((IC (Following p,s)) + k),SCM+FSA ) by A60, Th16; :: thesis: verum

end;

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

then consider db, da being Int-Location , f being FinSeq-Location such that
A70: CurInstr p,s = da := f,db by SCMFSA_2:62;
A71: IncAddr (CurInstr p,s),k = CurInstr p,s by A70, Th17;

A72: now

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

end;

A73: now

let d be Int-Location ; :: thesis: (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . b₁ = ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . b₁
consider m being Element of NAT such that
A74: m = abs (s . db) and
A75: (Exec (CurInstr p,s),s) . da = (s . f) /. m by A70, SCMFSA_2:98;
A76: ex m9 being Element of NAT st
( m9 = abs ((s +* (Start-At ((IC s) + k),SCM+FSA )) . db) & (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . da = ((s +* (Start-At ((IC s) + k),SCM+FSA )) . f) /. m9 ) by A70, SCMFSA_2:98;

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

suppose A77: da = d ; :: thesis: (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . b₁ = ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . b₁

(s +* (Start-At ((IC s) + k),SCM+FSA )) . db = s . db by SCMFSA_3:11;
hence (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . d = (s . f) /. m by A74, A76, A77, SCMFSA_3:12
.= ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . d by A75, A77, SCMFSA_3:11 ;
:: thesis: verum

end;

suppose A78: da <> d ; :: thesis: (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . b₁ = ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . b₁

hence (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) + k),SCM+FSA )) . d by A70, SCMFSA_2:98
.= s . d by SCMFSA_3:11
.= (Exec (CurInstr p,s),s) . d by A70, A78, SCMFSA_2:98
.= ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

end;

end;

( IC (Exec (CurInstr p,s),s) = succ (IC s) & IC (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) = IC ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) ) by A1, A70, SCMFSA_2:98;
hence Exec (IncAddr (CurInstr p,s),k),(s +* (Start-At ((IC s) + k),SCM+FSA )) = (Following p,s) +* (Start-At ((IC (Following p,s)) + k),SCM+FSA ) by A5, A71, A72, A73, SCMFSA_2:86; :: thesis: verum

end;

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

then consider db, da being Int-Location , f being FinSeq-Location such that
A79: CurInstr p,s = f,db := da by SCMFSA_2:63;
A80: IncAddr (CurInstr p,s),k = CurInstr p,s by A79, Th18;

A81: now

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

end;

A82: now

let g be FinSeq-Location ; :: thesis: (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . b₁ = ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . b₁
consider m being Element of NAT such that
A83: m = abs (s . db) and
A84: (Exec (CurInstr p,s),s) . f = (s . f) +* m,(s . da) by A79, SCMFSA_2:99;
A85: ex m9 being Element of NAT st
( m9 = abs ((s +* (Start-At ((IC s) + k),SCM+FSA )) . db) & (Exec (CurInstr p,s),(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) ) by A79, SCMFSA_2:99;

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

suppose A86: f = g ; :: thesis: (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . b₁ = ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . b₁

( (s +* (Start-At ((IC s) + k),SCM+FSA )) . f = s . f & (s +* (Start-At ((IC s) + k),SCM+FSA )) . db = s . db ) by SCMFSA_3:11, SCMFSA_3:12;
hence (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . g = (s . f) +* m,(s . da) by A83, A85, A86, SCMFSA_3:11
.= ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . g by A84, A86, SCMFSA_3:12 ;
:: thesis: verum

end;

suppose A87: f <> g ; :: thesis: (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . b₁ = ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . b₁

hence (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . g = (s +* (Start-At ((IC s) + k),SCM+FSA )) . g by A79, SCMFSA_2:99
.= s . g by SCMFSA_3:12
.= (Exec (CurInstr p,s),s) . g by A79, A87, SCMFSA_2:99
.= ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . g by SCMFSA_3:12 ;
:: thesis: verum

end;

end;

end;

( IC (Exec (CurInstr p,s),s) = succ (IC s) & IC (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) = IC ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) ) by A1, A79, SCMFSA_2:99;
hence Exec (IncAddr (CurInstr p,s),k),(s +* (Start-At ((IC s) + k),SCM+FSA )) = (Following p,s) +* (Start-At ((IC (Following p,s)) + k),SCM+FSA ) by A5, A80, A81, A82, SCMFSA_2:86; :: thesis: verum

end;

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

then consider da being Int-Location , f being FinSeq-Location such that
A88: CurInstr p,s = da :=len f by SCMFSA_2:64;
A89: IncAddr (CurInstr p,s),k = CurInstr p,s by A88, Th19;

A90: now

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

end;

A91: now

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

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

suppose A92: da = d ; :: thesis: (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . b₁ = ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . b₁

hence (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . d = len ((s +* (Start-At ((IC s) + k),SCM+FSA )) . f) by A88, SCMFSA_2:100
.= len (s . f) by SCMFSA_3:12
.= (Exec (CurInstr p,s),s) . d by A88, A92, SCMFSA_2:100
.= ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

suppose A93: da <> d ; :: thesis: (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . b₁ = ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . b₁

hence (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . d = (s +* (Start-At ((IC s) + k),SCM+FSA )) . d by A88, SCMFSA_2:100
.= s . d by SCMFSA_3:11
.= (Exec (CurInstr p,s),s) . d by A88, A93, SCMFSA_2:100
.= ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . d by SCMFSA_3:11 ;
:: thesis: verum

end;

end;

end;

( IC (Exec (CurInstr p,s),s) = succ (IC s) & IC (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) = IC ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) ) by A1, A88, SCMFSA_2:100;
hence Exec (IncAddr (CurInstr p,s),k),(s +* (Start-At ((IC s) + k),SCM+FSA )) = (Following p,s) +* (Start-At ((IC (Following p,s)) + k),SCM+FSA ) by A5, A89, A90, A91, SCMFSA_2:86; :: thesis: verum

end;

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

then consider da being Int-Location , f being FinSeq-Location such that
A94: CurInstr p,s = f :=<0,...,0> da by SCMFSA_2:65;
A95: IncAddr (CurInstr p,s),k = CurInstr p,s by A94, Th20;

A96: now

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

end;

A97: now

let g be FinSeq-Location ; :: thesis: (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . b₁ = ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . b₁
A98: ( ex m being Element of NAT st
( m = abs (s . da) & (Exec (CurInstr p,s),s) . f = m |-> 0 ) & ex m9 being Element of NAT st
( m9 = abs ((s +* (Start-At ((IC s) + k),SCM+FSA )) . da) & (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . f = m9 |-> 0 ) ) by A94, SCMFSA_2:101;

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

suppose A99: f = g ; :: thesis: (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . b₁ = ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . b₁

(s +* (Start-At ((IC s) + k),SCM+FSA )) . da = s . da by SCMFSA_3:11;
hence (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . g = ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . g by A98, A99, SCMFSA_3:12; :: thesis: verum

end;

suppose A100: f <> g ; :: thesis: (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . b₁ = ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . b₁

hence (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) . g = (s +* (Start-At ((IC s) + k),SCM+FSA )) . g by A94, SCMFSA_2:101
.= s . g by SCMFSA_3:12
.= (Exec (CurInstr p,s),s) . g by A94, A100, SCMFSA_2:101
.= ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) . g by SCMFSA_3:12 ;
:: thesis: verum

end;

end;

end;

( IC (Exec (CurInstr p,s),s) = succ (IC s) & IC (Exec (CurInstr p,s),(s +* (Start-At ((IC s) + k),SCM+FSA ))) = IC ((Exec (CurInstr p,s),s) +* (Start-At ((succ (IC s)) + k),SCM+FSA )) ) by A1, A94, SCMFSA_2:101;
hence Exec (IncAddr (CurInstr p,s),k),(s +* (Start-At ((IC s) + k),SCM+FSA )) = (Following p,s) +* (Start-At ((IC (Following p,s)) + k),SCM+FSA ) by A5, A95, A96, A97, SCMFSA_2:86; :: thesis: verum

end;

end;