Bertrand's conjecture (weak), some work in progress

[helm.git] / helm / software / matita / dama_didactic / deriv.ma

diff --git a/helm/software/matita/dama_didactic/deriv.ma b/helm/software/matita/dama_didactic/deriv.ma
index f4de77580a53d9d9d0b79791da174ef5904297a6..5c2e734c0697037a686f42c3257b25f377a23635 100644 (file)
--- a/helm/software/matita/dama_didactic/deriv.ma
+++ b/helm/software/matita/dama_didactic/deriv.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/didactic/deriv".
+
 
 include "reals.ma".
 
@@ -32,16 +32,16 @@ interpretation "function mult" 'mult x y =
 interpretation "function compositon" 'compose x y =
  (cic:/matita/didactic/deriv/fcomp.con x y).
 
-notation "hvbox(a break ⊕ b)"
+notation "hvbox(a break + b)"
   right associative with precedence 45
 for @{ 'oplus $a $b }.
 
-interpretation "function plus" 'oplus x y =
+interpretation "function plus" 'plus x y =
  (cic:/matita/didactic/deriv/fplus.con x y).
 
 axiom i:R→F. (*mappatura  R in F*)
 coercion cic:/matita/didactic/deriv/i.con.
-axiom i_comm_plus: ∀x,y:R. (i (x+y)) = (i x) ⊕ (i y).
+axiom i_comm_plus: ∀x,y:R. (i (x+y)) = (i x) + (i y).
 axiom i_comm_mult: ∀x,y:R. (i (Rmult x y)) = (i x) · (i y).
 
 axiom freflex:F.
@@ -77,22 +77,22 @@ let rec felev (f:F) (n:nat) on n: F ≝
 
 (* Proprietà *)
 
-axiom fplus_commutative: ∀ f,g:F. f ⊕ g = g ⊕ f.
-axiom fplus_associative: ∀ f,g,h:F. f ⊕ (g ⊕ h) = (f ⊕ g) ⊕ h.
-axiom fplus_neutral: ∀f:F. (i R0) ⊕ f = f.
+axiom fplus_commutative: ∀ f,g:F. f + g = g + f.
+axiom fplus_associative: ∀ f,g,h:F. f + (g + h) = (f + g) + h.
+axiom fplus_neutral: ∀f:F. (i R0) + f = f.
 axiom fmult_commutative: ∀ f,g:F. f · g = g · f.
 axiom fmult_associative: ∀ f,g,h:F. f · (g · h) = (f · g) · h.
 axiom fmult_neutral: ∀f:F. (i R1) · f = f.
 axiom fmult_assorb: ∀f:F. (i R0) · f = (i R0).
-axiom fdistr: ∀ f,g,h:F. (f ⊕ g) · h = (f · h) ⊕ (g · h).
+axiom fdistr: ∀ f,g,h:F. (f + g) · h = (f · h) + (g · h).
 axiom fcomp_associative: ∀ f,g,h:F. f ∘ (g ∘ h) = (f ∘ g) ∘ h.
 
-axiom fcomp_distr1: ∀ f,g,h:F. (f ⊕ g) ∘ h = (f ∘ h) ⊕ (g ∘ h).
+axiom fcomp_distr1: ∀ f,g,h:F. (f + g) ∘ h = (f ∘ h) + (g ∘ h).
 axiom fcomp_distr2: ∀ f,g,h:F. (f · g) ∘ h = (f ∘ h) · (g ∘ h).
 
-axiom demult: ∀ f,g:F. (f · g) ' = (f ' · g) ⊕ (f · g ').
+axiom demult: ∀ f,g:F. (f · g) ' = (f ' · g) + (f · g ').
 axiom decomp: ∀ f,g:F. (f ∘ g) ' = (f ' ∘ g) · g '.
-axiom deplus: ∀ f,g:F. (f ⊕ g) ' = (f ') ⊕ (g ').
+axiom deplus: ∀ f,g:F. (f + g) ' = (f ') + (g ').
 
 axiom cost_assorb: ∀x:R. ∀f:F. (i x) ∘ f = i x.
 axiom cost_deriv: ∀x:R. (i x) ' = i R0.
@@ -110,3 +110,5 @@ for @{ 'elev $a $b }.
  
 interpretation "function power" 'elev x y =
  (cic:/matita/didactic/deriv/felev.con x y). 
+
+axiom tech1: ∀n,m. F_OF_nat n + F_OF_nat m = F_OF_nat (n + m).