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
------------------------------------
0. p IN d
1. q IN d
2. LENGTH p = LENGTH q
3. LENGTH (CX l p q) = LENGTH p
4. LENGTH (CX l q p) = LENGTH q
5. LENGTH (CX l p q) = LENGTH (CX l q p)
6. n <= LENGTH p
7. n = LENGTH (TAKE n (CX l p q))
8. n = LENGTH (TAKE n (CX l q p))
: proof
- 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
------------------------------------
0. p IN d
1. q IN d
2. LENGTH p = LENGTH q
3. LENGTH (CX l p q) = LENGTH p
4. LENGTH (CX l q p) = LENGTH q
5. LENGTH (CX l p q) = LENGTH (CX l q p)
6. n <= LENGTH p
7. n = LENGTH (TAKE n (CX l p q))
8. n = LENGTH (TAKE n (CX l q p))
: 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?
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
