1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "emulator/opcodes/HC05_opcode_lemmas.ma".
24 include "emulator/opcodes/HC05_instr_mode_lemmas.ma".
25 include "emulator/opcodes/HC08_opcode_lemmas.ma".
26 include "emulator/opcodes/HC08_instr_mode_lemmas.ma".
27 include "emulator/opcodes/HCS08_opcode_lemmas.ma".
28 include "emulator/opcodes/RS08_opcode_lemmas.ma".
29 include "emulator/opcodes/RS08_instr_mode_lemmas.ma".
30 include "emulator/opcodes/IP2022_opcode_lemmas.ma".
31 include "emulator/opcodes/IP2022_instr_mode_lemmas.ma".
32 include "emulator/opcodes/opcode.ma".
34 nlemma eq_to_eqop : ∀m.∀n1,n2.(n1 = n2) → (eq_op m n1 n2 = true).
36 ##[ ##1: napply eq_to_eqHC05op
37 ##| ##2: napply eq_to_eqHC08op
38 ##| ##3: napply eq_to_eqHCS08op
39 ##| ##4: napply eq_to_eqRS08op
40 ##| ##5: napply eq_to_eqIP2022op
44 nlemma neqop_to_neq : ∀m.∀n1,n2.(eq_op m n1 n2 = false) → (n1 ≠ n2).
46 ##[ ##1: napply neqHC05op_to_neq
47 ##| ##2: napply neqHC08op_to_neq
48 ##| ##3: napply neqHCS08op_to_neq
49 ##| ##4: napply neqRS08op_to_neq
50 ##| ##5: napply neqIP2022op_to_neq
54 nlemma eqop_to_eq : ∀m.∀n1,n2.(eq_op m n1 n2 = true) → (n1 = n2).
56 ##[ ##1: napply eqHC05op_to_eq
57 ##| ##2: napply eqHC08op_to_eq
58 ##| ##3: napply eqHCS08op_to_eq
59 ##| ##4: napply eqRS08op_to_eq
60 ##| ##5: napply eqIP2022op_to_eq
64 nlemma neq_to_neqop : ∀m.∀n1,n2.(n1 ≠ n2) → (eq_op m n1 n2 = false).
66 ##[ ##1: napply neq_to_neqHC05op
67 ##| ##2: napply neq_to_neqHC08op
68 ##| ##3: napply neq_to_neqHCS08op
69 ##| ##4: napply neq_to_neqRS08op
70 ##| ##5: napply neq_to_neqIP2022op
74 nlemma decidable_op : ∀m.∀x,y:aux_op_type m.decidable (x = y).
76 ##[ ##1: napply decidable_HC05op
77 ##| ##2: napply decidable_HC08op
78 ##| ##3: napply decidable_HCS08op
79 ##| ##4: napply decidable_RS08op
80 ##| ##5: napply decidable_IP2022op
84 nlemma symmetric_eqop : ∀m.symmetricT (aux_op_type m) bool (eq_op m).
86 ##[ ##1: napply symmetric_eqHC05op
87 ##| ##2: napply symmetric_eqHC08op
88 ##| ##3: napply symmetric_eqHCS08op
89 ##| ##4: napply symmetric_eqRS08op
90 ##| ##5: napply symmetric_eqIP2022op
94 nlemma eq_to_eqim : ∀m.∀n1,n2.(n1 = n2) → (eq_im m n1 n2 = true).
96 ##[ ##1: napply eq_to_eqHC05im
97 ##| ##2: napply eq_to_eqHC08im
98 ##| ##3: napply eq_to_eqHC08im
99 ##| ##4: napply eq_to_eqRS08im
100 ##| ##5: napply eq_to_eqIP2022im
104 nlemma neqim_to_neq : ∀m.∀n1,n2.(eq_im m n1 n2 = false) → (n1 ≠ n2).
106 ##[ ##1: napply neqHC05im_to_neq
107 ##| ##2: napply neqHC08im_to_neq
108 ##| ##3: napply neqHC08im_to_neq
109 ##| ##4: napply neqRS08im_to_neq
110 ##| ##5: napply neqIP2022im_to_neq
114 nlemma eqim_to_eq : ∀m.∀n1,n2.(eq_im m n1 n2 = true) → (n1 = n2).
116 ##[ ##1: napply eqHC05im_to_eq
117 ##| ##2: napply eqHC08im_to_eq
118 ##| ##3: napply eqHC08im_to_eq
119 ##| ##4: napply eqRS08im_to_eq
120 ##| ##5: napply eqIP2022im_to_eq
124 nlemma neq_to_neqim : ∀m.∀n1,n2.(n1 ≠ n2) → (eq_im m n1 n2 = false).
126 ##[ ##1: napply neq_to_neqHC05im
127 ##| ##2: napply neq_to_neqHC08im
128 ##| ##3: napply neq_to_neqHC08im
129 ##| ##4: napply neq_to_neqRS08im
130 ##| ##5: napply neq_to_neqIP2022im
134 nlemma decidable_im : ∀m.∀x,y:aux_im_type m.decidable (x = y).
136 ##[ ##1: napply decidable_HC05im
137 ##| ##2: napply decidable_HC08im
138 ##| ##3: napply decidable_HC08im
139 ##| ##4: napply decidable_RS08im
140 ##| ##5: napply decidable_IP2022im
144 nlemma symmetric_eqim : ∀m.symmetricT (aux_im_type m) bool (eq_im m).
146 ##[ ##1: napply symmetric_eqHC05im
147 ##| ##2: napply symmetric_eqHC08im
148 ##| ##3: napply symmetric_eqHC08im
149 ##| ##4: napply symmetric_eqRS08im
150 ##| ##5: napply symmetric_eqIP2022im