[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))
\<Longrightarrow> \<forall>x. \<forall>y.
apply (rule conjunct1)
apply (rule conjunct2)
apply (rule conjE)
111 Cherry St.
This archive was generated by a fusion of
Pipermail (Mailman edition) and