Re: [isabelle] Doing induction on lists "backwards"
> Is there any way to use an inductive method to prove
> laststate_seq_stop despite it being defined going backwards over the
> list, rather than forwards as per the list definition?
this occurs from time to time. I haven't tried out your concrete
example, but there's a rule which could work for your case:
'rev_induct'. You can use it like this:
apply (induction t rule: rev_induct)
Hope that helps.
This archive was generated by a fusion of
Pipermail (Mailman edition) and