Online Otter-λ
-->
Examples
% Cantor's theorem and Russell's paradox
set(lambda).
set(demod_inf).
set(binary_res).
assign(max_distinct_vars,2).
assign(max_weight,24).
assign(pick_given_ratio,4).
% typings:
% Prop Ap(P(alpha),alpha).
% P(alpha) Ap(beta,alpha) where beta is the type of c
% so polymorphically, something Ap(something, alpha); the second arg always has type alpha
% Prop not(Prop).
% P(Alpha) c(alpha).
% alpha J(P(alpha)).
list(usable).
% x=x. not needed
w != not(w).
u != v | v = u.
end_of_list.
list(demodulators).
not(not(x)) = x.
end_of_list.
list(sos).
Ap(x,z) = Ap(Ap(c,J(x)),z) |$ANS(x) | $ANS(z). % "negated" goal. Says every x of type P(alpha) is extensionally equal to c(J(x)).
end_of_list.