nodes action nodes time step i i N
o, o' mutual exclusion o' interfere o f, f' i s –
f o, o i competing needs o
.]"
i —
o Proposition 1  Let P¹     O¹, I, G  be a relaxed STRIPS task.  Started on P¹, GRAPH-
PLAN will not mark any pair of facts or actions as mutually exclusive.

Proof:
Base case: time step Inductive case: time step i → time step i 口 N
l i s –
s —
N
Proposition 2  Let P¹     O¹¸ I' G  be a relaxed STRIPS task.  Started on P¹, GRAPH-
PLAN will never backtrack.

Proof:
.f fact