package logic_syntax_analysis_pak2;		 	-- second part of logic_syntax_analysis_pak  

		-- This package is a supplement to the main package 'logic_syntax_analysis_pak', 
		-- separated out only because that other file was becoming uncomfortably large. 
		-- The processes found here handle monotone and algebraic inference, and several utilities
		-- as seen in the header below. 
		-- It is also used as a repository for obsolete versions of inference and related codes.

		-- This file also includes (at its end) the package 'algebraic_parser', an auxiliary package for simple algebraic parsing,
		-- useful for communicating with external provers which use only a simple algebraic language, but possibly
		-- with operator signs and precedences different from those meeting the standard SETL syntactic conventions.
	
	var monotonicity_props := {};				-- maps an operator into its declared monotonicity properties
	var var_generator := 0;						-- used to generate VRXn_ variables
	var alg_of := {}, alg_role_of := {};		-- globals used in algebraic standardization (made visible for testing only)
	var sub_from_addn := {},reversal_from_addn := {},zero_from_addn := {},one_from_addn := {},mult_from_addn := {};
	var ring_from_addn := {};				-- globals used in algebraic standardization (visible for testing only)
	
	var mismatched_args,mismatched_symbvars,mismatched_expn;		-- substitution mismatches for diagnosis
	
--								*********** Monotonicity-based inference ***********

	procedure monotone_infer(node);				-- prepare to deduce a formula by monotone inference
												-- called from 'check_a_monot_inf' in top-level package
	procedure test_monotone_infer; 	 			-- test of the monotone_infer procedure

--								*********** Algebraic inference ***********
	
	procedure find_algebraic_nodes(tree);		-- finds the algebraic nodes in a tree, and returns them
	procedure standardize_subtree(tree,plus_op);
	procedure re_nest(flattened_tree);			-- reconvert a standardized (flattened) tree to its ordinary 'nested' form
	procedure canorder_subtree(tree);
			-- sorts the terms and factors of a standardized (flattened) subtree and performs cancellations
	procedure generate_algebraic_identity(tree);	-- generates identity of tree with standardized form
	procedure find_ring_members(tree);				-- collects the ring membership assertions at the top conjuctive level of a tree
	procedure post_alg_roles(stg);				-- adds an algebraic set to alg_of and alg_role_of maps

--					*********** Miscellaneous tree searching and transformation routines ***********

	procedure find_setformers_and_quants(tree);		-- finds the setformer and quantifier nodes in a tree, and returns them
	procedure find_fnc_symbs(node); 			-- find the function symbols in a tree 
	procedure dequantify(tree,substitution_tup); 		-- general substitution for quantified variables 
	
	procedure replace_fcn_symbol(expn,symbol,symbvars,symbdef);
		-- at each occurrence of a symbol in expn, finds the arguments of symbol,
		-- and substitutes them in symbdef for the indicated free variables of symbdef
		-- replacing the symbol occurrence by this substituted form

--								*********** Test Collection ***********

	procedure test_find_fnc_symbs; 				-- test of the find_fnc_symbs procedure
	procedure test_replace_fcn_symbol; 	 		-- test of the replace_fcn_symbol procedure
	procedure test_dequantify; 					-- test of the dequantify procedure

--								*********** Obsolete code ***********
	
	procedure monotone_inference(node1,node2); 		-- obsolete
	procedure test_monotone_inference; 	 		-- test of the monotone_inference procedure 		-- obsolete
	 			-- calculates conditions for value defined  by node 1 to include value defined by node 2

end logic_syntax_analysis_pak2;

package body logic_syntax_analysis_pak2;				-- second part of logic_syntax_analysis_pak
	use string_utility_pak,parser,sort_pak; 			--	standard Setl utilities
	use logic_parser_globals;							-- global variables for logic parser and other basic packages
	use logic_parser_aux;								-- auxiliary routines for logic basic routines
	use logic_syntax_analysis_pak;						-- use the main package of inferencing routines

	var difference_quintuples := {},monot_var_ctr := 0; -- globals used by 'monotone_inference_in'			
	var all_fnc_symbs := {}; 							-- globals used in 'find_fnc_symbs'
	var debug_flag := false;							-- debugging print switch
	
	const builtin_fcns:= {"CAR", "CDR","ast_arb","ast_if_expr","ast_if", "ast_range", "ast_domain","ast_nelt"};
			-- the definitions of these are  considered to be 'built-in'

--								****************************************************
--								*********** Monotonicity-based inference ***********
--								****************************************************

	-- This group of routines handle prof by monotonicity. Inferencing of this kind assumes that the 
	-- monotonicity properties of some of the operators and other constructions found in the  
	-- formulae which are being processed are known, at least in part. The routines seen below are prepared to handle
	-- inferences involving formulae of the form e1 incs e2, e1 •incin e2, e1 •imp e2, e1 = e2, and e1 •eq e2.
	-- Analysis of a formula of one of these forms always produces a stronger collection of simpler clauses, which 
	-- can then replace the original clause in the ELEM step used to complete the desired inference.
	-- Examples of formulae which can easily be verified by monotone inference are 

	--			#pow(Un(a + b)) incs #pow(Un(c))     and  Un(a + b) = Un(a) +  Un(b)
	
	-- and 

	-- 			{e(x): x in a | P(x)} + {e(x): x in a | Q(x)} = {e(x): x in a | Q(x) or P(x)}

	-- The first two of these evidently depend on prior knowledge of the monotonicity properties of 
	-- pow, Un, and cardinality. These are made known to the Ref system by special declarations, which invoke the 
	-- 'post_monotone' routine seen below.
	
	-- The general action of the family of routines in this 'monotonicity' set are most easily understood
	-- by considering one of them, namely monotone_infer_ast_incs, whhich handles formulae of the form e1 incs e2.
	
	-- In this case, we traverse the syntax trees of e1 and e2 downward in parallel as long as the lead operators of the nodes encountered
	-- are identical, have known monotonicity properties, and none bind any variables.
	-- When there are identical lead operators, we propagate a incs a' to corresponding arguments of increasing
	-- monotonicity,  but a' incs a  to corresponding arguments of decreasing monotonicity.
	-- For operator arguments of indeterminate monotonicity, monotone_infer_ast_eq is called. 
	-- When there are different lead operators, we demand inclusion of the expression values represented by the subtrees, 
	-- except in the following cases:

		-- (i) a incs b + c is treated as the conjunct (a incs b) & (a incs c)
		-- (ii) a * b incs c is treated as the conjunct (a incs c) & (b incs c)

	-- Consider, for example the first inclusion seen above. Assuming that the monotonicity of the operators
	-- pow, Un, and cardinality have been declared, parallel traversal of the parse trees of 
	-- #pow(Un(a + b)) and #pow(Un(c)) reduces this inclusion to a + b incs c, which is therefore the clause generated 
	-- for handling by the concluding ELEM deduction. For more examples of formulae which can be handled by monotone inference, 
	-- see the routine 'test_monotone_infer' below.

procedure monotone_infer(node);			-- deduce a formula by monotone inference
	-- this converts a node of any of the special cases that can be handled into a collection
	-- of simpler clauses to be verified by ELEM reasoning. If the clause cannot be handled,
	-- node is returned.
--print("monotone_infer: ",node);
	if not is_tuple(node) then return node; end if;
	[n1,n2,n3] := node;
--print("monotone_infer: ",n1," ",unparse(n2)," ",unparse(n3));	
	case n1 

		when "ast_eq" => return disjoin_really(disjoin_many({node,monotone_infer_ast_eq(n2,n3)})(2)); 

		when "ast_incs" => return disjoin_really(disjoin_many({node,monotone_infer_ast_incs(n2,n3)})(2)); 

		when "DOT_INCIN" => return disjoin_really(disjoin_many({node,monotone_infer_ast_incs(n3,n2)})(2)); 

		when "DOT_IMP" => return disjoin_really(disjoin_many({node,monotone_infer_ast_imp(n2,n3)})(2)); 

		when "DOT_EQ" => return disjoin_really(disjoin_many({node,monotone_infer_ast_equiv(n2,n3)})(2)); 

		otherwise => return node;

	end case;
	
end monotone_infer;

procedure monotone_infer_ast_incs(n1,n2);		-- deduce an inclusion by monotone inference
	-- We traverse the two syntax trees downward as long as the lead operators of the nodes encountered
	-- are identical, have known monotonicity properties, and none bind any variables.
	-- When there are identical lead operators, we propagate a incs a' to corresponding arguments of increasing
	-- monotonicity,  but a' incs a  to corresponding arguments of decreasing monotonicity.
	-- For operator arguments of indeterminate monotonicity, monotone_infer_ast_eq is called. 
	-- When there are different lead operators, we demand inclusion of the expression values represented by the subtrees, 
	-- except in the following cases:
		-- (i) a incs b + c is treated as the conjunct (a incs b) & (a incs c)
		-- (ii) a * b incs c is treated as the conjunct (a incs c) & (b incs c)
		-- (iii) n1 and n2 are both setformer nodes, of forms like {e(x): x in s | P(x)}. In this case we form the conjunct 
		--  ((s incs s') or monotone_infer_ast_incs(s,s')) & (FORALL x in s | e(x) = e'(x)) & (FORALL x in s' | P'(x) •imp P(x)),
		-- omitting any conjunct which is evident by blobbing.
		-- If both templates apply, the disjunction of both these sets of clauses should be formed.
--print("monotone_infer_ast_incs: ",unparse(n1)," ",unparse(n2));
		if is_string(n1) and is_string(n2) then return if n1 = n2 then "TRUE" else ["ast_incs",n1,n2] end if; end if;
		
		[blob_1,blob_2] := blob_tree(["ast_of","BOTH_",["ast_list",n1,n2]]);			-- call special 'common blobbing' function
		if blob_1 = blob_2 then return "TRUE"; end if;
					-- check for more general equality evident by blobbing
		
		if is_string(n2) then
			if n1(1) = "ast_add" then 
				return disjoin_many({["ast_incs",n1,n2],monotone_infer_ast_incs(n1(2),n2),monotone_infer_ast_incs(n1(3),n2)});
			else
				return ["ast_incs",n1,n2];
			end if;
		end if;
			
		if is_string(n1) then
			if b1 = "ast_add" then 
				return disjoin_many({["ast_incs",n1,n2],conjoin_many({monotone_infer_ast_incs(a2,n2),monotone_infer_ast_incs(a3,n2)})});
			else
				return ["ast_incs",n1,n2];
			end if;
		end if;
	
		[a1,a2,a3,a4] := n1; [b1,b2,b3,b4] := n2; 	-- otherwise decompose the two trees
		
		
		if a1 = "ast_genset_noexp" then 			-- convert to form with expression
			iter_var := a2(2)(2);
			n1 := [a1,a2,a3,a4] := ["ast_genset",iter_var,a2,a3];
		end if;
		
		if b1 = "ast_genset_noexp" then 			-- convert to form with expression
			iter_var := b2(2)(2);
			n2 := [b1,b2,b3,b4] := ["ast_genset",iter_var,b2,b3];
		end if;

		if a1 = b1 then			-- identical lead operators
		
			case a1 
			
			when "ast_if_expr" =>				-- inclusion of conditional expressions
					cond := monotone_infer_ast_equiv(a2,b2); 
					return disjoin_many({["ast_incs",n1,n2],
							if cond /= "TRUE" then conjoin_many({cond,monotone_infer_ast_incs(a3,b3),monotone_infer_ast_incs(a4,b4)})
							else monotone_infer_ast_incs(a3,b3) end if}); 
					
			when "ast_add","ast_mult" =>  			-- commutative expressions
				
					return disjoin_many({["ast_incs",n1,n2],
						conjoin_many({monotone_infer_ast_incs(a2,b2),monotone_infer_ast_incs(a3,b3)}),
									conjoin_many({monotone_infer_ast_incs(a2,b3),monotone_infer_ast_incs(a3,b2)})});
				
			when "ast_sub" =>  			-- set difference
		
					return disjoin_many({["ast_incs",n1,n2],conjoin_many({monotone_infer_ast_incs(a2,b2),monotone_infer_ast_incs(b3,a3)})});

			when "ast_pow","ast_nelt" =>  							-- SETL builtin monadics; both of these are monotone

					return disjoin_many({monotone_infer_ast_incs(a2,b2),["ast_incs",n1,n2]});	-- test arguments for equality

			when "ast_genset" =>     		-- setformer
				-- setformer pairs are treated in a special way if their sequences itseq of iterators are of the same
				-- length. 

				if #(itlist1 := a3(2..)) /= #(itlist2 := b3(2..)) then return ["ast_eq",n1,n2];	end if;
				
				conds := {};			-- condition for inclusion of variable bounds; will be collected.
				varlist_1 := varlist_2 := genvarlist := iterlimit_list := [];
				
				for [itop1,itvar1,itlimit1] = itlist1(j) loop			-- work over the two iterator lists in parallel

					[itop2,itvar2,itlimit2] := itlist2(j); 
		 				
					freevars1 := find_free_vars(itlimit1);		-- get the free variables in the iterators
					freevars2 := find_free_vars(itlimit2); 
					subst_map1 := {[v,genvarlist(j)]: v = varlist_1(j) | v in freevars1};
					subst_map2 := {[v,genvarlist(j)]: v = varlist_2(j) | v in freevars2};

					if subst_map1 /= {} then 			-- replace the indicated variables by their generated forms
						itlimit1 := substitute(itlimit1,subst_map1); 
					end if;

					if subst_map2 /= {} then 			-- replace the indicated variables by their generated forms
						itlimit2 := substitute(itlimit2,subst_map2); 
					end if;

					varlist_1 with:= itvar1;			-- extend the lists of iterator and generated variables
					varlist_2 with:=  itvar2; 
					genvarlist with:= "VRX" + (var_generator +:= 1) + "_"; 
					
					if itop1 /= itop2 then
						
						if itop1 = "DOT_INCIN" then 			-- convert to member of powerset
							itop1 := "ast_in"; itlimit1 := ["ast_pow",itlimit1];
						end if;
						
						if itop2 = "DOT_INCIN" then 			-- convert to member of powerset
							itop2 := "ast_in"; itlimit2 := ["ast_pow",itlimit2];
						end if;
				
					end if;
--print("itlimits: ",itlimit1," ",itlimit2);
					conds with:= monotone_infer_ast_incs(itlimit1,itlimit2);

					iterlimit_list with:= itlimit1;				-- collect the (first) list of iteration limits
					
				end loop;
				
							-- now demand that the substituted expressions are equal, 
							-- and the second substituted condition implies the first
				subst_map1 := {[v,genvarlist(j)]: v = varlist_1(j)};
				subst_map2 := {[v,genvarlist(j)]: v = varlist_2(j)};
				conds with:=  monotone_infer_ast_eq(substitute(a2,subst_map1),substitute(b2,subst_map2));
--print("conds::: ",{unparse(cond): cond in conds});
				
				if a4(1) = "ast_null" then a4 := ["TRUE"]; end if;
				if b4(1) = "ast_null" then b4 := ["TRUE"]; end if;
--print("a4: ",a4," ",b4);
				conds with:=  monotone_infer_ast_imp(substitute(b4,subst_map1),substitute(a4,subst_map2));
--print("conds: ",{unparse(cond): cond in conds});					
					 
				return conjoin_many(conds); 

			when "ast_of" =>  			-- function application
					
					mprops_of_args := monotonicity_props(a2); 
					
					if mprops_of_args = OM then 			-- demand equality
						if a2 /= b2 or #(a_list := a3(2..)) /= #(b_list := b3(2..)) then return ["ast_incs",n1,n2]; end if;
						return disjoin_many({monotone_infer_ast_eq(n1,n2),["ast_incs",n1,n2]});		
					end if;

						-- otherwise check the argument lists for identity in positions which are not monotone, but for inclusion in such posns.
					a_list := a3(2..); b_list := b3(2..);
					incposns := {j: arg = a_list(j) | mprops_of_args(j) > 0};
					decposns := {j: arg = a_list(j) | mprops_of_args(j) < 0};
--print("incposns,decposns: ",incposns," ",decposns);	
					
					if incposns = {} and decposns = {} then 		-- arguments must be equal
						return disjoin_many({monotone_infer_ast_eq(n1,n2),["ast_incs",n1,n2]});	
					end if;
					
							-- but if there are increasing and/or arguments, then collect inclusions and reversed inclusions
							-- for them, and identities for the others
					conditions := {if j in incposns then monotone_infer_ast_incs(argj,b_list(j))
									elseif j in decposns then monotone_infer_ast_incs(b_list(j),argj) 
									else  monotone_infer_ast_eq(argj,b_list(j)) end if: argj = a_list(j)};
					
					return disjoin_many(conditions with ["ast_incs",n1,n2]);	
				
			otherwise =>  
				
						-- otherwise check the argument lists for identity in positions which are not monotone, but for inclusion in such posns.
					return disjoin_many({["ast_incs",n1,n2],
						conjoin_many({monotone_infer_ast_eq(a2,b2),monotone_infer_ast_eq(a3,b3)})});

			end case;
			
		end if;

							-- if one of the operators is a conditional then check for evaluability
		if b1 = "ast_if_expr" then 			-- interchange and redecompose
			[n1,n2] := [n2,n1];
			[a1,a2,a3,a4] := n1; [b1,b2,b3,b4] := n2;
		end if;

		if a1 = "ast_if_expr" and  monotone_infer_ast_equiv(a2,"TRUE") = "TRUE" then 			-- use first branch
			return monotone_infer_ast_incs(a3,n2);
		end if;
							-- if one of the operators is a union then see if either of its arguments includes the other

--print("different lead ops incs: ",[n1,n2]);
		if a1 = "ast_add" then 			-- interchange and redecompose to put union operator in the second position
			[n1,n2] := [n2,n1];
			[a1,a2,a3,a4] := n1; [b1,b2,b3] := n2;
		end if;

		if b1 = "ast_add" then 			-- have a union operator in the second position
--print("ast_add case incs");					
			conditions := {["ast_incs",n1,n2],monotone_infer_ast_incs(n1,b2),monotone_infer_ast_incs(n1,b3)};
					-- two possible conditions which would force inclusion

			if a1 = "ast_of" then		-- we have a function application; see if there is a position in which the function is additive
										-- and the corresponding argument is a sum, apply additivity
				mprops_of_args := monotonicity_props(a2);
				alist := a3(2..);			-- the list of arguments
				addposns := {j: arg = alist(j) | mprops_of_args(j) = 2};
							-- at such argument positions apply additivity  
				for arg = alist(j) | j in addposns and is_tuple(arg) and arg(1) = "ast_add" loop		-- loop over all qualifying positions

					a31 := a3; a31(j + 1) := arg(2);			-- transform using additivity: build new arguments 
					a32 := a3; a32(j + 1) := arg(3);
					newf1 := [a1,a2,a31];
					newf2 := [a1,a2,a32];
	 				newsum := ["ast_add",newf1,newf2];
--print("newf1 incs: ",unparse(newsum));	 
					conditions with:= monotone_infer_ast_incs(newsum,n2);		-- try this inclusion as an alternative
				end loop; 
				
				return disjoin_many(conditions);	

			end if;

				-- setformers are treated in a special way if their sequences itseq of iterators contain 
				-- a limiting expression which is a union, or if their condition part is a disjunction.
			-- such positions are treated as 'additive arguments'
			if a1 = "ast_genset" then	

				conds := {};			-- conditions for inclusion derived from additivity; will be collected.
				varlist := genvarlist := [];
				itlist := a3(2..);

				for [itop,itvar,itlimit] = itlist(j) | itlimit(1) = "ast_add" and itop = "ast_in" loop
							-- work over the iterator list finding the 'additive' positions
	
					[-,itlimit_a,itlimit_b] := itlimit;
					ilj_a := [itop,itvar,itlimit_a]; ilj_b := [itop,itvar,itlimit_b];
					iters_a := a3; iters_a(j + 1) := ilj_a;
					iters_b := a3; iters_b(j + 1) := ilj_b;
					setf_a := [a1,a2,iters_a,a4];
					setf_b := [a1,a2,iters_b,a4];
					newsum := ["ast_add",setf_a,setf_b];
--print("ast_genset incs: ",unparse(newsum));					
					conds with:= monotone_infer_ast_incs(newsum,n2);		-- apply additivity as an alternative
					
				end loop;
				
				if is_tuple(a4) and a4(1) = "ast_or" then				-- condition part of setformer is 

					[-,cond_a,cond_b] := a4;
 					setf_a := [a1,a2,a3,cond_a];
					setf_b := [a1,a2,a3,cond_b];
					newsum := ["ast_add",setf_a,setf_b];
					
					conds with:= monotone_infer_ast_incs(newsum,n2);		-- apply additivity as an alternative

 				end if;

				return conjoin_many(conds); 

			end if;

		end if;
		
							-- if one of the operators is a union then check the other for additivity and an argument which is a union
		return ["ast_incs",n1,n2];
			
end monotone_infer_ast_incs;

procedure monotone_infer_ast_eq(n1,n2);			-- deduce an equality by monotone inference
	-- We traverse the two syntax trees downward as long as the lead operators of the nodes encountered
	-- are identical and none bind any variables. 
	-- When there are different lead operators, we demand equality of the subtrees, 
	-- except in the following cases:
		-- when there is a + operator in one node n1 but not the other n2, and the nodes have 
		-- one of the following forms: 
		-- (i) f(a1,a2..) and b + c, where the operator f must be additive in at least one of its
		-- arguments (say the first), which must have the form a11 + a12. In this case, generate the 
		-- disjunction of conjunctions ((f(a11,a2,..) = b) & (f(a12,a2,..) = c)) or vice-versa. 
		-- Note: conjuncts should be tested for 'trivial equality by blobbing', and omitted if this is the case. 
		-- (ii) n1 and n2 are both setformer nodes, of forms like {e(x): x in s | P(x)}. In this case we form the conjunct 
		--   ((s = s') or monotone_infer_ast_eq(s,s')) & (FORALL x in s | e(x) = e'(x)) & (FORALL x in s | P(x) •eq P'(x)),
		-- again omitting any conjunct which is evident by blobbing.
		-- (iii) One of the nodes, say the second, has the form b + c, and the other is a setformer of the form 
		-- (a) {e(x): x in s + t | P(x)}, or (b) {e(x): x in s | P(x) or Q(x)} (or both). In these cases we form conjuncts
		-- Case (a) (({e(x): x in s | P(x)} = b) & ({e(x): x in t | P(x)} = c)) or vice-versa
		-- Case (b) (({e(x): x in s | P(x)} = b) & ({e(x): x in s | P(x)} = Q(x))) or vice-versa
		-- If both templates apply, the disjunction of both these sets of clauses should be formed.
	
--print("\nmonotone_infer_ast_eq: ",unparse(n1),"\nn2: ",unparse(n2));		
		if is_string(n1) or is_string(n2) then return if n1 = n2 then "TRUE" else ["ast_eq",n1,n2] end if; end if; 
--print("blob_tree([both_,n1,n2]): ",blob_tree(["ast_of","BOTH_",["ast_list",n1,n2]])," ",n1," ",n2);		
		[blob_1,blob_2] := blob_tree(["ast_of","BOTH_",["ast_list",n1,n2]]);			-- call special 'common blobbing' function
		
		if blob_1 = blob_2 then return "TRUE"; end if;
					-- check for more general equality directly evident by blobbing
--print("not by blobbing");		
		[a1,a2,a3,a4] := n1; [b1,b2,b3,b4] := n2; 	-- otherwise decompose the two trees
		
		if a1 = "ast_genset_noexp" then 			-- convert to form with expression
			iter_var := a2(2)(2);
			n1 := [a1,a2,a3,a4] := ["ast_genset",iter_var,a2,a3];
		end if;
		
		if b1 = "ast_genset_noexp" then 			-- convert to form with expression
			iter_var := b2(2)(2);
			n2 := [b1,b2,b3,b4] := ["ast_genset",iter_var,b2,b3];
		end if;

		if a1 = b1 then
		
			case a1 
			
				when "ast_if_expr" =>				-- equality of conditional expressions
					cond := monotone_infer_ast_equiv(a2,b2); 
					return disjoin_many({["ast_eq",n1,n2],
							if cond /= "TRUE" then conjoin_many({cond,monotone_infer_ast_eq(a3,b3),monotone_infer_ast_eq(a4,b4)})
							else monotone_infer_ast_eq(a3,b3) end if}); 
					
			when "ast_add","ast_mult" =>  			-- commutative expressions
				
					return disjoin_many({["ast_eq",n1,n2],
						conjoin_many({monotone_infer_ast_eq(a2,b2),monotone_infer_ast_eq(a3,b3)}),
									conjoin_many({monotone_infer_ast_eq(a2,b3),monotone_infer_ast_eq(a3,b2)})});
					
			when "ast_sub" =>  			-- set difference
		
					return disjoin_many({["ast_eq",n1,n2],conjoin_many({monotone_infer_ast_eq(a2,b2),monotone_infer_ast_eq(a3,b3)})});
	
			when "ast_genset" =>     		-- two setformers to be tested for equality
				-- setformer pairs are treated in a special way if their sequences itseq of iterators are of the same
				-- length. 

				if (nil1 := #(itlist1 := a3(2..))) /= #(itlist2 := b3(2..)) then return ["ast_eq",n1,n2];	end if;
				
				conds := {};			-- condition for equality of variable bounds; will be collected.
				varlist_1 := varlist_2 := genvarlist := iterlimit_list := [];
--print("itlist1(j): ",itlist1(1));		
				first_genvar := "VRX" + (var_generator + 1) + "_";
						
				for [itop1,itvar1,itlimit1] = itlist1(j) loop			-- work over the two iterator lists in parallel

					[itop2,itvar2,itlimit2] := itlist2(j); 
		 				
					freevars1 := find_free_vars(itlimit1);		-- get the free variables in the iterators
					freevars2 := find_free_vars(itlimit2); 
					subst_map1 := {[v,genvarlist(j)]: v = varlist_1(j) | v in freevars1};
					subst_map2 := {[v,genvarlist(j)]: v = varlist_2(j) | v in freevars2};

					if subst_map1 /= {} then 			-- replace the indicated variables by their generated forms
						itlimit1 := substitute(itlimit1,subst_map1); 
					end if;

					if subst_map2 /= {} then 			-- replace the indicated variables by their generated forms
						itlimit2 := substitute(itlimit2,subst_map2); 
					end if;

					varlist_1 with:= itvar1;			-- extend the lists of iterator and generated variables
					varlist_2 with:=  itvar2; 
					genvarlist with:= "VRX" + (var_generator +:= 1) + "_"; 
					
					if itop1 /= itop2 then
						
						if itop1 = "DOT_INCIN" then 			-- convert to member of powerset
							itop1 := "ast_in"; itlimit1 := ["ast_pow",itlimit1];
						end if;
						
						if itop2 = "DOT_INCIN" then 			-- convert to member of powerset
							itop2 := "ast_in"; itlimit2 := ["ast_pow",itlimit2];
						end if;
				
					end if;

					conds with:= monotone_infer_ast_eq(itlimit1,itlimit2);

					iterlimit_list with:= itlimit1;				-- collect the (first) list of iteration limits
					
				end loop;
				
							-- now demand that the substituted expressions are equal, and the substituted conditions are equivalent
							-- on all the sets 
				subst_map1 := {[v,genvarlist(j)]: v = varlist_1(j)};
				subst_map2 := {[v,genvarlist(j)]: v = varlist_2(j)};
				
--print("conds::: ",{unparse(cond): cond in conds});
				
				if a4(1) = "ast_null" then a4 := "TRUE"; end if;
				if b4(1) = "ast_null" then b4 := "TRUE"; end if;
--print("a4: ",a4," ",b4);

				if nil1 = 1 then 			-- if there is just 1 iterator, capture the conditon that the bound variable belongs to the limit set
					conds with:= ["DOT_IMP",["ast_in",first_genvar,iterlimit_list(1)],
										monotone_infer_ast_eq(substitute(a2,subst_map1),substitute(b2,subst_map2))];
					conds with:= ["DOT_IMP",["ast_in",first_genvar,iterlimit_list(1)],
										monotone_infer_ast_equiv(substitute(a4,subst_map1),substitute(b4,subst_map2))];
 --print("just 1 iterator: ");
 				else
					conds with:= monotone_infer_ast_eq(substitute(a2,subst_map1),substitute(b2,subst_map2));
					conds with:= monotone_infer_ast_equiv(substitute(a4,subst_map1),substitute(b4,subst_map2));
				end if;
--print("conds: ",{unparse(cond): cond in conds});					
				
				-- The iteration bounds which appear in itseq are treated roughly as additive arguments  
				-- if 'In' appears, but as monotone arguments as '•incin' appears.
				-- for the lead expressions we generate 
				-- for the conditions we generate 
					 
				return conjoin_many(conds); 

			when "ast_pow","ast_nelt" =>  							-- SETL bulitin monadics
--print("builtin: ",unparse(n1)," ",unparse(n2));
					return disjoin_many({monotone_infer_ast_eq(a2,b2),["ast_eq",n1,n2]});	-- test arguments for equality

			when "ast_of" =>  			-- "DOT_EQ"
				
					if a2 /= b2 or #(a_list := a3(2..)) /= #(b_list := b3(2..)) then return ["ast_eq",n1,n2]; end if;
--print("otherwise check: ",a_list," ",b_list," ",conjoin_many({monotone_infer_ast_eq(aj,b_list(j)): aj = a_list(j)}));					
							-- otherwise check the argument lists for identity
					return disjoin_many({conjoin_many({monotone_infer_ast_eq(aj,b_list(j)): aj = a_list(j)}),["ast_eq",n1,n2]});		

				otherwise =>  
				
					return ["ast_eq",n1,n2];

			end case;
			
		end if;
							-- if one of the operators is a conditional then check for evaluability
		if b1 = "ast_if_expr" then 			-- interchange and redecompose
			[n1,n2] := [n2,n1];
			[a1,a2,a3,a4] := n1; [b1,b2,b3,b4] := n2;
		end if;
		
		if a1 = "ast_genset_noexp" then 			-- convert to form with expression
			iter_var := a2(2)(2);
			n1 := [a1,a2,a3,a4] := ["ast_genset",iter_var,a2,a3];
		end if;
		
		if b1 = "ast_genset_noexp" then 			-- convert to form with expression
			iter_var := b2(2)(2);
			n2 := [b1,b2,b3,b4] := ["ast_genset",iter_var,b2,b3];
		end if;
						 			-- see if there is an iterator over an enumerated set and if so reduce
		if a1 = "ast_genset" and is_tuple(reduced := reduce_enum_iterators(n1)) then
			return disjoin_many({["ast_eq",n1,n2],monotone_infer_ast_eq(reduced,n2)});
		end if;
		
		if b1 = "ast_genset" and is_tuple(reduced := reduce_enum_iterators(n2)) then
			return disjoin_many({["ast_eq",n1,n2],monotone_infer_ast_eq(n1,reduced)});
		end if;

		if a1 = "ast_if_expr" and  monotone_infer_ast_equiv(a2,"TRUE") = "TRUE" then 			 			-- use first branch
			return monotone_infer_ast_eq(a3,n2);
		end if;
							-- if one of the operators is a union then check the other for additivity and an argument which is a union

--print("different lead ops: ",[n1,n2]);
		if a1 = "ast_add" then 			-- interchange and redecompose to put union operator in the second position
			[n1,n2] := [n2,n1];
			[b1,b2,b3] := n2; [a1,a2,a3,a4] := n1;
		end if;

		if b1 = "ast_add" then 			-- there is a union operator in the second position
--print("ast_add case: ",[a1,a2,a3,a4]);					

			if a1 = "ast_of" then		-- we have a function application; 
										-- see if there is a position in which the function is additive,
										-- and in which a union operator appears as the top argument operator 
				mprops_of_args := monotonicity_props(a2);
				a_list := a3(2..);

				addposns := {j: arg = a_list(j) | mprops_of_args(j) = 2 and arg(1) = "ast_add"};

				conds := {["ast_eq",n1,n2]};		-- will collect additional possibilities
				
				for j in addposns loop

					[-,arg_first_summand,arg_second_summand] := a_list(j);
					a3(j + 1) := arg_first_summand;
					new_n11 := [a1,a2,a3];
					a3(j + 1) := arg_second_summand;
					new_n12 := [a1,a2,a3];
					new_n1 := ["ast_add",new_n11,new_n12];
					conds with:= monotone_infer_ast_eq(new_n1,n2);

				end loop;
		
				return disjoin_many(conds);			-- any of the deduced conditions would force equality

			end if;
	
			if a1 = "ast_genset" then		-- we have a setformer 
				-- see if the main operator in any of the iterator limits is an addition. If so, this can be treated as an 'additive argument'
				-- also, if the main operator in the condition clause is a disjunction, this can be treated as an 'additive argument'
				
				conds := {["ast_eq",n1,n2]};
				
				if is_tuple(a4) then 			-- examine the condition clause

					[cond_op,cond_1,cond_2] := a4;

					if cond_op = "ast_or" then 		-- treat as 'additive argument'

						setformer_1 := [a1,a2,a3,cond_1];
						setformer_2 := [a1,a2,a3,cond_2];
						eq1 :=  monotone_infer_ast_eq(b2,setformer_1);
						eq2 :=  monotone_infer_ast_eq(b3,setformer_2);
						conds with:= conjoin_many({eq1,eq2});
						eq1 :=  monotone_infer_ast_eq(b3,setformer_1);
						eq2 :=  monotone_infer_ast_eq(b2,setformer_2);
						conds with:= conjoin_many({eq1,eq2});

					end if;

				end if;
				
						-- now scan over the iterators, looking for all those in which the operator is 'in' and the topmost operator is '+'
						-- any of these can be treated as an 'additive argument' 
				itlist := a3(2..);			-- the list of iterators
				varlist := genvarlist := iterlimit_list := [];

				for [itop,itvar,itlimit] = itlist(j) loop			-- work over the iterator list
--print("add-iter case: ",itop," ",itlimit);					
					if itop = "ast_in" and itlimit(1) = "ast_add" then
			 				
						new_iter_1 := a3; new_iter_1(j + 1) := ["in",itvar,itlimit(2)];
						new_iter_2 := a3; new_iter_2(j + 1) := ["in",itvar,itlimit(3)]; 
						new_setf_1 := ["ast_genset",a2,new_iter_1,a4];
						new_setf_2 := ["ast_genset",a2,new_iter_2,a4];
--print("new_setf_1: ",unparse(new_setf_1)," ",unparse(b2));						 
						eq1 :=  monotone_infer_ast_eq(b2,new_setf_1);
						eq2 :=  monotone_infer_ast_eq(b3,new_setf_2);
						conds with:= conjoin_many({eq1,eq2});
						eq1 :=  monotone_infer_ast_eq(b3,new_setf_1);
						eq2 :=  monotone_infer_ast_eq(b2,new_setf_2);
						conds with:= conjoin_many({eq1,eq2});
			
					end if;

				end loop;
--print("collected conds: ",{unparse(cond): cond in conds});				
				return disjoin_many(conds);

			end if;
		
			return ["ast_eq",n1,n2];	
			
		end if;
				-- next we treat setformer and expressionless setformers,,
				-- which are converted to standard setformers {e: iter | cond}
				-- these are treated  by first finding as many lead parts of 'iter' 
				-- as are independent of the  parts of 'iter' that come before.
				-- The iteration bounds which appear in se are treated roughly as additive arguments  
				-- if 'In' appears, but as monotone arguments as '•incin' appears.
				-- for the lead expressions we generate 
				-- for the conditions we generate 

		return ["ast_eq",n1,n2];				-- temporary
		
end monotone_infer_ast_eq;

procedure disjoin_many(set_of_clauses);		-- construct a 'lazy' disjunction

	collected_disjunction_set := {} +/ {lazy_disj(2): lazy_disj in set_of_clauses | lazy_disj(1) = "disjoined"};
	collected_conjunction_set := {conjoin_really(lazy_conj(2)): lazy_conj in set_of_clauses | lazy_conj(1) = "conjoined"};
	collected_raw_set := {raw: raw in set_of_clauses | raw(1) /= "disjoined" and raw(1) /= "conjoined"}; 
	
	return ["disjoined",collected_disjunction_set + collected_conjunction_set + collected_raw_set];
	
end disjoin_many;

procedure conjoin_many(set_of_clauses);		-- construct a 'lazy' conjunction

	collected_conjunction_set := {} +/ {lazy_disj(2): lazy_disj in set_of_clauses | lazy_disj(1) = "conjoined"};
	collected_disjunction_set := {disjoin_really(lazy_conj(2)): lazy_conj in set_of_clauses | lazy_conj(1) = "disjoined"};
	collected_raw_set := {raw: raw in set_of_clauses | raw(1) /= "disjoined" and raw(1) /= "conjoined"}; 
	
	return ["conjoined",collected_disjunction_set + collected_conjunction_set + collected_raw_set];
		
end conjoin_many;

procedure disjoin_really(set_of_clauses);		-- construct a disjunction
--print("disjoin_really: ",set_of_clauses);		
		if (clause from set_of_clauses) = "TRUE" then return "TRUE"; end if;
		
		for subclause in set_of_clauses loop
			if subclause = "TRUE" then return "TRUE"; end if;
			clause := ["ast_or",clause,subclause];
		end loop;
		
		return clause;
		
end disjoin_really;

procedure conjoin_really(set_of_clauses);		-- construct a conjunction
--print("conjoin_really: ",set_of_clauses);		
		clause := [];
		for subclause in set_of_clauses | subclause /= "TRUE" loop
		
			if clause = [] then clause := subclause; continue; end if;
			clause := ["ast_and",clause,subclause];
		end loop;
		
		return if clause = [] then "TRUE" else clause end if;
		
end conjoin_really;

procedure monotone_infer_ast_equiv(n1,n2);		-- deduce an equivalence by monotone inference
	-- We traverse the two syntax trees downward as long as the lead operators of the nodes encountered
	-- are identical and none bind any variables. 
	-- When there are different lead operators, demand equality of the subtrees, 
	-- except in the following cases:
		-- when there is an or operator in one node n1 but not the other n2, and the nodes have 
		-- one of the following forms: 
		-- (iii) One of the nodes, say the second, has the form 'b or c', and the other is an existential quantifier of the form 
		-- (a) (EXISTS x in s + t | P(x)), or (b) (EXISTS x in s | P(x) or Q(x)) (or both). In thes cases we form conjuncts
		-- Case (a) (EXISTS x in s | P(x)) •eq b) & (EXISTS x in t | P(x)) •eq c)) or vice-versa
		-- Case (b) (EXISTS x in s | P(x)) •eq & (EXISTS x in s | Q(x)) •eq c)) or vice-versa
		-- If both templates apply, the disjunction of both these sets of clauses should be formed.
--print("monotone_infer_ast_equiv: ",n1,"\nn2: ",n2);		
		if is_string(n1) or is_string(n2) then return if n1 = n2 then "TRUE" else ["DOT_EQ",n1,n2] end if; end if; 

		[blob_1,blob_2] := blob_tree(["ast_of","BOTH_",["ast_list",n1,n2]]);			-- call special 'common blobbing' function
		if blob_1 = blob_2 then return "TRUE"; end if;
					-- check for more general equality directly evident by blobbing

		[a1,a2,a3,a4] := n1; [b1,b2,b3,a4] := n2; 	-- otherwise decompose the two trees
		
		if a1 = b1 then
--print("equal ops in equiv");		
			case a1 
			
				when "ast_if_expr" =>				-- equality of conditional expressions
					cond := monotone_infer_ast_equiv(a2,b2); 
					return disjoin_many({["DOT_EQ",n1,n2],
							conjoin_many({monotone_infer_ast_equiv(a2,b2),monotone_infer_ast_eq(a3,b3),monotone_infer_ast_eq(a4,b4)})}); 
					
			when "ast_or","ast_and" =>  			-- commutative expressions
				
					return disjoin_many({["DOT_EQ",n1,n2],
						conjoin_many({monotone_infer_ast_eq(a2,b2),monotone_infer_ast_eq(a3,b3)}),
									conjoin_many({monotone_infer_ast_equiv(a2,b3),monotone_infer_ast_equiv(a3,b2)})});

			when "ast_forall", "ast_exists" =>     		-- two quantifiers to be tested for equality
				-- quantifier pairs are treated in a special way if their sequences itseq of iterators are of the same
				-- length. 

				if #(itlist1 := a2(2..)) /= #(itlist2 := b2(2..)) then return ["DOT_EQ",n1,n2];	end if;
				
				conds := {};			-- condition for equality of variable bounds; will be collected.
				varlist_1 := varlist_2 := genvarlist := iterlimit_list := [];
			
				for [itop1,itvar1,itlimit1] = itlist1(j) loop			-- work over the two iterator lists in parallel

					[itop2,itvar2,itlimit2] := itlist2(j); 
		 				
					freevars1 := find_free_vars(itlimit1);		-- get the free variables in the iterators
					freevars2 := find_free_vars(itlimit2); 
					subst_map1 := {[v,genvarlist(j)]: v = varlist_1(j) | v in freevars1};
					subst_map2 := {[v,genvarlist(j)]: v = varlist_2(j) | v in freevars2};

					if subst_map1 /= {} then 			-- replace the indicated variables by their generated forms
						itlimit1 := substitute(itlimit1,subst_map1); 
					end if;

					if subst_map2 /= {} then 			-- replace the indicated variables by their generated forms
						itlimit2 := substitute(itlimit2,subst_map2); 
					end if;

					varlist_1 with:= itvar1;			-- extend the lists of iterator and generated variables
					varlist_2 with:=  itvar2; 
					genvarlist with:= "VRX" + (var_generator +:= 1) + "_"; 
					
					if itop1 /= itop2 then
						
						if itop1 = "DOT_INCIN" then 			-- convert to member of powerset
							itop1 := "ast_in"; itlimit1 := ["ast_pow",itlimit1];
						end if;
						
						if itop2 = "DOT_INCIN" then 			-- convert to member of powerset
							itop2 := "ast_in"; itlimit2 := ["ast_pow",itlimit2];
						end if;
				
					end if;

					conds with:= monotone_infer_ast_eq(itlimit1,itlimit2);

					iterlimit_list with:= itlimit1;				-- collect the (first) list of iteration limits
					
				end loop;
				
							-- now demand that the substituted conditions are equivalent
				conds with:=  monotone_infer_ast_equiv(substitute(a3,subst_map1),substitute(b3,subst_map2));
--print("conds: ",{unparse(cond): cond in conds});					
					 
				return conjoin_many(conds); 

			when "ast_not" =>  							-- SETL bulitin monadic

					return disjoin_many({monotone_infer_ast_equiv(a2,b2),["DOT_EQ",n1,n2]});	-- test arguments for equality

			when "ast_of" =>  			-- function application
				
					if a2 /= b2 or #(a_list := a3(2..)) /= #(b_list := b3(2..)) then return ["DOT_EQ",n1,n2]; end if;
--print("otherwise check: ",a_list," ",b_list," ",conjoin_many({monotone_infer_ast_eq(aj,b_list(j)): aj = a_list(j)}));					
							-- otherwise check the argument lists for identity
					return disjoin_many({conjoin_many({monotone_infer_ast_eq(aj,b_list(j)): aj = a_list(j)}),["DOT_EQ",n1,n2]});		

				otherwise =>  
				
					return disjoin_many({["DOT_EQ",n1,n2],
						conjoin_many({monotone_infer_ast_equiv(a2,b2),monotone_infer_ast_equiv(a3,b3)})});

			end case;
			
		end if;
							-- if one of the operators is a conditional then check for evaluability

		if a1 = "ast_if_expr" and  monotone_infer_ast_equiv(a2,"TRUE") = "TRUE" then 			 			-- use first branch
			return monotone_infer_ast_eq(a3,n2);
		end if;
							-- if one of the operators is a disjunction then check the other for additivity and an argument which is a union

--print("different lead ops in equiv: ",[n1,n2]);
		if a1 = "ast_or" or a1 = "ast_and" then 			-- interchange and redecompose to put con/disjunction operator in the second position
			[n1,n2] := [n2,n1];
			[b1,b2,b3] := n2; [a1,a2,a3] := n1;
		end if;

		if b1 = "ast_or" then 			-- there is a union operator in the second position
	
			if a1 = "ast_exists" then		-- we have an existential 
--print("ast_or_exists case in equiv: ",[a1,a2,a3]);					
				-- see if the main operator in any of the iterator limits is an addition. If so, this can be treated as an 'additive argument'
				-- also, if the main operator in the condition clause is a disjunction, this can be treated as an 'additive argument'
				
				conds := {["DOT_EQ",n1,n2]};
				
				if is_tuple(a3) then 			-- examine the condition clause

					[cond_op,cond_1,cond_2] := a3;

					if cond_op = "ast_or" then 		-- treat as 'additive argument'
--print("additive in equiv: ",[a1,a2,a3]);
						exis_1 := [a1,a2,cond_1];
						exis_2 := [a1,a2,cond_2];
						eq1 :=  monotone_infer_ast_equiv(b2,exis_1);
						eq2 :=  monotone_infer_ast_equiv(b3,exis_2);
						conds with:= conjoin_many({eq1,eq2});
						eq1 :=  monotone_infer_ast_equiv(b3,exis_1);
						eq2 :=  monotone_infer_ast_equiv(b2,exis_2);
						conds with:= conjoin_many({eq1,eq2});

					end if;

				end if;
				
						-- now scan over the iterators, looking for all those in which the operator is 'in' and the topmost operator is '+'
						-- any of these can be treated as an 'additive argument' 
				itlist := a2(2..);			-- the list of iterators
				varlist := genvarlist := iterlimit_list := [];

				for [itop,itvar,itlimit] = itlist(j) loop			-- work over two iterator list
--print("add-iter case in equiv: ",itop," ",itlimit);					
					if itop = "ast_in" and itlimit(1) = "ast_add" then
			 				
						new_iter_1 := a2; new_iter_1(j + 1) := ["in",itvar,itlimit(2)];
						new_iter_2 := a2; new_iter_2(j + 1) := ["in",itvar,itlimit(3)]; 
						new_exi_1 := ["ast_exists",new_iter_1,a3];
						new_exi_2 := ["ast_exists",new_iter_2,a3];
						 
						eq1 :=  monotone_infer_ast_equiv(b2,new_exi_1);
						eq2 :=  monotone_infer_ast_equiv(b3,new_exi_2);
						conds with:= conjoin_many({eq1,eq2});
						eq1 :=  monotone_infer_ast_equiv(b3,new_exi_1);
						eq2 :=  monotone_infer_ast_equiv(b2,new_exi_2);
						conds with:= conjoin_many({eq1,eq2});
			
					end if;

				end loop;
--print("collected conds: ",{unparse(cond): cond in conds});				
				return disjoin_many(conds);

			end if;

		end if;

		if b1 = "ast_and" then 			-- there is a conjunction operator in the second position
	
			if a1 = "ast_forall" then		-- we have a universal 
--print("ast_or_exists case in equiv: ",[a1,a2,a3]);					
				-- see if the main operator in any of the iterator limits is an addition. If so, this can be treated as an 'additive argument'
				-- also, if the main operator in the condition clause is a disjunction, this can be treated as an 'additive argument'
				
				conds := {["DOT_EQ",n1,n2]};
				
				if is_tuple(a3) then 			-- examine the condition clause

					[cond_op,cond_1,cond_2] := a3;

					if cond_op = "ast_and" then 		-- treat as 'conjunctive argument'
--print("conjunctive in equiv: ",[a1,a2,a3]);
						univ_1 := [a1,a2,cond_1];
						univ_2 := [a1,a2,cond_2];
						eq1 :=  monotone_infer_ast_equiv(b2,univ_1);
						eq2 :=  monotone_infer_ast_equiv(b3,univ_2);
						conds with:= conjoin_many({eq1,eq2});
						eq1 :=  monotone_infer_ast_equiv(b3,univ_1);
						eq2 :=  monotone_infer_ast_equiv(b2,univ_2);
						conds with:= conjoin_many({eq1,eq2});

					end if;

				end if;
				
						-- now scan over the iterators, looking for all those in which the operator is 'in' and the topmost operator is '+'
						-- any of these can be treated as an 'additive argument' 
				itlist := a2(2..);			-- the list of iterators
				varlist := genvarlist := iterlimit_list := [];

				for [itop,itvar,itlimit] = itlist(j) loop			-- work over two iterator list
--print("add-iter case in equiv: ",itop," ",itlimit);					
					if itop = "ast_in" and itlimit(1) = "ast_add" then
			 				
						new_iter_1 := a2; new_iter_1(j + 1) := ["in",itvar,itlimit(2)];
						new_iter_2 := a2; new_iter_2(j + 1) := ["in",itvar,itlimit(3)]; 
						new_exi_1 := ["ast_forall",new_iter_1,a3];
						new_exi_2 := ["ast_forall",new_iter_2,a3];
						 
						eq1 :=  monotone_infer_ast_equiv(b2,new_exi_1);
						eq2 :=  monotone_infer_ast_equiv(b3,new_exi_2);
						conds with:= conjoin_many({eq1,eq2});
						eq1 :=  monotone_infer_ast_equiv(b3,new_exi_1);
						eq2 :=  monotone_infer_ast_equiv(b2,new_exi_2);
						conds with:= conjoin_many({eq1,eq2});
			
					end if;

				end loop;
--print("collected conds: ",{unparse(cond): cond in conds});				
				return disjoin_many(conds);

			end if;
		
		
			return ["DOT_EQ",n1,n2];	-- if nothing special can be done
			
		end if;

		return ["DOT_EQ",n1,n2];		
	
end monotone_infer_ast_equiv;

procedure reduce_enum_iterators(node);		
		-- look for iterators over enumerated sets in a setformer or quantifier, 
		-- and if found then replace by assignments of variable
		-- if not found then return OM
	return OM;			-- *********** REMOVE
	
	if node(1) = "ast_genset" then 
		[a1,a0,a2,a3] := node;
	else				-- must be quantifier
		[a1,a2,a3] := node;
	end if;

	iter_list := a2(2..);
	if not(exists iter in iter_list | iter(1) = "ast_in" and (itlim := iter(3))(1) = "ast_enum_set") then return OM; end if;
	
	case a1
	
		when "ast_genset" => print("reduce_enum_iterators: ",iter_list);		-- reduce to union
	
		when "ast_exists" => print("reduce_enum_iterators: ",iter_list);			-- reduce to disjunction
	
		when "ast_forall" => print("reduce_enum_iterators: ",iter_list);			-- reduce to conjunction
		
	end case;
	
end reduce_enum_iterators;

procedure monotone_infer_ast_imp(n1,n2);		-- deduce an implication by monotone inference
	-- We traverse the two syntax trees downward as long as the lead operators of the nodes encountered
	-- are identical and none bind any variables.
	-- When there are different lead operators, we forego processing, except a few two quantifier-related cases: 
	-- except in the following cases:
		-- (i) (FORALL x in s * t | ..) •imp (b & c) might be the conjunct (FORALL x in s | ..) •imp b) & (FORALL x in t | ..) •imp t)
		-- (ii) (FORALL x in s | P & Q) •imp (b & c) might be the conjunct (FORALL x in s | P) •imp b) & (FORALL x in s | Q) •imp t)
		-- (iii) (b or c) •imp (EXISTS x in s + t | ..) might be the disjunct (b •imp (EXISTS x in s | ..)) or (c  •imp (EXISTS x in t | ..))
		-- (iv) (b or c) •imp (EXISTS x in s | P or Q) might be the disjunct (b •imp (EXISTS x in s | P)) or (c  •imp (EXISTS x in s | Q))
		-- If both templates apply, the disjunction of both these sets of clauses should be formed.

--print("monotone_infer_ast_imp: ",unparse(n1)," ",unparse(n2));
		if is_string(n1) and is_string(n2) then return if n1 = n2 then "TRUE" else ["DOT_IMP",n1,n2] end if; end if;
		
		[blob_1,blob_2] := blob_tree(["ast_of","BOTH_",["ast_list",n1,n2]]);			-- call special 'common blobbing' function

		if blob_1 = blob_2 then return "TRUE"; end if;
					-- check for more general equality evident by blobbing
		
		if  n2 = "TRUE" then return "TRUE"; end if;		-- this case will be common since generated by other monot-inference routines
		
		[a1,a2,a3,a4] := n1; 
		
		if is_string(n2) then
			if a1 = "ast_or" then 
				return disjoin_many({["DOT_IMP",n1,n2],conjoin_many({monotone_infer_ast_imp(a2,n2),monotone_infer_ast_imp(a3,n2)})});
			elseif a1 = "ast_and" then 
				return disjoin_many({["DOT_IMP",n1,n2],monotone_infer_ast_imp(a2,n2),monotone_infer_ast_imp(a3,n2)});
			elseif a1 = "ast_if_expr" and monotone_infer(a2) = "TRUE" then 
				return disjoin_many({["DOT_IMP",n1,n2],monotone_infer_ast_imp(a3,n2)});
			else
				return ["DOT_IMP",n1,n2];
			end if;
		end if;
		
		[b1,b2,b3,b4] := n2; 	-- otherwise decompose the two trees
		
		if a1 = b1 then			-- identical lead operators
		
			case a1 
--print("monotone_infer_ast_imp same: ",unparse(n1)," ",unparse(n2));
			
			when "ast_if_expr" =>				-- implication of conditional expressions
					cond := monotone_infer_ast_equiv(a2,b2); 
					return disjoin_many({["DOT_IMP",n1,n2],
							if cond /= "TRUE" then conjoin_many({cond,monotone_infer_ast_imp(a3,b3),monotone_infer_ast_imp(b4,a4)})
							else monotone_infer_ast_imp(a3,b3) end if}); 
					
			when "ast_or","ast_and" =>  			-- commutative expressions
				
					return disjoin_many({["ast_incs",n1,n2],
						conjoin_many({monotone_infer_ast_imp(a2,b2),monotone_infer_ast_imp(a3,b3)}),
									conjoin_many({monotone_infer_ast_imp(a2,b3),monotone_infer_ast_imp(a3,b2)})});
					
			when "ast_not" =>  			-- two inverse implications
				
				return monotone_infer_ast_imp(b2,a2);

			when "ast_forall" =>     		-- universals
				-- pairs of universals are treated in a special way if their sequences itseq of iterators are of the same length. 

				if #(itlist1 := a2(2..)) /= #(itlist2 := b2(2..)) then return ["DOT_IMP",n1,n2];	end if;
				
				conds := {};			-- condition for inclusion of variable bounds; will be collected.
				varlist_1 := varlist_2 := genvarlist := iterlimit_list := [];
--print("universals: ",itlist1," ",itlist2);				
				for [itop1,itvar1,itlimit1] = itlist1(j) loop			-- work over the two iterator lists in parallel

					[itop2,itvar2,itlimit2] := itlist2(j); 
		 				
					freevars1 := find_free_vars(itlimit1);		-- get the free variables in the iterators
					freevars2 := find_free_vars(itlimit2); 
					subst_map1 := {[v,genvarlist(j)]: v = varlist_1(j) | v in freevars1};
					subst_map2 := {[v,genvarlist(j)]: v = varlist_2(j) | v in freevars2};

					if subst_map1 /= {} then 			-- replace the indicated variables by their generated forms
						itlimit1 := substitute(itlimit1,subst_map1); 
					end if;

					if subst_map2 /= {} then 			-- replace the indicated variables by their generated forms
						itlimit2 := substitute(itlimit2,subst_map2); 
					end if;

					varlist_1 with:= itvar1;			-- extend the lists of iterator and generated variables
					varlist_2 with:=  itvar2; 
					genvarlist with:= "VRX" + (var_generator +:= 1) + "_"; 
					
					if itop1 /= itop2 then			-- convert inclusion to powerset membership
						
						if itop1 = "DOT_INCIN" then 			-- convert to member of powerset
							itop1 := "ast_in"; itlimit1 := ["ast_pow",itlimit1];
						end if;
						
						if itop2 = "DOT_INCIN" then 			-- convert to member of powerset
							itop2 := "ast_in"; itlimit2 := ["ast_pow",itlimit2];
						end if;
				
					end if;

					conds with:= monotone_infer_ast_incs(itlimit1,itlimit2);		-- hypothesis must 

					iterlimit_list with:= itlimit1;				-- collect the (first) list of iteration limits
					
				end loop;

	 				
				freevars1 := find_free_vars(a3);		-- get the free variables in the iterators
				freevars2 := find_free_vars(b3); 
				subst_map1 := {[v,genvarlist(j)]: v = varlist_1(j) | v in freevars1};
				subst_map2 := {[v,genvarlist(j)]: v = varlist_2(j) | v in freevars2};

				if subst_map1 /= {} then 			-- replace the indicated variables by their generated forms
					a3 := substitute(a3,subst_map1); 
				end if;

				if subst_map2 /= {} then 			-- replace the indicated variables by their generated forms
					b3 := substitute(b3,subst_map2); 
				end if;

				conds with:=  monotone_infer_ast_imp(substitute(a3,subst_map1),substitute(b3,subst_map2));
							-- demand that the condition in the first existential imply that in the second
						 
				return disjoin_many({conjoin_many(conds),["DOT_IMP",n1,n2]}); 

			when "ast_exists" =>     		-- existentials
				-- pairs of existentials are treated in a special way if their sequences itseq of iterators are of the same length. 

				if #(itlist1 := a2(2..)) /= #(itlist2 := b2(2..)) then return ["DOT_IMP",n1,n2];	end if;
				
				conds := {};			-- condition for inclusion of variable bounds; will be collected.
				varlist_1 := varlist_2 := genvarlist := iterlimit_list := [];
--print("existentials: ",itlist1," ",itlist2);				
				for [itop1,itvar1,itlimit1] = itlist1(j) loop			-- work over the two iterator lists in parallel

					[itop2,itvar2,itlimit2] := itlist2(j); 
		 				
					freevars1 := find_free_vars(itlimit1);		-- get the free variables in the iterators
					freevars2 := find_free_vars(itlimit2); 
					subst_map1 := {[v,genvarlist(j)]: v = varlist_1(j) | v in freevars1};
					subst_map2 := {[v,genvarlist(j)]: v = varlist_2(j) | v in freevars2};

					if subst_map1 /= {} then 			-- replace the indicated variables by their generated forms
						itlimit1 := substitute(itlimit1,subst_map1); 
					end if;

					if subst_map2 /= {} then 			-- replace the indicated variables by their generated forms
						itlimit2 := substitute(itlimit2,subst_map2); 
					end if;

					varlist_1 with:= itvar1;			-- extend the lists of iterator and generated variables
					varlist_2 with:=  itvar2; 
					genvarlist with:= "VRX" + (var_generator +:= 1) + "_"; 
					
					if itop1 /= itop2 then			-- convert inclusion to powerset membership
						
						if itop1 = "DOT_INCIN" then 			-- convert to member of powerset
							itop1 := "ast_in"; itlimit1 := ["ast_pow",itlimit1];
						end if;
						
						if itop2 = "DOT_INCIN" then 			-- convert to member of powerset
							itop2 := "ast_in"; itlimit2 := ["ast_pow",itlimit2];
						end if;
				
					end if;

					conds with:= monotone_infer_ast_incs(itlimit2,itlimit1);
								-- demand that limit from second existential include that from first 

					iterlimit_list with:= itlimit1;				-- collect the (first) list of iteration limits
					
				end loop;
	 				
				freevars1 := find_free_vars(a3);		-- get the free variables in the iterators
				freevars2 := find_free_vars(b3); 
				subst_map1 := {[v,genvarlist(j)]: v = varlist_1(j) | v in freevars1};
				subst_map2 := {[v,genvarlist(j)]: v = varlist_2(j) | v in freevars2};

				if subst_map1 /= {} then 			-- replace the indicated variables by their generated forms
					a3 := substitute(a3,subst_map1); 
				end if;

				if subst_map2 /= {} then 			-- replace the indicated variables by their generated forms
					b3 := substitute(b3,subst_map2); 
				end if;

				conds with:=  monotone_infer_ast_imp(substitute(a3,subst_map1),substitute(b3,subst_map2));
							-- demand that the condition in the first existential imply that in the second
--print("conds: ",{unparse(cond): cond in conds});					
					 
				return disjoin_many({conjoin_many(conds),["DOT_IMP",n1,n2]}); 

			when "ast_of" =>  			-- function application; equality is an alternative
					
					mprops_of_args := monotonicity_props(a2); 
					
					if mprops_of_args = OM then 			-- demand equality
						if a2 /= b2 or #(a_list := a3(2..)) /= #(b_list := b3(2..)) then return ["ast_incs",n1,n2]; end if;
						return disjoin_many({monotone_infer_ast_eq(n1,n2),["ast_incs",n1,n2]});		
					end if;

						-- otherwise check the argument lists for identity in positions which are not monotone, but for inclusion in such posns.
					a_list := a3(2..); b_list := b3(2..);
					incposns := {j: arg = a_list(j) | mprops_of_args(j) > 0};
					decposns := {j: arg = a_list(j) | mprops_of_args(j) < 0};
					
					if incposns = {} and decposns = {} then 		-- arguments must be equal
						return disjoin_many({monotone_infer_ast_eq(n1,n2),["ast_incs",n1,n2]});	
					end if;
--print("ast_of_imp: ",mprops_of_args," ",decposns);					
							-- but if there are increasing and/or arguments. then collect inclusions and reversed inclusions
							-- for them, and identities for the others
					conditions := {if j in incposns then monotone_infer_ast_incs(b_list(j),argj)
									elseif j in decposns then monotone_infer_ast_incs(argj,b_list(j)) 
									else  monotone_infer_ast_eq(argj,b_list(j)) end if: argj = a_list(j)};
					
					return disjoin_many(conditions with ["ast_imp",n1,n2]);	
					
			otherwise =>  	-- otherwise nothing to do

					return ["DOT_IMP",n1,n2];

			end case;
			
		end if;
--print("different ops imp: ",n1," ",n2);
							-- if one of the operators is a conditional then check for evaluability
		if b1 = "ast_if_expr" then 			-- interchange and redecompose
			[n1,n2] := [n2,n1];
			[a1,a2,a3,a4] := n1; [b1,b2,b3,b4] := n2;
		end if;

		if a1 = "ast_if_expr" and  monotone_infer_ast_equiv(a2,"TRUE") = "TRUE" then 			-- use first branch
print("ast_if_expr imp");
			return monotone_infer_ast_imp(a3,n2);
		end if;

		if b1 = "ast_or" then 			-- have a disjunction operator in the second position
					
			conds := {["DOT_IMP",n1,n2],monotone_infer_ast_imp(n1,b2),monotone_infer_ast_imp(n1,b3)};
					-- two possible conditions which would force implication
			
				-- existentials are treated in a special way if their sequences itseq of iterators contain 
				-- a limiting expression which is a union, or if their condition part is a disjunction.
				-- such positions are treated as 'additive arguments'
			if a1 = "ast_exists" then	-- transform using additivity and make recursive call to case of equal operators
					
				itlist := a2(2..);			-- get list of iterators
				
				for [itop,itvar,itlimit] = itlist(j) | itop = "ast_in" and itlimit(1) = "ast_add" loop

					a21 := a2; a21(j + 1) := [itop,itvar,itlimit(2)];			-- transform using additivity: build new arguments 
					a22 := a2; a22(j + 1) := [itop,itvar,itlimit(3)];
					newq1 := [a1,a21,a3];
					newq2 := [a1,a22,a3];
	 				newdis := ["ast_or",newq1,newq2];

					conds with:= monotone_infer_ast_imp(newdis,n2);		-- apply additivity as an alternative

					end loop;

					if a3(1) = "ast_or" then			-- the first condition is a disjunction
						newq1 := [a1,a2,a3(2)];
						newq2 := [a1,a2,a3(3)];
	 					newdis := ["ast_or",newq1,newq2];
						conds with:= monotone_infer_ast_imp(newdis,n2);		-- apply additivity as an alternative
					end if;
			
			end if;

			return disjoin_many(conds); 			-- any of the accumulated conditions would force implication

		end if;

		if a1 = "ast_or" then 			-- have a disjunction operator in the first position
					
			conds := {["DOT_IMP",n1,n2],conjoin_many({monotone_infer_ast_imp(a2,n2),monotone_infer_ast_imp(a3,n2)})};
					-- two conditions which would force implication
			
				-- existentials are treated in a special way if their sequences itseq of iterators contain 
				-- a limiting expression which is a union, or if their condition part is a disjunction.
				-- such positions are treated as 'additive arguments'
			if b1 = "ast_exists" then	-- transform using additivity and make recursive call to case of equal operators
					
				itlist := b2(2..);			-- get list of iterators
				
				for [itop,itvar,itlimit] = itlist(j) | itop = "ast_in" and itlimit(1) = "ast_add" loop

					b21 := b2; b21(j + 1) := [itop,itvar,itlimit(2)];			-- transform using additivity: build new arguments 
					b22 := b2; b22(j + 1) := [itop,itvar,itlimit(3)];
					newq1 := [b1,b21,b3];
					newq2 := [b1,b22,b3];
	 				newdis := ["ast_or",newq1,newq2];

					conds with:= monotone_infer_ast_imp(n1,newdis);		-- apply additivity as an alternative

				end loop;

				if b3(1) = "ast_or" then			-- the first condition is a disjunction
					newq1 := [b1,b2,b3(2)];
					newq2 := [b1,b2,b3(3)];
	 				newdis := ["ast_or",newq1,newq2];
					conds with:= monotone_infer_ast_imp(n1,newdis);		-- apply additivity as an alternative
				end if;
			
			end if;

			return disjoin_many(conds); 			-- any of the accumulated conditions would force implication

		end if;

		if b1 = "ast_and" then 			-- have a disjunction operator in the second position
					
			conds := {["DOT_IMP",n1,n2],conjoin_many({monotone_infer_ast_imp(n1,b2),monotone_infer_ast_imp(n1,b3)})};
					-- two possible conditions whose conjunction would force implication
			
				-- universals are treated in a special way if their sequences itseq of iterators contain 
				-- a limiting expression which is a union, or if their condition part is a conjunction.
				-- such positions are treated as 'additive arguments'
			if a1 = "ast_forall" then	-- transform using additivity and make recursive call to case of equal operators
					
				itlist := a2(2..);			-- get list of iterators
				
				for [itop,itvar,itlimit] = itlist(j) | itop = "ast_in" and itlimit(1) = "ast_add" loop

					a21 := a2; a21(j + 1) := [itop,itvar,itlimit(2)];			-- transform using additivity: build new arguments 
					a22 := a2; a22(j + 1) := [itop,itvar,itlimit(3)];
					newq1 := [a1,a21,a3];
					newq2 := [a1,a22,a3];
	 				newdis := ["ast_and",newq1,newq2];

					conds with:= monotone_infer_ast_imp(newdis,n2);		-- apply additivity as an alternative

					end loop;

					if a3(1) = "ast_and" then			-- the first condition is a disjunction
						newq1 := [a1,a2,a3(2)];
						newq2 := [a1,a2,a3(3)];
	 					newcon := ["ast_and",newq1,newq2];
						conds with:= monotone_infer_ast_imp(newcon,n2);		-- apply conjunction as an alternative
					end if;
			
			end if;

			return disjoin_many(conds); 			-- any of the accumulated conditions would force implication

		end if;

		if a1 = "ast_and" then 			-- have a conjunction operator in the first position
					
			conds := {["DOT_IMP",n1,n2],monotone_infer_ast_imp(a2,n2),monotone_infer_ast_imp(a3,n2)};
					-- two conditions either of which would force implication
			
				-- universals are treated in a special way if their sequences itseq of iterators contain 
				-- a limiting expression which is a union, or if their condition part is a conjunction.
				-- such positions are treated as 'additive arguments'
			if b1 = "ast_forall" then	-- transform using additivity and make recursive call to case of equal operators
					
				itlist := b2(2..);			-- get list of iterators
				
				for [itop,itvar,itlimit] = itlist(j) | itop = "ast_in" and itlimit(1) = "ast_add" loop

					b21 := b2; b21(j + 1) := [itop,itvar,itlimit(2)];			-- transform using additivity: build new arguments 
					b22 := b2; b22(j + 1) := [itop,itvar,itlimit(3)];
					newq1 := [b1,b21,b3];
					newq2 := [b1,b22,b3];
	 				newcon := ["ast_and",newq1,newq2];

					conds with:= monotone_infer_ast_imp(n1,newcon);		-- apply additivity as an alternative

				end loop;

				if b3(1) = "ast_and" then			-- the first condition is a disjunction
					newq1 := [b1,b2,b3(2)];
					newq2 := [b1,b2,b3(3)];
	 				newcon := ["ast_and",newq1,newq2];
					conds with:= monotone_infer_ast_imp(n1,newcon);		-- apply conjunction as an alternative
				end if;
			
			end if;

			return disjoin_many(conds); 			-- any of the accumulated conditions would force implication

		end if;
		
		return ["DOT_IMP",n1,n2];
		
end monotone_infer_ast_imp;

	procedure post_monotone(op_and_arg_string); 	-- note the monotonicity property of one or more function symbols
		-- this adds information concerning the monotonicity properties of an operator to the map 'monotonicity_props'
		-- for use by 'blob_to_monotone'. The parameter is a string of the form op_name,dep_1,...,dep_n, 
		-- where each dep is either '+' (increasing), '++' (additive), '-' (decreasing), '0' (mixed)
		-- these are stored in the map as 1,2,-1,0 respectively. Multiple semicolon-separated declarations of this kind can be supplied
		
		op_and_arg_tups := breakup(breakup(op_and_arg_string,";"),",");

		for op_and_arg_tup in op_and_arg_tups loop
			op := case_change(op_and_arg_tup(1),"lu"); 
			arg_qual := [if x = "+" then 1 elseif x = "++" then 2 elseif x = "--" then -2 elseif x = "-" then -1 else 0 end if: x in op_and_arg_tup(2..)];
			monotonicity_props(op) := arg_qual;
		end loop;

print("monotonicity_props: ",monotonicity_props);
		
	end post_monotone;

--								****************************************************
--								*************** Algebraic inference ****************
--								****************************************************

procedure find_algebraic_nodes(tree);	-- finds the algebraic nodes in a tree, and returns them
										-- as a map from the '+' operator defining an algebraic operator set

	var algebraic_nodes := {};	-- the value of this global is a map; see comment above.
				
		-- an algebraic node is one which is tagged by an algebraic operator belonging to some 
		-- algebraic operator set, but whose parent is either not algebraic or does not belong to
		-- the same algebraic operator set. 
		
	find_algebraic_nodes_in(tree,OM);		-- call the recursive workhorse
	
	return algebraic_nodes;					-- return the map produced

	procedure find_algebraic_nodes_in(tree,plus_op_of_parent);	-- internal recursive workhorse
--print("find_algebraic_nodes_in: ",plus_op_of_parent," ",unicode_unparse(tree));		
		if is_string(tree) then return; end if;		-- since this is not an algebraic expression
		
		if abbreviated_headers(tree(1)) in {"{}","{/}","EX","ALL"} then return; end if;
			-- we do not search below levels at which bound variables appear
		
		op := if (n1 := tree(1)) = "ast_of" then tree(2) else n1 end if; -- get the operator (infix, prefix, or fcn)
		args := if n1 = "ast_of" then tree(3)(2..) else tree(2..) end if;		-- get its arguments

		if (ao := alg_of(op)) /= OM and ao /= plus_op_of_parent then
					-- this is an algebraic node, so associate it with its plus_op
			algebraic_nodes(ao) := (algebraic_nodes(ao)?{}) with tree;
		end if;
					-- in any case, continue search down the tree, passing the algebraic type of the new parent
		for arg in args loop find_algebraic_nodes_in(arg,ao); end loop;
		
	end find_algebraic_nodes_in;
			
end find_algebraic_nodes;

-- Once having found all algebraic nodes in a tree we standardize them, and for each generate an
-- equality which states that the algebraic node is equal to its standardized form

--procedure algebraic_identities(tree);	-- generate algebraic identities from algebraic nodes

--	var all_identities := [];		-- will generate and return all algebraic identities from algebraic nodes
	
--	algebraic_nodes := find_algebraic_nodes(tree);		-- find the algebraic nodes
	
--	for [-,subtree_set] in algebraic_nodes, subtree in subtree_set loop
--		all_identities with:= generate_algebraic_identity(subtree);
					-- standardize the algebraic top of the tree and convert it into an identity
--	end loop;
	
--	return all_identities; 		-- return the generated list of algebraic identities
	
--end algebraic_identities;

procedure generate_algebraic_identity(tree);
			-- calculates the standard form of an algebraic tree and equates the original form with this
--print("generate_algebraic_identity: ",unparse(tree),"\n",unparse(canorder_subtree(tree)));

	return ["ast_eq",tree,canorder_subtree(tree)];		-- simply returns the equality generated by canorder_subtree
	
end generate_algebraic_identity;

procedure canorder_subtree(tree);
			-- sorts the terms and factors of a standardized (flattened) subtree and performs cancellations
			
	if is_string(tree) then return tree; end if;			-- nothing to do if tree is just a variable or constant
	
	plus_op := alg_of(topkind := if (tk := tree(1)) = "ast_of" then tree(2) else tk end if);
				-- get the topmost node and the corresponding addition operator, or the function sign if the top opearator is a function application

		-- sort the terms and factors ofthe standardized  subtree and performs cancellation; then return the re-nested result
	flattened_tree := re_nest(order_and_cancel(st := standardize_subtree(tree,plus_op),plus_op)); 
	flattened_tree := re_nest(order_and_cancel(standardize_subtree(flattened_tree,plus_op),plus_op));
								-- put the tree into standardized form; re-nest to allow for identical associative operators in sequence
								-- repeat twice to get simplifications 2 levels deep
				-- the topmost node can be a reversal, difference, sum, or product

--	res := re_nest(order_and_cancel(flattened_tree,plus_op));


	return flattened_tree;
end canorder_subtree;

procedure order_and_cancel(tree,plus_op);		-- debugging wrapper
	res := oorder_and_cancel(tree,plus_op);
--	print("order_and_cancel:::: ",tree,"\n",unparse(re_nest(tree))," returns: ",unparse(re_nest(res)));	
	return res;
end order_and_cancel;

procedure oorder_and_cancel(tree,plus_op);
	-- sorts the terms and factors of a standardized (flattened) subtree and performs cancellations (workhorse)
--if debug_flag then print("order_and_cancel: ",tree," ",plus_op); end if;	
					-- if the topmost operation in the tree is not algebraic, simply return it unchanged. 
					-- the 'ast_of' case is needed to hanldle unary minus ops, which are written as Rev(x).
					-- 'kind' is set to the topmos algebraic opearator of the teree, if it is algebraic
	if is_string(tree) or alg_of(kind := if (tk := tree(1)) = "ast_of" then tree(2) else tk end if) /= plus_op then return tree; end if;

	case alg_role_of(kind) 			-- handle the varrious kinds of algebraic operations separately
	
					-- monadic minus: process the argument recursively, and re-integrate into a monadic minus
		when "--" => provisional_result :=    ["ast_of",tree(2),["ast_list",sarg := order_and_cancel(tree(3)(2),plus_op)]];
							-- if the simplified argument of the monadic minus is now zero, return 0. Othersie return the constucted tree
					return if sarg = zero_from_addn(plus_op) then sarg else provisional_result end if;
	
		when "-" => 		-- subtraction; sort the positive and negative parts, and then cancel
		
			[sub_op,pos_part,neg_part] := tree;			-- get the two arguments of the subtraction
			
							-- get the lead operators of the positive and negative parts, allowing for monadic minuses
			pos_tk := if is_string(pos_part) or (pos_tk := pos_part(1)) = "ast_of" then OM else pos_tk end if; 
			neg_tk := if is_string(neg_part) or (neg_tk := neg_part(1)) = "ast_of" then OM else neg_tk end if;
			
			pos_reord := order_and_cancel(pos_part,plus_op);				-- process the first argument recursively
 			neg_reord := order_and_cancel(neg_part,plus_op);				-- process the second argument recursively

 						-- if at least one of these is a flattened sum, cancellation should be attempted
 						-- if both are flattened sums, we cancel matching terms of opposite signs.
 						-- if just one is a flattened sum, we add the other to it
--print(". ",pos_reord," neg_reord: ",neg_reord," plus_op: ",plus_op," pos_tk: ",pos_tk);
 					-- rewrite the positive and negative parts as a list of additive terms;
 					-- if either is not such a list, convert it to a singleton list
			pos_reord :=if pos_tk = plus_op then pos_reord(2..) else [pos_reord] end if;
			nnre := #(neg_reord := if neg_tk = plus_op then neg_reord(2..) else [neg_reord] end if);
					-- also, get the length of the negative list of terms

 			neg_posn := 1;	-- this is advanced in the loop which follows, which iterates in coodinated fashion over the two ordered lists
 			new_pos_reord := new_neg_reord := [];		-- these will be collected after cancellation
 			
			for pos_item in pos_reord loop		-- iterate over the list of positive terms

				stgform_pos := str(standardize_bound_vars(pos_item));		-- convert it into a string, for subsequent comparison
				
						-- advance in the negative list, searching for a matching term, until we have gone too far
				while neg_posn <= nnre and (stgform_neg := str(standardize_bound_vars(neg_item := neg_reord(neg_posn)))) < stgform_pos loop
		 			new_neg_reord with:= neg_item;			-- take the negative item and advance to the next negative item
		 			neg_posn +:= 1;
		 		end loop; 
		 				
		 				-- at this point stgform_neg is at least as large as stgform_pos; check for an identical term
		 		if neg_posn <= nnre and stgform_pos = (stgform_neg := str(standardize_bound_vars(neg_item := neg_reord(neg_posn)))) then
		 			neg_posn +:= 1; continue; 
		 		end if;
									-- omit any items which cancel
		 		
				new_pos_reord with:= pos_item;			-- take the positive item and advance to the next positive item
--print("nnre: ",nnre," new_pos_reord: ",new_pos_reord," new_neg_reord: ",new_neg_reord," neg_posn: ",neg_posn," stgform_pos: ",stgform_pos," stgform_neg: ",stgform_neg);
			end loop;
							-- here we must deal with any remaining negative and positive items
			if neg_posn <= nnre and stgform_neg > stgform_pos then new_neg_reord with:= neg_item; end if;
					-- take the last negative item examined if it is larger than the last positive item
			
			if neg_posn <= nnre then new_neg_reord +:= neg_reord(neg_posn + 1..); end if;
					-- take the unexamined negative items if any

			pos_tagged := if new_pos_reord = [] then [] 	-- tag positive and negative parts as sums if they involve more than one term
					elseif #new_pos_reord = 1 then new_pos_reord(1) else [plus_op] + new_pos_reord end if;
			
			neg_tagged := if new_neg_reord = [] then [] 	-- tag positive and negative parts as sums if they involve more than one term
					elseif #new_neg_reord = 1 then new_neg_reord(1) else [plus_op] + new_neg_reord end if;
--print("new_pos_reord: ",new_pos_reord," new_neg_reord: ",new_neg_reord,"  pos_tagged: ",pos_tagged," neg_tagged: ",neg_tagged);			
						
						-- if no terms remain, reeturn the appropraite zero
						-- if only a positive term remains, return it
						-- if only a negative term remains, return its reverse
						-- otherwise return the difference of the two terms
						
			return if pos_tagged = [] and neg_tagged = [] then zero_from_addn(plus_op)
						elseif neg_tagged = [] then pos_tagged 
							elseif pos_tagged = [] then ["ast_of",sub_from_addn(plus_op),["ast_list",neg_tagged]]
								else [sub_op,pos_tagged,neg_tagged] end if;
						
 		when "*" => return [tk] + [order_and_cancel(arg,plus_op): arg in sort_by_stgs(tree(2..))];
							-- products are handled just by processing their factors recursively
					
 		when "+" => return [tk] + [order_and_cancel(arg,plus_op): arg in sort_by_stgs(tree(2..))];
							-- sums are handled just by processing their terms recursively
							-- but with a little more work we could look for opposing terms and cancel them

		otherwise => return tree;

	end case;

end oorder_and_cancel;

procedure sort_by_stgs(tree_tup); 	-- sorts a tuple of formula trees into alphabetical order of their standardized string form forms

	return [y: [x,y] in merge_sort([[str(standardize_bound_vars(tree)),tree]: tree in tree_tup])];

end sort_by_stgs;

procedure standardize_subtree(tree,plus_op);		-- debugging wrapper
	res := sstandardize_subtree(tree,plus_op);
--	print("standardize_subtree:::: ",unparse(tree)," returns: ",unparse(res));	
	
	return res;
	
end standardize_subtree;

procedure sstandardize_subtree(tree,plus_op);
			-- reduces the top of an algebraic subtree to standardized form
			-- returns sequence of identical associative operator combinations as concatenated longer list of arguments, to allow sorting
--if debug_flag then  end if;
	
	reversal_op := reversal_from_addn(plus_op);		-- find the reversal operator for the algebraic opearator family of this tree
	subtraction_op := sub_from_addn(plus_op);		-- find the subtraction operator for the algebraic opearator family of  this tree
	zero := zero_from_addn(plus_op);				-- find the zero constant for the algebraic opearator family of  this tree
	one := one_from_addn(plus_op);					-- find the unit constant for the algebraic opearator family of  this tree
	
	if is_string(tree) then return tree; end if;	-- for variables there is nothing to do
	[n1,n2,n3] := tree;								-- unpack the tree into its lead operator and two (or fewer) arguments

	if (ao := alg_of(node_kind := if n1 = "ast_of" then n2 else n1 end if)) /= plus_op or alg_role_of(node_kind) = "OM" then return tree; end if;
		-- if the tree is not consistent with the indicated plus_op, simply return it

	args := if n1 = "ast_of" then n3(2..) else tree(2..) end if;
				-- allow for case of monadic reversal operator, in which case 'args' is abtained from the template 
				-- ["ast_of","rev",[ast_list,arg]]
		
	standardized_args := [standardize_subtree(arg,plus_op): arg in args]; 
		-- standardize the operator arguments recursively. Each standardized argument returned will be either a string
		-- representing a zero or unit constant, the topmost node of a subtree not belonging to the same 
		-- algebraic set as 'tree', or a flattened product, flattened sum of products, difference of
		-- flattened sums, or reversed flattened sum
--print("standardize_subtree: ",tree," ao: ",ao," standardized_args: ",standardized_args);	

				-- get the leading operator of the first argument
	opk := if (a1 := standardized_args(1))(1) = "ast_of" then a1(2) elseif a1 = zero or a1 = one then a1 else a1(1) end if;	
	
	first_op_kind := if alg_of(opk) /= plus_op then "OM" else alg_role_of(opk) end if;
		-- if the op_kind is OM, or the first argument does not belong to the same algebraic set as its parent,
		-- convert it to the string OM
	
	if a1(1) = "ast_of" and a1(2) = reversal_op then a1 := a1(3)(2); end if;			-- extract the value of argument if it is a reversal

			-- if here is a second argument, get its lead operator 
	if (a2 := standardized_args(2)) /= OM then 
		opk := if a2(1) = "ast_of" then a2(2) elseif a2 = OM then "OM" elseif a2 = zero or a2 = one then a2  else a2(1) end if;
		second_op_kind := if alg_of(opk) /= plus_op then "OM" else alg_role_of(opk) end if;

		if a2(1) = "ast_of"  and a2(2) = reversal_op then a2 := a2(3)(2); end if;			-- extract the value of argument if it is a reversal

	end if; 
--print("standardize_subtree: ",tree," first_op_kind: ",first_op_kind," second_op_kind: ",second_op_kind," zero: ",zero," a1: ",a1);		
--print("reversal_op: ",reversal_op,"  alg_role_of(n1): ", alg_role_of(n1));	

				-- process the separate cases that arise, accodring to the algebraic nature of the topmost
				-- tree operator, and then the nature of the lead operators of its first and second argument

--if debug_flag then print("alg_role_of(node_kind):::: ",alg_role_of(node_kind)); end if;	

	case alg_role_of(node_kind)  -- node_kind is used so that Rev operators, which are function aplications, are teated correctly 
	
		when "+","+nc" => 				-- TOP LEVEL CASE: addition or non-commutative addition
--print("addition: ",a1," ",a2);	
		  case first_op_kind			-- process the various kinds of first operands, case by case
		
			when "OM","1","*","*nc" => 				-- FIRST OPERAND CASE: addition: first op is non-algebraic or a flattened product
	
			case second_op_kind
			
				when "OM","1","*" => 			-- SECOND OPERAND CASE: second op is non-algebraic or a flattened product; 
												-- just return a sum after putting the two operands into standardized order

					return [n1] + sort_by_stgs([a1,a2]);
					
				when "0" => 				-- second op is zero; na + 0
					
					return a1;				-- return the first op
			
				when "+" => 				-- second op is a flattened sum; prepend first arg

					return conc_em(a1,a2,plus_op);		-- conc_em builds and returns a flattened sumflattened sum
			
				when "-" =>  				-- second op is a difference; prepend its first arg to the first argument, and return a difference

					[sub_op,a22,a23] := a2;
--print("addition then subtraction: ",first_op_kind," ",second_op_kind," a1: ",a1," a2: ",a2," result: ",[sub_op,conc_em(a1,a22,plus_op),a23]);			

					return [sub_op,conc_em(a1,a22,plus_op),a23];
					
				when "--" =>   			-- second op is a reversal; return the difference of the first op and the second op's argument
										-- note that here a2 is already the value of the reversal argument

					return [subtraction_op,a1,a2];
				
			end case;
		
			when "0" => 				-- FIRST OPERAND CASE: addition: first op is zero; return second op
--print("first op is zero: ",if second_op_kind = "--" then ["ast_of",reversal_op,["ast_list",a2]] else a2 end if);					
					return if second_op_kind = "--" then ["ast_of",reversal_op,["ast_list",a2]] else a2 end if;
		
			when "+","+nc" =>  				-- FIRST OPERAND CASE:  addition: first op is a sum
	
			case second_op_kind
			
				when "OM","1","*" => 				-- second op is non-algebraic or a product
			
					return conc_em(a1,a2,a1(1));
			
				when "0" => 				-- second op is zero
						
					return a1;				-- return the first op
			
				when "+" => 				-- second op is a flattened sum

					return conc_em(a1,a2,a1(1));
			
				when "-" =>  				-- second op is a difference; return concatenatated sum minus second arg of second arg
			
					[sub_op,a22,a23] := a2;

					return [sub_op,conc_em(a1,a22,a1(1)),a23];
			
				when "--" =>   			-- second op is a reversal this is a1 + (-a2)
										-- note that here a2 is already the value of the reversal argument
					
					return [subtraction_op,a1,a2];		-- return a difference
				
			end case;
		
			when "-" =>  				-- FIRST OPERAND CASE: subtraction: first op is a difference
	
			case second_op_kind
			
				when "OM","1","*" => 				-- second op is non-algebraic or a product
			
					[sub_op,a12,a13] := a1;

					return [sub_op,conc_em(a12,a2,n1),a13];
			
				when "0" => 				-- second op is zero
						
					return a1;				-- return the first op
			
				when "+" => 				-- second op is a flattened sum; return concatenatated sum minus second arg of first arg
			
					[sub_op,a12,a13] := a1;

					return [sub_op,conc_em(a12,a2,a2(1)),a13];		-- use the addition operator a2(1) from the second operand
			
				when "-" =>  				-- second op is a difference
			
					[sub_op,a12,a13] := a1; [-,a22,a23] := a2;

					return [sub_op,conc_em(a12,a22,n1),conc_em(a13,a23,n1)];
			
				when "--" =>   			-- second op is a reversal this is (a - b) - a2, becomes a - (b + a2) 
										-- note that here a2 is already the value of the reversal argument
					[sub_op,a12,a13] := a1; 
					
					conced_subs := conc_em(a13,a2,n1);
					
					return [sub_op,a12,conced_subs];			-- return a difference with a concatenated subtrahend
				
			end case;
		
			when "--" =>   			-- FIRST OPERAND CASE: addition: first op is a reversal
	
			case second_op_kind
	
				when "--" =>   			-- second op is also reversal. This is (-a) + (-b), becomes -(a + b)

					return ["ast_of",reversal_op,["ast_list",conc_em(a1,a2,plus_op)]];		-- JACK
								-- reversals are pushed to the outside, so this case becomes -(a + b)
			
				otherwise => return tree;  			-- no change in this case
				
			end case;
			
		end case;
	
		when "-" =>  				-- TOP LEVEL CASE: subtraction
--print("subtraction: ",a1," ",a2," ",first_op_kind," ",second_op_kind);	
		case first_op_kind
		
			when "OM","1","*" => 				-- subtraction: first op is non-algebraic, or a product
	
			case second_op_kind
			
				when "OM","1","*","+" => 				-- second op is non-algebraic, or a product, or a flattened sum

					return [n1,a1,a2];			-- build into difference

				when "0" => 				-- second op is zero

					return a1;				-- return the first op
			
				when "-" =>  				-- second op is a difference. this is the case (a - (b - c)) becomes a + c - b
					
					[-,a22,a23] := a2;		-- decompose second op
					return [n1,conc_em(a1,a23,plus_op),a22];			-- reverse second op and build into difference
			
				when "--" =>   			-- second op is a reversal; convert to a sum: (a - (-b)) becomes (a + b)
										-- note that here a2 is already the value of the reversal argument

					return conc_em(a1,a2,plus_op);
				
			end case;
		
			when "0" => 				-- subtraction: first op is zero
	
			case second_op_kind
			
				when "OM","1","+","*" => 				-- second op is non-algebraic

					return ["ast_of",reversal_op,["ast_list",a2]];		-- convert to a reversal
			
				when "0" => 				-- second op is zero

					return zero;
			
				when "-" =>  				-- second op is a difference: this is the case 0 - (a - b), becomes (b - a) 
					
					[sub_op,a22,a23] := a2;		-- decompose second op
					return [sub_op,a23,a22];			-- reverse the subtraction
			
				when "--" =>   			-- second op is a reversal; this is the case 0 - (-a) becomes a; just return the value being reversed
										-- note that here a2 is already the value of the reversal argument

					return a2;			-- reverse the difference
				
			end case;
		
			when "+" => 				-- subtraction: first op is a flattened sum
	
			case second_op_kind
			
				when "OM","1","+","*" => 				-- second op is non-algebraic, or involves no subtraction

					return [n1,a1,a2];			-- just build into subtraction
			
				when "0" => 				-- second op is zero

					return a1;				-- return the first op
			
				when "-" =>  				-- second op is a difference
					
					[-,a22,a23] := a2;		-- decompose second op
					return [n1,conc_em(a1,a23,plus_op),a22];			-- reverse the subtraction
			
				when "--" =>   			-- second op is a reversal: this is a1 - (-b))
										-- note that in this case a2 is already the value being reversed
					return conc_em(a1,a2,plus_op);
				
			end case;
		
			when "-" =>  				-- subtraction: first op is a difference

				[-,a12,a13] := a1;		-- unpack it
	
			case second_op_kind
			
				when "OM","1","*","+" => 				-- second op is non-algebraic, or involves no subtraction

					return [n1,a12,conc_em(a13,a2,plus_op)];			-- just build into subtraction
		
				when "0" => 				-- second op is zero

					return a1;				-- return the first op
			
				when "-" =>  				-- second op is a difference

					[-,a22,a23] := a2;		-- decompose second op
					return [n1,conc_em(a12,a23,plus_op),conc_em(a13,a22,plus_op)];			-- reverse the subtraction
			
				when "--" =>   			-- second op is a reversal

					return [n1,conc_em(a12,a2,plus_op),a13];			-- reverse and add
				
			end case;
		
			when "--" =>   			-- subtraction: first op is a reversal
									-- note that in this case a1 is already the value being reversed
--print("subtraction first op is a reversal: ",a1," ",a2," ",[n1,a1,a2]);	
			case second_op_kind
			
				when "OM","1","+","*" => 				-- second op is non-algebraic, or involves no subtraction. 
														-- This is (-a1) - b becomes -(a  +  b), since the reversal cannot be pushed into b

					return ["ast_of",reversal_op,["ast_list",standardize_subtree([plus_op,a1,a2],plus_op)]];
			
				when "0" => 				-- second op is zero

					return ["ast_of",reversal_op,["ast_list",a1]];				-- return the rebuilt first op
			
				when "-" =>  				-- second op is a difference

					[-,a22,a23] := standardize_subtree([n1,a1,a2],plus_op);		-- handle recursively
					return [n1,a23,a22];			-- build reversed arguments into subtraction
			
				when "--" =>   			-- second op is a reversal: this is (-a1) - (-a2), becomes (a2 - a1)

					return [n1,a2,a1];			-- build reversed arguments into subtraction
						
				end case;
			
		end case;
	
		when "--" =>   			-- TOP LEVEL CASE: additive inverse; there is just one argument
--print("additive inverse: ",a1);	
		case first_op_kind
		
			when "+" => 				-- Inversion: argument is an addition; push reversals outward so -(a + b) remains the same
				
				return ["ast_of",reversal_op,["ast_list",a1]];			-- standardize the argument, and return as Inversion
		
			when "OM","1","*" => 				-- Inversion: first op is non-algebraic or involves no subtraction

				return ["ast_of",reversal_op,["ast_list",a1]];
		
			when "0" => 				-- Inversion: first op is zero

				return zero;			-- result is 0
		
			when "-" =>  				-- Inversion: first op is a difference

				[sub_op,a12,a13] := a1;		-- decompose first op
				return [sub_op,a13,a12];			-- reverse the subtraction
		
			when "--" =>   			-- Inversion: first op is a reversal

				return a1;			-- double reversal is original
			
		end case;
	
		when "*","*nc" =>   				-- TOP LEVEL CASE: commutative or non-commutative multiplication
	
		case first_op_kind
		
			when "OM" => 				-- FIRST OPERAND CASE:  multiplication: first op is non-algebraic
	
			case second_op_kind
			
				when "OM" => 				-- second op is non-algebraic

					return [n1,a1,a2];
			
				when "0" => 				-- second op is zero

					return zero;
			
				when "1" => 				-- second op is unity

					return a1;
			
				when "+" => 				-- second op is a flattened sum; distribute the product
--print("second op is a flattened sum: ",a2(2..)," ",distribute_mult([a1],a2(2..),n1));
							-- this routine expects to be passed tuples of sums to be multiplied out
					return distribute_mult([a1],a2(2..),n1);
			
				when "-" =>  				-- second op is a difference; distribute the product
					
					[sub_op,a22,a23] := a2;		-- decompose second op
--print("second op is a difference: a2: ",a2," a1: ",a1," n1: ",n1);
							-- this routine expects to be passed tuples of sums to be multiplied out
					return [sub_op,distribute_mult([a1],[a22],n1),distribute_mult([a1],[a23],n1)];			-- distribute the subtraction
			
				when "--" =>   			-- second op is a reversal; return a reversed concatenated product

					unreversed_prod := conc_em(a1,a2,n1);
							-- concatenate the nonalgebraic argument with the argument of the reversal
--print("unreversed_prod: ",unreversed_prod," ",a2);
					return ["ast_of",reversal_op,["ast_list",unreversed_prod]];		-- build into a top-level reversal and return
			
				when "*" =>   				-- second op is a flattened product
--print("second op is a flattened product: ",conc_em(a1,a2,a2(1))," ",a2(1));
					return conc_em(a1,a2,a2(1));		-- use the product operation from the second operand
				
			end case;
		
			when "0" => 				-- FIRST OPERAND CASE:  multiplication: first op is zero
	
				return zero;
		
			when "1" => 				-- FIRST OPERAND CASE:  multiplication: first op is unity

				return if second_op_kind = "--" then ["ast_of",reversal_op,["ast_list",a2]] else a2 end if;	-- return the actual second argument
		
			when "+" => 				-- FIRST OPERAND CASE: addition: first op is a flattened sum
--print("top level is multiplication: first op is a flattened sum, second_op_kind is: ",second_op_kind," a1: ",unparse(a1)," a2: ",unparse(a2));
			case second_op_kind
			
				when "OM","*" => 				-- second op is non-algebraic or is a product
--print("distribute_mult: ",unparse(distribute_mult(a1(2..),[a2],n1)));
					return distribute_mult(a1(2..),[a2],n1);
							-- this routine expects to be passed tuples of sums to be multiplied out
			
				when "0" => 				-- second op is zero

					return zero;
			
				when "1" => 				-- second op is unity

					return a1;				-- return the first op
			
				when "+" => 				-- second op is a flattened sum; form double distribution of sums
--print("double distribution: ",a1(2..)," ",a2(2..)," ",distribute_mult(a1(2..),a2(2..),n1));
					return distribute_mult(a1(2..),a2(2..),n1);
							-- this routine expects to be passed tuples of sums to be multiplied out
			
				when "-" =>  				-- second op is a difference; form double distribution of difference

					[sub_op,a22,a23] := a2;		-- decompose second op
--print("sum times difference: ",a1," ",a2," ",distribute_mult(a1(2..),a22(2..),n1)," ",distribute_mult(a1(2..),a23(2..),n1));
					return [sub_op,distribute_mult(a1(2..),if is_string(a22)  or alg_of(a22(1)) /= plus_op then [a22] else a22(2..) end if,n1),
					distribute_mult(a1(2..),if is_string(a23)  or alg_of(a23(1)) /= plus_op then [a23] else a23(2..) end if,n1)];			
									-- distribute the subtraction									
									-- distribute_mult expects to be passed tuples of sums to be multiplied out

			
				when "--" =>   			-- second op is a reversal; form reversed result
--print("second op is a reversal: ",ao," ",a1," ",a2);
					return ["ast_of",reversal_op,["ast_list",standardize_subtree([n1,a1,a2],ao)]];		-- this operation is executed recursively
				
			end case;
		
			when "-" =>  				-- FIRST OPERAND CASE:  multiplication: first op is a difference
				
			[-,a12,a13] := a1; 	-- decompose first op; this is a12 - a13

			case second_op_kind
			
				when "OM" => 				-- second op is non-algebraic. This case is (a12 - a13) • a2, where a12 and a13 can be flattened sums
											-- we distribute the multiplication over the subtraction and return a difference
					first_arg_pos_terms := if is_string(a12) or alg_of(a12(1)) /= plus_op or alg_role_of(a12(1)) /= "+"
										then [a12] else a12(2..) end if;
					first_arg_neg_terms := if is_string(a13) or alg_of(a13(1)) /= plus_op or alg_role_of(a13(1)) /= "+"
										then [a13] else a13(2..) end if;
										
--print("first arg of a product is a difference, second arg is non-algebraic: a1: ",unparse(a1)," a2: ",unparse(a2)," first_dist: ",unparse(distribute_mult(first_arg_pos_terms,[a2],n1))," second_dist: ",unparse(distribute_mult(first_arg_neg_terms,[a2],n1)));

					return [a1(1),distribute_mult(first_arg_pos_terms,[a2],n1), distribute_mult(first_arg_neg_terms,[a2],n1)];
								-- distribute the multiplications and return a difference			
								-- distribute_mult expects to be passed tuples of sums to be multiplied out

				when "0" => 				-- second op is zero

					return zero;
			
				when "1" => 				-- second op is unity

					return a1;
			
				when "+" => 				-- second op is a flattened sum

					return [a1(1),distribute_mult(if is_string(a12) or alg_of(a12(1)) /= plus_op  or alg_role_of(a12(1)) /= "+"
										then [a12] else a12(2..) end if,[a2],n1),
						distribute_mult(if is_string(a13)  or alg_of(a13(1)) /= plus_op  or alg_role_of(a13(1)) /= "+"
											then [a13] else a13(2..) end if,[a2],n1)];			-- distribute the subtraction			
			
				when "-" =>  				-- second op is a difference; product of two differences

					[-,a12,a13] := a1; 	-- decompose first op

					a12ta22 := distribute_mult(if is_string(a12) or alg_of(a12(1)) /= plus_op  or alg_role_of(a12(1)) /= "+"
							then [a12] else a12(2..) end if,if is_string(a22) or alg_of(a22(1)) /= plus_op then [a22] else a22(2..) end if,n1);
					a13ta23 := distribute_mult(if is_string(a13) or alg_of(a13(1)) /= plus_op  or alg_role_of(a13(1)) /= "+"
							then [a13] else a13(2..) end if,if is_string(a23) or alg_of(a23(1)) /= plus_op then [a23] else a23(2..) end if,n1);
					pos_part := conc_em(a12ta22,a13ta23,ao);

					a12ta23 := distribute_mult(if is_string(a12) or alg_of(a12(1)) /= plus_op  or alg_role_of(a12(1)) /= "+"
							then [a12] else a12(2..) end if,if is_string(a23) or alg_of(a23(1)) /= plus_op then [a23] else a23(2..) end if,n1);
					a13ta22 := distribute_mult(if is_string(a13) or alg_of(a13(1)) /= plus_op  or alg_role_of(a13(1)) /= "+"
								then [a13] else a13(2..) end if,if is_string(a22) or alg_of(a22(1)) /= plus_op then [a22] else a22(2..) end if,n1);
					neg_part := conc_em(a12ta23,a13ta23,ao);

					return [a1(1),pos_part,neg_part];
			
				when "--" =>   			-- second op is a reversal

					[-,a12,a13] := a1; 	-- decompose first op
					pos_prod := distribute_mult(if is_string(a12) or alg_of(a12(1)) /= plus_op  or alg_role_of(a12(1)) /= "+"
								then [a12] else a12(2..) end if,if is_string(a2) or alg_of(a2(1)) /= plus_op then [a2] else a2(2..) end if,n1);
					neg_prod := distribute_mult(if is_string(a13) or alg_of(a13(1)) /= plus_op  or alg_role_of(a13(1)) /= "+"
										then [a13] else a13(2..) end if,if is_string(a2) or alg_of(a2(1)) /= plus_op then [a2] else a2(2..) end if,n1);
	
					return [a1(1),neg_prod,pos_prod];
		
				when "*" =>   	-- second op is a flattened product; prepend the first argument to the second and return as a flattened product
									-- the case here is (a12 - a13) • a2, a2 being a product
					return [a1(1),conc_em(a12,a2,n1),conc_em(a13,a2,n1)];		-- return the distributed difference
--					return something;
				
			end case;
		
			when "--" =>   			-- FIRST OPERAND CASE:  multiplication: first op is a reversal
	
			case second_op_kind
			
				when "OM","+","*" => 				-- second op is non-algebraic (times reversal or sum; handle recursivey)

					unreversed_prod := [n1,a1,a2];
					return ["ast_of",reversal_op,["ast_list",standardize_subtree(unreversed_prod,ao)]];
			
				when "0" => 				-- second op is zero

					return zero;
			
				when "1" => 				-- second op is unity

					return ["ast_of",reversal_op,["ast_list",a1]];		-- restore the initially removed reversal
			
				when "-" =>  				-- second op is a difference

					[r0,r1,r2] := standardize_subtree([n1,a1,a2],ao);
					return [r0,r2,r1];
			
				when "--" =>   			-- second op is a reversal (drop reversals and handle recursively)

					unreversed_prod := [n1,a1,a2];
					return standardize_subtree(unreversed_prod,ao);
				
			end case;
		
			when "*" =>   				-- FIRST OPERAND CASE:  multiplication: first op is a flattened product
	
			case second_op_kind
			
				when "OM" => 				-- second op is non-algebraic
--print("multiplication: first op is a flattened product second op is non-algebraic: ",conc_em(a1,a2,n1));
					return conc_em(a1,a2,n1);		-- concatenate the products
			
				when "0" => 				-- second op is zero

					return zero;
			
				when "1" => 				-- second op is unity

					return a1;
			
				when "+" => 				-- second op is a flattened sum; distribute

					return distribute_mult([a1],a2(2..),n1);
			
				when "-" =>  				-- second op is a difference; distribute over difference

					[sub_op,a22,a23] := a2; 	-- decompose second op
					pos_part := distribute_mult([a1],if is_string (a22) then a22 else a22(2..) end if,n1);
					neg_part := distribute_mult([a1],if is_string (a23) then a23 else a23(2..) end if,n1);
					return [sub_op,pos_part,neg_part];
			
				when "--" =>   			-- second op is a reversal; handle recursively

					unreversed_prod := [n1,a1,a2];
					return ["ast_of",reversal_op,["ast_list",standardize_subtree(unreversed_prod,ao)]];
			
				when "*" =>   				-- second op is a flattened product
--print("product of products: ",a1," ",a2);
					return conc_em(a1,a2,n1);
				
			end case;
		
			otherwise => return tree;
			
		end case;
		
		otherwise => return tree;

	end case;
	
end sstandardize_subtree;

procedure conc_em(a1,a2,conc_op);
		-- concatenates two flattened sequences, at least one of which begins with conc_op
	
	a1 := if is_tuple(a1) and a1(1) = conc_op then a1(2..) else [a1] end if;
	a2 := if is_tuple(a2) and a2(1) = conc_op then a2(2..) else [a2] end if;
	
	return [conc_op] + a1 + a2;

end conc_em;

procedure re_nest(flattened_tree);	-- recursively reconvert a standardized (flattened) tree to its ordinary 'nested' form
--if debug_flag then print("tree to unflatten: ",flattened_tree);	end if;
	if is_string(flattened_tree) then return flattened_tree; end if;
	
	[n1,n2,n3] := flattened_tree;		-- unpack the flattened tree 
	
	op_kind := if n1 = "ast_of" then alg_role_of(n2) else alg_role_of(n1) end if;
--if debug_flag then print("re_nest: ",op_kind," ",n1," ",flattened_tree);	end if;
	if op_kind = OM or op_kind notin {"+","+nc","*","*nc","-","--"} then return flattened_tree; end if;
					-- handle non-algebraic nodes
	
	if op_kind = "--" then  		-- put reversal into standard form, dropping double reversals
		if is_tuple(revarg := n3(2)) and revarg(1) = n1 and revarg(2) = n2 then 			-- double reversal, so drop (recursively)
			return re_nest(revarg(3)(2));
		end if;
		return [n1,n2,["ast_list",re_nest(n3(2))]];
	end if;

	if op_kind = "-" then 					-- flatten the subtraction arguments
		[sub_op,a1,a2] := flattened_tree; return [sub_op,re_nest(a1),re_nest(a2)]; 
	end if;
				-- if the operation is commutative, and is either a multiplication of an addition, sort its arguments
	if op_kind = "+" or op_kind = "*" then 
--if debug_flag then print("flattened_tree before: ",flattened_tree); end if;
		flattened_tree := [n1] + sort_by_stgs([re_nest(comp): comp = flattened_tree(2..)(j)]);
--if debug_flag then print("flattened_tree after: ",flattened_tree); end if;
	else			-- ovoid sorting since not known to be commutative
		flattened_tree := [if j = 1 then comp else re_nest(comp) end if: comp = flattened_tree(j)];		-- re-nest the tree arguments
	end if;
	
	nested := flattened_tree(1..3); for j in [4..#flattened_tree] loop nested := [n1,nested,flattened_tree(j)]; end loop;
--print("re_nesting: ",op_kind," ",n1," ",flattened_tree," ",nested);	
	return nested; 
	
end re_nest;

procedure distribute_mult(tup1,tup2,mult_op);			-- distribute one tuple of sums over another
		-- this routine expects to be passed tuples of sums to be multiplied out
--print("distribute_mult tup1: ",tup1,"  tup2: ",tup2," mult_op: ",mult_op);	
	plus_op := alg_of(mult_op);
--print("unstandardized result: ",[plus_op] + [conc_em(x,y,mult_op): x in tup1,y in tup2]);		

	res := if #tup1 = 1 and #tup2 = 1 then conc_em(tup1(1),tup2(1),mult_op) 		-- if the argumets are both monomials, just multiply them
				-- otherwise mutiply their separate terms and return the sum of these products
--		else re_nest(standardize_subtree(unstand := [plus_op] + [re_nest(conc_em(x,y,mult_op)): x in tup1,y in tup2],plus_op)) end if;
		else re_nest(standardize_subtree(re_nest(unstand := [plus_op] + [re_nest(conc_em(x,y,mult_op)): x in tup1,y in tup2]),plus_op)) end if;
--print("distribute_mult tup1: ",unparse(tup1),"  tup2: ",unparse(tup2)," mult_op: ",mult_op," res: ",unparse(res)," unstand: ",unstand," standardize_subtree(unstand,plus_op): ",standardize_subtree(unstand,plus_op));	
	return res;
	
end distribute_mult;

-- *********************************************************************
-- ********************* Algebraic standardization *********************
-- *********************************************************************

-- If addition, subtraction, and multiplication, and both zero and unit constants are available,
-- we reduce formulae by distributing multiplication over addition and subtraction, until
-- a formula is fully reduced to a sum/difference of products. If multiplication is commutative
-- all the bottom-level products are then rearranged in alphabetical order of their blobs. Pure 
-- nested runs of additions and subtractions are first rearranged in alphabetical order of their blobs
-- so that cancellaion of terms having identical blobs can be performed. These terms are then rearranged
-- in alphabetical order. Hence the standardized form of an algebraic node is either: (i) one of
-- the constants 0 or 1; (ii) a non-algebraic term; (iii) a product of non-algebraic terms,
-- arranged in alphabetical order of their blobs if multiplication is commutaive; 
-- (iv) a sum of such products, arranged in alphabetical order of their blobs; (v) a difference
-- of such sums; or (vi) the reverse of such a sum.

-- Each algebraic node in a tree is associated with an algebraic operator set, which contains at least 
-- an associative addition operator '+', and perhaps also and additive unit '0', an additive inversion
-- operator '-' which can also be used in infix form as a subtraction operator, 
-- a multiplication operator '*' (in which case the addition operator is required to be commutative),
-- and a multiplicative unit constant '1'.  The map alg_of op sends each of these operators into the
-- associated '+' operator (which is always used as the representative of the algebraic operator set
-- to which it belongs). The map alg_role_of(op_sign), whose value can be '0', '1', '+', 
-- '+nc' (non-commutative addition), '-', '--' (additive inverse), '*' (multiplication), or 
-- '*nc' (non-commutative multiplication).
-- (additive inverse), 


procedure post_alg_roles(stg);		-- adds an algebraic set to alg_of and alg_role_of maps
									-- also builds the auxiliary maps sub_from_addn,reversal_from_addn
									-- the string contains the comma-separated operator names in 
									-- any order, each followed by its role
-- The string supplied should consit of ring operator names in alll the odd positions, followed by standard names
-- for the algebraic roles of each operator and constant in the following even position. The standard 
-- operator names to be used are + - -- (monadic minus) *; the standard constant signs are 0 1
-- an example is post_alg_roles("•S_PLUS,+,•S_ZERO,0,•S_ONE,1,•S_MINUS,-,•S_REV,--,•S_TIMES,*,Za,ring");

	data := breakup(stg,",;");		-- cut the string into a tuple

				-- check that the string supplied has an even number of components and contains a plus operator
				-- and has ony known standard operator signs in its even positions
	if (not even(#data)) or (not (exists plusop = data(j) | (odd(j) and data(j + 1) = "+"))) or 
				(exists opsign = data(j) | (even(j) and data(j) notin {"0","1","+","+nc","-","--","*","*nc","OM","ring"})) then 
		print("******* Error: algebraic operator set declaration ",stg," is faulty"); return;
	end if;
	
	for opsign = data(j) | odd(j) loop		-- iterate over the tuple, noting the algebraic role of each operator sign supplied

		alg_of(opsign) := plusop;						-- maps all algebraic operators into the plus operator of their ring
		alg_role_of(opsign) := djp := data(j + 1);  	-- but then correct
					-- extend supplementary maps sub_from_addn, reversal_from_addn, zero_from_addn, one_from_addn, mult_from_addn, etc.
		if djp = "-" then sub_from_addn(plusop) := opsign; elseif djp = "--" then reversal_from_addn(plusop) := opsign; end if;
		if djp = "0" then zero_from_addn(plusop) := opsign; end if;
		if djp = "1" then one_from_addn(plusop) := opsign; end if;
		if djp = "*" then mult_from_addn(plusop) := opsign; end if;
		if djp = "ring" then ring_from_addn(plusop) := opsign; end if;
		
	end loop;

--print("alg_of: ",alg_of," ",alg_role_of," ",zero_from_addn);
	
end post_alg_roles;

procedure find_ring_members(tree);	-- collects the ring membership assertions at the top conjunctive level of a tree
	
	var memb_assertions := 
		{[x,{["ast_in",y,ring := ring_from_addn(x)],["ast_in",zero_from_addn(x),ring]}]: [x,y] in one_from_addn};
					-- intialize to known members (0 and 1) this maps each known addition operator for a ring R into a pair of assertions
					-- of the abstract form {'0 in R', '1 in R'}
		-- recursive workhorse will collect and arrange by algebraic set
	
	find_ring_members_in(tree);		-- collects the ring membership assertions by recursive treewalk
--print("
find_ring_members return: ",memb_assertions);
	return memb_assertions;			-- return the full set of ring membership assertions found at top level
	
	procedure find_ring_members_in(tree);		-- collects the ring membership assertions

		if is_string(tree) then return; end if;		-- nothing to do if string
		
		[n1,n2,n3] := tree;							-- unpack tree
				
				-- process top-level conjuncts by walkig recursively dwn the lis of conjuctions at the top level
		if n1 = "ast_and" or n1 = "AMP_" then find_ring_members_in(n2); find_ring_members_in(n3); return; end if;
	
--print("find_ring_members_in: ",tree," alg_of(n3): ",alg_of(n3));				
					-- otherwise, if we have a membership statement in a node whose opearator is algebraic, then collect it
		if n1 = "ast_in" and (plus_op := alg_of(n3)) /= OM and n3 = ring_from_addn(plus_op) then
						-- we have a conjunct of the form x in R; collect this ring membership assertion
			memb_assertions(plus_op) := (memb_assertions(plus_op)?{}) with tree;	
		end if;
				

	end find_ring_members_in;

end find_ring_members;

--					********************************************************************************
--					*********** Miscellaneous tree searching and transformation routines ***********
--					********************************************************************************

	procedure find_fnc_symbs(node); 		-- find the function symbols in a tree (main entry)
		all_fnc_symbs := {}; find_fnc_symbs_in(node);
		return all_fnc_symbs - builtin_fcns;			-- use the recursive workhorse and a global variable
	end find_fnc_symbs;
	
	procedure find_fnc_symbs_in(node); 		-- find the function symbols in a tree (recursive workhorse)
--print("find_fnc_symbs_in: ",node," ",is_string(node)," ",all_fnc_symbs);
		if is_string(node) then return;  end if; 			-- down to a variable or constant

		case (ah := abbreviated_headers(n1 := node(1)))?n1

			when "()" => 				-- this is the case of functional and predicate application; the second variable is a reserved symbol, not a set

				all_fnc_symbs with:= node(2); for sn in node(3..) loop find_fnc_symbs_in(sn); end loop;

			when "and","or","==","+","-","{-}","in","notin","/==","=","/=","[]","[-]","ast_if_expr","ast_if", 
						"{.}","itr","Etr","incs","incin","imp","*","->","not","null","{}","{/}","EX","ALL" =>
						-- various builtins

				for sn in node(2..) loop find_fnc_symbs_in(sn); end loop;
				-- now collect free variables in args

			otherwise => 		-- additional infix, prefix, and ordinary operators; functional application

				all_fnc_symbs with:= node(if #node = 2 then 1 else 1 end if); 
				for sn in node(2..) loop find_fnc_symbs_in(sn); end loop; 
						-- now collect free variables in args
		
		end case;
		
	end find_fnc_symbs_in;

	procedure dequantify(tree,substitution_tup);
	 	-- makes substitutions for specified quantified variables of a formula. (main entry; uses workhorse)

		-- this routine works from left-to right through a quantified formula, progressively using elements from the 
		-- indicated tuple to make day_total for the bound variables encountered. It descends thru quantifiers,
		-- the boolean operators and, or, not, and •imp (but not equivalences), keeping track of the boolean sign
		-- of the terms encountered, and replacing quantified variables where possible. day_total of non-strings
		-- for existential quantified variables are refused.
		-- A triple [substituted_formula,set_of_strings_skolemized,unused_] is returned.
		-- non-empty unused_substitutions list probably represents an error.
		
		-- to allow specified quantifiers or setformers which would otherwise attract substitutions to be bypassed
		-- selectively, we allow OM elements to be included in the susbstitution tup passed to this routine.
		-- when such an OM is matched to a substitution-candidate explciitly or implicitly quantified subexpression,
		-- it terminates substitution, either before it started or at the quantifier reached.  

		return dequantify_in(tree,substitution_tup,{},true,{}); print("returned: ",res); 
		 			-- call the workhorse with an initially null list of bound variables
	end dequantify;

	procedure dequantify_in(tree,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced);	 
--print("dequantify_in_trace: ",unparse(tree));
res := dequantify_in_trace(tree,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced);	
--print("returned: ",res); 
return res;
	end dequantify_in;

	procedure dequantify_in_trace(tree,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced);
	 	-- inner recursive workhorse of substitution routine. substitution_tup is passed down from the initial
	 	-- call, with progressive deletion of the elements of substitution_tup as they are used and 
	 	-- pass into substitution_map, which is used so that every occurrence of a bound variable
		-- will be replaced by its assigned expression, if it has not been bypassed  

		if is_string(tree) and tree in bound_vars then 	-- replace bottom-level names as specified
				return substitution_map(tree)?tree; 
		end if;
				
		[n1,n2,n3] := tree;			-- unpack the node
		
		case abbreviated_headers(n1)?n1		-- handle quantifiers and setformers in a special way, to detect bound variables 

			when "and","or" => 	-- 'positive' boolean operators

				[n2,skolemized_in_a1,substitution_tup] := 
					dequantify_in(n2,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced);		-- continue recursively
				[n3,skolemized_in_a2,substitution_tup] := 	
					dequantify_in(n3,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced);		-- continue recursively

				return [[n1,n2,n3],skolemized_in_a1 + skolemized_in_a2,substitution_tup];
						-- since substitutions may have been done in either of the arguments, substitution_tup may have shortened
 
 			when "not" => 		-- 'negative' boolean operator

				[n2,skolemized_in_a1,substitution_tup] := 		-- continue recursively, reversing the virtual sign of the subformula
					dequantify_in(n2,substitution_tup,substitution_map,not bool_sign,bound_vars_not_replaced);
	
				return [[n1,n2],skolemized_in_a1,substitution_tup];
						-- since substitutions may have been done in either of the arguments, substitution_tup may have shortened

			when "imp" => 		-- 'mixed' boolean operator; this is like 'or', but the first argument reverses sign

				[n2,skolemized_in_a1,substitution_tup] := 
					dequantify_in(n2,substitution_tup,substitution_map,not bool_sign,bound_vars_not_replaced);		-- continue recursively
--print("imp: ",n3," substitution_tup: ",substitution_tup," substitution_map: ",substitution_map);
				[n3,skolemized_in_a2,substitution_tup] := 	
					dequantify_in(n3,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced);		-- continue recursively

				return [[n1,n2,n3],skolemized_in_a1 + skolemized_in_a2,substitution_tup];
						-- since substitutions may have been done in either of the arguments, substitution_tup may have shortened

			when "EX" => 		-- existential. The second node is an iterator
				-- a syntactic example is: ["ast_iter_list", ["ast_in", "X", "S"], ["DOT_INCIN", "Y", "T"]].
				
				[n1,n2,n3] := tree;		-- unpack the parts of the syntax node
	 				
				limiting_clauses := [];		-- the limiting_clauses will be conjoined into a final conjunction, which will appear in 
											-- result formula as (clause1 & clause2 & ...) •imp substituted_body
				leftover_iteration_clauses := [];		-- to accumulate iteration_clauses whose bound variable is not replaced
				
				iter_tag := n2(1); 			-- get the list tag for the iterator
				replacement_stopped := false;		-- flag indicating wheter replacement was stopped either explicitly or implicitly

				if not bool_sign then
							-- the sign has reversed, so this is an implicit universal. all substitutions will be accepted
					
	 				for [iter_op,bv,limiting_expn] in n2(2..) loop		-- process all the clauses of the iterator
	 
	 					if substitution_tup /= [] and not replacement_stopped then		-- there are still more substitutions available, so make one more
	 	
	 						limiting_expn := substitute_in(limiting_expn,substitution_map,bound_vars_not_replaced);
	 							 		-- make the accumulated substitution in the limiting_expn; use the inner workhorse directly
							
							replacement_expression fromb substitution_tup;		-- get the next replacement expression to use
		
							if replacement_expression = OM then		-- replacement is being stopped manually 
							
								replacement_stopped := true;	-- only prior replacements will be used
								substitution_tup := [replacement_expression] + substitution_tup;	-- return the unused replacement expression
								
							else	-- note the replacement to be made henceforth
					
								substitution_map(bv) := replacement_expression;		-- this will replace the bound variable henceforth
	
							end if;
							
							limiting_clauses with:= [iter_op,replacement_expression,limiting_expn];		-- in the new clause, the bound variable is replaced
										-- accumulate the substituted limiting_clause, for later use, as explained above
	
						else			-- there are no more substitutions available or replacement has been stopped, 
										-- so the remaining pieces of the iterator  are  'leftovers'
	
							limiting_expn := substitute_in(limiting_expn,substitution_map,bound_vars_not_replaced);
	 							 		-- make the accumulated substitution in the limiting_expn; use the inner workhorse directly
							leftover_iteration_clauses with:= [iter_op,bv,limiting_expn];	-- the substituted clause will be used in a quantifier
	
						end if;
		
					end loop;		-- once all the clauses of the iterator have been processed, we process the quantified predicate
									-- this is the existential case, reversed
	 
	 				bound_vars_not_replaced +:= {b: [op,bv,limit] in leftover_iteration_clauses};
							-- there may be additional bound variables not being replaced
	 				
	 				if leftover_iteration_clauses = [] then		-- just return the substituted body as an implication involving all the limiting_clauses 
 		 			
	 					[n3,skolemized_in_pred,substitution_tup] := dequantify_in(n3,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced);
	 							-- make substitutions in the predicate
				 		conj := conjoin(limiting_clauses); 		-- conjoin a collection of clauses
				 		return [if limiting_clauses = [] then n3 else ["ast_and",conj,n3] end if,skolemized_in_pred,substitution_tup];			-- return the said implication
	 					 
	 				else 		-- return the substituted body as a quantified implication involving all the limiting_clauses
	 	
	 					n3 := substitute_in(n3,substitution_map,bound_vars_not_replaced); -- make a simple substitution
	 					n3 := [n1,[iter_tag] + leftover_iteration_clauses,n3];			-- reattach the quantifier and remaining iterators
	 					
				 		conj := conjoin(limiting_clauses); 		-- conjoin a collection of clauses
				 		return [if limiting_clauses = [] then n3 else ["ast_and",conj,n3] end if,[],substitution_tup];			-- return the said implication. nothing is skolemized
	 					
	 				end if;
	 
	 			else		-- this is really an existential, so only constant substitutions will be accepted. These will be
							-- noted as having been skolemized, i.e. they receive their definitions by replacing bound variables in an existential
			
					skolemized_here := [];		-- start collecting variables which are skolemized by this existential
			
	 				for [iter_op,bv,limiting_expn] in n2(2..) loop		-- process the clauses of the iterator until the first that gives trouble
	 
	 					if substitution_tup /= [] and not replacement_stopped then
			-- there are still more substitutions available, so see if we can make one more
	 	
	 						limiting_expn := substitute_in(limiting_expn,substitution_map,bound_vars_not_replaced);
	 							 		-- make the accumulated substitution in the limiting_expn; use the inner workhorse directly
	
							replacement_expression fromb substitution_tup;		-- get the next replacement expression to use
	
							if replacement_expression = OM or not is_string(replacement_expression) then
								-- replacement is being stopped manually or implicitly
--print("really an existential replacement_stopped:");							
								replacement_stopped := true;	-- only prior replacements will be used
								leftover_iteration_clauses with:= [iter_op,bv,limiting_expn];		-- this iteration clause is bypassed
								substitution_tup := [replacement_expression] + substitution_tup;	-- return the unused replacement expression
		
							else			-- skolemization by this existential is possible
							 
								substitution_map(bv) := replacement_expression;		-- this string will replace the bound variable henceforth
							
								limiting_clauses with:= [iter_op,replacement_expression,limiting_expn];
										-- in the new clause, the bound variable is replaced.
										-- accumulate the substituted limiting_clause, for later use, as explained above
	 							skolemized_here with:= replacement_expression;		-- note that the replacement_expression	(a string)
	 																				-- is being defined here				
	
							end if;
							
						else			-- there are no more susbstitutions available  or replacement has been stopped,
										-- so the remaining pieces of the iterator  are  'leftovers'
	
							limiting_expn := substitute_in(limiting_expn,substitution_map,bound_vars_not_replaced);
	 							 		-- make the accumulated substitution in the limiting_expn; use the inner workhorse directly
							leftover_iteration_clauses with:= [iter_op,bv,limiting_expn];	-- the substituted clause will be used in a quantifier
	
						end if;
		
					end loop;		-- once all the clauses of the iterator have been processed, we process the quantified predicate
									-- this is the existential case, not reversed

	 				if leftover_iteration_clauses = [] then		-- just return the substituted body as an implication involving all the limiting_clauses 
	 					
		 				[n3,skolemized_in_pred,substitution_tup] := dequantify_in(n3,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced);
				 		conj := conjoin(limiting_clauses); 		-- conjoin a collection of clauses
				 		return [if limiting_clauses = [] then n3 else ["ast_and",conj,n3] end if,skolemized_here + skolemized_in_pred,substitution_tup];			-- return the said implication
	 					 
	 				else 		-- just return the substituted body as a quantified implication involving all the limiting_clauses
	 	
	 					n3 := substitute_in(n3,substitution_map,bound_vars_not_replaced);
	 							-- make substitutions in the predicate. Here, only a simple substitution is made
	 					n3 := [n1,[iter_tag] + leftover_iteration_clauses,n3];			-- reattach the quantifier and remaining iterators
--print("really an existential leftover: ",n3," ",leftover_iteration_clauses);	 					
				 		conj := conjoin(limiting_clauses); 		-- conjoin a collection of clauses
				 		return [if limiting_clauses = [] then n3 else ["ast_and",conj,n3] end if,skolemized_here,substitution_tup];
				 					-- return the said implication, noting all  the variables that have been skolemized here and in the predicate
	 					
	 				end if;
				
				end if;

		when "ALL" => 		-- universal. This is similar to the existential case, but with reversal of the case to skolemize 
			
			[n1,n2,n3] := tree;		-- unpack the parts of the syntax node
 				
			limiting_clauses := [];		-- the limiting_clauses will be conjoined into a final conjunction, which will appear in 
										-- result formula as (clause1 & clause2 & ...) •imp substituted_body
			leftover_iteration_clauses := [];		-- to accumulate iteration_clauses whose bound variable is not replaced
			
			iter_tag := n2(1); 			-- get the list tag for the iterator

			replacement_stopped := false;		-- flag indicating whether replacement was stopped either explicitly or implicitly
	
			if bool_sign then
						-- the sign has not reversed, so this is a true universal. all substitutions will be accepted
				
 				for [iter_op,bv,limiting_expn] in n2(2..) loop		-- process all the clauses of the iterator
 
 					if substitution_tup /= [] and not replacement_stopped then		-- there are still more substitutions available, so make one more
 	
 						limiting_expn := substitute_in(limiting_expn,substitution_map,bound_vars_not_replaced);
 							 		-- make the accumulated substitution in the limiting_expn; use the inner workhorse directly
						
						replacement_expression fromb substitution_tup;		-- get the next replacement expression to use
	
						if replacement_expression = OM then		-- replacement is being stopped manually 
						
							replacement_stopped := true;	-- only prior replacements will be used
							leftover_iteration_clauses with:= [iter_op,bv,limiting_expn];		-- this will not be used, so become a leftover_iteration_clause
--print("replacement_stopped: ");							
						else	-- note the replacement to be made henceforth
				
							substitution_map(bv) := replacement_expression;		-- this will replace the bound variable henceforth
							limiting_clauses with:= [iter_op,replacement_expression,limiting_expn];
									-- in the new clause, the bound variable is replaced
									-- accumulate the substituted limiting_clause, for later use, as explained above

						end if;

					else			-- there are no more susbstitutions available or replacement has been stopped, 
									-- so the remaining pieces of the iterator  are  'leftovers'

						limiting_expn := substitute_in(limiting_expn,substitution_map,bound_vars_not_replaced);
 							 		-- make the accumulated substitution in the limiting_expn; use the inner workhorse directly
						leftover_iteration_clauses with:= [iter_op,bv,limiting_expn];	-- the substituted clause will be used in a quantifier

					end if;
	
				end loop;		-- once all the clauses of the iterator have been processed, we process the quantified predicate
								-- this is the universal case, not reversed
 
 				bound_vars_not_replaced +:= {b: [op,bv,limit] in leftover_iteration_clauses};
						-- there may be additional bound variables not being  replaced
--print("leftover_iteration_clauses: ",leftover_iteration_clauses);			
  				if leftover_iteration_clauses = [] then		-- just return the substituted body as an implication involving all the limiting_clauses 
 					
					[n3,skolemized_in_pred,substitution_tup] := dequantify_in(n3,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced);
 							-- make substitutions in the predicate
		 			conj := conjoin(limiting_clauses); 		-- conjoin a collection of clauses
			 		return [if limiting_clauses = [] then n3 else ["DOT_IMP",conj,n3] end if,skolemized_in_pred,substitution_tup];			-- return the said implication
					 
 				else 		-- return the substituted body as a quantified implication involving all the limiting_clauses
	
 					n3:= substitute_in(n3,substitution_map,bound_vars_not_replaced);
					n3 := [n1,[iter_tag] + leftover_iteration_clauses,n3];			-- re-attach the quantifier and remaining iterators
 					
			 		conj := conjoin(limiting_clauses); 		-- conjoin a collection of clauses
			 		return [if limiting_clauses = [] then n3 else ["DOT_IMP",conj,n3] end if,[],substitution_tup];			-- return the said implication. nothing is skolemized
 					
 				end if;
 
			else		-- this is really an implicit existential, so only constant substitutions will be accepted. These will be
						-- skolemized
				
				skolemized_here := [];		-- start collecting variables which are skolemized by this existential
		
 				for [iter_op,bv,limiting_expn] in n2(2..) loop		-- process the clauses of the iterator until the first that gives trouble
 
 					if substitution_tup /= [] and not replacement_stopped then
		-- there are still more sustitutions available, so see if we can make one more
 	
 						limiting_expn := substitute_in(limiting_expn,substitution_map,bound_vars_not_replaced);
 							 		-- make the accumulated substitution in the limiting_expn; use the inner workhorse directly

						replacement_expression fromb substitution_tup;		-- get the next replacement expression to use

						if replacement_expression = OM or not is_string(replacement_expression) then
							-- replacement is being stopped manually or implicitly
						
							replacement_stopped := true;	-- only prior replacements will be used
							leftover_iteration_clauses with:= [iter_op,bv,limiting_expn];		-- this iteration clause is bypassed
							substitution_tup := [replacement_expression] + substitution_tup;	-- return the unused replacement expression
							
						else			-- skolemization by this existential is possible
						 
							substitution_map(bv) := replacement_expression;		-- this string will replace the bound variable henceforth
						
							limiting_clauses with:= [iter_op,replacement_expression,limiting_expn];
									-- in the new clause, the bound variable is replaced.
									-- accumulate the substituted limiting_clause, for later use, as explained above
 							skolemized_here with:= replacement_expression;		-- note that the replacement_expression	(a string)
 																				-- is being defined here				

						end if;
						
					else			-- there are no more susbstitutions available  or replacement has been stopped,
									-- so the remaining pieces of the iterator  are  'leftovers'

						limiting_expn := substitute_in(limiting_expn,substitution_map,bound_vars_not_replaced);
 							 		-- make the accumulated substitution in the limiting_expn; use the inner workhorse directly
						leftover_iteration_clauses with:= [iter_op,bv,limiting_expn];	-- the substituted clause will be used in a quantifier

					end if;
	
				end loop;		-- once all the clauses of the iterator have been processed, we process the quantified predicate
  				
 				if leftover_iteration_clauses = [] then		-- just return the substituted body as an implication involving all the limiting_clauses 
 					
					[n3,skolemized_in_pred,substitution_tup] := dequantify_in(n3,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced);
 							-- make substitutions in the predicate
			 		conj := conjoin(limiting_clauses); 		-- conjoin a collection of clauses
			 		return [if limiting_clauses = [] then n3 else ["DOT_IMP",conj,n3] end if,skolemized_here + skolemized_in_pred,substitution_tup];			-- return the said implication
 					 
 				else 		-- just return the substituted body as a quantified implication involving all the limiting_clauses
 --print("leftover_iteration_clauses: ",leftover_iteration_clauses);	
 					n3 := [n1,[iter_tag] + leftover_iteration_clauses,n3];			-- reattach the quantifier and remaining iterators
 					

 					n3 := substitute_in(n3,substitution_map,bound_vars_not_replaced);
 							-- make substitutions in the predicate. Here, only a simple substitution is made
			 		conj := conjoin(limiting_clauses); 		-- conjoin a collection of clauses
			 		return [if limiting_clauses = [] then n3 else ["DOT_IMP",conj,n3] end if,skolemized_here,substitution_tup];
			 					-- return the said implication, noting all the variables that have been skolemized here and in the predicate
 					
 				end if;
			
			end if;

			when "in" => 		-- this can only be processed when the second argument is a setformer

				if (n31 := n3(1)) /= "ast_genset" and  n31 /= "ast_genset_noexp" then  -- cannot be dequantified 
						-- just perform a simple substitution, and return the triple 
						-- [substituted_result,nothing_skolemized,remaining_substitution_tup] 
--print("cannot be dequantified: ",tree," substitution_map: ",substitution_map);					
					return [[tree(1)] + [substitute_in(x,substitution_map,bound_vars_not_replaced): x in tree(2..)],[],substitution_tup];
				
				elseif n31 = "ast_genset" then 				-- we have a set-former with an expression
						-- convert it to an existential, and process as such
						-- here the subnode is of length 4, m2 being the tree for the expr and m3 the iterator

					[m1,m2,m3,m4] := n3;			-- unpack the setformer subnode

					corresponding_existential := ["ast_exists",m3,["ast_and",["ast_eq",n2,m2],m4]];
					return dequantify_in(corresponding_existential,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced);
							-- continue recursively, treating this as an existential
				
				else  				-- we have a set-former with no expression. 
									-- The membership relation x in {y in u | P(y)} simplifies to (x in u and P(x)), but not here	

					return [[tree(1)] + [substitute_in(x,substitution_map,bound_vars_not_replaced): x in tree(2..)],[],substitution_tup];
				
				end if;
				
			when "notin" => 	-- this is much like 'in', but with a reversal of sign

				if (n31 := n3(1)) /= "ast_genset" and  n31 /= "ast_genset_noexp" then  -- cannot be dequantified 
						-- just perform a simple substitution, and return the triple 
						-- [substituted_result,nothing_skolemized,remaining_substitution_tup] 
					
					return [[tree(1)] + [substitute_in(x,substitution_map,bound_vars_not_replaced): x in tree(2..)],[],substitution_tup];
				
				elseif n31 = "ast_genset" then 				-- we have a set-former with an expression
						-- convert it to a related existential, and process as such. we use the 'FORALL ... not ...' form
						-- here the subnode is of length 4, m2 being the tree for the expr and m3 the iterator

					[m1,m2,m3,m4] := n3;			-- unpack the setformer subnode

					corresponding_universal := ["ast_forall",m3,["ast_not",["ast_and",["ast_eq",n2,m2],m4]]];
--print("'notin ast_genset' case: ",corresponding_universal); print(unparse(corresponding_universal));
					return dequantify_in(corresponding_universal,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced);
							-- continue recursively, treating this as a universal
				
				else  				-- we have a set-former with no expression. 
									-- The membership relation x notin {y in u | P(y)} simplifies to not(x in u and P(x)), but not here	
 
 					return [[tree(1)] + [substitute_in(x,substitution_map,bound_vars_not_replaced): x in tree(2..)],[],substitution_tup];
				
				end if;

--->working dequantify
			when "incs" =>				-- set inclusion. we handle this in case the second argument is a setformer by rewriting
												-- a incs {e(x): x in s | P(x)} as (FORALL x in s | P(x) •imp (e(x) in a))
												-- and a incs {x in s | P(x)} as (FORALL x in s | P(x) •imp (x in a))
 
				if (n31 := n3(1)) /= "ast_genset" and  n31 /= "ast_genset_noexp" then  -- cannot be dequantified 
						-- just perform a simple substitution, and return the triple 
						-- [substituted_result,nothing_skolemized,remaining_substitution_tup] 
					
					return [[tree(1)] + [substitute_in(x,substitution_map,bound_vars_not_replaced): x in tree(2..)],[],substitution_tup];
				
				elseif n31 = "ast_genset" then 				-- we have a set-former with an expression; see above
						-- convert it to a universal, and process as such
						-- here the subnode is of length 4, m2 being the tree for the expr and m3 the iterator

					[m1,m2,m3,m4] := n3;			-- unpack the setformer subnode

					corresponding_universal := ["ast_forall",m3,["DOT_IMP",m4,["ast_in",m2,n2]]];
					return dequantify_in(corresponding_universal,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced);
							-- continue recursively, treating this as a universal
				
				else  				-- we have a set-former with no expression. Treat as described above

					[m1,m2,m3] := n3;			-- unpack the setformer subnode
 
 					the_var := m2(2)(2);			-- get the quantified variable 
					corresponding_universal := ["ast_forall",m2,["DOT_IMP",m3,["ast_in",the_var,n2]]];
					return dequantify_in(corresponding_universal,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced);
							-- continue recursively, treating this as a universal
				
				end if;

 			when "incin" => 				-- reversed set inclusion. we handle this in case the first argument is a setformer by rewriting
												-- {e(x): x in s | P(x)} •incin a as (FORALL x in s | P(x) •imp (e(x) in a))
												-- and {x in s | P(x)} •incin a as (FORALL x in s | P(x) •imp (x in a))
 
				if (n21 := n2(1)) /= "ast_genset" and  n21 /= "ast_genset_noexp" then  -- cannot be dequantified 
						-- just perform a simple substitution, and return the triple 
						-- [substituted_result,nothing_skolemized,remaining_substitution_tup] 
					
					return [[tree(1)] + [substitute_in(x,substitution_map,bound_vars_not_replaced): x in tree(2..)],[],substitution_tup];
				
				elseif n21 = "ast_genset" then 				-- we have a set-former with an expression; see above
						-- convert it to a universal, and process as such
						-- here the subnode is of length 4, m2 being the tree for the expr and m3 the iterator

					[m1,m2,m3,m4] := n2;			-- unpack the setformer subnode

					corresponding_universal := ["ast_forall",m3,["DOT_IMP",m4,["ast_in",m2,n3]]];
					return dequantify_in(corresponding_universal,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced);
							-- continue recursively, treating this as a universal
				
				else  				-- we have a set-former with no expression. Treat as described above

					[m1,m2,m3] := n2;			-- unpack the setformer subnode
 
 					the_var := m2(2)(2);			-- get the quantified variable 
					corresponding_universal := ["ast_forall",m2,["DOT_IMP",m3,["ast_in",the_var,n3]]];
					return dequantify_in(corresponding_universal,substitution_tup,substitution_map,bool_sign,bound_vars_not_replaced);
							-- continue recursively, treating this as a universal
				
				end if;

			when "()" => 	-- predicate or function application
--print("function application: ",tree);
			return [tree(1..2) with substitute_in(tree(3),substitution_map,bound_vars_not_replaced),[],substitution_tup];

		end case;		-- in the remaining cases we just perform a simple substitution, 
						-- and return the triple [substituted_result,nothing_skolemized,remaining_substitution_tup] 
		
		return [[tree(1)] + [substitute_in(x,substitution_map,bound_vars_not_replaced): x in tree(2..)],[],substitution_tup];
		
	end dequantify_in_trace;
 				
 	procedure conjoin(clauses); 			-- conjoin a collection of clauses

		conj := clauses(1); 				-- start building a conjunction
 				
 		for j in [2..#clauses] loop conj := ["ast_and", conj,clauses(j)]; end loop;		-- conjoin the next  clause
 		
 		return conj;
		
	end conjoin;


--->tests
--								****************************************************
--								***************** Test Collection ******************
--								****************************************************
--
procedure test_find_fnc_symbs; 			-- test of the find_fnc_symbs procedure
print("****** TESTS OF FIND_FUNCTION_SYMBOLS PROC ******");
	
	stgs := ["sin(x) + cos(x);",
			"{sin(x) + cos(x): x in f(y) | P(x,y)};",
			"{x in f(y) | P(x,y)};",
			"(EXISTS x in f(y)~[g(y,h(y))] | P(x,y));",
			"{{x},{{x},{{y},y}}};"];
	
	for stg in stgs loop
		print(); tree := parze_expr(stg); print(find_fnc_symbs(tree(2)));
	end loop; 
	
end test_find_fnc_symbs;

procedure test_dequantify(); 			-- test of the dequantify procedure
print("****** TESTS OF DEQUANTIFY PROC ******");
	-- the tuples used for testing consist of a formula to be dequantified, 
	-- followed by a string of tems to be substituted for the quantified variables in the first formula.
	
	tups := [["not ((EXISTS x in s | (FORALL y in s | P(x,y))) •imp (FORALL y in s | (EXISTS x in s | P(x,y))));","a;","","b;"],
			["(not (((A in s) and (FORALL Y in s | P(A,Y))) •imp ((B in s) •imp (EXISTS X in s | P(X,B)))));","b;","a;"],
			["not ((FORALL x in s | (FORALL y in s | P(x,y))) •imp (FORALL y in s | (FORALL x in s | P(x,y))));","","a;","b;"],
			["not ((FORALL X in S | (FORALL Y in S | P(X,Y))) •imp ((A in S) •imp ((B in S) •imp P(B,A))));","b;","a;"],
--			["(not (((FORALL Y in s | P(A,Y))) •imp ((EXISTS X in s | P(X,B)))));","b;","a;"],
--			["(FORALL x in u | P(x));","g(c);"],
--			["(EXISTS x in u, y in v(x) | P(x,y)) or (FORALL x in u | R(x));","cc;","","dd;"],
--			["(FORALL x in u, y in v(x) | P(x,y)) or (FORALL x in u | R(x));","H(u);","","G(u);"],
--			["(EXISTS y in u | (FORALL X in S | P(x,y)));","cc;","G(u);"],
--			["(EXISTS y in u | (FORALL X in S | P(x,y)));","cc;"],
--			["(EXISTS y in u | (FORALL X in S | P(x,y))) or (FORALL X in S | Q(x));","G(u);"],
--			["(FORALL X in S | (P(X) •imp (E(X) in A)));","G(u);"],
--			["a incs {e(x,y): x in  s,y in t | P(x,y)};","G(u);","H(u);"],
--			["a incs {e(x,y): x in  s,y in t | P(x,y)};","G(u);"],
--			["a incs {x in  s| P(x)};","G(u);"],
--			["{e(x,y): x in  s,y in t | P(x,y)} •incin a;","G(u);","H(u);"],
--			["{e(x,y): x in  s,y in t | P(x,y)} •incin a;","G(u);"],
--			["{x in  s| P(x)} •incin a;","G(u);"],
--			["(FORALL Y in S | (not (X = E(Y) and P(Y))));","G(u);"],
--			["(EXISTS x in u | P(x));","G(u);"],
--			["(FORALL x in u, y in v | P(x,y));","cc;"],
--			["(FORALL x in u, y in v | P(x,y));","cc;","dd;"],
--			["(FORALL x in u, y in v(x) | P(x,y));","cc;","G(u);"],
--			["(FORALL x in u, y in v(x) | P(x,y));","H(u);","G(u);"],
--			["(FORALL x in u | (EXISTS y in v(x) | P(x,y)));","H(u);","cc;"],
--			["(FORALL x in u | (EXISTS y in v(x) | P(x,y)));","H(u);","G(u);"],
--			["(EXISTS x in u | P(x));","G(u);"],
--			["(EXISTS x in u, y in v | P(x,y));","cc;"],
--			["(EXISTS x in u, y in v | P(x,y));","cc;","dd;"],
--			["(EXISTS x in u, y in v | P(x,y));","cc;","G(u);"],
--			["(EXISTS x in u, y in v | P(x,y));","H(u);","G(u);"],
--			["not (FORALL x in u | P(x));","dd;"],
--			["not (EXISTS x in u | P(x));","G(u);"],
--			["(FORALL x in u | P(x)) and (FORALL x in u | Q(x));","G(u);","H(u);"],
--			["(FORALL x in u | P(x)) or (FORALL x in u | Q(x));","G(u);","H(u);"],
--			["(EXISTS x in u | P(x)) •imp (FORALL x in u | Q(x));","G(u);","H(u);"],
--			["x in {y in s | P(y)};","cc;"],
--			["x notin {y in s | P(y)};","H(u);"],
--			["x in {e(y): y in s | P(y)};","cc;"],
--			["x notin {e(y): y in s | P(y)};","H(u);"],
			["(EXISTS x in u | P(x));","cc;"]];
	
	for tup in tups loop
		print(); tree := parze_expr(tup(1))(2); substitution_tup := [if f = "" then OM else parze_expr(f)(2) end if: f in tup(2..)];
		[formula,skolemized,unused] := dequantify(tree,substitution_tup); 
		print("dequantified formula is: ",unparse(formula)); 
		print("variables skolemized are: ",skolemized); 
		print("unused replacements are: ",[unparse(r): r in unused]);
	end loop;
	
end test_dequantify;

procedure test_monotone_infer; 	 		-- test of the monotone_infer procedure
--->tests2
print("****** TESTS OF NEW MONOTONE INFERENCE PROC ******");
	post_monotone("Un,++;Pow,+;#,+;•PLUS,+,+;•TIMES,+,+;Finite,-;Is_map,--;One_1_map,-");
			 -- note monotonicity properties of builtins

	forms := ["a + b = b + a;",
			"(FORALL u in domain(f) | #u in x2) •imp (FORALL u in #domain(f) | #u in x2);",
--			"{[x,f(x)]: x in s | x in {c}} = {[x,f(x)]: x in s * {c}};",
--			"a * b = b * a;",
--			"if true then a + b else c end if = b + a;",
--			"Un(a + b) = Un(b + a);",
--			"pow(Un(a + b)) = pow(Un(b + a));",
--			"#pow(Un(a + b)) = #pow(Un(b + a));",
--			"#pow(Un(a + b)) = #pow(b + a);",
--			"a + b incs a;",
--			"#(a + b) incs #a;",
--			"#pow((a + b)) incs #pow(a);",
--			"#pow(Un(a + b)) incs #pow(Un(a));",
--			"#pow(Un(a + b)) incs #pow(Un(c));",
--			"Un(a + b) = Un(a) +  Un(b);",
--			"Un(a) +  Un(b) = Un(a + b);",
--			"Un(Un(a + b)) = Un(Un(a)) +  Un(Un(b));",
--			"Un(Un(a) + Un(b)) = Un(Un(a)) +  Un(Un(b));",
--			"pow(Un(a + b)) = pow(Un(a)) +  pow(Un(b));",
--			"{e(x): x in a + b | P(x)} = {e(x): x in b + a | P(x)};",
--			"{e(x,x2): x in a + b, x2 in f(x) | P(x,x2)} = {e(y,y2): y in b + a, y2 in f(y) | P(y,y2)};",
--			"{e(x): x •incin (a + b) | P(x)} = {e(x): x in pow(b + a) | P(x)};",
--			"{e(x): x •incin (a + b) | P(x)} = {e(x): x in pow(b + a)};",
--			"{e(x): x •incin (a + b) | true} = {e(x): x in pow(b + a)};",
--			"{e(x): x •incin (a * b) | true} = {e(x): x in pow(b * a)};",
--			"{x: x •incin (a * b)} = {x in pow(b * a) | true};",
--			"{x in pow(b * a) | true} = {x: x •incin (a * b)};",
--			"{x in pow(b * a + d * c) | true} = {x: x •incin (a * b + c * d)};",
--			"{e(x): x in a | P(x)} + {e(x): x in a | Q(x)} = {e(x): x in a | Q(x) or P(x)};",
--			"{e(x): x in a | P(x)} + {e(x): x in b | P(x)} = {e(x): x in a + b  | P(x)};",
--			"Un(a + b) = c +  d;",
--			"(EXISTS x in a + b | P(x)) •eq (EXISTS x in b + a | P(x));",
--			"((EXISTS x in a | P(x)) or (EXISTS x in b | P(x))) •eq (EXISTS x in b + a | P(x));",
--			"((EXISTS x in a | P(x)) or (EXISTS x in a | Q(x))) •eq (EXISTS x in a | P(x) or Q(x));",
--			"((FORALL x in a | P(x)) and (FORALL x in a | Q(x))) •eq (FORALL x in a | P(x) and Q(x));",
--			"((FORALL x in a | P(x)) and (FORALL x in b | P(x))) •eq (FORALL x in b + a | P(x));",
--			"Un(Un(a + b)) = Un(Un(a) + Un(b));",
--			"pow(Un(a)) +  pow(Un(b)) incs pow(Un(a + b));",
--			"{e(x): x in a + b | P(x)} = {ee(x): x in b + a | P(x)};",
--			"{g(x) * h(x): x in pow(b * a + d * c) | true} = {h(x) * g(x): x •incin (a * b + c * d)};",
--			"{e(x): x •incin (a + b) | P(x)} incs {e(x): x in pow(b) | P(x)};",
--			"{e(x): x •incin (a + b) | P(x)} incs {e(x): x in pow(c) | P(x)};",
--			"Un((a + b) + c) incs Un(c) + Un(b);",
--			"(Un(c) + Un(b)) •incin Un((a + b) + c);",
--			"{e(x): x in (a + (b + c)) | P(x)} incs {e(x): x in c | P(x)} + {e(x): x in b | P(x)};",
--			"{e(x): x in (a + (b + c)) | P(x)} incs {e(x): x in a | P(x)} + ({e(x): x in b | P(x)} + {e(x): x in c | P(x)});",
--			"{e(x): x in (b + (a + c)) | P(x)} incs {e(x): x in c | P(x)} + {e(x): x in b | P(x)};",
--			"(a or b) •imp c;",
--			"(a and b) •imp c;",
--			"(a and b) •imp a;",
--			"if (a and b) •imp a then c else d end if •imp c;",
--			"if (a and b) •imp a then c else d end if •imp d;",
--			"if a = a then c else d end if •imp c;",
--			"if a = a then c else d end if •imp d;",
--			"(a and b) •imp a;",
--			"((a and b) or (c and d)) •imp (a or c);",
--			"((a and b) and (c and d)) •imp (a and c);",
--			"((not(a and c)) •imp (not((a and b) and (c and d))));",
--			"(FORALL x in b + a | P(x)) •imp (FORALL x in a | P(x));",
--			"(FORALL x in b + a | P(x) and Q(x)) •imp (FORALL x in a | P(x));",
--			"(FORALL x in b + a | P(x)) •imp (FORALL x in a | P(x) or Q(x));",
--			"(EXISTS x in a | P(x)) •imp (EXISTS x in b + a | P(x) or Q(x));",
--			"(EXISTS x in b + a | P(x) or Q(x)) •imp ((EXISTS x in b | P(x) or Q(x)) or (EXISTS x in a | P(x) or Q(x)));",
--			"(EXISTS x in a | P(x) or Q(x)) •imp ((EXISTS x in a | P(x)) or (EXISTS x in a | Q(x)));",
--			"((EXISTS x in b | P(x) or Q(x)) or (EXISTS x in a | P(x) or Q(x))) •imp (EXISTS x in b + a | P(x) or Q(x));",
--			"((EXISTS x in a | P(x)) or (EXISTS x in a | Q(x))) •imp (EXISTS x in a | P(x) or Q(x));",
--			"(FORALL x in b + a | P(x) and Q(x)) •imp ((FORALL x in b | P(x) and Q(x)) and (FORALL x in a | P(x) and Q(x)));",
--			"(FORALL x in a | P(x) and Q(x)) •imp ((FORALL x in a | P(x)) and (FORALL x in a | Q(x)));",
--			"((FORALL x in b | P(x) and Q(x)) and (FORALL x in a | P(x) and Q(x))) •imp (FORALL x in b + a | P(x) and Q(x));",
--			"((FORALL x in a | P(x)) and (FORALL x in a | Q(x))) •imp (FORALL x in a | P(x) and Q(x));",
--			"{cdr(u): u in {[x,y],[zz,w]} | car(u) in {x}} = {cdr(u): u in {[x,y]} | car(u) in {x}} + {cdr(u): u in {[zz,w]} | car(u) in {x}};",
--			"{e(x,y): x in g, y in (f + ff) | P(x,y)} = {e(x,y): x in g, y in f | P(x,y)} +  {e(x,y): x in g, y in ff | P(x,y)};",
--			"{if x = a then b elseif x = b then a else x end if: x in s} incs {if x = a then b elseif x = b then a else x end if: x in {a,b,c}};",
--			"{E(X,Y): X in G, Y in F | P(X,Y)} = {E(X,Y): X in G, Y in F | P(X,Y)};",
--			"({[X,Y]: X in A, Y in C} + {[X,Y]: X in B, Y in C}) = ({[X,Y]: X in A, Y in C} + {[X,Y]: X in B, Y in C});",
--			"{[x,y]: x in a, y in c} + {[x,y]: x in b, y in c} = {[x,y]: x in a + b, y in c};",
--			"(s - {orden(y): y in o2 + a}) •incin (s - {orden(y): y in o2});",
--			"{[[car(u),car(cdr(u))],cdr(cdr(u))]: u in {[x,[y,0]]: x in n, y in m} + {[x,[y,1]]: x in n, y in k}} =  {[[car(u),car(cdr(u))],cdr(cdr(u))]: u in {[x,[y,0]]: x in n, y in m}} + {[[car(u),car(cdr(u))],cdr(cdr(u))]: u in {[x,[y,1]]: x in n, y in k}};",
--			"{e(u): u in {f(x,y): x in n, y in m} + {f(x,y): x in n, y in k}} =  {e(u): u in {f(x,y): x in n, y in m}} + {e(u): u in {f(x,y): x in n, y in k}};",
--			"{cdr(u): u in {[x,y]} + {[zz,w]} | car(u) in {x}} =    	{cdr(u): u in {[x,y]} | car(u) in {x}} + {cdr(u): u in {[zz,w]} | car(u) in {x}};",
--			"Finite(a + b) •imp Finite(a);",
--			"Finite(#(a + b)) •imp Finite(#a);",
--			"Is_map(a + b) •imp Is_map(a);",
--			"One_1_map(a + b) •imp One_1_map(a);",
			"a = a;"];
	
	for form in forms loop
		print(); 
--		print("Tree returned: ",monotone_infer(parze_expr(form)(2)));
		print(unparse(monotone_infer(parze_expr(form)(2))));
	end loop; 
	
end test_monotone_infer;

procedure test_replace_fcn_symbol; 	 		-- test of the replace_fcn_symbol procedure
	
	quads := [["hsko(s,t)~[s];","H_THRYVAR","U,V","hsko(u,v)~[u];"],
		["(h_thryvar(s,t) /= f({g(h_thryvar(y,t),y,s,t): y •incin s | (y /= s) & P(h_thryvar(y,t),y,s,t)},s,t)) & (hsko(s,t)~[s] /= f({g(hsko(y,t)~[y],y,s,t): y •incin s | (y /= s) & P(hsko(y,t)~[y],y,s,t)},s,t));","H_THRYVAR","U,V","hsko(u,v)~[u];"],
--	 ["pow(Un(a));","ast_pow","X","{u: u •incin x};"],  
--				["pow(Un(a));","UN","X","{u: v in x, u in v};"],
--				["Un(Un(a));","UN","X","{u: v in x, u in v};"],
--				["if Un(a) /= 0 then pow(Un(a)) else Un(Un(a)) end if ;","UN","X","{u: v in x, u in v};"],
--				["range(Un(a));","ast_range","X","{cdr(u): u in x};"],
--				["range(Un(range(a)));","ast_range","X","{cdr(u): u in x};"],
--				["{Un(a),Un(Un(a))};","UN","X","{u: v in x, u in v};"],
--				["{Un(a),Un(b)};","UN","X","{u: v in x, u in v};"],
--				["[Un(a),Un(Un(a))];","UN","X","{u: v in x, u in v};"],
--				["{Un(a): a in pow(Un(b)) | Un(Un(a)) = 0};","UN","X","{u: v in x, u in v};"],
--				["{a in pow(Un(b)) | Un(Un(a)) = 0};","UN","X","{u: v in x, u in v};"],
--				["(FORALL a in pow(Un(b)) | Un(Un(a)) = 0);","UN","X","{u: v in x, u in v};"],
--				["(EXISTS a in pow(Un(b)) | Un(Un(a)) = 0) or (FORALL a in pow(Un(b)) | Un(Un(a)) = 0);","UN","X","{u: v in x, u in v};"],
--				["a •MINUS b;","DOT_MINUS","X,Y","#(X - Y);"],
--				["f~[b];","TILDE_","F,X","cdr(arb({y: y in F •ON {X}}));"],
--			["arb({{c},{{c},{{d},d}}}) = arb([c,d]);","ast_enum_tup","X,Y","{{X},{{X},{{Y},Y}}};"],
--			["[c,d];","ast_enum_tup","X,Y","{{X},{{X},{{Y},Y}}};"],
--			["[Un(c),Un(d)];","UN","X","{u: v in x,u in v};"],
			["Un(f(Un(a)));","UN","X","{u: v in x,u in v};"]];

	for [form,symb,symbargs,symbdef] in quads loop
		print(); 
		print(unparse(replace_fcn_symbol(parze_expr(form)(2),symb,breakup(symbargs,","),parze_expr(symbdef)(2))));
	end loop; 
	
end test_replace_fcn_symbol;

procedure replace_fcn_symbol(expn,symbol,symbvars,symbdef);
		-- at each occurrence of a symbol in expn, finds the arguments of symbol,
		-- and substitutes them in symbdef for the indicated free variables of symbdef
		-- replacing the symbol occurrence by this substituted form 
		-- but if symbvars = OM, in which case the definition should a simple string, occurrences of
		-- 'symbol' are replaced by occurrences of 'symbdef'

		if is_string(expn) then return if expn = symbol then symbdef else expn end if; end if; 
				-- conditionally replace variables found at bottom level
--print("replace_fcn_symbol: ",expn);		
		[n1,n2,n3,n4] := expn;			-- otherwise unpack top level of tree
		
		case n1
			
			when "ast_of" => 			-- function application 
				
				arglist := [if j = 1 then arg else replace_fcn_symbol(arg,symbol,symbvars,symbdef) end if: arg = n3(j)];
							-- make substitutions within them 

				if n2 = symbol then 		-- we have occurrence of a significant symbol
--print("
replace_fcn_symbol: symbol is: ",symbol," symbvars: ",symbvars?"OM"," symbol definition is: ",unicode_unparse(symbdef)," replacement takes place in expression: ",unicode_unparse(expn)," node tag ",expn(1)," opname = symbol",expn(2) = symbol,"
");
					
--print("
now testing symbvars: ",symbvars = OM," ",symbvars?"UNDEfined");
					if symbvars = OM then 	-- just replace 'symbol' by 'symbdef' and keep the same argument list
--print("
returning substituted: ",unicode_unparse([n1,symbdef,arglist]));
						return [n1,symbdef,arglist]; 
					end if;
					
					if n3 = OM or #symbvars /= #(n3(2..)) then	
--print("[n1,n2,n3,n4]: ",[n1,n2,n3,n4]," ",symbvars);				
							-- mismatch between number of args and number of parameters supplied
						mismatched_args := true;			-- keep record of the offense
						mismatched_symbvars := symbvars;
						mismatched_expn := unparse(expn);
						return expn;			-- do no substitutions
					end if;
							
			
					replacement_map := {[symbvar,arglist(j + 1)?symbvar]: symbvar = symbvars(j)};
							-- map each definition parameter into the argument which replaces it
					return substitute(symbdef,replacement_map);
							-- substitute these replacements within the symbol definition and return the result

				end if;
				
				return [n1,n2,arglist]; 			-- otherwise just return the symbol with the substituted arguments
				
			when "ast_genset" => 		-- setformer 

				subst_n2 := replace_fcn_symbol(n2,symbol,symbvars,symbdef);
				subst_iter := [if j = 1 then iter else replace_fcn_symbol(iter,symbol,symbvars,symbdef) end if: iter = n3(j)];
				subst_cond := if n4 = "st_null" then n4 else replace_fcn_symbol(n4,symbol,symbvars,symbdef) end if;
				return [n1,subst_n2,subst_iter,subst_cond];

			when "ast_genset_no_expr","ast_forall","ast_exists" => 	-- setformer, no expression, quantifier 

				subst_iter := [if j = 1 then iter else replace_fcn_symbol(iter,symbol,symbvars,symbdef) end if: iter = n2(j)];
				subst_cond := if n3 = "st_null" then n4 else replace_fcn_symbol(n3,symbol,symbvars,symbdef) end if;
				return [n1,subst_iter,subst_cond];
--
--			when "ast_forall" => 		-- universal quantifier 
--print(expn);			
--			when "ast_exists" => 		-- existential quantifier
--print(expn);						
			when "ast_enum_set" => 		-- enumerated set 
			
				return [n1] + [replace_fcn_symbol(elt,symbol,symbvars,symbdef): elt in expn(2..)];

			when "ast_enum_tup" => 		-- enumerated tuple 
				
				arglist := [replace_fcn_symbol(elt,symbol,symbvars,symbdef): elt in expn(2..)];

				if case_change(n1,"lu") = case_change(symbol,"lu") then		-- if the tuple iself is being expanded then
					replacement_map := {[symbvar,arglist(j)?symbvar]: symbvar = symbvars(j)};
								-- map each definition parameter into the argument which replaces it
					return substitute(symbdef,replacement_map);
								-- substitute these replacements within the symbol definition and return the result
				end if;
				
				return [n1] + arglist;		-- otherwise just return the tuple arguments, as a tuple
		
			when "#","ast_pow","ast_range","ast_domain","ast_arb" => 		-- builtin monadics
				
				substarg := replace_fcn_symbol(n2,symbol,symbvars,symbdef);
				
				if n1 = symbol then 		-- we have occurrence of a significant symbol
					
					replacement_map := {[symbvar,substarg?symbvar]: symbvar = symbvars(j)};
							-- map each definition parameter into the argument which replaces it

					return substitute(symbdef,replacement_map);
							-- substitute these replacements within the symbol definition and return the result

				end if;
				
				return [n1,substarg]; 			-- otherwise just return the symbol with the substituted arguments
			
			when "TILDE_" => 		-- function application (has special syntax)
--print("expn: ",expn);					
					substarg := replace_fcn_symbol(n2,symbol,symbvars,symbdef);
					
					substarg2 := replace_fcn_symbol(n3(2),symbol,symbvars,symbdef);		-- throw away nonstandard square brackets

--print("replacement_map: ",replacement_map," result: ",unparse(substitute(symbdef,replacement_map))," substarg: ",unparse(substarg)," substarg2: ",unparse(substarg2)," symbdef: ",unparse(symbdef));
					if n1 /= symbol then return ["TILDE_",substarg,["ast_enum_tup",substarg2]]; end if;
					
					return ["ast_of", "CDR", ["ast_list", ["ast_arb", ["DOT_ON", substarg, ["ast_enum_set", substarg2]]]]];
							-- combine these replacements as a tilde and return the result
						
			otherwise =>
			
				if n1 = symbol then 		-- defined binary operator
				
					substarg := replace_fcn_symbol(n2,symbol,symbvars,symbdef);
					substarg2 :=if n3 /= OM then replace_fcn_symbol(n3,symbol,symbvars,symbdef) else OM end if;
						
					if n1 = symbol then 		-- we have occurrence of a significant symbol
						
						replacement_map := {[symbvar,if j = 1 then substarg else substarg2 end if?symbvar]: symbvar = symbvars(j)};
								-- map each definition parameter into the argument which replaces it
	
						return substitute(symbdef,replacement_map);
								-- substitute these replacements within the symbol definition and return the result
	
					end if;
					
					return [n1,substarg,substarg2]; 			-- otherwise just return the symbol with the substituted arguments

				else 						-- some other operator
			
					substarg :=if n2 /= OM then replace_fcn_symbol(n2,symbol,symbvars,symbdef) else OM end if;
					substarg2 :=if n3 /= OM then replace_fcn_symbol(n3,symbol,symbvars,symbdef) else OM end if;
					substarg3 :=if n4 /= OM then replace_fcn_symbol(n4,symbol,symbvars,symbdef) else OM end if;
						
					return [n1,substarg,substarg2,substarg3];
			
				end if;

		end case;
		
end replace_fcn_symbol;

procedure find_setformers_and_quants(tree);		-- finds the setformer and quantifier nodes in a tree, and returns them
												-- as a list
	
	var setformers_and_quants := [];	-- the list to be returned
		
	find_setformers_and_quants_in(tree);		-- call the recursive workhorse
	
	return setformers_and_quants;					-- return the map produced

	procedure find_setformers_and_quants_in(tree);	-- internal recursive workhorse
		
		if is_string(tree) then return; end if;
--print("find_setformers_and_quants_in::: ",unparse(tree));		
		[n1,n2,n3] := tree;			-- break node into operands and operator: generally infix (but not always)

		if (ah := abbreviated_headers(n1)) in {"{}","{/}","EX","ALL"} then 
			setformers_and_quants with:= tree; 
		end if;
		
		case ah 
	
			when "if" => find_setformers_and_quants_in(n2); find_setformers_and_quants_in(n3); find_setformers_and_quants_in(tree(4));
						-- if expression

			when "and","or","==","=",":=","incs","incin","imp","+","*","-" ,"in","notin","/=","/==","@" => 	-- various binaries
				
					find_setformers_and_quants_in(n2); find_setformers_and_quants_in(n3); 
					
			when "{-}" => for nj in tree(2..) loop find_setformers_and_quants_in(nj); end loop;	-- enumerated set

			when "[-]" => find_setformers_and_quants_in(n2); if n3 /= OM then find_setformers_and_quants_in(n3); end if;
					 		-- ordered pair, or singleton for tilde pplication
	
			when "domain","range","not","arb" => find_setformers_and_quants_in(n2);		-- built-in monadics
			
			when "EX","ALL","{/}" =>	-- quant or setformer, no expr; look for sets in the iterator list bounds and in the condition
				
				find_setformers_and_quants_in(n2); find_setformers_and_quants_in(n3); 
				
			when "{}" =>	-- setformer; look for sets in the lead expression, the iterator list bounds and in the condition

				find_setformers_and_quants_in(n2); find_setformers_and_quants_in(n3); find_setformers_and_quants_in(tree(4));

			when "[]" =>	-- list, e.g. of arguments; search for sets in the iterator bounds

				for iter in tree(2..) | not (is_string(iter) or is_string(bound := iter(3))) loop 
					find_setformers_and_quants_in(bound);
				end loop;

			when "()" => 			-- function and predicate application; just search all the arguments
					
				for nj in tree(3)(2..) loop find_setformers_and_quants_in(nj); end loop;

			otherwise => for nj in tree(2..) loop find_setformers_and_quants_in(nj); end loop;	
						-- other operators; process all arguments
		
		end case;
			
	end find_setformers_and_quants_in;

end find_setformers_and_quants;

--			*********************************************************************************
--			********************************* Obsolete code *********************************
--			*********************************************************************************
	
	procedure monotone_inference(node1,node2); 	-- calculates conditions for value defined  by node 1 to include value defined by node 2
		-- We begin by standardizing the two  nodes so as to  bring them into the closest feasible correspondence. 
		-- Then  we descend the two  trees in parallel, looking for differences in the parse trees, and collecting bound variables.
		-- A difference can be found either at a common functional or predicate node. A dummy variable is assigned to each difference,
		-- and we return the set of quintuples  [subtree1,subtree2,bound_variables,dummy_variable,is_pred] and the common reduced formula in which
		-- all differences have been replaced by the generated dummy variables. This common formula is then  surveyed for monotone dependencies
		-- using 'blob_to_monotone'. Then the following deductions are possible: (a) if there is just one  difference under no bound variables, 
		-- and the expression is additive, then we can  deduce an inequality between sums. (b) if there is any differnce at a position depending
		-- in a mixed  way on the variable inserted at that position,  then no deduction is possible. (c) Otherwise we can deduce either 
		-- of two inclusions, from corrresponnding inclusions for the differences,  with reversals in the difference positions which are decreasing_kind.  

		difference_quintuples := {};			-- set of difference quintuples
		monot_var_ctr := 0;						-- counter used for generation of variables

--		node1 := standardize_bound_vars(node1); node2 := standardize_bound_vars(node2);		-- standardize the bound variables in both formulae
		
		res := monotone_inference_in(node1,node2,{},true); 	-- workhorse; start at predicate level with no bound variables
print("difference_quintuples: ",difference_quintuples);		
		return res;
		
	end monotone_inference;

	procedure monotone_inference_in(tree1,tree2,bound_vars_with_ranges,is_pred); 	-- workhorse for 'monotone_inference'

--print("monotone_inference_in: ",unparse(tree1)," ",unparse(tree2)," bound_vars_with_ranges = ",bound_vars_with_ranges," is_pred = ",is_pred);

		if is_string(tree1) or is_string(tree2) then 		-- a variable confronts a subexpression
		
			if tree1 = tree2 then return tree1; end if;			-- no difference in bottom-level leaves; just return

			difference_quintuples with := [tree1,tree2,bound_vars_with_ranges,newvar := "mv_" + str(monot_var_ctr +:= 1),is_pred]; 
			return newvar;		-- return the representing variable
		
		end if;		-- otherwise the nodes differ in their principal operator; collect the difference
		
		[n1_1,n2_1,n3_1] := tree1; [n1_2,n2_2,n3_2] := tree2; 			-- get the likely parts of the two clauses
		
		if n1_1 /= n1_2 then			-- the nodes are not of the same kind, so return a difference variable
		
			difference_quintuples with:= [tree1,tree2,bound_vars_with_ranges,newvar := "mv_" + str(monot_var_ctr +:= 1),is_pred];
			return newvar;		-- return the representing variable

		end if; 						-- otherwise two subexpressions confront each other
		
			-- othewise the nodes are of the same kind,  so go on to look for differences in their arguments
	
		case (ah := abbreviated_headers(n1_1))

			when "and","or","==","/==","imp","null" =>				-- boolean operations
						 -- ordinary operators with a fixed number of arguments; look for differences in their arguments

					res_1 := monotone_inference_in(n2_1,n2_2,bound_vars_with_ranges,true);		-- find subpart differences
					res_2 := monotone_inference_in(n3_1,n3_2,bound_vars_with_ranges,true);		-- subparts are predicates 

					return [n1_1,res_1,res_2];		-- return the condensed tree, having found differences

			when "+","-","{.}","in","notin","=","/=","incs","incin","*","[-]" =>			
						 -- ordinary operators with a fixed number of arguments; look for differences in their arguments
						-- ast_enum_tup should be ordered pair only; singleton for application operator is handled elsewhere
--print("[n1_1,n2_1,n3_1]: ",[n1_1,n2_1,n3_1]," ",[n1_2,n2_2,n3_2]);	
					res_1 := monotone_inference_in(n2_1,n2_2,bound_vars_with_ranges,false);		-- find subpart differences
					res_2 := monotone_inference_in(n3_1,n3_2,bound_vars_with_ranges,false);		-- subparts are terms 

					return [n1_1,res_1,res_2];		-- return the condensed tree, having found differences

			when "->" =>			-- "->" is the functional application operator "TILDE_"

					res_1 := monotone_inference_in(n2_1,n2_2,bound_vars_with_ranges,false); 		-- subparts are expressions 
					res_2 := monotone_inference_in(n3_1(2),n3_2(2),bound_vars_with_ranges,false); 	-- syntax is ["TILDE_", "F", ["ast_enum_tup", "X"]]

					return [n1_1,res_1,["ast_enum_tup",res_2]];		-- return the condensed tree, having found differences

			when "not" =>

					res_1 := monotone_inference_in(n2_1,n2_2,bound_vars_with_ranges,true); 		-- subparts are predicates
					return [n1_1,res_1];		-- return the condensed tree, having found differences

			when "[]" =>			-- ast_list
					
					print("****** shouldnt happen - monotone_inference_in: ",ah);
					
			when "{-}" => 				-- enumerated sets. here we try to improve the agreement by sorting the elements

				if #(args1 := tree1(2..)) /= #(args2 := tree2(2..)) then 		-- the nodes differ in their number of arguments; treat as different
					difference_quintuples with:= [tree1,tree2,bound_vars_with_ranges,newvar := "mv_" + str(monot_var_ctr +:= 1),is_pred];
					return newvar;		-- return the representing variable
				end if;				-- otherwise blob the elements and sort them to bring into the order most likely to agree
				
				args1_with_blobs := [[blob_to_string(a1,[],name_ctr),a1]: a1 in args1];		-- we leave out the bound variables, since these will be common to both sets
				args2_with_blobs := [[blob_to_string(a2,[],name_ctr),a2]: a2 in args2];
				args1_sorted := [y: [x,y] in merge_sort(args1_with_blobs)];
				args2_sorted := [y: [x,y] in merge_sort(args2_with_blobs)];
--print("args1_with_blobs: ",args1_sorted," ",args2_sorted);stop;				

											-- look for differences in their arguments
				if args1_sorted /= args2_sorted then 
					difference_quintuples with:= [tree1,tree2,bound_vars_with_ranges,newvar := "mv_" + str(monot_var_ctr +:= 1),is_pred];
					return newvar;		-- return the representing variable
				end if;

				return tree1;		-- otherise we have fond identity, so return the common tree

			when "()" => 				-- this is the case of functional and predicate application; the second variable is a reserved symbol, not a set
--print("function trees: ",tree1," ",tree2);					

				if tree1 /= tree2 then 		-- the nodes differ 
					difference_quintuples with:= [tree1,tree2,bound_vars_with_ranges,newvar := "mv_" + str(monot_var_ctr +:= 1),is_pred];
					return newvar;		-- return the representing variable
				end if;				-- otherwise blob the elements and sort them to bring into the order most likely to agree

				return tree1;		-- otherise we have fond identity, so return the common tree

			when "{}" => 		-- setformer with expression; here there is a fourth argument, namely the predicate (this may be "ast_null", represetnting 'true')
					-- here we are comparing two setformers having structures like {e1(x,y,z): x in s1, y in t1(x), z in w1(x,y) | A(x,y,z)}.
					-- if the iterator lists which appear are of the same length and have corresponding structures throughout, and have identical expressions,
					-- then we look for differences in the restrictions of the bound variables, and also for differences in the predicates
					
					-- otherwise we treat the two setformers as different  
				
				body_1 := n2_1; body_2 := n2_2; 										-- get the two expressions being accumulated
				list_of_iters_1 := orig_list_of_iters_1 := n3_1(2..); list_of_iters_2 := orig_list_of_iters_2 := n3_2(2..); 	-- get the two lists of iterators
						-- the iter_list syntax is exemplified by ["ast_iter_list", ["ast_in", "X", "A"], ["ast_incs", "Y", "B"],...]
				cond_1 := tree1(4); cond_2 := tree2(4); 					-- get the two conditions
				if cond_1 = ["ast_null"] then cond_1 := "TRUE"; end if;		-- replace empty conditions with "TRUE"
				if cond_2 = ["ast_null"] then cond_2 := "TRUE"; end if;
				
				if body_1 /= body_2 then			-- iterator expressions differ; so treat as diferent
					difference_quintuples with:= [tree1,tree2,bound_vars_with_ranges,newvar := "mv_" + str(monot_var_ctr +:= 1),is_pred];
					return newvar;		-- return the representing variable
				end if;

				if (cl := #list_of_iters_1) /= #list_of_iters_2 then 		-- the iterators are of different lengths, so treat s different
					difference_quintuples with:= [tree1,tree2,bound_vars_with_ranges,newvar := "mv_" + str(monot_var_ctr +:= 1),is_pred];
					return newvar;		-- return the representing variable
				end if;			-- otherise check that the iterators are all  of the same types

--					if not verify_equality_in(body_1,body_2,bound_vars_with_ranges + list_of_iters_1,false) then -- the bodies are not identical
--						return false;				-- verification by examination of subparts succeeds		
--					end if;				-- otherwise we must check to see if the iterator lists are equivalent
--
--					if not verify_equality_in(cond_1,cond_2,bound_vars_with_ranges + list_of_iters_1,true) then -- the conditions are not identical
--						return false;				-- verification by examination of subparts succeeds		
--					end if;				-- otherwise we must check to see if the iterator lists are equivalent
--				
--				succeeds := true;		-- see if the following loop succeeds
----print("body_1,body_2:: ",body_1," ",body_2," ",list_of_iters_1," ",list_of_iters_2);
--				for k in [1..cl] loop
--					[-,-,restr_set_1] := list_of_iters_1(k); [-,-,restr_set_2] := list_of_iters_2(k); 		-- get the restriction sets
----print("restr_set_1,restr_set_2:: ",restr_set_1," ",restr_set_2," ",bound_vars_with_ranges + list_of_iters_1(1..k - 1)," ");
--					if not verify_equality_in(restr_set_1,restr_set_2,bound_vars_with_ranges + list_of_iters_1(1..k - 1),false) then
--						succeeds := false; exit;
--					end if;
--
--				end loop;
--				
--				if succeeds then return true; end if;		-- otherwise not all of the restriction sets are eqivalent, so we 
--															-- go on to see if identity can be verified 'directly' in some way 
--		
--				for j in [1..cl] loop
--
--					if j = cl then				-- there are no suffixed qualifiers
--
--						required_implication := ["ast_forall",["ast_iter_list"] + orig_list_of_iters_1,["DOT_EQ",cond_1,cond_2]];
--						required_identity := ["ast_forall",["ast_iter_list"] + orig_list_of_iters_1,["ast_eq",body_1,body_2]];
--
--						if not check_in_context(required_implication,bound_vars_with_ranges) then continue; end if;
--						if not check_in_context(required_identity,bound_vars_with_ranges) then continue; end if;
--
--						succeeds := true;		-- see if the following loop succeeds
--						for k in [1..cl] loop
--
--							[-,-,restr_set_1] := list_of_iters_1(k); [-,-,restr_set_2] := list_of_iters_2(k); 		-- get the restriction sets
--
--							if not verify_equality_in(restr_set_1,restr_set_2,bound_vars_with_ranges + list_of_iters_1(1..k - 1),false) then
--								succeeds := false; exit;
--							end if;
--
--						end loop;
--
--						if succeeds then return true; end if;			-- otherwise keep looing to try to find a verification
--						
--					else				-- there are suffixed qualifiers; use these in setformers
--
--						set_1 := ["ast_genset",body_1,["ast_iter_list"] + orig_list_of_iters_1(j + 1..),cond_1];
--						set_2 := ["ast_genset",body_2,["ast_iter_list"] + orig_list_of_iters_2(j + 1..),cond_2];
--						required_identity := ["ast_forall",["ast_iter_list"] + orig_list_of_iters_1(1..j),["ast_eq",set_1,set_2]];
--						
--						if not check_in_context(required_identity,bound_vars_with_ranges) then continue; end if;
--
--						succeeds := true;		-- see if the following loop succeeds
--						for k in [1..j] loop
--
--							[-,-,restr_set_1] := list_of_iters_1(k); [-,-,restr_set_2] := list_of_iters_2(k); 		-- get the restriction sets
--
--							if not verify_equality_in(restr_set_1,restr_set_2,bound_vars_with_ranges + list_of_iters_1(1..k - 1),false) then
--								succeeds := false; exit;
--							end if;
--
--						end loop;
--
--						if succeeds then return true; end if;			-- otherwise keep looping to try to find a verification
--
--					end if;
--
--				end loop;
--					
--					return false;			-- if the iterator sequences don't agree, we give up in this case, allowing proof to proceed more manually,
--				
--				end if;
--
--				when "{/}" => 							-- setformer without expression
--														-- see comment at start of preceding case
--						
--					list_of_iters_1 := n2_1(2..); list_of_iters_2 := n2_2(2..); 			-- get the two lists of iterators
--					cond_1 := n3_1; cond_2 := n3_2; 					-- get the two conditions
--					[cl,list_of_iters_1,list_of_iters_2,cond_1,cond_2] := common_iter_len(list_of_iters_1,list_of_iters_2,cond_1,cond_2);
--
--					if cl = #list_of_iters_1 and cl = #list_of_iters_2 then 		-- the iterators agree out to their full lengths; look for differences in bodies
--
-- 						if not verify_equality_in(cond_1,cond_2,bound_vars_with_ranges + list_of_iters_1,true) then -- the conditions are not identical
-- 							return false;				-- verification by examination of subparts succeeds		
-- 						end if;				-- otherwise we must check to see if the iterator lists are equivalent
--						
----print("cond_1,cond_2:: ",cond_1," ",cond_2," ",list_of_iters_1," ",list_of_iters_2);
--						[-,-,restr_set_1] := list_of_iters_1(1); [-,-,restr_set_2] := list_of_iters_2(1); 		-- get the restriction sets
--
--						if not verify_equality_in(restr_set_1,restr_set_2,bound_vars_with_ranges,false) then
--							return false; 
--						end if;
--					
--					end if;
--						
--					return true;		-- if all tests are passed, we return true
--					 	
--				when "ALL","EX" => 					-- universal and existential quantifiers
--					
--					lead_quantifier := if ah = "ALL" then "ast_forall" else "ast_exists" end if;
--
--					[list_of_iters_1,body_1] := flatten_universal(tree1); [list_of_iters_2,body_2] := flatten_universal(tree2);
--									-- find the full flattened lists of prefixed universal quantifiers in the two trees
--									-- now find the iterator portions which are of the same types. That is, the operators "ast_in" or "DOT_INCIN"
--									-- must be the same, and for the "ast_in" case, either both ranges or none must be OM 
--					
--					[cl,list_of_iters_1,list_of_iters_2,body_1,body_2] := common_iter_len(list_of_iters_1,list_of_iters_2,body_1,body_2);
--										-- find the length of the iterator parts which are common
--
--					if cl = #list_of_iters_1 and cl = #list_of_iters_2 then 		-- the iterators agree out to their full lengths; look for differences in bodies
--
-- 						if not verify_equality_in(body_1,body_2,bound_vars_with_ranges + list_of_iters_1,true) then -- the bodies are not identical
-- 							return false;				-- verification by examination of subparts succeeds		
-- 						end if;				-- otherwise we must check to see if the iterator lists are equivalent
--						
--						succeeds := true;		-- see if the following loop succeeds
----print("body_1,body_2:: ",body_1," ",body_2," ",list_of_iters_1," ",list_of_iters_2);
--						for k in [1..cl] loop
--							[-,-,restr_set_1] := list_of_iters_1(k); [-,-,restr_set_2] := list_of_iters_2(k); 		-- get the restriction sets
----print("restr_set_1,restr_set_2:: ",restr_set_1," ",restr_set_2,`" ",bound_vars_with_ranges + list_of_iters_1(1..k - 1)," ");
--							if not verify_equality_in(restr_set_1,restr_set_2,bound_vars_with_ranges + list_of_iters_1(1..k - 1),false) then
--								succeeds := false; exit;
--							end if;
--
--						end loop;
--						
--						if succeeds then return true; end if;		-- otherwise not all of the restriction sets are eqivalent, so we 
--																	-- go on to see if identity can be verified 'directly' in some way 
--				
--					elseif cl = #list_of_iters_1 then 		-- the full first iterator agrees with a prefix of the second iterator
--						
--						remaining_iters := list_of_iters_2(cl + 1..);			-- find the remaining iters in the first group
--						body_2 := ["ast_forall",["ast_iter_list"] + remaining_iters,body_2];			-- restore the remaining universals to the second clause
--
--					elseif cl = #list_of_iters_2 then 		-- the full second iterator agrees with a prefix of the second iterator; insist on an identity
--						
--						remaining_iters := list_of_iters_1(cl + 1..);			-- find the remaining iters in the second group
--						body_1 := ["ast_forall",["ast_iter_list"] + remaining_iters,body_1];			-- restore the remaining universals to the first clause
--						
--					else 		-- only portions of the iterators agree; insist on an identity of the remaining parts
--						
--						remaining_iters1 := list_of_iters_1(cl + 1..);			-- find the remaining iters in the first group
--						body_1 := ["ast_forall",["ast_iter_list"] + remaining_iters1,body_1];			-- restore the remaining universals to the first clause
--						
--						remaining_iters2 := list_of_iters_2(cl + 1..);			-- find the remaining iters in the second group
--						body_2 := ["ast_forall",["ast_iter_list"] + remaining_iters2,body_2];			-- restore the remaining universals to the second clause
--					
--					end if;
--							-- here we attempt 'direct', rather than 'subpart' verifiction, by trying identities 
--							-- prefixed by the full list of quantifiers and by any of its initial subparts, any one of which might be relevant
----print("try direct verification: cl = ",cl," lead_quantifier = ",lead_quantifier," list_of_iters_1 = ",list_of_iters_1," list_of_iters_2 = ",list_of_iters_2," body_1 = ",body_1," body_2 = ",body_2);						
--					for j in [cl + 1,cl..1] loop		-- try clauses with varying numbers of prefixed quantifiers
--
--						qbody_1 := if j > cl then body_1 else [lead_quantifier,["ast_iter_list"] + list_of_iters_1(j..),body_1] end if;
--												-- prefix the bodies with varying numbers of quantifiers
--						qbody_2 := if j > cl then body_2 else [lead_quantifier,["ast_iter_list"] + list_of_iters_2(j..),body_2] end if;
--						
--						required_equivalence := ["DOT_EQ",qbody_1,qbody_2];		-- set up, and then quantify, the required equivalence
--						if j > 1 then required_equivalence := ["ast_forall",["ast_iter_list"] + list_of_iters_1(1..j - 1),required_equivalence]; end if;
--
----print("required_equivalence: ",j," ",unparse(required_equivalence));
--						if not check_in_context(required_equivalence,bound_vars_with_ranges) then continue; end if;
--										-- since the equivalence, quantified using the list of quantifiers drawn from the first formula, fails.
--										-- otherwise we must verify that the two lists of restriction sets are equivalent. 
--										-- This can be done recursively, since the restriction sets are syntacticallly 'smaller' than the
--										-- expressions in which thy appear
--
--						succeeds := true;		-- see if the following loop succeeds
--								
--						for k in [1..j - 1] loop		-- check the restriction sets in the prefixed iterators
--							[-,-,restr_set_1] := list_of_iters_1(k); [-,-,restr_set_2] := list_of_iters_2(k); 		-- get the restriction sets
--
--							if not verify_equality_in(restr_set_1,restr_set_2,bound_vars_with_ranges + list_of_iters_1(1..k - 1),false) then
--								succeeds := false; exit;
--							end if;
--																
----							req_ident := ["ast_eq",restr_set_1,restr_set_2];			-- form the body of the required identity 
----							required_equivalence := ["ast_and",required_equivalence,build_quantified_version(req_ident,list_of_iters_1(1..k - 1))];
----										-- add the necessary quantifiers and conjoin to the required equivalence
--						end loop;
--						
--						if succeeds then return true; end if;		-- since a quantified equivalence and all the restriction set equivalences have been verified
--
--					end loop;
--
--					return false;		-- if none of the quantified clauses verifies, we fail at this level
--	
--				when "itr","Etr" => 				-- iterators; here the iterators must be of the same kinds, and if one is involves a bounding set
--													-- so must the other. the bound variable names may differ; if they do we generate a common new name for both, 
--													-- and sustitute it uniformly down both trees.
--							-- find the common minimum of the iterator lists lengths
--					if #(args1 := tree1(2..)) /= #(args2 := tree2(2..)) then 		-- the nodes differ in their number of arguments; treat as different
--	
--						diffs_vars_ranges with:= [bound_vars_with_ranges,tree1,tree2];
--						return; 
--
--					end if;
--				
--					for sn = args1(j) loop verify_equality_in(sn,args2(j),bound_vars_with_ranges,is_pred); end loop;

			otherwise => print("shouldn't happen verify_equality_in: ",ah," ",node); 		-- shouldn't happen
		
		end case;

	end monotone_inference_in;

	procedure test_monotone_inference; 			-- test of the monotone_inference procedure
	print("****** TESTS OF BASIC MONOTONE INFERENCE PROC ******");
	
	--	print(); print("test_monotone_inference: ",parze_expr("{e(x): x incs a | P(x)};")); 
	--	print(); print("test_monotone_inference forall: ",parze_expr("(FORALL x incs a | P(x));"));
		
		pairs := [["x incs a;","(x + y) incs a;"],
					["x incs a or (not (y incs b));","(x + y) incs a or (not ((z + w) incs b));"]];
		
		for [hypothesis,conclusion] in pairs loop
			print(); tree1 := parze_expr(hypothesis); tree2 := parze_expr(conclusion); 
			print(monotone_inference(tree1(2),tree2(2)));
		end loop; 
		
	end test_monotone_inference;

end logic_syntax_analysis_pak2; 

--					****************************************************
--					**************** Proof by structure ****************
--					****************************************************

--	Proof by structure uses a simple auxiliary language of structure
--	descriptors to keep track of the top structural levels of sets appearing
--	in scenario proofs. Any special set defined in a scenario, for example
--	Za, the set of all non-negative integers, or Re, the set of all reals, can be used as
--	a primary structure symbol in this language. This descriptor attaches to
--	all members of the set, i.e. any integer has the descriptor Za. A
--	significant but less basic example is Si, the set of all
--	signed integers, which does not occur in our present scenario but could
--	easily be defined. Structure descriptors need not be confined to sets,
--	but can also designate classes, like the class Ord of all ordinals, the
--	class Fin of all finite sets, the class Infin of all infinite sets,
--	and the class U of all sets, etc.

--	Given any symbols S,S_1,S_2,... representing structures we can then
--	form:

--	(i) {S}: describes a set all of whose elements have the descriptor S.
--	For example,the set Za has the descriptor {Za}; the set of sets of
--	integers has the descriptor {{Za}}.

--	(ii) [S_1,S_2]: describes a pair whose components have respectively the
--	descriptors S_1 and S_2.

--	These constructions can be compounded. For example

--	(e.1) {[Za,Za]} describes a set of integer pairs (and so applies to Si,
--	the set of signed integers

--	(e.2) {[Za,U]} describes a map from integers to elements of any kind, i.e
--	describe any finite or infinite sequence.

--	A given set can have several descriptors. For example, a finite sequence
--	of signed integers has the descriptors {[Za,Si]} and Fin. Since Si itself
--	has the descriptor {[Za,Za]}, a sequence of signed integers also has the
--	descriptor {[Za,[Za,Za]]}, which in any given situation we may wish either
--	to use of ignore. Infinite sequences of signed integers have the
--	descriptors {[Za,Si]} and Infin. Real numbers in Cantor's representation
--	are equivalence classes of such sequences, and therefore have the
--	descriptors {{[Za,Si]}} and {Infin}.

--	A mechanism within the verifier should track the descriptors of
--	variables and expressions appearing in proofs whenever possible. For
--	example, a variable x known to satisfy a clause 'x in Z' has the
--	descriptor Za, a variable known to satisfy 'x in Si' has the descriptors
--	Si and [Za,Za].

--	Setformers and other basic constructors operate in a known way on the
--	structure descriptors introduced above. Suppose, for example, that s is
--	a set known to have some descriptor {D}, and that e(x) is an expression
--	having the free variable x which is known to map elements having the
--	descriptor D into elements having the descriptor D'. Then

--	 {e(x): x in s | P}

--	has the descriptor {D'}, while

--	 {[x,e(y)]: x in s, y in s | P}

--	has the descriptor {[D,D']}.

--	When a set s is known to have a descriptor {D}, any element x for which
--	'x in s' has been proved is known to have the descriptor D. If D is a
--	primitive descriptor representing a known set, this will give us the
--	assertion 'x in D', for example 'x in Z', which may be needed as an
--	auxiliary hypothesis for the application of some theorem. Similarly any
--	set s having the descriptor {[Za,Za]} is known to satisfy Is_map(s), and
--	also

--	 (FORALL x in s | car(x) in Za & cdr(x) in Za)

--	Conclusions of this kind can often result automatically. This is a
--	principal use for our system of structure descriptors.

--	Many other basic set-theoretic operations have known effects on
--	descriptors. These often follow from the definitions of the operators in
--	question. For example:

--	(1) if s has the descriptor {D}, then so does every one of its subsets,
--	and pow(s) has the descriptor {{D}}.

--	(2) if s has the descriptor {{D}}, then Un(s) has the descriptor {D}.
--	Note hat this follows automatically from the definition {x: y in s, x in
--	y} of Un(s), since the bound variable y in the iterator has the
--	descriptor {D}, so each of the x has the descriptor D, and the set as a
--	whole has the descriptor {D}.

--	(3) if s_1 and s_2 both have a descriptor {D}, then so does s_1 + s_2.

--	(4) if s_1 and s_2 both have the descriptor Fin, then so does s_1 + s_2.

--	(5) if s_1 and s_2 have descriptors {D_1} and {D_2} respectively, then
--	s_1 * s_2 has both descriptors {D_1} and {D_2}. Even if s_2 has no
--	descriptor, s_1 * s_2 and s_1 - s_2 has the descriptor {D_1}, as does
--	any set s for which an assertion s •incin s_1 has been proved.

--	(6) if s_1 has the descriptor Fin, so do s_1 * s_2 and s_1 - s_2, as
--	does any set s for which an assertion s •incin s_1 has been proved.

--	(7) if s_1 and s_2 have the descriptor Fin, so does any setformer {e: x
--	in s_1, y in s_2 | P},or any setformer {e: x in s_1 | P}

--	(8) #s always has the descriptor Card. Since the class of cardinals has
--	the descriptor {Ord}, #s also has the descriptor Ord, as does any x
--	known to be a cardinal. If s has the descriptor Fin, then #s has the
--	descriptor Za. Since Za itself has the descriptor {Fin}, #s also has the
--	descriptor Fin.

--	(9) if has the descriptor {D}, then any setformer like {x: x •incin s|
--	p} is known to have the descriptor {{D}}; this result obviously
--	generalizes.

--	(10) if sets s and t have the descriptors {D} and {D'} respectively,
--	then their Cartesian product s •PROD t has the descriptor {[D,D']}, If s
--	and t both have the descriptor Fin, so does s •PROD t.

--	(11) if s and t have descriptors {[D,D']} and {[D',D'']} respectively,
--	then s@t has the descriptor {[D,D'']}. If s and t both have the
--	descriptor Fin, so does s@t.

--	(12) if s and t have descriptors D, D' respectively, then [s,t] has the
--	descriptor [D,D']. If u has the descriptor [D,D'], then car(u) has the
--	descriptor D and cdr(u) has the descriptor D'.

--	(12) if F has the descriptor {[D,D']}, then inv(F) has the descriptor
--	{[D',D]}, and F •ON s has the descriptor {[D',D]}. if F has the
--	descriptor Fin, then inv(F) and F •ON s both have the descriptor Fin
--	also.

--	There may be useful extensions of these ideas to single-valued and
--	one-one maps; also to topologcal situations, spaces of continuous
--	functions, etc.
--	Note that some of the conclusions derived manually in the present
--	scenarios can result automatically by use of structure descriptors. For
--	example, the cardinal sum is defined as

--	 #({[x,0]: x in s_1} + {[x,1]: x in s_2}),

--	making it obvious that the sum of two integers is an integer. Similarly,
--	the definition of cardinal product, namely

--	 #{[x,y]: x in s_1,y in s_2}

--	makes it apparent that the product of two integers is an integer. Since
--	the difference of integers is defined by #(n - m), it also follows
--	immediately that the difference of integers is an integer.

--	Ordinals also have the descriptors {Ord}, since any element of an
--	ordinal is an ordinal. Any Un(s) of a set having the descriptor {Ord}
--	has the descriptor Ord. It may be worth carrying the set next(Z) as an
--	additional descriptor. If this s done, Un(s) will be known to have the
--	descriptor next(Za) is s has the descriptor {Za}, and so to have the
--	descriptor Za (i.e. to be an integer) if there is another s' having the
--	descriptor next(Z) for which
--	a statement s in s' is available.

--	In many cases a definition or theorem appearing in a scenario will
--	characterize the action on structure descriptors of one or more of the
--	function symbols appearing in it. The examples given just above
--	illustrate this. Such facts combined with the other rules given above
--	extend the verifier's ability to tack the structures of objects appearing
--	in proofs. For example, if s, t and u are sets known to have the
--	descriptor {Za}, then

--	 {(x •TIMES y) •PLUS z: x in s, y in t, z in u | P}

--	is also known to have the descriptor {Za}.

--	The theory of summation yields the fact that Sum(f) has the descriptor D
--	if f has the descriptors {[d,D]} and Fin, and if the 'PLUZ' operator
--	appearing in the summation can be shown to map pairs of objects having
--	the descriptor D into objects having this same descriptor. Thus, for
--	example, the sum or product of any setformer like

--	 {[[x,y,z],(x •TIMES y) •PLUS z]: x in s, y in t, z in u | P}

--	is also known to be an integer if s, t and u are sets known to have the
--	descriptor {Za}.

--	The structure definition mechanism explained above carries over in a
--	useful way to recursively defined functions (in our set-theoretic
--	context, these can be functions defined by transfinite induction.) To
--	show why such extension is possible, we first need to note that the
--	system of descriptors extends readily to function symbols, since these
--	are very close semantically to sets of pairs. For example, the
--	descriptor {[D_1,D_2]} can be ascribed to any one-parameter function
--	symbol which maps each object having the descriptor D_1 into an object
--	having the descriptor D_2. Similarly, the descriptor {[[D_1,D_2],D_3]}
--	can be ascribed to any two-parameter function symbol which yields an
--	object having the descriptor D_3 whenever its two parameters have the
--	respective descriptors D_1 and D_2. (For example, the integer addition
--	operator •PLUS has the descriptor {[[Za,Za],Za]}, but also the descriptors
--	{[U,U],Ord]} since it always produces an ordinal, and the descriptor
--	{[[Fin,Fin],Za]}, since it produces an integer for any two finite
--	inputs.) In the three-parameter case, {[[[D_1,D_2],D_3],D_4]} can be
--	ascribed to any three-parameter function symbol which yields an object
--	having the descriptor D_4 whenever its three parameters have the
--	respective descriptors D_1, D_2 and D_3.

--	Using these descriptors, we can state the rule for function application
--	as follows: If a one-parameter function symbol f has the descriptor
--	{[D_1,D_2]}, and x has the descriptor D_1, then f(x) has the descriptor
--	D_2. Similarly, if a two-parameter function symbol f has the descriptor
--	{[[D_1,D_2],D_3]}, and its two arguments x_1,x_2 has the descriptor
--	D_1,D_2, then f(x_1,x_2) has the descriptor D_3. We leave it to the
--	reader to formulate the rules for more than two arguments.

--	Function compounding acts in an obvious way on descriptors, for example
--	if f has the descriptor {[D_1,D_2]} and g has the descriptor
--	{[D_2,D_3]}, then g(f(.)) has the descriptor {[D_1,D_3]}. Rules like
--	this make it obvious why

--	 #({[x,0]: x in s_1} + {[x,1]: x in s_2}),

--	yields an integer for every pair of integer arguments: the functional
--	expression {[x,0]: x in s_1} has the descriptor {[Fin,Fin]} simply
--	because it is a setformer with s_1 as its only free variable, and
--	likewise for {[x,1]: x in s_2}. Since the union operator '+' has the
--	descriptor {[[Fin,Fin],Fin]}, it follows immediately that {[x,0]: x in
--	s_1} + {[x,1]: x in s_2} has the descriptor {[[Fin,Fin],Fin]} also.
--	Since #has the descriptors {[Fin,Fin]} and{[U,Ord]}, #({[x,0]: x in s_1}
--	+ {[x,1]: x in s_2}) has the descriptors {[[Za,Za],Fin]} and
--	{[[Za,Za],Ord]}, and therefore {[[Za,Za],Za]}. Much the same argument applies
--	to the integer product.

--	Next consider a transfinite recursive definition of one of the general
--	types we allow,namely

--	 f(s,t) := d({g(f(x,h(s,t)),s,t): x in s | P(x,f(x,h(s,t)),s,t)},s,t),

--	where as before we assume that the functions d, g, and h have been
--	defined prior to the occurrence of the recursive definition shown. In
--	working with this definition we will want to establish that f has some
--	descriptor {[[D_1,D_2],D_3]}, i.e. that it yields an element having
--	descriptor D_3 for any input arguments with descriptors D_1,D_2
--	respectively. This conclusion will be valid under the following
--	circumstances: we need to know that there exits descriptor D' such that

--	 (a) h has the descriptor {[[D_1,D_2],D_2]};

--	 (b) g has the descriptor {[[[D_3,D_1],D_2],D']};

--	 (c) d has the descriptor {[[[{D'},D_1],D_2],D_3]}.

--	Then in the ground case of the transfinite recursive definition f({},t)
--	has the value d({},s,t), and so must produce an element with the
--	descriptor D_3. In the remaining case it follows inductively (given that
--	s and t have the respective descriptors D_1,D_2) that f(x,h(s,t)) has
--	the descriptor D_3 for every x in s, so that g(f(x,h(s,t)),s,t) has the
--	descriptor D', and so

--	(*) {g(f(x,h(s,t)),s,t): x in s | P(x,f(x,h(s,t)),s,t)}

--	has the descriptor {D'}. Therefore the right side of the recursive
--	definition seen above has the descriptor D_3, and it follows inductively
--	that f has the descriptor {[[D_1,D_2],D_3]}.

--	If s has the descriptor Fin, then the set (*) will have this descriptor
--	also, and so if d has the descriptor {[[[Fin,Fin],D_2],Fin]}, f will
--	have the descriptor {[[Fin,D_2],Fin]}. O the other hand, if d is an
--	operator like arb, and so has the descriptor {[{D_1},D_2]} (where the
--	null set must have the descriptor D_2), then g must have the descriptor
--	{[[[Fin,Fin],D_2],Fin]}, and s the descriptor {Fin},for f(s,t) to have
--	the descriptor Fin. In this case f has once again the descriptor
--	{[[Fin,D_2],Fin]}.
--
-- *****************************************************************
-- ************ routines realizing 'Proof by Structure' ************
-- *****************************************************************

package proof_by_structure;
	var vars_to_descriptors,debug_extract,debug_conj_tree;			-- exposed for debugging purposes only
	
-- main interface procedures
	procedure extract_relevant_descriptors(conj_tree);	-- extract additional descriptors given	tree of a conjunction	
	procedure expression_descriptor(expn_stg,vars_to_descriptors);			


-- secondary interface procedures (exposed for debugging purposes only and to be invoked by test programs)
	procedure get_assertions_from_descriptors(vars_to_descriptors);	-- convert descriptors to set membership assertions	

	procedure descriptor_action_of_memb(descriptor_set);			-- result of choosing an unknown member
	procedure descriptor_action_of_subset(descriptor_set);			-- result of choosing an unknown subset
	procedure descriptor_action_of_pow(descriptor_set);
	procedure descriptor_action_of_Un(descriptor_set);
	procedure descriptor_action_of_union(descriptor_set1,descriptor_set2);
	procedure descriptor_action_of_intersection(descriptor_set1,descriptor_set2);
	procedure descriptor_action_of_difference(descriptor_set1,descriptor_set2);
	procedure descriptor_action_of_range(descriptor_set);
	procedure descriptor_action_of_domain(descriptor_set);
	procedure descriptor_action_of_arb(descriptor_set);
	procedure descriptor_action_of_pair(descriptor_set1,descriptor_set2);
	procedure descriptor_action_of_car(descriptor_set);
	procedure descriptor_action_of_cdr(descriptor_set);
	procedure descriptor_action_of_count(descriptor_set);

	procedure descriptor_action_of_next(descriptor_set);
	procedure descriptor_action_of_cartprod(descriptor_set1,descriptor_set2);
	procedure descriptor_action_of_funcprod(descriptor_set1,descriptor_set2);
	procedure descriptor_action_of_func_inv(descriptor_set);
--	procedure descriptor_action_of_func_ident(descriptor_set); -- UNUSED

--procedure tests;			-- SYSTEMATIC TESTS FOR ABOVE PROCEDURES

end proof_by_structure;

package body proof_by_structure;

	use parser,string_utility_pak,logic_syntax_analysis_pak,logic_syntax_analysis_pak2;

var first_proof_by_structure := true;



var basic_sets := {"ZA","HFIN","RA","RE","SI","CM"};

var basic_preds := {"ORD","CARD","FIN","INFIN","COUNTABLE","NONNULL","SVM","IS_MAP","ONE_1_MAP"};

var basic_descriptors; -- union of basic_sets with basic_preds

-- "COUNTABLE" MEANS 'FINITE OR ENUMERABLY INFINITE'; "HFIN" MEANS 'HEREDITARILY FINITE'

-- COMPOUND DESCRIPTORS ARE CONSTRUCTED FROM THESE BASIC DESCRIPTORS BY PAIRING AND SINGLETON FORMATION

var descriptors_of_basic := {			-- MAPPING FROM BASIC DESCRIPTORS TO COMPOUND DESCRIPTORS GIVING THEIR PROPERTIES
	["ZA",{{"ORD"},{"FIN"},{"HFIN"},"COUNTABLE","ORD","CARD","FIN","HFIN",{"CARD"},{"ZA"},{"COUNTABLE"}}],
	["ORD",{{"ORD"}}],
	["CARD",{"ORD",{"ORD"}}],
	["HFIN",{{"HFIN"},{"FIN"},{"COUNTABLE"},"FIN","COUNTABLE"}],
	["FIN",{"COUNTABLE"}],
--	["SI",{["ZA","ZA"]}], -- overly conventional
	["RASEQ",{{["ZA","RA"]},"NONNULL","INFIN","IS_MAP","SVM","COUNTABLE"}],
	["CM",{["RE","RE"]}],
	["IS_MAP",{{["OM","OM"]}}],
	["SVM",{{["OM","OM"]},"IS_MAP"}],
	["ONE_1_MAP",{{["OM","OM"]},"SVM","IS_MAP"}],
	["OM",{{"OM"}}] -- IS THIS NEEDED?? 
};

var m_descriptors_of_basic := {		-- SIMILAR TO THE PRECEDING ONE, HANDLES MULTIPLE INHERITANCE

    [{"FIN",{"HFIN"}}, {"HFIN"}],
	[{"FIN","CARD"}, {"ZA"}],
	[{"FIN","ORD"}, {"ZA"}]
};

				-- *********** ASSOCIATION OF ACTIONS WITH SYNTAX-TREE NODES ***********

var unary_op_actions := {["ast_arb",DESCRIPTOR_ACTION_OF_ARB],
		["ast_range",DESCRIPTOR_ACTION_OF_RANGE],["ast_domain",DESCRIPTOR_ACTION_OF_DOMAIN],
		["ast_nelt",DESCRIPTOR_ACTION_OF_COUNT],["ast_pow",DESCRIPTOR_ACTION_OF_POW]};

var binary_op_actions := {["ast_add",DESCRIPTOR_ACTION_OF_UNION],["ast_mult",DESCRIPTOR_ACTION_OF_INTERSECTION],
		["DOT_PROD",DESCRIPTOR_ACTION_OF_CARTPROD],																				
		["TILDE_",DESCRIPTOR_ACTION_OF_FUNC_APP],["AT_",DESCRIPTOR_ACTION_OF_FUNCPROD],
		["ast_sub",DESCRIPTOR_ACTION_OF_DIFFERENCE],["ast_enum_tup",DESCRIPTOR_ACTION_OF_PAIR]};

var function_actions_and_numpars := {["UN",[DESCRIPTOR_ACTION_OF_UN,1]],["NEXT",[DESCRIPTOR_ACTION_OF_NEXT,1]],
		["INV",[DESCRIPTOR_ACTION_OF_FUNC_INV,1]],
		["CAR",[DESCRIPTOR_ACTION_OF_CAR,1]], ["CDR",[DESCRIPTOR_ACTION_OF_CDR,1]]};

var const_properties := {		-- MAPS CONSTANTS TO COLLECTIONS OF SETS TO WHICH THEY ARE KNOWN TO BELONG
		["0",{"CARD","FIN","COUNTABLE","IS_MAP","SVM","ONE_1_MAP"}], 
		["1",{"CARD","FIN","COUNTABLE","NONNULL"}],
		["2",{"CARD","FIN","COUNTABLE","NONNULL"}],
		["3",{"CARD","FIN","COUNTABLE","NONNULL"}],
		["ZA",{"CARD","ORD","INFIN","COUNTABLE","NONNULL"}], ["RA",{"INFIN","COUNTABLE","NONNULL"}],
		["RE",{"INFIN","NONNULL"}], ["HFIN",{"INFIN","COUNTABLE","NONNULL"}],

		["CM",{{["RE","RE"]},"INFIN","NONNULL"}],

		["SI",{"INFIN","NONNULL"}],
-- ONLY A FEW OF THE CONSTANTS WHICH FOLLOW ARE DESCRIBED AS BEING NONNULL, ALTHOUGH THEY ALL ARE
		["S_0",{"SI"}],  ["S_1",{"SI"}], ["RA_0",{"RA"}], ["RA_1",{"RA"}], ["R_0",{"RE"}], ["R_1",{"RE"}], ["C_0",{"CM",["RE","RE"]}], ["C_1",{"CM",["RE","RE"]}],
		["RASEQ",   {{{["ZA","RA"]},"IS_MAP","SVM","COUNTABLE"},"NONNULL","INFIN"}],
		["RACAUCHY",{{"RASEQ",{["ZA","RA"]},"IS_MAP","SVM","COUNTABLE"},"NONNULL","INFIN"}],
		["RESEQ",   {{{["ZA","RE"]},"IS_MAP","SVM","COUNTABLE"},"NONNULL","INFIN"}],
		["RECAUCHY",{{"RESEQ",{["ZA","RE"]},"IS_MAP","SVM","COUNTABLE"},"NONNULL","INFIN"}],
		["RA0SEQ",{"RASEQ",{["ZA","RA"]},"NONNULL","INFIN","IS_MAP","SVM","COUNTABLE"}],
		["RA1SEQ",{"RASEQ",{["ZA","RA"]},"IS_MAP","SVM","NONNULL","INFIN","COUNTABLE"}],
		["RE0SEQ",{"RESEQ",{["ZA","RE"]},"NONNULL","INFIN","IS_MAP","SVM","COUNTABLE"}],
		["RE1SEQ",{"RESEQ",{["ZA","RE"]},"IS_MAP","SVM","NONNULL","INFIN","COUNTABLE"}]
	};

var unary_closed_on := {		-- MAPS UNARY OPERATORS AND FUNCTIONS TO COLLECTIONS OF SETS ON WHICH THEY ARE KNOWN TO BE CLOSED
		["S_REV",{"SI"}], ["RA_REV",{"RA"}], ["RA_ABS",{"RA"}],
		["R_REV",{"RE"}], ["ABS",{"RE"}], ["C_REV",{"CM"}], ["INV",{"HFIN"}],
		["RAS_REV",{{["ZA","RA"]}}], ["RAS_ABS",{{["ZA","RA"]}}], ["RES_REV",{{["ZA","RE"]}}], ["RES_ABS",{{["ZA","RE"]}}]
	};


var binary_closed_on := {		-- MAPS BINARY OPERATORS AND FUNCTIONS TO COLLECTIONS OF SETS ON WHICH THEY ARE KNOWN TO BE CLOSED
		["ast_add",{"CARD","ZA","ORD"}], ["ast_mult",{"CARD","ZA","ORD"}],
		["DOT_PLUS",{"CARD","ZA"}], ["DOT_TIMES",{"CARD","ZA"}], -- NEEDED??
		["DOT_MINUS",{"CARD","ZA"}], ["DOT_OVER",{"ZA"}],
		["DOT_S_PLUS",{"SI"}], ["DOT_S_TIMES",{"SI"}], ["DOT_S_MINUS",{"SI"}],
		["DOT_RA_PLUS",{"RA"}], ["DOT_RA_TIMES",{"RA"}], ["DOT_RA_MINUS",{"RA"}],
		["DOT_R_PLUS",{"RE"}], ["DOT_R_TIMES",{"RE"}], ["DOT_R_MINUS",{"RE"}],  
		["DOT_C_PLUS",{"CM"}], ["DOT_C_TIMES",{"CM"}], ["DOT_C_MINUS",{"CM"}],
		["DOT_RAS_PLUS",{"RASEQ"}], ["DOT_RAS_TIMES",{"RASEQ"}], ["DOT_RAS_MINUS",{"RASEQ"}],
		["DOT_RES_PLUS",{{["ZA","RE"]}}], ["DOT_RES_TIMES",{{["ZA","RE"]}}], ["DOT_RES_MINUS",{{["ZA","RE"]}}],
		["DOT_PROD",{"NONNULL","FIN","COUNTABLE"}], ["AT_",{"FIN","HFIN","COUNTABLE","SVM","ONE_1_MAP"}]
	};
	
var finitely_additive_descriptors := {			-- BASIC DESCRIPTORS KNOWN TO BE FINITELY ADDITIVE
			"ZA", "ORD", "FIN", "HFIN", "COUNTABLE", "CARD", "IS_MAP", {"ZA"} };

var fully_additive_descriptors := {				-- BASIC DESCRIPTORS KNOWN TO BE UNCONDITIONALLY ADDITIVE
			"ORD", "IS_MAP", {"ZA"}};

var quasi_additive_descriptors := {		-- BASIC DESCRIPTORS KNOWN TO BE UNCONDITIONALLY ADDITIVE (IF THE OVERALL ARGUMENT IS NONNULL)
			"INFIN","NONNULL"};

var inherited_descriptors := {					-- BASIC DESCRIPTORS KNOWN TO BE INHERITED BY SUBSETS
			"FIN","HFIN","COUNTABLE","IS_MAP","SVM","ONE_1_MAP"};

var transitive_descriptors := {				-- BASIC DESCRIPTORS KNOWN TO BE INHERITED BY MEMBERS
			"ZA","HFIN","ORD"};


procedure init_proof_by_structure();



--print("first_proof_by_structure", first_proof_by_structure);


	
if first_proof_by_structure then


		first_proof_by_structure := false;


		basic_sets +:= domain descriptors_of_basic - basic_preds;

		basic_descriptors :=  (basic_sets + basic_preds) with "OM";

		for k in ["0","1","2","3"] loop
			const_properties(k) := const_properties(k) + transitive_descriptors;
		end loop;

		for x in domain(const_properties)  * basic_descriptors loop

			const_properties(x) := extended_descriptors3(const_properties(x) with {x});

		end loop;

--print("const_properties: ", const_properties);

		m_descriptors_of_basic := {[m, mm + descriptors_of_basic(arb(mm))]: mm = m_descriptors_of_basic(m)};

--print("m_descriptors_of_basic: ", m_descriptors_of_basic);


	end if;


end init_proof_by_structure;




procedure expression_descriptor(expn_stg,vars_to_descriptors);			

		-- Calculates result descriptor set given an expression in the form of string (to be internally parsed into a tree)
		-- and the descriptors applicable to its free variables.
		-- This is the main routine of the the proof_by_structure system. We are concerned here with expressions of two
		-- principal kinds, simple expressions and setformer expressions.
		-- Simple expressions are processed recursively, descriptors being attached to all their nodes from bottom to top 
		-- in accordance with the expressions found at each node.
		-- Conditional expressions of the form 'if c1 then e1 elseif c2 then e2.. end if' are treated as intersections of
		-- their 'e' parts;  set-theoretic expressions have the form {e(x,y,..): x in s1, y in s2 | C } etc.
		-- We collect relevant clauses from the condition part C, and then calculate descriptors for all of the bounding sets 
		-- s1, s2,... This gives us descriptors for their members x,y,.., which are then used to calculate 
		-- a descriptor set D for e(x,y,..). The setformer then gets the descriptor {D}, to which Fin and Countable
		-- are attached if all the s1, s2,... have these descriptors, and NonNull is attached if all the sj are NonNull
		-- and the condition C is missing.
		
		tree := parse_expr(expn_stg + ";")(2);			-- get the parse tree of the expression

		
init_proof_by_structure();



		return expression_descriptor_in(tree,vars_to_descriptors);			-- call the recursive workhorse
					-- this will return the set of descriptors which attach to the top-level expression
		
end expression_descriptor;

procedure expression_descriptor_in(tree,vars_to_descriptors);			-- recursive workhorse for 'expression_descriptor' (debugging wrapper)
	res := expression_descriptor_inn(tree,vars_to_descriptors);
--print("expression_descriptor_in: ",tree," vars_to_descriptors: ",vars_to_descriptors," res: ",res);
	return if res = {} then {"OM"} elseif res /= {"OM"} then res less "OM" else res end if;
end expression_descriptor_in;

procedure expression_descriptor_inn(tree,vars_to_descriptors);			-- recursive workhorse for 'expression_descriptor'		
		-- returns the set of known descriptors of the top node of a tree
 --print("expression_descriptor_inn: ",tree,"\n",vars_to_descriptors);		
		-- this routine also exploits known closure properties of unary and binary operators and functions of several parameters.
		-- Whenever such an operator or function is encountered, we find the set on which it is closed. If this appears in the
		-- descriptors of both arguments (or one argument in the case of unaries) it is transmitted to the result
	
	
	if is_string(tree) then return (vars_to_descriptors(tree)?{}) + (const_properties(tree)?{}); end if; 
				-- if simple variable or constant, then return its given or known descriptor
	
	buffer_set := vars_to_descriptors(unparse(tree)) ? {};

	[n1,n2,n3] := tree;				-- otherwise decompose the tree at its top level, allowing for two arguments
									-- [n1,n2,n3] is [op,arg1,arg2]
									-- we check first for descriptors available because of general transitive closure properties,
									-- and return these if there are any
	if n1 = "TILDE_" then
		if #n3 /= 2 then buffer_set with:= "OM"; end if;
		n3 := n3(2);
	end if; 
	
--	if (closure_sets := unary_closed_on(n1)) /= OM then		-- this is a non-built-in operator closed on some basic set 
--		arg_descs := expression_descriptor_in(n2,vars_to_descriptors);		-- get the descriptors of the operator argument
--		ok_descs := closure_sets * arg_descs;
--		if ok_descs /= {} then buffer_set +:= ok_descs; end if;		-- if transitivity generates a useful result, return it
--	end if;

	if (closure_sets := binary_closed_on(n1)) /= OM then		-- this is a non-built-in binary operator closed on some basic set 
		arg_descs1 := expression_descriptor_in(n2,vars_to_descriptors);		-- get the descriptors of the operator argument
		arg_descs2 := expression_descriptor_in(n3,vars_to_descriptors);		-- get the descriptors of the operator argument
		ok_descs := closure_sets * arg_descs1 * arg_descs2;
--print("binary_closed_on(n1): ",n1," ",closure_sets," ",arg_descs1," ",arg_descs2," ok_descs: ",ok_descs);
		if ok_descs /= {} then buffer_set +:= ok_descs; end if;		-- if transitivity generates a useful result, return it
	end if;
	
	if n1 = "ast_of" and (closure_sets := unary_closed_on(n2)) /= OM then		-- unary function case; 
					-- these are non-built-in; abs is special since it is an operator
		arg_descs := expression_descriptor_in(n3(2),vars_to_descriptors);
		ok_descs := closure_sets * arg_descs;			-- see if any of the closure sets is available as an arg descriptor
--print("closure_sets: ",closure_sets," ",n3(2)," arg_descs: ",arg_descs);
		if ok_descs /= {} then buffer_set +:= ok_descs; end if;		-- if transitivity generates a useful result, return it
	end if;
	
			-- Note: the following 'actions' are found in the library of procedures given at the beginning of this package
	action := unary_op_actions(n1)?binary_op_actions(n1)?if n1 = "ast_of" then (fanp := (function_actions_and_numpars(n2))?[])(1) end if;
						-- get the action associated with the function at this node, if any 
--print("expression_descriptor_in: ",tree," ",action," ",descriptor_action_of_intersection);	
	if n1 notin {"ast_enum_set","ast_genset","ast_if_expr"} and action = OM then buffer_set with:= "OM"; end if;
						-- if there is none, we know nothing, so return the descriptor 'generic set'
	
	case n1				-- handle the various possible cases separately
	
		when "ast_arb","ast_range","ast_domain","ast_nelt","ast_pow" =>		-- unary operators

			argdescs := expression_descriptor_in(n2,vars_to_descriptors);		-- get the descriptors of the argument expression
--print("unary operator: ",n1," ",n2," ",argdescs," vars_to_descriptors: ",vars_to_descriptors);
			buffer_set +:= action(argdescs);		-- apply the action relevant at this node
			
		when "ast_add","ast_mult","ast_sub","ast_enum_tup","DOT_PROD","TILDE_","AT_" => 		-- binary operators

			if n1 = "ast_enum_tup" and #tree /= 3 then buffer_set with:= "OM"; end if;

			argdescs1 := expression_descriptor_in(n2,vars_to_descriptors);		-- get the descriptors of the argument expression
			argdescs2 := expression_descriptor_in(n3,vars_to_descriptors);		-- get the descriptors of the argument expression
--print("binary operator: ",n1," ",n2," ",n3," ",argdescs1," ",argdescs2);
			buffer_set +:= action(argdescs1,argdescs2);		-- apply the action relevant at this node
	
		when "ast_of" =>		-- function application
			
			arglist := n3(2..);		-- get the list of argument expressions of the function application
			argdescs1 := expression_descriptor_in(arglist(1),vars_to_descriptors);		-- get the descriptors of the argument expressions
			if (np := fanp(2)?0) > 1 then argdescs2 := expression_descriptor_in(arglist(2),vars_to_descriptors); end if;

			if np > 2 then argdescs3 := expression_descriptor_in(arglist(3),vars_to_descriptors); end if;
--print("np: ",np," ",action," ",descriptor_action_of_Un);			
			if np = 1 then buffer_set +:= action(argdescs1); end if;
			if np = 2 then buffer_set +:= action(argdescs1,argdescs2); end if;
			if np = 3 then buffer_set +:= action(argdescs1,argdescs2,argdescs3); end if;		-- other cases can obviously be added

		when "ast_enum_set" =>			-- enumerated sets: find the common descriptors of all the elements

			descs := expression_descriptor_in(n2,vars_to_descriptors);	-- the members are the tree elements after n1
--print("ast_enum_set: ",descs," ",n2);
			descs := descs */[expression_descriptor_in(memb,vars_to_descriptors): memb = tree(j) | j > 2];

			buffer_set +:= {{d}: d in descs} + {"FIN","NONNULL"} + -- the result is of course finite and nonempty

				 if (forall tree_j = tree(j) | j = 1 or
					(exists d in expression_descriptor_in(tree_j,vars_to_descriptors) | is_pair(d)))
				then
					{"IS_MAP"}
				else
					{}
				end if;
					-- We are checking that there exists at least one pair d among the descriptors
					--  of each enumerated element, to allow for sets of the type
					-- {[x,y], a}, where a has a pair as descriptor. However, its efficiency
					-- can be improved, as expression_descriptor_in gets computed one more time.

-- The following extension to the treatment of maps would be unsound:
--
--			if "IS_MAP" in buffer_set then
--
--				is_svm := true;
--
--				map_check := {};
--
--				for j in [2..#tree] loop
--
--					if is_tuple(p := tree(j)) and (p(1) = "ast_enum_tup") and (#p = 3) and (map_check(p(2)) = OM) then
-- 
--				                       map_check(p(2)) := p(3);
--					else
--                        				is_svm := false;
--					end if;
--				end loop;
--
--				if (is_svm) then
--
--					buffer_set with:= "SVM";
--
--					if (#domain(map_check) = #range(map_check)) then buffer_set with:= "ONE_1_MAP"; end if;
--				end if;
--			end if;
 
		when "ast_genset" =>			-- setformer; see comment above
				-- a sample template, for {e(x,y): x in s, y in t | P(x,y)}, is
				--  ["ast_genset", tree_of_e(x,y), ["ast_iter_list", ["ast_in", "X", "S"], ["ast_in", "Y", "T"]], tree_of_P(x,y)]
				-- if the condition is void, we have instead
				--  ["ast_genset", tree_of_e(x,y), ["ast_iter_list", ["ast_in", "X", "S"], ["ast_in", "Y", "T"]], ["ast_null"]]
				
				lc1 := (limiting_clauses := n3(2..))(1);		-- the limiting clauses of the setformer
				bound_var_descs := {};			-- these will be collected as we go along in the limiting clauses
				restriction_set_descs := [];	-- we also collect the descriptors of the restriction sets themselves
				
							-- get the descriptor of the first limiting set
				restriction_set_descs with:= (descs_ls1 := expression_descriptor_in(lc1(3),vars_to_descriptors));
--print("lc1(3): ",lc1(3)," ",vars_to_descriptors," restriction_set_descs: ",restriction_set_descs);
				bound_var_descs(lc1(2)) :=	if lc1(1) = "ast_in" then descriptor_action_of_memb(descs_ls1)  
							elseif lc1(1) = "DOT_INCIN" then descriptor_action_of_subset(descs_ls1)
							else {} end if;		-- allow for inclusion-form iterators

							-- progressing from left to right, get the descriptors of the other limiting sets,
				for j in [2..#limiting_clauses] loop
					lcj := limiting_clauses(j);		-- the limiting clauses of the setformer
				
							-- get the descriptor of the jth limiting set
					restriction_set_descs with:= (descs_lsj := expression_descriptor_in(lcj(3),vars_to_descriptors + bound_var_descs));

							-- meanwhile assigning descriptors to the bound variables as they are encountered
					bound_var_descs(lcj(2)) :=
						if lcj(1) = "ast_in" then descriptor_action_of_memb(descs_lsj)
						elseif lcj(1) = "DOT_INCIN" then descriptor_action_of_subset(descs_lsj)
						else {} end if;		-- allow for inclusion-form iterators
				end loop;
				
				 			-- recursively calculate the descriptor of the lead expression
				 vars_to_descriptors_save := vars_to_descriptors;
				 					-- save, in case some of the bound variables have the same name as some of the free variables
				for [v,descs] in bound_var_descs loop vars_to_descriptors(v) := descs; end loop;
				descs_lead := expression_descriptor_in(n2,vars_to_descriptors);

--print(" descs_lead: ",descs_lead," vars_to_descriptors: ",vars_to_descriptors," n2: ",n2);				
				vars_to_descriptors := vars_to_descriptors_save; -- restore, so as not to affect the external environment
				 
				descs_lead := {{x}: x in descs_lead}; -- form the descriptor for a set of elements of this kind




-- n1 is "ast_genset"

-- n2 is of the form ["ast_enum_tup","x",tree_of_e(x)]

-- n3 is of the form ["ast_iter_list",["ast_in","x","s"]]
-- or of the equivalent form in which "ast_in" is replaced by "DOT_INCIN"



				if n2(1) = "ast_enum_tup" then


					lhss := {x(2): x = n3(i) | i > 1 and (x(1) = "ast_in" or x(1) = "DOT_INCIN")}; -- variables bound by iterators


					if (#lhss = #n3 - 1) -- viz., each iterator binds a distinct variable


						and

							if #lhss = 1 then n2(2) = arb(lhss)
							else is_tuple(n22 := n2(2)) and n22(1) = "ast_enum_tup" and
								#n22 = 3 and {n22(2),n22(3)} = lhss
							end if

						and

							all_conss(n2(3)) = lhss

					then


						descs_lead with:= "ONE_1_MAP";


					end if;


					if ("ONE_1_MAP" in descs_lead) or (is_string(n2(2)) and -- we check that we have a pair [x,e(x)], where x is indeed a variable

					   n3(1) = "ast_iter_list" and -- we check that we indeed have a list of iterators

					   #n3 < 3 and -- we check that we have only one iterator and no condition P(x)

					   ( (iter_type := n3(2)(1)) = "ast_in" or iter_type = "DOT_INCIN" ))

					then

 
						  descs_lead with:= "SVM";

					end if;



					descs_lead with:= "IS_MAP";

				end if;



--print("restriction_set_descs: ",restriction_set_descs);
									-- if all of the limiting sets are known to be finite, the result is finite
				if (forall de in restriction_set_descs | "FIN" in de) then descs_lead with:= "FIN"; end if;

							-- the setformer is countable if every restriction set is either finite or countable and a membership restriction 
				if (forall de = restriction_set_descs(j) | ("COUNTABLE" in de or "FIN" in de) 
								and (not("FIN" notin de and limiting_clauses(j)(1) = "DOT_INCIN"))) then descs_lead with:= "COUNTABLE"; end if;
					
									-- if all of the limiting sets are known to be NonNull and there is no condition the result is NonNull
				if (forall de = restriction_set_descs(j) | "NONNULL" in de) and tree(4) = ["ast_null"] then descs_lead with:= "NONNULL"; end if;
									-- if all of the limiting sets are known to be NonNull and there is no condition and one is infinite the result is Infinite
				if (forall de = restriction_set_descs(j) | ("NONNULL" in de or "INFIN" in de)) and 
							(exists de = restriction_set_descs(j) | "INFIN" in de) and tree(4) = ["ast_null"] and

					all_conss(n2) = {x(2): x = n3(i) | i > 1 and (x(1) = "ast_in" or x(1) = "DOT_INCIN")}

				then descs_lead with:= "INFIN"; end if;

				buffer_set +:= descs_lead;			-- return the calculated descriptors

		when "ast_if_expr" =>			-- conditional expression; find the common descriptors of both branches
			-- template is ["ast_if_expr", "A", "B", ["ast_if_expr", "C", "D", "E"]]
			argdescs1 := expression_descriptor_in(n3,vars_to_descriptors);		-- get the descriptors of the first branch
			argdescs2 := expression_descriptor_in(tree(4),vars_to_descriptors);		-- get the descriptors of the second branch
--print("ast_if_expr: ",argdescs1," ",argdescs2);			
			buffer_set +:= argdescs1 * argdescs2;				-- return those descriptors that are common to both branches

	end case;
	
	return buffer_set;

end expression_descriptor_inn;



procedure all_conss(tree);		-- test a tree for being all cons operators, and return the set of its variables


		return


			if is_string(tree) then {tree}


			elseif is_tuple(tree) and tree(1) = "ast_enum_tup" and #tree = 3 then

							-- if not all cons operators then return OM

				if (left := all_conss(tree(2))) = OM or  (right := all_conss(tree(3))) = OM then OM


				else left + right end if


			else


				OM


			end if;


end all_conss;


procedure extract_relevant_descriptors(conj_tree);	-- extract relevant descriptors given tree of a conjunction	
	-- this involves information concerning membership, equality, and inclusion; also particular predicates
	-- it looks for Ref clauses of various forms directly expressible as descriptors, and collects these descriptors into a set which is returned.
	-- the clauses which can be handled in this way, and their translations, are x in Za, x in Re, Card(x), Ord(x), and in the other elementary sets, 
	-- which translate into Za, Re, Card, Ord, etc.; x •incin Za etc., which translate into 
	-- {Za}, {Re}, {Card}, {Ord}, etc.  Finite(x) and Countable(x), which become Fin and Countable; not Finite(x) which becomes Infin;
	-- and x /= 0 which becomes NonNull. This extraction is iterated twice to handle cases like 'x in n and n in Za', and also handles cases like
	-- 'x /= 0 and y incs x' and 'Finite(x) and x incs y'. We also handle Svm and one_1_map.

	-- note that this routine works with variables only, not with subexpressions, so in some cases local variables will need to be defined in
	-- proofs and properties stated for these variables.

	init_proof_by_structure();



	debug_extract := [memb_conjs,inc_conjs,equality_conjs] := extract_relevant_conjuncts(debug_conj_tree := conj_tree);
					-- walk the tree, collecting the relevant top-level conjuncts. This adds non-nullity assertions whenever memberships are found.

		-- dummy inclusions like [x,"FIN"] are used to represent the predicates Fin, Svm, Is_map, and one_1_map
		-- dummy inclusions like ["Nonull",x]  are used to represent the predicates 'x /= 0' and 'not Finite(x)'
		-- Note the use of partially lowercase forms, which will distinguish these from actual scenario clauses which resemble them                                             
		
		-- an attempt is made to identify the range and domain of variables for which Is_map(f) is asserted

		-- equalities with simple variables on one side are treated in a special way by calculating descriptors for their right-hand side
		-- and propagating them to the left-hand variable. This makes it possible to identify some setformers that give rise 
		-- to mappings, single-valued mappings, and 1-1 mappings, or to subsets of known sets.
		

	vars_to_descriptors := {[v,w] in memb_conjs | w in basic_descriptors} + {[v,{w}]: [v,w] in inc_conjs | w in basic_descriptors};

				-- preliminary conversion into map from vars to descriptors, as multivalued map

--print("\nmemb_conjs before loop: ",memb_conjs); print("inc_conjs before loop: ",inc_conjs); print("equality_conjs before loop: ",equality_conjs); 
--print("vars_to_descriptors before loop: ",vars_to_descriptors); 
	
				-- now we use a bit of transitive closure: if a in b is available and b incin basic_descriptor
				-- is present, we collect a in basic_descriptor; if a incin b is available and b incin basic_descriptor
				-- is present, we collect a incin basic_descriptor; if a in Za is available we collect a incin Za, and likewise
				-- for ordinals and cardinals. This process is continued as long as we are finding more
				-- primitives like Is_map, Svm, and Fin are treated a bit specially because of their relationship to inclusion,
				-- as is Infin.
				
	something_changed := true;			-- force entry to loop

	debug_count := 0;
	
	while something_changed loop			-- this propagation loop iterates as long as new attributes are being found
											-- for the variables which it encounters. 

		something_changed := false;			-- but maybe something will change in the body of the loop
			-- set inclusions are used to propagate all inheritable descriptors from their right-hand side to their  
			-- left, and to propagate all membership relationship involving their left-hand sides to their right.

			if (debug_count +:= 1) > 10 then exit; end if;		-- limit to at most 10 iterations

			newincs := {[s1,s3]: [s1,s2] in inc_conjs, s3 in inc_conjs{s2}} - inc_conjs;		-- exploit the transitivity of inclusion
			if newincs /= {} then		-- expand the set of known inclusions
				inc_conjs +:= newincs; something_changed := true;		-- and flag for another iteration
			end if;

			newmembs := {[s1,s3]: [s1,s2] in memb_conjs, s3 in inc_conjs{s2}};

			newmembs -:= memb_conjs;
			if newmembs /= {} then		-- expand the set of known inclusions
				memb_conjs +:= newmembs; something_changed := true;		-- and flag for another iteration
			end if;
			
			vars_to_descriptors +:= {[u,{v}]: [u,v] in inc_conjs | is_string(u) and u notin basic_preds and v in basic_descriptors}
										+ {[u,v]: [u,v] in memb_conjs | is_string(u) and u notin basic_preds and v in basic_descriptors}
										+ {[u,"NONNULL"]: u in inc_conjs{"NONNULL"} | is_string(u) and u notin basic_descriptors}
										+ {[u,"INFIN"]: u in inc_conjs{"INFIN"} | is_string(u) and u notin basic_descriptors};
			
									-- convert the conjuncts we have so far to a vars_to_descriptors multivalued map
									-- for each memb_conj [u,v], we get all the descriptors of v given the 
									-- current vars_to_descriptors,
									-- and of thoos take the ones which are sets, whos menbers become descriptors of x.  
									-- for each inc_conj [u,v], we get all the descriptors of v given the 
									-- current vars_to_descriptors,
									-- and of those take the ones which are sets, which become descriptors of x.

--print("propagation iteration " + debug_count + ": vars_to_descriptors in extract_relevant_descriptors: ",vars_to_descriptors);									

			for [u,v] in memb_conjs loop 			-- v can be the tree of an expression


				if is_string(u) then


					vtd := {[x,vars_to_descriptors{x}]: x in domain(vars_to_descriptors)}; -- convert to set-valued map, as required by expression_descriptor_in


					expn_descriptors := expression_descriptor_in(v,vtd);

							-- call the recursive workhorse to get the descriptor set of the expression


					new_u := {};

	

				
					if v in basic_preds then



						new_u := {[u,d]: d in descriptors_of_basic(v) with v};


	 				elseif u notin basic_preds then --?? wouldn't this be an indication of an earlier bug? [ALEXANDRU]



						new_u := {[u,d]: d in descriptor_action_of_memb(expn_descriptors)};

	
				end if;


					
					if not( vars_to_descriptors incs new_u) then


						vars_to_descriptors +:= new_u;

						something_changed := true;

					end if;


				end if;


			end loop;
									
			for [u,v] in inc_conjs loop 			-- v can be the tree of an expression

				vtd := {[x,vars_to_descriptors{x}]: x in domain(vars_to_descriptors)};		-- convert to set-valued map, as required by expression_descriptor_in

				expn_descriptors := expression_descriptor_in(v,vtd);
							-- call the recursive workhorse to get the descriptor set of the expression

				vars_to_descriptors +:= ({[u,ed]: ed in expn_descriptors | (is_set(ed) or (ed in inherited_descriptors and u notin basic_descriptors))} 
						+ {[u,ed]: ed in expn_descriptors | is_string(ed) and (ed notin basic_descriptors) and (u = "INFIN" or u = "NONNULL")});

			end loop;		-- end of loop for initial propagation by transitive closure
			
									-- for equalities, we calculate the descriptor set of the right hand side using 
									-- the available vars_to_descriptors and propagate it to the left-hand variable.

					-- here expn is the parse tree of an expression
			for [v,expn] in equality_conjs loop			-- iterate over all available equalities

				if v notin basic_sets then

					vtd := {[x,vars_to_descriptors{x}]: x in domain(vars_to_descriptors)};		-- convert to set-valud map, as required by expression_descriptor_in
				
					expn_descriptors := expression_descriptor_in(expn,vtd);
							-- call the recursive workhorse to get the descriptor set of the expression

-- look for the new_descriptors for this variable

--					new_descriptors := expn_descriptors - (desv := vars_to_descriptors{v}); 
					new_descriptors := expn_descriptors + vars_to_descriptors{unparse(expn)} - (desv := vars_to_descriptors{v});

--print("vars_to_descriptors equality loop: ",v," ",vars_to_descriptors," expn_descriptors: ",expn_descriptors," new_descriptors: ",new_descriptors);

					if new_descriptors /= {} then vars_to_descriptors{v} := desv + new_descriptors; something_changed := true; end if;

				end if;	

			end loop;

			-- if any of these operations extend the set of descriptors available for any variable, we set the 'something_changed'
			-- to true, thereby forcing another iteration.
				
	end loop;		-- on exiting this loop we have collected all relevant descriptors
			
	vars_to_descriptors +:= ({[v,"INFIN"]: v in inc_conjs{"INFIN"} | is_string(v)} + {[v,"NONNULL"]: v in inc_conjs{"NONNULL"} | is_string(v)}); 
									-- convert the INFIN and NONULL special inclusions to standard descriptors
	
	res := {[x,vars_to_descriptors{x}]: x in domain(vars_to_descriptors) | x notin basic_descriptors};
								-- convert into map-to-sets and return
				
--print("\ndebug_count: ",debug_count," vars_to_descriptors after loop exit: ",res," inc_conjs after loop exit: ",inc_conjs); 
	return res;
				
end extract_relevant_descriptors;

procedure extract_relevant_conjuncts(tree);		-- walk the tree, collecting the relevant top-level conjuncts.
			-- the relevant conjuncts are those stating membrship or inclusion of one variable in another
	var memb_conjs := {};		-- conjuncts designating membership: will be collected as pairs
	var inc_conjs := {};		-- conjuncts designating inclusion: will be collected as pairs
	var equality_conjs := {};		-- conjuncts designating equalities to setformers: will be collected as pairs
	
	extract_relevant_conjuncts_in_new(tree);		-- call the recursive workhorse
--print("[memb_conjs,inc_conjs,equality_conjs]: ",[memb_conjs,inc_conjs,equality_conjs]);	
	return [memb_conjs,inc_conjs,equality_conjs];		-- return all the pairs collected
	
	procedure extract_relevant_conjuncts_in_new(tree);		-- internal recursive workhorse
--print("extract_relevant_conjuncts_in_new: ",tree);	
		if is_string(tree) then return; end if;		-- since we have hit bottom
		
		[n1,n2,n3] := tree;			-- decompose the node
		
		case n1
		
			when "ast_in" => 		-- collect if membership between variables
				
						-- memberships with compound right hand side are collected, since these can produce valuable descriptors
				memb_conjs with:= [unparse(n2),n3];
				inc_conjs with:= ["NONNULL",unparse(n3)];		-- memberships with simple right hand side are collected as assertions of non-nullity

			when "ast_incs" => 		-- reverse and collect if inclusion between variables
				
				if is_tuple(n3) and n3(1) = "ast_enum_set" then

					for j in [2..#n3] loop
              					memb_conjs with:= [unparse(n3(j)), n2];
       					end loop;
				else
				
					inc_conjs with:= [unparse(n3),n2];		-- inclusions with compound right hand side are collected, since these can produce valuable descriptors
				end if;

			when "DOT_INCIN" => 		-- collect if inclusion between variables

				if is_tuple(n2) and n2(1) = "ast_enum_set" then

					for j in [2..#n2] loop
               					memb_conjs with:= [unparse(n2(j)), n3];
       					end loop;
				else				
					inc_conjs with:= [unparse(n2),n3];		-- inclusions with compound right hand side are collected, since these can produce valuable descriptors
				end if;
--print("inc_conjs: ",inc_conjs);
			when "ast_ne" =>		-- collect assertions of non-nullity

				if n3 = "0" then	
					inc_conjs with:= ["NONNULL",unparse(n2)];			-- this is collected as an inclusion of a dummy  element
				elseif n2 = "0" then	
					inc_conjs with:= ["NONNULL",unparse(n3)];			-- this is collected as an inclusion of a dummy  element
				end if;

			when "ast_eq" =>		-- we are concerned here with just a few kinds of equality clauses
				-- (1) assertions domain(x) = y and range(x) = y between variables, which are collected into dom_conjs and range_conjs respectively
				-- (2) assertions of equality between a variable and a setformer whose lead expression is a pair
				-- and whose limiting sets are simple variables, e.g. {[e(x),f(x)]: x in s | P(x)} but not 
				-- {[e(x),f(x)]: x in (s + t) | P(x)}. These always define maps, and the closure properties of e(x) and 
				-- f(x) may allow something to be said concerning the domain and range of these maps. In some cases like
				-- {[x,f(x)]: x in s | P(x)} we may be able to say that the map is single valued, and in cases like
				-- {[[x,y],[y,x]]: x in s, y in t | P(x,y)} we may be able to say that the map is 1-1.

				if is_string(n2) then							-- variable equals setformer
						-- we collect equalities of all kinds, since even if they do not define maps we may be able to deduce something concerning their elements
					equality_conjs with:= [n2,n3]; 	
					if is_string(n3) then equality_conjs with:= [n3,n2]; end if;	-- collect symmetrically to propagate descriptors in both directions

				elseif is_string(n3) then							-- setformer equals variable
						-- we collect equalities of all kinds, since even if they do not define maps we may be able to deduce something concerning their elements

					equality_conjs with:= [n3,n2]; 

				end if;		-- these equalities should be used to propagate type info to the next level 
							-- 'expression_descriptor' routine that calls this routine.
				
			when "ast_of" => 		-- collect if this is a predicate we can handle, converting it to a nominal membership
		
				case n2				-- examine the predicate

					when "FINITE" => 		-- collect and convert into a nominal inclusion

						memb_conjs with:= [unparse(n3(2)),"FIN"];		

					when "COUNTABLE" => 		-- collect and convert into a nominal inclusion

						memb_conjs with:= [unparse(n3(2)),"COUNTABLE"];		
						
					when "SVM" => 		-- collect and convert into a nominal inclusion

						memb_conjs with:= [unparse(n3(2)),"SVM"];

					when "ONE_1_MAP" => 		-- collect and convert into a nominal inclusion

						memb_conjs with:= [unparse(n3(2)),"ONE_1_MAP"];

					when "IS_MAP" => 		-- collect and convert into a nominal inclusion

						memb_conjs with:= [unparse(n3(2)),"IS_MAP"];	

					when "ORD" => 		-- collect and convert into a descriptor

						memb_conjs with:= [unparse(n3(2)),"ORD"];	

					when "CARD" => 		-- collect and convert into a descriptor

						memb_conjs with:= [unparse(n3(2)),"CARD"];	

				end case;
		
			when "ast_not" => 		-- collect if this is a negated predicate we can handle, converting it to a nominal membership
				
				if is_tuple(n2) then
				
					[m1,m2,m3] := n2;			-- unpack the argument of the 'not'
					
					case m1

						when "ast_eq" =>		-- collect assertions of non-nullity
							
							if is_string(m2) and m3 = "0" then	
								inc_conjs with:= ["NONNULL",m2];			-- this is collected as an inclusion of a dummy  element
							elseif is_string(m3) and m2 = "0" then	
								inc_conjs with:= ["NONNULL",m3];			-- this is collected as an inclusion of a dummy  element
							end if;

						when "ast_of" =>		-- collect assertions of infiniteness

							if m2 = "FINITE" then
							
								inc_conjs with:= ["INFIN",unparse(m3(2))];			-- this is collected as an inclusion of a dummy  element
							
							end if;

					end case;

				end if;
				
				return;		-- what remains is opaque

			when "ast_and","AMP_" => 			-- process arguments recursively; note that conjunctions can have two syntactic forms
				
				extract_relevant_conjuncts_in_new(n2); extract_relevant_conjuncts_in_new(n3);

			otherwise => return;		-- what remains is opaque
			
		end case;
		
	end extract_relevant_conjuncts_in_new;
	
	procedure extract_relevant_conjuncts_in(tree);		-- internal recursive workhorse (OLD VERSION)
	
		if is_string(tree) then return; end if;		-- since we have hit bottom
		
		[n1,n2,n3] := tree;			-- decompose the node
		
		case n1
		
			when "ast_in" => 		-- collect if membership between variables
				
				if is_string(n2) then		-- memberships with compound right hand side are collected, since these can produce valuable descriptors
					memb_conjs with:= [n2,n3];
				end if;

				if is_string(n3) then		-- memberships with simple right hand side are collected as assertions of non-nullity
					inc_conjs with:= ["NONNULL",n3];
				end if;
				
				return;		-- what remains is opaque

			when "ast_incs" => 		-- reverse and collect if inclusion between variables
				
				if is_string(n3) then		-- inclusions with compound right hand side are collected, since these can produce valuable descriptors
					inc_conjs with:= [n3,n2];
				end if;
				
				return;		-- what remains is opaque

			when "DOT_INCIN" => 		-- collect if inclusion between variables
				
				if is_string(n2) then		-- inclusions with compound right hand side are collected, since these can produce valuable descriptors
					inc_conjs with:= [n2,n3];
				end if;
				
				return;		-- what remains is opaque

			when "ast_ne" =>		-- collect assertions of non-nullity

				if is_string(n2) and n3 = "0" then	
					inc_conjs with:= ["NONNULL",n2];			-- this is collected as an inclusion of a dummy  element
				elseif is_string(n3) and n2 = "0" then	
					inc_conjs with:= ["NONNULL",n3];			-- this is collected as an inclusion of a dummy  element
				end if;
				
				return;		-- what remains is opaque

			when "ast_eq" =>		-- we are concerned here with just a few kinds of equality clauses
				-- (1) assertions domain(x) = y and range(x) = y between variables, which are collected into dom_conjs and range_conjs respectively
				-- (2) assertions of equality between a variable and a setformer whose lead expression is a pair
				-- and whose limiting sets are simple variables, e.g. {[e(x),f(x)]: x in s | P(x)} but not 
				-- {[e(x),f(x)]: x in (s + t) | P(x)}. These always define maps, and the closure properties of e(x) and 
				-- f(x) may allow something to be said concerning the domain and range of these maps. In some cases like
				-- {[x,f(x)]: x in s | P(x)} we may be able to say that the map is single valued, and in cases like
				-- {[[x,y],[y,x]]: x in s, y in t | P(x,y)} we may be able to say that the map is 1-1.

				if is_string(n2) then							-- variable equals setformer
						-- we collect equalities of all kinds, since even if they do not define maps we may be able to deduce something concerning their elements
					equality_conjs with:= [n2,n3]; 	
					if is_string(n3) then equality_conjs with:= [n3,n2]; end if;	-- collect symmetrically to propagate descriptors in both directions

				elseif is_string(n3) then							-- setformer equals variable
						-- we collect equalities of all kinds, since even if they do not define maps we may be able to deduce something concerning their elements

					equality_conjs with:= [n3,n2]; 

				end if;
				
			when "ast_of" => 		-- collect if this is a predicate we can handle, converting it to a nominal membership
		
				case n2				-- examine the predicate

					when "FINITE" => 		-- collect and convert into a nominal inclusion

						if is_string(arg := n3(2))	then 		-- argument is a variable
							memb_conjs with:= [arg,"FIN"];		
						end if;
				
						return;		-- what remains is opaque

					when "COUNTABLE" => 		-- collect and convert into a nominal inclusion

						if is_string(arg := n3(2))	then 		-- argument is a variable
							memb_conjs with:= [arg,"COUNTABLE"];		
						end if;
				
						return;		-- what remains is opaque
						
					when "SVM" => 		-- collect and convert into a nominal inclusion

						if is_string(arg := n3(2))	then 		-- argument is a variable
							memb_conjs with:= [arg,"SVM"];
						end if;
				
						return;		-- what remains is opaque

					when "ONE_1_MAP" => 		-- collect and convert into a nominal inclusion

						if is_string(arg := n3(2))	then 			-- argument is a variable
							memb_conjs with:= [arg,"ONE_1_MAP"];
						end if;
				
						return;		-- what remains is opaque

					when "IS_MAP" => 		-- collect and convert into a nominal inclusion

						if is_string(arg := n3(2))	then 			-- argument is a variable
							memb_conjs with:= [arg,"IS_MAP"];	
						end if;
				
						return;		-- what remains is opaque

					when "ORD" => 		-- collect and convert into a descriptor

						if is_string(arg := n3(2))	then 			-- argument is a variable
							memb_conjs with:= [arg,"ORD"];	
						end if;
				
						return;		-- what remains is opaque

				end case;
		
			when "ast_not" => 		-- collect if this is a negated predicate we can handle, converting it to a nominal membership
				
				if is_tuple(n2) then
				
					[m1,m2,m3] := n2;			-- unpack the argument of the 'not'
					
					case m1

						when "ast_eq" =>		-- collect assertions of non-nullity
							
							if is_string(m2) and m3 = "0" then	
								inc_conjs with:= ["NONNULL",m2];			-- this is collected as an inclusion of a dummy  element
							elseif is_string(m3) and m2 = "0" then	
								inc_conjs with:= ["NONNULL",m3];			-- this is collected as an inclusion of a dummy  element
							end if;

						when "ast_of" =>		-- collect assertions of infiniteness

							if m2 = "FINITE" then
							
								if is_string(arg := m3(2))	then 			-- argument is a variable
									inc_conjs with:= ["INFIN",arg];			-- this is collected as an inclusion of a dummy  element
								end if;
							
							end if;

					end case;

				end if;
				
				return;		-- what remains is opaque

			when "ast_and","AMP_" => 			-- process arguments recursively; note that conjunctions can have two syntactic forms
				
				extract_relevant_conjuncts_in(n2); extract_relevant_conjuncts_in(n3);

			otherwise => return;		-- what remains is opaque
			
		end case;
		
	end extract_relevant_conjuncts_in;
	
end extract_relevant_conjuncts;

procedure get_assertions_from_descriptors(vars_to_descriptors);	-- convert descriptors to set membership assertions for use in ELEM deductions
	-- this looks for descriptors of various forms directly expressible as Ref clauses, and generates these clauses.
	-- the descriptors which can be handled in this way, and their translations, are Za, Re, Card, Ord, and the other elementary sets, 
	-- which translate into x in Za, x in Re, Card(x), Ord(x), etc.; {Za}, {Re}, {Card}, {Ord}, which translate into 
	-- x •incin Za etc., Fin and Countable, which become Finite(x) and Countable(x); Infin which becomes not Finite(x);
	-- and NonNull, which becomes x /= 0. We also handle Svm and one_1_map.
	
	new_vars_to_descriptors := vars_to_descriptors;		-- make copy to extend
--print("vars_to_descriptors: ",vars_to_descriptors);	

	for [x,descs] in vars_to_descriptors loop
		if "CARD" in descs then descs with:= "ORD"; end if;
		for m in (domain m_descriptors_of_basic) loop
			if (descs incs m) then descs +:= m_descriptors_of_basic(m); end if;
		end loop;

		new_vars_to_descriptors(x) := descs;
	end loop;
--print("new_vars_to_descriptors: ",new_vars_to_descript