HotelKeyCards

Notation

Basis

State

NewCard

Trace

Equivalence