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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and