include "ASM.ma".

ndefinition test: List instruction ≝
 [LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;true;false;false;false]]);
  LCALL … (ADDR16 [[false;false;false;false;false;false;false;false;false;true;true;false;false;true;false;false]]);
  SJMP … (RELATIVE [[true;true;true;true;true;true;true;false]]);
  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;false;true]]),(DATA [[false;false;false;false;false;true;true;true]])〉))));
  LCALL … (ADDR16 [[false;false;false;false;false;false;false;false;false;true;true;false;true;true;true;false]]);
  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[true;false;false;false;false;false;true;false]])〉)))));
  Jump … (JZ … (RELATIVE [[false;false;false;false;false;false;true;true]]));
  LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;true;true]]);
  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;true]])〉)))));
  ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
  Jump … (JZ … (RELATIVE [[false;false;false;true;true;false;true;true]]));
  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
  MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;true;true;true;false;false;true;false]])〉)));
  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
  CLR … (ACC_A);
  MOVC … (ACC_A) (ACC_DPTR);
  MOVX … (Right … 〈(EXT_INDIRECT false),(ACC_A)〉);
  INC … (DPTR);
  INC … (REGISTER [[false;false;false]]);
  Jump … (CJNE … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉) (RELATIVE [[false;false;false;false;false;false;true;false]]));
  INC … (DIRECT [[true;false;true;false;false;false;false;false]]);
  Jump … (DJNZ … (REGISTER [[false;false;true]]) (RELATIVE [[true;true;true;true;false;true;false;false]]));
  Jump … (DJNZ … (REGISTER [[false;true;false]]) (RELATIVE [[true;true;true;true;false;false;true;false]]));
  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉))));
  CLR … (ACC_A);
  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉)))));
  MOV … (Left … (Left … (Left … (Left … (Right … 〈(INDIRECT false),(ACC_A)〉)))));
  Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;true]]));
  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;false]])〉)))));
  ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
  Jump … (JZ … (RELATIVE [[false;false;false;false;true;false;true;false]]));
  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
  CLR … (ACC_A);
  MOVX … (Right … 〈(EXT_INDIRECT true),(ACC_A)〉);
  INC … (REGISTER [[false;false;true]]);
  Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;false]]));
  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
  MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;false]])〉)))));
  ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
  Jump … (JZ … (RELATIVE [[false;false;false;false;true;true;false;false]]));
  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
  MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;false;false]])〉)));
  CLR … (ACC_A);
  MOVX … (Right … 〈(EXT_INDIRECT_DPTR),(ACC_A)〉);
  INC … (DPTR);
  Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;false]]));
  Jump … (DJNZ … (REGISTER [[false;false;true]]) (RELATIVE [[true;true;true;true;true;false;true;false]]));
  LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;true;true]]);
  MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;true;false;true]])〉)))));
  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;true;false;true]]),(DATA [[false;false;false;false;true;true;true;true]])〉))));
  XCHD … (ACC_A) (INDIRECT false);
  MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;false;false]])〉)));
  RET … ;
  MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
  RET … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ;
  NOP … ].
 @.
nqed.