H
otel
K
ey
C
ards
Notation
Basis
State
NewCard
Trace
Equivalence