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 EXTPRO_1:def 3 ;
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, EXTPRO_1:def 3 ;
:: 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;