Email Gateway (Jan 23 2024 at 12:01): Email Gateway (Jan 23 2024 at 12:01):From: Lawrence Paulson <lp15@cam.ac.uk>
I'm happy to announce a new entry: Decomposition of totally ordered hoops, by Sebastián Buss.
We formalize a well known result in theory of hoops: every totally ordered hoop can be written as an ordinal sum of irreducible (equivalently Wajsberg) hoops. This formalization is based on the proof for BL-chains (i.e., bounded totally ordered hoops) found in Decomposition of BL-chains by M. Busaniche (Algebra Universalis, 2005).
It is now online at https://www.isa-afp.org/entries/Isabelle_hoops.html
Larry
Last updated: May 05 2024 at 04:19 UTC