Proof: To begin with, we need to show that computing FAp takes only polynomial time.

From the results in (Blum & Furst, 1997), it follows directly that building a planning graph is polynomial in | I | , | O | , l and t , where l is the maximal length of any precondition, add or delete list of an action, and t is the number of time steps built. Taking l as a parameter of the input size, it remains to show that a planning graph levels off after a polynomial nmber t of time steps. Now, a planning graph has leveled off if between some time steps t and t + 1 neither the set of facts nor the number of exclusion relations change. Between two subsequent time steps, the set of facts can only increase—facts already occuring in the graph remain there—and the number of exclusions can only decrease—non-exclusive facts will be non-exclusive in all subsequent layers. Thus, the maximal number of time steps to be built until the graph has leveled off is dominated by the maximal number of changes that can occur between two subsequent layers, which is dominated by the maximal number of facts plus the maximal number of exclusion relations. The maximal number of facts is O(| I | + | O | * l ), and the maximal number of exclusions is O((| I | + | O | * l ) 2 ), the square of the maximal number of facts.

Having computed F A P in polynomial time, testing B ≤ e A involves looking at all actions in O, and rejecting them if they either
- delete A, which is decidable in time O ( l ), or
- have a precondition, which is an element of F AP , decidable in time O ( l *( I | + | O | * l )).

Thus we have an additional runtime for the test, which is O(|O| * l * (|I| + |O| * l )).   ■
Let us consider the following example, which illustrates the computation of a common representational variant of the blocks world with actions to stack, unstack, pickup, and putdown blocks:
pickup(?ob)
clear(?ob)  on-table(?ob)  arm-empty()  - →  ADD  holding(?ob)

# $\mathrm{img}\left(?ob\right)$   $\left(?ob\right)$ $\mathrm{on}\text{-}\mathrm{table}(?ob)$  at $\mathrm{new}$  . 
DEL clear(?ob) on-table(?ob) arm-empty().

putdown(?ob)
holding(?ob) −→ ADD clear(?ob) arm-empty() on-table(?ob)
DEL holding (?ob).

stack(?ob,?underob) clear(?underob)  holding(?ob)  →  ADD  arm-empty()  clear(?ob)  on(?ob,?underob)
DEL clear(?underob) holding(?ob) .

unstack(?ob,?underob)
on(?ob,?underob) clear(?ob) arm-empty() −→ ADD holding(?ob) clear(?underob)
DEL on(?ob,?underob) clear(?ob) arm-empty().

Given the simple task of stacking three blocks:
initial state: on-table(a) on-table(b) on-table(c)
goal state:    on(a,b) on(b,c)