Online Otter-λ

Examples

Examples -> FirstOrderLogic -> quantifiers.prf

7 [] -P(x)| -P(i(x,y))|P(y).
8 [] P(i(x,i(y,x))).
10 [] P(i(i(x,y),i(i(x,n(y)),n(x)))).
12 [] P(i(all(lambda(x,Ap(y,x))),Ap(y,z))).
14 [] -P(n(all(lambda(x,n(Ap(a,x)))))).
16 [binary,7.2,7.3] -P(x)|P(y)| -P(z)| -P(i(z,i(x,y))).
18 [factor,16.1.3] -P(x)|P(y)| -P(i(x,i(x,y))).
20 [binary,8.1,7.2] -P(x)|P(i(y,x)).
21 [binary,8.1,7.1] -P(i(i(x,i(y,x)),z))|P(z).
101 [binary,21.2,14.1] -P(i(i(x,i(y,x)),n(all(lambda(z,n(Ap(a,z))))))).
110 [hyper,12,18,10,demod,beta] P(n(all(lambda(x,n(Ap(y,z)))))).
115 [binary,110.1,20.1] P(i(x,n(all(lambda(y,n(Ap(z,u))))))).
116 [binary,115.1,101.1] $F.