Email Gateway (Aug 18 2022 at 16:41): Email Gateway (Aug 18 2022 at 16:41):From: Victor Porton <porton@narod.ru>
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 - http://portonvictor.org
Email Gateway (Aug 18 2022 at 16:41):From: John Matthews <matthews@galois.com>
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.
-john
smime.p7s
Last updated: Nov 21 2024 at 12:39 UTC