Core Maude, 315 302 286 277 276 273 bytes

mod E is pr LIST{Int}. ops e i : Int ~> Int . var A B N X Y Z :[Int]. ceq  e(N X A Y B Z)= 1 if(size(X)rem N + size(Y)rem N)size(A)size(B)X B Y A Z = 0 N N i(N(N ^ 2)). ceq e(N X A Y)= 1 if X I:Int Y := i(N(N ^ 2)). eq i(N 0)= nil . eq i(N s A)= i(N A)(0 ^(A rem s N)). endm 

mod E is pr LIST{Int} . ops e i : Int ~> Int . var A B N X Y Z : [Int] . ceq e(N X A Y B Z) = 1 if (size(X) rem N + size(Y) rem N) size(A) size(B) X B Y A Z = 0 N N i(N (N ^ 2)) . ceq e(N X A Y) = 1 if X I:Int Y := i(N (N ^ 2)) .    eq i(N 0) = nil . eq i(N s A) = i(N A) (0 ^ (A rem s N)) . endm 

Saved 3 more bytes using 0 ^ X to do the equivalent of !x in C — i.e., convert non-zero to zero and zero to one. Maude's convention is that \$x ^ 0 = 1\$ even for \$x = 0\$.

Core Maude, 315 302 286 277 276 273 268 bytes

mod E is pr LIST{Int}. ops e i : Int ~> Int . var A B N X Y Z :[Int]. ceq e(N  X A Y B Z)= 1 if(size(X)rem N + size(Y)rem N)size(A)size(B)i(N 0)X B Y A Z = 0 N N i(N(N ^ 2)). ceq e(N X A Y)= 1 if i(N 0)X I:Int Y := i(N(N ^ 2)). eq i(N s A)= i(N A)(0 ^(A rem s N)). endm 

mod E is pr LIST{Int} . ops e i : Int ~> Int . var A B N X Y Z : [Int] . ceq e(N X A Y B Z) = 1 if (size(X) rem N + size(Y) rem N) size(A) size(B) i(N 0) X B Y A Z = 0 N N i(N (N ^ 2)) . ceq e(N X A Y) = 1 if i(N 0) X I:Int Y := i(N (N ^ 2)) . eq i(N s A) = i(N A) (0 ^ (A rem s N)) . endm 

Saved 3 more bytes using 0 ^ X to do the equivalent of !x in C — i.e., convert non-zero to zero and zero to one. Maude's convention is that \$x ^ 0 = 1\$ even for \$x = 0\$.

Saved 5 more bytes by removing the base case for i and handling it in the pattern matches.

Core Maude, 315 302 286 277 276 bytes

mod E is pr LIST{Int}. ops e i : Int ~> Int . var A B N X Y Z :[Int]. ceq e(N X A Y B Z)= 1 if(size(X)rem N + size(Y)rem N)size(A)size(B)X B Y A Z = 0 N N i(N(N ^ 2)). ceq e(N X A Y)= 1 if X I:Int Y := i(N(N ^ 2)). eq i(N 1)= 1 . eq i(N s s A)= i(N s A)(A rem s N quo N). endm 

mod E is pr LIST{Int} . ops e i : Int ~> Int . var A B N X Y Z : [Int] . ceq e(N X A Y B Z) = 1 if (size(X) rem N + size(Y) rem N) size(A) size(B) X B Y A Z = 0 N N i(N (N ^ 2)) . ceq e(N X A Y) = 1 if X I:Int Y := i(N (N ^ 2)) . eq i(N 1) = 1 . eq i(N s s A) = i(N s A) (A rem s N quo N) . endm 

Saved 9 10 more bytes by combining conditions into one list equality.

Core Maude, 315 302 286 277 276 273 bytes

mod E is pr LIST{Int}. ops e i : Int ~> Int . var A B N X Y Z :[Int]. ceq e(N X A Y B Z)= 1 if(size(X)rem N + size(Y)rem N)size(A)size(B)X B Y A Z = 0 N N i(N(N ^ 2)). ceq e(N X A Y)= 1 if X I:Int Y := i(N(N ^ 2)). eq i(N 0)= nil . eq i(N s A)= i(N A)(0 ^(A rem s N)). endm 

mod E is pr LIST{Int} . ops e i : Int ~> Int . var A B N X Y Z : [Int] . ceq e(N X A Y B Z) = 1 if (size(X) rem N + size(Y) rem N) size(A) size(B) X B Y A Z = 0 N N i(N (N ^ 2)) . ceq e(N X A Y) = 1 if X I:Int Y := i(N (N ^ 2)) . eq i(N 0) = nil . eq i(N s A) = i(N A) (0 ^ (A rem s N)) . endm 

Saved 9 10 more bytes by combining conditions into one list equality.

Saved 3 more bytes using 0 ^ X to do the equivalent of !x in C — i.e., convert non-zero to zero and zero to one. Maude's convention is that \$x ^ 0 = 1\$ even for \$x = 0\$.

Core Maude, 315 302 286 bytes

mod E is pr LIST{Int}. ops e i : Int ~> Int . var A B N X Y Z :[Int]. ceq e(N  X A Y B Z)= 1 if size(X)rem N + size(Y)rem N = 0 /\ size(A)size(B)= N N /\ X B Y A Z = i(N(N ^ 2)). ceq e(N X A Y)= 1 if X I:Int Y := i(N(N ^ 2)). eq  i(N 1)= 1 . eq i(N s s A)= i(N s A)(A rem s N quo N). endm 

mod E is pr LIST{Int} . ops e i : Int ~> Int . var A B N X Y Z : [Int] . ceq e(N X A Y B Z) = 1 if size(X) rem N + size(Y) rem N = 0 /\ size(A) size(B) = N N  /\ X B Y A Z = i(N (N ^ 2)) . ceq e(N X A Y) = 1 if X I:Int Y := i(N (N ^ 2)) . eq i(N 1) = 1 . eq i(N s s A) = i(N s A) (A rem s N quo N) . endm 

Saved 16 more bytes by collapsing multiplying and adding into a single case and changing the signature to only one list argument with length prepended.

Core Maude, 315 302 286 277 276 bytes

mod E is pr LIST{Int}. ops e i : Int ~> Int . var A B N X Y Z :[Int]. ceq  e(N X A Y B Z)= 1 if(size(X)rem N + size(Y)rem N)size(A)size(B)X B Y A Z = 0 N N i(N(N ^ 2)). ceq e(N X A Y)= 1 if X I:Int Y := i(N(N ^ 2)). eq i(N 1)=  1 . eq i(N s s A)= i(N s A)(A rem s N quo N). endm 

mod E is pr LIST{Int} . ops e i : Int ~> Int . var A B N X Y Z : [Int] . ceq e(N X A Y B Z) = 1 if (size(X) rem N + size(Y) rem N) size(A) size(B) X B Y A Z  = 0 N N i(N (N ^ 2)) . ceq e(N X A Y) = 1 if X I:Int Y := i(N (N ^ 2)) . eq i(N 1) = 1 . eq i(N s s A) = i(N s A) (A rem s N quo N) . endm 

Saved 16 more bytes by collapsing multiplying and adding into a single case and changing the signature to only one list argument with length prepended.

Saved 9 10 more bytes by combining conditions into one list equality.