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

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

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

end;

let f be FinSeq-Location ; :: thesis: (Exec ((Divide (a,a)),s)) . f = s . f
A7: not f in dom (Exec ((Divide (A,A)),S)) by Th68;
thus (Exec ((Divide (a,a)),s)) . f = (s +* (Exec ((Divide (A,A)),S))) . f by A3
.= s . f by A7, FUNCT_4:11 ; :: thesis: verum