# Re: [tlaplus] Re: TLA+ Video Course

```The two definitions are equivalent:

```
big' = small - (3 - big) <==> big' = small - 3 + big <==> big' = big - (3 - small)
```
On 09/06/2017 08:33 PM, Balaji Arun wrote:
```
```Dr. Lamport

```
Thanks for the wonderful lectures. I was trying video4.html and saw that the definition for BigToSmall differs from mine:
```
*video4.html*
*
*

BigToSmall == IF big + small =< 3

THEN /\ big' = 0

/\ small' = big + small

ELSE /\ big' = small - (3 - big)

/\ small' = 3

*My Solution*

BigToSmall == IF big + small =< 3

THEN /\ big' = 0

/\ small' = big + small

ELSE /\ big' = big - (3 - small)

/\ small' = 3

```
Notice the ELSE statement. Wouldnt big' = small - (3 - big) lead to negative values (e.g. big = 5 and small = 2)? In that case, why does TLC model checker not catch this with the invariant TypeOK?
```

On Monday, August 14, 2017 at 10:06:16 PM UTC-4, Leslie Lamport wrote:

The scripts of all the lectures in the TLA+ Video Course are now
available.  Each script contains everything shown and said on the
video, except for shots of me.  It can be useful for the hearing
impaired, viewers who want to review a lecture, and people who hate
videos.  However, the html file that displays the video may be
```Visit this group at https://groups.google.com/group/tlaplus.