Receiver indices and reflection, extracted from the former SmallS module.

theorem ConwaySoifer.reflL_apply (p : Point) : reflL p = refl p

def ConwaySoifer.recvOf (c : ContactCase) : Fin 6

The receiver of the minimal endpoint: S₅ for Sext, S₁ otherwise.

Equations

• ConwaySoifer.recvOf c = ConwaySoifer.neighbor 0 c.right

theorem ConwaySoifer.recvOf_Sext : recvOf ContactCase.Sext = 5

theorem ConwaySoifer.recvOf_Sint : recvOf ContactCase.Sint = 1