Email Gateway (Aug 23 2022 at 08:43): Email Gateway (Aug 23 2022 at 08:43):From: Pedro Sánchez Terraf <sterraf@famaf.unc.edu.ar>
Dear all,
I would like to know if [trans] rules can have additional assumptions.
Meaning, I have a binary relation ≈r that is transitive when arguments
are restricted, something like this:
"[| M(X); M(Y) ; M(Z); X ≈r Y; Y ≈r Z |] ==> X ≈r Z".
However, I couldn't make this work using "also ... finally ...". Must
trans rules only state the plain transitivity unconditionally?
Thanks in advance.
PS. I've been searching the mailing list archives using Google with
"site:lists.cam.ac.uk/pipermail/cl-isabelle-users/". Is there a more
efficient approach to search through them?
PST.-
cs.famaf.unc.edu.ar/~pedro/home_en
<https://cs.famaf.unc.edu.ar/~pedro/home_en.html>
Email Gateway (Aug 23 2022 at 08:44):From: Pedro Sánchez Terraf <sterraf@famaf.unc.edu.ar>
El 20/3/20 a las 09:57, Pedro Sánchez Terraf escribió:
I think I solved the issue... Perhaps it is enough to move assumptions a
bit:
"[|X ≈r Y; Y ≈r Z; M(X); M(Y) ; M(Z) |] ==> X ≈r Z"?
Last updated: Nov 21 2024 at 12:39 UTC