Email Gateway (Aug 18 2022 at 10:53): Email Gateway (Aug 18 2022 at 10:53):From: RF Todd <R.F.Todd@sms.ed.ac.uk>
Hi,
I have just been trying to type the following into Isabelle in order
to prove it, if it is provable, but it comes up with an error and i am
not sure why:
(\<forall>x y. (S y \<longrightarrow> F x)) \<longrightarrow>
(\<exists>y. S y \<longrightarrow> \<forall>x. F x)
Rachel
Email Gateway (Aug 18 2022 at 10:53):From: Tjark Weber <tjark.weber@gmx.de>
Try using parentheses around "\<forall>x. F x":
lemma "(\<forall>x y. (S y \<longrightarrow> F x)) \<longrightarrow>
(\<exists>y. S y \<longrightarrow> (\<forall>x. F x))"
by auto
Tjark
Email Gateway (Aug 18 2022 at 19:25):From: Andrei Popescu <uuomul@yahoo.com>
this is pretty awesome you should look into this http://t.co/2c7wNQ4r
~*Advertisement
Last updated: Apr 25 2024 at 16:19 UTC