Small Cosmetic Changes to RARE rules (cvc5#11666)

I apologize in advance for needing this change but I keep messing up
thinking that y3 isn't a list and zs is.

Author: Lachnitt

proofs/eo/cpc/rules/Rewrites.eo

@@ -339,13 +339,13 @@
   :args (x1 y1 zs1)
   :conclusion (= (not (and x1 y1 zs1)) (or (not x1) (not ($singleton_elim (and y1 zs1)))))
 )
-(declare-rule bool-or-and-distrib ((y1 Bool) (y2 Bool) (y3 Bool :list) (zs1 Bool :list))
-  :args (y1 y2 y3 zs1)
-  :conclusion (= ($singleton_elim (or (and y1 y2 y3) zs1)) (and ($singleton_elim (or y1 zs1)) ($singleton_elim (or ($singleton_elim (and y2 y3)) zs1))))
+(declare-rule bool-or-and-distrib ((y1 Bool) (y2 Bool) (ys1 Bool :list) (zs1 Bool :list))
+  :args (y1 y2 ys1 zs1)
+  :conclusion (= ($singleton_elim (or (and y1 y2 ys1) zs1)) (and ($singleton_elim (or y1 zs1)) ($singleton_elim (or ($singleton_elim (and y2 ys1)) zs1))))
 )
-(declare-rule bool-implies-or-distrib ((y1 Bool) (y2 Bool) (y3 Bool :list) (zs1 Bool))
-  :args (y1 y2 y3 zs1)
-  :conclusion (= (=> (or y1 y2 y3) zs1) (and (=> y1 zs1) (=> ($singleton_elim (or y2 y3)) zs1)))
+(declare-rule bool-implies-or-distrib ((y1 Bool) (y2 Bool) (ys1 Bool :list) (z1 Bool))
+  :args (y1 y2 ys1 z1)
+  :conclusion (= (=> (or y1 y2 ys1) z1) (and (=> y1 z1) (=> ($singleton_elim (or y2 ys1)) z1)))
 )
 (declare-rule bool-xor-refl ((x1 Bool))
   :args (x1)

src/theory/booleans/rewrites

@@ -42,16 +42,16 @@
 
 ; We only permit distributing from the first child, or otherwise this rule
 ; could apply to fix point on all AND children of an OR at once.
-(define-rule* bool-or-and-distrib ((y1 Bool) (y2 Bool) (y3 Bool :list) (zs Bool :list))
-  (or (and y1 y2 y3) zs)
-  (or (and y2 y3) zs)
+(define-rule* bool-or-and-distrib ((y1 Bool) (y2 Bool) (ys Bool :list) (zs Bool :list))
+  (or (and y1 y2 ys) zs)
+  (or (and y2 ys) zs)
   (and (or y1 zs) _))
 
 ; Used for diamonds preprocessing
-(define-rule* bool-implies-or-distrib ((y1 Bool) (y2 Bool) (y3 Bool :list) (zs Bool))
-  (=> (or y1 y2 y3) zs)
-  (=> (or y2 y3) zs)
-  (and (=> y1 zs) _))
+(define-rule* bool-implies-or-distrib ((y1 Bool) (y2 Bool) (ys Bool :list) (z Bool))
+  (=> (or y1 y2 ys) z)
+  (=> (or y2 ys) z)
+  (and (=> y1 z) _))
 
 (define-rule bool-xor-refl ((x Bool)) (xor x x) false)
 (define-rule bool-xor-nrefl ((x Bool)) (xor x (not x)) true)