> On 21 Mar 2016, at 01:18, Ada <ada.k...@qq.com> wrote: > > Hi,guys > I am working with HOL4. > > val it = > TAKE n (TAKE n (CX l p q) ++ DROP n (CX l q p)) ++ > DROP n (TAKE n (CX l q p) ++ DROP n (CX l p q)) = > CX l p q > ------------------------------------ > ...
> - e (SRW_TAC [numSimps.ARITH_ss][TAKE_APPEND1,DROP_APPEND1]); > OK.. > 1 subgoal: > > val it = > TAKE n (TAKE n (CX l p q)) ++ > DROP n (TAKE n (CX l q p)) ++ DROP n (CX l p q) = > CX l p q > ------------------------------------ > ... : proof > > In this proof, the rewrite of TAKE_APPEND1 has worked, but the rewrite of > DROP_APPEND1 doesn't. > Does anyone know the reason? Or, Who has good advice? Both rewrites have worked. Look at the way the parentheses have moved. Michael ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ------------------------------------------------------------------------------ Transform Data into Opportunity. Accelerate data analysis in your applications with Intel Data Analytics Acceleration Library. Click to learn more. http://pubads.g.doubleclick.net/gampad/clk?id=278785351&iu=/4140 _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
