Re: [isabelle] trivial proof to solve



Clint,

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
this formula.

Are F, S, HS, and EQ defined constants, or just uninterpreted functions?

Best,
Tjark





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