print(`ROB PRATT's DISTINCT DNF TAUTOLOGY WITH 10 VARIABLES and >=7 LITERALS IN EACH TERM `): print(``): print(`Aug. 24, 2020 `): print(``): print(`This is a short Maple procedure to display and test Rob Pratt's amazing Distinct DNF tautology`): print(`To see it, type `): print(` Rob; `): print(``): print(`to test it type `): print(``): print(`CheckDT(Rob,X,Y,10,7); `): print(``): #Rob Pratt's amazing DISTINCT DNF TAUTOLOFGY meeting the challenge of the Zaleski-Zeilberger paper # It has ten variables X[1], ..., X[10] and each term with >=7 literals. Y[i] denotes not X[i], * denotes AND and + denotes OR #The procedure below CheckDT(f,X,Y,n,k) checks that a DNF given in that format is indeed what it claims to be. #Typing #CheckDT(Rob,X,Y,10,7); #returns true Rob:= Y[1]*X[2]*X[3]*Y[4]*Y[5]*X[6]*X[7] + X[1]*X[2]*Y[3]*Y[4]*Y[5]*Y[6]*Y[8] + X[1]*X[2]*Y[3]*X[4]*Y[5]*X[7]*X[8] + X[1]*Y[2]*Y[3]*Y[4]*Y[6]*Y[7]*Y[8] + X[1]*X[2]*X[3]*X[5]*X[6]*X[7]*Y[8] + X[1]*Y[2]*Y[4]*X[5]*X[6]*Y[7]*Y[8] + Y[1]*Y[3]*X[4]*X[5]*X[6]*Y[7]*Y[8] + Y[2]*X[3]*Y[4]*X[5]*X[6]*Y[7]*X[8] + X[1]*X[2]*X[3]*X[4]*X[5]*Y[6]*Y[9] + Y[1]*X[2]*X[3]*Y[4]*X[5]*Y[7]*X[9] + X[1]*Y[2]*Y[3]*X[4]*Y[6]*Y[7]*X[9] + X[1]*Y[2]*X[3]*X[5]*X[6]*X[7]*Y[9] + X[1]*X[2]*Y[4]*Y[5]*X[6]*Y[7]*X[9] + Y[1]*X[3]*Y[4]*Y[5]*X[6]*Y[7]*X[9] + Y[2]*Y[3]*X[4]*Y[5]*X[6]*X[7]*Y[9] + Y[1]*Y[2]*X[3]*Y[4]*X[5]*Y[8]*X[9] + Y[1]*X[2]*Y[3]*X[4]*Y[6]*Y[8]*Y[9] + Y[1]*X[2]*X[3]*Y[5]*Y[6]*X[8]*X[9] + X[1]*Y[2]*X[4]*Y[5]*Y[6]*X[8]*Y[9] + X[1]*Y[3]*X[4]*Y[5]*Y[6]*Y[8]*Y[9] + X[2]*Y[3]*Y[4]*X[5]*X[6]*X[8]*X[9] + Y[1]*Y[2]*Y[3]*X[4]*X[7]*Y[8]*X[9] + X[1]*Y[2]*X[3]*X[5]*X[7]*X[8]*X[9] + X[1]*X[2]*Y[4]*Y[5]*X[7]*X[8]*X[9] + Y[1]*Y[3]*Y[4]*X[5]*Y[7]*Y[8]*X[9] + Y[2]*Y[3]*Y[4]*X[5]*X[7]*X[8]*X[9] + Y[1]*Y[2]*Y[3]*X[6]*Y[7]*Y[8]*Y[9] + Y[1]*X[2]*X[4]*X[6]*X[7]*X[8]*Y[9] + Y[1]*X[3]*X[4]*Y[6]*X[7]*X[8]*Y[9] + X[2]*Y[3]*X[4]*X[6]*X[7]*Y[8]*Y[9] + X[1]*X[2]*X[5]*X[6]*Y[7]*Y[8]*X[9] + X[1]*X[3]*X[5]*Y[6]*X[7]*Y[8]*X[9] + X[2]*Y[3]*X[5]*X[6]*X[7]*Y[8]*X[9] + X[1]*Y[4]*Y[5]*X[6]*X[7]*Y[8]*X[9] + Y[2]*X[4]*X[5]*X[6]*Y[7]*Y[8]*X[9] + X[3]*X[4]*Y[5]*X[6]*X[7]*X[8]*X[9] + Y[1]*X[2]*Y[3]*Y[4]*X[5]*Y[6]*Y[10] + Y[1]*X[2]*Y[3]*Y[4]*Y[5]*X[7]*X[10] + Y[1]*X[2]*X[3]*Y[4]*Y[6]*X[7]*Y[10] + Y[1]*X[2]*X[3]*X[5]*X[6]*X[7]*Y[10] + Y[1]*Y[2]*X[4]*Y[5]*X[6]*Y[7]*X[10] + Y[1]*X[3]*Y[4]*X[5]*Y[6]*X[7]*X[10] + Y[2]*Y[3]*Y[4]*Y[5]*Y[6]*X[7]*Y[10] + X[1]*X[2]*X[3]*X[4]*Y[5]*Y[8]*X[10] + Y[1]*X[2]*X[3]*X[4]*Y[6]*Y[8]*Y[10] + X[1]*X[2]*Y[3]*X[5]*Y[6]*Y[8]*X[10] + X[1]*X[2]*X[4]*X[5]*X[6]*X[8]*Y[10] + X[1]*X[3]*Y[4]*Y[5]*Y[6]*Y[8]*Y[10] + Y[2]*X[3]*Y[4]*Y[5]*X[6]*X[8]*X[10] + Y[1]*X[2]*X[3]*X[4]*X[7]*Y[8]*X[10] + Y[1]*Y[2]*X[3]*Y[5]*X[7]*Y[8]*Y[10] + Y[1]*Y[2]*X[4]*X[5]*Y[7]*X[8]*X[10] + Y[1]*Y[3]*Y[4]*Y[5]*Y[7]*X[8]*Y[10] + Y[2]*X[3]*Y[4]*Y[5]*X[7]*X[8]*Y[10] + X[1]*Y[2]*Y[3]*X[6]*Y[7]*X[8]*X[10] + Y[1]*Y[2]*X[4]*Y[6]*Y[7]*Y[8]*X[10] + X[1]*Y[3]*Y[4]*Y[6]*Y[7]*X[8]*Y[10] + Y[2]*Y[3]*Y[4]*Y[6]*X[7]*Y[8]*X[10] + X[1]*X[2]*X[5]*Y[6]*X[7]*X[8]*X[10] + X[1]*X[3]*X[5]*Y[6]*Y[7]*Y[8]*X[10] + Y[2]*X[3]*Y[5]*Y[6]*Y[7]*X[8]*Y[10] + Y[1]*Y[4]*Y[5]*Y[6]*Y[7]*Y[8]*Y[10] + Y[2]*X[4]*X[5]*X[6]*Y[7]*X[8]*Y[10] + X[3]*Y[4]*X[5]*X[6]*X[7]*X[8]*X[10] + X[1]*X[2]*X[3]*X[4]*Y[5]*Y[9]*Y[10] + Y[1]*X[2]*Y[3]*X[4]*Y[6]*X[9]*Y[10] + X[1]*X[2]*Y[3]*X[5]*Y[6]*X[9]*Y[10] + X[1]*X[2]*Y[4]*X[5]*X[6]*Y[9]*X[10] + X[1]*Y[3]*Y[4]*Y[5]*X[6]*Y[9]*X[10] + X[2]*Y[3]*Y[4]*X[5]*X[6]*Y[9]*X[10] + X[1]*Y[2]*Y[3]*X[4]*X[7]*X[9]*X[10] + Y[1]*X[2]*Y[3]*Y[5]*X[7]*X[9]*Y[10] + Y[1]*Y[2]*Y[4]*X[5]*X[7]*Y[9]*Y[10] + X[1]*Y[3]*Y[4]*X[5]*X[7]*Y[9]*Y[10] + X[2]*Y[3]*Y[4]*Y[5]*X[7]*Y[9]*Y[10] + X[1]*Y[2]*Y[3]*X[6]*X[7]*X[9]*Y[10] + Y[1]*X[2]*X[4]*Y[6]*Y[7]*X[9]*X[10] + Y[1]*X[3]*Y[4]*Y[6]*Y[7]*Y[9]*X[10] + Y[2]*Y[3]*X[4]*Y[6]*X[7]*X[9]*Y[10] + X[1]*Y[2]*Y[5]*X[6]*Y[7]*X[9]*Y[10] + X[1]*X[3]*X[5]*Y[6]*Y[7]*X[9]*Y[10] + Y[2]*Y[3]*X[5]*X[6]*X[7]*Y[9]*X[10] + Y[1]*X[4]*Y[5]*X[6]*Y[7]*X[9]*Y[10] + Y[2]*X[4]*X[5]*X[6]*X[7]*Y[9]*Y[10] + Y[3]*X[4]*Y[5]*X[6]*Y[7]*Y[9]*Y[10] + X[1]*X[2]*X[3]*Y[4]*X[8]*Y[9]*Y[10] + X[1]*Y[2]*X[3]*Y[5]*Y[8]*Y[9]*Y[10] + X[1]*X[2]*X[4]*Y[5]*Y[8]*X[9]*Y[10] + Y[1]*Y[3]*X[4]*Y[5]*X[8]*X[9]*X[10] + X[2]*Y[3]*X[4]*Y[5]*Y[8]*X[9]*X[10] + Y[1]*Y[2]*X[3]*X[6]*Y[8]*Y[9]*X[10] + Y[1]*Y[2]*X[4]*Y[6]*Y[8]*Y[9]*Y[10] + Y[1]*Y[3]*X[4]*Y[6]*X[8]*Y[9]*X[10] + X[2]*Y[3]*X[4]*Y[6]*X[8]*Y[9]*Y[10] + X[1]*Y[2]*X[5]*Y[6]*X[8]*Y[9]*X[10] + X[1]*X[3]*Y[5]*X[6]*X[8]*Y[9]*X[10] + X[2]*X[3]*Y[5]*Y[6]*Y[8]*X[9]*X[10] + X[1]*X[4]*X[5]*Y[6]*Y[8]*Y[9]*Y[10] + X[2]*X[4]*X[5]*X[6]*X[8]*X[9]*X[10] + Y[3]*Y[4]*X[5]*X[6]*X[8]*Y[9]*Y[10] + Y[1]*X[2]*X[3]*Y[7]*X[8]*Y[9]*Y[10] + Y[1]*X[2]*X[4]*Y[7]*Y[8]*Y[9]*X[10] + Y[1]*Y[3]*Y[4]*Y[7]*X[8]*Y[9]*X[10] + X[2]*Y[3]*X[4]*Y[7]*X[8]*Y[9]*X[10] + X[1]*Y[2]*Y[5]*Y[7]*Y[8]*X[9]*X[10] + X[1]*X[3]*Y[5]*Y[7]*Y[8]*Y[9]*X[10] + Y[2]*X[3]*Y[5]*X[7]*Y[8]*X[9]*X[10] + Y[1]*X[4]*X[5]*X[7]*X[8]*X[9]*X[10] + Y[2]*Y[4]*Y[5]*X[7]*X[8]*X[9]*X[10] + X[3]*Y[4]*Y[5]*X[7]*Y[8]*Y[9]*X[10] + X[1]*X[2]*Y[6]*Y[7]*X[8]*X[9]*X[10] + Y[1]*X[3]*X[6]*Y[7]*Y[8]*Y[9]*Y[10] + Y[2]*Y[3]*Y[6]*Y[7]*Y[8]*Y[9]*X[10] + Y[1]*X[4]*Y[6]*Y[7]*Y[8]*X[9]*Y[10] + Y[2]*X[4]*Y[6]*X[7]*Y[8]*Y[9]*X[10] + X[3]*X[4]*Y[6]*X[7]*X[8]*X[9]*Y[10] + X[1]*X[5]*X[6]*Y[7]*Y[8]*Y[9]*Y[10] + Y[2]*X[5]*Y[6]*Y[7]*X[8]*Y[9]*Y[10] + X[3]*Y[5]*Y[6]*Y[7]*X[8]*Y[9]*X[10] + Y[4]*X[5]*Y[6]*Y[7]*Y[8]*Y[9]*Y[10] + Y[1]*X[2]*Y[3]*Y[4]*Y[5]*X[6]*Y[7]*Y[8] + Y[1]*Y[2]*Y[3]*Y[4]*Y[5]*X[6]*X[7]*Y[9] + Y[1]*Y[2]*Y[3]*Y[4]*Y[5]*X[6]*Y[8]*X[9] + Y[1]*Y[2]*X[3]*X[4]*X[5]*X[7]*Y[8]*X[9] + Y[1]*X[2]*X[3]*X[4]*X[6]*Y[7]*Y[8]*X[9] + X[1]*Y[2]*X[3]*X[5]*X[6]*X[7]*Y[8]*X[9] + X[1]*X[2]*X[4]*Y[5]*X[6]*Y[7]*X[8]*X[9] + X[1]*X[3]*Y[4]*X[5]*Y[6]*X[7]*Y[8]*Y[9] + Y[2]*Y[3]*Y[4]*X[5]*X[6]*Y[7]*X[8]*X[9] + Y[1]*X[2]*X[3]*X[4]*Y[5]*X[6]*X[7]*Y[10] + Y[1]*X[2]*Y[3]*X[4]*X[5]*X[6]*X[8]*Y[10] + Y[1]*X[2]*X[3]*Y[4]*X[5]*X[7]*Y[8]*X[10] + Y[1]*X[2]*X[3]*X[4]*X[6]*Y[7]*X[8]*X[10] + Y[1]*X[2]*Y[3]*X[5]*Y[6]*X[7]*Y[8]*X[10] + X[1]*Y[2]*Y[4]*Y[5]*Y[6]*Y[7]*X[8]*X[10] + X[1]*X[3]*X[4]*Y[5]*Y[6]*X[7]*X[8]*X[10] + Y[2]*Y[3]*Y[4]*Y[5]*Y[6]*X[7]*X[8]*X[10] + X[1]*Y[2]*Y[3]*Y[4]*Y[5]*X[6]*Y[9]*Y[10] + X[1]*X[2]*X[3]*Y[4]*Y[5]*X[7]*Y[9]*Y[10] + Y[1]*X[2]*X[3]*Y[4]*X[6]*Y[7]*Y[9]*X[10] + X[1]*X[2]*X[3]*Y[5]*Y[6]*Y[7]*X[9]*Y[10] + X[1]*X[2]*Y[4]*Y[5]*X[6]*Y[7]*Y[9]*Y[10] + X[1]*X[3]*X[4]*X[5]*X[6]*Y[7]*Y[9]*X[10] + Y[2]*X[3]*X[4]*Y[5]*X[6]*X[7]*Y[9]*X[10] + X[1]*Y[2]*X[3]*X[4]*Y[5]*Y[8]*X[9]*Y[10] + Y[1]*Y[2]*Y[3]*X[4]*Y[6]*X[8]*Y[9]*Y[10] + Y[1]*Y[2]*X[3]*Y[5]*Y[6]*X[8]*X[9]*X[10] + Y[1]*X[2]*Y[4]*X[5]*Y[6]*X[8]*X[9]*X[10] + X[1]*Y[3]*Y[4]*Y[5]*Y[6]*X[8]*Y[9]*X[10] + X[2]*Y[3]*Y[4]*X[5]*X[6]*Y[8]*Y[9]*Y[10] + X[1]*Y[2]*X[3]*X[4]*Y[7]*X[8]*X[9]*X[10] + Y[1]*Y[2]*X[3]*X[5]*X[7]*X[8]*X[9]*Y[10] + Y[1]*X[2]*X[4]*X[5]*Y[7]*X[8]*X[9]*Y[10] + Y[1]*Y[3]*Y[4]*Y[5]*Y[7]*X[8]*X[9]*X[10] + Y[2]*Y[3]*Y[4]*X[5]*X[7]*Y[8]*X[9]*Y[10] + Y[1]*Y[2]*Y[3]*X[6]*X[7]*X[8]*X[9]*Y[10] + X[1]*X[2]*X[4]*X[6]*X[7]*X[8]*Y[9]*X[10] + X[1]*Y[3]*X[4]*X[6]*Y[7]*Y[8]*Y[9]*X[10] + Y[2]*Y[3]*Y[4]*X[6]*X[7]*Y[8]*X[9]*X[10] + Y[1]*Y[2]*X[5]*Y[6]*Y[7]*X[8]*X[9]*Y[10] + Y[1]*Y[3]*X[5]*Y[6]*X[7]*X[8]*Y[9]*X[10] + Y[2]*X[3]*Y[5]*X[6]*Y[7]*X[8]*Y[9]*Y[10] + Y[1]*Y[4]*Y[5]*Y[6]*Y[7]*Y[8]*X[9]*X[10] + Y[2]*Y[4]*X[5]*Y[6]*Y[7]*X[8]*X[9]*X[10] + X[3]*Y[4]*Y[5]*Y[6]*X[7]*X[8]*Y[9]*X[10] + X[1]*X[2]*X[3]*Y[4]*X[5]*X[6]*Y[7]*X[8]*X[9] + Y[1]*X[2]*X[3]*X[4]*X[5]*Y[6]*Y[7]*X[8]*X[10] + Y[1]*Y[2]*X[3]*X[4]*X[5]*X[6]*X[7]*Y[9]*X[10] + X[1]*Y[2]*Y[3]*X[4]*X[5]*Y[6]*X[8]*Y[9]*Y[10] + X[1]*X[2]*X[3]*Y[4]*X[5]*X[7]*X[8]*X[9]*Y[10] + Y[1]*X[2]*Y[3]*Y[4]*Y[6]*Y[7]*Y[8]*Y[9]*X[10] + X[1]*Y[2]*X[3]*X[5]*Y[6]*X[7]*X[8]*Y[9]*Y[10] + X[1]*X[2]*Y[4]*X[5]*Y[6]*Y[7]*X[8]*Y[9]*X[10] + X[1]*Y[3]*X[4]*Y[5]*Y[6]*Y[7]*X[8]*X[9]*Y[10] + Y[2]*X[3]*X[4]*Y[5]*X[6]*X[7]*X[8]*Y[9]*Y[10] + Y[1]*Y[2]*Y[3]*X[4]*Y[5]*Y[6]*Y[7]*X[8]*X[9]*Y[10] : #A(n): the set of all 0-1 vectors of length n A:=proc(n) local gu,gu1: option remember: if n=0 then RETURN({[]}): fi: gu:=A(n-1): {seq([op(gu1),0],gu1 in gu),seq([op(gu1),1],gu1 in gu)}: end: #CheckDT(f,X,Y,n,k): checks that f is indeed a Distinct DNF tautology CheckDT:=proc(f,X,Y,n,k) local gu,gu1,i,lu: gu:=[op(f)]: lu:=convert(subs({seq(Y[i]=X[i],i=1..n)},gu),set): if nops(gu)<>nops(lu) then print(`Not distinct`): RETURN(false): fi: if min(seq(nops(gu[i]),i=1..nops(gu)))