Query:
	ex:v0 ex:P ?value . FILTER NOT EXISTS { FILTER NOT EXISTS ex:v0 ex:Q ?value }

translates into

P = Path(ex:v0, link(ex:P), ?value)
F = fn:not(exists(translate( FILTER NOT EXISTS { ex:v0 ex:Q ?value } )))
Filter(F, P) = Filter(F, { { ?value -> ex:va }, { ?value -> ex:vb }, { ?value -> ex:vc } }, D(G))

  expr(μ) = F = fn:not(exists(translate( FILTER NOT EXISTS { ex:v0 ex:Q ?value } )))

  μ_0 = { ?value -> ex:va }:

    expr(μ_0) = fn:not(exists(Q)), with Q = translate( FILTER NOT EXISTS { ex:v0 ex:Q ?value } )

                       exists(Q)  = eval(D(G), substitute(Q, μ_0)) is a non empty sequence?
                                  = eval(D(G), translate( FILTER NOT EXISTS { ex:v0 ex:Q ex:va } )) is a non empty sequence?

                                        translates into

                                          P =
                                          F = fn:not(exists(translate( ex:v0 ex:Q ex:va )))
                                          Filter(F, P) = Filter(F, { {} }, D(G))

                                            expr(μ) = F = fn:not(exists(translate( ex:v0 ex:Q ex:va )))

                                            μ_0 = {}:

                                              expr(μ_0) = fn:not(exists(R)), with R = translate( ex:v0 ex:Q ex:va )

                                                                 exists(R) = eval(D(G), substitute(R, μ_0)) is a non empty sequence?
                                                                           = eval(D(G), translate( ex:v0 ex:Q ex:va )) is a non empty sequence?
                                                                           = \emptyset is a non empty sequence?
                                                                           = false
                                                        = fn:not(false)
                                                        = true

                                          Filter(F, P) = { {} }
                                  = { {} } is a non empty sequence?
                                  = true

              = fn:not(true)
              = false

  μ_1 = { ?value -> ex:vb }:

    expr(μ_1) = fn:not(exists(Q)), with Q = translate( FILTER NOT EXISTS { ex:v0 ex:Q ?value } )

                       exists(Q)  = eval(D(G), substitute(Q, μ_1)) is a non empty sequence?
                                  = eval(D(G), translate( FILTER NOT EXISTS { ex:v0 ex:Q ex:vb } )) is a non empty sequence?

                                        translates into

                                          P =
                                          F = fn:not(exists(translate( ex:v0 ex:Q ex:vb )))
                                          Filter(F, P) = Filter(F, { {} }, D(G))

                                            expr(μ) = F = fn:not(exists(translate( ex:v0 ex:Q ex:vb )))

                                            μ_0 = {}:

                                              expr(μ_0) = fn:not(exists(R)), with R = translate( ex:v0 ex:Q ex:vb )

                                                                 exists(R) = eval(D(G), substitute(R, μ_0)) is a non empty sequence?
                                                                           = eval(D(G), translate( ex:v0 ex:Q ex:vb )) is a non empty sequence?
                                                                           = \emptyset is a non empty sequence?
                                                                           = false
                                                        = fn:not(false)
                                                        = true

                                          Filter(F, P) = { {} }
                                  = { {} } is a non empty sequence?
                                  = true

              = fn:not(true)
              = false

  μ_2 = { ?value -> ex:vc }:

    expr(μ_2) = fn:not(exists(Q)), with Q = translate( FILTER NOT EXISTS { ex:v0 ex:Q ?value } )

                       exists(Q)  = eval(D(G), substitute(Q, μ_2)) is a non empty sequence?
                                  = eval(D(G), translate( FILTER NOT EXISTS { ex:v0 ex:Q ex:vc } )) is a non empty sequence?

                                        translates into

                                          P =
                                          F = fn:not(exists(translate( ex:v0 ex:Q ex:vc )))
                                          Filter(F, P) = Filter(F, { {} }, D(G))

                                            expr(μ) = F = fn:not(exists(translate( ex:v0 ex:Q ex:vc )))

                                            μ_0 = {}:

                                              expr(μ_0) = fn:not(exists(R)), with R = translate( ex:v0 ex:Q ex:vc )

                                                                 exists(R) = eval(D(G), substitute(R, μ_0)) is a non empty sequence?
                                                                           = eval(D(G), translate( ex:v0 ex:Q ex:vc )) is a non empty sequence?
                                                                           = { {} } is a non empty sequence?
                                                                           = true
                                                        = fn:not(true)
                                                        = false

                                          Filter(F, P) = \emptyset
                                  = \emptyset is a non empty sequence
                                  = false

              = fn:not(false)
              = true

Filter(F, P) = { ?value -> ex:vc }