Lecture 9 - Part 1

This web page was written on:
30 August 2021

The video was produced on:
7 December 2017

Copy the following tiny text, either by clicking on the Copy button below it, or by your usual method of copying text.

EXTENDS Integers, Sequences

Remove(i, seq) == 
  [j \in 1..(Len(seq)-1) |-> IF j < i THEN seq[j] 
                                      ELSE seq[j+1]]

Stop the video and right-click on the
following link to download the file:
ABSpec.tla

Copy the following tiny text, either by clicking on the Copy button below it, or by your usual method of copying text.

\A v \in Data \X {0,1} : (AVar = v) ~> (BVar = v)

Lecture 9 - Part 1

The Next Video