# [isabelle] trivial proof to solve

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

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