11) ngeneralize bug di unificazione: ngeneralize in match (x1 = x2)
12) generazione dei nomi non va:
include "freescale/byte8.ma".
nlemma test: ∀b1,b2,b3.
plus_b8_d_d b1 (plus_b8_d_d b2 b3) = plus_b8_d_d (plus_b8_d_d b1 b2) b3.
#b1; #b2; #b3; ncases b1; ncases b2; ncases b3;
11) ngeneralize bug di unificazione: ngeneralize in match (x1 = x2)
12) generazione dei nomi non va:
include "freescale/byte8.ma".
nlemma test: ∀b1,b2,b3.
plus_b8_d_d b1 (plus_b8_d_d b2 b3) = plus_b8_d_d (plus_b8_d_d b1 b2) b3.
#b1; #b2; #b3; ncases b1; ncases b2; ncases b3;