(* \langle \rangle *)
notation "〈x,y〉" non associative with precedence 80
for @{ 'mk_byte8 $x $y }.
-interpretation "mk_byte8" 'mk_byte8 x y =
- (cic:/matita/freescale/byte8/byte8.ind#xpointer(1/1/1) x y).
+interpretation "mk_byte8" 'mk_byte8 x y = (mk_byte8 x y).
(* operatore = *)
definition eq_b8 ≝ λb1,b2:byte8.(eq_ex (b8h b1) (b8h b2)) ⊗ (eq_ex (b8l b1) (b8l b2)).
(* byte → naturali *)
definition nat_of_byte8 ≝ λb:byte8.16*(b8h b) + (b8l b).
-coercion cic:/matita/freescale/byte8/nat_of_byte8.con.
+coercion nat_of_byte8.
(* naturali → byte *)
definition byte8_of_nat ≝ λn.mk_byte8 (exadecim_of_nat (n/16)) (exadecim_of_nat n).
rewrite > mod_plus in ⊢ (? ? % ?);
rewrite > mod_plus in ⊢ (? ? ? %);
apply eq_mod_to_eq_plus_mod;
- rewrite < mod_mod in ⊢ (? ? ? %); [ | autobatch];
- rewrite < mod_mod in ⊢ (? ? % ?); [ | autobatch];
+ rewrite < mod_mod in ⊢ (? ? ? %); [ | autobatch by divides_n_n];
+ rewrite < mod_mod in ⊢ (? ? % ?); [ | autobatch by divides_n_n];
rewrite < (eq_mod_times_times_mod ? ? 16 256) in ⊢ (? ? (? % ?) ?); [2: reflexivity | ];
rewrite < mod_mod in ⊢ (? ? % ?);
[ reflexivity
- | autobatch
+ | autobatch by divides_n_n
].
qed.
generalize in match (plusb8_ok b1 b2 false);
elim (plus_b8 b1 b2 false);
simplify in H ⊢ %;
- change with (nat_of_byte8 t = (b1 + b2) \mod 256);
+ change with (nat_of_byte8 a = (b1 + b2) \mod 256);
rewrite < plus_n_O in H;
rewrite > H; clear H;
rewrite > mod_plus;
- letin K ≝ (eq_nat_of_byte8_mod t); clearbody K;
- letin K' ≝ (eq_mod_times_n_m_m_O (nat_of_bool t1) 256 ?); clearbody K';
- [ autobatch | ];
- autobatch paramodulation.
+ letin K ≝ (eq_nat_of_byte8_mod a); clearbody K;
+ letin K' ≝ (eq_mod_times_n_m_m_O (nat_of_bool b) 256 ?); clearbody K';
+ [ unfold;apply le_S_S;apply le_O_n| ];
+ rewrite > K' in ⊢ (? ? ? (? (? ? %) ?));
+ rewrite < K in ⊢ (? ? ? (? (? % ?) ?));
+ rewrite < plus_n_O;
+ apply K;
qed.
lemma eq_eqb8_x0_x0_byte8_of_nat_S_false:
| unfold eq_b8;
change in ⊢ (? ? (? % ?) ?) with (eq_ex x0 (exadecim_of_nat (S b/16)));
letin K ≝ (leq_m_n_to_eq_div_n_m_S (S b) 16 ? ?);
- [ autobatch
+ [ unfold; autobatch by le_S_S,le_O_n;
| unfold in H1;
apply le_S_S;
assumption
unfold lt in H;
rewrite < H2;
clear H2; clear a; clear H1; clear Hcut;
- apply (le_times_to_le 16) [ autobatch | ] ;
- rewrite > (div_mod (S b) 16) in H;[2:autobatch|]
- rewrite > (div_mod 255 16) in H:(? ? %);[2:autobatch|]
+ apply (le_times_to_le 16) [ autobatch by le_S_S,le_O_n;| ] ;
+ rewrite > (div_mod (S b) 16) in H;[2:unfold; autobatch by le_S_S,le_O_n;|]
+ rewrite > (div_mod 255 16) in H:(? ? %);[2:unfold; autobatch by le_S_S,le_O_n;|]
lapply (le_to_le_plus_to_le ? ? ? ? ? H);
[apply lt_S_to_le;
- apply lt_mod_m_m;autobatch
+ apply lt_mod_m_m; unfold; apply le_S_S; apply le_O_n;
|rewrite > sym_times;
rewrite > sym_times in ⊢ (? ? %);
normalize in ⊢ (? ? %);apply Hletin;
rewrite > nat_of_exadecim_exadecim_of_nat in Hletin1;
elim (eq_mod_O_to_exists ? ? Hletin1); clear Hletin1;
rewrite > H1;
- rewrite > lt_O_to_div_times; [2: autobatch | ]
+ rewrite > lt_O_to_div_times; [2: unfold; apply le_S_S; apply le_O_n; | ]
lapply (eq_f ? ? (λx.x/16) ? ? H1);
- rewrite > lt_O_to_div_times in Hletin; [2: autobatch | ]
+ rewrite > lt_O_to_div_times in Hletin; [2: unfold; apply le_S_S; apply le_O_n; | ]
lapply (eq_f ? ? (λx.x \mod 16) ? ? H1);
rewrite > eq_mod_times_n_m_m_O in Hletin1;
elim daemon
rewrite > eq_nat_of_byte8_n_nat_of_byte8_mod_n_256 in ⊢ (? ? ? %);
rewrite > mod_plus in ⊢ (? ? (? %) ?);
rewrite > mod_plus in ⊢ (? ? ? (? %));
- rewrite < mod_mod in ⊢ (? ? (? (? (? % ?) ?)) ?); [2: autobatch | ];
+ rewrite < mod_mod in ⊢ (? ? (? (? (? % ?) ?)) ?); [2: apply divides_n_n; | ];
rewrite > sym_plus in ⊢ (? ? (? (? % ?)) ?);
reflexivity.
qed.