mod change (-x)

[helm.git] / helm / software / matita / contribs / ng_assembly / emulator / status / status_lemmas.ma

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/status_lemmas.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/status_lemmas.ma
old mode 100755 (executable)
new mode 100644 (file)
index aee06a2..2320efa
--- a/helm/software/matita/contribs/ng_assembly/emulator/status/status_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/status/status_lemmas.ma
@@ -27,7 +27,7 @@ include "emulator/status/IP2022_status_lemmas.ma".
 include "emulator/status/status.ma".
 include "common/option_lemmas.ma".
 include "common/prod_lemmas.ma".
-include "emulator/opcodes/opcode_lemmas.ma".
+include "emulator/opcodes/pseudo_lemmas.ma".
 
 (* *********************************** *)
 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
@@ -39,7 +39,7 @@ nlemma symmetric_eqclk : ∀m.∀clk1,clk2.eq_clk m clk1 clk2 = eq_clk m clk2 cl
  ##[ ##1: napply symmetric_eqw16
  ##| ##2: napply symmetric_eqb8
  ##| ##3: napply (symmetric_eqim m)
- ##| ##4: napply (symmetric_eqop m)
+ ##| ##4: napply (symmetric_eqpseudo m)
  ##| ##5: napply symmetric_eqb8
  ##]
 nqed.
@@ -50,7 +50,7 @@ nlemma eqclk_to_eq : ∀m.∀clk1,clk2.eq_clk m clk1 clk2 = true → clk1 = clk2
  ##[ ##1: napply eqw16_to_eq
  ##| ##2: napply eqb8_to_eq
  ##| ##3: napply (eqim_to_eq m)
- ##| ##4: napply (eqop_to_eq m)
+ ##| ##4: napply (eqpseudo_to_eq m)
  ##| ##5: napply eqb8_to_eq
  ##]
 nqed.
@@ -61,7 +61,7 @@ nlemma eq_to_eqclk : ∀m.∀clk1,clk2.(clk1 = clk2) → (eq_clk m clk1 clk2 = t
  ##[ ##1: napply eq_to_eqw16
  ##| ##2: napply eq_to_eqb8
  ##| ##3: napply (eq_to_eqim m)
- ##| ##4: napply (eq_to_eqop m)
+ ##| ##4: napply (eq_to_eqpseudo m)
  ##| ##5: napply eq_to_eqb8
  ##]
 nqed.
@@ -72,7 +72,7 @@ nlemma neqclk_to_neq : ∀m.∀clk1,clk2.eq_clk m clk1 clk2 = false → clk1 ≠
  ##[ ##1: napply neqw16_to_neq
  ##| ##2: napply neqb8_to_neq
  ##| ##3: napply (neqim_to_neq m)
- ##| ##4: napply (neqop_to_neq m)
+ ##| ##4: napply (neqpseudo_to_neq m)
  ##| ##5: napply neqb8_to_neq
  ##]
 nqed.
@@ -83,12 +83,12 @@ nlemma neq_to_neqclk : ∀m.∀clk1,clk2.(clk1 ≠ clk2) → (eq_clk m clk1 clk2
  ##[ ##1: napply neq_to_neqw16
  ##| ##2: napply neq_to_neqb8
  ##| ##3: napply (neq_to_neqim m)
- ##| ##4: napply (neq_to_neqop m)
+ ##| ##4: napply (neq_to_neqpseudo m)
  ##| ##5: napply neq_to_neqb8
  ##| ##6: napply decidable_w16
  ##| ##7: napply decidable_b8
  ##| ##8: napply (decidable_im m)
- ##| ##9: napply (decidable_op m)
+ ##| ##9: napply (decidable_pseudo m)
  ##| ##10: napply decidable_b8
  ##]
 nqed.
@@ -99,7 +99,7 @@ nlemma decidable_clk : ∀m.∀clk1,clk2:option (aux_clk_type m).decidable (clk1
  ##[ ##1: napply decidable_w16
  ##| ##2: napply decidable_b8
  ##| ##3: napply (decidable_im m)
- ##| ##4: napply (decidable_op m)
+ ##| ##4: napply (decidable_pseudo m)
  ##| ##5: napply decidable_b8
  ##]
 nqed.