(* data ultima modifica 15/11/2007 *)
(* ********************************************************************** *)
-set "baseuri" "cic:/matita/freescale/exadecim/".
-
-(*include "/media/VIRTUOSO/freescale/extra.ma".*)
include "freescale/extra.ma".
(* ***************************** *)
definition rcr_ex ≝
λe:exadecim.λc:bool.match c with
[ true ⇒ match e with
- [ x0 ⇒ pairT exadecim bool x8 false | x1 ⇒ pairT exadecim bool x8 true
- | x2 ⇒ pairT exadecim bool x9 false | x3 ⇒ pairT exadecim bool x9 true
- | x4 ⇒ pairT exadecim bool xA false | x5 ⇒ pairT exadecim bool xA true
- | x6 ⇒ pairT exadecim bool xB false | x7 ⇒ pairT exadecim bool xB true
- | x8 ⇒ pairT exadecim bool xC false | x9 ⇒ pairT exadecim bool xC true
- | xA ⇒ pairT exadecim bool xD false | xB ⇒ pairT exadecim bool xD true
- | xC ⇒ pairT exadecim bool xE false | xD ⇒ pairT exadecim bool xE true
- | xE ⇒ pairT exadecim bool xF false | xF ⇒ pairT exadecim bool xF true ]
+ [ x0 ⇒ pair exadecim bool x8 false | x1 ⇒ pair exadecim bool x8 true
+ | x2 ⇒ pair exadecim bool x9 false | x3 ⇒ pair exadecim bool x9 true
+ | x4 ⇒ pair exadecim bool xA false | x5 ⇒ pair exadecim bool xA true
+ | x6 ⇒ pair exadecim bool xB false | x7 ⇒ pair exadecim bool xB true
+ | x8 ⇒ pair exadecim bool xC false | x9 ⇒ pair exadecim bool xC true
+ | xA ⇒ pair exadecim bool xD false | xB ⇒ pair exadecim bool xD true
+ | xC ⇒ pair exadecim bool xE false | xD ⇒ pair exadecim bool xE true
+ | xE ⇒ pair exadecim bool xF false | xF ⇒ pair exadecim bool xF true ]
| false ⇒ match e with
- [ x0 ⇒ pairT exadecim bool x0 false | x1 ⇒ pairT exadecim bool x0 true
- | x2 ⇒ pairT exadecim bool x1 false | x3 ⇒ pairT exadecim bool x1 true
- | x4 ⇒ pairT exadecim bool x2 false | x5 ⇒ pairT exadecim bool x2 true
- | x6 ⇒ pairT exadecim bool x3 false | x7 ⇒ pairT exadecim bool x3 true
- | x8 ⇒ pairT exadecim bool x4 false | x9 ⇒ pairT exadecim bool x4 true
- | xA ⇒ pairT exadecim bool x5 false | xB ⇒ pairT exadecim bool x5 true
- | xC ⇒ pairT exadecim bool x6 false | xD ⇒ pairT exadecim bool x6 true
- | xE ⇒ pairT exadecim bool x7 false | xF ⇒ pairT exadecim bool x7 true ]
+ [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x0 true
+ | x2 ⇒ pair exadecim bool x1 false | x3 ⇒ pair exadecim bool x1 true
+ | x4 ⇒ pair exadecim bool x2 false | x5 ⇒ pair exadecim bool x2 true
+ | x6 ⇒ pair exadecim bool x3 false | x7 ⇒ pair exadecim bool x3 true
+ | x8 ⇒ pair exadecim bool x4 false | x9 ⇒ pair exadecim bool x4 true
+ | xA ⇒ pair exadecim bool x5 false | xB ⇒ pair exadecim bool x5 true
+ | xC ⇒ pair exadecim bool x6 false | xD ⇒ pair exadecim bool x6 true
+ | xE ⇒ pair exadecim bool x7 false | xF ⇒ pair exadecim bool x7 true ]
].
(* operatore shift destro *)
definition shr_ex ≝
λe:exadecim.match e with
- [ x0 ⇒ pairT exadecim bool x0 false | x1 ⇒ pairT exadecim bool x0 true
- | x2 ⇒ pairT exadecim bool x1 false | x3 ⇒ pairT exadecim bool x1 true
- | x4 ⇒ pairT exadecim bool x2 false | x5 ⇒ pairT exadecim bool x2 true
- | x6 ⇒ pairT exadecim bool x3 false | x7 ⇒ pairT exadecim bool x3 true
- | x8 ⇒ pairT exadecim bool x4 false | x9 ⇒ pairT exadecim bool x4 true
- | xA ⇒ pairT exadecim bool x5 false | xB ⇒ pairT exadecim bool x5 true
- | xC ⇒ pairT exadecim bool x6 false | xD ⇒ pairT exadecim bool x6 true
- | xE ⇒ pairT exadecim bool x7 false | xF ⇒ pairT exadecim bool x7 true ].
+ [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x0 true
+ | x2 ⇒ pair exadecim bool x1 false | x3 ⇒ pair exadecim bool x1 true
+ | x4 ⇒ pair exadecim bool x2 false | x5 ⇒ pair exadecim bool x2 true
+ | x6 ⇒ pair exadecim bool x3 false | x7 ⇒ pair exadecim bool x3 true
+ | x8 ⇒ pair exadecim bool x4 false | x9 ⇒ pair exadecim bool x4 true
+ | xA ⇒ pair exadecim bool x5 false | xB ⇒ pair exadecim bool x5 true
+ | xC ⇒ pair exadecim bool x6 false | xD ⇒ pair exadecim bool x6 true
+ | xE ⇒ pair exadecim bool x7 false | xF ⇒ pair exadecim bool x7 true ].
(* operatore rotazione destra *)
definition ror_ex ≝
definition rcl_ex ≝
λe:exadecim.λc:bool.match c with
[ true ⇒ match e with
- [ x0 ⇒ pairT exadecim bool x1 false | x1 ⇒ pairT exadecim bool x3 false
- | x2 ⇒ pairT exadecim bool x5 false | x3 ⇒ pairT exadecim bool x7 false
- | x4 ⇒ pairT exadecim bool x9 false | x5 ⇒ pairT exadecim bool xB false
- | x6 ⇒ pairT exadecim bool xD false | x7 ⇒ pairT exadecim bool xF false
- | x8 ⇒ pairT exadecim bool x1 true | x9 ⇒ pairT exadecim bool x3 true
- | xA ⇒ pairT exadecim bool x5 true | xB ⇒ pairT exadecim bool x7 true
- | xC ⇒ pairT exadecim bool x9 true | xD ⇒ pairT exadecim bool xB true
- | xE ⇒ pairT exadecim bool xD true | xF ⇒ pairT exadecim bool xF true ]
+ [ x0 ⇒ pair exadecim bool x1 false | x1 ⇒ pair exadecim bool x3 false
+ | x2 ⇒ pair exadecim bool x5 false | x3 ⇒ pair exadecim bool x7 false
+ | x4 ⇒ pair exadecim bool x9 false | x5 ⇒ pair exadecim bool xB false
+ | x6 ⇒ pair exadecim bool xD false | x7 ⇒ pair exadecim bool xF false
+ | x8 ⇒ pair exadecim bool x1 true | x9 ⇒ pair exadecim bool x3 true
+ | xA ⇒ pair exadecim bool x5 true | xB ⇒ pair exadecim bool x7 true
+ | xC ⇒ pair exadecim bool x9 true | xD ⇒ pair exadecim bool xB true
+ | xE ⇒ pair exadecim bool xD true | xF ⇒ pair exadecim bool xF true ]
| false ⇒ match e with
- [ x0 ⇒ pairT exadecim bool x0 false | x1 ⇒ pairT exadecim bool x2 false
- | x2 ⇒ pairT exadecim bool x4 false | x3 ⇒ pairT exadecim bool x6 false
- | x4 ⇒ pairT exadecim bool x8 false | x5 ⇒ pairT exadecim bool xA false
- | x6 ⇒ pairT exadecim bool xC false | x7 ⇒ pairT exadecim bool xE false
- | x8 ⇒ pairT exadecim bool x0 true | x9 ⇒ pairT exadecim bool x2 true
- | xA ⇒ pairT exadecim bool x4 true | xB ⇒ pairT exadecim bool x6 true
- | xC ⇒ pairT exadecim bool x8 true | xD ⇒ pairT exadecim bool xA true
- | xE ⇒ pairT exadecim bool xC true | xF ⇒ pairT exadecim bool xE true ]
+ [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x2 false
+ | x2 ⇒ pair exadecim bool x4 false | x3 ⇒ pair exadecim bool x6 false
+ | x4 ⇒ pair exadecim bool x8 false | x5 ⇒ pair exadecim bool xA false
+ | x6 ⇒ pair exadecim bool xC false | x7 ⇒ pair exadecim bool xE false
+ | x8 ⇒ pair exadecim bool x0 true | x9 ⇒ pair exadecim bool x2 true
+ | xA ⇒ pair exadecim bool x4 true | xB ⇒ pair exadecim bool x6 true
+ | xC ⇒ pair exadecim bool x8 true | xD ⇒ pair exadecim bool xA true
+ | xE ⇒ pair exadecim bool xC true | xF ⇒ pair exadecim bool xE true ]
].
(* operatore shift sinistro *)
definition shl_ex ≝
λe:exadecim.match e with
- [ x0 ⇒ pairT exadecim bool x0 false | x1 ⇒ pairT exadecim bool x2 false
- | x2 ⇒ pairT exadecim bool x4 false | x3 ⇒ pairT exadecim bool x6 false
- | x4 ⇒ pairT exadecim bool x8 false | x5 ⇒ pairT exadecim bool xA false
- | x6 ⇒ pairT exadecim bool xC false | x7 ⇒ pairT exadecim bool xE false
- | x8 ⇒ pairT exadecim bool x0 true | x9 ⇒ pairT exadecim bool x2 true
- | xA ⇒ pairT exadecim bool x4 true | xB ⇒ pairT exadecim bool x6 true
- | xC ⇒ pairT exadecim bool x8 true | xD ⇒ pairT exadecim bool xA true
- | xE ⇒ pairT exadecim bool xC true | xF ⇒ pairT exadecim bool xE true ].
+ [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x2 false
+ | x2 ⇒ pair exadecim bool x4 false | x3 ⇒ pair exadecim bool x6 false
+ | x4 ⇒ pair exadecim bool x8 false | x5 ⇒ pair exadecim bool xA false
+ | x6 ⇒ pair exadecim bool xC false | x7 ⇒ pair exadecim bool xE false
+ | x8 ⇒ pair exadecim bool x0 true | x9 ⇒ pair exadecim bool x2 true
+ | xA ⇒ pair exadecim bool x4 true | xB ⇒ pair exadecim bool x6 true
+ | xC ⇒ pair exadecim bool x8 true | xD ⇒ pair exadecim bool xA true
+ | xE ⇒ pair exadecim bool xC true | xF ⇒ pair exadecim bool xE true ].
(* operatore rotazione sinistra *)
definition rol_ex ≝
match e1 with
[ x0 ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool x1 false
- | x1 ⇒ pairT exadecim bool x2 false
- | x2 ⇒ pairT exadecim bool x3 false
- | x3 ⇒ pairT exadecim bool x4 false
- | x4 ⇒ pairT exadecim bool x5 false
- | x5 ⇒ pairT exadecim bool x6 false
- | x6 ⇒ pairT exadecim bool x7 false
- | x7 ⇒ pairT exadecim bool x8 false
- | x8 ⇒ pairT exadecim bool x9 false
- | x9 ⇒ pairT exadecim bool xA false
- | xA ⇒ pairT exadecim bool xB false
- | xB ⇒ pairT exadecim bool xC false
- | xC ⇒ pairT exadecim bool xD false
- | xD ⇒ pairT exadecim bool xE false
- | xE ⇒ pairT exadecim bool xF false
- | xF ⇒ pairT exadecim bool x0 true ]
+ [ x0 ⇒ pair exadecim bool x1 false
+ | x1 ⇒ pair exadecim bool x2 false
+ | x2 ⇒ pair exadecim bool x3 false
+ | x3 ⇒ pair exadecim bool x4 false
+ | x4 ⇒ pair exadecim bool x5 false
+ | x5 ⇒ pair exadecim bool x6 false
+ | x6 ⇒ pair exadecim bool x7 false
+ | x7 ⇒ pair exadecim bool x8 false
+ | x8 ⇒ pair exadecim bool x9 false
+ | x9 ⇒ pair exadecim bool xA false
+ | xA ⇒ pair exadecim bool xB false
+ | xB ⇒ pair exadecim bool xC false
+ | xC ⇒ pair exadecim bool xD false
+ | xD ⇒ pair exadecim bool xE false
+ | xE ⇒ pair exadecim bool xF false
+ | xF ⇒ pair exadecim bool x0 true ]
| x1 ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool x2 false
- | x1 ⇒ pairT exadecim bool x3 false
- | x2 ⇒ pairT exadecim bool x4 false
- | x3 ⇒ pairT exadecim bool x5 false
- | x4 ⇒ pairT exadecim bool x6 false
- | x5 ⇒ pairT exadecim bool x7 false
- | x6 ⇒ pairT exadecim bool x8 false
- | x7 ⇒ pairT exadecim bool x9 false
- | x8 ⇒ pairT exadecim bool xA false
- | x9 ⇒ pairT exadecim bool xB false
- | xA ⇒ pairT exadecim bool xC false
- | xB ⇒ pairT exadecim bool xD false
- | xC ⇒ pairT exadecim bool xE false
- | xD ⇒ pairT exadecim bool xF false
- | xE ⇒ pairT exadecim bool x0 true
- | xF ⇒ pairT exadecim bool x1 true ]
+ [ x0 ⇒ pair exadecim bool x2 false
+ | x1 ⇒ pair exadecim bool x3 false
+ | x2 ⇒ pair exadecim bool x4 false
+ | x3 ⇒ pair exadecim bool x5 false
+ | x4 ⇒ pair exadecim bool x6 false
+ | x5 ⇒ pair exadecim bool x7 false
+ | x6 ⇒ pair exadecim bool x8 false
+ | x7 ⇒ pair exadecim bool x9 false
+ | x8 ⇒ pair exadecim bool xA false
+ | x9 ⇒ pair exadecim bool xB false
+ | xA ⇒ pair exadecim bool xC false
+ | xB ⇒ pair exadecim bool xD false
+ | xC ⇒ pair exadecim bool xE false
+ | xD ⇒ pair exadecim bool xF false
+ | xE ⇒ pair exadecim bool x0 true
+ | xF ⇒ pair exadecim bool x1 true ]
| x2 ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool x3 false
- | x1 ⇒ pairT exadecim bool x4 false
- | x2 ⇒ pairT exadecim bool x5 false
- | x3 ⇒ pairT exadecim bool x6 false
- | x4 ⇒ pairT exadecim bool x7 false
- | x5 ⇒ pairT exadecim bool x8 false
- | x6 ⇒ pairT exadecim bool x9 false
- | x7 ⇒ pairT exadecim bool xA false
- | x8 ⇒ pairT exadecim bool xB false
- | x9 ⇒ pairT exadecim bool xC false
- | xA ⇒ pairT exadecim bool xD false
- | xB ⇒ pairT exadecim bool xE false
- | xC ⇒ pairT exadecim bool xF false
- | xD ⇒ pairT exadecim bool x0 true
- | xE ⇒ pairT exadecim bool x1 true
- | xF ⇒ pairT exadecim bool x2 true ]
+ [ x0 ⇒ pair exadecim bool x3 false
+ | x1 ⇒ pair exadecim bool x4 false
+ | x2 ⇒ pair exadecim bool x5 false
+ | x3 ⇒ pair exadecim bool x6 false
+ | x4 ⇒ pair exadecim bool x7 false
+ | x5 ⇒ pair exadecim bool x8 false
+ | x6 ⇒ pair exadecim bool x9 false
+ | x7 ⇒ pair exadecim bool xA false
+ | x8 ⇒ pair exadecim bool xB false
+ | x9 ⇒ pair exadecim bool xC false
+ | xA ⇒ pair exadecim bool xD false
+ | xB ⇒ pair exadecim bool xE false
+ | xC ⇒ pair exadecim bool xF false
+ | xD ⇒ pair exadecim bool x0 true
+ | xE ⇒ pair exadecim bool x1 true
+ | xF ⇒ pair exadecim bool x2 true ]
| x3 ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool x4 false
- | x1 ⇒ pairT exadecim bool x5 false
- | x2 ⇒ pairT exadecim bool x6 false
- | x3 ⇒ pairT exadecim bool x7 false
- | x4 ⇒ pairT exadecim bool x8 false
- | x5 ⇒ pairT exadecim bool x9 false
- | x6 ⇒ pairT exadecim bool xA false
- | x7 ⇒ pairT exadecim bool xB false
- | x8 ⇒ pairT exadecim bool xC false
- | x9 ⇒ pairT exadecim bool xD false
- | xA ⇒ pairT exadecim bool xE false
- | xB ⇒ pairT exadecim bool xF false
- | xC ⇒ pairT exadecim bool x0 true
- | xD ⇒ pairT exadecim bool x1 true
- | xE ⇒ pairT exadecim bool x2 true
- | xF ⇒ pairT exadecim bool x3 true ]
+ [ x0 ⇒ pair exadecim bool x4 false
+ | x1 ⇒ pair exadecim bool x5 false
+ | x2 ⇒ pair exadecim bool x6 false
+ | x3 ⇒ pair exadecim bool x7 false
+ | x4 ⇒ pair exadecim bool x8 false
+ | x5 ⇒ pair exadecim bool x9 false
+ | x6 ⇒ pair exadecim bool xA false
+ | x7 ⇒ pair exadecim bool xB false
+ | x8 ⇒ pair exadecim bool xC false
+ | x9 ⇒ pair exadecim bool xD false
+ | xA ⇒ pair exadecim bool xE false
+ | xB ⇒ pair exadecim bool xF false
+ | xC ⇒ pair exadecim bool x0 true
+ | xD ⇒ pair exadecim bool x1 true
+ | xE ⇒ pair exadecim bool x2 true
+ | xF ⇒ pair exadecim bool x3 true ]
| x4 ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool x5 false
- | x1 ⇒ pairT exadecim bool x6 false
- | x2 ⇒ pairT exadecim bool x7 false
- | x3 ⇒ pairT exadecim bool x8 false
- | x4 ⇒ pairT exadecim bool x9 false
- | x5 ⇒ pairT exadecim bool xA false
- | x6 ⇒ pairT exadecim bool xB false
- | x7 ⇒ pairT exadecim bool xC false
- | x8 ⇒ pairT exadecim bool xD false
- | x9 ⇒ pairT exadecim bool xE false
- | xA ⇒ pairT exadecim bool xF false
- | xB ⇒ pairT exadecim bool x0 true
- | xC ⇒ pairT exadecim bool x1 true
- | xD ⇒ pairT exadecim bool x2 true
- | xE ⇒ pairT exadecim bool x3 true
- | xF ⇒ pairT exadecim bool x4 true ]
+ [ x0 ⇒ pair exadecim bool x5 false
+ | x1 ⇒ pair exadecim bool x6 false
+ | x2 ⇒ pair exadecim bool x7 false
+ | x3 ⇒ pair exadecim bool x8 false
+ | x4 ⇒ pair exadecim bool x9 false
+ | x5 ⇒ pair exadecim bool xA false
+ | x6 ⇒ pair exadecim bool xB false
+ | x7 ⇒ pair exadecim bool xC false
+ | x8 ⇒ pair exadecim bool xD false
+ | x9 ⇒ pair exadecim bool xE false
+ | xA ⇒ pair exadecim bool xF false
+ | xB ⇒ pair exadecim bool x0 true
+ | xC ⇒ pair exadecim bool x1 true
+ | xD ⇒ pair exadecim bool x2 true
+ | xE ⇒ pair exadecim bool x3 true
+ | xF ⇒ pair exadecim bool x4 true ]
| x5 ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool x6 false
- | x1 ⇒ pairT exadecim bool x7 false
- | x2 ⇒ pairT exadecim bool x8 false
- | x3 ⇒ pairT exadecim bool x9 false
- | x4 ⇒ pairT exadecim bool xA false
- | x5 ⇒ pairT exadecim bool xB false
- | x6 ⇒ pairT exadecim bool xC false
- | x7 ⇒ pairT exadecim bool xD false
- | x8 ⇒ pairT exadecim bool xE false
- | x9 ⇒ pairT exadecim bool xF false
- | xA ⇒ pairT exadecim bool x0 true
- | xB ⇒ pairT exadecim bool x1 true
- | xC ⇒ pairT exadecim bool x2 true
- | xD ⇒ pairT exadecim bool x3 true
- | xE ⇒ pairT exadecim bool x4 true
- | xF ⇒ pairT exadecim bool x5 true ]
+ [ x0 ⇒ pair exadecim bool x6 false
+ | x1 ⇒ pair exadecim bool x7 false
+ | x2 ⇒ pair exadecim bool x8 false
+ | x3 ⇒ pair exadecim bool x9 false
+ | x4 ⇒ pair exadecim bool xA false
+ | x5 ⇒ pair exadecim bool xB false
+ | x6 ⇒ pair exadecim bool xC false
+ | x7 ⇒ pair exadecim bool xD false
+ | x8 ⇒ pair exadecim bool xE false
+ | x9 ⇒ pair exadecim bool xF false
+ | xA ⇒ pair exadecim bool x0 true
+ | xB ⇒ pair exadecim bool x1 true
+ | xC ⇒ pair exadecim bool x2 true
+ | xD ⇒ pair exadecim bool x3 true
+ | xE ⇒ pair exadecim bool x4 true
+ | xF ⇒ pair exadecim bool x5 true ]
| x6 ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool x7 false
- | x1 ⇒ pairT exadecim bool x8 false
- | x2 ⇒ pairT exadecim bool x9 false
- | x3 ⇒ pairT exadecim bool xA false
- | x4 ⇒ pairT exadecim bool xB false
- | x5 ⇒ pairT exadecim bool xC false
- | x6 ⇒ pairT exadecim bool xD false
- | x7 ⇒ pairT exadecim bool xE false
- | x8 ⇒ pairT exadecim bool xF false
- | x9 ⇒ pairT exadecim bool x0 true
- | xA ⇒ pairT exadecim bool x1 true
- | xB ⇒ pairT exadecim bool x2 true
- | xC ⇒ pairT exadecim bool x3 true
- | xD ⇒ pairT exadecim bool x4 true
- | xE ⇒ pairT exadecim bool x5 true
- | xF ⇒ pairT exadecim bool x6 true ]
+ [ x0 ⇒ pair exadecim bool x7 false
+ | x1 ⇒ pair exadecim bool x8 false
+ | x2 ⇒ pair exadecim bool x9 false
+ | x3 ⇒ pair exadecim bool xA false
+ | x4 ⇒ pair exadecim bool xB false
+ | x5 ⇒ pair exadecim bool xC false
+ | x6 ⇒ pair exadecim bool xD false
+ | x7 ⇒ pair exadecim bool xE false
+ | x8 ⇒ pair exadecim bool xF false
+ | x9 ⇒ pair exadecim bool x0 true
+ | xA ⇒ pair exadecim bool x1 true
+ | xB ⇒ pair exadecim bool x2 true
+ | xC ⇒ pair exadecim bool x3 true
+ | xD ⇒ pair exadecim bool x4 true
+ | xE ⇒ pair exadecim bool x5 true
+ | xF ⇒ pair exadecim bool x6 true ]
| x7 ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool x8 false
- | x1 ⇒ pairT exadecim bool x9 false
- | x2 ⇒ pairT exadecim bool xA false
- | x3 ⇒ pairT exadecim bool xB false
- | x4 ⇒ pairT exadecim bool xC false
- | x5 ⇒ pairT exadecim bool xD false
- | x6 ⇒ pairT exadecim bool xE false
- | x7 ⇒ pairT exadecim bool xF false
- | x8 ⇒ pairT exadecim bool x0 true
- | x9 ⇒ pairT exadecim bool x1 true
- | xA ⇒ pairT exadecim bool x2 true
- | xB ⇒ pairT exadecim bool x3 true
- | xC ⇒ pairT exadecim bool x4 true
- | xD ⇒ pairT exadecim bool x5 true
- | xE ⇒ pairT exadecim bool x6 true
- | xF ⇒ pairT exadecim bool x7 true ]
+ [ x0 ⇒ pair exadecim bool x8 false
+ | x1 ⇒ pair exadecim bool x9 false
+ | x2 ⇒ pair exadecim bool xA false
+ | x3 ⇒ pair exadecim bool xB false
+ | x4 ⇒ pair exadecim bool xC false
+ | x5 ⇒ pair exadecim bool xD false
+ | x6 ⇒ pair exadecim bool xE false
+ | x7 ⇒ pair exadecim bool xF false
+ | x8 ⇒ pair exadecim bool x0 true
+ | x9 ⇒ pair exadecim bool x1 true
+ | xA ⇒ pair exadecim bool x2 true
+ | xB ⇒ pair exadecim bool x3 true
+ | xC ⇒ pair exadecim bool x4 true
+ | xD ⇒ pair exadecim bool x5 true
+ | xE ⇒ pair exadecim bool x6 true
+ | xF ⇒ pair exadecim bool x7 true ]
| x8 ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool x9 false
- | x1 ⇒ pairT exadecim bool xA false
- | x2 ⇒ pairT exadecim bool xB false
- | x3 ⇒ pairT exadecim bool xC false
- | x4 ⇒ pairT exadecim bool xD false
- | x5 ⇒ pairT exadecim bool xE false
- | x6 ⇒ pairT exadecim bool xF false
- | x7 ⇒ pairT exadecim bool x0 true
- | x8 ⇒ pairT exadecim bool x1 true
- | x9 ⇒ pairT exadecim bool x2 true
- | xA ⇒ pairT exadecim bool x3 true
- | xB ⇒ pairT exadecim bool x4 true
- | xC ⇒ pairT exadecim bool x5 true
- | xD ⇒ pairT exadecim bool x6 true
- | xE ⇒ pairT exadecim bool x7 true
- | xF ⇒ pairT exadecim bool x8 true ]
+ [ x0 ⇒ pair exadecim bool x9 false
+ | x1 ⇒ pair exadecim bool xA false
+ | x2 ⇒ pair exadecim bool xB false
+ | x3 ⇒ pair exadecim bool xC false
+ | x4 ⇒ pair exadecim bool xD false
+ | x5 ⇒ pair exadecim bool xE false
+ | x6 ⇒ pair exadecim bool xF false
+ | x7 ⇒ pair exadecim bool x0 true
+ | x8 ⇒ pair exadecim bool x1 true
+ | x9 ⇒ pair exadecim bool x2 true
+ | xA ⇒ pair exadecim bool x3 true
+ | xB ⇒ pair exadecim bool x4 true
+ | xC ⇒ pair exadecim bool x5 true
+ | xD ⇒ pair exadecim bool x6 true
+ | xE ⇒ pair exadecim bool x7 true
+ | xF ⇒ pair exadecim bool x8 true ]
| x9 ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool xA false
- | x1 ⇒ pairT exadecim bool xB false
- | x2 ⇒ pairT exadecim bool xC false
- | x3 ⇒ pairT exadecim bool xD false
- | x4 ⇒ pairT exadecim bool xE false
- | x5 ⇒ pairT exadecim bool xF false
- | x6 ⇒ pairT exadecim bool x0 true
- | x7 ⇒ pairT exadecim bool x1 true
- | x8 ⇒ pairT exadecim bool x2 true
- | x9 ⇒ pairT exadecim bool x3 true
- | xA ⇒ pairT exadecim bool x4 true
- | xB ⇒ pairT exadecim bool x5 true
- | xC ⇒ pairT exadecim bool x6 true
- | xD ⇒ pairT exadecim bool x7 true
- | xE ⇒ pairT exadecim bool x8 true
- | xF ⇒ pairT exadecim bool x9 true ]
+ [ x0 ⇒ pair exadecim bool xA false
+ | x1 ⇒ pair exadecim bool xB false
+ | x2 ⇒ pair exadecim bool xC false
+ | x3 ⇒ pair exadecim bool xD false
+ | x4 ⇒ pair exadecim bool xE false
+ | x5 ⇒ pair exadecim bool xF false
+ | x6 ⇒ pair exadecim bool x0 true
+ | x7 ⇒ pair exadecim bool x1 true
+ | x8 ⇒ pair exadecim bool x2 true
+ | x9 ⇒ pair exadecim bool x3 true
+ | xA ⇒ pair exadecim bool x4 true
+ | xB ⇒ pair exadecim bool x5 true
+ | xC ⇒ pair exadecim bool x6 true
+ | xD ⇒ pair exadecim bool x7 true
+ | xE ⇒ pair exadecim bool x8 true
+ | xF ⇒ pair exadecim bool x9 true ]
| xA ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool xB false
- | x1 ⇒ pairT exadecim bool xC false
- | x2 ⇒ pairT exadecim bool xD false
- | x3 ⇒ pairT exadecim bool xE false
- | x4 ⇒ pairT exadecim bool xF false
- | x5 ⇒ pairT exadecim bool x0 true
- | x6 ⇒ pairT exadecim bool x1 true
- | x7 ⇒ pairT exadecim bool x2 true
- | x8 ⇒ pairT exadecim bool x3 true
- | x9 ⇒ pairT exadecim bool x4 true
- | xA ⇒ pairT exadecim bool x5 true
- | xB ⇒ pairT exadecim bool x6 true
- | xC ⇒ pairT exadecim bool x7 true
- | xD ⇒ pairT exadecim bool x8 true
- | xE ⇒ pairT exadecim bool x9 true
- | xF ⇒ pairT exadecim bool xA true ]
+ [ x0 ⇒ pair exadecim bool xB false
+ | x1 ⇒ pair exadecim bool xC false
+ | x2 ⇒ pair exadecim bool xD false
+ | x3 ⇒ pair exadecim bool xE false
+ | x4 ⇒ pair exadecim bool xF false
+ | x5 ⇒ pair exadecim bool x0 true
+ | x6 ⇒ pair exadecim bool x1 true
+ | x7 ⇒ pair exadecim bool x2 true
+ | x8 ⇒ pair exadecim bool x3 true
+ | x9 ⇒ pair exadecim bool x4 true
+ | xA ⇒ pair exadecim bool x5 true
+ | xB ⇒ pair exadecim bool x6 true
+ | xC ⇒ pair exadecim bool x7 true
+ | xD ⇒ pair exadecim bool x8 true
+ | xE ⇒ pair exadecim bool x9 true
+ | xF ⇒ pair exadecim bool xA true ]
| xB ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool xC false
- | x1 ⇒ pairT exadecim bool xD false
- | x2 ⇒ pairT exadecim bool xE false
- | x3 ⇒ pairT exadecim bool xF false
- | x4 ⇒ pairT exadecim bool x0 true
- | x5 ⇒ pairT exadecim bool x1 true
- | x6 ⇒ pairT exadecim bool x2 true
- | x7 ⇒ pairT exadecim bool x3 true
- | x8 ⇒ pairT exadecim bool x4 true
- | x9 ⇒ pairT exadecim bool x5 true
- | xA ⇒ pairT exadecim bool x6 true
- | xB ⇒ pairT exadecim bool x7 true
- | xC ⇒ pairT exadecim bool x8 true
- | xD ⇒ pairT exadecim bool x9 true
- | xE ⇒ pairT exadecim bool xA true
- | xF ⇒ pairT exadecim bool xB true ]
+ [ x0 ⇒ pair exadecim bool xC false
+ | x1 ⇒ pair exadecim bool xD false
+ | x2 ⇒ pair exadecim bool xE false
+ | x3 ⇒ pair exadecim bool xF false
+ | x4 ⇒ pair exadecim bool x0 true
+ | x5 ⇒ pair exadecim bool x1 true
+ | x6 ⇒ pair exadecim bool x2 true
+ | x7 ⇒ pair exadecim bool x3 true
+ | x8 ⇒ pair exadecim bool x4 true
+ | x9 ⇒ pair exadecim bool x5 true
+ | xA ⇒ pair exadecim bool x6 true
+ | xB ⇒ pair exadecim bool x7 true
+ | xC ⇒ pair exadecim bool x8 true
+ | xD ⇒ pair exadecim bool x9 true
+ | xE ⇒ pair exadecim bool xA true
+ | xF ⇒ pair exadecim bool xB true ]
| xC ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool xD false
- | x1 ⇒ pairT exadecim bool xE false
- | x2 ⇒ pairT exadecim bool xF false
- | x3 ⇒ pairT exadecim bool x0 true
- | x4 ⇒ pairT exadecim bool x1 true
- | x5 ⇒ pairT exadecim bool x2 true
- | x6 ⇒ pairT exadecim bool x3 true
- | x7 ⇒ pairT exadecim bool x4 true
- | x8 ⇒ pairT exadecim bool x5 true
- | x9 ⇒ pairT exadecim bool x6 true
- | xA ⇒ pairT exadecim bool x7 true
- | xB ⇒ pairT exadecim bool x8 true
- | xC ⇒ pairT exadecim bool x9 true
- | xD ⇒ pairT exadecim bool xA true
- | xE ⇒ pairT exadecim bool xB true
- | xF ⇒ pairT exadecim bool xC true ]
+ [ x0 ⇒ pair exadecim bool xD false
+ | x1 ⇒ pair exadecim bool xE false
+ | x2 ⇒ pair exadecim bool xF false
+ | x3 ⇒ pair exadecim bool x0 true
+ | x4 ⇒ pair exadecim bool x1 true
+ | x5 ⇒ pair exadecim bool x2 true
+ | x6 ⇒ pair exadecim bool x3 true
+ | x7 ⇒ pair exadecim bool x4 true
+ | x8 ⇒ pair exadecim bool x5 true
+ | x9 ⇒ pair exadecim bool x6 true
+ | xA ⇒ pair exadecim bool x7 true
+ | xB ⇒ pair exadecim bool x8 true
+ | xC ⇒ pair exadecim bool x9 true
+ | xD ⇒ pair exadecim bool xA true
+ | xE ⇒ pair exadecim bool xB true
+ | xF ⇒ pair exadecim bool xC true ]
| xD ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool xE false
- | x1 ⇒ pairT exadecim bool xF false
- | x2 ⇒ pairT exadecim bool x0 true
- | x3 ⇒ pairT exadecim bool x1 true
- | x4 ⇒ pairT exadecim bool x2 true
- | x5 ⇒ pairT exadecim bool x3 true
- | x6 ⇒ pairT exadecim bool x4 true
- | x7 ⇒ pairT exadecim bool x5 true
- | x8 ⇒ pairT exadecim bool x6 true
- | x9 ⇒ pairT exadecim bool x7 true
- | xA ⇒ pairT exadecim bool x8 true
- | xB ⇒ pairT exadecim bool x9 true
- | xC ⇒ pairT exadecim bool xA true
- | xD ⇒ pairT exadecim bool xB true
- | xE ⇒ pairT exadecim bool xC true
- | xF ⇒ pairT exadecim bool xD true ]
+ [ x0 ⇒ pair exadecim bool xE false
+ | x1 ⇒ pair exadecim bool xF false
+ | x2 ⇒ pair exadecim bool x0 true
+ | x3 ⇒ pair exadecim bool x1 true
+ | x4 ⇒ pair exadecim bool x2 true
+ | x5 ⇒ pair exadecim bool x3 true
+ | x6 ⇒ pair exadecim bool x4 true
+ | x7 ⇒ pair exadecim bool x5 true
+ | x8 ⇒ pair exadecim bool x6 true
+ | x9 ⇒ pair exadecim bool x7 true
+ | xA ⇒ pair exadecim bool x8 true
+ | xB ⇒ pair exadecim bool x9 true
+ | xC ⇒ pair exadecim bool xA true
+ | xD ⇒ pair exadecim bool xB true
+ | xE ⇒ pair exadecim bool xC true
+ | xF ⇒ pair exadecim bool xD true ]
| xE ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool xF false
- | x1 ⇒ pairT exadecim bool x0 true
- | x2 ⇒ pairT exadecim bool x1 true
- | x3 ⇒ pairT exadecim bool x2 true
- | x4 ⇒ pairT exadecim bool x3 true
- | x5 ⇒ pairT exadecim bool x4 true
- | x6 ⇒ pairT exadecim bool x5 true
- | x7 ⇒ pairT exadecim bool x6 true
- | x8 ⇒ pairT exadecim bool x7 true
- | x9 ⇒ pairT exadecim bool x8 true
- | xA ⇒ pairT exadecim bool x9 true
- | xB ⇒ pairT exadecim bool xA true
- | xC ⇒ pairT exadecim bool xB true
- | xD ⇒ pairT exadecim bool xC true
- | xE ⇒ pairT exadecim bool xD true
- | xF ⇒ pairT exadecim bool xE true ]
+ [ x0 ⇒ pair exadecim bool xF false
+ | x1 ⇒ pair exadecim bool x0 true
+ | x2 ⇒ pair exadecim bool x1 true
+ | x3 ⇒ pair exadecim bool x2 true
+ | x4 ⇒ pair exadecim bool x3 true
+ | x5 ⇒ pair exadecim bool x4 true
+ | x6 ⇒ pair exadecim bool x5 true
+ | x7 ⇒ pair exadecim bool x6 true
+ | x8 ⇒ pair exadecim bool x7 true
+ | x9 ⇒ pair exadecim bool x8 true
+ | xA ⇒ pair exadecim bool x9 true
+ | xB ⇒ pair exadecim bool xA true
+ | xC ⇒ pair exadecim bool xB true
+ | xD ⇒ pair exadecim bool xC true
+ | xE ⇒ pair exadecim bool xD true
+ | xF ⇒ pair exadecim bool xE true ]
| xF ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool x0 true
- | x1 ⇒ pairT exadecim bool x1 true
- | x2 ⇒ pairT exadecim bool x2 true
- | x3 ⇒ pairT exadecim bool x3 true
- | x4 ⇒ pairT exadecim bool x4 true
- | x5 ⇒ pairT exadecim bool x5 true
- | x6 ⇒ pairT exadecim bool x6 true
- | x7 ⇒ pairT exadecim bool x7 true
- | x8 ⇒ pairT exadecim bool x8 true
- | x9 ⇒ pairT exadecim bool x9 true
- | xA ⇒ pairT exadecim bool xA true
- | xB ⇒ pairT exadecim bool xB true
- | xC ⇒ pairT exadecim bool xC true
- | xD ⇒ pairT exadecim bool xD true
- | xE ⇒ pairT exadecim bool xE true
- | xF ⇒ pairT exadecim bool xF true ]
+ [ x0 ⇒ pair exadecim bool x0 true
+ | x1 ⇒ pair exadecim bool x1 true
+ | x2 ⇒ pair exadecim bool x2 true
+ | x3 ⇒ pair exadecim bool x3 true
+ | x4 ⇒ pair exadecim bool x4 true
+ | x5 ⇒ pair exadecim bool x5 true
+ | x6 ⇒ pair exadecim bool x6 true
+ | x7 ⇒ pair exadecim bool x7 true
+ | x8 ⇒ pair exadecim bool x8 true
+ | x9 ⇒ pair exadecim bool x9 true
+ | xA ⇒ pair exadecim bool xA true
+ | xB ⇒ pair exadecim bool xB true
+ | xC ⇒ pair exadecim bool xC true
+ | xD ⇒ pair exadecim bool xD true
+ | xE ⇒ pair exadecim bool xE true
+ | xF ⇒ pair exadecim bool xF true ]
]
| false ⇒
match e1 with
[ x0 ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool x0 false
- | x1 ⇒ pairT exadecim bool x1 false
- | x2 ⇒ pairT exadecim bool x2 false
- | x3 ⇒ pairT exadecim bool x3 false
- | x4 ⇒ pairT exadecim bool x4 false
- | x5 ⇒ pairT exadecim bool x5 false
- | x6 ⇒ pairT exadecim bool x6 false
- | x7 ⇒ pairT exadecim bool x7 false
- | x8 ⇒ pairT exadecim bool x8 false
- | x9 ⇒ pairT exadecim bool x9 false
- | xA ⇒ pairT exadecim bool xA false
- | xB ⇒ pairT exadecim bool xB false
- | xC ⇒ pairT exadecim bool xC false
- | xD ⇒ pairT exadecim bool xD false
- | xE ⇒ pairT exadecim bool xE false
- | xF ⇒ pairT exadecim bool xF false ]
+ [ x0 ⇒ pair exadecim bool x0 false
+ | x1 ⇒ pair exadecim bool x1 false
+ | x2 ⇒ pair exadecim bool x2 false
+ | x3 ⇒ pair exadecim bool x3 false
+ | x4 ⇒ pair exadecim bool x4 false
+ | x5 ⇒ pair exadecim bool x5 false
+ | x6 ⇒ pair exadecim bool x6 false
+ | x7 ⇒ pair exadecim bool x7 false
+ | x8 ⇒ pair exadecim bool x8 false
+ | x9 ⇒ pair exadecim bool x9 false
+ | xA ⇒ pair exadecim bool xA false
+ | xB ⇒ pair exadecim bool xB false
+ | xC ⇒ pair exadecim bool xC false
+ | xD ⇒ pair exadecim bool xD false
+ | xE ⇒ pair exadecim bool xE false
+ | xF ⇒ pair exadecim bool xF false ]
| x1 ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool x1 false
- | x1 ⇒ pairT exadecim bool x2 false
- | x2 ⇒ pairT exadecim bool x3 false
- | x3 ⇒ pairT exadecim bool x4 false
- | x4 ⇒ pairT exadecim bool x5 false
- | x5 ⇒ pairT exadecim bool x6 false
- | x6 ⇒ pairT exadecim bool x7 false
- | x7 ⇒ pairT exadecim bool x8 false
- | x8 ⇒ pairT exadecim bool x9 false
- | x9 ⇒ pairT exadecim bool xA false
- | xA ⇒ pairT exadecim bool xB false
- | xB ⇒ pairT exadecim bool xC false
- | xC ⇒ pairT exadecim bool xD false
- | xD ⇒ pairT exadecim bool xE false
- | xE ⇒ pairT exadecim bool xF false
- | xF ⇒ pairT exadecim bool x0 true ]
+ [ x0 ⇒ pair exadecim bool x1 false
+ | x1 ⇒ pair exadecim bool x2 false
+ | x2 ⇒ pair exadecim bool x3 false
+ | x3 ⇒ pair exadecim bool x4 false
+ | x4 ⇒ pair exadecim bool x5 false
+ | x5 ⇒ pair exadecim bool x6 false
+ | x6 ⇒ pair exadecim bool x7 false
+ | x7 ⇒ pair exadecim bool x8 false
+ | x8 ⇒ pair exadecim bool x9 false
+ | x9 ⇒ pair exadecim bool xA false
+ | xA ⇒ pair exadecim bool xB false
+ | xB ⇒ pair exadecim bool xC false
+ | xC ⇒ pair exadecim bool xD false
+ | xD ⇒ pair exadecim bool xE false
+ | xE ⇒ pair exadecim bool xF false
+ | xF ⇒ pair exadecim bool x0 true ]
| x2 ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool x2 false
- | x1 ⇒ pairT exadecim bool x3 false
- | x2 ⇒ pairT exadecim bool x4 false
- | x3 ⇒ pairT exadecim bool x5 false
- | x4 ⇒ pairT exadecim bool x6 false
- | x5 ⇒ pairT exadecim bool x7 false
- | x6 ⇒ pairT exadecim bool x8 false
- | x7 ⇒ pairT exadecim bool x9 false
- | x8 ⇒ pairT exadecim bool xA false
- | x9 ⇒ pairT exadecim bool xB false
- | xA ⇒ pairT exadecim bool xC false
- | xB ⇒ pairT exadecim bool xD false
- | xC ⇒ pairT exadecim bool xE false
- | xD ⇒ pairT exadecim bool xF false
- | xE ⇒ pairT exadecim bool x0 true
- | xF ⇒ pairT exadecim bool x1 true ]
+ [ x0 ⇒ pair exadecim bool x2 false
+ | x1 ⇒ pair exadecim bool x3 false
+ | x2 ⇒ pair exadecim bool x4 false
+ | x3 ⇒ pair exadecim bool x5 false
+ | x4 ⇒ pair exadecim bool x6 false
+ | x5 ⇒ pair exadecim bool x7 false
+ | x6 ⇒ pair exadecim bool x8 false
+ | x7 ⇒ pair exadecim bool x9 false
+ | x8 ⇒ pair exadecim bool xA false
+ | x9 ⇒ pair exadecim bool xB false
+ | xA ⇒ pair exadecim bool xC false
+ | xB ⇒ pair exadecim bool xD false
+ | xC ⇒ pair exadecim bool xE false
+ | xD ⇒ pair exadecim bool xF false
+ | xE ⇒ pair exadecim bool x0 true
+ | xF ⇒ pair exadecim bool x1 true ]
| x3 ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool x3 false
- | x1 ⇒ pairT exadecim bool x4 false
- | x2 ⇒ pairT exadecim bool x5 false
- | x3 ⇒ pairT exadecim bool x6 false
- | x4 ⇒ pairT exadecim bool x7 false
- | x5 ⇒ pairT exadecim bool x8 false
- | x6 ⇒ pairT exadecim bool x9 false
- | x7 ⇒ pairT exadecim bool xA false
- | x8 ⇒ pairT exadecim bool xB false
- | x9 ⇒ pairT exadecim bool xC false
- | xA ⇒ pairT exadecim bool xD false
- | xB ⇒ pairT exadecim bool xE false
- | xC ⇒ pairT exadecim bool xF false
- | xD ⇒ pairT exadecim bool x0 true
- | xE ⇒ pairT exadecim bool x1 true
- | xF ⇒ pairT exadecim bool x2 true ]
+ [ x0 ⇒ pair exadecim bool x3 false
+ | x1 ⇒ pair exadecim bool x4 false
+ | x2 ⇒ pair exadecim bool x5 false
+ | x3 ⇒ pair exadecim bool x6 false
+ | x4 ⇒ pair exadecim bool x7 false
+ | x5 ⇒ pair exadecim bool x8 false
+ | x6 ⇒ pair exadecim bool x9 false
+ | x7 ⇒ pair exadecim bool xA false
+ | x8 ⇒ pair exadecim bool xB false
+ | x9 ⇒ pair exadecim bool xC false
+ | xA ⇒ pair exadecim bool xD false
+ | xB ⇒ pair exadecim bool xE false
+ | xC ⇒ pair exadecim bool xF false
+ | xD ⇒ pair exadecim bool x0 true
+ | xE ⇒ pair exadecim bool x1 true
+ | xF ⇒ pair exadecim bool x2 true ]
| x4 ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool x4 false
- | x1 ⇒ pairT exadecim bool x5 false
- | x2 ⇒ pairT exadecim bool x6 false
- | x3 ⇒ pairT exadecim bool x7 false
- | x4 ⇒ pairT exadecim bool x8 false
- | x5 ⇒ pairT exadecim bool x9 false
- | x6 ⇒ pairT exadecim bool xA false
- | x7 ⇒ pairT exadecim bool xB false
- | x8 ⇒ pairT exadecim bool xC false
- | x9 ⇒ pairT exadecim bool xD false
- | xA ⇒ pairT exadecim bool xE false
- | xB ⇒ pairT exadecim bool xF false
- | xC ⇒ pairT exadecim bool x0 true
- | xD ⇒ pairT exadecim bool x1 true
- | xE ⇒ pairT exadecim bool x2 true
- | xF ⇒ pairT exadecim bool x3 true ]
+ [ x0 ⇒ pair exadecim bool x4 false
+ | x1 ⇒ pair exadecim bool x5 false
+ | x2 ⇒ pair exadecim bool x6 false
+ | x3 ⇒ pair exadecim bool x7 false
+ | x4 ⇒ pair exadecim bool x8 false
+ | x5 ⇒ pair exadecim bool x9 false
+ | x6 ⇒ pair exadecim bool xA false
+ | x7 ⇒ pair exadecim bool xB false
+ | x8 ⇒ pair exadecim bool xC false
+ | x9 ⇒ pair exadecim bool xD false
+ | xA ⇒ pair exadecim bool xE false
+ | xB ⇒ pair exadecim bool xF false
+ | xC ⇒ pair exadecim bool x0 true
+ | xD ⇒ pair exadecim bool x1 true
+ | xE ⇒ pair exadecim bool x2 true
+ | xF ⇒ pair exadecim bool x3 true ]
| x5 ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool x5 false
- | x1 ⇒ pairT exadecim bool x6 false
- | x2 ⇒ pairT exadecim bool x7 false
- | x3 ⇒ pairT exadecim bool x8 false
- | x4 ⇒ pairT exadecim bool x9 false
- | x5 ⇒ pairT exadecim bool xA false
- | x6 ⇒ pairT exadecim bool xB false
- | x7 ⇒ pairT exadecim bool xC false
- | x8 ⇒ pairT exadecim bool xD false
- | x9 ⇒ pairT exadecim bool xE false
- | xA ⇒ pairT exadecim bool xF false
- | xB ⇒ pairT exadecim bool x0 true
- | xC ⇒ pairT exadecim bool x1 true
- | xD ⇒ pairT exadecim bool x2 true
- | xE ⇒ pairT exadecim bool x3 true
- | xF ⇒ pairT exadecim bool x4 true ]
+ [ x0 ⇒ pair exadecim bool x5 false
+ | x1 ⇒ pair exadecim bool x6 false
+ | x2 ⇒ pair exadecim bool x7 false
+ | x3 ⇒ pair exadecim bool x8 false
+ | x4 ⇒ pair exadecim bool x9 false
+ | x5 ⇒ pair exadecim bool xA false
+ | x6 ⇒ pair exadecim bool xB false
+ | x7 ⇒ pair exadecim bool xC false
+ | x8 ⇒ pair exadecim bool xD false
+ | x9 ⇒ pair exadecim bool xE false
+ | xA ⇒ pair exadecim bool xF false
+ | xB ⇒ pair exadecim bool x0 true
+ | xC ⇒ pair exadecim bool x1 true
+ | xD ⇒ pair exadecim bool x2 true
+ | xE ⇒ pair exadecim bool x3 true
+ | xF ⇒ pair exadecim bool x4 true ]
| x6 ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool x6 false
- | x1 ⇒ pairT exadecim bool x7 false
- | x2 ⇒ pairT exadecim bool x8 false
- | x3 ⇒ pairT exadecim bool x9 false
- | x4 ⇒ pairT exadecim bool xA false
- | x5 ⇒ pairT exadecim bool xB false
- | x6 ⇒ pairT exadecim bool xC false
- | x7 ⇒ pairT exadecim bool xD false
- | x8 ⇒ pairT exadecim bool xE false
- | x9 ⇒ pairT exadecim bool xF false
- | xA ⇒ pairT exadecim bool x0 true
- | xB ⇒ pairT exadecim bool x1 true
- | xC ⇒ pairT exadecim bool x2 true
- | xD ⇒ pairT exadecim bool x3 true
- | xE ⇒ pairT exadecim bool x4 true
- | xF ⇒ pairT exadecim bool x5 true ]
+ [ x0 ⇒ pair exadecim bool x6 false
+ | x1 ⇒ pair exadecim bool x7 false
+ | x2 ⇒ pair exadecim bool x8 false
+ | x3 ⇒ pair exadecim bool x9 false
+ | x4 ⇒ pair exadecim bool xA false
+ | x5 ⇒ pair exadecim bool xB false
+ | x6 ⇒ pair exadecim bool xC false
+ | x7 ⇒ pair exadecim bool xD false
+ | x8 ⇒ pair exadecim bool xE false
+ | x9 ⇒ pair exadecim bool xF false
+ | xA ⇒ pair exadecim bool x0 true
+ | xB ⇒ pair exadecim bool x1 true
+ | xC ⇒ pair exadecim bool x2 true
+ | xD ⇒ pair exadecim bool x3 true
+ | xE ⇒ pair exadecim bool x4 true
+ | xF ⇒ pair exadecim bool x5 true ]
| x7 ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool x7 false
- | x1 ⇒ pairT exadecim bool x8 false
- | x2 ⇒ pairT exadecim bool x9 false
- | x3 ⇒ pairT exadecim bool xA false
- | x4 ⇒ pairT exadecim bool xB false
- | x5 ⇒ pairT exadecim bool xC false
- | x6 ⇒ pairT exadecim bool xD false
- | x7 ⇒ pairT exadecim bool xE false
- | x8 ⇒ pairT exadecim bool xF false
- | x9 ⇒ pairT exadecim bool x0 true
- | xA ⇒ pairT exadecim bool x1 true
- | xB ⇒ pairT exadecim bool x2 true
- | xC ⇒ pairT exadecim bool x3 true
- | xD ⇒ pairT exadecim bool x4 true
- | xE ⇒ pairT exadecim bool x5 true
- | xF ⇒ pairT exadecim bool x6 true ]
+ [ x0 ⇒ pair exadecim bool x7 false
+ | x1 ⇒ pair exadecim bool x8 false
+ | x2 ⇒ pair exadecim bool x9 false
+ | x3 ⇒ pair exadecim bool xA false
+ | x4 ⇒ pair exadecim bool xB false
+ | x5 ⇒ pair exadecim bool xC false
+ | x6 ⇒ pair exadecim bool xD false
+ | x7 ⇒ pair exadecim bool xE false
+ | x8 ⇒ pair exadecim bool xF false
+ | x9 ⇒ pair exadecim bool x0 true
+ | xA ⇒ pair exadecim bool x1 true
+ | xB ⇒ pair exadecim bool x2 true
+ | xC ⇒ pair exadecim bool x3 true
+ | xD ⇒ pair exadecim bool x4 true
+ | xE ⇒ pair exadecim bool x5 true
+ | xF ⇒ pair exadecim bool x6 true ]
| x8 ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool x8 false
- | x1 ⇒ pairT exadecim bool x9 false
- | x2 ⇒ pairT exadecim bool xA false
- | x3 ⇒ pairT exadecim bool xB false
- | x4 ⇒ pairT exadecim bool xC false
- | x5 ⇒ pairT exadecim bool xD false
- | x6 ⇒ pairT exadecim bool xE false
- | x7 ⇒ pairT exadecim bool xF false
- | x8 ⇒ pairT exadecim bool x0 true
- | x9 ⇒ pairT exadecim bool x1 true
- | xA ⇒ pairT exadecim bool x2 true
- | xB ⇒ pairT exadecim bool x3 true
- | xC ⇒ pairT exadecim bool x4 true
- | xD ⇒ pairT exadecim bool x5 true
- | xE ⇒ pairT exadecim bool x6 true
- | xF ⇒ pairT exadecim bool x7 true ]
+ [ x0 ⇒ pair exadecim bool x8 false
+ | x1 ⇒ pair exadecim bool x9 false
+ | x2 ⇒ pair exadecim bool xA false
+ | x3 ⇒ pair exadecim bool xB false
+ | x4 ⇒ pair exadecim bool xC false
+ | x5 ⇒ pair exadecim bool xD false
+ | x6 ⇒ pair exadecim bool xE false
+ | x7 ⇒ pair exadecim bool xF false
+ | x8 ⇒ pair exadecim bool x0 true
+ | x9 ⇒ pair exadecim bool x1 true
+ | xA ⇒ pair exadecim bool x2 true
+ | xB ⇒ pair exadecim bool x3 true
+ | xC ⇒ pair exadecim bool x4 true
+ | xD ⇒ pair exadecim bool x5 true
+ | xE ⇒ pair exadecim bool x6 true
+ | xF ⇒ pair exadecim bool x7 true ]
| x9 ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool x9 false
- | x1 ⇒ pairT exadecim bool xA false
- | x2 ⇒ pairT exadecim bool xB false
- | x3 ⇒ pairT exadecim bool xC false
- | x4 ⇒ pairT exadecim bool xD false
- | x5 ⇒ pairT exadecim bool xE false
- | x6 ⇒ pairT exadecim bool xF false
- | x7 ⇒ pairT exadecim bool x0 true
- | x8 ⇒ pairT exadecim bool x1 true
- | x9 ⇒ pairT exadecim bool x2 true
- | xA ⇒ pairT exadecim bool x3 true
- | xB ⇒ pairT exadecim bool x4 true
- | xC ⇒ pairT exadecim bool x5 true
- | xD ⇒ pairT exadecim bool x6 true
- | xE ⇒ pairT exadecim bool x7 true
- | xF ⇒ pairT exadecim bool x8 true ]
+ [ x0 ⇒ pair exadecim bool x9 false
+ | x1 ⇒ pair exadecim bool xA false
+ | x2 ⇒ pair exadecim bool xB false
+ | x3 ⇒ pair exadecim bool xC false
+ | x4 ⇒ pair exadecim bool xD false
+ | x5 ⇒ pair exadecim bool xE false
+ | x6 ⇒ pair exadecim bool xF false
+ | x7 ⇒ pair exadecim bool x0 true
+ | x8 ⇒ pair exadecim bool x1 true
+ | x9 ⇒ pair exadecim bool x2 true
+ | xA ⇒ pair exadecim bool x3 true
+ | xB ⇒ pair exadecim bool x4 true
+ | xC ⇒ pair exadecim bool x5 true
+ | xD ⇒ pair exadecim bool x6 true
+ | xE ⇒ pair exadecim bool x7 true
+ | xF ⇒ pair exadecim bool x8 true ]
| xA ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool xA false
- | x1 ⇒ pairT exadecim bool xB false
- | x2 ⇒ pairT exadecim bool xC false
- | x3 ⇒ pairT exadecim bool xD false
- | x4 ⇒ pairT exadecim bool xE false
- | x5 ⇒ pairT exadecim bool xF false
- | x6 ⇒ pairT exadecim bool x0 true
- | x7 ⇒ pairT exadecim bool x1 true
- | x8 ⇒ pairT exadecim bool x2 true
- | x9 ⇒ pairT exadecim bool x3 true
- | xA ⇒ pairT exadecim bool x4 true
- | xB ⇒ pairT exadecim bool x5 true
- | xC ⇒ pairT exadecim bool x6 true
- | xD ⇒ pairT exadecim bool x7 true
- | xE ⇒ pairT exadecim bool x8 true
- | xF ⇒ pairT exadecim bool x9 true ]
+ [ x0 ⇒ pair exadecim bool xA false
+ | x1 ⇒ pair exadecim bool xB false
+ | x2 ⇒ pair exadecim bool xC false
+ | x3 ⇒ pair exadecim bool xD false
+ | x4 ⇒ pair exadecim bool xE false
+ | x5 ⇒ pair exadecim bool xF false
+ | x6 ⇒ pair exadecim bool x0 true
+ | x7 ⇒ pair exadecim bool x1 true
+ | x8 ⇒ pair exadecim bool x2 true
+ | x9 ⇒ pair exadecim bool x3 true
+ | xA ⇒ pair exadecim bool x4 true
+ | xB ⇒ pair exadecim bool x5 true
+ | xC ⇒ pair exadecim bool x6 true
+ | xD ⇒ pair exadecim bool x7 true
+ | xE ⇒ pair exadecim bool x8 true
+ | xF ⇒ pair exadecim bool x9 true ]
| xB ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool xB false
- | x1 ⇒ pairT exadecim bool xC false
- | x2 ⇒ pairT exadecim bool xD false
- | x3 ⇒ pairT exadecim bool xE false
- | x4 ⇒ pairT exadecim bool xF false
- | x5 ⇒ pairT exadecim bool x0 true
- | x6 ⇒ pairT exadecim bool x1 true
- | x7 ⇒ pairT exadecim bool x2 true
- | x8 ⇒ pairT exadecim bool x3 true
- | x9 ⇒ pairT exadecim bool x4 true
- | xA ⇒ pairT exadecim bool x5 true
- | xB ⇒ pairT exadecim bool x6 true
- | xC ⇒ pairT exadecim bool x7 true
- | xD ⇒ pairT exadecim bool x8 true
- | xE ⇒ pairT exadecim bool x9 true
- | xF ⇒ pairT exadecim bool xA true ]
+ [ x0 ⇒ pair exadecim bool xB false
+ | x1 ⇒ pair exadecim bool xC false
+ | x2 ⇒ pair exadecim bool xD false
+ | x3 ⇒ pair exadecim bool xE false
+ | x4 ⇒ pair exadecim bool xF false
+ | x5 ⇒ pair exadecim bool x0 true
+ | x6 ⇒ pair exadecim bool x1 true
+ | x7 ⇒ pair exadecim bool x2 true
+ | x8 ⇒ pair exadecim bool x3 true
+ | x9 ⇒ pair exadecim bool x4 true
+ | xA ⇒ pair exadecim bool x5 true
+ | xB ⇒ pair exadecim bool x6 true
+ | xC ⇒ pair exadecim bool x7 true
+ | xD ⇒ pair exadecim bool x8 true
+ | xE ⇒ pair exadecim bool x9 true
+ | xF ⇒ pair exadecim bool xA true ]
| xC ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool xC false
- | x1 ⇒ pairT exadecim bool xD false
- | x2 ⇒ pairT exadecim bool xE false
- | x3 ⇒ pairT exadecim bool xF false
- | x4 ⇒ pairT exadecim bool x0 true
- | x5 ⇒ pairT exadecim bool x1 true
- | x6 ⇒ pairT exadecim bool x2 true
- | x7 ⇒ pairT exadecim bool x3 true
- | x8 ⇒ pairT exadecim bool x4 true
- | x9 ⇒ pairT exadecim bool x5 true
- | xA ⇒ pairT exadecim bool x6 true
- | xB ⇒ pairT exadecim bool x7 true
- | xC ⇒ pairT exadecim bool x8 true
- | xD ⇒ pairT exadecim bool x9 true
- | xE ⇒ pairT exadecim bool xA true
- | xF ⇒ pairT exadecim bool xB true ]
+ [ x0 ⇒ pair exadecim bool xC false
+ | x1 ⇒ pair exadecim bool xD false
+ | x2 ⇒ pair exadecim bool xE false
+ | x3 ⇒ pair exadecim bool xF false
+ | x4 ⇒ pair exadecim bool x0 true
+ | x5 ⇒ pair exadecim bool x1 true
+ | x6 ⇒ pair exadecim bool x2 true
+ | x7 ⇒ pair exadecim bool x3 true
+ | x8 ⇒ pair exadecim bool x4 true
+ | x9 ⇒ pair exadecim bool x5 true
+ | xA ⇒ pair exadecim bool x6 true
+ | xB ⇒ pair exadecim bool x7 true
+ | xC ⇒ pair exadecim bool x8 true
+ | xD ⇒ pair exadecim bool x9 true
+ | xE ⇒ pair exadecim bool xA true
+ | xF ⇒ pair exadecim bool xB true ]
| xD ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool xD false
- | x1 ⇒ pairT exadecim bool xE false
- | x2 ⇒ pairT exadecim bool xF false
- | x3 ⇒ pairT exadecim bool x0 true
- | x4 ⇒ pairT exadecim bool x1 true
- | x5 ⇒ pairT exadecim bool x2 true
- | x6 ⇒ pairT exadecim bool x3 true
- | x7 ⇒ pairT exadecim bool x4 true
- | x8 ⇒ pairT exadecim bool x5 true
- | x9 ⇒ pairT exadecim bool x6 true
- | xA ⇒ pairT exadecim bool x7 true
- | xB ⇒ pairT exadecim bool x8 true
- | xC ⇒ pairT exadecim bool x9 true
- | xD ⇒ pairT exadecim bool xA true
- | xE ⇒ pairT exadecim bool xB true
- | xF ⇒ pairT exadecim bool xC true ]
+ [ x0 ⇒ pair exadecim bool xD false
+ | x1 ⇒ pair exadecim bool xE false
+ | x2 ⇒ pair exadecim bool xF false
+ | x3 ⇒ pair exadecim bool x0 true
+ | x4 ⇒ pair exadecim bool x1 true
+ | x5 ⇒ pair exadecim bool x2 true
+ | x6 ⇒ pair exadecim bool x3 true
+ | x7 ⇒ pair exadecim bool x4 true
+ | x8 ⇒ pair exadecim bool x5 true
+ | x9 ⇒ pair exadecim bool x6 true
+ | xA ⇒ pair exadecim bool x7 true
+ | xB ⇒ pair exadecim bool x8 true
+ | xC ⇒ pair exadecim bool x9 true
+ | xD ⇒ pair exadecim bool xA true
+ | xE ⇒ pair exadecim bool xB true
+ | xF ⇒ pair exadecim bool xC true ]
| xE ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool xE false
- | x1 ⇒ pairT exadecim bool xF false
- | x2 ⇒ pairT exadecim bool x0 true
- | x3 ⇒ pairT exadecim bool x1 true
- | x4 ⇒ pairT exadecim bool x2 true
- | x5 ⇒ pairT exadecim bool x3 true
- | x6 ⇒ pairT exadecim bool x4 true
- | x7 ⇒ pairT exadecim bool x5 true
- | x8 ⇒ pairT exadecim bool x6 true
- | x9 ⇒ pairT exadecim bool x7 true
- | xA ⇒ pairT exadecim bool x8 true
- | xB ⇒ pairT exadecim bool x9 true
- | xC ⇒ pairT exadecim bool xA true
- | xD ⇒ pairT exadecim bool xB true
- | xE ⇒ pairT exadecim bool xC true
- | xF ⇒ pairT exadecim bool xD true ]
+ [ x0 ⇒ pair exadecim bool xE false
+ | x1 ⇒ pair exadecim bool xF false
+ | x2 ⇒ pair exadecim bool x0 true
+ | x3 ⇒ pair exadecim bool x1 true
+ | x4 ⇒ pair exadecim bool x2 true
+ | x5 ⇒ pair exadecim bool x3 true
+ | x6 ⇒ pair exadecim bool x4 true
+ | x7 ⇒ pair exadecim bool x5 true
+ | x8 ⇒ pair exadecim bool x6 true
+ | x9 ⇒ pair exadecim bool x7 true
+ | xA ⇒ pair exadecim bool x8 true
+ | xB ⇒ pair exadecim bool x9 true
+ | xC ⇒ pair exadecim bool xA true
+ | xD ⇒ pair exadecim bool xB true
+ | xE ⇒ pair exadecim bool xC true
+ | xF ⇒ pair exadecim bool xD true ]
| xF ⇒
match e2 with
- [ x0 ⇒ pairT exadecim bool xF false
- | x1 ⇒ pairT exadecim bool x0 true
- | x2 ⇒ pairT exadecim bool x1 true
- | x3 ⇒ pairT exadecim bool x2 true
- | x4 ⇒ pairT exadecim bool x3 true
- | x5 ⇒ pairT exadecim bool x4 true
- | x6 ⇒ pairT exadecim bool x5 true
- | x7 ⇒ pairT exadecim bool x6 true
- | x8 ⇒ pairT exadecim bool x7 true
- | x9 ⇒ pairT exadecim bool x8 true
- | xA ⇒ pairT exadecim bool x9 true
- | xB ⇒ pairT exadecim bool xA true
- | xC ⇒ pairT exadecim bool xB true
- | xD ⇒ pairT exadecim bool xC true
- | xE ⇒ pairT exadecim bool xD true
- | xF ⇒ pairT exadecim bool xE true ]
+ [ x0 ⇒ pair exadecim bool xF false
+ | x1 ⇒ pair exadecim bool x0 true
+ | x2 ⇒ pair exadecim bool x1 true
+ | x3 ⇒ pair exadecim bool x2 true
+ | x4 ⇒ pair exadecim bool x3 true
+ | x5 ⇒ pair exadecim bool x4 true
+ | x6 ⇒ pair exadecim bool x5 true
+ | x7 ⇒ pair exadecim bool x6 true
+ | x8 ⇒ pair exadecim bool x7 true
+ | x9 ⇒ pair exadecim bool x8 true
+ | xA ⇒ pair exadecim bool x9 true
+ | xB ⇒ pair exadecim bool xA true
+ | xC ⇒ pair exadecim bool xB true
+ | xD ⇒ pair exadecim bool xC true
+ | xE ⇒ pair exadecim bool xD true
+ | xF ⇒ pair exadecim bool xE true ]
]
].
(* operatore somma senza carry *)
definition plus_exnc ≝
-λe1,e2:exadecim.fstT ?? (plus_ex e1 e2 false).
+λe1,e2:exadecim.fst ?? (plus_ex e1 e2 false).
(* operatore carry della somma *)
definition plus_exc ≝
-λe1,e2:exadecim.sndT ?? (plus_ex e1 e2 false).
+λe1,e2:exadecim.snd ?? (plus_ex e1 e2 false).
(* operatore Most Significant Bit *)
definition MSB_ex ≝
lemma plusex_ok:
∀b1,b2,c.
match plus_ex b1 b2 c with
- [ pairT r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_exadecim r + nat_of_bool c' * 16 ].
+ [ pair r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_exadecim r + nat_of_bool c' * 16 ].
intros;
elim b1; (elim b2; (elim c; normalize; reflexivity)).
qed.
lemma ok_rcr_ex : ∀e:exadecim.∀b:bool.
rcr_ex e b =
- pairT exadecim bool
+ pair exadecim bool
(exadecim_of_nat ((e/2)+match b with [ true ⇒ 8 | false ⇒ 0]))
(eqb (mod e 2) 1).
intros;
lemma ok_rcl_ex : ∀e:exadecim.∀b:bool.
rcl_ex e b =
- pairT exadecim bool
+ pair exadecim bool
(exadecim_of_nat ((mod (e*2) 16)+match b with [ true ⇒ 1 | false ⇒ 0]))
(notb (ltb e 8)).
intros;
lemma ok_shr_ex : ∀e:exadecim.
shr_ex e =
- pairT exadecim bool
+ pair exadecim bool
(exadecim_of_nat (e/2))
(eqb (mod e 2) 1).
intros;
lemma ok_shl_ex : ∀e:exadecim.
shl_ex e =
- pairT exadecim bool
+ pair exadecim bool
(exadecim_of_nat (mod (e*2) 16))
(notb (ltb e 8)).
intros;