Spectators and local experiments

For disjoint $S,T\subseteq L$, put $Z=L\setminus (S\cup T)$. The sequential experiment is

The reverse experiment reads $T$ first but reports the same ordered classical pair. Joint readout of $S\cup T$ likewise returns $Z$. These terms have the same observation interface after linear tuple rearrangement.

A local identity experiment may return its names with a constant classical unit. A remote allocation experiment returns the additional allocated name. Thus ancilla comparisons below do not use quantum weakening.

There are two record scopes:

1. readout instances: $S=L$ and $u=\ast$;

2. continuation instances: $u$ consumes all of $L\setminus S$.

The outcome proof uses only readout instances. The update proof uses

No equation for arbitrary surrounding contexts is assumed.