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/Freescale_pseudo_lemmas.ma".
24 include "emulator/opcodes/Freescale_instr_mode_lemmas.ma".
25 include "emulator/opcodes/IP2022_pseudo_lemmas.ma".
26 include "emulator/opcodes/IP2022_instr_mode_lemmas.ma".
27 include "emulator/opcodes/pseudo.ma".
29 nlemma eq_to_eqpseudo : ∀m.∀n1,n2.(n1 = n2) → (eq_pseudo m n1 n2 = true).
31 ##[ ##1,2,3,4: napply eq_to_eqFreescalepseudo
32 ##| ##5: napply eq_to_eqIP2022pseudo
36 nlemma neqpseudo_to_neq : ∀m.∀n1,n2.(eq_pseudo m n1 n2 = false) → (n1 ≠ n2).
38 ##[ ##1,2,3,4: napply neqFreescalepseudo_to_neq
39 ##| ##5: napply neqIP2022pseudo_to_neq
43 nlemma eqpseudo_to_eq : ∀m.∀n1,n2.(eq_pseudo m n1 n2 = true) → (n1 = n2).
45 ##[ ##1,2,3,4: napply eqFreescalepseudo_to_eq
46 ##| ##5: napply eqIP2022pseudo_to_eq
50 nlemma neq_to_neqpseudo : ∀m.∀n1,n2.(n1 ≠ n2) → (eq_pseudo m n1 n2 = false).
52 ##[ ##1,2,3,4: napply neq_to_neqFreescalepseudo
53 ##| ##5: napply neq_to_neqIP2022pseudo
57 nlemma decidable_pseudo : ∀m.∀x,y:aux_pseudo_type m.decidable (x = y).
59 ##[ ##1,2,3,4: napply decidable_Freescalepseudo
60 ##| ##5: napply decidable_IP2022pseudo
64 nlemma symmetric_eqpseudo : ∀m.symmetricT (aux_pseudo_type m) bool (eq_pseudo m).
66 ##[ ##1,2,3,4: napply symmetric_eqFreescalepseudo
67 ##| ##5: napply symmetric_eqIP2022pseudo
71 nlemma eq_to_eqim : ∀m.∀n1,n2.(n1 = n2) → (eq_im m n1 n2 = true).
73 ##[ ##1,2,3,4: napply eq_to_eqFreescaleim
74 ##| ##5: napply eq_to_eqIP2022im
78 nlemma neqim_to_neq : ∀m.∀n1,n2.(eq_im m n1 n2 = false) → (n1 ≠ n2).
80 ##[ ##1,2,3,4: napply neqFreescaleim_to_neq
81 ##| ##5: napply neqIP2022im_to_neq
85 nlemma eqim_to_eq : ∀m.∀n1,n2.(eq_im m n1 n2 = true) → (n1 = n2).
87 ##[ ##1,2,3,4: napply eqFreescaleim_to_eq
88 ##| ##5: napply eqIP2022im_to_eq
92 nlemma neq_to_neqim : ∀m.∀n1,n2.(n1 ≠ n2) → (eq_im m n1 n2 = false).
94 ##[ ##1,2,3,4: napply neq_to_neqFreescaleim
95 ##| ##5: napply neq_to_neqIP2022im
99 nlemma decidable_im : ∀m.∀x,y:aux_im_type m.decidable (x = y).
101 ##[ ##1,2,3,4: napply decidable_Freescaleim
102 ##| ##5: napply decidable_IP2022im
106 nlemma symmetric_eqim : ∀m.symmetricT (aux_im_type m) bool (eq_im m).
108 ##[ ##1,2,3,4: napply symmetric_eqFreescaleim
109 ##| ##5: napply symmetric_eqIP2022im