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;
(* fAMC e' la logica da applicare: somma con/senza carry *)
definition execute_ADC_ADD_aux ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
-λfAMC:byte8 → byte8 → bool → ProdT byte8 bool.
+λfAMC:byte8 → byte8 → bool → Prod byte8 bool.
opt_map ?? (multi_mode_load true m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
let A_op ≝ get_acc_8_low_reg m t s_tmp1 in
match fAMC A_op M_op (get_c_flag m t s_tmp1) with
- [ pairT R_op carry ⇒
+ [ pair R_op carry ⇒
let A7 ≝ MSB_b8 A_op in let M7 ≝ MSB_b8 M_op in let R7 ≝ MSB_b8 R_op in
let A3 ≝ MSB_ex (b8l A_op) in let M3 ≝ MSB_ex (b8l M_op) in let R3 ≝ MSB_ex (b8l R_op) in
(* A = [true] fAMC(A,M,C), [false] A *)
(* V = A7&M7&nR7 | nA7&nM7&R7 *)
let s_tmp7 ≝ setweak_v_flag m t s_tmp6 ((A7⊗M7⊗(⊖R7)) ⊕ ((⊖A7)⊗(⊖M7)⊗R7)) in
(* newpc = nextpc *)
- Some ? (pairT ?? s_tmp7 new_pc) ]]).
+ Some ? (pair ?? s_tmp7 new_pc) ]]).
(* A = [true] fAM(A,M), [false] A *)
(* cioe' in caso di false l'operazione viene eseguita ma modifica solo i flag *)
(* V = 0 *)
let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
(* newpc = nextpc *)
- Some ? (pairT ?? s_tmp5 new_pc) ]).
+ Some ? (pair ?? s_tmp5 new_pc) ]).
(* M = fMC(M,C) *)
(* fMC e' la logica da applicare: rc_/ro_/sh_ *)
definition execute_ASL_ASR_LSR_ROL_ROR_aux ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
-λfMC:byte8 → bool → ProdT byte8 bool.
+λfMC:byte8 → bool → Prod byte8 bool.
opt_map ?? (multi_mode_load true m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op _ ⇒
- match fMC M_op (get_c_flag m t s_tmp1) with [ pairT R_op carry ⇒
+ match fMC M_op (get_c_flag m t s_tmp1) with [ pair R_op carry ⇒
(* M = fMC(M,C) *)
opt_map ?? (multi_mode_write true m t s_tmp1 cur_pc i R_op)
(λS_PC.match S_PC with
- [ pairT s_tmp2 new_pc ⇒
+ [ pair s_tmp2 new_pc ⇒
(* C = carry *)
let s_tmp3 ≝ set_c_flag m t s_tmp2 carry in
(* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
(* V = R7 ⊙ carry *)
let s_tmp6 ≝ setweak_v_flag m t s_tmp5 ((MSB_b8 R_op) ⊙ carry) in
(* newpc = nextpc *)
- Some ? (pairT ?? s_tmp6 new_pc) ])]]).
+ Some ? (pair ?? s_tmp6 new_pc) ])]]).
(* estensione del segno byte → word *)
definition byte_extension ≝
(* if true, branch *)
match fCOND with
(* newpc = nextpc + rel *)
- [ true ⇒ Some ? (pairT ?? s_tmp1 (branched_pc m t s_tmp1 new_pc M_op))
+ [ true ⇒ Some ? (pair ?? s_tmp1 (branched_pc m t s_tmp1 new_pc M_op))
(* newpc = nextpc *)
- | false ⇒ Some ? (pairT ?? s_tmp1 new_pc) ]]).
+ | false ⇒ Some ? (pair ?? s_tmp1 new_pc) ]]).
(* Mn = filtered optval *)
(* il chiamante passa 0x00 per azzerare, 0xFF per impostare il bit di M *)
opt_map ?? (multi_mode_write true m t s cur_pc i optval)
(λS_PC.match S_PC with
(* newpc = nextpc *)
- [ pairT s_tmp1 new_pc ⇒ Some ? (pairT ?? s_tmp1 new_pc) ]).
+ [ pair s_tmp1 new_pc ⇒ Some ? (pair ?? s_tmp1 new_pc) ]).
(* if COND(Mn) branch *)
(* il chiamante passa la logica da testare (0x00,¬0x00) e poi si salta *)
(* if COND(Mn) branch *)
match fCOND MH_op with
(* newpc = nextpc + rel *)
- [ true ⇒ Some ? (pairT ?? s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
+ [ true ⇒ Some ? (pair ?? s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
(* newpc = nextpc *)
- | false ⇒ Some ? (pairT ?? s_tmp1 new_pc) ]]]).
+ | false ⇒ Some ? (pair ?? s_tmp1 new_pc) ]]]).
(* M = fM(M) *)
(* fM e' la logica da applicare: not/neg/++/-- *)
(* M = fM(M) *)
opt_map ?? (multi_mode_write true m t s_tmp1 cur_pc i R_op)
(λS_PC.match S_PC with
- [ pairT s_tmp2 new_pc ⇒
+ [ pair s_tmp2 new_pc ⇒
(* C = fCR (C,R) *)
let s_tmp3 ≝ set_c_flag m t s_tmp2 (fC (get_c_flag m t s_tmp2) R_op) in
(* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
(* V = fV (M7,R7) *)
let s_tmp6 ≝ setweak_v_flag m t s_tmp5 (fV (MSB_b8 M_op) (MSB_b8 R_op)) in
(* newpc = nextpc *)
- Some ? (pairT ?? s_tmp6 new_pc) ])]).
+ Some ? (pair ?? s_tmp6 new_pc) ])]).
(* A = [true] fAMC(A,M,C), [false] A *)
(* cioe' in caso di false l'operazione viene eseguita ma modifica solo i flag *)
(* fAMC e' la logica da applicare: sottrazione con/senza carry *)
definition execute_SBC_SUB_aux ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
-λfAMC:byte8 → byte8 → bool → ProdT byte8 bool.
+λfAMC:byte8 → byte8 → bool → Prod byte8 bool.
opt_map ?? (multi_mode_load true m t s cur_pc i)
(λS_M_PC.match S_M_PC with
[ tripleT s_tmp1 M_op new_pc ⇒
let A_op ≝ get_acc_8_low_reg m t s_tmp1 in
match fAMC A_op M_op (get_c_flag m t s_tmp1) with
- [ pairT R_op carry ⇒
+ [ pair R_op carry ⇒
let A7 ≝ MSB_b8 A_op in let M7 ≝ MSB_b8 M_op in let R7 ≝ MSB_b8 R_op in
(* A = [true] fAMC(A,M,C), [false] A *)
let s_tmp2 ≝ match setflag with [ true ⇒ set_acc_8_low_reg m t s_tmp1 R_op | false ⇒ s_tmp1 ] in
(* V = A7&nM7&nR7 | nA7&M7&R7 *)
let s_tmp6 ≝ setweak_v_flag m t s_tmp5 ((A7⊗(⊖M7)⊗(⊖R7)) ⊕ ((⊖A7)⊗M7⊗R7)) in
(* newpc = nextpc *)
- Some ? (pairT ?? s_tmp6 new_pc) ]]).
+ Some ? (pair ?? s_tmp6 new_pc) ]]).
(* il classico push *)
definition aux_push ≝
(λs_tmp1.opt_map ?? (get_sp_reg m t s_tmp1)
(* val = [SP] *)
(λSP_op'.opt_map ?? (memory_filter_read m t s_tmp1 SP_op')
- (λval.Some ? (pairT ?? s_tmp1 val))))).
+ (λval.Some ? (pair ?? s_tmp1 val))))).
(* CCR corrisponde a V11HINZC e cmq 1 se un flag non esiste *)
(* i flag mantengono posizione costante nelle varie ALU, e se non sono
opt_map ?? (get_sp_reg m t s_tmp1)
(* SP += extended M *)
(λSP_op.opt_map ?? (set_sp_reg m t s_tmp1 (plus_w16nc SP_op (byte_extension M_op)))
- (λs_tmp2.Some ? (pairT ?? s_tmp2 new_pc))) ]).
+ (λs_tmp2.Some ? (pair ?? s_tmp2 new_pc))) ]).
(* H:X += extended M *)
definition execute_AIX ≝
opt_map ?? (get_indX_16_reg m t s_tmp1)
(* H:X += extended M *)
(λHX_op.opt_map ?? (set_indX_16_reg m t s_tmp1 (plus_w16nc HX_op (byte_extension M_op)))
- (λs_tmp2.Some ? (pairT ?? s_tmp2 new_pc))) ]).
+ (λs_tmp2.Some ? (pair ?? s_tmp2 new_pc))) ]).
(* A = A & M *)
definition execute_AND ≝
(* BGND mode *)
definition execute_BGND ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pairT ?? s cur_pc).
+ Some ? (pair ?? s cur_pc).
(* if Z|N⊙V=0, branch *)
definition execute_BGT ≝
(* push (new_pc high) *)
(λs_tmp2.opt_map ?? (aux_push m t s_tmp2 (w16h new_pc))
(* new_pc = new_pc + rel *)
- (λs_tmp3.Some ? (pairT ?? s_tmp3 (branched_pc m t s_tmp3 new_pc M_op))))
+ (λs_tmp3.Some ? (pair ?? s_tmp3 (branched_pc m t s_tmp3 new_pc M_op))))
in match m with
[ HC05 ⇒ aux | HC08 ⇒ aux | HCS08 ⇒ aux
| RS08 ⇒
(* SPC = new_pc *)
opt_map ?? (set_spc_reg m t s_tmp1 new_pc)
(* new_pc = new_pc + rel *)
- (λs_tmp2.Some ? (pairT ?? s_tmp2 (branched_pc m t s_tmp2 new_pc M_op)))
+ (λs_tmp2.Some ? (pair ?? s_tmp2 (branched_pc m t s_tmp2 new_pc M_op)))
]]).
(* if A=M, branch *)
(* if A=M, branch *)
match eq_b8 (get_acc_8_low_reg m t s_tmp1) MH_op with
(* new_pc = new_pc + rel *)
- [ true ⇒ Some ? (pairT ?? s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
+ [ true ⇒ Some ? (pair ?? s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
(* new_pc = new_pc *)
- | false ⇒ Some ? (pairT ?? s_tmp1 new_pc)
+ | false ⇒ Some ? (pair ?? s_tmp1 new_pc)
]]]).
(* if X=M, branch *)
(* if X=M, branch *)
(λX_op.match eq_b8 X_op MH_op with
(* new_pc = new_pc + rel *)
- [ true ⇒ Some ? (pairT ?? s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
+ [ true ⇒ Some ? (pair ?? s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
(* new_pc = new_pc *)
- | false ⇒ Some ? (pairT ?? s_tmp1 new_pc)
+ | false ⇒ Some ? (pair ?? s_tmp1 new_pc)
])]]).
(* C = 0 *)
definition execute_CLC ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pairT ?? (set_c_flag m t s false) cur_pc).
+ Some ? (pair ?? (set_c_flag m t s false) cur_pc).
(* I = 0 *)
definition execute_CLI ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
opt_map ?? (set_i_flag m t s false)
- (λs_tmp.Some ? (pairT ?? s_tmp cur_pc)).
+ (λs_tmp.Some ? (pair ?? s_tmp cur_pc)).
(* M = 0 *)
definition execute_CLR ≝
(* M = 0 *)
opt_map ?? (multi_mode_write true m t s cur_pc i 〈x0,x0〉)
(λS_PC.match S_PC with
- [ pairT s_tmp1 new_pc ⇒
+ [ pair s_tmp1 new_pc ⇒
(* Z = 1 *)
let s_tmp2 ≝ set_z_flag m t s_tmp1 true in
(* N = 0 *)
(* V = 0 *)
let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
(* newpc = nextpc *)
- Some ? (pairT ?? s_tmp4 new_pc) ]).
+ Some ? (pair ?? s_tmp4 new_pc) ]).
(* flags = A - M *)
definition execute_CMP ≝
opt_map ?? (get_indX_16_reg m t s_tmp1)
(λX_op.
match plus_w16 X_op (compl_w16 M_op) false with
- [ pairT R_op carry ⇒
+ [ pair R_op carry ⇒
let X15 ≝ MSB_w16 X_op in let M15 ≝ MSB_w16 M_op in let R15 ≝ MSB_w16 R_op in
(* Z = nR15&nR14&nR13&nR12&nR11&nR10&nR9&nR8&nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_w16 R_op 〈〈x0,x0〉:〈x0,x0〉〉) in
(* V = X15&nM15&nR15 | nX15&M15&R15 *)
let s_tmp5 ≝ setweak_v_flag m t s_tmp4 ((X15⊗(⊖M15)⊗(⊖R15)) ⊕ ((⊖X15)⊗M15⊗R15)) in
(* newpc = nextpc *)
- Some ? (pairT ?? s_tmp5 new_pc) ] ) ]).
+ Some ? (pair ?? s_tmp5 new_pc) ] ) ]).
(* flags = X - M *)
definition execute_CPX ≝
opt_map ?? (get_indX_8_low_reg m t s_tmp1)
(λX_op.
match plus_b8 X_op (compl_b8 M_op) false with
- [ pairT R_op carry ⇒
+ [ pair R_op carry ⇒
let X7 ≝ MSB_b8 X_op in let M7 ≝ MSB_b8 M_op in let R7 ≝ MSB_b8 R_op in
(* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 R_op 〈x0,x0〉) in
(* V = X7&nM7&nR7 | nX7&M7&R7 *)
let s_tmp5 ≝ setweak_v_flag m t s_tmp4 ((X7⊗(⊖M7)⊗(⊖R7)) ⊕ ((⊖X7)⊗M7⊗R7)) in
(* newpc = nextpc *)
- Some ? (pairT ?? s_tmp5 new_pc) ] ) ]).
+ Some ? (pair ?? s_tmp5 new_pc) ] ) ]).
(* decimal adjiust A *)
(* per i dettagli vedere daa_b8 (modulo byte8) *)
(λH.
let M_op ≝ get_acc_8_low_reg m t s in
match daa_b8 H (get_c_flag m t s) M_op with
- [ pairT R_op carry ⇒
+ [ pair R_op carry ⇒
(* A = R *)
let s_tmp1 ≝ set_acc_8_low_reg m t s R_op in
(* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
(* V = M7 ⊙ R7 *)
let s_tmp5 ≝ setweak_v_flag m t s_tmp4 ((MSB_b8 M_op) ⊙ (MSB_b8 R_op)) in
(* newpc = curpc *)
- Some ? (pairT ?? s_tmp5 cur_pc) ]).
+ Some ? (pair ?? s_tmp5 cur_pc) ]).
(* if (--M)≠0, branch *)
definition execute_DBNZ ≝
let MH_op' ≝ pred_b8 MH_op in
opt_map ?? (multi_mode_write true m t s_tmp1 cur_pc i MH_op')
(λS_PC.match S_PC with
- [ pairT s_tmp2 _ ⇒
+ [ pair s_tmp2 _ ⇒
(* if (--M)≠0, branch *)
match eq_b8 MH_op' 〈x0,x0〉 with
(* new_pc = new_pc *)
- [ true ⇒ Some ? (pairT ?? s_tmp2 new_pc)
+ [ true ⇒ Some ? (pair ?? s_tmp2 new_pc)
(* new_pc = new_pc + rel *)
- | false ⇒ Some ? (pairT ?? s_tmp2 (branched_pc m t s_tmp2 new_pc ML_op)) ]])]]).
+ | false ⇒ Some ? (pair ?? s_tmp2 (branched_pc m t s_tmp2 new_pc ML_op)) ]])]]).
(* M = M - 1 *)
definition execute_DEC ≝
opt_map ?? (match overflow with
[ true ⇒ Some ? s_tmp3
| false ⇒ set_indX_8_high_reg m t s_tmp3 rest])
- (λs_tmp4.Some ? (pairT ?? s_tmp4 cur_pc)) ])).
+ (λs_tmp4.Some ? (pair ?? s_tmp4 cur_pc)) ])).
(* A = A ⊙ M *)
definition execute_EOR ≝
opt_map ?? (multi_mode_load false m t s cur_pc i)
(λS_M_PC.
(* newpc = M_op *)
- Some ? (pairT ?? (fst3T ??? S_M_PC) (snd3T ??? S_M_PC))).
+ Some ? (pair ?? (fst3T ??? S_M_PC) (snd3T ??? S_M_PC))).
(* jump to subroutine *)
(* HC05/HC08/HCS08 si appoggiano allo stack, RS08 a SPC *)
(* push (new_pc high) *)
(λs_tmp2.opt_map ?? (aux_push m t s_tmp2 (w16h new_pc))
(* newpc = M_op *)
- (λs_tmp3.Some ? (pairT ?? s_tmp3 M_op)))
+ (λs_tmp3.Some ? (pair ?? s_tmp3 M_op)))
in match m with
[ HC05 ⇒ aux | HC08 ⇒ aux | HCS08 ⇒ aux
| RS08 ⇒
(* SPC = new_pc *)
opt_map ?? (set_spc_reg m t s_tmp1 new_pc)
(* newpc = M_op *)
- (λs_tmp2.Some ? (pairT ?? s_tmp2 M_op))
+ (λs_tmp2.Some ? (pair ?? s_tmp2 M_op))
]]).
(* A = M *)
(* V = 0 *)
let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
(* newpc = nextpc *)
- Some ? (pairT ?? s_tmp5 new_pc) ]).
+ Some ? (pair ?? s_tmp5 new_pc) ]).
(* H:X = M *)
definition execute_LDHX ≝
(* V = 0 *)
let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
(* newpc = nextpc *)
- Some ? (pairT ?? s_tmp5 new_pc)) ]).
+ Some ? (pair ?? s_tmp5 new_pc)) ]).
(* X = M *)
definition execute_LDX ≝
(* V = 0 *)
let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
(* newpc = nextpc *)
- Some ? (pairT ?? s_tmp5 new_pc)) ]).
+ Some ? (pair ?? s_tmp5 new_pc)) ]).
(* M = 0 -> rcr M -> C' *)
definition execute_LSR ≝
(* M2 = R_op *)
opt_map ?? (multi_mode_write true m t s_tmp1 tmp_pc i R_op)
(λS_PC.match S_PC with
- [ pairT s_tmp2 new_pc ⇒
+ [ pair s_tmp2 new_pc ⇒
(* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 R_op 〈x0,x0〉) in
(* N = R7 *)
(* V = 0 *)
let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
(* newpc = nextpc *)
- Some ? (pairT ?? s_tmp5 new_pc)])]).
+ Some ? (pair ?? s_tmp5 new_pc)])]).
(* X:A = X * A *)
definition execute_MUL ≝
opt_map ?? (get_indX_8_low_reg m t s)
(λX_op.let R_op ≝ mul_b8 X_op (get_acc_8_low_reg m t s) in
opt_map ?? (set_indX_8_low_reg m t s (w16h R_op))
- (λs_tmp.Some ? (pairT ?? (set_acc_8_low_reg m t s_tmp (w16l R_op)) cur_pc))).
+ (λs_tmp.Some ? (pair ?? (set_acc_8_low_reg m t s_tmp (w16l R_op)) cur_pc))).
(* M = compl M *)
definition execute_NEG ≝
(* nulla *)
definition execute_NOP ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pairT ?? s cur_pc).
+ Some ? (pair ?? s cur_pc).
(* A = (mk_byte8 (b8l A) (b8h A)) *)
(* cioe' swap del nibble alto/nibble basso di A *)
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
match get_acc_8_low_reg m t s with [ mk_byte8 ah al ⇒
(* A = (mk_byte8 (b8l A) (b8h A)) *)
- Some ? (pairT ?? (set_acc_8_low_reg m t s 〈al,ah〉) cur_pc) ].
+ Some ? (pair ?? (set_acc_8_low_reg m t s 〈al,ah〉) cur_pc) ].
(* A = A | M *)
definition execute_ORA ≝
definition execute_PSHA ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
opt_map ?? (aux_push m t s (get_acc_8_low_reg m t s))
- (λs_tmp1.Some ? (pairT ?? s_tmp1 cur_pc)).
+ (λs_tmp1.Some ? (pair ?? s_tmp1 cur_pc)).
(* push H *)
definition execute_PSHH ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
opt_map ?? (get_indX_8_high_reg m t s)
(λH_op.opt_map ?? (aux_push m t s H_op)
- (λs_tmp1.Some ? (pairT ?? s_tmp1 cur_pc))).
+ (λs_tmp1.Some ? (pair ?? s_tmp1 cur_pc))).
(* push X *)
definition execute_PSHX ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
opt_map ?? (get_indX_8_low_reg m t s)
(λH_op.opt_map ?? (aux_push m t s H_op)
- (λs_tmp1.Some ? (pairT ?? s_tmp1 cur_pc))).
+ (λs_tmp1.Some ? (pair ?? s_tmp1 cur_pc))).
(* pop A *)
definition execute_PULA ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
opt_map ?? (aux_pop m t s)
- (λS_and_A.match S_and_A with [ pairT s_tmp1 A_op ⇒
- Some ? (pairT ?? (set_acc_8_low_reg m t s_tmp1 A_op) cur_pc) ]).
+ (λS_and_A.match S_and_A with [ pair s_tmp1 A_op ⇒
+ Some ? (pair ?? (set_acc_8_low_reg m t s_tmp1 A_op) cur_pc) ]).
(* pop H *)
definition execute_PULH ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
opt_map ?? (aux_pop m t s)
- (λS_and_H.match S_and_H with [ pairT s_tmp1 H_op ⇒
+ (λS_and_H.match S_and_H with [ pair s_tmp1 H_op ⇒
opt_map ?? (set_indX_8_high_reg m t s_tmp1 H_op)
- (λs_tmp2.Some ? (pairT ?? s_tmp2 cur_pc))]).
+ (λs_tmp2.Some ? (pair ?? s_tmp2 cur_pc))]).
(* pop X *)
definition execute_PULX ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
opt_map ?? (aux_pop m t s)
- (λS_and_X.match S_and_X with [ pairT s_tmp1 X_op ⇒
+ (λS_and_X.match S_and_X with [ pair s_tmp1 X_op ⇒
opt_map ?? (set_indX_8_low_reg m t s_tmp1 X_op)
- (λs_tmp2.Some ? (pairT ?? s_tmp2 cur_pc))]).
+ (λs_tmp2.Some ? (pair ?? s_tmp2 cur_pc))]).
(* M = C' <- rcl M <- C *)
definition execute_ROL ≝
opt_map ?? (get_sp_reg m t s)
(λSP_op.match SP_op with [ mk_word16 sph spl ⇒
opt_map ?? (set_sp_reg m t s 〈sph:〈xF,xF〉〉)
- (λs_tmp.Some ? (pairT ?? s_tmp cur_pc))]).
+ (λs_tmp.Some ? (pair ?? s_tmp cur_pc))]).
(* return from interrupt *)
definition execute_RTI ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
(* pop (CCR) *)
opt_map ?? (aux_pop m t s)
- (λS_and_CCR.match S_and_CCR with [ pairT s_tmp1 CCR_op ⇒
+ (λS_and_CCR.match S_and_CCR with [ pair s_tmp1 CCR_op ⇒
let s_tmp2 ≝ aux_set_CCR m t s_tmp1 CCR_op in
(* pop (A) *)
opt_map ?? (aux_pop m t s_tmp2)
- (λS_and_A.match S_and_A with [ pairT s_tmp3 A_op ⇒
+ (λS_and_A.match S_and_A with [ pair s_tmp3 A_op ⇒
let s_tmp4 ≝ set_acc_8_low_reg m t s_tmp3 A_op in
(* pop (X) *)
opt_map ?? (aux_pop m t s_tmp4)
- (λS_and_X.match S_and_X with [ pairT s_tmp5 X_op ⇒
+ (λS_and_X.match S_and_X with [ pair s_tmp5 X_op ⇒
opt_map ?? (set_indX_8_low_reg m t s_tmp5 X_op)
(* pop (PC high) *)
(λs_tmp6.opt_map ?? (aux_pop m t s_tmp6)
- (λS_and_PCH.match S_and_PCH with [ pairT s_tmp7 PCH_op ⇒
+ (λS_and_PCH.match S_and_PCH with [ pair s_tmp7 PCH_op ⇒
(* pop (PC low) *)
opt_map ?? (aux_pop m t s_tmp7)
- (λS_and_PCL.match S_and_PCL with [ pairT s_tmp8 PCL_op ⇒
- Some ? (pairT ?? s_tmp8 〈PCH_op:PCL_op〉)])]))])])]).
+ (λS_and_PCL.match S_and_PCL with [ pair s_tmp8 PCL_op ⇒
+ Some ? (pair ?? s_tmp8 〈PCH_op:PCL_op〉)])]))])])]).
(* return from subroutine *)
(* HC05/HC08/HCS08 si appoggia allo stack, RS08 si appoggia a SPC *)
let aux ≝
(* pop (PC high) *)
opt_map ?? (aux_pop m t s)
- (λS_and_PCH.match S_and_PCH with [ pairT s_tmp1 PCH_op ⇒
+ (λS_and_PCH.match S_and_PCH with [ pair s_tmp1 PCH_op ⇒
(* pop (PC low) *)
opt_map ?? (aux_pop m t s_tmp1)
- (λS_and_PCL.match S_and_PCL with [ pairT s_tmp2 PCL_op ⇒
- Some ? (pairT ?? s_tmp2 〈PCH_op:PCL_op〉)])])
+ (λS_and_PCL.match S_and_PCL with [ pair s_tmp2 PCL_op ⇒
+ Some ? (pair ?? s_tmp2 〈PCH_op:PCL_op〉)])])
in match m with
[ HC05 ⇒ aux | HC08 ⇒ aux | HCS08 ⇒ aux
| RS08 ⇒
(* new_pc = SPC *)
opt_map ?? (get_spc_reg m t s)
- (λSPC_op.Some ? (pairT ?? s SPC_op))
+ (λSPC_op.Some ? (pair ?? s SPC_op))
].
(* A = A - M - C *)
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
execute_SBC_SUB_aux m t s i cur_pc true
(λA_op.λM_op.λC_op.match plus_b8 A_op (compl_b8 M_op) false with
- [ pairT resb resc ⇒ match C_op with
+ [ pair resb resc ⇒ match C_op with
[ true ⇒ plus_b8 resb 〈xF,xF〉 resc
- | false ⇒ pairT ?? resb resc ]]).
+ | false ⇒ pair ?? resb resc ]]).
(* C = 1 *)
definition execute_SEC ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pairT ?? (set_c_flag m t s true) cur_pc).
+ Some ? (pair ?? (set_c_flag m t s true) cur_pc).
(* I = 1 *)
definition execute_SEI ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
opt_map ?? (set_i_flag m t s true)
- (λs_tmp.Some ? (pairT ?? s_tmp cur_pc)).
+ (λs_tmp.Some ? (pair ?? s_tmp cur_pc)).
(* swap SPCh,A *)
(* senso: nell'RS08 SPC non e' accessibile direttamente e come si possono
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
opt_map ?? (get_spc_reg m t s)
(λSPC_op.opt_map ?? (set_spc_reg m t s 〈(get_acc_8_low_reg m t s):(w16l SPC_op)〉)
- (λs_tmp1.Some ? (pairT ?? (set_acc_8_low_reg m t s_tmp1 (w16h SPC_op)) cur_pc))).
+ (λs_tmp1.Some ? (pair ?? (set_acc_8_low_reg m t s_tmp1 (w16h SPC_op)) cur_pc))).
(* swap SPCl,A *)
(* senso: nell'RS08 SPC non e' accessibile direttamente e come si possono
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
opt_map ?? (get_spc_reg m t s)
(λSPC_op.opt_map ?? (set_spc_reg m t s 〈(w16h SPC_op):(get_acc_8_low_reg m t s)〉)
- (λs_tmp1.Some ? (pairT ?? (set_acc_8_low_reg m t s_tmp1 (w16l SPC_op)) cur_pc))).
+ (λs_tmp1.Some ? (pair ?? (set_acc_8_low_reg m t s_tmp1 (w16l SPC_op)) cur_pc))).
(* M = A *)
definition execute_STA ≝
let A_op ≝ (get_acc_8_low_reg m t s) in
opt_map ?? (multi_mode_write true m t s cur_pc i A_op)
(λS_op_and_PC.match S_op_and_PC with
- [ pairT s_tmp1 new_pc ⇒
+ [ pair s_tmp1 new_pc ⇒
(* Z = nA7&nA6&nA5&nA4&nA3&nA2&nA1&nA0 *)
let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 A_op 〈x0,x0〉) in
(* N = A7 *)
(* V = 0 *)
let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
(* newpc = nextpc *)
- Some ? (pairT ?? s_tmp4 new_pc) ]).
+ Some ? (pair ?? s_tmp4 new_pc) ]).
(* M = H:X *)
definition execute_STHX ≝
opt_map ?? (get_indX_16_reg m t s)
(λX_op.opt_map ?? (multi_mode_write false m t s cur_pc i X_op)
(λS_op_and_PC.match S_op_and_PC with
- [ pairT s_tmp1 new_pc ⇒
+ [ pair s_tmp1 new_pc ⇒
(* Z = nR15&nR14&nR13nR12&nR11&nR10&nR9&nR8nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_w16 X_op 〈〈x0,x0〉:〈x0,x0〉〉) in
(* N = R15 *)
(* V = 0 *)
let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
(* newpc = nextpc *)
- Some ? (pairT ?? s_tmp4 new_pc) ])).
+ Some ? (pair ?? s_tmp4 new_pc) ])).
(* I = 0 *)
definition execute_STOP ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pairT ?? (setweak_i_flag m t s false) cur_pc).
+ Some ? (pair ?? (setweak_i_flag m t s false) cur_pc).
(* M = X *)
definition execute_STX ≝
opt_map ?? (get_indX_8_low_reg m t s)
(λX_op.opt_map ?? (multi_mode_write true m t s cur_pc i X_op)
(λS_op_and_PC.match S_op_and_PC with
- [ pairT s_tmp1 new_pc ⇒
+ [ pair s_tmp1 new_pc ⇒
(* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 X_op 〈x0,x0〉) in
(* N = R7 *)
(* V = 0 *)
let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
(* newpc = nextpc *)
- Some ? (pairT ?? s_tmp4 new_pc) ])).
+ Some ? (pair ?? s_tmp4 new_pc) ])).
(* A = A - M *)
definition execute_SUB ≝
(* load from vector low *)
(λaddrh.opt_map ?? (memory_filter_read m t s_tmp6 (succ_w16 vector))
(* newpc = [vector] *)
- (λaddrl.Some ? (pairT ?? s_tmp6 〈addrh:addrl〉)))))))))).
+ (λaddrl.Some ? (pair ?? s_tmp6 〈addrh:addrl〉)))))))))).
(* flags = A *)
definition execute_TAP ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pairT ?? (aux_set_CCR m t s (get_acc_8_low_reg m t s)) cur_pc).
+ Some ? (pair ?? (aux_set_CCR m t s (get_acc_8_low_reg m t s)) cur_pc).
(* X = A *)
definition execute_TAX ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
opt_map ?? (set_indX_8_low_reg m t s (get_acc_8_low_reg m t s))
- (λs_tmp.Some ? (pairT ?? s_tmp cur_pc)).
+ (λs_tmp.Some ? (pair ?? s_tmp cur_pc)).
(* A = flags *)
definition execute_TPA ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pairT ?? (set_acc_8_low_reg m t s (aux_get_CCR m t s)) cur_pc).
+ Some ? (pair ?? (set_acc_8_low_reg m t s (aux_get_CCR m t s)) cur_pc).
(* flags = M - 0 *)
(* implementata senza richiamare la sottrazione, la modifica dei flag
(* V = 0 *)
let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
(* newpc = nextpc *)
- Some ? (pairT ?? s_tmp4 new_pc) ]).
+ Some ? (pair ?? s_tmp4 new_pc) ]).
(* H:X = SP + 1 *)
definition execute_TSX ≝
opt_map ?? (get_sp_reg m t s )
(λSP_op.opt_map ?? (set_indX_16_reg m t s (succ_w16 SP_op))
(* H:X = SP + 1 *)
- (λs_tmp.Some ? (pairT ?? s_tmp cur_pc))).
+ (λs_tmp.Some ? (pair ?? s_tmp cur_pc))).
(* A = X *)
definition execute_TXA ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
opt_map ?? (get_indX_8_low_reg m t s)
- (λX_op.Some ? (pairT ?? (set_acc_8_low_reg m t s X_op) cur_pc)).
+ (λX_op.Some ? (pair ?? (set_acc_8_low_reg m t s X_op) cur_pc)).
(* SP = H:X - 1 *)
definition execute_TXS ≝
opt_map ?? (get_indX_16_reg m t s )
(λX_op.opt_map ?? (set_sp_reg m t s (pred_w16 X_op))
(* SP = H:X - 1 *)
- (λs_tmp.Some ? (pairT ?? s_tmp cur_pc))).
+ (λs_tmp.Some ? (pair ?? s_tmp cur_pc))).
(* I = 0 *)
definition execute_WAIT ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
- Some ? (pairT ?? (setweak_i_flag m t s false) cur_pc).
+ Some ? (pair ?? (setweak_i_flag m t s false) cur_pc).
(* **** *)
(* TICK *)
| Some status_and_newpc ⇒
(* aggiornamento centralizzato di pc e clk *)
match status_and_newpc with
- [ pairT s_tmp1 new_pc ⇒
+ [ pair s_tmp1 new_pc ⇒
let s_tmp2 ≝ set_pc_reg m t s_tmp1 new_pc in
let s_tmp3 ≝ set_clk_desc m t s_tmp2 (None ?) in
let abs_magic ≝ magic_of_opcode abs_pseudo in
projects / helm.git / commitdiff