coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Woon Ming" <woon_ming AT comp.nus.edu.sg>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] (no subject)
- Date: Tue, 17 Feb 2009 02:06:30 +0800 (SGT)
- Importance: Normal
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi all,
I was working with a toy program (attached FindMax.java) and was trying to
find a way to solve memory structure modeled by Coq (using 'shift',
'select' and 'store'). However, I am stuck at a particular one which has
the subgoal as follows:
select intM_intP (shift t j) <= select intM_intP (shift t 0)
I am unable to find this lemma in both my FindMax.v file nor in the
library at the Coq website. Can anyone help me with this and enlighten me
on how to solve this kind of problem?
Best Regards,
Woon Ming
- [Coq-Club] (no subject), Woon Ming
Archive powered by MhonArc 2.6.16.