| INCSZ : IP2022_pseudo (* increment & skip if zero *)
| INT : IP2022_pseudo (* interrupt -- not impl. ERR *)
| IREAD : IP2022_pseudo (* memory read *)
-| IREADI : IP2022_pseudo (* memory read & inc *)
+(* NB: ignorata la differenza IREAD/IREADI perche' non e' implementata EXT_MEM
+ IREAD → ADDRX= 0x00 ram, 0x01 flash, 0x80 0x81 ext_mem
+ IREADI → ADDRX= 0x00 ram, 0x01 flash *)
| IWRITE : IP2022_pseudo (* memory write *)
-| IWRITEI : IP2022_pseudo (* memory write & inc *)
+(* NB: ignorata la differenza IWRITE/IWRITEI perche' non e' implementata EXT_MEM
+ IREAD → ADDRX= 0x00 ram, 0x80 0x81 ext_mem
+ IREADI → ADDRX= 0x00 ram *)
| JMP : IP2022_pseudo (* jump *)
| LOADH : IP2022_pseudo (* load Data Pointer High *)
| LOADL : IP2022_pseudo (* load Data Pointer Low *)
| FREAD ⇒ match ps2 with [ FREAD ⇒ true | _ ⇒ false ] | FWRITE ⇒ match ps2 with [ FWRITE ⇒ true | _ ⇒ false ]
| INC ⇒ match ps2 with [ INC ⇒ true | _ ⇒ false ] | INCSNZ ⇒ match ps2 with [ INCSNZ ⇒ true | _ ⇒ false ]
| INCSZ ⇒ match ps2 with [ INCSZ ⇒ true | _ ⇒ false ] | INT ⇒ match ps2 with [ INT ⇒ true | _ ⇒ false ]
- | IREAD ⇒ match ps2 with [ IREAD ⇒ true | _ ⇒ false ] | IREADI ⇒ match ps2 with [ IREADI ⇒ true | _ ⇒ false ]
- | IWRITE ⇒ match ps2 with [ IWRITE ⇒ true | _ ⇒ false ] | IWRITEI ⇒ match ps2 with [ IWRITEI ⇒ true | _ ⇒ false ]
+ | IREAD ⇒ match ps2 with [ IREAD ⇒ true | _ ⇒ false ] | IWRITE ⇒ match ps2 with [ IWRITE ⇒ true | _ ⇒ false ]
| JMP ⇒ match ps2 with [ JMP ⇒ true | _ ⇒ false ] | LOADH ⇒ match ps2 with [ LOADH ⇒ true | _ ⇒ false ]
| LOADL ⇒ match ps2 with [ LOADL ⇒ true | _ ⇒ false ] | MOV ⇒ match ps2 with [ MOV ⇒ true | _ ⇒ false ]
| MULS ⇒ match ps2 with [ MULS ⇒ true | _ ⇒ false ] | MULU ⇒ match ps2 with [ MULU ⇒ true | _ ⇒ false ]
ndefinition forall_IP2022_pseudo ≝ λP:IP2022_pseudo → bool.
P ADD ⊗ P ADDC ⊗ P AND ⊗ P BREAK ⊗ P BREAKX ⊗ P CALL ⊗ P CLR ⊗ P CLRB ⊗
P CMP ⊗ P CSE ⊗ P CSNE ⊗ P CWDT ⊗ P DEC ⊗ P DECSNZ ⊗ P DECSZ ⊗ P FERASE ⊗
- P FREAD ⊗ P FWRITE ⊗ P INC ⊗ P INCSNZ ⊗ P INCSZ ⊗ P INT ⊗ P IREAD ⊗ P IREADI ⊗
- P IWRITE ⊗ P IWRITEI ⊗ P JMP ⊗ P LOADH ⊗ P LOADL ⊗ P MOV ⊗ P MULS ⊗ P MULU ⊗
- P NOP ⊗ P NOT ⊗ P OR ⊗ P PAGE ⊗ P POP ⊗ P PUSH ⊗ P RET ⊗ P RETI ⊗
- P RETNP ⊗ P RETW ⊗ P RL ⊗ P RR ⊗ P SB ⊗ P SETB ⊗ P SNB ⊗ P SPEED ⊗
- P SUB ⊗ P SUBC ⊗ P SWAP ⊗ P TEST ⊗ P XOR.
+ P FREAD ⊗ P FWRITE ⊗ P INC ⊗ P INCSNZ ⊗ P INCSZ ⊗ P INT ⊗ P IREAD ⊗ P IWRITE ⊗
+ P JMP ⊗ P LOADH ⊗ P LOADL ⊗ P MOV ⊗ P MULS ⊗ P MULU ⊗ P NOP ⊗ P NOT ⊗
+ P OR ⊗ P PAGE ⊗ P POP ⊗ P PUSH ⊗ P RET ⊗ P RETI ⊗ P RETNP ⊗ P RETW ⊗
+ P RL ⊗ P RR ⊗ P SB ⊗ P SETB ⊗ P SNB ⊗ P SPEED ⊗ P SUB ⊗ P SUBC ⊗
+ P SWAP ⊗ P TEST ⊗ P XOR.