let a, b be Int-Location; :: thesis: for s being State of SCM+FSA holds
( (Exec ((Divide (a,b)),s)) . (IC ) = (IC s) + 1 & ( 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 ) = (IC s) + 1 & ( 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 Def10;
reconsider S = s | SCM-Memory as State of SCM by Th42;
A4: Exec ((Divide (a,b)),s) = s +* (Exec ((Divide (A,B)),S)) by A3, Th44;
hence (Exec ((Divide (a,b)),s)) . (IC ) = (Exec ((Divide (A,B)),S)) . (IC ) by Th46
.= (IC S) + 1 by AMI_3:6
.= (IC s) + 1 by Th55 ;
:: 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, Th47
.= (S . A) div (S . B) by A1, A2, A5, AMI_3:6
.= (S . A) div (s . b) by A2, Th48
.= (s . a) div (s . b) by A1, Th48 ; :: thesis: verum

end;

thus (Exec ((Divide (a,b)),s)) . b = (Exec ((Divide (A,B)),S)) . B by A2, A4, Th47
.= (S . A) mod (S . B) by AMI_3:6
.= (S . A) mod (s . b) by A2, Th48
.= (s . a) mod (s . b) by A1, Th48 ; :: 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 Th5;
thus (Exec ((Divide (a,b)),s)) . c = (Exec ((Divide (A,B)),S)) . C by A4, Th47
.= S . C by A1, A2, A6, AMI_3:6
.= s . c by Th48 ; :: thesis: verum

end;

let f be FinSeq-Location ; :: thesis: (Exec ((Divide (a,b)),s)) . f = s . f
A7: not f in dom (Exec ((Divide (A,B)),S)) by Th37;
thus (Exec ((Divide (a,b)),s)) . f = s . f by A4, A7, FUNCT_4:11; :: thesis: verum