[isabelle] trivial proof to solve


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.


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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.