1:- module(count_algebra, [bin_symm_funs/3]).    2:- use_module(library(apply)).    3:- use_module(library(apply_macros)).    4:- use_module(library(clpfd)).    5:- use_module(library(statistics)).    6:- use_module(zdd('zdd-array')).    7:- use_module(util(meta2)).    8:- use_module(pac(basic)).    9:- use_module(pac(meta)).   10:- use_module(util(math)).   11:- use_module(pac('expand-pac')). % For the kind block.
   12:- use_module(zdd('zdd-misc')).   13:- use_module(zdd(zdd)).   14:- use_module(pac(op)).   15
   16:- set_prolog_flag(stack_limit, 10_200_147_483_648).   17
   18 :- op(1060, xfy, ~).		% equivalence
   19 :- op(1060, xfy, #).		% exor
   20 :- op(1060, xfy, <->).		% equivalence
   21 :- op(1050, yfx, <-).   22 :- op(1060, xfy, <=> ).	% equivalence
   23 :- op(1040, xfy, \/).		% OR
   24 :- op(1030, xfy, /\).		% AND
   25 :- op(1020, fy, \).		% NOT
   26 :- op(700, xfx, :=).		% Assignment
   27 :- op(1000, xfy, &).   28
   29% For pac query.
   30 :- pac:op(1000, xfy, &).   31 :- pac:op(700, xfx, :=).   32
   33term_expansion --> pac:expand_pac.
   34
   35% :- meta_predicate(@(:)).
   36% @(X):- shift(X).
   37
   38join(X, Y, Z):- @(join(X, Y, Z)).
   39%
   40join(X, Y, Z, S):- zdd_join(X, Y, Z, S).
   41
   42%
   43hyphen([],[],[]).
   44hyphen([X|Xs],[Y|Ys],[X-Y|Zs]):- hyphen(Xs, Ys, Zs).
   45%
   46mk_pair(X, Y, [X,Y]).
   47% ?- prod_pair([1,2],[a,b,c], X).
   48prod_pair(A, B, C):- product(mk_pair, A, B, C).
   49
   50
   51% ?- Oprs=[[1,1]-1,[1,2]-2,[1,3]-3,[1,4]-4,[1,5]-5,[1,6]-6,[2,1]-2,[2,2]-6,[2,3]-5,[2,4]-3,[2,5]-4,[2,6]-1,[3,1]-3,[3,2]-4,[3,3]-1,[3,4]-2,[3,5]-6,[3,6]-5,[4,1]-4,[4,2]-5,[4,3]-6,[4,4]-1,[4,5]-2,[4,6]-3,[5,1]-5,[5,2]-3,[5,3]-2,[5,4]-6,[5,5]-1,[5,6]-4,[6,1]-6,[6,2]-1,[6,3]-4,[6,4]-5,[6,5]-3,[6,6]-2],
   52%	alg_der(Oprs, Der), maplist(writeln, Der).
   53
   54% Sample for 1*(2*3) not equal to    (1*2)*3
   55% ?-   X = [[2,3]-4, [1,4]-5, [1,2]-6, [6,3]-7], alg_der(X, Y).
   56% => false
   57% ?-   X = [[2,3]-6, [1,6]-6, [1,2]-2, [2,3]-6],
   58%	alg_der(X, Y).
   59
   60merge_xalg_der([], X, X).
   61merge_xalg_der([P|Ps], X, Y):- merge_in_der(P, X, X0),
   62	merge_xalg_der(Ps, X0, Y).
   63
   64% ?- merge_in_der(a-b*c, [a-[b*c]], R).
   65% ?- merge_in_der(a-c*d, [a-[b*c]], R).
   66% ?- merge_in_der(a-c*d, [a-[c*e]], R).  % false
   67merge_in_der(X, Y, Z):- merge_in_der_(Y, X, Z).
   68%
   69merge_in_der_([], A-P, [A-[P]]).
   70merge_in_der_([A-L|R], A-P, [A-L0|R]):-!,
   71	add_ord_keyval(P, L, L0).
   72merge_in_der_([A0-L|R], A-P, [A0-L|R0]):- A0 @< A,!,
   73	merge_in_der_(R, A-P, R0).
   74merge_in_der_(R, A-P, [A-[P]|R]).
   75
   76% ?- add_ord_keyval(a*1, [], L).
   77% ?- add_ord_keyval(a*1, [a*2], L).  % false
   78% ?- add_ord_keyval(b*1, [a*1, c*3], L).
   79% ?- add_ord_keyval(d*1, [a*1, c*3], L).
   80% ?- add_ord_keyval(a*1, [b*2, c*3], L).
   81add_ord_keyval(K*V, [K*U|L], [K*V|L]):-!, U=V.
   82add_ord_keyval(P, [Q|L], [Q|L0]):- P = K*_, Q = K0*_,
   83	K0 @< K, !,
   84	add_ord_keyval(P, L, L0).
   85add_ord_keyval(P, L, [P|L]).
   86
   87% ?- check_ord_keyval(a*1, [], L).
   88% ?- check_ord_keyval(a*V, [], L).  % false
   89% ?- check_ord_keyval(a*1, [a*2], L).  % false
   90% ?- check_ord_keyval(b*1, [a*1, c*3], L).
   91% ?- check_ord_keyval(d*1, [a*1, c*3], L).
   92% ?- check_ord_keyval(a*1, [b*2, c*3], L).
   93check_ord_keyval(K*V, L, L):- var(V), !, check_ord_keyval(K*V, L).
   94check_ord_keyval(P, L, L0):- add_ord_keyval(P, L, L0).
   95
   96% ?- check_ord_keyval(b*2, [a*1, b*2, c*3]).
   97% ?- check_ord_keyval(b*3, [a*1, b*2, c*3]).  % false
   98% ?- check_ord_keyval(b*X, [a*1, b*2, c*3]).
   99% ?- check_ord_keyval(b*X, [a*1, c*3]).	% false
  100check_ord_keyval(K*V, [K*U|_]):-!, U=V.
  101check_ord_keyval(P, [K0*_|L]):- P=K*_, K0 @< K,
  102	check_ord_keyval(P, L).
  103
  104% ?- time(find_model(2, B, S)).
  105% ?- time(find_model(3, B, S)).
  106% ?- time(find_model(4, B, S)).
  107% ?- time(find_model(5, B, S)).
  108% ?- time(find_model(6, B, S)), psa(B, S).
  109% ?- time(find_model(6, B, S)), psa(B, S). % [2021/12/24]
  110%@ % 896,018,635,494 inferences, 56245.613 CPU in 110023.200 seconds (51% CPU, 15930463 Lips)
  111%@  zid = 5677
  112%@ 	[[1,1]-1,[1,2]-2,[1,3]-3,[1,4]-4,[1,5]-5,[1,6]-6,[2,1]-2,[2,2]-6,[2,3]-5,[2,4]-3,[2,5]-4,[2,6]-1,[3,1]-3,[3,2]-4,[3,3]-1,[3,4]-2,[3,5]-6,[3,6]-5,[4,1]-4,[4,2]-5,[4,3]-6,[4,4]-1,[4,5]-2,[4,6]-3,[5,1]-5,[5,2]-3,[5,3]-2,[5,4]-6,[5,5]-1,[5,6]-4,[6,1]-6,[6,2]-1,[6,3]-4,[6,4]-5,[6,5]-3,[6,6]-2]
  113%@ B = 5677,
  114%@ S = ..
  115% ?- time(find_model(7, B, S)).  % Not terminate ?
  116
  117find_model(N, B, S):-
  118	open_state(S),
  119	numlist(1, N, D),
  120	filter_left_unit(D, A, S),
  121	filter_non_commutative(2, 3, A, A0, S),
  122	filter_inversible(D, A0, A1, S),
  123	find_associative(A1, [], [], B, S).
  124%
  125find_associative(A, _, _, A, _):- A<2, !.
  126find_associative(A, Alg, Der, B, S):- cofact(A, t(Eqn, L, R), S),
  127	find_associative(L, Alg, Der, L0, S),
  128	(	L0 > 1 -> R0 = 0
  129	;	(	merge_in_der(Eqn, Alg, Der, Der0)
  130		-> 	find_associative(R, [Eqn|Alg], Der0, R0, S)
  131		;	R0 = 0
  132		)
  133	),
  134	cofact(B, t(Eqn, L0, R0), S).
  135
  136%
  137filter_associative(A, B, S):- filter_associative(A, [], [], B, S).
  138%
  139filter_associative(A, _, _, A, _):- A<2, !.
  140filter_associative(A, Oprs, Der, B, S):- cofact(A, t(Opr, L, R), S),
  141	filter_associative(L, Oprs, Der, L0, S),
  142	(	merge_in_der(Opr, Oprs, Der, Der0)
  143	-> 	filter_associative(R, [Opr|Oprs], Der0, R0, S)
  144	;	R0 = 0
  145	),
  146	cofact(B, t(Opr, L0, R0), S).
  147
  148% ?- eqn_der([1,1]-1, [], P), sort(P, P0).
  149% ?- eqn_der([1,2]-1, [[1,3]-1], P), sort(P, P0).
  150eqn_der(L, Ls, P):-	apply_eqn_one(L, [L|Ls], D, []),
  151	sort(D, P).
  152%
  153apply_eqn_one(_, [], P, P):-!.
  154apply_eqn_one(L, [M|Ms], P, Q):- basic_der(L, M, P, P0),
  155	apply_eqn_one(L, Ms, P0, Q).
  156
  157% ?- basic_der([1,1]-1,[1,1]-1, P, []).
  158% ?- basic_der([1,2]-3,[3,3]-4, P, []).
  159% ?- basic_der([1,2]-2,[2,1]-1, P, []).
  160% ?- basic_der([1,2]-3,[2,1]-4, P, []).
  161basic_der(P, Q, M, N):- der_rule(P, Q, L),
  162	collect_der(L, M, N).
  163%
  164collect_der([], V, V):-!.
  165collect_der([X=X, A|U], [A|V], V0):-!, collect_der(U, V, V0).
  166collect_der([_, _|U], V, V0):- collect_der(U, V, V0).
  167%
  168der_rule([A, B]-C, [U, V]-W,
  169	[	C = U, B-[A,V]*W,
  170		C = V, A-[U,B]*W,
  171		W = A, V-[U,B]*C,
  172		W = B, U-[A,V]*C
  173	]).
  174
  175%
  176alg_der(Alg, Der):- merge_xalg_der(Alg, [], [], Der).
  177%
  178merge_xalg_der([], _, Der, Der):-!.
  179merge_xalg_der([Eqn|Alg], Alg0, Der, Der0):-
  180	merge_in_der(Eqn, Alg0, Der, Der1),
  181	merge_xalg_der(Alg, [Eqn|Alg0], Der1, Der0).
  182%
  183merge_in_der(Eqn, Alg, Der, Der0):-
  184	eqn_der(Eqn, Alg, P),
  185	sort(P, Q),
  186	merge_xalg_der(Q, Der, Der0).
  187
  188% ?- left_identy_rule(1, [1,2,3], E).
  189left_identy_rule(_, [], []):-!.
  190left_identy_rule(E, [N|Ns], [[1, N]-N |Rest]):-
  191	left_identy_rule(E, Ns, Rest).
  192
  193% ?- N = 3, open_state(S), numlist(1, N, D), binary_algebra(D, A, S),
  194%	filter_associative(A, B, S), card(B, C, S).
  195% ?- N = 4, open_state(S), numlist(1, N, D), binary_algebra(D, A, S),
  196%	filter_associative(A, B, S), card(B, C, S).
  197%
  198binary_algebra(D, A, S):- raise_list(D, 2, D2),
  199	zdd_funs(D2, D, A, S).
  200
  201% ?- open_state(S), filter_left_unit([1], A, S), psa(A, S).
  202% ?- open_state(S), filter_left_unit([1,2,3], A, S), psa(A, S).
  203% ?- open_state(S), numlist(1, 3, D), filter_left_unit(D, A, S).
  204
  205filter_left_unit(D, A, S):- D=[E|D0],
  206	prod_pair(D0, D, D2),
  207	zdd_funs(D2, D, A0, S),
  208	left_identy_rule(E, D, U),
  209	zdd_append(U, A0, A, S).
  210
  211% ?- open_state(S), numlist(1, 4, D),
  212%	filter_left_unit(D, A, S),
  213%	filter_associative(A,[],[], B, S).
  214%
  215filter_inversible([], A, A, _):-!.
  216filter_inversible(_, A, 0, _):- A<2, !.
  217filter_inversible(D, A, B, S):-  memo(filter_inversible(D, A)-B, S),
  218	(	nonvar(B) -> true	%, write(.) % many hits.
  219	;
  220	cofact(A, t(P, L, R), S),
  221	(	P = [_, X]-1
  222	->  (	select(X, D, D0) -> true
  223		;	D0 = D
  224		)
  225	;	D0 = D
  226	),
  227	filter_inversible(D, L, L0, S),
  228	filter_inversible(D0, R, R0, S),
  229	cofact(B, t(P, L0, R0), S)
  230	).
  231%
  232filter_non_commutative(_, _, X, 0, _):- X<2, !.
  233filter_non_commutative(I, J, X, Y, S):- cofact(X, t(P, L, R), S),
  234	filter_non_commutative(I, J, L, L0, S),
  235	(	P = [I, J]-K
  236	->	filter_non_commutative(J, I, K, R, R0, S)
  237	;	filter_non_commutative(I, J, R, R0, S)
  238	),
  239	cofact(Y, t(P, L0, R0), S).
  240
  241%
  242filter_non_commutative(_, _, _, X, 0, _):- X < 2, !.
  243filter_non_commutative(I, J, K,  X, Y, S):- cofact(X, t(Q, L, R), S),
  244	filter_non_commutative(I, J, K, L, L0, S),
  245	(	Q = [I,J]-N
  246	->	(	N\==K -> R0 = R
  247		;	R0 = 0
  248		)
  249	;	filter_non_commutative(I, J, K, R, R0, S)
  250	),
  251	cofact(Y, t(Q, L0, R0), S).
  252
  253
  254		/***********************************************
  255		*     old version count_A_algebras_with_zdd    *
  256		***********************************************/
  257
  258% ?-zdd(( count_A_algebras_with_zdd(1, C))).
  259% ?-zdd(( count_A_algebras_with_zdd(2, C))).
  260% ?-time(zdd(( count_A_algebras_with_zdd(3, C)))).
  261% ?-time(zdd(( count_A_algebras_with_zdd(4, C)))).
  262% ?-call_with_time_limit(1800, zdd(( count_A_algebras_with_zdd(5, C)))).
  263%@ ERROR: Unhandled exception: Time limit exceeded
  264
  265count_A_algebras_with_zdd(N, C):-
  266	prepare_count_A_algebras(N, Track, Etree),
  267	count_A_algebras([h(Etree, [], Track)], 0, C).
  268%
  269prepare_count_A_algebras(N, Track, Etree):-
  270	numlist(1, N, Dom),
  271	raise_list(Dom, 2, Dom2),
  272	distribute_cons(Dom, Dom2, Dom3),
  273	maplist(pred([U, a(U, [], [])]), Dom3, Track),
  274	set_pred(mk_pair, equational_mapsto),
  275	zdd:zdd_funs(Dom2, Dom, Etree).
  276%	zdd:map_space(Dom2, Dom, Etree, symmetric_mapsto).
  277%
  278count_A_algebras(X, Y, Z):- @(count_A_algebras(X, Y, Z)).
  279%
  280count_A_algebras([], C, C, _).
  281count_A_algebras([h(0, _, _)|Hs], C, C0, S):-!,
  282	count_A_algebras(Hs, C, C0, S).
  283count_A_algebras([h(_, _, 0)|Hs], C, C0, S):-!,
  284	count_A_algebras(Hs, C, C0, S).
  285count_A_algebras([h(1, _, [])|Hs], C, C0, S):-!, C1 is C+1,
  286	count_A_algebras(Hs, C1, C0, S).
  287count_A_algebras([h(1, _, _)|Hs], C, C0, S):-!,
  288	count_A_algebras(Hs, C, C0, S).
  289count_A_algebras([h(Etree, Es, Tr)|Hs], C, C0, S):-
  290	cofact(Etree, t(E, L, R), S),
  291	repeat_law([E|Es], Tr, Tr0),		% for early detection.
  292	(	Tr0 = 0
  293	->	count_A_algebras([h(L, Es, Tr)|Hs], C, C0, S)
  294	;	count_A_algebras([h(L, Es, Tr), h(R, [E|Es], Tr0)|Hs], C, C0, S)
  295	).		% no difference order of h(L)  and h(R).
  296
  297% ?-zdd(( count_AC_algebras_with_zdd(1, C))).
  298% ?-zdd(( count_AC_algebras_with_zdd(2, C))).
  299% ?-zdd(( count_AC_algebras_with_zdd(3, C))).
  300% ?-time(zdd(( count_AC_algebras_with_zdd(4, C)))).
  301% ?-call_with_time_limit(100, time(zdd(( count_AC_algebras_with_zdd(5, C))))).
  302%@ % 347,069,373 inferences, 99.855 CPU in 100.001 seconds (100% CPU, 3475729 Lips)
  303%@ ERROR: Unhandled exception: Time limit exceeded
  304
  305count_AC_algebras_with_zdd(N, C):-
  306	prepare_count_AC_algebras(N, Track, Etree),
  307	count_AC_algebras([h(Etree, [], Track)], 0, C).
  308%
  309prepare_count_AC_algebras(N, Track, Etree):-
  310	numlist(1, N, Dom),
  311	raise_list(Dom, 2, Dom2),
  312	distribute_cons(Dom, Dom2, Dom3),
  313	maplist(pred([U, a(U, [], [])]), Dom3, Track),
  314	set_pred(mk_pair, equational_mapsto),
  315	bin_symm_funs(Dom2, Dom, Etree).
  316
  317equational_mapsto([A,B], C, A+B = C).
  318
  319%	zdd:map_space(Dom2, Dom, Etree, symmetric_mapsto).
  320%
  321count_AC_algebras(X, Y, Z):- @(count_AC_algebras(X, Y, Z)).
  322
  323%
  324count_AC_algebras([], C, C, _).
  325count_AC_algebras([h(0, _, _)|Hs], C, C0, S):-!,
  326	count_AC_algebras(Hs, C, C0, S).
  327count_AC_algebras([h(_, _, 0)|Hs], C, C0, S):-!,
  328	count_AC_algebras(Hs, C, C0, S).
  329count_AC_algebras([h(1, _, [])|Hs], C, C0, S):-!, C1 is C+1,
  330	count_AC_algebras(Hs, C1, C0, S).
  331count_AC_algebras([h(1, _, _)|Hs], C, C0, S):-!,
  332	count_AC_algebras(Hs, C, C0, S).
  333count_AC_algebras([h(Etree, Es, Tr)|Hs], C, C0, S):-
  334	cofact(Etree, t(E, L, R), S),
  335	symm_repeat_law([E|Es], Tr, Tr0),		% for early detection.
  336	(	Tr0 = 0
  337	->	count_AC_algebras([h(L, Es, Tr)|Hs], C, C0, S)
  338	;	count_AC_algebras([h(L, Es, Tr), h(R, [E|Es], Tr0)|Hs], C, C0, S)
  339	).		% no difference order of h(L)  and h(R).
  340
  341
  342% ?- I=3, J=2, K=1, L=1,
  343%	numlist(1, I, X), numlist(1, K, Y),
  344%	raise_list(X, J, Xj),
  345%	raise_list(Y, L, Yl),
  346%	time( ( call_with_time_limit(200, (
  347%		zdd((bin_symm_funs(Xj, Yl, F, test_equational_form),
  348%			psa(F), card(F, C))))))).
  349
  350test_equational_form([X, Y], [Z], X+Y=Z).
  351
  352%
  353bin_symm_funs(D, R, F):-
  354	bin_symm_funs(D, R, F, equational_mapsto).
  355%
  356:- meta_predicate bin_symm_funs(?,?,?,3).  357bin_symm_funs(D, R, F, Pred):- @(bin_symm_funs(D, R, F, Pred)).
  358%
  359bin_symm_funs([], _, 1, _, _).
  360bin_symm_funs([[U, V]|As], Bs, F, Pred, S):- U @> V, !,
  361	bin_symm_funs(As, Bs, F, Pred, S).
  362bin_symm_funs([A|As], Bs, F, Pred, S):-
  363	bin_symm_funs(As, Bs, F0, Pred, S),
  364	bin_symm_extend_funs_by_one(A, Bs, F0, 0, F, Pred, S).
  365%
  366bin_symm_extend_funs_by_one(_, [], _, F, F, _, _):-!.
  367bin_symm_extend_funs_by_one(A, [B|Bs], H, F0, F, Pred, S):-
  368	call(Pred, A, B, Pair),
  369	zdd_insert(Pair, H, H0, S),
  370	zdd_join(H0, F0, F1, S),
  371	bin_symm_extend_funs_by_one(A, Bs, H, F1, F, Pred, S).
  372
  373% ?- count_associative_algebra(1, X).
  374% ?- count_associative_algebra(2, X).
  375% ?- time(count_associative_algebra(3, X)).
  376% ?- time(count_associative_algebra(4, X)).
  377% ?- call_with_time_limit(180, time(count_associative_algebra(4, X))).
  378%@ % 984,263,663 inferences, 157.935 CPU in 198.803 seconds (79% CPU, 6232073 Lips)
  379%@ ERROR: Unhandled exception: Time limit exceeded
  380
  381count_associative_algebra(N, NumOfAssocAlgebras):-
  382	numlist(1, N, Dom),
  383	raise_list(Dom, 2, Dom2),
  384	distribute_cons(Dom, Dom2, Dom3),
  385	maplist(pred([U, a(U, [], [])]), Dom3, Track0),
  386	sort(Track0, Track1),
  387	all_funs(Dom2, Dom, Maps, default_mapsto),
  388	maplist(maplist( pred([[A,B]-C, A+B=C]) ), Maps, FamEs),
  389	foldl( pred(Track1, (	[Es, C, C0]	:-
  390							repeat_law(Es, Track1, Track),
  391							(		Track = [] -> C0 is C+1
  392							;		C0 = C
  393						    ))
  394					   ),
  395		   FamEs,  0,  NumOfAssocAlgebras).
  396
  397%
  398repeat_law(E, [a(_,[A],[A])|X], Y):-!, repeat_law(E, X, Y).
  399repeat_law(_, [a(_,[_],[_])|_], 0):-!.	% 0 means NON Associativitty.
  400repeat_law(Eqs, X, X0):- member(E, Eqs),
  401	apply_law_once(E, X, X1),
  402	!,
  403	repeat_law(Eqs, X1, X0).
  404repeat_law(_, X, X).
  405
  406%
  407apply_law_once(E, X, [A0|X0]):-
  408	select(A, X, X0),
  409	law(E, A, A0).
  410
  411% law/3
  412law( A+B=C,	a([X, A, B], U, []),
  413			a([X, A, B], U, [X, C])).
  414law( A+B=C,	a(T, U, [A, B]),
  415			a(T, U, [C])).
  416law( A+B=C,	a(T, [A, B], U),
  417			a(T, [C], U)).
  418law( A+B=C,	a([A, B, X], [], U),
  419			a([A, B, X], [C, X], U)).
  420
  421% ?-  symm_count_associative_algebra(1, X).
  422% ?- symm_count_associative_algebra(2, X).
  423% ?- time(symm_count_associative_algebra(3, X)).
  424% ?- call_with_time_limit(180, time(symm_count_associative_algebra(4, X))).
  425%@ % 1,290,894,487 inferences, 161.322 CPU in 180.000 seconds (90% CPU, 8001973 Lips)
  426%@ ERROR: Unhandled exception: Time limit exceeded
  427
  428symm_count_associative_algebra(N, NumOfAssocAlgebras):-
  429	numlist(1, N, Dom),
  430	raise_list(Dom, 2, Dom2),
  431	distribute_cons(Dom, Dom2, Dom3),
  432	maplist(pred([U, a(U, [], [])]), Dom3, Track0),
  433	sort(Track0, Track1),
  434	all_funs(Dom2, Dom, Maps, ordered_mapsto),
  435	sort(Maps, Maps0),
  436	maplist(maplist( pred([[A,B]-C, A+B=C]) ), Maps0, FamEs),
  437	foldl( pred(Track1, (	[Es, C, C0]	:-
  438							symm_repeat_law(Es, Track1, Track),
  439							(		Track = [] -> C0 is C+1
  440							;		C0 = C
  441						    ))
  442					   ),
  443		   FamEs,  0,  NumOfAssocAlgebras).
  444
  445%
  446symm_repeat_law(E, [a(_,[A],[A])|X], Y):-!, symm_repeat_law(E, X, Y).
  447symm_repeat_law(_, [a(_,[_],[_])|_], 0):-!.	% 0 means NON Associativitty.
  448symm_repeat_law(Eqs, X, X0):- member(E, Eqs),
  449	symm_apply_law_once(E, X, X1),
  450	!,
  451	symm_repeat_law(Eqs, X1, X0).
  452symm_repeat_law(_, X, X).
  453
  454%
  455symm_apply_law_once(E, X, [A0|X0]):-
  456	select(A, X, X0),
  457	symm_law(E, A, A0).
  458
  459symm_law( A+B=C,	a([X, A, B], U, []), a([X, A, B], U, [X, C])).
  460symm_law( A+B=C,	a([X, B, A], U, []), a([X, B, A], U, [X, C])).
  461symm_law( A+B=C,	a(T, U, [A, B]), a(T, U, [C])).
  462symm_law( A+B=C,	a(T, U, [B, A]), a(T, U, [C])).
  463symm_law( A+B=C,	a(T, [A, B], U), a(T, [C], U)).
  464symm_law( A+B=C,	a(T, [B, A], U), a(T, [C], U)).
  465symm_law( A+B=C,	a([A, B, X], [], U), a([A, B, X], [C, X], U)).
  466symm_law( A+B=C,	a([B, A, X], [], U), a([B, A, X], [C, X], U)).
  467
  468%
  469:- meta_predicate all_funs(?, ?, ?, 3).  470
  471all_funs(Xs, Y, Z):-
  472	all_funs(Xs, Y, Z, default_mapsto).
  473
  474% ?- N is 2, M is 2, time(( numlist(1, N, X), numlist(1, M, Y),
  475%	raise_list(X, 2, X2),
  476%	all_funs(X2, Y, F, ordered_mapsto), length(F, C))).
  477
  478all_funs([], _, [[]], _).
  479all_funs([X|Xs], Y, Z, M):- all_funs(Xs, Y, Z0, M),
  480	all_funs(Y, X, Z0, Z, [], M).
  481%
  482all_funs([], _, _, Z, Z, _).
  483all_funs([Y|Ys], X, Z, U, V, M):-
  484	all_funs_extend(Z, Y, X, U, U0, M),
  485	all_funs(Ys, X, Z, U0, V, M).
  486%
  487all_funs_extend([], _, _, U, U, _).
  488all_funs_extend([Z|Zs], Y, X, U, V, M):-
  489	(	call(M, X, Y, P) -> U =[[P|Z]|U0]
  490	;	U = [Z|U0]
  491	),
  492	all_funs_extend(Zs, Y, X, U0, V, M).
  493%
  494ordered_mapsto([A, B], Y, [A, B]-Y):- A@=<B, !.
  495
  496%
  497default_mapsto(X, Y, X-Y)