Email Gateway (Aug 18 2022 at 10:07): Email Gateway (Aug 18 2022 at 10:07):From: clefort <ipub@charter.net>
Hello,
Could I offer this trivial proof for some suggestions as to possible
tactics to use. I'm still very much in the infancy "crawling" stage
in Isabelle. I'll appreciate any help.
Hello,
I have myself in a jam with my first trivial proof in Isabelle and
would welcome and suggestions for tactics to be used to resolve it. I
have it down to 1 subgoal now.
theory trivial = Main:
lemma "\<forall>x. \<forall>y. \<forall>z. EQ(F(x,y),S(y,z),EQ(y,x))
\<and> EQ(HS(z,x),F(x,z),S(z,y))
\<Longrightarrow> \<forall>x. \<forall>y.
\<forall>z. EQ(S(y,y),F(x,x),HS(z,z))"
apply (rule conjunct1)
apply (rule conjunct2)
apply (rule conjE)
apply (auto)
Clint LeFort
Immaculata Publishing
111 Cherry St.
Suite 113
Union, Mo
63084-1600
Email Gateway (Aug 18 2022 at 10:07):From: Tjark Weber <tjark.weber@gmx.de>
Clint,
are you using Isabelle/HOL? I am getting a type error when I try to input
this formula.
Are F, S, HS, and EQ defined constants, or just uninterpreted functions?
Best,
Tjark
Last updated: May 03 2024 at 08:18 UTC