Re: [isabelle] Multiple equivalences

Hi Victor,

You can formulate this concisely using set notation:

 lemma "{F1, F2, F3, F4, F5, F6, F7, F8, F9, F10} = {F1}"

Similarly for showing that ten expressions are equal.


On Dec 14, 2010, at 10:51 AM, Victor Porton wrote:

What is the right way to formulate in Isabelle a theorem which states that every two of 10 logical expressions are equivalent?

This is equivalent to 9 equivalences:

(1) <-> (2)
(1) <-> (10)

but that seems not the best way to formulate it.

What is the right way?

(The same for 10 equal (not necessarily logical) terms?)

Victor Porton -

Attachment: smime.p7s
Description: S/MIME cryptographic signature

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