Is it possible to get good termination condition extraction for functions
like listTheory$MAP2?
I can prove something like this:
|- ∀l1 l1' l2 l2' f f'.
(l1 = l1') ∧ (l2 = l2') ∧ (LENGTH l1 = LENGTH l2) ∧
(∀x y. MEM x l1' ∧ MEM y l2' ⇒ (f x y = f' x y)) ⇒
(MAP2 f l1 l2 = MAP2 f' l1' l2')
But it's probably of the wrong form (because of the condition about the
lengths being equal), and indeed adding it to the database in DefnBase
doesn't help with termination condition extraction for uses of MAP2.
Without a condition like that, though, I think the congruence is unprovable.
Is there a right form?
------------------------------------------------------------------------------
This SF email is sponsosred by:
Try Windows Azure free for 90 days Click Here
http://p.sf.net/sfu/sfd2d-msazure
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
