diff --git a/parser/tau.tgf b/parser/tau.tgf
index 7ac5e3f3..56e1d36e 100644
--- a/parser/tau.tgf
+++ b/parser/tau.tgf
@@ -82,9 +82,9 @@ in				=> "?i_" chars. # instead of '<', easy to remember
 out				=> "?o_" chars. # instead of '>', easy to remember
 
 # tau
-tau_rule			=> tau_matcher definition tau_body dot.
+tau_rule	=> tau_matcher definition tau_body dot.
 tau_matcher	=> tau.
-tau_body	=> tau.
+tau_body	=> tau | tau_collapse_positives_cb | tau_positives_upwards_cb.
 
 
 # TODO (HIGH) check programatically that we do not have inappropriated element from wff in tau
@@ -262,6 +262,12 @@ wff_has_clashing_subformulas_cb_sym		=> ws "wff_has_clashing_subformulas_cb" ws.
 wff_has_subformula_cb_sym				=> ws "wff_has_subformula_cb" ws.
 wff_remove_existential_cb_sym			=> ws "wff_remove_existential_cb" ws.
 
+
+# cb for tau
+tau_collapse_positives_cb	=> tau_collapse_positives_cb_sym ws_required tau_cb_arg ws_required tau_cb_arg ws_required tau_cb_arg.
+tau_positives_upwards_cb	=> tau_positives_upwards_cb_sym ws_required tau_cb_arg ws_required tau_cb_arg.
+tau_cb_arg	=> capture | tau.
+
 # input definition
 input			=> in colon open_brace source_binding close_brace.
 
diff --git a/parser/tau_parser.generated.h b/parser/tau_parser.generated.h
index 4f5d76df..0c6344dc 100644
--- a/parser/tau_parser.generated.h
+++ b/parser/tau_parser.generated.h
@@ -8,7 +8,7 @@
 struct tau_parser {
 	tau_parser() :
 		nts(load_nonterminals()), cc(load_cc()),
-		g(nts, load_prods(), nt(207), cc), p(g, load_opts()) {}
+		g(nts, load_prods(), nt(212), cc), p(g, load_opts()) {}
 	std::unique_ptr<typename idni::parser<char, char>::pforest> parse(
 		const char* data, size_t size = 0, size_t max_l = 0,
 		char eof = std::char_traits<char>::eof())
@@ -38,21 +38,21 @@ struct tau_parser {
 		open_bracket, close_bracket, open_brace, close_brace, minus, colon, semicolon, less, comma, sym,
 		offsets, step, offset, _Roffsets_8, _Roffsets_9, num, capture, shift, timed_offset, timed_step,
 		timed_capture, timed_shift, variable, var, timed, in, out, _Rtimed_10, tau_rule, tau_matcher,
-		tau_body, tau, wff, tau_and, tau_or, tau_neg, tau_t, tau_f, tau_and_sym, tau_or_sym,
-		tau_neg_sym, wff_rule, wff_matcher, wff_body, wff_rec_relation, wff_ref, bf_eq_cb, bf_neq_cb, wff_has_clashing_subformulas_cb, wff_has_subformula_cb,
-		wff_remove_existential, wff_and, wff_neg, wff_xor, wff_conditional, wff_or, wff_all, wff_ex, wff_imply, wff_equiv,
-		wff_t, wff_f, bf_eq, bf_neq, bf_less, bf_less_equal, bf_greater, wff_ref_args, _Rwff_ref_args_11, _Rwff_ref_args_12,
-		wff_and_sym, wff_or_sym, wff_xor_sym, wff_conditional_sym, wff_neg_sym, wff_imply_sym, wff_equiv_sym, wff_all_sym, _Rwff_all_13, wff_ex_sym,
-		_Rwff_ex_14, bf, bf_equality_sym, bf_nequality_sym, bf_less_sym, bf_less_equal_sym, bf_greater_sym, bf_rule, bf_matcher, bf_body,
-		bf_rec_relation, bf_ref, bf_is_zero_cb, bf_is_one_cb, bf_has_clashing_subformulas_cb, bf_has_subformula_cb, bf_constant, bf_and, bf_neg, bf_xor,
-		bf_or, bf_all, bf_ex, bf_subs_cb, bf_t, bf_f, bf_ref_args, _Rbf_ref_args_15, _Rbf_ref_args_16, bf_and_sym,
-		bf_or_sym, bf_xor_sym, bf_neg_sym, bf_all_sym, _Rbf_all_17, bf_ex_sym, _Rbf_ex_18, constant, binding, bf_and_cb,
-		bf_or_cb, bf_xor_cb, bf_neg_cb, source_binding, named_binding, type, source, source0, _Rsource_19, _Rsource_20,
-		bf_cb_arg, bf_and_cb_sym, bf_or_cb_sym, bf_xor_cb_sym, bf_neg_cb_sym, bf_subs_cb_sym, bf_eq_cb_sym, wff_cb_arg, bf_neq_cb_sym, bf_is_zero_cb_sym,
-		bf_is_one_cb_sym, bf_has_clashing_subformulas_cb_sym, wff_has_clashing_subformulas_cb_sym, bf_has_subformula_cb_sym, wff_has_subformula_cb_sym, wff_remove_existential_cb_sym, input, inputs, _Rinputs_21, _Rinputs_22,
-		main, rule, rules, _Rrules_23, _Rrules_24, rec_relation, rec_relations, _Rrec_relations_25, _Rrec_relations_26, formula,
-		library, builder, builder_head, builder_body, _Rbuilder_head_27, _Rbuilder_head_28, gssotc, start, __neg_0, __neg_1,
-		__neg_2, __neg_3, __neg_4, __neg_5,
+		tau_body, tau, tau_collapse_positives_cb, tau_positives_upwards_cb, wff, tau_and, tau_or, tau_neg, tau_t, tau_f,
+		tau_and_sym, tau_or_sym, tau_neg_sym, wff_rule, wff_matcher, wff_body, wff_rec_relation, wff_ref, bf_eq_cb, bf_neq_cb,
+		wff_has_clashing_subformulas_cb, wff_has_subformula_cb, wff_remove_existential, wff_and, wff_neg, wff_xor, wff_conditional, wff_or, wff_all, wff_ex,
+		wff_imply, wff_equiv, wff_t, wff_f, bf_eq, bf_neq, bf_less, bf_less_equal, bf_greater, wff_ref_args,
+		_Rwff_ref_args_11, _Rwff_ref_args_12, wff_and_sym, wff_or_sym, wff_xor_sym, wff_conditional_sym, wff_neg_sym, wff_imply_sym, wff_equiv_sym, wff_all_sym,
+		_Rwff_all_13, wff_ex_sym, _Rwff_ex_14, bf, bf_equality_sym, bf_nequality_sym, bf_less_sym, bf_less_equal_sym, bf_greater_sym, bf_rule,
+		bf_matcher, bf_body, bf_rec_relation, bf_ref, bf_is_zero_cb, bf_is_one_cb, bf_has_clashing_subformulas_cb, bf_has_subformula_cb, bf_constant, bf_and,
+		bf_neg, bf_xor, bf_or, bf_all, bf_ex, bf_subs_cb, bf_t, bf_f, bf_ref_args, _Rbf_ref_args_15,
+		_Rbf_ref_args_16, bf_and_sym, bf_or_sym, bf_xor_sym, bf_neg_sym, bf_all_sym, _Rbf_all_17, bf_ex_sym, _Rbf_ex_18, constant,
+		binding, bf_and_cb, bf_or_cb, bf_xor_cb, bf_neg_cb, source_binding, named_binding, type, source, source0,
+		_Rsource_19, _Rsource_20, bf_cb_arg, bf_and_cb_sym, bf_or_cb_sym, bf_xor_cb_sym, bf_neg_cb_sym, bf_subs_cb_sym, bf_eq_cb_sym, wff_cb_arg,
+		bf_neq_cb_sym, bf_is_zero_cb_sym, bf_is_one_cb_sym, bf_has_clashing_subformulas_cb_sym, wff_has_clashing_subformulas_cb_sym, bf_has_subformula_cb_sym, wff_has_subformula_cb_sym, wff_remove_existential_cb_sym, tau_collapse_positives_cb_sym, tau_cb_arg,
+		tau_positives_upwards_cb_sym, input, inputs, _Rinputs_21, _Rinputs_22, main, rule, rules, _Rrules_23, _Rrules_24,
+		rec_relation, rec_relations, _Rrec_relations_25, _Rrec_relations_26, formula, library, builder, builder_head, builder_body, _Rbuilder_head_27,
+		_Rbuilder_head_28, gssotc, start, __neg_0, __neg_1, __neg_2, __neg_3, __neg_4, __neg_5,
 	};
 	size_t id(const std::basic_string<char>& name) { return nts.get(name); }
 private:
@@ -85,21 +85,21 @@ struct tau_parser {
 			"open_bracket", "close_bracket", "open_brace", "close_brace", "minus", "colon", "semicolon", "less", "comma", "sym",
 			"offsets", "step", "offset", "_Roffsets_8", "_Roffsets_9", "num", "capture", "shift", "timed_offset", "timed_step",
 			"timed_capture", "timed_shift", "variable", "var", "timed", "in", "out", "_Rtimed_10", "tau_rule", "tau_matcher",
-			"tau_body", "tau", "wff", "tau_and", "tau_or", "tau_neg", "tau_t", "tau_f", "tau_and_sym", "tau_or_sym",
-			"tau_neg_sym", "wff_rule", "wff_matcher", "wff_body", "wff_rec_relation", "wff_ref", "bf_eq_cb", "bf_neq_cb", "wff_has_clashing_subformulas_cb", "wff_has_subformula_cb",
-			"wff_remove_existential", "wff_and", "wff_neg", "wff_xor", "wff_conditional", "wff_or", "wff_all", "wff_ex", "wff_imply", "wff_equiv",
-			"wff_t", "wff_f", "bf_eq", "bf_neq", "bf_less", "bf_less_equal", "bf_greater", "wff_ref_args", "_Rwff_ref_args_11", "_Rwff_ref_args_12",
-			"wff_and_sym", "wff_or_sym", "wff_xor_sym", "wff_conditional_sym", "wff_neg_sym", "wff_imply_sym", "wff_equiv_sym", "wff_all_sym", "_Rwff_all_13", "wff_ex_sym",
-			"_Rwff_ex_14", "bf", "bf_equality_sym", "bf_nequality_sym", "bf_less_sym", "bf_less_equal_sym", "bf_greater_sym", "bf_rule", "bf_matcher", "bf_body",
-			"bf_rec_relation", "bf_ref", "bf_is_zero_cb", "bf_is_one_cb", "bf_has_clashing_subformulas_cb", "bf_has_subformula_cb", "bf_constant", "bf_and", "bf_neg", "bf_xor",
-			"bf_or", "bf_all", "bf_ex", "bf_subs_cb", "bf_t", "bf_f", "bf_ref_args", "_Rbf_ref_args_15", "_Rbf_ref_args_16", "bf_and_sym",
-			"bf_or_sym", "bf_xor_sym", "bf_neg_sym", "bf_all_sym", "_Rbf_all_17", "bf_ex_sym", "_Rbf_ex_18", "constant", "binding", "bf_and_cb",
-			"bf_or_cb", "bf_xor_cb", "bf_neg_cb", "source_binding", "named_binding", "type", "source", "source0", "_Rsource_19", "_Rsource_20",
-			"bf_cb_arg", "bf_and_cb_sym", "bf_or_cb_sym", "bf_xor_cb_sym", "bf_neg_cb_sym", "bf_subs_cb_sym", "bf_eq_cb_sym", "wff_cb_arg", "bf_neq_cb_sym", "bf_is_zero_cb_sym",
-			"bf_is_one_cb_sym", "bf_has_clashing_subformulas_cb_sym", "wff_has_clashing_subformulas_cb_sym", "bf_has_subformula_cb_sym", "wff_has_subformula_cb_sym", "wff_remove_existential_cb_sym", "input", "inputs", "_Rinputs_21", "_Rinputs_22",
-			"main", "rule", "rules", "_Rrules_23", "_Rrules_24", "rec_relation", "rec_relations", "_Rrec_relations_25", "_Rrec_relations_26", "formula",
-			"library", "builder", "builder_head", "builder_body", "_Rbuilder_head_27", "_Rbuilder_head_28", "gssotc", "start", "__neg_0", "__neg_1",
-			"__neg_2", "__neg_3", "__neg_4", "__neg_5",
+			"tau_body", "tau", "tau_collapse_positives_cb", "tau_positives_upwards_cb", "wff", "tau_and", "tau_or", "tau_neg", "tau_t", "tau_f",
+			"tau_and_sym", "tau_or_sym", "tau_neg_sym", "wff_rule", "wff_matcher", "wff_body", "wff_rec_relation", "wff_ref", "bf_eq_cb", "bf_neq_cb",
+			"wff_has_clashing_subformulas_cb", "wff_has_subformula_cb", "wff_remove_existential", "wff_and", "wff_neg", "wff_xor", "wff_conditional", "wff_or", "wff_all", "wff_ex",
+			"wff_imply", "wff_equiv", "wff_t", "wff_f", "bf_eq", "bf_neq", "bf_less", "bf_less_equal", "bf_greater", "wff_ref_args",
+			"_Rwff_ref_args_11", "_Rwff_ref_args_12", "wff_and_sym", "wff_or_sym", "wff_xor_sym", "wff_conditional_sym", "wff_neg_sym", "wff_imply_sym", "wff_equiv_sym", "wff_all_sym",
+			"_Rwff_all_13", "wff_ex_sym", "_Rwff_ex_14", "bf", "bf_equality_sym", "bf_nequality_sym", "bf_less_sym", "bf_less_equal_sym", "bf_greater_sym", "bf_rule",
+			"bf_matcher", "bf_body", "bf_rec_relation", "bf_ref", "bf_is_zero_cb", "bf_is_one_cb", "bf_has_clashing_subformulas_cb", "bf_has_subformula_cb", "bf_constant", "bf_and",
+			"bf_neg", "bf_xor", "bf_or", "bf_all", "bf_ex", "bf_subs_cb", "bf_t", "bf_f", "bf_ref_args", "_Rbf_ref_args_15",
+			"_Rbf_ref_args_16", "bf_and_sym", "bf_or_sym", "bf_xor_sym", "bf_neg_sym", "bf_all_sym", "_Rbf_all_17", "bf_ex_sym", "_Rbf_ex_18", "constant",
+			"binding", "bf_and_cb", "bf_or_cb", "bf_xor_cb", "bf_neg_cb", "source_binding", "named_binding", "type", "source", "source0",
+			"_Rsource_19", "_Rsource_20", "bf_cb_arg", "bf_and_cb_sym", "bf_or_cb_sym", "bf_xor_cb_sym", "bf_neg_cb_sym", "bf_subs_cb_sym", "bf_eq_cb_sym", "wff_cb_arg",
+			"bf_neq_cb_sym", "bf_is_zero_cb_sym", "bf_is_one_cb_sym", "bf_has_clashing_subformulas_cb_sym", "wff_has_clashing_subformulas_cb_sym", "bf_has_subformula_cb_sym", "wff_has_subformula_cb_sym", "wff_remove_existential_cb_sym", "tau_collapse_positives_cb_sym", "tau_cb_arg",
+			"tau_positives_upwards_cb_sym", "input", "inputs", "_Rinputs_21", "_Rinputs_22", "main", "rule", "rules", "_Rrules_23", "_Rrules_24",
+			"rec_relation", "rec_relations", "_Rrec_relations_25", "_Rrec_relations_26", "formula", "library", "builder", "builder_head", "builder_body", "_Rbuilder_head_27",
+			"_Rbuilder_head_28", "gssotc", "start", "__neg_0", "__neg_1", "__neg_2", "__neg_3", "__neg_4", "__neg_5",
 		}) nts.get(nt);
 		return nts;
 	}
@@ -166,19 +166,19 @@ struct tau_parser {
 		// _Rchar_punct_3 => esc q_bqstr.
 		q(nt(24), (nt(17)+nt(20)));
 		// __neg_0 => q_char.
-		q(nt(208), (nt(18)));
+		q(nt(213), (nt(18)));
 		// __neg_1 => q_str.
-		q(nt(209), (nt(19)));
+		q(nt(214), (nt(19)));
 		// __neg_2 => q_bqstr.
-		q(nt(210), (nt(20)));
+		q(nt(215), (nt(20)));
 		// __neg_3 => _Rchar_punct_1.
-		q(nt(211), (nt(22)));
+		q(nt(216), (nt(22)));
 		// __neg_4 => _Rchar_punct_2.
-		q(nt(212), (nt(23)));
+		q(nt(217), (nt(23)));
 		// __neg_5 => _Rchar_punct_3.
-		q(nt(213), (nt(24)));
+		q(nt(218), (nt(24)));
 		// char_punct => punct & ~( __neg_0 ) & ~( __neg_1 ) & ~( __neg_2 ) & ~( __neg_3 ) & ~( __neg_4 ) & ~( __neg_5 ).
-		q(nt(21), (nt(7)) & ~(nt(208)) & ~(nt(209)) & ~(nt(210)) & ~(nt(211)) & ~(nt(212)) & ~(nt(213)));
+		q(nt(21), (nt(7)) & ~(nt(213)) & ~(nt(214)) & ~(nt(215)) & ~(nt(216)) & ~(nt(217)) & ~(nt(218)));
 		// char0 => space.
 		q(nt(25), (nt(2)));
 		// char0 => alnum.
@@ -341,432 +341,444 @@ struct tau_parser {
 		q(nt(69), (nt(71)));
 		// tau_body => tau.
 		q(nt(70), (nt(71)));
+		// tau_body => tau_collapse_positives_cb.
+		q(nt(70), (nt(72)));
+		// tau_body => tau_positives_upwards_cb.
+		q(nt(70), (nt(73)));
 		// tau => wff.
-		q(nt(71), (nt(72)));
+		q(nt(71), (nt(74)));
 		// tau => tau_and.
-		q(nt(71), (nt(73)));
+		q(nt(71), (nt(75)));
 		// tau => tau_or.
-		q(nt(71), (nt(74)));
+		q(nt(71), (nt(76)));
 		// tau => tau_neg.
-		q(nt(71), (nt(75)));
+		q(nt(71), (nt(77)));
 		// tau => tau_t.
-		q(nt(71), (nt(76)));
+		q(nt(71), (nt(78)));
 		// tau => tau_f.
-		q(nt(71), (nt(77)));
+		q(nt(71), (nt(79)));
 		// tau_and => open_parenthesis tau tau_and_sym tau close_parenthesis.
-		q(nt(73), (nt(38)+nt(71)+nt(78)+nt(71)+nt(39)));
+		q(nt(75), (nt(38)+nt(71)+nt(80)+nt(71)+nt(39)));
 		// tau_or => open_parenthesis tau tau_or_sym tau close_parenthesis.
-		q(nt(74), (nt(38)+nt(71)+nt(79)+nt(71)+nt(39)));
+		q(nt(76), (nt(38)+nt(71)+nt(81)+nt(71)+nt(39)));
 		// tau_neg => tau_neg_sym tau.
-		q(nt(75), (nt(80)+nt(71)));
+		q(nt(77), (nt(82)+nt(71)));
 		// tau_t => ws 'T' ws.
-		q(nt(76), (nt(13)+t(45)+nt(13)));
+		q(nt(78), (nt(13)+t(45)+nt(13)));
 		// tau_f => ws 'F' ws.
-		q(nt(77), (nt(13)+t(46)+nt(13)));
+		q(nt(79), (nt(13)+t(46)+nt(13)));
 		// tau_and_sym => ws '&' '&' '&' ws.
-		q(nt(78), (nt(13)+t(47)+t(47)+t(47)+nt(13)));
+		q(nt(80), (nt(13)+t(47)+t(47)+t(47)+nt(13)));
 		// tau_or_sym => ws '|' '|' '|' ws.
-		q(nt(79), (nt(13)+t(48)+t(48)+t(48)+nt(13)));
+		q(nt(81), (nt(13)+t(48)+t(48)+t(48)+nt(13)));
 		// tau_neg_sym => ws '%' ws.
-		q(nt(80), (nt(13)+t(49)+nt(13)));
+		q(nt(82), (nt(13)+t(49)+nt(13)));
 		// wff_rule => wff_matcher definition wff_body dot.
-		q(nt(81), (nt(82)+nt(36)+nt(83)+nt(37)));
+		q(nt(83), (nt(84)+nt(36)+nt(85)+nt(37)));
 		// wff_rec_relation => wff_ref definition wff dot.
-		q(nt(84), (nt(85)+nt(36)+nt(72)+nt(37)));
+		q(nt(86), (nt(87)+nt(36)+nt(74)+nt(37)));
 		// wff_matcher => wff.
-		q(nt(82), (nt(72)));
+		q(nt(84), (nt(74)));
 		// wff_matcher => wff_ref.
-		q(nt(82), (nt(85)));
+		q(nt(84), (nt(87)));
 		// wff_body => wff.
-		q(nt(83), (nt(72)));
+		q(nt(85), (nt(74)));
 		// wff_body => bf_eq_cb.
-		q(nt(83), (nt(86)));
+		q(nt(85), (nt(88)));
 		// wff_body => bf_neq_cb.
-		q(nt(83), (nt(87)));
+		q(nt(85), (nt(89)));
 		// wff_body => wff_has_clashing_subformulas_cb.
-		q(nt(83), (nt(88)));
+		q(nt(85), (nt(90)));
 		// wff_body => wff_has_subformula_cb.
-		q(nt(83), (nt(89)));
+		q(nt(85), (nt(91)));
 		// wff_body => wff_remove_existential.
-		q(nt(83), (nt(90)));
+		q(nt(85), (nt(92)));
 		// wff => capture.
-		q(nt(72), (nt(56)));
+		q(nt(74), (nt(56)));
 		// wff => wff_ref.
-		q(nt(72), (nt(85)));
+		q(nt(74), (nt(87)));
 		// wff => wff_and.
-		q(nt(72), (nt(91)));
+		q(nt(74), (nt(93)));
 		// wff => wff_neg.
-		q(nt(72), (nt(92)));
+		q(nt(74), (nt(94)));
 		// wff => wff_xor.
-		q(nt(72), (nt(93)));
+		q(nt(74), (nt(95)));
 		// wff => wff_conditional.
-		q(nt(72), (nt(94)));
+		q(nt(74), (nt(96)));
 		// wff => wff_or.
-		q(nt(72), (nt(95)));
+		q(nt(74), (nt(97)));
 		// wff => wff_all.
-		q(nt(72), (nt(96)));
+		q(nt(74), (nt(98)));
 		// wff => wff_ex.
-		q(nt(72), (nt(97)));
+		q(nt(74), (nt(99)));
 		// wff => wff_imply.
-		q(nt(72), (nt(98)));
+		q(nt(74), (nt(100)));
 		// wff => wff_equiv.
-		q(nt(72), (nt(99)));
+		q(nt(74), (nt(101)));
 		// wff => wff_t.
-		q(nt(72), (nt(100)));
+		q(nt(74), (nt(102)));
 		// wff => wff_f.
-		q(nt(72), (nt(101)));
+		q(nt(74), (nt(103)));
 		// wff => bf_eq.
-		q(nt(72), (nt(102)));
+		q(nt(74), (nt(104)));
 		// wff => bf_neq.
-		q(nt(72), (nt(103)));
+		q(nt(74), (nt(105)));
 		// wff => bf_less.
-		q(nt(72), (nt(104)));
+		q(nt(74), (nt(106)));
 		// wff => bf_less_equal.
-		q(nt(72), (nt(105)));
+		q(nt(74), (nt(107)));
 		// wff => bf_greater.
-		q(nt(72), (nt(106)));
+		q(nt(74), (nt(108)));
 		// wff_ref => sym offsets wff_ref_args.
-		q(nt(85), (nt(49)+nt(50)+nt(107)));
+		q(nt(87), (nt(49)+nt(50)+nt(109)));
 		// _Rwff_ref_args_11 => variable.
-		q(nt(108), (nt(62)));
+		q(nt(110), (nt(62)));
 		// _Rwff_ref_args_12 => null.
-		q(nt(109), (nul));
+		q(nt(111), (nul));
 		// _Rwff_ref_args_12 => _Rwff_ref_args_11 _Rwff_ref_args_12.
-		q(nt(109), (nt(108)+nt(109)));
+		q(nt(111), (nt(110)+nt(111)));
 		// wff_ref_args => open_parenthesis _Rwff_ref_args_12 close_parenthesis.
-		q(nt(107), (nt(38)+nt(109)+nt(39)));
+		q(nt(109), (nt(38)+nt(111)+nt(39)));
 		// wff_and => open_parenthesis wff wff_and_sym wff close_parenthesis.
-		q(nt(91), (nt(38)+nt(72)+nt(110)+nt(72)+nt(39)));
+		q(nt(93), (nt(38)+nt(74)+nt(112)+nt(74)+nt(39)));
 		// wff_or => open_parenthesis wff wff_or_sym wff close_parenthesis.
-		q(nt(95), (nt(38)+nt(72)+nt(111)+nt(72)+nt(39)));
+		q(nt(97), (nt(38)+nt(74)+nt(113)+nt(74)+nt(39)));
 		// wff_xor => open_parenthesis wff wff_xor_sym wff close_parenthesis.
-		q(nt(93), (nt(38)+nt(72)+nt(112)+nt(72)+nt(39)));
+		q(nt(95), (nt(38)+nt(74)+nt(114)+nt(74)+nt(39)));
 		// wff_conditional => open_parenthesis wff wff_conditional_sym wff colon wff close_parenthesis.
-		q(nt(94), (nt(38)+nt(72)+nt(113)+nt(72)+nt(45)+nt(72)+nt(39)));
+		q(nt(96), (nt(38)+nt(74)+nt(115)+nt(74)+nt(45)+nt(74)+nt(39)));
 		// wff_neg => wff_neg_sym wff.
-		q(nt(92), (nt(114)+nt(72)));
+		q(nt(94), (nt(116)+nt(74)));
 		// wff_imply => open_parenthesis wff wff_imply_sym wff close_parenthesis.
-		q(nt(98), (nt(38)+nt(72)+nt(115)+nt(72)+nt(39)));
+		q(nt(100), (nt(38)+nt(74)+nt(117)+nt(74)+nt(39)));
 		// wff_equiv => open_parenthesis wff wff_equiv_sym wff close_parenthesis.
-		q(nt(99), (nt(38)+nt(72)+nt(116)+nt(72)+nt(39)));
+		q(nt(101), (nt(38)+nt(74)+nt(118)+nt(74)+nt(39)));
 		// _Rwff_all_13 => capture.
-		q(nt(118), (nt(56)));
+		q(nt(120), (nt(56)));
 		// _Rwff_all_13 => variable.
-		q(nt(118), (nt(62)));
+		q(nt(120), (nt(62)));
 		// wff_all => wff_all_sym _Rwff_all_13 ws_required wff.
-		q(nt(96), (nt(117)+nt(118)+nt(12)+nt(72)));
+		q(nt(98), (nt(119)+nt(120)+nt(12)+nt(74)));
 		// _Rwff_ex_14 => capture.
-		q(nt(120), (nt(56)));
+		q(nt(122), (nt(56)));
 		// _Rwff_ex_14 => variable.
-		q(nt(120), (nt(62)));
+		q(nt(122), (nt(62)));
 		// wff_ex => wff_ex_sym ws_required _Rwff_ex_14 ws_required wff.
-		q(nt(97), (nt(119)+nt(12)+nt(120)+nt(12)+nt(72)));
+		q(nt(99), (nt(121)+nt(12)+nt(122)+nt(12)+nt(74)));
 		// bf_eq => open_parenthesis bf bf_equality_sym bf close_parenthesis.
-		q(nt(102), (nt(38)+nt(121)+nt(122)+nt(121)+nt(39)));
+		q(nt(104), (nt(38)+nt(123)+nt(124)+nt(123)+nt(39)));
 		// bf_neq => open_parenthesis bf bf_nequality_sym bf close_parenthesis.
-		q(nt(103), (nt(38)+nt(121)+nt(123)+nt(121)+nt(39)));
+		q(nt(105), (nt(38)+nt(123)+nt(125)+nt(123)+nt(39)));
 		// bf_less => open_parenthesis bf bf_less_sym bf close_parenthesis.
-		q(nt(104), (nt(38)+nt(121)+nt(124)+nt(121)+nt(39)));
+		q(nt(106), (nt(38)+nt(123)+nt(126)+nt(123)+nt(39)));
 		// bf_less_equal => open_parenthesis bf bf_less_equal_sym bf close_parenthesis.
-		q(nt(105), (nt(38)+nt(121)+nt(125)+nt(121)+nt(39)));
+		q(nt(107), (nt(38)+nt(123)+nt(127)+nt(123)+nt(39)));
 		// bf_greater => open_parenthesis bf bf_greater_sym bf close_parenthesis.
-		q(nt(106), (nt(38)+nt(121)+nt(126)+nt(121)+nt(39)));
+		q(nt(108), (nt(38)+nt(123)+nt(128)+nt(123)+nt(39)));
 		// wff_and_sym => ws '&' '&' ws.
-		q(nt(110), (nt(13)+t(47)+t(47)+nt(13)));
+		q(nt(112), (nt(13)+t(47)+t(47)+nt(13)));
 		// wff_or_sym => ws '|' '|' ws.
-		q(nt(111), (nt(13)+t(48)+t(48)+nt(13)));
+		q(nt(113), (nt(13)+t(48)+t(48)+nt(13)));
 		// wff_xor_sym => ws '^' ws.
-		q(nt(112), (nt(13)+t(50)+nt(13)));
+		q(nt(114), (nt(13)+t(50)+nt(13)));
 		// wff_conditional_sym => ws '?' ws.
-		q(nt(113), (nt(13)+t(43)+nt(13)));
+		q(nt(115), (nt(13)+t(43)+nt(13)));
 		// wff_neg_sym => ws '!' ws.
-		q(nt(114), (nt(13)+t(51)+nt(13)));
+		q(nt(116), (nt(13)+t(51)+nt(13)));
 		// wff_imply_sym => ws '-' '>' ws.
-		q(nt(115), (nt(13)+t(38)+t(52)+nt(13)));
+		q(nt(117), (nt(13)+t(38)+t(52)+nt(13)));
 		// wff_equiv_sym => ws '<' '-' '>' ws.
-		q(nt(116), (nt(13)+t(40)+t(38)+t(52)+nt(13)));
+		q(nt(118), (nt(13)+t(40)+t(38)+t(52)+nt(13)));
 		// wff_all_sym => ws 'a' 'l' 'l' ws.
-		q(nt(117), (nt(13)+t(10)+t(11)+t(11)+nt(13)));
+		q(nt(119), (nt(13)+t(10)+t(11)+t(11)+nt(13)));
 		// wff_ex_sym => ws 'e' 'x' ws.
-		q(nt(119), (nt(13)+t(24)+t(5)+nt(13)));
+		q(nt(121), (nt(13)+t(24)+t(5)+nt(13)));
 		// wff_t => ws 'T' ws.
-		q(nt(100), (nt(13)+t(45)+nt(13)));
+		q(nt(102), (nt(13)+t(45)+nt(13)));
 		// wff_f => ws 'F' ws.
-		q(nt(101), (nt(13)+t(46)+nt(13)));
+		q(nt(103), (nt(13)+t(46)+nt(13)));
 		// bf_rule => bf_matcher definition bf_body dot.
-		q(nt(127), (nt(128)+nt(36)+nt(129)+nt(37)));
+		q(nt(129), (nt(130)+nt(36)+nt(131)+nt(37)));
 		// bf_rec_relation => bf_ref definition bf dot.
-		q(nt(130), (nt(131)+nt(36)+nt(121)+nt(37)));
+		q(nt(132), (nt(133)+nt(36)+nt(123)+nt(37)));
 		// bf_matcher => bf.
-		q(nt(128), (nt(121)));
+		q(nt(130), (nt(123)));
 		// bf_body => bf.
-		q(nt(129), (nt(121)));
+		q(nt(131), (nt(123)));
 		// bf_body => bf_is_zero_cb.
-		q(nt(129), (nt(132)));
+		q(nt(131), (nt(134)));
 		// bf_body => bf_is_one_cb.
-		q(nt(129), (nt(133)));
+		q(nt(131), (nt(135)));
 		// bf_body => bf_has_clashing_subformulas_cb.
-		q(nt(129), (nt(134)));
+		q(nt(131), (nt(136)));
 		// bf_body => bf_has_subformula_cb.
-		q(nt(129), (nt(135)));
+		q(nt(131), (nt(137)));
 		// bf => capture.
-		q(nt(121), (nt(56)));
+		q(nt(123), (nt(56)));
 		// bf => variable.
-		q(nt(121), (nt(62)));
+		q(nt(123), (nt(62)));
 		// bf => bf_ref.
-		q(nt(121), (nt(131)));
+		q(nt(123), (nt(133)));
 		// bf => bf_constant.
-		q(nt(121), (nt(136)));
+		q(nt(123), (nt(138)));
 		// bf => bf_and.
-		q(nt(121), (nt(137)));
+		q(nt(123), (nt(139)));
 		// bf => bf_neg.
-		q(nt(121), (nt(138)));
+		q(nt(123), (nt(140)));
 		// bf => bf_xor.
-		q(nt(121), (nt(139)));
+		q(nt(123), (nt(141)));
 		// bf => bf_or.
-		q(nt(121), (nt(140)));
+		q(nt(123), (nt(142)));
 		// bf => bf_all.
-		q(nt(121), (nt(141)));
+		q(nt(123), (nt(143)));
 		// bf => bf_ex.
-		q(nt(121), (nt(142)));
+		q(nt(123), (nt(144)));
 		// bf => bf_subs_cb.
-		q(nt(121), (nt(143)));
+		q(nt(123), (nt(145)));
 		// bf => bf_t.
-		q(nt(121), (nt(144)));
+		q(nt(123), (nt(146)));
 		// bf => bf_f.
-		q(nt(121), (nt(145)));
+		q(nt(123), (nt(147)));
 		// bf_ref => sym offsets bf_ref_args.
-		q(nt(131), (nt(49)+nt(50)+nt(146)));
+		q(nt(133), (nt(49)+nt(50)+nt(148)));
 		// _Rbf_ref_args_15 => variable.
-		q(nt(147), (nt(62)));
+		q(nt(149), (nt(62)));
 		// _Rbf_ref_args_16 => null.
-		q(nt(148), (nul));
+		q(nt(150), (nul));
 		// _Rbf_ref_args_16 => _Rbf_ref_args_15 _Rbf_ref_args_16.
-		q(nt(148), (nt(147)+nt(148)));
+		q(nt(150), (nt(149)+nt(150)));
 		// bf_ref_args => open_parenthesis _Rbf_ref_args_16 close_parenthesis.
-		q(nt(146), (nt(38)+nt(148)+nt(39)));
+		q(nt(148), (nt(38)+nt(150)+nt(39)));
 		// bf_and => open_parenthesis bf bf_and_sym bf close_parenthesis.
-		q(nt(137), (nt(38)+nt(121)+nt(149)+nt(121)+nt(39)));
+		q(nt(139), (nt(38)+nt(123)+nt(151)+nt(123)+nt(39)));
 		// bf_or => open_parenthesis bf bf_or_sym bf close_parenthesis.
-		q(nt(140), (nt(38)+nt(121)+nt(150)+nt(121)+nt(39)));
+		q(nt(142), (nt(38)+nt(123)+nt(152)+nt(123)+nt(39)));
 		// bf_xor => open_parenthesis bf bf_xor_sym ws bf close_parenthesis.
-		q(nt(139), (nt(38)+nt(121)+nt(151)+nt(13)+nt(121)+nt(39)));
+		q(nt(141), (nt(38)+nt(123)+nt(153)+nt(13)+nt(123)+nt(39)));
 		// bf_neg => bf_neg_sym bf.
-		q(nt(138), (nt(152)+nt(121)));
+		q(nt(140), (nt(154)+nt(123)));
 		// _Rbf_all_17 => capture.
-		q(nt(154), (nt(56)));
+		q(nt(156), (nt(56)));
 		// _Rbf_all_17 => variable.
-		q(nt(154), (nt(62)));
+		q(nt(156), (nt(62)));
 		// bf_all => bf_all_sym ws_required _Rbf_all_17 ws_required bf.
-		q(nt(141), (nt(153)+nt(12)+nt(154)+nt(12)+nt(121)));
+		q(nt(143), (nt(155)+nt(12)+nt(156)+nt(12)+nt(123)));
 		// _Rbf_ex_18 => capture.
-		q(nt(156), (nt(56)));
+		q(nt(158), (nt(56)));
 		// _Rbf_ex_18 => variable.
-		q(nt(156), (nt(62)));
+		q(nt(158), (nt(62)));
 		// bf_ex => bf_ex_sym ws_required _Rbf_ex_18 ws_required bf.
-		q(nt(142), (nt(155)+nt(12)+nt(156)+nt(12)+nt(121)));
+		q(nt(144), (nt(157)+nt(12)+nt(158)+nt(12)+nt(123)));
 		// bf_and_sym => ws '&' ws.
-		q(nt(149), (nt(13)+t(47)+nt(13)));
+		q(nt(151), (nt(13)+t(47)+nt(13)));
 		// bf_or_sym => ws '|' ws.
-		q(nt(150), (nt(13)+t(48)+nt(13)));
+		q(nt(152), (nt(13)+t(48)+nt(13)));
 		// bf_xor_sym => ws '+' ws.
-		q(nt(151), (nt(13)+t(53)+nt(13)));
+		q(nt(153), (nt(13)+t(53)+nt(13)));
 		// bf_neg_sym => ws '~' ws.
-		q(nt(152), (nt(13)+t(54)+nt(13)));
+		q(nt(154), (nt(13)+t(54)+nt(13)));
 		// bf_equality_sym => ws '=' ws.
-		q(nt(122), (nt(13)+t(30)+nt(13)));
+		q(nt(124), (nt(13)+t(30)+nt(13)));
 		// bf_nequality_sym => ws '!' '=' ws.
-		q(nt(123), (nt(13)+t(51)+t(30)+nt(13)));
+		q(nt(125), (nt(13)+t(51)+t(30)+nt(13)));
 		// bf_less_sym => ws '<' ws.
-		q(nt(124), (nt(13)+t(40)+nt(13)));
+		q(nt(126), (nt(13)+t(40)+nt(13)));
 		// bf_less_equal_sym => ws '<' '=' ws.
-		q(nt(125), (nt(13)+t(40)+t(30)+nt(13)));
+		q(nt(127), (nt(13)+t(40)+t(30)+nt(13)));
 		// bf_greater_sym => ws '>' ws.
-		q(nt(126), (nt(13)+t(52)+nt(13)));
+		q(nt(128), (nt(13)+t(52)+nt(13)));
 		// bf_all_sym => ws 'f' 'a' 'l' 'l' ws.
-		q(nt(153), (nt(13)+t(26)+t(10)+t(11)+t(11)+nt(13)));
+		q(nt(155), (nt(13)+t(26)+t(10)+t(11)+t(11)+nt(13)));
 		// bf_ex_sym => ws 'f' 'e' 'x' ws.
-		q(nt(155), (nt(13)+t(26)+t(24)+t(5)+nt(13)));
+		q(nt(157), (nt(13)+t(26)+t(24)+t(5)+nt(13)));
 		// bf_t => ws '1' ws.
-		q(nt(144), (nt(13)+t(55)+nt(13)));
+		q(nt(146), (nt(13)+t(55)+nt(13)));
 		// bf_f => ws '0' ws.
-		q(nt(145), (nt(13)+t(56)+nt(13)));
+		q(nt(147), (nt(13)+t(56)+nt(13)));
 		// bf_constant => open_brace constant close_brace.
-		q(nt(136), (nt(42)+nt(157)+nt(43)));
+		q(nt(138), (nt(42)+nt(159)+nt(43)));
 		// constant => capture.
-		q(nt(157), (nt(56)));
+		q(nt(159), (nt(56)));
 		// constant => binding.
-		q(nt(157), (nt(158)));
+		q(nt(159), (nt(160)));
 		// constant => bf_and_cb.
-		q(nt(157), (nt(159)));
+		q(nt(159), (nt(161)));
 		// constant => bf_or_cb.
-		q(nt(157), (nt(160)));
+		q(nt(159), (nt(162)));
 		// constant => bf_xor_cb.
-		q(nt(157), (nt(161)));
+		q(nt(159), (nt(163)));
 		// constant => bf_neg_cb.
-		q(nt(157), (nt(162)));
+		q(nt(159), (nt(164)));
 		// binding => source_binding.
-		q(nt(158), (nt(163)));
+		q(nt(160), (nt(165)));
 		// binding => named_binding.
-		q(nt(158), (nt(164)));
+		q(nt(160), (nt(166)));
 		// named_binding => chars.
-		q(nt(164), (nt(29)));
+		q(nt(166), (nt(29)));
 		// source_binding => type colon source.
-		q(nt(163), (nt(165)+nt(45)+nt(166)));
+		q(nt(165), (nt(167)+nt(45)+nt(168)));
 		// type => null.
-		q(nt(165), (nul));
+		q(nt(167), (nul));
 		// type => chars.
-		q(nt(165), (nt(29)));
+		q(nt(167), (nt(29)));
 		// source0 => space.
-		q(nt(167), (nt(2)));
+		q(nt(169), (nt(2)));
 		// source0 => alnum.
-		q(nt(167), (nt(6)));
+		q(nt(169), (nt(6)));
 		// source0 => char_escape_encode.
-		q(nt(167), (nt(16)));
+		q(nt(169), (nt(16)));
 		// source0 => char_punct.
-		q(nt(167), (nt(21)));
+		q(nt(169), (nt(21)));
 		// _Rsource_19 => source0.
-		q(nt(168), (nt(167)));
+		q(nt(170), (nt(169)));
 		// _Rsource_20 => _Rsource_19.
-		q(nt(169), (nt(168)));
+		q(nt(171), (nt(170)));
 		// _Rsource_20 => _Rsource_19 _Rsource_20.
-		q(nt(169), (nt(168)+nt(169)));
+		q(nt(171), (nt(170)+nt(171)));
 		// source => _Rsource_20.
-		q(nt(166), (nt(169)));
+		q(nt(168), (nt(171)));
 		// bf_and_cb => bf_cb_arg bf_and_cb_sym bf_cb_arg.
-		q(nt(159), (nt(170)+nt(171)+nt(170)));
+		q(nt(161), (nt(172)+nt(173)+nt(172)));
 		// bf_or_cb => bf_cb_arg bf_or_cb_sym bf_cb_arg.
-		q(nt(160), (nt(170)+nt(172)+nt(170)));
+		q(nt(162), (nt(172)+nt(174)+nt(172)));
 		// bf_xor_cb => bf_cb_arg bf_xor_cb_sym bf_cb_arg.
-		q(nt(161), (nt(170)+nt(173)+nt(170)));
+		q(nt(163), (nt(172)+nt(175)+nt(172)));
 		// bf_neg_cb => bf_neg_cb_sym bf_cb_arg.
-		q(nt(162), (nt(174)+nt(170)));
+		q(nt(164), (nt(176)+nt(172)));
 		// bf_subs_cb => bf_subs_cb_sym bf_cb_arg ws_required bf_cb_arg ws_required bf_cb_arg.
-		q(nt(143), (nt(175)+nt(170)+nt(12)+nt(170)+nt(12)+nt(170)));
+		q(nt(145), (nt(177)+nt(172)+nt(12)+nt(172)+nt(12)+nt(172)));
 		// bf_eq_cb => bf_eq_cb_sym bf_cb_arg ws_required wff_cb_arg ws_required wff_cb_arg.
-		q(nt(86), (nt(176)+nt(170)+nt(12)+nt(177)+nt(12)+nt(177)));
+		q(nt(88), (nt(178)+nt(172)+nt(12)+nt(179)+nt(12)+nt(179)));
 		// bf_neq_cb => bf_neq_cb_sym bf_cb_arg ws_required wff_cb_arg ws_required wff_cb_arg.
-		q(nt(87), (nt(178)+nt(170)+nt(12)+nt(177)+nt(12)+nt(177)));
+		q(nt(89), (nt(180)+nt(172)+nt(12)+nt(179)+nt(12)+nt(179)));
 		// bf_is_zero_cb => bf_is_zero_cb_sym bf_cb_arg ws_required bf_cb_arg.
-		q(nt(132), (nt(179)+nt(170)+nt(12)+nt(170)));
+		q(nt(134), (nt(181)+nt(172)+nt(12)+nt(172)));
 		// bf_is_one_cb => bf_is_one_cb_sym bf_cb_arg ws_required bf_cb_arg.
-		q(nt(133), (nt(180)+nt(170)+nt(12)+nt(170)));
+		q(nt(135), (nt(182)+nt(172)+nt(12)+nt(172)));
 		// bf_has_clashing_subformulas_cb => bf_has_clashing_subformulas_cb_sym bf_cb_arg ws_required bf_cb_arg.
-		q(nt(134), (nt(181)+nt(170)+nt(12)+nt(170)));
+		q(nt(136), (nt(183)+nt(172)+nt(12)+nt(172)));
 		// wff_has_clashing_subformulas_cb => wff_has_clashing_subformulas_cb_sym wff_cb_arg ws_required wff_cb_arg.
-		q(nt(88), (nt(182)+nt(177)+nt(12)+nt(177)));
+		q(nt(90), (nt(184)+nt(179)+nt(12)+nt(179)));
 		// bf_has_subformula_cb => bf_has_subformula_cb_sym bf_cb_arg ws_required bf_cb_arg ws_required bf_cb_arg.
-		q(nt(135), (nt(183)+nt(170)+nt(12)+nt(170)+nt(12)+nt(170)));
+		q(nt(137), (nt(185)+nt(172)+nt(12)+nt(172)+nt(12)+nt(172)));
 		// wff_has_subformula_cb => wff_has_subformula_cb_sym wff_cb_arg ws_required wff_cb_arg ws_required wff_cb_arg.
-		q(nt(89), (nt(184)+nt(177)+nt(12)+nt(177)+nt(12)+nt(177)));
+		q(nt(91), (nt(186)+nt(179)+nt(12)+nt(179)+nt(12)+nt(179)));
 		// wff_remove_existential => wff_remove_existential_cb_sym wff_cb_arg ws_required wff_cb_arg.
-		q(nt(90), (nt(185)+nt(177)+nt(12)+nt(177)));
+		q(nt(92), (nt(187)+nt(179)+nt(12)+nt(179)));
 		// bf_cb_arg => capture.
-		q(nt(170), (nt(56)));
+		q(nt(172), (nt(56)));
 		// bf_cb_arg => bf.
-		q(nt(170), (nt(121)));
+		q(nt(172), (nt(123)));
 		// wff_cb_arg => capture.
-		q(nt(177), (nt(56)));
+		q(nt(179), (nt(56)));
 		// wff_cb_arg => wff.
-		q(nt(177), (nt(72)));
+		q(nt(179), (nt(74)));
 		// bf_and_cb_sym => ws 'b' 'f' '_' 'a' 'n' 'd' '_' 'c' 'b' ws.
-		q(nt(171), (nt(13)+t(16)+t(26)+t(44)+t(10)+t(12)+t(21)+t(44)+t(18)+t(16)+nt(13)));
+		q(nt(173), (nt(13)+t(16)+t(26)+t(44)+t(10)+t(12)+t(21)+t(44)+t(18)+t(16)+nt(13)));
 		// bf_or_cb_sym => ws 'b' 'f' '_' 'o' 'r' '_' 'c' 'b' ws.
-		q(nt(172), (nt(13)+t(16)+t(26)+t(44)+t(25)+t(20)+t(44)+t(18)+t(16)+nt(13)));
+		q(nt(174), (nt(13)+t(16)+t(26)+t(44)+t(25)+t(20)+t(44)+t(18)+t(16)+nt(13)));
 		// bf_xor_cb_sym => ws 'b' 'f' '_' 'x' 'o' 'r' '_' 'c' 'b' ws.
-		q(nt(173), (nt(13)+t(16)+t(26)+t(44)+t(5)+t(25)+t(20)+t(44)+t(18)+t(16)+nt(13)));
+		q(nt(175), (nt(13)+t(16)+t(26)+t(44)+t(5)+t(25)+t(20)+t(44)+t(18)+t(16)+nt(13)));
 		// bf_neg_cb_sym => ws 'b' 'f' '_' 'n' 'e' 'g' '_' 'c' 'b' ws.
-		q(nt(174), (nt(13)+t(16)+t(26)+t(44)+t(12)+t(24)+t(23)+t(44)+t(18)+t(16)+nt(13)));
+		q(nt(176), (nt(13)+t(16)+t(26)+t(44)+t(12)+t(24)+t(23)+t(44)+t(18)+t(16)+nt(13)));
 		// bf_subs_cb_sym => ws 'b' 'f' '_' 's' 'u' 'b' 's' '_' 'c' 'b' ws.
-		q(nt(175), (nt(13)+t(16)+t(26)+t(44)+t(28)+t(6)+t(16)+t(28)+t(44)+t(18)+t(16)+nt(13)));
+		q(nt(177), (nt(13)+t(16)+t(26)+t(44)+t(28)+t(6)+t(16)+t(28)+t(44)+t(18)+t(16)+nt(13)));
 		// bf_eq_cb_sym => ws 'b' 'f' '_' 'e' 'q' '_' 'c' 'b' ws.
-		q(nt(176), (nt(13)+t(16)+t(26)+t(44)+t(24)+t(57)+t(44)+t(18)+t(16)+nt(13)));
+		q(nt(178), (nt(13)+t(16)+t(26)+t(44)+t(24)+t(57)+t(44)+t(18)+t(16)+nt(13)));
 		// bf_neq_cb_sym => ws 'b' 'f' '_' 'n' 'e' 'q' '_' 'c' 'b' ws.
-		q(nt(178), (nt(13)+t(16)+t(26)+t(44)+t(12)+t(24)+t(57)+t(44)+t(18)+t(16)+nt(13)));
+		q(nt(180), (nt(13)+t(16)+t(26)+t(44)+t(12)+t(24)+t(57)+t(44)+t(18)+t(16)+nt(13)));
 		// bf_is_zero_cb_sym => ws 'b' 'f' '_' 'i' 's' '_' 'z' 'e' 'r' 'o' '_' 'c' 'b' ws.
-		q(nt(179), (nt(13)+t(16)+t(26)+t(44)+t(22)+t(28)+t(44)+t(58)+t(24)+t(20)+t(25)+t(44)+t(18)+t(16)+nt(13)));
+		q(nt(181), (nt(13)+t(16)+t(26)+t(44)+t(22)+t(28)+t(44)+t(58)+t(24)+t(20)+t(25)+t(44)+t(18)+t(16)+nt(13)));
 		// bf_is_one_cb_sym => ws 'b' 'f' '_' 'i' 's' '_' 'o' 'n' 'e' '_' 'c' 'b' ws.
-		q(nt(180), (nt(13)+t(16)+t(26)+t(44)+t(22)+t(28)+t(44)+t(25)+t(12)+t(24)+t(44)+t(18)+t(16)+nt(13)));
+		q(nt(182), (nt(13)+t(16)+t(26)+t(44)+t(22)+t(28)+t(44)+t(25)+t(12)+t(24)+t(44)+t(18)+t(16)+nt(13)));
 		// bf_has_clashing_subformulas_cb_sym => ws 'b' 'f' '_' 'h' 'a' 's' '_' 'c' 'l' 'a' 's' 'h' 'i' 'n' 'g' '_' 's' 'u' 'b' 'f' 'o' 'r' 'm' 'u' 'l' 'a' 's' '_' 'c' 'b' ws.
-		q(nt(181), (nt(13)+t(16)+t(26)+t(44)+t(15)+t(10)+t(28)+t(44)+t(18)+t(11)+t(10)+t(28)+t(15)+t(22)+t(12)+t(23)+t(44)+t(28)+t(6)+t(16)+t(26)+t(25)+t(20)+t(13)+t(6)+t(11)+t(10)+t(28)+t(44)+t(18)+t(16)+nt(13)));
+		q(nt(183), (nt(13)+t(16)+t(26)+t(44)+t(15)+t(10)+t(28)+t(44)+t(18)+t(11)+t(10)+t(28)+t(15)+t(22)+t(12)+t(23)+t(44)+t(28)+t(6)+t(16)+t(26)+t(25)+t(20)+t(13)+t(6)+t(11)+t(10)+t(28)+t(44)+t(18)+t(16)+nt(13)));
 		// bf_has_subformula_cb_sym => ws 'b' 'f' '_' 'h' 'a' 's' '_' 's' 'u' 'b' 'f' 'o' 'r' 'm' 'u' 'l' 'a' '_' 'c' 'b' ws.
-		q(nt(183), (nt(13)+t(16)+t(26)+t(44)+t(15)+t(10)+t(28)+t(44)+t(28)+t(6)+t(16)+t(26)+t(25)+t(20)+t(13)+t(6)+t(11)+t(10)+t(44)+t(18)+t(16)+nt(13)));
+		q(nt(185), (nt(13)+t(16)+t(26)+t(44)+t(15)+t(10)+t(28)+t(44)+t(28)+t(6)+t(16)+t(26)+t(25)+t(20)+t(13)+t(6)+t(11)+t(10)+t(44)+t(18)+t(16)+nt(13)));
 		// wff_has_clashing_subformulas_cb_sym => ws 'w' 'f' 'f' '_' 'h' 'a' 's' '_' 'c' 'l' 'a' 's' 'h' 'i' 'n' 'g' '_' 's' 'u' 'b' 'f' 'o' 'r' 'm' 'u' 'l' 'a' 's' '_' 'c' 'b' ws.
-		q(nt(182), (nt(13)+t(27)+t(26)+t(26)+t(44)+t(15)+t(10)+t(28)+t(44)+t(18)+t(11)+t(10)+t(28)+t(15)+t(22)+t(12)+t(23)+t(44)+t(28)+t(6)+t(16)+t(26)+t(25)+t(20)+t(13)+t(6)+t(11)+t(10)+t(28)+t(44)+t(18)+t(16)+nt(13)));
+		q(nt(184), (nt(13)+t(27)+t(26)+t(26)+t(44)+t(15)+t(10)+t(28)+t(44)+t(18)+t(11)+t(10)+t(28)+t(15)+t(22)+t(12)+t(23)+t(44)+t(28)+t(6)+t(16)+t(26)+t(25)+t(20)+t(13)+t(6)+t(11)+t(10)+t(28)+t(44)+t(18)+t(16)+nt(13)));
 		// wff_has_subformula_cb_sym => ws 'w' 'f' 'f' '_' 'h' 'a' 's' '_' 's' 'u' 'b' 'f' 'o' 'r' 'm' 'u' 'l' 'a' '_' 'c' 'b' ws.
-		q(nt(184), (nt(13)+t(27)+t(26)+t(26)+t(44)+t(15)+t(10)+t(28)+t(44)+t(28)+t(6)+t(16)+t(26)+t(25)+t(20)+t(13)+t(6)+t(11)+t(10)+t(44)+t(18)+t(16)+nt(13)));
+		q(nt(186), (nt(13)+t(27)+t(26)+t(26)+t(44)+t(15)+t(10)+t(28)+t(44)+t(28)+t(6)+t(16)+t(26)+t(25)+t(20)+t(13)+t(6)+t(11)+t(10)+t(44)+t(18)+t(16)+nt(13)));
 		// wff_remove_existential_cb_sym => ws 'w' 'f' 'f' '_' 'r' 'e' 'm' 'o' 'v' 'e' '_' 'e' 'x' 'i' 's' 't' 'e' 'n' 't' 'i' 'a' 'l' '_' 'c' 'b' ws.
-		q(nt(185), (nt(13)+t(27)+t(26)+t(26)+t(44)+t(20)+t(24)+t(13)+t(25)+t(59)+t(24)+t(44)+t(24)+t(5)+t(22)+t(28)+t(19)+t(24)+t(12)+t(19)+t(22)+t(10)+t(11)+t(44)+t(18)+t(16)+nt(13)));
+		q(nt(187), (nt(13)+t(27)+t(26)+t(26)+t(44)+t(20)+t(24)+t(13)+t(25)+t(59)+t(24)+t(44)+t(24)+t(5)+t(22)+t(28)+t(19)+t(24)+t(12)+t(19)+t(22)+t(10)+t(11)+t(44)+t(18)+t(16)+nt(13)));
+		// tau_collapse_positives_cb => tau_collapse_positives_cb_sym ws_required tau_cb_arg ws_required tau_cb_arg ws_required tau_cb_arg.
+		q(nt(72), (nt(188)+nt(12)+nt(189)+nt(12)+nt(189)+nt(12)+nt(189)));
+		// tau_positives_upwards_cb => tau_positives_upwards_cb_sym ws_required tau_cb_arg ws_required tau_cb_arg.
+		q(nt(73), (nt(190)+nt(12)+nt(189)+nt(12)+nt(189)));
+		// tau_cb_arg => capture.
+		q(nt(189), (nt(56)));
+		// tau_cb_arg => tau.
+		q(nt(189), (nt(71)));
 		// input => in colon open_brace source_binding close_brace.
-		q(nt(186), (nt(65)+nt(45)+nt(42)+nt(163)+nt(43)));
+		q(nt(191), (nt(65)+nt(45)+nt(42)+nt(165)+nt(43)));
 		// _Rinputs_21 => input.
-		q(nt(188), (nt(186)));
+		q(nt(193), (nt(191)));
 		// _Rinputs_22 => null.
-		q(nt(189), (nul));
+		q(nt(194), (nul));
 		// _Rinputs_22 => _Rinputs_21 _Rinputs_22.
-		q(nt(189), (nt(188)+nt(189)));
+		q(nt(194), (nt(193)+nt(194)));
 		// inputs => less input _Rinputs_22 dot.
-		q(nt(187), (nt(47)+nt(186)+nt(189)+nt(37)));
+		q(nt(192), (nt(47)+nt(191)+nt(194)+nt(37)));
 		// main => wff dot.
-		q(nt(190), (nt(72)+nt(37)));
+		q(nt(195), (nt(74)+nt(37)));
 		// rule => tau_rule.
-		q(nt(191), (nt(68)));
+		q(nt(196), (nt(68)));
 		// rule => wff_rule.
-		q(nt(191), (nt(81)));
+		q(nt(196), (nt(83)));
 		// rule => bf_rule.
-		q(nt(191), (nt(127)));
+		q(nt(196), (nt(129)));
 		// _Rrules_23 => rule.
-		q(nt(193), (nt(191)));
+		q(nt(198), (nt(196)));
 		// _Rrules_24 => null.
-		q(nt(194), (nul));
+		q(nt(199), (nul));
 		// _Rrules_24 => _Rrules_23 _Rrules_24.
-		q(nt(194), (nt(193)+nt(194)));
+		q(nt(199), (nt(198)+nt(199)));
 		// rules => _Rrules_24.
-		q(nt(192), (nt(194)));
+		q(nt(197), (nt(199)));
 		// rec_relation => wff_rec_relation dot.
-		q(nt(195), (nt(84)+nt(37)));
+		q(nt(200), (nt(86)+nt(37)));
 		// rec_relation => bf_rec_relation.
-		q(nt(195), (nt(130)));
+		q(nt(200), (nt(132)));
 		// _Rrec_relations_25 => rec_relation.
-		q(nt(197), (nt(195)));
+		q(nt(202), (nt(200)));
 		// _Rrec_relations_26 => null.
-		q(nt(198), (nul));
+		q(nt(203), (nul));
 		// _Rrec_relations_26 => _Rrec_relations_25 _Rrec_relations_26.
-		q(nt(198), (nt(197)+nt(198)));
+		q(nt(203), (nt(202)+nt(203)));
 		// rec_relations => _Rrec_relations_26.
-		q(nt(196), (nt(198)));
+		q(nt(201), (nt(203)));
 		// formula => rec_relations main.
-		q(nt(199), (nt(196)+nt(190)));
+		q(nt(204), (nt(201)+nt(195)));
 		// library => rules.
-		q(nt(200), (nt(192)));
+		q(nt(205), (nt(197)));
 		// builder => builder_head definition builder_body dot.
-		q(nt(201), (nt(202)+nt(36)+nt(203)+nt(37)));
+		q(nt(206), (nt(207)+nt(36)+nt(208)+nt(37)));
 		// _Rbuilder_head_27 => ws_required capture.
-		q(nt(204), (nt(12)+nt(56)));
+		q(nt(209), (nt(12)+nt(56)));
 		// _Rbuilder_head_28 => null.
-		q(nt(205), (nul));
+		q(nt(210), (nul));
 		// _Rbuilder_head_28 => _Rbuilder_head_27 _Rbuilder_head_28.
-		q(nt(205), (nt(204)+nt(205)));
+		q(nt(210), (nt(209)+nt(210)));
 		// builder_head => open_parenthesis capture _Rbuilder_head_28 close_parenthesis.
-		q(nt(202), (nt(38)+nt(56)+nt(205)+nt(39)));
+		q(nt(207), (nt(38)+nt(56)+nt(210)+nt(39)));
 		// builder_body => tau.
-		q(nt(203), (nt(71)));
+		q(nt(208), (nt(71)));
 		// builder_body => wff.
-		q(nt(203), (nt(72)));
+		q(nt(208), (nt(74)));
 		// builder_body => bf.
-		q(nt(203), (nt(121)));
+		q(nt(208), (nt(123)));
 		// gssotc => tau semicolon.
-		q(nt(206), (nt(71)+nt(46)));
+		q(nt(211), (nt(71)+nt(46)));
 		// start => inputs.
-		q(nt(207), (nt(187)));
+		q(nt(212), (nt(192)));
 		// start => formula.
-		q(nt(207), (nt(199)));
+		q(nt(212), (nt(204)));
 		// start => library.
-		q(nt(207), (nt(200)));
+		q(nt(212), (nt(205)));
 		// start => builder.
-		q(nt(207), (nt(201)));
+		q(nt(212), (nt(206)));
 		// start => gssotc.
-		q(nt(207), (nt(206)));
+		q(nt(212), (nt(211)));
 		return q;
 	}
 };
diff --git a/src/formula.h b/src/formula.h
index 624bfc7c..fc14bc20 100644
--- a/src/formula.h
+++ b/src/formula.h
@@ -1192,6 +1192,8 @@ struct callback_applier {
 			case tau_parser::wff_has_clashing_subformulas_cb: return apply_wff_clashing_subformulas_check(n);
 			case tau_parser::wff_has_subformula_cb: return apply_has_subformula_check(n, tau_parser::wff_cb_arg);
 			case tau_parser::wff_remove_existential: return apply_wff_remove_existential(n);
+			case tau_parser::tau_collapse_positives_cb: return apply_tau_collapse_positives(n);
+			case tau_parser::tau_positives_upwards_cb: return apply_tau_positives_upwards(n);
 			default: return n;
 		}
 	}
@@ -1412,6 +1414,19 @@ struct callback_applier {
 		auto tmp = replace<sp_tau_node<BAs...>>(args[2], m)| only_child_extractor<BAs...> | optional_value_extractor<sp_tau_node<BAs...>>;
 		return tmp;
 	}
+
+	sp_tau_node<BAs...> apply_tau_collapse_positives(const sp_tau_node<BAs...>& n) {
+		auto args = n || tau_parser::bf_cb_arg || only_child_extractor<BAs...>;
+		std::map<sp_tau_node<BAs...>, sp_tau_node<BAs...>> m;
+
+	}
+
+	sp_tau_node<BAs...> apply_tau_positives_upwards(const sp_tau_node<BAs...>& n) {
+		auto args = n || tau_parser::tau_cb_arg || only_child_extractor<BAs...>;
+		if (auto check_1eft = args[0] | tau_parser::wff; check_left)
+			if (auto check_right = args[1] | tau_parser::wff; check_right) return args[2];
+		return n;
+	}
 };
 
 // apply one tau rule to the given expression
diff --git a/src/tau.h b/src/tau.h
index e718fa32..9650103b 100644
--- a/src/tau.h
+++ b/src/tau.h
@@ -54,6 +54,13 @@ RULE(TAU_SIMPLIFY_SELF_3, "( $X ||| % $X ) := T.")
 RULE(TAU_SIMPLIFY_SELF_4, "( % $X &&& $X ) := F.")
 RULE(TAU_SIMPLIFY_SELF_5, "( % $X ||| $X ) := T.")
 
+RULE(TAU_COLLAPSE_POSITIVES_0, "($X &&& $Y) := tau_collapse_positives $X $Y ($X && $Y).")
+RULE(TAU_PUSH_POSITIVES_UPWARDS_0, "($X &&& ($Y &&& $Z) := tau_positives_upwards $Y ($Y &&& ($X &&& $Z).")
+RULE(TAU_PUSH_POSITIVES_UPWARDS_1, "($X &&& ($Y &&& $Z) := tau_positives_upwards $Z ($Z &&& ($X &&& $Y).")
+RULE(TAU_PUSH_POSITIVES_UPWARDS_2, "(($X &&& $Y) &&& $Z) := tau_positives_upwards $X ($X &&& ($Y &&& $Z).")
+RULE(TAU_PUSH_POSITIVES_UPWARDS_3, "(($X &&& $Y) &&& $Z) := tau_positives_upwards $X ($Y &&& ($X &&& $Z).")
+RULE(TAU_PUSH_POSITIVES_UPWARDS_4, "($X &&& $Y) := ($Y &&& $X).")
+
 template<typename... BAs>
 static auto to_dnf_tau = make_library<BAs...>(
 	TAU_DISTRIBUTE_0
@@ -84,6 +91,7 @@ static auto simplify_tau = make_library<BAs...>(
 );
 
 // definitions of bf builder rules
+// IDEA maybe move it to formula.h or normalizer.h
 const std::string BLDR_TAU_AND = "( $X $Y ) := ($X &&& $Y).";
 const std::string BLDR_TAU_OR = "( $X $Y ) := ($X ||| $Y).";
 const std::string BLDR_TAU_NEG = "( $X ) := % $X.";