+ is the addition operation of the natural numbers. The natural numbers can be defined in TLA+. In this introduction, we just assume they are given.