your claim that all of the three specifications admit the same single behavior is true only because you ignore stuttering. The TLA+ specification
x ∈ Nat ∧ t = 1 ∧ ☐[t’ = t + 1 ∧ x’ = x + 1 ∧ t = 100 ⇒ x = 100]_<<x,t>>
has behaviors where x initially holds an arbitrary natural number, and t and x get incremented until t hits 100, at which point only stuttering is possible. So it cannot be equivalent to the TLA+ specification
x = 1 ∧ t = 1 ∧ ☐[t’ = t + 1 ∧ x’ = x + 1]_<<t,x>>
A similar observation holds for (the TLA+ version of) the third specification
x = 1 ∧ t = 1 ∧ ☐[t’ = t + 1 ∧ ((t < 100 ∧ x’ = x - 1) ∨ x’ = x + 1) ∧ (t = 100 ⇒ x = 100)]_<<x,t>>
You can force the equivalence of the specifications by adding the conjunct
⬦(t > 100)
and this observation shows that liveness conditions may sometimes constrain the safety part of the specifications. Such specifications are known as "not machine-closed" , and are hard to reason about. (You'd have to prove the invariant ☐(x=t), but this requires temporal logic reasoning since you must appeal to the liveness condition to show that the execution would be blocked when t hits 100.)
The standard form of TLA+ specifications where liveness conditions are conjunctions of (weak or strong) fairness conditions on sub-actions of the specification (essentially, disjuncts of the next-state relation) ensures that specifications are machine closed, and all safety properties can be proved just from the initial condition and the next-state relation.
 M. Abadi, L. Lamport. The existence of refinement mappings. TCS 81(2), 1991. See also section 8.9.2 of Specifying Systems.