X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdidactic%2Falgebra.ma;h=17c30e341212c41882fc6d8c31ced3acf47251b0;hb=79a184f4d6a78a737909d7358e926716e9bab257;hp=eabbdb1104838f83fb1754e870b136dd2f381b85;hpb=4d4ea7cf3ab9ca05fa41c3f7b680cb10232acb82;p=helm.git

diff --git a/helm/software/matita/contribs/didactic/algebra.ma b/helm/software/matita/contribs/didactic/algebra.ma
index eabbdb110..17c30e341 100644
--- a/helm/software/matita/contribs/didactic/algebra.ma
+++ b/helm/software/matita/contribs/didactic/algebra.ma
@@ -8,11 +8,11 @@ notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp
 interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else _ e t f).
 
 inductive F : Type ≝
-| X       : ℕ → F
-| EPlus   : F → F → F
-| ETimes  : F → F → F
 | EZero   : F
 | EOne    : F
+| EPlus   : F → F → F
+| ETimes  : F → F → F
+| X       : ℕ → F
 .
 
 let rec val (E : F) (v : ℕ → ℕ) on E : ℕ :=
@@ -67,18 +67,35 @@ assume i : ℕ.
 suppose (equiv E1 E2) (H).
 we proceed by induction on G to prove
   (equiv (subst G E1 i) (subst G E2 i)).
-case X.
-  assume n : ℕ.
-  the thesis becomes 
-    (equiv 
-      (if (eqb i n) then E1 else (X n))
-      (subst (X n) E2 i)).
+case EZero.
+  the thesis becomes (equiv (subst EZero E1 i) (subst EZero E2 i)).
+  the thesis becomes (equiv EZero (subst EZero E2 i)).
+  the thesis becomes (equiv EZero EZero).
+  the thesis becomes (∀v.val EZero v = val EZero v).
+  assume v : (ℕ → ℕ).
+  the thesis becomes (0 = val EZero v).
+  the thesis becomes (0 = 0).
+  done.
+case EOne.  
+  the thesis becomes (∀v.val EOne v = val EOne v).
+  assume v : (ℕ → ℕ).
+  the thesis becomes (1 = 1).
+  done.
+case EPlus.
+  assume e1 : F.
+  by induction hypothesis we know (equiv (subst e1 E1 i) (subst e1 E2 i)) (H1).
+  assume e2 : F.
+  by induction hypothesis we know (equiv (subst e2 E1 i) (subst e2 E2 i)) (H2).
+  by H1 we proved (∀v.val (subst e1 E1 i) v = val (subst e1 E2 i) v) (H11).  
+  by H2 we proved (∀v.val (subst e2 E1 i) v = val (subst e2 E2 i) v) (H22).
   the thesis becomes 
-    (equiv 
-      (if (eqb i n) then E1 else (X n))
-      (if (eqb i n) then E2 else (X n))).
-  we proceed by cases ...    
-  
-
-
-  
\ No newline at end of file
+    (∀v. val (subst e1 E1 i) v + val (subst e2 E1 i) v =
+         val (subst e1 E2 i) v + val (subst e2 E2 i) v).
+  assume v : (ℕ → ℕ).       
+  conclude 
+    (val (subst e1 E1 i) v + val (subst e2 E1 i) v) =
+    (val (subst e1 E1 i) v + val (subst e2 E2 i) v) by H11.
+  conclude 
+    (val (subst e1 E1 i) v + val (subst e2 E1 i) v) =
+    (val (subst e1 E1 i) v + val (subst e2 E1 i) v) by H22.
+  done.