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.