X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Femulator%2Fstatus%2Fstatus_lemmas.ma;h=2320efa7db7a9e96f8c5aa2a0f53bd9957f9bbca;hb=HEAD;hp=48d10ecf686945256f6530c26565e9c741c5885c;hpb=eb4144a401147a44a9620169eb6dafeb8f5a2c17;p=helm.git

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
new mode 100644
index 48d10ecf6..2320efa7d
--- a/helm/software/matita/contribs/ng_assembly/emulator/status/status_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/status/status_lemmas.ma
@@ -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.