Re: [isabelle] trivial proof to solve
On Thursday 11 January 2007 16:55, clefort wrote:
> 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))"
are you using Isabelle/HOL? I am getting a type error when I try to input
Are F, S, HS, and EQ defined constants, or just uninterpreted functions?
This archive was generated by a fusion of
Pipermail (Mailman edition) and