mod BLOCKS-WORLD is
  protecting QID .
  sorts BlockId Prop State .
  subsort Qid < BlockId .
  subsort Prop < State .

  op table : BlockId -> Prop .      *** block is on the table
  op on : BlockId BlockId -> Prop . *** block A is on block B
  op clear : BlockId -> Prop .      *** block is clear
  op hold : BlockId -> Prop .       *** robot arm holds the block
  op empty : -> Prop .              *** robot arm is empty
  op 1 : -> State .
  op _&_ : State State -> State [assoc comm id: 1] .

  vars X Y : BlockId .

  rl [pickup] : empty & clear(X) & table(X) => hold(X) .
  rl [putdown] : hold(X) => empty & clear(X) & table(X) .
  rl [unstack] : empty & clear(X) & on(X,Y) => hold(X) & clear(Y) .
  rl [stack] : hold(X) & clear(Y) => empty & clear(X) & on(X,Y) .
endm

set trace on .

rew [10] empty & clear('c) & clear('b) & table('a) & table('b) & on('c,'a) .

***(
rewrite [10] in BLOCKS-WORLD : empty & clear('c) &
    clear('b) & table('a) & table('b) & on('c, 'a) .
*********** rule
rl [pickup]: empty & table(X) & clear(X) => hold(X) .
X:BlockId --> 'b
empty & table('a) & table('b) & clear('c) & clear('b) & on('c, 'a)
--->
table('a) & clear('c) & on('c, 'a) & hold('b)
*********** rule
rl [stack]: clear(Y) & hold(X) => empty & clear(X) & on(X, Y) .
X:BlockId --> 'b
Y:BlockId --> 'c
table('a) & clear('c) & hold('b) & on('c, 'a)
--->
table('a) & on('c, 'a) & empty & clear('b) & on('b, 'c)
*********** rule
rl [unstack]: empty & clear(X) & on(X, Y) => clear(Y) & hold(X) .
Y:BlockId --> 'c
X:BlockId --> 'b
empty & table('a) & clear('b) & on('c, 'a) & on('b, 'c)
--->
table('a) & on('c, 'a) & clear('c) & hold('b)
*********** rule
rl [stack]: clear(Y) & hold(X) => empty & clear(X) & on(X, Y) .
X:BlockId --> 'b
Y:BlockId --> 'c
table('a) & clear('c) & hold('b) & on('c, 'a)
--->
table('a) & on('c, 'a) & empty & clear('b) & on('b, 'c)
*********** rule
rl [unstack]: empty & clear(X) & on(X, Y) => clear(Y) & hold(X) .
Y:BlockId --> 'c
X:BlockId --> 'b
empty & table('a) & clear('b) & on('c, 'a) & on('b, 'c)
--->
table('a) & on('c, 'a) & clear('c) & hold('b)
*********** rule
rl [stack]: clear(Y) & hold(X) => empty & clear(X) & on(X, Y) .
X:BlockId --> 'b
Y:BlockId --> 'c
table('a) & clear('c) & hold('b) & on('c, 'a)
--->
table('a) & on('c, 'a) & empty & clear('b) & on('b, 'c)
*********** rule
rl [unstack]: empty & clear(X) & on(X, Y) => clear(Y) & hold(X) .
Y:BlockId --> 'c
X:BlockId --> 'b
empty & table('a) & clear('b) & on('c, 'a) & on('b, 'c)
--->
table('a) & on('c, 'a) & clear('c) & hold('b)
*********** rule
rl [stack]: clear(Y) & hold(X) => empty & clear(X) & on(X, Y) .
X:BlockId --> 'b
Y:BlockId --> 'c
table('a) & clear('c) & hold('b) & on('c, 'a)
--->
table('a) & on('c, 'a) & empty & clear('b) & on('b, 'c)
*********** rule
rl [unstack]: empty & clear(X) & on(X, Y) => clear(Y) & hold(X) .
Y:BlockId --> 'c
X:BlockId --> 'b
empty & table('a) & clear('b) & on('c, 'a) & on('b, 'c)
--->
table('a) & on('c, 'a) & clear('c) & hold('b)
*********** rule
rl [stack]: clear(Y) & hold(X) => empty & clear(X) & on(X, Y) .
X:BlockId --> 'b
Y:BlockId --> 'c
table('a) & clear('c) & hold('b) & on('c, 'a)
--->
table('a) & on('c, 'a) & empty & clear('b) & on('b, 'c)
rewrites: 10 in -10ms cpu (159ms real) (~ rewrites/second)
result State: empty & table('a) & clear('b) & on('c, 'a) & on('b, 'c)
)

set trace off .