X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Funiverse%2Funiverse.ma;h=a673c999ba2f5147a25cc813c1ff21bee31405fb;hb=a62de71cf6821c955bd41fa691c52ea62173f25d;hp=2d84b78e5d767be04195348a2a1c32c14186194d;hpb=f9b16ad62794042c2b31c6e3433b3c4035f8a0d5;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/universe/universe.ma b/helm/software/matita/contribs/ng_assembly/universe/universe.ma
index 2d84b78e5..a673c999b 100755
--- a/helm/software/matita/contribs/ng_assembly/universe/universe.ma
+++ b/helm/software/matita/contribs/ng_assembly/universe/universe.ma
@@ -21,663 +21,242 @@
 (* ********************************************************************** *)
 
 include "common/list.ma".
-include "num/bool_lemmas.ma".
+include "common/nat_lemmas.ma".
+include "common/prod.ma".
 
-nlet rec nmember_list (T:Type) (elem:T) (f:T → T → bool) (l:list T) on l ≝
+nlet rec nmember_natList (elem:nat) (l:ne_list nat) on l ≝
  match l with
-  [ nil ⇒ true
-  | cons h t ⇒ match f elem h with
-   [ true ⇒ false | false ⇒ nmember_list T elem f t ]
+  [ ne_nil h ⇒ ⊖(eq_nat elem h)
+  | ne_cons h t ⇒ match eq_nat elem h with
+   [ true ⇒ false | false ⇒ nmember_natList elem t ]
   ].
 
 (* elem presente una ed una sola volta in l *)
-nlet rec member_list (T:Type) (elem:T) (f:T → T → bool) (l:list T) on l ≝
+nlet rec member_natList (elem:nat) (l:ne_list nat) on l ≝
  match l with
-  [ nil ⇒ false
-  | cons h t ⇒ match f elem h with
-    [ true ⇒ nmember_list T elem f t | false ⇒ member_list T elem f t ]
+  [ ne_nil h ⇒ eq_nat elem h
+  | ne_cons h t ⇒ match eq_nat elem h with
+    [ true ⇒ nmember_natList elem t | false ⇒ member_natList elem t ]
   ].
 
-(* tutti gli atomi dell'universo che poi saranno raggruppati in sottouniversi *)
-ninductive UN : Type ≝
-(* quaternari[4] 1-4 *)
-  uq0 : UN
-| uq1 : UN
-| uq2 : UN
-| uq3 : UN
-
-(* ottali[8] 5-12 *)
-| uo0 : UN
-| uo1 : UN
-| uo2 : UN
-| uo3 : UN
-| uo4 : UN
-| uo5 : UN
-| uo6 : UN
-| uo7 : UN
-
-(* esadecimali[16] 13-28 *)
-| ux0 : UN
-| ux1 : UN
-| ux2 : UN
-| ux3 : UN
-| ux4 : UN
-| ux5 : UN
-| ux6 : UN
-| ux7 : UN
-| ux8 : UN
-| ux9 : UN
-| uxA : UN
-| uxB : UN
-| uxC : UN
-| uxD : UN
-| uxE : UN
-| uxF : UN
-
-(* bitrigesimali[32] 29-60 *)
-| ut00 : UN
-| ut01 : UN
-| ut02 : UN
-| ut03 : UN
-| ut04 : UN
-| ut05 : UN
-| ut06 : UN
-| ut07 : UN
-| ut08 : UN
-| ut09 : UN
-| ut0A : UN
-| ut0B : UN
-| ut0C : UN
-| ut0D : UN
-| ut0E : UN
-| ut0F : UN
-| ut10 : UN
-| ut11 : UN
-| ut12 : UN
-| ut13 : UN
-| ut14 : UN
-| ut15 : UN
-| ut16 : UN
-| ut17 : UN
-| ut18 : UN
-| ut19 : UN
-| ut1A : UN
-| ut1B : UN
-| ut1C : UN
-| ut1D : UN
-| ut1E : UN
-| ut1F : UN
-
-(* ascii[63] 61-123 *)
-| uch_0 : UN
-| uch_1 : UN
-| uch_2 : UN
-| uch_3 : UN
-| uch_4 : UN
-| uch_5 : UN
-| uch_6 : UN
-| uch_7 : UN
-| uch_8 : UN
-| uch_9 : UN
-| uch__ : UN
-| uch_A : UN
-| uch_B : UN
-| uch_C : UN
-| uch_D : UN
-| uch_E : UN
-| uch_F : UN
-| uch_G : UN
-| uch_H : UN
-| uch_I : UN
-| uch_J : UN
-| uch_K : UN
-| uch_L : UN
-| uch_M : UN
-| uch_N : UN
-| uch_O : UN
-| uch_P : UN
-| uch_Q : UN
-| uch_R : UN
-| uch_S : UN
-| uch_T : UN
-| uch_U : UN
-| uch_V : UN
-| uch_W : UN
-| uch_X : UN
-| uch_Y : UN
-| uch_Z : UN
-| uch_a : UN
-| uch_b : UN
-| uch_c : UN
-| uch_d : UN
-| uch_e : UN
-| uch_f : UN
-| uch_g : UN
-| uch_h : UN
-| uch_i : UN
-| uch_j : UN
-| uch_k : UN
-| uch_l : UN
-| uch_m : UN
-| uch_n : UN
-| uch_o : UN
-| uch_p : UN
-| uch_q : UN
-| uch_r : UN
-| uch_s : UN
-| uch_t : UN
-| uch_u : UN
-| uch_v : UN
-| uch_w : UN
-| uch_x : UN
-| uch_y : UN
-| uch_z : UN
-
-(* opcode[91] 124-214 *)
-| uADC    : UN
-| uADD    : UN
-| uAIS    : UN
-| uAIX    : UN
-| uAND    : UN
-| uASL    : UN
-| uASR    : UN
-| uBCC    : UN
-| uBCLRn  : UN
-| uBCS    : UN
-| uBEQ    : UN
-| uBGE    : UN
-| uBGND   : UN
-| uBGT    : UN
-| uBHCC   : UN
-| uBHCS   : UN
-| uBHI    : UN
-| uBIH    : UN
-| uBIL    : UN
-| uBIT    : UN
-| uBLE    : UN
-| uBLS    : UN
-| uBLT    : UN
-| uBMC    : UN
-| uBMI    : UN
-| uBMS    : UN
-| uBNE    : UN
-| uBPL    : UN
-| uBRA    : UN
-| uBRCLRn : UN
-| uBRN    : UN
-| uBRSETn : UN
-| uBSETn  : UN
-| uBSR    : UN
-| uCBEQA  : UN
-| uCBEQX  : UN
-| uCLC    : UN
-| uCLI    : UN
-| uCLR    : UN
-| uCMP    : UN
-| uCOM    : UN
-| uCPHX   : UN
-| uCPX    : UN
-| uDAA    : UN
-| uDBNZ   : UN
-| uDEC    : UN
-| uDIV    : UN
-| uEOR    : UN
-| uINC    : UN
-| uJMP    : UN
-| uJSR    : UN
-| uLDA    : UN
-| uLDHX   : UN
-| uLDX    : UN
-| uLSR    : UN
-| uMOV    : UN
-| uMUL    : UN
-| uNEG    : UN
-| uNOP    : UN
-| uNSA    : UN
-| uORA    : UN
-| uPSHA   : UN
-| uPSHH   : UN
-| uPSHX   : UN
-| uPULA   : UN
-| uPULH   : UN
-| uPULX   : UN
-| uROL    : UN
-| uROR    : UN
-| uRSP    : UN
-| uRTI    : UN
-| uRTS    : UN
-| uSBC    : UN
-| uSEC    : UN
-| uSEI    : UN
-| uSHA    : UN
-| uSLA    : UN
-| uSTA    : UN
-| uSTHX   : UN
-| uSTOP   : UN
-| uSTX    : UN
-| uSUB    : UN
-| uSWI    : UN
-| uTAP    : UN
-| uTAX    : UN
-| uTPA    : UN
-| uTST    : UN
-| uTSX    : UN
-| uTXA    : UN
-| uTXS    : UN
-| uWAIT   : UN
-.
-
-(* funzione di uguaglianza sugli atomi *)
-ndefinition eq_UN ≝
-λu1,u2.match u1 with
- [ uq0 ⇒ match u2 with [ uq0 ⇒ true | _ ⇒ false ]
- | uq1 ⇒ match u2 with [ uq1 ⇒ true | _ ⇒ false ]
- | uq2 ⇒ match u2 with [ uq2 ⇒ true | _ ⇒ false ]
- | uq3 ⇒ match u2 with [ uq3 ⇒ true | _ ⇒ false ]
-
- | uo0 ⇒ match u2 with [ uo0 ⇒ true | _ ⇒ false ]
- | uo1 ⇒ match u2 with [ uo1 ⇒ true | _ ⇒ false ]
- | uo2 ⇒ match u2 with [ uo2 ⇒ true | _ ⇒ false ]
- | uo3 ⇒ match u2 with [ uo3 ⇒ true | _ ⇒ false ]
- | uo4 ⇒ match u2 with [ uo4 ⇒ true | _ ⇒ false ]
- | uo5 ⇒ match u2 with [ uo5 ⇒ true | _ ⇒ false ]
- | uo6 ⇒ match u2 with [ uo6 ⇒ true | _ ⇒ false ]
- | uo7 ⇒ match u2 with [ uo7 ⇒ true | _ ⇒ false ]
-
- | ux0 ⇒ match u2 with [ ux0 ⇒ true | _ ⇒ false ]
- | ux1 ⇒ match u2 with [ ux1 ⇒ true | _ ⇒ false ]
- | ux2 ⇒ match u2 with [ ux2 ⇒ true | _ ⇒ false ]
- | ux3 ⇒ match u2 with [ ux3 ⇒ true | _ ⇒ false ]
- | ux4 ⇒ match u2 with [ ux4 ⇒ true | _ ⇒ false ]
- | ux5 ⇒ match u2 with [ ux5 ⇒ true | _ ⇒ false ]
- | ux6 ⇒ match u2 with [ ux6 ⇒ true | _ ⇒ false ]
- | ux7 ⇒ match u2 with [ ux7 ⇒ true | _ ⇒ false ]
- | ux8 ⇒ match u2 with [ ux8 ⇒ true | _ ⇒ false ]
- | ux9 ⇒ match u2 with [ ux9 ⇒ true | _ ⇒ false ]
- | uxA ⇒ match u2 with [ uxA ⇒ true | _ ⇒ false ]
- | uxB ⇒ match u2 with [ uxB ⇒ true | _ ⇒ false ]
- | uxC ⇒ match u2 with [ uxC ⇒ true | _ ⇒ false ]
- | uxD ⇒ match u2 with [ uxD ⇒ true | _ ⇒ false ]
- | uxE ⇒ match u2 with [ uxE ⇒ true | _ ⇒ false ]
- | uxF ⇒ match u2 with [ uxF ⇒ true | _ ⇒ false ]
-
- | ut00 ⇒ match u2 with [ ut00 ⇒ true | _ ⇒ false ]
- | ut01 ⇒ match u2 with [ ut01 ⇒ true | _ ⇒ false ]
- | ut02 ⇒ match u2 with [ ut02 ⇒ true | _ ⇒ false ]
- | ut03 ⇒ match u2 with [ ut03 ⇒ true | _ ⇒ false ]
- | ut04 ⇒ match u2 with [ ut04 ⇒ true | _ ⇒ false ]
- | ut05 ⇒ match u2 with [ ut05 ⇒ true | _ ⇒ false ]
- | ut06 ⇒ match u2 with [ ut06 ⇒ true | _ ⇒ false ]
- | ut07 ⇒ match u2 with [ ut07 ⇒ true | _ ⇒ false ]
- | ut08 ⇒ match u2 with [ ut08 ⇒ true | _ ⇒ false ]
- | ut09 ⇒ match u2 with [ ut09 ⇒ true | _ ⇒ false ]
- | ut0A ⇒ match u2 with [ ut0A ⇒ true | _ ⇒ false ]
- | ut0B ⇒ match u2 with [ ut0B ⇒ true | _ ⇒ false ]
- | ut0C ⇒ match u2 with [ ut0C ⇒ true | _ ⇒ false ]
- | ut0D ⇒ match u2 with [ ut0D ⇒ true | _ ⇒ false ]
- | ut0E ⇒ match u2 with [ ut0E ⇒ true | _ ⇒ false ]
- | ut0F ⇒ match u2 with [ ut0F ⇒ true | _ ⇒ false ]
- | ut10 ⇒ match u2 with [ ut10 ⇒ true | _ ⇒ false ]
- | ut11 ⇒ match u2 with [ ut11 ⇒ true | _ ⇒ false ]
- | ut12 ⇒ match u2 with [ ut12 ⇒ true | _ ⇒ false ]
- | ut13 ⇒ match u2 with [ ut13 ⇒ true | _ ⇒ false ]
- | ut14 ⇒ match u2 with [ ut14 ⇒ true | _ ⇒ false ]
- | ut15 ⇒ match u2 with [ ut15 ⇒ true | _ ⇒ false ]
- | ut16 ⇒ match u2 with [ ut16 ⇒ true | _ ⇒ false ]
- | ut17 ⇒ match u2 with [ ut17 ⇒ true | _ ⇒ false ]
- | ut18 ⇒ match u2 with [ ut18 ⇒ true | _ ⇒ false ]
- | ut19 ⇒ match u2 with [ ut19 ⇒ true | _ ⇒ false ]
- | ut1A ⇒ match u2 with [ ut1A ⇒ true | _ ⇒ false ]
- | ut1B ⇒ match u2 with [ ut1B ⇒ true | _ ⇒ false ]
- | ut1C ⇒ match u2 with [ ut1C ⇒ true | _ ⇒ false ]
- | ut1D ⇒ match u2 with [ ut1D ⇒ true | _ ⇒ false ]
- | ut1E ⇒ match u2 with [ ut1E ⇒ true | _ ⇒ false ]
- | ut1F ⇒ match u2 with [ ut1F ⇒ true | _ ⇒ false ]
-
- | uch_0 ⇒ match u2 with [ uch_0 ⇒ true | _ ⇒ false ]
- | uch_1 ⇒ match u2 with [ uch_1 ⇒ true | _ ⇒ false ]
- | uch_2 ⇒ match u2 with [ uch_2 ⇒ true | _ ⇒ false ]
- | uch_3 ⇒ match u2 with [ uch_3 ⇒ true | _ ⇒ false ]
- | uch_4 ⇒ match u2 with [ uch_4 ⇒ true | _ ⇒ false ]
- | uch_5 ⇒ match u2 with [ uch_5 ⇒ true | _ ⇒ false ]
- | uch_6 ⇒ match u2 with [ uch_6 ⇒ true | _ ⇒ false ]
- | uch_7 ⇒ match u2 with [ uch_7 ⇒ true | _ ⇒ false ]
- | uch_8 ⇒ match u2 with [ uch_8 ⇒ true | _ ⇒ false ]
- | uch_9 ⇒ match u2 with [ uch_9 ⇒ true | _ ⇒ false ]
- | uch__ ⇒ match u2 with [ uch__ ⇒ true | _ ⇒ false ]
- | uch_A ⇒ match u2 with [ uch_A ⇒ true | _ ⇒ false ]
- | uch_B ⇒ match u2 with [ uch_B ⇒ true | _ ⇒ false ]
- | uch_C ⇒ match u2 with [ uch_C ⇒ true | _ ⇒ false ]
- | uch_D ⇒ match u2 with [ uch_D ⇒ true | _ ⇒ false ]
- | uch_E ⇒ match u2 with [ uch_E ⇒ true | _ ⇒ false ]
- | uch_F ⇒ match u2 with [ uch_F ⇒ true | _ ⇒ false ]
- | uch_G ⇒ match u2 with [ uch_G ⇒ true | _ ⇒ false ]
- | uch_H ⇒ match u2 with [ uch_H ⇒ true | _ ⇒ false ]
- | uch_I ⇒ match u2 with [ uch_I ⇒ true | _ ⇒ false ]
- | uch_J ⇒ match u2 with [ uch_J ⇒ true | _ ⇒ false ]
- | uch_K ⇒ match u2 with [ uch_K ⇒ true | _ ⇒ false ]
- | uch_L ⇒ match u2 with [ uch_L ⇒ true | _ ⇒ false ]
- | uch_M ⇒ match u2 with [ uch_M ⇒ true | _ ⇒ false ]
- | uch_N ⇒ match u2 with [ uch_N ⇒ true | _ ⇒ false ]
- | uch_O ⇒ match u2 with [ uch_O ⇒ true | _ ⇒ false ]
- | uch_P ⇒ match u2 with [ uch_P ⇒ true | _ ⇒ false ]
- | uch_Q ⇒ match u2 with [ uch_Q ⇒ true | _ ⇒ false ]
- | uch_R ⇒ match u2 with [ uch_R ⇒ true | _ ⇒ false ]
- | uch_S ⇒ match u2 with [ uch_S ⇒ true | _ ⇒ false ]
- | uch_T ⇒ match u2 with [ uch_T ⇒ true | _ ⇒ false ]
- | uch_U ⇒ match u2 with [ uch_U ⇒ true | _ ⇒ false ]
- | uch_V ⇒ match u2 with [ uch_V ⇒ true | _ ⇒ false ]
- | uch_W ⇒ match u2 with [ uch_W ⇒ true | _ ⇒ false ]
- | uch_X ⇒ match u2 with [ uch_X ⇒ true | _ ⇒ false ]
- | uch_Y ⇒ match u2 with [ uch_Y ⇒ true | _ ⇒ false ]
- | uch_Z ⇒ match u2 with [ uch_Z ⇒ true | _ ⇒ false ]
- | uch_a ⇒ match u2 with [ uch_a ⇒ true | _ ⇒ false ]
- | uch_b ⇒ match u2 with [ uch_b ⇒ true | _ ⇒ false ]
- | uch_c ⇒ match u2 with [ uch_c ⇒ true | _ ⇒ false ]
- | uch_d ⇒ match u2 with [ uch_d ⇒ true | _ ⇒ false ]
- | uch_e ⇒ match u2 with [ uch_e ⇒ true | _ ⇒ false ]
- | uch_f ⇒ match u2 with [ uch_f ⇒ true | _ ⇒ false ]
- | uch_g ⇒ match u2 with [ uch_g ⇒ true | _ ⇒ false ]
- | uch_h ⇒ match u2 with [ uch_h ⇒ true | _ ⇒ false ]
- | uch_i ⇒ match u2 with [ uch_i ⇒ true | _ ⇒ false ]
- | uch_j ⇒ match u2 with [ uch_j ⇒ true | _ ⇒ false ]
- | uch_k ⇒ match u2 with [ uch_k ⇒ true | _ ⇒ false ]
- | uch_l ⇒ match u2 with [ uch_l ⇒ true | _ ⇒ false ]
- | uch_m ⇒ match u2 with [ uch_m ⇒ true | _ ⇒ false ]
- | uch_n ⇒ match u2 with [ uch_n ⇒ true | _ ⇒ false ]
- | uch_o ⇒ match u2 with [ uch_o ⇒ true | _ ⇒ false ]
- | uch_p ⇒ match u2 with [ uch_p ⇒ true | _ ⇒ false ]
- | uch_q ⇒ match u2 with [ uch_q ⇒ true | _ ⇒ false ]
- | uch_r ⇒ match u2 with [ uch_r ⇒ true | _ ⇒ false ]
- | uch_s ⇒ match u2 with [ uch_s ⇒ true | _ ⇒ false ]
- | uch_t ⇒ match u2 with [ uch_t ⇒ true | _ ⇒ false ]
- | uch_u ⇒ match u2 with [ uch_u ⇒ true | _ ⇒ false ]
- | uch_v ⇒ match u2 with [ uch_v ⇒ true | _ ⇒ false ]
- | uch_w ⇒ match u2 with [ uch_w ⇒ true | _ ⇒ false ]
- | uch_x ⇒ match u2 with [ uch_x ⇒ true | _ ⇒ false ]
- | uch_y ⇒ match u2 with [ uch_y ⇒ true | _ ⇒ false ]
- | uch_z ⇒ match u2 with [ uch_z ⇒ true | _ ⇒ false ]
-
- | uADC    ⇒ match u2 with [ uADC    ⇒ true | _ ⇒ false ]
- | uADD    ⇒ match u2 with [ uADD    ⇒ true | _ ⇒ false ]
- | uAIS    ⇒ match u2 with [ uAIS    ⇒ true | _ ⇒ false ]
- | uAIX    ⇒ match u2 with [ uAIX    ⇒ true | _ ⇒ false ]
- | uAND    ⇒ match u2 with [ uAND    ⇒ true | _ ⇒ false ]
- | uASL    ⇒ match u2 with [ uASL    ⇒ true | _ ⇒ false ]
- | uASR    ⇒ match u2 with [ uASR    ⇒ true | _ ⇒ false ]
- | uBCC    ⇒ match u2 with [ uBCC    ⇒ true | _ ⇒ false ]
- | uBCLRn  ⇒ match u2 with [ uBCLRn  ⇒ true | _ ⇒ false ]
- | uBCS    ⇒ match u2 with [ uBCS    ⇒ true | _ ⇒ false ]
- | uBEQ    ⇒ match u2 with [ uBEQ    ⇒ true | _ ⇒ false ]
- | uBGE    ⇒ match u2 with [ uBGE    ⇒ true | _ ⇒ false ]
- | uBGND   ⇒ match u2 with [ uBGND   ⇒ true | _ ⇒ false ]
- | uBGT    ⇒ match u2 with [ uBGT    ⇒ true | _ ⇒ false ]
- | uBHCC   ⇒ match u2 with [ uBHCC   ⇒ true | _ ⇒ false ]
- | uBHCS   ⇒ match u2 with [ uBHCS   ⇒ true | _ ⇒ false ]
- | uBHI    ⇒ match u2 with [ uBHI    ⇒ true | _ ⇒ false ]
- | uBIH    ⇒ match u2 with [ uBIH    ⇒ true | _ ⇒ false ]
- | uBIL    ⇒ match u2 with [ uBIL    ⇒ true | _ ⇒ false ]
- | uBIT    ⇒ match u2 with [ uBIT    ⇒ true | _ ⇒ false ]
- | uBLE    ⇒ match u2 with [ uBLE    ⇒ true | _ ⇒ false ]
- | uBLS    ⇒ match u2 with [ uBLS    ⇒ true | _ ⇒ false ]
- | uBLT    ⇒ match u2 with [ uBLT    ⇒ true | _ ⇒ false ]
- | uBMC    ⇒ match u2 with [ uBMC    ⇒ true | _ ⇒ false ]
- | uBMI    ⇒ match u2 with [ uBMI    ⇒ true | _ ⇒ false ]
- | uBMS    ⇒ match u2 with [ uBMS    ⇒ true | _ ⇒ false ]
- | uBNE    ⇒ match u2 with [ uBNE    ⇒ true | _ ⇒ false ]
- | uBPL    ⇒ match u2 with [ uBPL    ⇒ true | _ ⇒ false ]
- | uBRA    ⇒ match u2 with [ uBRA    ⇒ true | _ ⇒ false ]
- | uBRCLRn ⇒ match u2 with [ uBRCLRn ⇒ true | _ ⇒ false ]
- | uBRN    ⇒ match u2 with [ uBRN    ⇒ true | _ ⇒ false ]
- | uBRSETn ⇒ match u2 with [ uBRSETn ⇒ true | _ ⇒ false ]
- | uBSETn  ⇒ match u2 with [ uBSETn  ⇒ true | _ ⇒ false ]
- | uBSR    ⇒ match u2 with [ uBSR    ⇒ true | _ ⇒ false ]
- | uCBEQA  ⇒ match u2 with [ uCBEQA  ⇒ true | _ ⇒ false ]
- | uCBEQX  ⇒ match u2 with [ uCBEQX  ⇒ true | _ ⇒ false ]
- | uCLC    ⇒ match u2 with [ uCLC    ⇒ true | _ ⇒ false ]
- | uCLI    ⇒ match u2 with [ uCLI    ⇒ true | _ ⇒ false ]
- | uCLR    ⇒ match u2 with [ uCLR    ⇒ true | _ ⇒ false ]
- | uCMP    ⇒ match u2 with [ uCMP    ⇒ true | _ ⇒ false ]
- | uCOM    ⇒ match u2 with [ uCOM    ⇒ true | _ ⇒ false ]
- | uCPHX   ⇒ match u2 with [ uCPHX   ⇒ true | _ ⇒ false ]
- | uCPX    ⇒ match u2 with [ uCPX    ⇒ true | _ ⇒ false ]
- | uDAA    ⇒ match u2 with [ uDAA    ⇒ true | _ ⇒ false ]
- | uDBNZ   ⇒ match u2 with [ uDBNZ   ⇒ true | _ ⇒ false ]
- | uDEC    ⇒ match u2 with [ uDEC    ⇒ true | _ ⇒ false ]
- | uDIV    ⇒ match u2 with [ uDIV    ⇒ true | _ ⇒ false ]
- | uEOR    ⇒ match u2 with [ uEOR    ⇒ true | _ ⇒ false ]
- | uINC    ⇒ match u2 with [ uINC    ⇒ true | _ ⇒ false ]
- | uJMP    ⇒ match u2 with [ uJMP    ⇒ true | _ ⇒ false ]
- | uJSR    ⇒ match u2 with [ uJSR    ⇒ true | _ ⇒ false ]
- | uLDA    ⇒ match u2 with [ uLDA    ⇒ true | _ ⇒ false ]
- | uLDHX   ⇒ match u2 with [ uLDHX   ⇒ true | _ ⇒ false ]
- | uLDX    ⇒ match u2 with [ uLDX    ⇒ true | _ ⇒ false ]
- | uLSR    ⇒ match u2 with [ uLSR    ⇒ true | _ ⇒ false ]
- | uMOV    ⇒ match u2 with [ uMOV    ⇒ true | _ ⇒ false ]
- | uMUL    ⇒ match u2 with [ uMUL    ⇒ true | _ ⇒ false ]
- | uNEG    ⇒ match u2 with [ uNEG    ⇒ true | _ ⇒ false ]
- | uNOP    ⇒ match u2 with [ uNOP    ⇒ true | _ ⇒ false ]
- | uNSA    ⇒ match u2 with [ uNSA    ⇒ true | _ ⇒ false ]
- | uORA    ⇒ match u2 with [ uORA    ⇒ true | _ ⇒ false ]
- | uPSHA   ⇒ match u2 with [ uPSHA   ⇒ true | _ ⇒ false ]
- | uPSHH   ⇒ match u2 with [ uPSHH   ⇒ true | _ ⇒ false ]
- | uPSHX   ⇒ match u2 with [ uPSHX   ⇒ true | _ ⇒ false ]
- | uPULA   ⇒ match u2 with [ uPULA   ⇒ true | _ ⇒ false ]
- | uPULH   ⇒ match u2 with [ uPULH   ⇒ true | _ ⇒ false ]
- | uPULX   ⇒ match u2 with [ uPULX   ⇒ true | _ ⇒ false ]
- | uROL    ⇒ match u2 with [ uROL    ⇒ true | _ ⇒ false ]
- | uROR    ⇒ match u2 with [ uROR    ⇒ true | _ ⇒ false ]
- | uRSP    ⇒ match u2 with [ uRSP    ⇒ true | _ ⇒ false ]
- | uRTI    ⇒ match u2 with [ uRTI    ⇒ true | _ ⇒ false ]
- | uRTS    ⇒ match u2 with [ uRTS    ⇒ true | _ ⇒ false ]
- | uSBC    ⇒ match u2 with [ uSBC    ⇒ true | _ ⇒ false ]
- | uSEC    ⇒ match u2 with [ uSEC    ⇒ true | _ ⇒ false ]
- | uSEI    ⇒ match u2 with [ uSEI    ⇒ true | _ ⇒ false ]
- | uSHA    ⇒ match u2 with [ uSHA    ⇒ true | _ ⇒ false ]
- | uSLA    ⇒ match u2 with [ uSLA    ⇒ true | _ ⇒ false ]
- | uSTA    ⇒ match u2 with [ uSTA    ⇒ true | _ ⇒ false ]
- | uSTHX   ⇒ match u2 with [ uSTHX   ⇒ true | _ ⇒ false ]
- | uSTOP   ⇒ match u2 with [ uSTOP   ⇒ true | _ ⇒ false ]
- | uSTX    ⇒ match u2 with [ uSTX    ⇒ true | _ ⇒ false ]
- | uSUB    ⇒ match u2 with [ uSUB    ⇒ true | _ ⇒ false ]
- | uSWI    ⇒ match u2 with [ uSWI    ⇒ true | _ ⇒ false ]
- | uTAP    ⇒ match u2 with [ uTAP    ⇒ true | _ ⇒ false ]
- | uTAX    ⇒ match u2 with [ uTAX    ⇒ true | _ ⇒ false ]
- | uTPA    ⇒ match u2 with [ uTPA    ⇒ true | _ ⇒ false ]
- | uTST    ⇒ match u2 with [ uTST    ⇒ true | _ ⇒ false ]
- | uTSX    ⇒ match u2 with [ uTSX    ⇒ true | _ ⇒ false ]
- | uTXA    ⇒ match u2 with [ uTXA    ⇒ true | _ ⇒ false ]
- | uTXS    ⇒ match u2 with [ uTXS    ⇒ true | _ ⇒ false ]
- | uWAIT   ⇒ match u2 with [ uWAIT   ⇒ true | _ ⇒ false ]
-
- ].
-
 (* costruttore di un sottouniverso:
    S_EL cioe' uno qualsiasi degli elementi del sottouniverso
-   S_KO cioe' il caso impossibile
 *)
-ninductive S_UN (l:list UN) : Type ≝
-  S_EL : Πx:UN.((member_list UN x eq_UN l) = true) → (∀y.eq_UN x y = true → x = y) → S_UN l
-| S_KO : False → S_UN l. 
+ninductive S_UN (l:ne_list nat) : Type ≝
+ S_EL : Πx:nat.((member_natList x l) = true) → S_UN l.
 
-ndefinition getelem : ∀l.∀e:S_UN l.UN.
+ndefinition getelem : ∀l.∀e:S_UN l.nat.
  #l; #s; nelim s;
- ##[ ##1: #u; #dim1; #dim2; napply u
- ##| ##2: #F; nelim F
- ##]
+ #u; #dim;
+ napply u.
 nqed.
 
-ndefinition eq_SUN ≝ λl.λx,y:S_UN l.eq_UN (getelem ? x) (getelem ? y).
-
-ndefinition getdim1 : ∀l.∀e:S_UN l.member_list UN (getelem ? e) eq_UN l = true.
- #l; #s; nelim s;
- ##[ ##2: #F; nelim F
- ##| ##1: #u; #dim1; #dim2; napply dim1
- ##]
-nqed.
+ndefinition eq_SUN ≝ λl.λx,y:S_UN l.eq_nat (getelem ? x) (getelem ? y).
 
-ndefinition getdim2 : ∀l.∀e:S_UN l.(∀y.eq_UN (getelem ? e) y = true → (getelem ? e) = y).
+ndefinition getdim : ∀l.∀e:S_UN l.member_natList (getelem ? e) l = true.
  #l; #s; nelim s;
- ##[ ##2: #F; nelim F
- ##| ##1: #u; #dim1; #dim2; napply dim2
- ##]
+ #u; #dim;
+ napply dim.
 nqed.
 
 nlemma SUN_destruct_1
- : ∀l.∀e1,e2.∀dim11,dim21.∀dim12,dim22.S_EL l e1 dim11 dim12 = S_EL l e2 dim21 dim22 → e1 = e2.
- #l; #e1; #e2; #dim11; #dim21; #dim12; #dim22; #H;
- nchange with (match S_EL l e2 dim21 dim22 with [ S_EL a _ _ ⇒ e1 = a | S_KO _ ⇒ False ]);
+ : ∀l.∀e1,e2.∀dim1,dim2.S_EL l e1 dim1 = S_EL l e2 dim2 → e1 = e2.
+ #l; #e1; #e2; #dim1; #dim2; #H;
+ nchange with (match S_EL l e2 dim2 with [ S_EL a _ ⇒ e1 = a ]);
  nrewrite < H;
  nnormalize;
  napply refl_eq.
 nqed.
 
-ndefinition UN_destruct : ∀x,y.∀P:Prop.x = y → match eq_UN x y with [ true ⇒ P → P  | false ⇒ P ].
- #x; #y; #P; #H;
- nrewrite > H;
- nelim y;
- nnormalize;
- napply (λx.x).
-nqed.
-
+(* destruct universale *)
 ndefinition SUN_destruct : ∀l.∀x,y:S_UN l.∀P:Prop.x = y → match eq_SUN l x y with [ true ⇒ P → P | false ⇒ P ].
  #l; #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
-          ##[ ##2: #F; nelim F
-          ##| ##1: #u2; #dim21; #dim22; #P;
-                   nchange with (? → (match eq_UN u1 u2 with [ true ⇒ P → P | false ⇒ P ]));
-                   #H; napply (UN_destruct u1 u2);
-                   napply (SUN_destruct_1 l … H)
-          ##]
- ##]
-nqed.
-
-nlemma eq_to_eqUN : ∀e1,e2.e1 = e2 → eq_UN e1 e2 = true.
- #e1; #e2; #H;
- nrewrite > H;
- nelim e2;
+ #u1; #dim1;
+ #y; nelim y;
+ #u2; #dim2;
+ #P;
+ nchange with (? → (match eq_nat u1 u2 with [ true ⇒ P → P | false ⇒ P ]));
+ #H;
+ nrewrite > (SUN_destruct_1 l … H);
+ nrewrite > (eq_to_eqnat u2 u2 (refl_eq …));
  nnormalize;
- napply refl_eq.
+ napply (λx.x).
 nqed.
 
+(* eq_to_eqxx universale *)
 nlemma eq_to_eqSUN : ∀l.∀x,y:S_UN l.x = y → eq_SUN l x y = true.
  #l; #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
-          ##[ ##2: #F; nelim F
-          ##| ##1: #u2; #dim21; #dim22;
-                   nchange with (? → eq_UN u1 u2 = true);
-                   #H; napply (eq_to_eqUN u1 u2);
-                   napply (SUN_destruct_1 l … H)
-          ##]
- ##]
+ #u1; #dim1;
+ #y; nelim y;
+ #u2; #dim2;
+ nchange with (? → eq_nat u1 u2 = true);
+ #H; napply (eq_to_eqnat u1 u2);
+ napply (SUN_destruct_1 l … H).
 nqed.
 
-nlemma neqUN_to_neq : ∀e1,e2.eq_UN e1 e2 = false → e1 ≠ e2.
- #e1; #e2; #H;
- napply (not_to_not (e1 = e2) (eq_UN e1 e2 = true) …);
- ##[ ##1: napply (eq_to_eqUN e1 e2)
+(* neqxx_to_neq universale *)
+nlemma neqSUN_to_neq : ∀l.∀x,y:S_UN l.eq_SUN l x y = false → x ≠ y.
+ #l; #n1; #n2; #H;
+ napply (not_to_not (n1 = n2) (eq_SUN l n1 n2 = true) …);
+ ##[ ##1: napply (eq_to_eqSUN l n1 n2)
  ##| ##2: napply (eqfalse_to_neqtrue … H)
  ##]
 nqed.
 
-nlemma neqSUN_to_neq : ∀l.∀x,y:S_UN l.eq_SUN l x y = false → x ≠ y.
- #l; #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
-          ##[ ##2: #F; nelim F
-          ##| ##1: #u2; #dim21; #dim22;
-                        nchange with ((eq_UN u1 u2 = false) → ?);
-                        #H; nnormalize; #H1;
-                        napply (neqUN_to_neq u1 u2 H);
-                        napply (SUN_destruct_1 l … H1)
-          ##]
- ##]
+(* perche' non si riesce a dimstrare ??? *
+nlemma SUN_construct
+ : ∀l.∀u.
+   ∀dim1,dim2:(member_natList u l = true).
+   ((S_EL l u dim1) = (S_EL l u dim2)).
+ #l; #u; #dim1; #dim2;
+ nchange with (S_EL l u dim1 = S_EL l u dim1);
+ napply refl_eq.
 nqed.
-
+*)
 naxiom SUN_construct
  : ∀l.∀u.
-   ∀dim11,dim21:(member_list UN u eq_UN l = true).
-   ∀dim12,dim22:(∀y0.(eq_UN u y0 = true) → (u = y0)).
-   ((S_EL l u dim11 dim12) = (S_EL l u dim21 dim22)).
+   ∀dim1,dim2:(member_natList u l = true).
+   ((S_EL l u dim1) = (S_EL l u dim2)).
 
 nlemma eqgetelem_to_eq : ∀l.∀x,y:S_UN l.(getelem ? x) = (getelem ? y) → x = y.
  #l; #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
-          ##[ ##2: #F; nelim F
-          ##| ##1: #u2; #dim21; #dim22;
-                   nchange with (u1 = u2 → ?); #H;
-                   nrewrite > H in dim11:(%) dim12:(%) ⊢ %; #dim11; #dim12;
-                   napply (SUN_construct l u2 dim11 dim21 dim12 dim22);
-          ##]
- ##]
-nqed.
-
-nlemma neq_to_neqgetelem : ∀l.∀x,y:S_UN l.x ≠ y → (getelem ? x) ≠ (getelem ? y).
- #l; #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
-          ##[ ##2: #F; nelim F
-          ##| ##1: #u2; #dim21; #dim22; #H;
-                   napply (not_to_not ((getelem l ?) = (getelem l ?))
-                                      ((S_EL l u1 dim11 dim12) = (S_EL l u2 dim21 dim22)) ?);
-                   ##[ ##1: napply H
-                   ##| ##2: napply (eqgetelem_to_eq l …)
-                   ##]
-          ##]
- ##]
+ #u1; #dim1;
+ #y; nelim y;
+ #u2; #dim2;
+ nchange with (u1 = u2 → ?);
+ #H;
+ nrewrite > H in dim1:(%) ⊢ %;
+ #dim1;
+ napply (SUN_construct l u2 dim1 dim2).
 nqed.
 
+(* eqxx_to_eq universale *)
 nlemma eqSUN_to_eq : ∀l.∀x,y:S_UN l.eq_SUN l x y = true → x = y.
  #l; #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
-          ##[ ##2: #F; nelim F
-          ##| ##1: #u2; #dim21; #dim22;
-                   nchange with ((eq_UN u1 u2 = true) → ?); #H;
-                   nrewrite > (eqgetelem_to_eq l (S_EL l u1 dim11 dim12) (S_EL l u2 dim21 dim22) (dim12 u2 H));
-                   napply refl_eq
-          ##]
- ##]
+ #u1; #dim1;
+ #y; nelim y;
+ #u2; #dim2;
+ nchange with ((eq_nat u1 u2 = true) → ?);
+ #H;
+ nrewrite > (eqgetelem_to_eq l (S_EL l u1 dim1) (S_EL l u2 dim2) (eqnat_to_eq u1 u2 H));
+ napply refl_eq.
 nqed.
 
+(* neq_to_neqxx universale *)
 nlemma neq_to_neqSUN : ∀l.∀x,y:S_UN l.x ≠ y → eq_SUN l x y = false.
- #l; #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
-          ##[ ##2: #F; nelim F
-          ##| ##1: #u2; #dim21; #dim22; #H;
-                   napply neqtrue_to_eqfalse;
-                   napply (not_to_not ?? (eqSUN_to_eq l ??) ?) ;
-                   napply H
-          ##]
- ##]
+ #l; #n1; #n2; #H;
+ napply (neqtrue_to_eqfalse (eq_SUN l n1 n2));
+ napply (not_to_not (eq_SUN l n1 n2 = true) (n1 = n2) ? H);
+ napply (eqSUN_to_eq l n1 n2).
 nqed.
 
+(* decidibilita' universale *)
 nlemma decidable_SUN : ∀l.∀x,y:S_UN l.decidable (x = y).
- #l; #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
-          ##[ ##2: #F; nelim F
-          ##| ##1: #u2; #dim21; #dim22; nnormalize;
-                   napply (or2_elim … (decidable_bexpr (eq_SUN l (S_EL l u1 dim11 dim12) (S_EL l u2 dim21 dim22))));
- ##[ ##1: #H; napply (or2_intro1 (? = ?) (? ≠ ?) (eqSUN_to_eq l … H))
- ##| ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) (neqSUN_to_neq l … H))
+ #l; #x; #y; nnormalize;
+ napply (or2_elim (eq_SUN l x y = true) (eq_SUN l x y = false) ? (decidable_bexpr ?));
+ ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqSUN_to_eq l … H))
+ ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqSUN_to_neq l … H))
  ##]
 nqed.
 
+(* simmetria di uguaglianza universale *)
 nlemma symmetric_eqSUN : ∀l.symmetricT (S_UN l) bool (eq_SUN l).
- #l; #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
-          ##[ ##2: #F; nelim F
-          ##| ##1: #u2; #dim21; #dim22;
-                   napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_SUN l (S_EL l u1 dim11 dim12) (S_EL l u2 dim21 dim22)));
+ #l; #n1; #n2;
+ napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_SUN l n1 n2));
  ##[ ##1: #H; nrewrite > H; napply refl_eq
- ##| ##2: #H; nrewrite > (neq_to_neqSUN l … H);
-          napply (symmetric_eq ? (eq_SUN l ??) false);
-          napply (neq_to_neqSUN l … (symmetric_neq … H))
+ ##| ##2: #H; nrewrite > (neq_to_neqSUN l n1 n2 H);
+          napply (symmetric_eq ? (eq_SUN l n2 n1) false);
+          napply (neq_to_neqSUN l n2 n1 (symmetric_neq ? n1 n2 H))
  ##]
 nqed.
+
+(* scheletro di funzione generica ad 1 argomento *)
+nlet rec farg1_auxT (T:Type) (l:ne_list nat) on l ≝
+ match l with
+  [ ne_nil _ ⇒ T
+  | ne_cons _ t ⇒ ProdT T (farg1_auxT T t)
+  ].
+
+nlemma farg1_auxDim : ∀h,t,x.eq_nat x h = false → member_natList x (h§§t) = true → member_natList x t = true.
+ #h; #t; #x; #H; #H1;
+ nnormalize in H1:(%);
+ nrewrite > H in H1:(%);
+ nnormalize;
+ napply (λx.x).
+nqed.
+
+nlet rec farg1 (T:Type) (l:ne_list nat) on l ≝
+ match l with
+  [ ne_nil h ⇒ λarg:farg1_auxT T «£h».λx:S_UN «£h».arg
+  | ne_cons h t ⇒ λarg:farg1_auxT T (h§§t).λx:S_UN (h§§t).
+   match eq_nat (getelem ? x) h
+    return λy.eq_nat (getelem ? x) h = y → ?
+   with
+    [ true ⇒ λp:(eq_nat (getelem ? x) h = true).fst … arg
+    | false ⇒ λp:(eq_nat (getelem ? x) h = false).
+     farg1 T t
+      (snd … arg)
+      (S_EL t (getelem ? x) (farg1_auxDim h t (getelem ? x) p (getdim ? x)))
+    ] (refl_eq ? (eq_nat (getelem ? x) h))
+  ].
+
+(* scheletro di funzione generica a 2 argomenti *)
+nlet rec farg2 (T:Type) (l,lfix:ne_list nat) on l ≝
+ match l with
+  [ ne_nil h ⇒ λarg:farg1_auxT (farg1_auxT T lfix) «£h».λx:S_UN «£h».farg1 T lfix arg
+  | ne_cons h t ⇒ λarg:farg1_auxT (farg1_auxT T lfix) (h§§t).λx:S_UN (h§§t).
+   match eq_nat (getelem ? x) h
+    return λy.eq_nat (getelem ? x) h = y → ?
+   with
+    [ true ⇒ λp:(eq_nat (getelem ? x) h = true).farg1 T lfix (fst … arg)
+    | false ⇒ λp:(eq_nat (getelem ? x) h = false).
+     farg2 T t lfix
+      (snd … arg)
+      (S_EL t (getelem ? x) (farg1_auxDim h t (getelem ? x) p (getdim ? x)))
+    ] (refl_eq ? (eq_nat (getelem ? x) h))
+  ].
+
+(* esempio0: universo ottale *)
+ndefinition oct0 ≝ O.
+ndefinition oct1 ≝ S O.
+ndefinition oct2 ≝ S (S O).
+ndefinition oct3 ≝ S (S (S O)).
+ndefinition oct4 ≝ S (S (S (S O))).
+ndefinition oct5 ≝ S (S (S (S (S O)))).
+ndefinition oct6 ≝ S (S (S (S (S (S O))))).
+ndefinition oct7 ≝ S (S (S (S (S (S (S O)))))).
+
+ndefinition oct_UN ≝ « oct0 ; oct1 ; oct2 ; oct3 ; oct4 ; oct5 ; oct6 £ oct7 ».
+
+ndefinition uoct0 ≝ S_EL oct_UN oct0 (refl_eq …).
+ndefinition uoct1 ≝ S_EL oct_UN oct1 (refl_eq …).
+ndefinition uoct2 ≝ S_EL oct_UN oct2 (refl_eq …).
+ndefinition uoct3 ≝ S_EL oct_UN oct3 (refl_eq …).
+ndefinition uoct4 ≝ S_EL oct_UN oct4 (refl_eq …).
+ndefinition uoct5 ≝ S_EL oct_UN oct5 (refl_eq …).
+ndefinition uoct6 ≝ S_EL oct_UN oct6 (refl_eq …).
+ndefinition uoct7 ≝ S_EL oct_UN oct7 (refl_eq …).
+
+(* esempio1: NOT ottale *)
+ndefinition octNOT ≝
+ farg1 (S_UN oct_UN) oct_UN
+  (pair … uoct7 (pair … uoct6 (pair … uoct5 (pair … uoct4 (pair … uoct3 (pair … uoct2 (pair … uoct1 uoct0))))))). 
+
+(* esempio2: AND ottale *)
+ndefinition octAND0 ≝ pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct0 uoct0)))))).
+ndefinition octAND1 ≝ pair … uoct0 (pair … uoct1 (pair … uoct0 (pair … uoct1 (pair … uoct0 (pair … uoct1 (pair … uoct0 uoct1)))))).
+ndefinition octAND2 ≝ pair … uoct0 (pair … uoct0 (pair … uoct2 (pair … uoct2 (pair … uoct0 (pair … uoct0 (pair … uoct2 uoct2)))))).
+ndefinition octAND3 ≝ pair … uoct0 (pair … uoct1 (pair … uoct2 (pair … uoct3 (pair … uoct0 (pair … uoct1 (pair … uoct2 uoct3)))))).
+ndefinition octAND4 ≝ pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct4 (pair … uoct4 (pair … uoct4 uoct4)))))).
+ndefinition octAND5 ≝ pair … uoct0 (pair … uoct1 (pair … uoct0 (pair … uoct1 (pair … uoct4 (pair … uoct5 (pair … uoct4 uoct5)))))).
+ndefinition octAND6 ≝ pair … uoct0 (pair … uoct0 (pair … uoct2 (pair … uoct2 (pair … uoct4 (pair … uoct4 (pair … uoct6 uoct6)))))).
+ndefinition octAND7 ≝ pair … uoct0 (pair … uoct1 (pair … uoct2 (pair … uoct3 (pair … uoct4 (pair … uoct5 (pair … uoct6 uoct7)))))).
+
+ndefinition octAND ≝
+ farg2 (S_UN oct_UN) oct_UN oct_UN
+  (pair … octAND0 (pair … octAND1 (pair … octAND2 (pair … octAND3 (pair … octAND4 (pair … octAND5 (pair … octAND6 octAND7))))))).
+
+(* ora e' possibile fare
+   octNOT uoctX
+   octAND uoctX uoctY
+*)