I just wrote a fairly manual 48-line proof of the following.
Is there some decision procedure, simpset, or tactic I could use to
automate it that I'm not aware of?
The theorems in srw_ss() seem not to play very well together on this kind
of stuff.
TAKE (LENGTH bvs + 1)
(REVERSE bvs ++
Block 3 [CodePtr a; bve]::
(blvs ++ [benv; CodePtr ret] ++ REVERSE args0 ++ [cl0] ++ st)) ++
DROP (LENGTH args0 + (LENGTH blvs + (LENGTH bvs + 4)))
(REVERSE bvs ++
Block 3 [CodePtr a; bve]::
(blvs ++ [benv; CodePtr ret] ++ REVERSE args0 ++ [cl0] ++ st)) =
TAKE (LENGTH bvs + 1)
(REVERSE bvs ++
Block 3 [CodePtr a; bve]::
(blvs ++ [benv; CodePtr ret] ++ REVERSE args0 ++ [cl0] ++ st)) ++
st
------------------------------------------------------------------------------
Everyone hates slow websites. So do we.
Make your web apps faster with AppDynamics
Download AppDynamics Lite for free today:
http://p.sf.net/sfu/appdyn_d2d_feb
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
