### 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
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)