Email Gateway (Aug 18 2022 at 13:10): Email Gateway (Aug 18 2022 at 13:10):From: Stephy Wong <s.wong.731@googlemail.com>
Hi,
I have a rather basic problem and hope someone could help me out.
I have no idea why the following fails:
axioms Ax1 [rule_format] : "!! x y z. (y = Foo(z)) = (gn_inj_Int(Bar(x, y))
' 0'"
theorem t: "!! x y. gn_inj_Int(Bar(x, Foo(y))) >' 0"
using Ax1
by auto
Since Ax1 says that (gn_inj_Int(Bar(x, y)) >' 0 if and only if the second
argument of Bar is Foo(z), then how come t can't be proved?
Any help will be appreciated.
Regards,
Steph
Email Gateway (Aug 18 2022 at 13:10):From: Tobias Nipkow <nipkow@in.tum.de>
Just like simp, auto uses equations only in the left-to-right direction.
Tobias
PS you don't need any of the !! or the [rule_format].
Stephy Wong schrieb:
Last updated: May 03 2024 at 08:18 UTC