let a, b be Int-Location ; :: thesis: for s being State of SCM+FSA holds
( (Exec (Divide a,b),s) . (IC SCM+FSA ) = succ (IC s) & ( a <> b implies (Exec (Divide a,b),s) . a = (s . a) div (s . b) ) & (Exec (Divide a,b),s) . b = (s . a) mod (s . b) & ( for c being Int-Location st c <> a & c <> b holds
(Exec (Divide a,b),s) . c = s . c ) & ( for f being FinSeq-Location holds (Exec (Divide a,b),s) . f = s . f ) )
let s be State of SCM+FSA ; :: thesis: ( (Exec (Divide a,b),s) . (IC SCM+FSA ) = succ (IC s) & ( a <> b implies (Exec (Divide a,b),s) . a = (s . a) div (s . b) ) & (Exec (Divide a,b),s) . b = (s . a) mod (s . b) & ( for c being Int-Location st c <> a & c <> b holds
(Exec (Divide a,b),s) . c = s . c ) & ( for f being FinSeq-Location holds (Exec (Divide a,b),s) . f = s . f ) )
consider A, B being Data-Location such that
A1: a = A and
A2: b = B and
A3: Divide a,b = Divide A,B by Def15;
reconsider S = (s | SCM-Memory ) +* (NAT --> (Divide A,B)) as State of SCM by Th73;
A4: Exec (Divide a,b),s = (s +* (Exec (Divide A,B),S)) +* (s | NAT ) by A3, Th75;
hence (Exec (Divide a,b),s) . (IC SCM+FSA ) = (Exec (Divide A,B),S) . (IC SCM ) by Th78
.= succ (IC S) by AMI_3:12
.= succ (IC s) by Th88 ;
:: thesis: ( ( a <> b implies (Exec (Divide a,b),s) . a = (s . a) div (s . b) ) & (Exec (Divide a,b),s) . b = (s . a) mod (s . b) & ( for c being Int-Location st c <> a & c <> b holds
(Exec (Divide a,b),s) . c = s . c ) & ( for f being FinSeq-Location holds (Exec (Divide a,b),s) . f = s . f ) )

hereby :: thesis: ( (Exec (Divide a,b),s) . b = (s . a) mod (s . b) & ( for c being Int-Location st c <> a & c <> b holds
(Exec (Divide a,b),s) . c = s . c ) & ( for f being FinSeq-Location holds (Exec (Divide a,b),s) . f = s . f ) )

assume A5: a <> b ; :: thesis: (Exec (Divide a,b),s) . a = (s . a) div (s . b)
thus (Exec (Divide a,b),s) . a = (Exec (Divide A,B),S) . A by A1, A4, Th79
.= (S . A) div (S . B) by A1, A2, A5, AMI_3:12
.= (S . A) div (s . b) by A2, Th80
.= (s . a) div (s . b) by A1, Th80 ; :: thesis: verum

end;

thus (Exec (Divide a,b),s) . b = (Exec (Divide A,B),S) . B by A2, A4, Th79
.= (S . A) mod (S . B) by AMI_3:12
.= (S . A) mod (s . b) by A2, Th80
.= (s . a) mod (s . b) by A1, Th80 ; :: thesis: ( ( for c being Int-Location st c <> a & c <> b holds
(Exec (Divide a,b),s) . c = s . c ) & ( for f being FinSeq-Location holds (Exec (Divide a,b),s) . f = s . f ) )

hereby :: thesis: for f being FinSeq-Location holds (Exec (Divide a,b),s) . f = s . f

let c be Int-Location ; :: thesis: ( c <> a & c <> b implies (Exec (Divide a,b),s) . c = s . c )
assume A6: ( c <> a & c <> b ) ; :: thesis: (Exec (Divide a,b),s) . c = s . c
reconsider C = c as Data-Location by Th25;
thus (Exec (Divide a,b),s) . c = (Exec (Divide A,B),S) . C by A4, Th79
.= S . C by A1, A2, A6, AMI_3:12
.= s . c by Th80 ; :: thesis: verum

end;

let f be FinSeq-Location ; :: thesis: (Exec (Divide a,b),s) . f = s . f

A7: now

assume f in NAT ; :: thesis: contradiction
then A8: SCM+FSA-OK . f = SCM+FSA-Instr by SCMFSA_1:11;
f in SCM+FSA-Data*-Loc by Def5;
hence contradiction by A8, SCMFSA_1:12, SCMFSA_1:13; :: thesis: verum

end;

A9: not f in dom (Exec (Divide A,B),S) by Th68;
dom (s | NAT ) = (dom s) /\ NAT by RELAT_1:90;
then not f in dom (s | NAT ) by A7, XBOOLE_0:def 4;
hence (Exec (Divide a,b),s) . f = (s +* (Exec (Divide A,B),S)) . f by A4, FUNCT_4:12
.= s . f by A9, FUNCT_4:12 ;
:: thesis: verum