From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 20 Oct 2008 14:00:47 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~4653
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=38916383ce5964d801930f252e7942f90062530e;p=helm.git

...
---

diff --git a/helm/software/matita/contribs/didactic/algebra.ma b/helm/software/matita/contribs/didactic/algebra.ma
index eabbdb110..3bfa6d7f7 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,7 +67,34 @@ 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.
+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 
+    (∀v. val (EPlus (subst e1 E1 i) (subst e2 E1 i)) v =
+         val (EPlus (subst e1 E2 i) (subst e2 E2 i)) v).
+  assume v : (ℕ → ℕ).       
+  conclude (val (EPlus (subst e1 E1 i) (subst e2 E1 i)) v)
+         = (val (EPlus (subst e1 E1 i) (subst e2 E2 i)) v).
+    = (val (EPlus (subst e1 E2 i) (subst e2 E2 i)) v) by H22.
   assume n : ℕ.
   the thesis becomes 
     (equiv