Re: [isabelle] How does one reason about the subset of a list?



Thanks a whole lot for the replies!

>Firstly, the "\<forall>i < j. xs!j < xs!i" doesn't seem to correspond
with anything in your English description.

I definetly did make a mistake in the english formulation of the
problem.

I am studying your approach now and I believe I can start something
(actually a whole lot) with this. 
I am now beginning to think my problem is that I am not used to this
verification snowballing effect where verifying one thing leads to
describing or verifying something smaller or more general.

I will get back once I have been able to do something (or when I am
stuck again :))

Thanks once more.
Primrose





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.