OKlibrary
0.2.1.6

Investigations regarding the presentation of unary addition. More...
Go to the source code of this file.
Investigations regarding the presentation of unary addition.
declare(una,noun)$ declare(una,posfun)$ una_var(v,i) := apply(nounify(una),[v,i])$ una_var_l(v,a,b) := create_list(una_var(v,i),i,a,b)$ unary_all_tass_std(p,q) := all_tass(append( una_var_l('x,1,max(p,1)),una_var_l('y,1,max(q,1)), una_var_l('z,1,max(p+q,2))))$ unary_add_full_dnf_fcl_std(p,q) := unary_add_full_dnf_fcl( una_var_l('x,1,max(p,1)),una_var_l('y,1,max(q,1)), una_var_l('z,1,max(p+q,2)))$ unary_add_full_dnf_fcl(X,Y,Z) := [append(X,Y,Z),create_list( setify(append( create_list(if i > p then X[i] else X[i], i, 1, length(X)), create_list(if j > q then Y[j] else Y[j], j, 1, length(Y)), create_list(if k > p+q then Z[k] else Z[k], k, 1, length(Z)))), p,0,length(X), q, 0, length(Y))]$ unary_add_cnf_fcl_std(p,q) := unary_add_cnf_fcl( una_var_l('x,1,max(p,1)),una_var_l('y,1,max(q,1)), una_var_l('z,1,max(p,1)+max(q,1)))$ unary_add_cnf_fcl(X,Y,Z) := [append(X,Y,Z), create_list( comp_sl(setify(append( create_list(if i > p then X[i] else X[i], i, 1, length(X)), create_list(if j > q then Y[j] else Y[j], j, 1, length(Y)), [if r > p+q then Z[r] else Z[r]]))), p,0,length(X), q, 0, length(Y), r, 1, length(X)+length(Y))]$
m : 2; n : 2; print("p q #min_F_0 stat_min_F #min_F_1 stat_min_F_1 stat_BB_F Eq_0? Eq_1?"); for p : 0 thru m do for q : 0 thru n do block([min_F_0_l, BB_F], min_F_0_l : all_minequiv_bvsr_cs(expand_fcs(map(setify,unary_add_cnf_fcl_std(p,q)))[2]), min_F_1_l : all_minequiv_bvsr_cs( map(comp_sl, setdifference(unary_all_tass_std(p,q), setify(unary_add_full_dnf_fcl_std(p,q)[2])))), BB_F : setify(unary_bb_add_fcl( una_var_l('x,1,max(1,p)),una_var_l('y,1,max(1,q)), una_var_l('z,1,max(p,1)+max(q,1)))[2]), print(p,q,length(min_F_0_l),statistics_cs(min_F_0_l[1]), length(min_F_1_l),statistics_cs(min_F_1_l[1]),statistics_cs(BB_F), is(min_F_0_l[1] = BB_F), is(min_F_1_l[1] = BB_F)))$
p q #min_F_0 stat_min_F #min_F_1 stat_min_F_1 stat_BB_F Eq_0? Eq_1? 0 0 1 [4,6,14,3,2] 1 [4,6,14,3,2] [4,6,14,3,2] true true 0 1 1 [4,6,14,3,2] 1 [4,6,14,3,2] [4,6,14,3,2] true true 0 2 1 [6,10,30,4,2] 1 [5,7,17,3,2] [6,10,24,3,2] false false 1 0 1 [4,6,14,3,2] 1 [4,6,14,3,2] [4,6,14,3,2] true true 1 1 1 [4,6,14,3,2] 1 [4,6,14,3,2] [4,6,14,3,2] true true 1 2 1 [6,10,30,4,2] 1 [6,10,24,3,2] [6,10,24,3,2] false true 2 0 1 [6,10,30,4,2] 1 [5,7,17,3,2] [6,10,24,3,2] false false 2 1 1 [6,10,30,4,2] 1 [6,10,24,3,2] [6,10,24,3,2] false true *timeout*
unary_add_min_reps(m,n) := all_minequiv_bvsr_sub_cs( unary_add_full_dnf_fcl_std(m,n)[2], setdifference(unary_all_tass_std(m,n),setify(map(comp_sl,unary_add_cnf_fcl_std(m,n)[2]))))$ unary_add_min_reps(1,1);
Definition in file UnaryAddition.hpp.