(* data ultima modifica 15/11/2007 *)
(* ********************************************************************** *)
(* data ultima modifica 15/11/2007 *)
(* ********************************************************************** *)
- [ 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'' ]].
- [ 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'' ]].
- [ 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'' ]].
- [ 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'' ]].
- [ 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'' ]].
[ true ⇒ X
| false ⇒ plus_b8nc X 〈x0,x6〉 ] in
let X'' ≝ plus_b8nc X' 〈x6,x0〉 in
[ true ⇒ X
| false ⇒ plus_b8nc X 〈x0,x6〉 ] in
let X'' ≝ plus_b8nc X' 〈x6,x0〉 in