freescale porting

[helm.git] / helm / software / matita / contribs / ng_assembly / emulator / opcodes / opcode_lemmas.ma

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/opcode_lemmas.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/opcode_lemmas.ma
deleted file mode 100755 (executable)
index bb12d86..0000000
--- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/opcode_lemmas.ma
+++ /dev/null
@@ -1,152 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* ********************************************************************** *)
-(*                          Progetto FreeScale                            *)
-(*                                                                        *)
-(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Sviluppo: 2008-2010                                                  *)
-(*                                                                        *)
-(* ********************************************************************** *)
-
-include "emulator/opcodes/HC05_opcode_lemmas.ma".
-include "emulator/opcodes/HC05_instr_mode_lemmas.ma".
-include "emulator/opcodes/HC08_opcode_lemmas.ma".
-include "emulator/opcodes/HC08_instr_mode_lemmas.ma".
-include "emulator/opcodes/HCS08_opcode_lemmas.ma".
-include "emulator/opcodes/RS08_opcode_lemmas.ma".
-include "emulator/opcodes/RS08_instr_mode_lemmas.ma".
-include "emulator/opcodes/IP2022_opcode_lemmas.ma".
-include "emulator/opcodes/IP2022_instr_mode_lemmas.ma".
-include "emulator/opcodes/opcode.ma".
-
-nlemma eq_to_eqop : ∀m.∀n1,n2.(n1 = n2) → (eq_op m n1 n2 = true).
- #m; nelim m;
- ##[ ##1: napply eq_to_eqHC05op
- ##| ##2: napply eq_to_eqHC08op
- ##| ##3: napply eq_to_eqHCS08op
- ##| ##4: napply eq_to_eqRS08op
- ##| ##5: napply eq_to_eqIP2022op
- ##]
-nqed.
-
-nlemma neqop_to_neq : ∀m.∀n1,n2.(eq_op m n1 n2 = false) → (n1 ≠ n2).
- #m; nelim m;
- ##[ ##1: napply neqHC05op_to_neq
- ##| ##2: napply neqHC08op_to_neq
- ##| ##3: napply neqHCS08op_to_neq
- ##| ##4: napply neqRS08op_to_neq
- ##| ##5: napply neqIP2022op_to_neq
- ##]
-nqed.
-
-nlemma eqop_to_eq : ∀m.∀n1,n2.(eq_op m n1 n2 = true) → (n1 = n2).
- #m; nelim m;
- ##[ ##1: napply eqHC05op_to_eq
- ##| ##2: napply eqHC08op_to_eq
- ##| ##3: napply eqHCS08op_to_eq
- ##| ##4: napply eqRS08op_to_eq
- ##| ##5: napply eqIP2022op_to_eq
- ##]
-nqed.
-
-nlemma neq_to_neqop : ∀m.∀n1,n2.(n1 ≠ n2) → (eq_op m n1 n2 = false).
- #m; nelim m;
- ##[ ##1: napply neq_to_neqHC05op
- ##| ##2: napply neq_to_neqHC08op
- ##| ##3: napply neq_to_neqHCS08op
- ##| ##4: napply neq_to_neqRS08op
- ##| ##5: napply neq_to_neqIP2022op
- ##]
-nqed.
-
-nlemma decidable_op : ∀m.∀x,y:aux_op_type m.decidable (x = y).
- #m; nelim m;
- ##[ ##1: napply decidable_HC05op
- ##| ##2: napply decidable_HC08op
- ##| ##3: napply decidable_HCS08op
- ##| ##4: napply decidable_RS08op
- ##| ##5: napply decidable_IP2022op
- ##]
-nqed.
-
-nlemma symmetric_eqop : ∀m.symmetricT (aux_op_type m) bool (eq_op m).
- #m; nelim m;
- ##[ ##1: napply symmetric_eqHC05op
- ##| ##2: napply symmetric_eqHC08op
- ##| ##3: napply symmetric_eqHCS08op
- ##| ##4: napply symmetric_eqRS08op
- ##| ##5: napply symmetric_eqIP2022op
- ##]
-nqed.
-
-nlemma eq_to_eqim : ∀m.∀n1,n2.(n1 = n2) → (eq_im m n1 n2 = true).
- #m; nelim m;
- ##[ ##1: napply eq_to_eqHC05im
- ##| ##2: napply eq_to_eqHC08im
- ##| ##3: napply eq_to_eqHC08im
- ##| ##4: napply eq_to_eqRS08im
- ##| ##5: napply eq_to_eqIP2022im
- ##]
-nqed.
-
-nlemma neqim_to_neq : ∀m.∀n1,n2.(eq_im m n1 n2 = false) → (n1 ≠ n2).
- #m; nelim m;
- ##[ ##1: napply neqHC05im_to_neq
- ##| ##2: napply neqHC08im_to_neq
- ##| ##3: napply neqHC08im_to_neq
- ##| ##4: napply neqRS08im_to_neq
- ##| ##5: napply neqIP2022im_to_neq
- ##]
-nqed.
-
-nlemma eqim_to_eq : ∀m.∀n1,n2.(eq_im m n1 n2 = true) → (n1 = n2).
- #m; nelim m;
- ##[ ##1: napply eqHC05im_to_eq
- ##| ##2: napply eqHC08im_to_eq
- ##| ##3: napply eqHC08im_to_eq
- ##| ##4: napply eqRS08im_to_eq
- ##| ##5: napply eqIP2022im_to_eq
- ##]
-nqed.
-
-nlemma neq_to_neqim : ∀m.∀n1,n2.(n1 ≠ n2) → (eq_im m n1 n2 = false).
- #m; nelim m;
- ##[ ##1: napply neq_to_neqHC05im
- ##| ##2: napply neq_to_neqHC08im
- ##| ##3: napply neq_to_neqHC08im
- ##| ##4: napply neq_to_neqRS08im
- ##| ##5: napply neq_to_neqIP2022im
- ##]
-nqed.
-
-nlemma decidable_im : ∀m.∀x,y:aux_im_type m.decidable (x = y).
- #m; nelim m;
- ##[ ##1: napply decidable_HC05im
- ##| ##2: napply decidable_HC08im
- ##| ##3: napply decidable_HC08im
- ##| ##4: napply decidable_RS08im
- ##| ##5: napply decidable_IP2022im
- ##]
-nqed.
-
-nlemma symmetric_eqim : ∀m.symmetricT (aux_im_type m) bool (eq_im m).
- #m; nelim m;
- ##[ ##1: napply symmetric_eqHC05im
- ##| ##2: napply symmetric_eqHC08im
- ##| ##3: napply symmetric_eqHC08im
- ##| ##4: napply symmetric_eqRS08im
- ##| ##5: napply symmetric_eqIP2022im
- ##]
-nqed.