In Exercise 451, the solution provided lets assignment take time 1.

Originally, the left process looks like this:

but after incorporating time, it looks like this:

Isn’t just the assignment of ‘not b’ to time t+1? I don’t see how that is the same as

# Exercise 451, confusion about the notation

**lemirand**#1

**hehner**#2

An interactive variable is a function of time. b is an interactive variable. b(t+1) is the value of interactive variable b at time t+1. An assignment x:=e to an interactive variable x that takes time 1 is

x(t’)=e ∧ t’=t+1

So b:=⊥ is

b(t’)=⊥ ∧ t’=t+1

or equivalently

¬b(t+1) ∧ t’=t+1