Release 0.5.9.

[helm.git] / helm / software / matita / contribs / ng_assembly / num / oct.ma

diff --git a/helm/software/matita/contribs/ng_assembly/num/oct.ma b/helm/software/matita/contribs/ng_assembly/num/oct.ma
index d6bfa21e7a033b6599537d2672f04d9c25ea92d4..479a1ca8278a7f0796f60eaa5f77c9954c98ea80 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/oct.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/oct.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Sviluppo: 2008-2010                                                  *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -36,10 +36,6 @@ ninductive oct : Type ≝
 | o6: oct
 | o7: oct.
 
-(* iteratore sugli ottali *)
-ndefinition forall_oct ≝ λP.
- P o0 ⊗ P o1 ⊗ P o2 ⊗ P o3 ⊗ P o4 ⊗ P o5 ⊗ P o6 ⊗ P o7.
-
 (* operatore = *)
 ndefinition eq_oct ≝
 λn1,n2:oct.
@@ -54,92 +50,9 @@ ndefinition eq_oct ≝
   | o7 ⇒ match n2 with [ o7 ⇒ true  | _ ⇒ false ] 
   ].
 
-(* operatore and *)
-ndefinition and_oct ≝
-λe1,e2:oct.match e1 with
- [ o0 ⇒ match e2 with
-  [ o0 ⇒ o0 | o1 ⇒ o0 | o2 ⇒ o0 | o3 ⇒ o0 
-  | o4 ⇒ o0 | o5 ⇒ o0 | o6 ⇒ o0 | o7 ⇒ o0 ]
- | o1 ⇒ match e2 with
-  [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o0 | o3 ⇒ o1 
-  | o4 ⇒ o0 | o5 ⇒ o1 | o6 ⇒ o0 | o7 ⇒ o1 ]
- | o2 ⇒ match e2 with
-  [ o0 ⇒ o0 | o1 ⇒ o0 | o2 ⇒ o2 | o3 ⇒ o2 
-  | o4 ⇒ o0 | o5 ⇒ o0 | o6 ⇒ o2 | o7 ⇒ o2 ]
- | o3 ⇒ match e2 with
-  [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o2 | o3 ⇒ o3 
-  | o4 ⇒ o0 | o5 ⇒ o1 | o6 ⇒ o2 | o7 ⇒ o3 ]
- | o4 ⇒ match e2 with
-  [ o0 ⇒ o0 | o1 ⇒ o0 | o2 ⇒ o0 | o3 ⇒ o0 
-  | o4 ⇒ o4 | o5 ⇒ o4 | o6 ⇒ o4 | o7 ⇒ o4 ]
- | o5 ⇒ match e2 with
-  [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o0 | o3 ⇒ o1 
-  | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o4 | o7 ⇒ o5 ]
- | o6 ⇒ match e2 with
-  [ o0 ⇒ o0 | o1 ⇒ o0 | o2 ⇒ o2 | o3 ⇒ o2 
-  | o4 ⇒ o4 | o5 ⇒ o4 | o6 ⇒ o6 | o7 ⇒ o6 ]
- | o7 ⇒ match e2 with
-  [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o2 | o3 ⇒ o3 
-  | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o6 | o7 ⇒ o7 ]
- ]. 
-
-(* operatore or *)
-ndefinition or_oct ≝
-λe1,e2:oct.match e1 with
- [ o0 ⇒ match e2 with
-  [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o2 | o3 ⇒ o3 
-  | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o6 | o7 ⇒ o7 ]
- | o1 ⇒ match e2 with
-  [ o0 ⇒ o1 | o1 ⇒ o1 | o2 ⇒ o3 | o3 ⇒ o3 
-  | o4 ⇒ o5 | o5 ⇒ o5 | o6 ⇒ o7 | o7 ⇒ o7 ]
- | o2 ⇒ match e2 with
-  [ o0 ⇒ o2 | o1 ⇒ o3 | o2 ⇒ o2 | o3 ⇒ o3 
-  | o4 ⇒ o6 | o5 ⇒ o7 | o6 ⇒ o6 | o7 ⇒ o7 ]
- | o3 ⇒ match e2 with
-  [ o0 ⇒ o3 | o1 ⇒ o3 | o2 ⇒ o3 | o3 ⇒ o3 
-  | o4 ⇒ o7 | o5 ⇒ o7 | o6 ⇒ o7 | o7 ⇒ o7 ]
- | o4 ⇒ match e2 with
-  [ o0 ⇒ o4 | o1 ⇒ o5 | o2 ⇒ o6 | o3 ⇒ o7 
-  | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o6 | o7 ⇒ o7 ]
- | o5 ⇒ match e2 with
-  [ o0 ⇒ o5 | o1 ⇒ o5 | o2 ⇒ o7 | o3 ⇒ o7 
-  | o4 ⇒ o5 | o5 ⇒ o5 | o6 ⇒ o7 | o7 ⇒ o7 ]
- | o6 ⇒ match e2 with
-  [ o0 ⇒ o6 | o1 ⇒ o7 | o2 ⇒ o6 | o3 ⇒ o7 
-  | o4 ⇒ o6 | o5 ⇒ o7 | o6 ⇒ o6 | o7 ⇒ o7 ]
- | o7 ⇒ match e2 with
-  [ o0 ⇒ o7 | o1 ⇒ o7 | o2 ⇒ o7 | o3 ⇒ o7 
-  | o4 ⇒ o7 | o5 ⇒ o7 | o6 ⇒ o7 | o7 ⇒ o7 ]
- ].
-
-(* operatore xor *)
-ndefinition xor_oct ≝
-λe1,e2:oct.match e1 with
- [ o0 ⇒ match e2 with
-  [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o2 | o3 ⇒ o3 
-  | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o6 | o7 ⇒ o7 ] 
- | o1 ⇒ match e2 with
-  [ o0 ⇒ o1 | o1 ⇒ o0 | o2 ⇒ o3 | o3 ⇒ o2 
-  | o4 ⇒ o5 | o5 ⇒ o4 | o6 ⇒ o7 | o7 ⇒ o6 ] 
- | o2 ⇒ match e2 with
-  [ o0 ⇒ o2 | o1 ⇒ o3 | o2 ⇒ o0 | o3 ⇒ o1 
-  | o4 ⇒ o6 | o5 ⇒ o7 | o6 ⇒ o4 | o7 ⇒ o5 ] 
- | o3 ⇒ match e2 with
-  [ o0 ⇒ o3 | o1 ⇒ o2 | o2 ⇒ o1 | o3 ⇒ o0 
-  | o4 ⇒ o7 | o5 ⇒ o6 | o6 ⇒ o5 | o7 ⇒ o4 ] 
- | o4 ⇒ match e2 with
-  [ o0 ⇒ o4 | o1 ⇒ o5 | o2 ⇒ o6 | o3 ⇒ o7 
-  | o4 ⇒ o0 | o5 ⇒ o1 | o6 ⇒ o2 | o7 ⇒ o3 ] 
- | o5 ⇒ match e2 with
-  [ o0 ⇒ o5 | o1 ⇒ o4 | o2 ⇒ o7 | o3 ⇒ o6 
-  | o4 ⇒ o1 | o5 ⇒ o0 | o6 ⇒ o3 | o7 ⇒ o2 ] 
- | o6 ⇒ match e2 with
-  [ o0 ⇒ o6 | o1 ⇒ o7 | o2 ⇒ o4 | o3 ⇒ o5 
-  | o4 ⇒ o2 | o5 ⇒ o3 | o6 ⇒ o0 | o7 ⇒ o1 ] 
- | o7 ⇒ match e2 with
-  [ o0 ⇒ o7 | o1 ⇒ o6 | o2 ⇒ o5 | o3 ⇒ o4 
-  | o4 ⇒ o3 | o5 ⇒ o2 | o6 ⇒ o1 | o7 ⇒ o0 ] 
- ].
+(* iteratore sugli ottali *)
+ndefinition forall_oct ≝ λP.
+ P o0 ⊗ P o1 ⊗ P o2 ⊗ P o3 ⊗ P o4 ⊗ P o5 ⊗ P o6 ⊗ P o7.
 
 (* operatore successore *)
 ndefinition succ_oct ≝