Online Otter-λ
-->
Examples
% test file for second-order unification
op(400, xfx, *).
set(lambda).
set(demod_inf).
set(binary_res).
%set(very_verbose).
assign(max_distinct_vars,6).
%set(knuth_bendix).
%weight_list(pick_and_purge).
%weight(cases($(1),$(1),$(1),$(1)), 10).
%end_of_list.
%assign(max_weight,32).
list(usable).
x = x.
% the universe is a group G and H is a subgroup of G
%-H(x) | -H(y) | H(x*y).
%-H(x) | H(i(x)).
%(x * y) * z = x * (y * z). % product is associative
%x*i(x) = 1.
%i(x) * x = 1.
%1*x = 1.
%x*1 = 1.
u * x = v | u != v *i(x).
-Ap(Z,w) | exists(lambda(x,Ap(Z,x))).
end_of_list.
list(demodulators).
f(w) = exists(lambda(x, and(H(x), x*a = w))). % f is the characteristic function of Ha
%i(i(x))= x.
end_of_list.
list(sos).
H(g(X)). % c = g(X) is forbidden to X and belongs to H
-f(Ap(X,g(X)))| $ANS(X) | Ap(X,Ap(Y,r(Y))) != r(Y) | $ANS(Y). % X takes H to Ha and Y is the inverse of X.
end_of_list.