added simulation relation computation to yield type checking
updated the type check to incorporate {:terminates} annotation
added another sample