include "Universes.ma".
include "Equality.ma".
include "BitVector.ma".

ninductive AddressingMode: Type[0] ≝
  Direct: Byte → AddressingMode
| Indirect: Bit → AddressingMode
| ExtIndirect: Bit → AddressingMode
| Register: Bit → Bit → Bit → AddressingMode
| AccumulatorA: AddressingMode
| AccumulatorB: AddressingMode
| DPointer: AddressingMode
| Data: Byte → AddressingMode
| Data16: Word → AddressingMode
| AccumulatorDPointer: AddressingMode
| AccumulatorProgramCounter: AddressingMode
| ExternalIndirectDPointer: AddressingMode
| IndirectDPointer: AddressingMode
| Carry: AddressingMode
| Bit: Bit → AddressingMode
| ComplementBit: Bit → AddressingMode
| Relative: Byte → AddressingMode
| Address11: Word11 → AddressingMode
| Address16: Word → AddressingMode.