From 19b6e9b68fa0403461aff44e77a08e0e4eb84840 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 8 Feb 2008 11:50:42 +0000 Subject: [PATCH] prodT merged with prod fstT merged with fst sndT merged with fst --- .../matita/library/freescale/byte8.ma | 40 +- .../matita/library/freescale/exadecim.ma | 1134 ++++++++--------- .../matita/library/freescale/load_write.ma | 36 +- .../matita/library/freescale/medium_tests.ma | 2 +- .../matita/library/freescale/multivm.ma | 192 +-- .../matita/library/freescale/word16.ma | 36 +- 6 files changed, 720 insertions(+), 720 deletions(-) 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. -- 2.39.2