Hi,guys
I am working with HOL4.
I am going to prove
g`!p q n l. ( (LENGTH p = LENGTH q) /\ (LENGTH p <= n)) ==> (LENGTH (cx l
p q) <=n ) `;
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"
so I used,
e (RW_TAC list_ss [cx_length]);
But it can't work, does anyone know the reason?
Thanks!------------------------------------------------------------------------------
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
