Email Gateway (Aug 18 2022 at 09:49): Email Gateway (Aug 18 2022 at 09:49):From: Julien <julien@cs.uni-sb.de>
Hi All,
I am trying to prove a goal P knowing:
a implies P ; b implies P ; c implies P ; a \/ b \/ c
Each term a, b and c are of the form u /\ v.
The conclusion P is of the form u /\ (x \/ y \/ z ...).
But this should not matter for the proof.
With small formulae, auto or force work. But otherwise they both never
terminate.
Does anyone know what I should use instead of "auto" or "force" to solve
this kind of goal ?
I tried safe but it is not better.
Thanks a lot,
Julien
Email Gateway (Aug 18 2022 at 09:50):From: Tjark Weber <tjark.weber@gmx.de>
Try
lemma "[| a --> P; b --> P; c --> P; a | b | c --> P |]" ==> P
by ((erule disjE)?, erule mp, assumption)+
Best,
Tjark
Email Gateway (Aug 18 2022 at 09:50):From: Tobias Nipkow <nipkow@in.tum.de>
"blast" should do the job.
Tobias
Julien schrieb:
Last updated: May 03 2024 at 08:18 UTC