Email Gateway (Aug 22 2022 at 13:38): Email Gateway (Aug 22 2022 at 13:38):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Hi Andreas,
Much nicer!
Btw, we could have axiomatized BNFs using a version of your axioms (plus the bound) and then defined the set structure from the relator structure:
definition set_G :: "'a G ? 'a set" where
"set_G x = {a . ALL P. rel_G (% a1 a2. a1 = a2 & P a1) x x ? P a}"
Andrei
Last updated: Nov 21 2024 at 12:39 UTC