(**************************************************************************)
(* ********************************************************************** *)
-(* Progetto FreeScale *)
+(* Progetto FreeScale *)
(* *)
-(* Sviluppato da: *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
(* *)
-(* Questo materiale fa parte della tesi: *)
-(* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
-(* *)
-(* data ultima modifica 15/11/2007 *)
(* ********************************************************************** *)
include "freescale/aux_bases.ma".
λbw1,bw2:byte8_or_word16.
match bw1 with
[ Byte b1 ⇒ match bw2 with [ Byte b2 ⇒ eq_b8 b1 b2 | Word _ ⇒ false ]
- | Word w1 ⇒ match bw2 with [ Byte _ ⇒ false | Word w2 ⇒ eq_w16 w1 w1 ]
+ | Word w1 ⇒ match bw2 with [ Byte _ ⇒ false | Word w2 ⇒ eq_w16 w1 w2 ]
].