val n = 5; PH 1 n ph CS 1 n cs PH p fun Chopsticks(ph(i)) = 1`cs(i) ++ 1`cs(if i=n then 1 else i+1); Eat Think Unused Chopstics Take Chopsticks Put Down Chopsticks p p Chopsticks(p) p Chopsticks(p) p <same as model> true true false false false true true false false true false false true false true false false true true false false false false false false false false true false true false false true true false false false true false