(let ((a!1 (and <tail>))) (=> a!1 <head>))
chc_tail ::= | (and (u_predicate var+)* i_formula*)
(u_predicate var*)needs to be changed to
u_predicateshould either always or never be required to be over distinct variables. (I'm fine either way.) I think it would make the rules simpler and less confusing thanks to uniformity.
I actually don't want anything, neither as a participant for my tool or an organizer for the formatting script. Whatever the rules end up being my tool will support them (modulo bug) and I'll modify the script in consequence. I was trying to make the rules simpler.
chc_tail my point was simply that we can remove the first two variants and only keep the
The formatting script produces systems in a fragment a bit more restrictive than the one from the rules, I'll update the google doc shortly if you want to take a look.