(* Progetto FreeScale *)
(* *)
(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Ultima modifica: 05/08/2009 *)
+(* Sviluppo: 2008-2010 *)
(* *)
(* ********************************************************************** *)
alias num (instance 0) = "natural number".
*)
+nlet rec nat_it (T:Type) (f:T → T) (arg:T) (n:nat) on n ≝
+ match n with
+ [ O ⇒ arg
+ | S n' ⇒ nat_it T f (f arg) n'
+ ].
+
ndefinition nat1 ≝ S O.
ndefinition nat2 ≝ S nat1.
ndefinition nat3 ≝ S nat2.
ndefinition pred ≝ λn.match n with [ O ⇒ O | S n ⇒ n ].
-ndefinition nat128 ≝ nat64 * nat2.
-ndefinition nat256 ≝ nat128 * nat2.
-ndefinition nat512 ≝ nat256 * nat2.
-ndefinition nat1024 ≝ nat512 * nat2.
-ndefinition nat2048 ≝ nat1024 * nat2.
-ndefinition nat4096 ≝ nat2048 * nat2.
-ndefinition nat8192 ≝ nat4096 * nat2.
-ndefinition nat16384 ≝ nat8192 * nat2.
-ndefinition nat32768 ≝ nat16384 * nat2.
-ndefinition nat65536 ≝ nat32768 * nat2.
+ndefinition nat128 ≝ nat64 + nat64.
+ndefinition nat256 ≝ nat128 + nat128.
+ndefinition nat512 ≝ nat256 + nat256.
+ndefinition nat1024 ≝ nat512 + nat512.
+ndefinition nat2048 ≝ nat1024 + nat1024.
+ndefinition nat4096 ≝ nat2048 + nat2048.
+ndefinition nat8192 ≝ nat4096 + nat4096.
+ndefinition nat16384 ≝ nat8192 + nat8192.
+ndefinition nat32768 ≝ nat16384 + nat16384.
+ndefinition nat65536 ≝ nat32768 + nat32768.