Returned 92 matches (100 formulae, 79 docs)
    Lookup 5.000 ms, Re-ranking 442.511 ms
    Found 36561 tuple postings, 24343 formulae, 7367 documents
[ formulas ] [ documents ] [ documents-by-formula ]

1.0000
0.0000
25.0000
x , y A [ x y ¬ z X [ z x z y ] ] .

0.3793
-13.0000
8.0000
u S v x , y M ( x u y S x v y S ) .

0.3052
-6.0000
7.0000
x , y A x y x y

0.2807
-11.0000
6.0000
x y [ x y z y C ( x ; y z ) ] .

0.2524
-6.0000
6.0000
x , y : ¬ ( x < y y < x )

0.2524
-10.0000
6.0000
x , y : ¬ ( x < y y < x ) x = y

0.2524
-12.0000
5.0000
A = { x F ; y F ( x R y y A ) }

0.2389
-9.0000
5.0000
x , y . P ( x , y ) Q ( f ( x ) )

0.2230
0.0000
6.0000
x , y A

0.2230
0.0000
5.0000
x , y G
x , y N

0.2230
-1.0000
5.0000
x , y S ,
x , y V ,

0.2230
-4.0000
5.0000
x , y U , x y

0.2230
-6.0000
5.0000
x , y H : y , x
x , y I : x - y I

0.2230
-9.0000
6.0000
x , y A : x y x y

0.2230
-10.0000
5.0000
x + y x + y x , y V

0.2230
-12.0000
5.0000
κ ( x , y ) := Tr ( ad x ad y ) x , y 𝔤

0.2230
-12.0000
5.0000
x , y X , x y x S y S

0.2230
-13.0000
6.0000
x , y A , f ( x ) = f ( y ) x = y .

0.2230
-13.0000
6.0000
x , y A , x y f ( x ) f ( y ) .

0.2230
-13.0000
5.0000
x , y N x < y z N x + z = y

0.2230
-13.0000
5.0000
x , y H : ¬ ( x y ) = ¬ x ¬ y .

0.2230
-15.0000
6.0000
x , y A , f ( x + y ) f ( x ) + f ( y ) .

0.2230
-16.0000
5.0000
x , y H : ¬ ( x y ) = ¬ ¬ ( ¬ x ¬ y ) .

0.2230
-17.0000
5.0000
ϕ ( [ x , y ] ) = [ ϕ ( x ) , ϕ ( y ) ] x , y 𝔤 1 .

0.2230
-18.0000
5.0000
K ( x , y ) 2 K ( x , x ) K ( y , y ) x , y X .

0.2230
-19.0000
5.0000
i , x , y X , x y x S i y S i

0.2230
-21.0000
5.0000
x , y U , x y : Pr h H [ h ( x ) = h ( y ) ] 1 m

0.2192
-10.0000
7.0000
x , y , z ( x F y x F z y = z )
x , y , z ( x R y y R z x R z )

0.2192
-22.0000
4.0000
x V y ( y x ) y ( y x ¬ z ( z y z x ) ) .

0.2090
-19.0000
5.0000
{ ( x , z ) | x ( S R ) z y Y ( x R y y S z ) } .

0.1967
-19.0000
3.0000
τ = { G X : x , y X x G x y y G , }

0.1818
0.0000
5.0000
x , y A

0.1818
0.0000
4.0000
x , y X

0.1818
-1.0000
5.0000
x , y A

0.1818
-1.0000
5.0000
x , y A 1
x , y A 2

0.1818
-2.0000
4.0000
x x y x

0.1818
-3.0000
2.0000
x , y , z N

0.1818
-4.0000
5.0000
x , y A 1 A 2

0.1818
-4.0000
4.0000
x , y B , x y

0.1818
-7.0000
4.0000
x , y V , ( x , y ) E

0.1818
-8.0000
5.0000
A A := { x y : x , y A }

0.1818
-10.0000
5.0000
A + A := { x + y : x , y A } ,
A - A := { x - y : x , y A } ,

0.1818
-12.0000
5.0000
x , y [ x y [ x R y y R x ] ]

0.1818
-12.0000
4.0000
d = min x , y C , x y d ( x , y )

0.1818
-13.0000
4.0000
d = min { x , y C : x y } d ( x , y )

0.1818
-13.0000
4.0000
¬ ( ¬ x ¬ y ) = x y for all regular x , y H ,

0.1818
-16.0000
2.0000
( x * y ) * z = x * ( y * z ) x , y , z G

0.1818
-18.0000
2.0000
{ S X : x , y X x S y x y S , }

0.1798
-10.0000
5.0000
x y z ( z y z x ϕ ( z ) )

0.1728
-8.0000
6.0000
x y z ( x z y z ) .

0.1728
-8.0000
4.0000
P x y z [ O z x O z y ] .

0.1728
-22.0000
2.0000
x [ a ( a x ) y ( y x ¬ z ( z y z x ) ) ] .

0.1644
-9.0000
5.0000
x z M [ x := y ] [ z ] = M [ z ]

0.1644
-13.0000
1.0000
x y z [ ( R x y R y z ) R x z ]

0.1644
-20.0000
1.0000
𝟏𝟏𝟓 : I ( R ) x y z [ ( x R y x R z ) y = z ]

0.1644
-22.0000
2.0000
z w 1 w 2 w n y x [ x y ( x z ϕ ) ] .

0.1538
-4.0000
5.0000
x A [ x ] = A [ x ] .

0.1538
-6.0000
3.0000
x y x y y x

0.1538
-14.0000
4.0000
x , y , z : x < y ( x < z z < y )

0.1538
-15.0000
5.0000
x , y : A . f ( x ) # B f ( y ) \Rarr x # A y

0.1538
-15.0000
2.0000
z y x [ x y ( x z ϕ ( x ) ) ] .

0.1404
-8.0000
4.0000
x , y ( x R y y R x )

0.1404
-9.0000
4.0000
( x , y ) , x A , y A c

0.1284
-19.0000
4.0000
¬ P x y z [ P z x and ¬ O z y and ¬ v [ P P v z ] ] .

0.1237
-3.0000
4.0000
x y = ¬ ( x y )

0.1237
-7.0000
5.0000
x + y , A ( x + y ) = 0

0.1237
-9.0000
5.0000
x y z [ z x z y ] .

0.1237
-11.0000
5.0000
P P x y z [ P z y and ¬ O z x ] .

0.1237
-13.0000
3.0000
x y x R y ( z x R z z R y ) .

0.1237
-15.0000
3.0000
x y \exist w z [ z w ( z x z = y ) ] .
x y w z [ z w ( z x z = y ) ] .

0.1237
-16.0000
4.0000
z [ z x z y ] w [ x w y w ] .

0.1176
-2.0000
4.0000
x y y y

0.1176
-4.0000
3.0000
x / z , y / z

0.1176
-6.0000
4.0000
z [ x z and y z ] .

0.1176
-8.0000
4.0000
( x z and z y ) x y .

0.1176
-8.0000
3.0000
{ ( x , y ) x y x y }

0.1176
-8.0000
3.0000
x < y z [ x < z < y ] .

0.1176
-9.0000
3.0000
x , x y F ( x ) G ( y )

0.1176
-10.0000
2.0000
z [ z < x z < y ] x y .

0.1176
-11.0000
2.0000
x y = def . { z : z x z y }

0.1176
-15.0000
3.0000
x y [ z [ z x z y ] x = y ] .

0.1176
-15.0000
2.0000
x y ( z ( z x z y ) x = y ) .

0.1096
-3.0000
4.0000
x z = y z

0.1096
-3.0000
4.0000
x * z y * z
x + z y + z

0.1096
-6.0000
2.0000
z ( z x z y )

0.1096
-10.0000
3.0000
let x : x = y in z = z [ x := y ]

0.1096
-10.0000
3.0000
x y ( F x x R y F y )

0.1096
-15.0000
2.0000
x y [ z ( z x z y ) x = y ]

0.1096
-16.0000
2.0000
x y [ z ( z x z y ) x = y ] .

0.1096
-22.0000
2.0000
x y [ z ( z x z y ) z ( x z y z ) ]

0.1096
-23.0000
2.0000
x y [ z ( z x z y ) w ( x w y w ) ] ,

0.0984
-9.0000
0.0000
x = y and ( L z ) [ x := y ]