Online Otter-λ

Utility Link | Utility Link | Utility Link
ExternalSimplification | SetTheory | LambdaLogic | Induction | More >
-->

Examplessmall logo



Examples -> Algebra -> identity.in


% prove the existence of the identity function.

set(lambda).
set(demod_inf).
set(binary_res).
set(very_verbose).

list(usable).
x = x.
end_of_list.

list(sos).
g(X) != Ap(X,g(X)) | $ANS(X).
end_of_list.