Online Otter-λ

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

Examplessmall logo



Examples -> FirstOrderLogic -> quantifiers4.prf


7 [] P(i(all(lambda(x,Ap(y,x))),Ap(y,z))).
8 [] -P(i(all(lambda(x,n(Ap(y,x)))),n(Ap(y,z)))).
9 [binary,8.1,7.1] $F.