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.
(* 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.
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).