set "baseuri" "cic:/matita/assembly/exadecimal/".
-include "extra.ma".
+include "assembly/extra.ma".
inductive exadecimal : Type ≝
x0: exadecimal
elim b;
simplify;
[
- |*: alias id "lt_S_S" = "cic:/matita/algebra/finite_groups/lt_S_S.con".
- repeat (apply lt_S_S)
+ |*: repeat (apply lt_to_lt_S_S)
];
autobatch.
qed.
change in ⊢ (? ? ? (? (? % ?))) with (n16 \mod 16);
rewrite < mod_mod;
[ apply H;
- autobatch
+ unfold lt;
+ autobatch.
| autobatch
]
qed.
]
qed.
+lemma exadecimal_of_nat_nat_of_exadecimal:
+ ∀b.exadecimal_of_nat (nat_of_exadecimal b) = b.
+ intro;
+ elim b;
+ reflexivity.
+qed.
+
lemma plusex_ok:
∀b1,b2,c.
match plusex b1 b2 c with
[ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_exadecimal r + nat_of_bool c' * 16 ].
intros;
- elim c;
- elim b1;
- elim b2;
- normalize;
- reflexivity.
+ elim b1; (elim b2; (elim c; normalize; reflexivity)).
qed.
definition xpred ≝
first [ reflexivity | destruct H ].
qed.
+lemma eqex_false_to_not_eq: ∀b,b'. eqex b b' = false → b ≠ b'.
+ intros 2;
+ elim b 0;
+ elim b' 0;
+ simplify;
+ intro;
+ try (destruct H);
+ intro K;
+ destruct K.
+qed.
+
(*
lemma xpred_S: ∀b. xpred (exadecimal_of_nat (S b)) = exadecimal_of_nat b.
intros;
rewrite > exadecimal_of_nat_mod;
rewrite > exadecimal_of_nat_mod in ⊢ (? ? ? %);
-*)
\ No newline at end of file
+*)