From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 8 Feb 2008 11:50:42 +0000 (+0000)
Subject: prodT merged with prod
X-Git-Tag: make_still_working~5624
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=19b6e9b68fa0403461aff44e77a08e0e4eb84840;p=helm.git
prodT merged with prod
fstT merged with fst
sndT merged with fst
---
diff --git a/helm/software/matita/library/freescale/byte8.ma b/helm/software/matita/library/freescale/byte8.ma
index fedc5a65a..9c39bdb14 100644
--- a/helm/software/matita/library/freescale/byte8.ma
+++ b/helm/software/matita/library/freescale/byte8.ma
@@ -80,20 +80,20 @@ definition xor_b8 â
(* operatore rotazione destra con carry *)
definition rcr_b8 â
λb:byte8.λc:bool.match rcr_ex (b8h b) c with
- [ pairT bh' c' â match rcr_ex (b8l b) c' with
- [ pairT bl' c'' â pairT ?? (mk_byte8 bh' bl') c'' ]].
+ [ pair bh' c' â match rcr_ex (b8l b) c' with
+ [ pair bl' c'' â pair ?? (mk_byte8 bh' bl') c'' ]].
(* operatore shift destro *)
definition shr_b8 â
λb:byte8.match rcr_ex (b8h b) false with
- [ pairT bh' c' â match rcr_ex (b8l b) c' with
- [ pairT bl' c'' â pairT ?? (mk_byte8 bh' bl') c'' ]].
+ [ pair bh' c' â match rcr_ex (b8l b) c' with
+ [ pair bl' c'' â pair ?? (mk_byte8 bh' bl') c'' ]].
(* operatore rotazione destra *)
definition ror_b8 â
λb:byte8.match rcr_ex (b8h b) false with
- [ pairT bh' c' â match rcr_ex (b8l b) c' with
- [ pairT bl' c'' â match c'' with
+ [ pair bh' c' â match rcr_ex (b8l b) c' with
+ [ pair bl' c'' â match c'' with
[ true â mk_byte8 (or_ex x8 bh') bl'
| false â mk_byte8 bh' bl' ]]].
@@ -106,20 +106,20 @@ let rec ror_b8_n (b:byte8) (n:nat) on n â
(* operatore rotazione sinistra con carry *)
definition rcl_b8 â
λb:byte8.λc:bool.match rcl_ex (b8l b) c with
- [ pairT bl' c' â match rcl_ex (b8h b) c' with
- [ pairT bh' c'' â pairT ?? (mk_byte8 bh' bl') c'' ]].
+ [ pair bl' c' â match rcl_ex (b8h b) c' with
+ [ pair bh' c'' â pair ?? (mk_byte8 bh' bl') c'' ]].
(* operatore shift sinistro *)
definition shl_b8 â
λb:byte8.match rcl_ex (b8l b) false with
- [ pairT bl' c' â match rcl_ex (b8h b) c' with
- [ pairT bh' c'' â pairT ?? (mk_byte8 bh' bl') c'' ]].
+ [ pair bl' c' â match rcl_ex (b8h b) c' with
+ [ pair bh' c'' â pair ?? (mk_byte8 bh' bl') c'' ]].
(* operatore rotazione sinistra *)
definition rol_b8 â
λb:byte8.match rcl_ex (b8l b) false with
- [ pairT bl' c' â match rcl_ex (b8h b) c' with
- [ pairT bh' c'' â match c'' with
+ [ pair bl' c' â match rcl_ex (b8h b) c' with
+ [ pair bh' c'' â match c'' with
[ true â mk_byte8 bh' (or_ex x1 bl')
| false â mk_byte8 bh' bl' ]]].
@@ -137,16 +137,16 @@ definition not_b8 â
definition plus_b8 â
λb1,b2:byte8.λc:bool.
match plus_ex (b8l b1) (b8l b2) c with
- [ pairT l c' â match plus_ex (b8h b1) (b8h b2) c' with
- [ pairT h c'' â pairT ?? (mk_byte8 h l) c'' ]].
+ [ pair l c' â match plus_ex (b8h b1) (b8h b2) c' with
+ [ pair h c'' â pair ?? (mk_byte8 h l) c'' ]].
(* operatore somma senza carry *)
definition plus_b8nc â
-λb1,b2:byte8.fstT ?? (plus_b8 b1 b2 false).
+λb1,b2:byte8.fst ?? (plus_b8 b1 b2 false).
(* operatore carry della somma *)
definition plus_b8c â
-λb1,b2:byte8.sndT ?? (plus_b8 b1 b2 false).
+λb1,b2:byte8.snd ?? (plus_b8 b1 b2 false).
(* operatore Most Significant Bit *)
definition MSB_b8 â λb:byte8.eq_ex x8 (and_ex x8 (b8h b)).
@@ -279,7 +279,7 @@ definition daa_b8 â
let X'' â match c with
[ true â plus_b8nc X' â©x6,x0âª
| false â X' ] in
- pairT ?? X'' c
+ pair ?? X'' c
(* [X:0x9A-0xFF] *)
(* c' = 1 *)
(* X' = [X:0x9A-0xFF]
@@ -290,7 +290,7 @@ definition daa_b8 â
[ true â X
| false â plus_b8nc X â©x0,x6⪠] in
let X'' â plus_b8nc X' â©x6,x0⪠in
- pairT ?? X'' true
+ pair ?? X'' true
].
(* iteratore sui byte *)
@@ -374,13 +374,13 @@ qed.
lemma plusb8_ok:
âb1,b2,c.
match plus_b8 b1 b2 c with
- [ pairT r c' â b1 + b2 + nat_of_bool c = nat_of_byte8 r + nat_of_bool c' * 256
+ [ pair r c' â b1 + b2 + nat_of_bool c = nat_of_byte8 r + nat_of_bool c' * 256
].
intros; elim daemon.
qed.
lemma plusb8_O_x:
- âb. plus_b8 (mk_byte8 x0 x0) b false = pairT ?? b false.
+ âb. plus_b8 (mk_byte8 x0 x0) b false = pair ?? b false.
intros;
elim b;
elim e;
diff --git a/helm/software/matita/library/freescale/exadecim.ma b/helm/software/matita/library/freescale/exadecim.ma
index 21a31c98e..f7afbdf6c 100644
--- a/helm/software/matita/library/freescale/exadecim.ma
+++ b/helm/software/matita/library/freescale/exadecim.ma
@@ -740,36 +740,36 @@ definition xor_ex â
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 â
@@ -789,36 +789,36 @@ let rec ror_ex_n (e:exadecim) (n:nat) on n â
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 â
@@ -850,593 +850,593 @@ definition plus_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 â
@@ -1637,7 +1637,7 @@ qed.
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.
@@ -1745,7 +1745,7 @@ lemma ok_succ_ex : âe:exadecim.
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;
@@ -1760,7 +1760,7 @@ qed.
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;
@@ -1776,7 +1776,7 @@ lemma ok_rcl_ex : âe:exadecim.âb:bool.
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;
@@ -1789,7 +1789,7 @@ qed.
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;
diff --git a/helm/software/matita/library/freescale/load_write.ma b/helm/software/matita/library/freescale/load_write.ma
index 7f743cd3e..9ed176129 100644
--- a/helm/software/matita/library/freescale/load_write.ma
+++ b/helm/software/matita/library/freescale/load_write.ma
@@ -97,7 +97,7 @@ match s with
accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr
*)
match in_range addr â©â©x0,x0âª:â©xC,x0âªâª â©â©x0,x0âª:â©xF,xFâªâª with
- [ true â fMEM mem chk (or_w16 (fstT ?? (shr_w16 (fstT ?? (shr_w16 â©psm:â©x0,x0âªâª))))
+ [ true â fMEM mem chk (or_w16 (fst ?? (shr_w16 (fst ?? (shr_w16 â©psm:â©x0,x0âªâª))))
(and_w16 addr â©â©x0,x0âª:â©x3,xFâªâª))
(*
accesso normale
@@ -195,7 +195,7 @@ match s with
accesso al paging: [00pp pppp ppxx xxxx] con p=PS x=addr
*)
match in_range addr â©â©x0,x0âª:â©xC,x0âªâª â©â©x0,x0âª:â©xF,xFâªâª with
- [ true â opt_map ?? (fMEM mem chk (or_w16 (fstT ?? (shr_w16 (fstT ?? (shr_w16 â©psm:â©x0,x0âªâª))))
+ [ true â opt_map ?? (fMEM mem chk (or_w16 (fst ?? (shr_w16 (fst ?? (shr_w16 â©psm:â©x0,x0âªâª))))
(and_w16 addr â©â©x0,x0âª:â©x3,xFâªâª)))
(λmem'.Some ? (mk_any_status RS08 t (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl) mem' chk clk))
(*
@@ -338,20 +338,20 @@ definition loadw_from â
definition writeb_to â
λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.λwriteb:byte8.
opt_map ?? (memory_filter_write m t s addr writeb)
- (λtmps.Some ? (pairT ?? tmps (filtered_plus_w16 m t s cur_pc fetched))).
+ (λtmps.Some ? (pair ?? tmps (filtered_plus_w16 m t s cur_pc fetched))).
(* scrittura bit su addr *)
definition writebit_to â
λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λsub:oct.λcur_pc:word16.λfetched:nat.λwriteb:bool.
opt_map ?? (memory_filter_write_bit m t s addr sub writeb)
- (λtmps.Some ? (pairT ?? tmps (filtered_plus_w16 m t s cur_pc fetched))).
+ (λtmps.Some ? (pair ?? tmps (filtered_plus_w16 m t s cur_pc fetched))).
(* scrittura word su addr *)
definition writew_to â
λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.λwritew:word16.
opt_map ?? (memory_filter_write m t s addr (w16h writew))
(λtmps.opt_map ?? (memory_filter_write m t s (succ_w16 addr) (w16l writew))
- (λtmps'.Some ? (pairT ?? tmps' (filtered_plus_w16 m t s cur_pc fetched)))).
+ (λtmps'.Some ? (pair ?? tmps' (filtered_plus_w16 m t s cur_pc fetched)))).
(* ausiliari per definire i tipi e la lettura/scrittura *)
@@ -371,7 +371,7 @@ definition aux_write_typing â
λm:mcu_type.λt:memory_impl.λbyteflag:bool.
any_status m t â word16 â word16 â nat â
match byteflag with [ true â byte8 | false â word16 ] â
- option (ProdT (any_status m t) word16).
+ option (Prod (any_status m t) word16).
(* per non dover ramificare i vari load in byte/word *)
definition aux_write â
@@ -744,19 +744,19 @@ definition multi_mode_write â
λbyteflag:bool.λm:mcu_type.λt:memory_impl.match byteflag
return λbyteflag:bool.any_status m t â word16 â instr_mode â
match byteflag with [ true â byte8 | false â word16 ] â
- option (ProdT (any_status m t) word16) with
+ option (Prod (any_status m t) word16) with
(* scrittura di un byte *)
[ true â λs:any_status m t.λcur_pc:word16.λi:instr_mode.λwriteb:byte8.match i with
(* NO: non ci sono indicazioni *)
[ MODE_INH â None ?
(* scrive A *)
- | MODE_INHA â Some ? (pairT ?? (set_acc_8_low_reg m t s writeb) cur_pc)
+ | MODE_INHA â Some ? (pair ?? (set_acc_8_low_reg m t s writeb) cur_pc)
(* scrive X *)
| MODE_INHX â opt_map ?? (set_indX_8_low_reg m t s writeb)
- (λtmps.Some ? (pairT ?? tmps cur_pc))
+ (λtmps.Some ? (pair ?? tmps cur_pc))
(* scrive H *)
| MODE_INHH â opt_map ?? (set_indX_8_high_reg m t s writeb)
- (λtmps.Some ? (pairT ?? tmps cur_pc))
+ (λtmps.Some ? (pair ?? tmps cur_pc))
(* NO: solo lettura byte *)
| MODE_IMM1 â None ?
@@ -783,22 +783,22 @@ definition multi_mode_write â
| MODE_IMM1_to_DIR1 â mode_DIR1_write true m t s cur_pc writeb
(* passo2: scrittura su DIR1 e X++, passo1: lettura da IX0 *)
| MODE_IX0p_to_DIR1 â opt_map ?? (mode_DIR1_write true m t s cur_pc writeb)
- (λS_and_PC.match S_and_PC with [ pairT S_op PC_op â
+ (λS_and_PC.match S_and_PC with [ pair S_op PC_op â
(* H:X++ *)
opt_map ?? (aux_inc_indX_16 m t S_op)
- (λS_op'.Some ? (pairT ?? S_op' PC_op))])
+ (λS_op'.Some ? (pair ?? S_op' PC_op))])
(* passo2: scrittura su IX0 e X++, passo1: lettura da DIR1 *)
| MODE_DIR1_to_IX0p â opt_map ?? (mode_IX0_write true m t s cur_pc writeb)
- (λS_and_PC.match S_and_PC with [ pairT S_op PC_op â
+ (λS_and_PC.match S_and_PC with [ pair S_op PC_op â
(* H:X++ *)
opt_map ?? (aux_inc_indX_16 m t S_op)
- (λS_op'.Some ? (pairT ?? S_op' PC_op))])
+ (λS_op'.Some ? (pair ?? S_op' PC_op))])
(* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = INHA *)
- | MODE_INHA_and_IMM1 â Some ? (pairT ?? (set_acc_8_low_reg m t s writeb) cur_pc)
+ | MODE_INHA_and_IMM1 â Some ? (pair ?? (set_acc_8_low_reg m t s writeb) cur_pc)
(* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = INHX *)
| MODE_INHX_and_IMM1 â opt_map ?? (set_indX_8_low_reg m t s writeb)
- (λtmps.Some ? (pairT ?? tmps cur_pc))
+ (λtmps.Some ? (pair ?? tmps cur_pc))
(* NO: solo lettura word *)
| MODE_IMM1_and_IMM1 â None ?
(* dopo aver prelevato 2 byte la possibilita' modificare Io argomento = DIR1 *)
@@ -820,10 +820,10 @@ definition multi_mode_write â
| MODE_DIRn_and_IMM1 _ â None ?
(* scrive 1 byte su 0000 0000 0000 xxxxb *)
| MODE_TNY e â opt_map ?? (memory_filter_write m t s â©â©x0,x0âª:â©x0,eâªâª writeb)
- (λtmps.Some ? (pairT ?? tmps cur_pc))
+ (λtmps.Some ? (pair ?? tmps cur_pc))
(* scrive 1 byte su 0000 0000 000x xxxxb *)
| MODE_SRT e â opt_map ?? (memory_filter_write m t s â©â©x0,x0âª:(byte8_of_bitrigesim e)⪠writeb)
- (λtmps.Some ? (pairT ?? tmps cur_pc)) ]
+ (λtmps.Some ? (pair ?? tmps cur_pc)) ]
(* scrittura di una word *)
| false â λs:any_status m t.λcur_pc:word16.λi:instr_mode.λwritew:word16.match i with
(* NO: non ci sono indicazioni *)
diff --git a/helm/software/matita/library/freescale/medium_tests.ma b/helm/software/matita/library/freescale/medium_tests.ma
index 41cc96ae9..91e185b6f 100644
--- a/helm/software/matita/library/freescale/medium_tests.ma
+++ b/helm/software/matita/library/freescale/medium_tests.ma
@@ -195,7 +195,7 @@ lemma dTest_HCS08_sReverse_aux â
| TickOK s â Some ? (set_mem_desc HCS08 t s (load_from_source_at t (get_mem_desc HCS08 t s) dTest_bytes â©â©x0,xDâª:â©x0,x0âªâª))
] =
Some ? (set_pc_reg HCS08 t
- (dTest_HCS08_sReverse_status t (fstT ?? (shr_w16 (byte8_strlen string))) (byte8_strlen string) (byte8_reverse string))
+ (dTest_HCS08_sReverse_status t (fst ?? (shr_w16 (byte8_strlen string))) (byte8_strlen string) (byte8_reverse string))
(mk_word16 (mk_byte8 x1 x9) (mk_byte8 x2 xB)))).
(* dimostrazione senza svolgimento degli stati *)
diff --git a/helm/software/matita/library/freescale/multivm.ma b/helm/software/matita/library/freescale/multivm.ma
index 35e8328cb..7088fc1c2 100644
--- a/helm/software/matita/library/freescale/multivm.ma
+++ b/helm/software/matita/library/freescale/multivm.ma
@@ -47,13 +47,13 @@ include "freescale/load_write.ma".
(* 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 *)
@@ -69,7 +69,7 @@ definition execute_ADC_ADD_aux â
(* 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 *)
@@ -90,21 +90,21 @@ definition execute_AND_BIT_EOR_ORA_aux â
(* 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 *)
@@ -114,7 +114,7 @@ definition execute_ASL_ASR_LSR_ROL_ROR_aux â
(* 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 â
@@ -135,9 +135,9 @@ definition execute_any_BRANCH â
(* 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 *)
@@ -147,7 +147,7 @@ definition execute_BCLRn_BSETn_aux â
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 *)
@@ -160,9 +160,9 @@ definition execute_BRCLRn_BRSETn_aux â
(* 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/++/-- *)
@@ -176,7 +176,7 @@ definition execute_COM_DEC_INC_NEG_aux â
(* 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 *)
@@ -186,20 +186,20 @@ definition execute_COM_DEC_INC_NEG_aux â
(* 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
@@ -212,7 +212,7 @@ definition execute_SBC_SUB_aux â
(* 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 â
@@ -234,7 +234,7 @@ definition aux_pop â
(λ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
@@ -291,7 +291,7 @@ definition execute_AIS â
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 â
@@ -302,7 +302,7 @@ 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 â
@@ -349,7 +349,7 @@ definition execute_BGE â
(* 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 â
@@ -479,14 +479,14 @@ definition execute_BSR â
(* 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 *)
@@ -500,9 +500,9 @@ definition execute_CBEQA â
(* 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 *)
@@ -517,21 +517,21 @@ definition execute_CBEQX â
(* 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 â
@@ -539,7 +539,7 @@ 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 *)
@@ -547,7 +547,7 @@ definition execute_CLR â
(* 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 â
@@ -572,7 +572,7 @@ definition execute_CPHX â
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
@@ -583,7 +583,7 @@ definition execute_CPHX â
(* 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 â
@@ -594,7 +594,7 @@ 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
@@ -605,7 +605,7 @@ definition execute_CPX â
(* 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) *)
@@ -615,7 +615,7 @@ definition execute_DAA â
(λ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 *)
@@ -627,7 +627,7 @@ definition execute_DAA â
(* 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 â
@@ -641,13 +641,13 @@ 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 â
@@ -679,7 +679,7 @@ definition execute_DIV â
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 â
@@ -701,7 +701,7 @@ definition execute_JMP â
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 *)
@@ -715,14 +715,14 @@ definition execute_JSR â
(* 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 *)
@@ -740,7 +740,7 @@ definition execute_LDA â
(* 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 â
@@ -757,7 +757,7 @@ 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 â
@@ -774,7 +774,7 @@ 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 â
@@ -791,7 +791,7 @@ definition execute_MOV â
(* 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 *)
@@ -799,7 +799,7 @@ definition execute_MOV â
(* 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 â
@@ -807,7 +807,7 @@ 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 â
@@ -821,7 +821,7 @@ 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 *)
@@ -829,7 +829,7 @@ definition execute_NSA â
λ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 â
@@ -840,44 +840,44 @@ 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 â
@@ -896,30 +896,30 @@ definition execute_RSP â
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 *)
@@ -928,17 +928,17 @@ definition execute_RTS â
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 *)
@@ -946,20 +946,20 @@ definition execute_SBC â
λ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
@@ -969,7 +969,7 @@ definition execute_SHA â
λ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
@@ -979,7 +979,7 @@ definition execute_SLA â
λ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 â
@@ -988,7 +988,7 @@ 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 *)
@@ -996,7 +996,7 @@ definition execute_STA â
(* 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 â
@@ -1005,7 +1005,7 @@ 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 *)
@@ -1013,12 +1013,12 @@ definition execute_STHX â
(* 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 â
@@ -1027,7 +1027,7 @@ 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 *)
@@ -1035,7 +1035,7 @@ definition execute_STX â
(* 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 â
@@ -1065,23 +1065,23 @@ definition execute_SWI â
(* 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
@@ -1098,7 +1098,7 @@ definition execute_TST â
(* 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 â
@@ -1106,13 +1106,13 @@ 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 â
@@ -1120,12 +1120,12 @@ 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 *)
@@ -1259,7 +1259,7 @@ definition tick_execute â
| 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
diff --git a/helm/software/matita/library/freescale/word16.ma b/helm/software/matita/library/freescale/word16.ma
index 9a260b10e..b1448b985 100644
--- a/helm/software/matita/library/freescale/word16.ma
+++ b/helm/software/matita/library/freescale/word16.ma
@@ -80,20 +80,20 @@ definition xor_w16 â
(* operatore rotazione destra con carry *)
definition rcr_w16 â
λw:word16.λc:bool.match rcr_b8 (w16h w) c with
- [ pairT wh' c' â match rcr_b8 (w16l w) c' with
- [ pairT wl' c'' â pairT ?? (mk_word16 wh' wl') c'' ]].
+ [ pair wh' c' â match rcr_b8 (w16l w) c' with
+ [ pair wl' c'' â pair ?? (mk_word16 wh' wl') c'' ]].
(* operatore shift destro *)
definition shr_w16 â
λw:word16.match rcr_b8 (w16h w) false with
- [ pairT wh' c' â match rcr_b8 (w16l w) c' with
- [ pairT wl' c'' â pairT ?? (mk_word16 wh' wl') c'' ]].
+ [ pair wh' c' â match rcr_b8 (w16l w) c' with
+ [ pair wl' c'' â pair ?? (mk_word16 wh' wl') c'' ]].
(* operatore rotazione destra *)
definition ror_w16 â
λw:word16.match rcr_b8 (w16h w) false with
- [ pairT wh' c' â match rcr_b8 (w16l w) c' with
- [ pairT wl' c'' â match c'' with
+ [ pair wh' c' â match rcr_b8 (w16l w) c' with
+ [ pair wl' c'' â match c'' with
[ true â mk_word16 (or_b8 (mk_byte8 x8 x0) wh') wl'
| false â mk_word16 wh' wl' ]]].
@@ -106,20 +106,20 @@ let rec ror_w16_n (w:word16) (n:nat) on n â
(* operatore rotazione sinistra con carry *)
definition rcl_w16 â
λw:word16.λc:bool.match rcl_b8 (w16l w) c with
- [ pairT wl' c' â match rcl_b8 (w16h w) c' with
- [ pairT wh' c'' â pairT ?? (mk_word16 wh' wl') c'' ]].
+ [ pair wl' c' â match rcl_b8 (w16h w) c' with
+ [ pair wh' c'' â pair ?? (mk_word16 wh' wl') c'' ]].
(* operatore shift sinistro *)
definition shl_w16 â
λw:word16.match rcl_b8 (w16l w) false with
- [ pairT wl' c' â match rcl_b8 (w16h w) c' with
- [ pairT wh' c'' â pairT ?? (mk_word16 wh' wl') c'' ]].
+ [ pair wl' c' â match rcl_b8 (w16h w) c' with
+ [ pair wh' c'' â pair ?? (mk_word16 wh' wl') c'' ]].
(* operatore rotazione sinistra *)
definition rol_w16 â
λw:word16.match rcl_b8 (w16l w) false with
- [ pairT wl' c' â match rcl_b8 (w16h w) c' with
- [ pairT wh' c'' â match c'' with
+ [ pair wl' c' â match rcl_b8 (w16h w) c' with
+ [ pair wh' c'' â match c'' with
[ true â mk_word16 wh' (or_b8 (mk_byte8 x0 x1) wl')
| false â mk_word16 wh' wl' ]]].
@@ -137,16 +137,16 @@ definition not_w16 â
definition plus_w16 â
λw1,w2:word16.λc:bool.
match plus_b8 (w16l w1) (w16l w2) c with
- [ pairT l c' â match plus_b8 (w16h w1) (w16h w2) c' with
- [ pairT h c'' â pairT ?? (mk_word16 h l) c'' ]].
+ [ pair l c' â match plus_b8 (w16h w1) (w16h w2) c' with
+ [ pair h c'' â pair ?? (mk_word16 h l) c'' ]].
(* operatore somma senza carry *)
definition plus_w16nc â
-λw1,w2:word16.fstT ?? (plus_w16 w1 w2 false).
+λw1,w2:word16.fst ?? (plus_w16 w1 w2 false).
(* operatore carry della somma *)
definition plus_w16c â
-λw1,w2:word16.sndT ?? (plus_w16 w1 w2 false).
+λw1,w2:word16.snd ?? (plus_w16 w1 w2 false).
(* operatore Most Significant Bit *)
definition MSB_w16 â λw:word16.eq_ex x8 (and_ex x8 (b8h (w16h w))).
@@ -252,14 +252,14 @@ axiom eq_nat_of_word16_n_nat_of_word16_mod_n_65536:
lemma plusw16_ok:
âb1,b2,c.
match plus_w16 b1 b2 c with
- [ pairT r c' â b1 + b2 + nat_of_bool c = nat_of_word16 r + nat_of_bool c' * (256 * 256)
+ [ pair r c' â b1 + b2 + nat_of_bool c = nat_of_word16 r + nat_of_bool c' * (256 * 256)
].
intros; elim daemon.
qed.
(* TODO: dimostrare diversamente *)
axiom plusw16_O_x:
- âb. plus_w16 (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x0 x0)) b false = pairT ?? b false.
+ âb. plus_w16 (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x0 x0)) b false = pair ?? b false.
lemma plusw16nc_O_x:
âx. plus_w16nc (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x0 x0)) x = x.