added invariants
checkpoint embeddings and performUpdates before checking postcondition.
also fixes some issues in TKappa