- #t;
- napply (eq_to_eqanystatus_weak [ 〈〈x0,x0〉:〈x7,x0〉〉 ; 〈〈x0,x0〉:〈x7,x1〉〉 ; 〈〈x0,x0〉:〈x7,x2〉〉 ] HCS08 t
- (match execute HCS08 t (TickOK ? (mTest_HCS08_CBEQ_DBNZ_status t 〈x0,x0〉 〈x0,x1〉 〈x0,x2〉)) nat68
- with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ])
- (set_acc_8_low_reg HCS08 t (* nuovo A *)
- (set_pc_reg HCS08 t (* nuovo PC *)
- (setweak_indX_16_reg HCS08 t (mTest_HCS08_CBEQ_DBNZ_status t 〈xF,xE〉 〈x0,x1〉 〈x0,x0〉) (* nuovo H:X *)
- (mk_word16 〈x0,x0〉 〈x7,x0〉))
- (mk_word16 〈x1,x8〉 〈x8,xE〉))
- (mk_byte8 xF xF)));
- nelim t;
- nnormalize in ⊢ (? ? ? %);
- napply refl_eq.
+ #t;
+
+ (* nelim t; napply refl_eq; *)
+ (* cosi' in 7sec fa tutto *)
+
+ napply (eq_to_eqanystatus_weak [ 〈〈x0,x0〉:〈x7,x0〉〉 ; 〈〈x0,x0〉:〈x7,x1〉〉 ; 〈〈x0,x0〉:〈x7,x2〉〉 ] HCS08 t …);
+ ##[ ##3: (* ram *)
+ nelim t;
+ nnormalize in ⊢ (? ? % ?);
+ napply refl_eq;
+ (* 10sec con normalize, leggermente di piu' senza *)
+ ##| ##2: (* descrittore *)
+ nelim t;
+ nnormalize in ⊢ (? ? ? %);
+ nnormalize in ⊢ (? ? % ?);
+ napply refl_eq;
+ (* 7sec con normalize, leggermente di piu' senza il secondo normalize,
+ non termina senza il primo *)
+ ##| ##1: (* alu *)
+ nelim t;
+ (* senza questo normalize non va nulla *)
+ ##[ ##2,3: nnormalize in ⊢ (? ? ? %);
+ napply refl_eq;
+ ##| ##1: (* in questo punto si vede benissimo come stato1 = stato2 esplode
+ mentre la trasformazione eq_stato s1 s2 = true computa benissimo *)
+ (* un napply refl_eq diretto non ci riesce proprio... *)
+ napply (eqaluHC08_to_eq
+ (alu HCS08 MEM_FUNC (match execute HCS08 MEM_FUNC (TickOK ? (mTest_HCS08_CBEQ_DBNZ_status MEM_FUNC 〈x0,x0〉 〈x0,x1〉 〈x0,x2〉)) nat68 with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ]))
+ (alu HCS08 MEM_FUNC (set_acc_8_low_reg HCS08 MEM_FUNC (* nuovo A *)
+ (set_pc_reg HCS08 MEM_FUNC (* nuovo PC *)
+ (setweak_indX_16_reg HCS08 MEM_FUNC (mTest_HCS08_CBEQ_DBNZ_status MEM_FUNC 〈xF,xE〉 〈x0,x1〉 〈x0,x0〉) (* nuovo H:X *)
+ (mk_word16 〈x0,x0〉 〈x7,x0〉)) (mk_word16 〈x1,x8〉 〈x8,xE〉)) (mk_byte8 xF xF)))
+ ?);
+ nnormalize in ⊢ (? ? % ?);
+ napply refl_eq;
+ ##]
+ ##]
+(* pero' ora si e' inceppato nqed... *)