X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fnum%2Fbitrigesim.ma;h=18dcce4b773bce3bb53b68d8a83685716a2a4253;hb=34e2c8f59dd7924e15a7746644182d12ad09fed3;hp=943d2cb8498f87eaccf08adcd804e09660f77b3c;hpb=b1c174cffd3c1d10383a52d63a6e662156fb0bb7;p=helm.git diff --git a/helm/software/matita/contribs/ng_assembly/num/bitrigesim.ma b/helm/software/matita/contribs/ng_assembly/num/bitrigesim.ma index 943d2cb84..18dcce4b7 100755 --- a/helm/software/matita/contribs/ng_assembly/num/bitrigesim.ma +++ b/helm/software/matita/contribs/ng_assembly/num/bitrigesim.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) @@ -64,38 +64,22 @@ ninductive bitrigesim : Type ≝ ndefinition eq_bit ≝ λt1,t2:bitrigesim. match t1 with - [ t00 ⇒ match t2 with [ t00 ⇒ true | _ ⇒ false ] - | t01 ⇒ match t2 with [ t01 ⇒ true | _ ⇒ false ] - | t02 ⇒ match t2 with [ t02 ⇒ true | _ ⇒ false ] - | t03 ⇒ match t2 with [ t03 ⇒ true | _ ⇒ false ] - | t04 ⇒ match t2 with [ t04 ⇒ true | _ ⇒ false ] - | t05 ⇒ match t2 with [ t05 ⇒ true | _ ⇒ false ] - | t06 ⇒ match t2 with [ t06 ⇒ true | _ ⇒ false ] - | t07 ⇒ match t2 with [ t07 ⇒ true | _ ⇒ false ] - | t08 ⇒ match t2 with [ t08 ⇒ true | _ ⇒ false ] - | t09 ⇒ match t2 with [ t09 ⇒ true | _ ⇒ false ] - | t0A ⇒ match t2 with [ t0A ⇒ true | _ ⇒ false ] - | t0B ⇒ match t2 with [ t0B ⇒ true | _ ⇒ false ] - | t0C ⇒ match t2 with [ t0C ⇒ true | _ ⇒ false ] - | t0D ⇒ match t2 with [ t0D ⇒ true | _ ⇒ false ] - | t0E ⇒ match t2 with [ t0E ⇒ true | _ ⇒ false ] - | t0F ⇒ match t2 with [ t0F ⇒ true | _ ⇒ false ] - | t10 ⇒ match t2 with [ t10 ⇒ true | _ ⇒ false ] - | t11 ⇒ match t2 with [ t11 ⇒ true | _ ⇒ false ] - | t12 ⇒ match t2 with [ t12 ⇒ true | _ ⇒ false ] - | t13 ⇒ match t2 with [ t13 ⇒ true | _ ⇒ false ] - | t14 ⇒ match t2 with [ t14 ⇒ true | _ ⇒ false ] - | t15 ⇒ match t2 with [ t15 ⇒ true | _ ⇒ false ] - | t16 ⇒ match t2 with [ t16 ⇒ true | _ ⇒ false ] - | t17 ⇒ match t2 with [ t17 ⇒ true | _ ⇒ false ] - | t18 ⇒ match t2 with [ t18 ⇒ true | _ ⇒ false ] - | t19 ⇒ match t2 with [ t19 ⇒ true | _ ⇒ false ] - | t1A ⇒ match t2 with [ t1A ⇒ true | _ ⇒ false ] - | t1B ⇒ match t2 with [ t1B ⇒ true | _ ⇒ false ] - | t1C ⇒ match t2 with [ t1C ⇒ true | _ ⇒ false ] - | t1D ⇒ match t2 with [ t1D ⇒ true | _ ⇒ false ] - | t1E ⇒ match t2 with [ t1E ⇒ true | _ ⇒ false ] - | t1F ⇒ match t2 with [ t1F ⇒ true | _ ⇒ false ] + [ t00 ⇒ match t2 with [ t00 ⇒ true | _ ⇒ false ] | t01 ⇒ match t2 with [ t01 ⇒ true | _ ⇒ false ] + | t02 ⇒ match t2 with [ t02 ⇒ true | _ ⇒ false ] | t03 ⇒ match t2 with [ t03 ⇒ true | _ ⇒ false ] + | t04 ⇒ match t2 with [ t04 ⇒ true | _ ⇒ false ] | t05 ⇒ match t2 with [ t05 ⇒ true | _ ⇒ false ] + | t06 ⇒ match t2 with [ t06 ⇒ true | _ ⇒ false ] | t07 ⇒ match t2 with [ t07 ⇒ true | _ ⇒ false ] + | t08 ⇒ match t2 with [ t08 ⇒ true | _ ⇒ false ] | t09 ⇒ match t2 with [ t09 ⇒ true | _ ⇒ false ] + | t0A ⇒ match t2 with [ t0A ⇒ true | _ ⇒ false ] | t0B ⇒ match t2 with [ t0B ⇒ true | _ ⇒ false ] + | t0C ⇒ match t2 with [ t0C ⇒ true | _ ⇒ false ] | t0D ⇒ match t2 with [ t0D ⇒ true | _ ⇒ false ] + | t0E ⇒ match t2 with [ t0E ⇒ true | _ ⇒ false ] | t0F ⇒ match t2 with [ t0F ⇒ true | _ ⇒ false ] + | t10 ⇒ match t2 with [ t10 ⇒ true | _ ⇒ false ] | t11 ⇒ match t2 with [ t11 ⇒ true | _ ⇒ false ] + | t12 ⇒ match t2 with [ t12 ⇒ true | _ ⇒ false ] | t13 ⇒ match t2 with [ t13 ⇒ true | _ ⇒ false ] + | t14 ⇒ match t2 with [ t14 ⇒ true | _ ⇒ false ] | t15 ⇒ match t2 with [ t15 ⇒ true | _ ⇒ false ] + | t16 ⇒ match t2 with [ t16 ⇒ true | _ ⇒ false ] | t17 ⇒ match t2 with [ t17 ⇒ true | _ ⇒ false ] + | t18 ⇒ match t2 with [ t18 ⇒ true | _ ⇒ false ] | t19 ⇒ match t2 with [ t19 ⇒ true | _ ⇒ false ] + | t1A ⇒ match t2 with [ t1A ⇒ true | _ ⇒ false ] | t1B ⇒ match t2 with [ t1B ⇒ true | _ ⇒ false ] + | t1C ⇒ match t2 with [ t1C ⇒ true | _ ⇒ false ] | t1D ⇒ match t2 with [ t1D ⇒ true | _ ⇒ false ] + | t1E ⇒ match t2 with [ t1E ⇒ true | _ ⇒ false ] | t1F ⇒ match t2 with [ t1F ⇒ true | _ ⇒ false ] ]. (* iteratore sui bitrigesimali *)