The Coq mailing list

["Woon Ming" <woon_ming AT comp.nus.edu.sg>]

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