Hi,guys
I am working with HOL4.
I am going to prove
g`!p q. (LENGTH p = LENGTH q)
==> !l m n .
TAKE n (TAKE m (CX l p q) ++ DROP m (CX l q p)) ++
DROP n (TAKE m (CX l q p) ++ DROP m (CX l p q)) =
TAKE m (TAKE n (CX l p q) ++ DROP n (CX l q p)) ++
DROP m (TAKE n (CX l q p) ++ DROP n (CX l p q)) `;
Where the definition of CX is
val CX_def = Define`
(CX [] p q = p) ??
(CX (x::xs) p q =
TAKE x (CX xs p q) ++
DROP x (CX xs q p))`;
I had proved " !l p q . (LENGTH p = LENGTH q) ==> (LENGTH (CX l p q) =
LENGTH p)", named "CX_length".
I had tried several times. But the proof failed. How to prove it? Does
anyone have any good idea?
Thanks!------------------------------------------------------------------------------
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=278785231&iu=/4140
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
