Online Otter-λ

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

Examplessmall logo



Examples -> LambdaLogic -> lambda4.in


% verification of standard fixed point construction

set(lambda).
set(binary_res).

list(usable).
x = x.
end_of_list.

list(sos).
ap(c,ap(lambda(x,ap(c,ap(x,x))), lambda(x,ap(c,ap(x,x))))) != ap(lambda(x,ap(c,ap(x,x))), lambda(x,ap(c,ap(x,x)))).
end_of_list.