mod change (-x)

[helm.git] / helm / software / matita / contribs / assembly / string / ascii_min.ma

diff --git a/helm/software/matita/contribs/assembly/string/ascii_min.ma b/helm/software/matita/contribs/assembly/string/ascii_min.ma
old mode 100755 (executable)
new mode 100644 (file)
index 8871397..b3a247a
--- a/helm/software/matita/contribs/assembly/string/ascii_min.ma
+++ b/helm/software/matita/contribs/assembly/string/ascii_min.ma
@@ -175,3 +175,97 @@ definition magic_of_ascii_min ≝
 (* confronto fra ascii_min *)
 definition eqAsciiMin ≝
 λc,c':ascii_min.(eq_b8 (magic_of_ascii_min c) (magic_of_ascii_min c')).
+
+lemma eq_to_eqasciimin : ∀a1,a2.a1 = a2 → eqAsciiMin a1 a2 = true.
+ do 3 intro;
+ unfold eqAsciiMin;
+ rewrite > H;
+ elim a2;
+ reflexivity.
+qed.
+
+(* 63^2 casi... *)
+lemma eqasciimin_to_eq_00 : ∀a.eqAsciiMin ch_0 a = true → ch_0 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_01 : ∀a.eqAsciiMin ch_1 a = true → ch_1 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_02 : ∀a.eqAsciiMin ch_2 a = true → ch_2 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_03 : ∀a.eqAsciiMin ch_3 a = true → ch_3 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_04 : ∀a.eqAsciiMin ch_4 a = true → ch_4 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_05 : ∀a.eqAsciiMin ch_5 a = true → ch_5 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_06 : ∀a.eqAsciiMin ch_6 a = true → ch_6 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_07 : ∀a.eqAsciiMin ch_7 a = true → ch_7 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_08 : ∀a.eqAsciiMin ch_8 a = true → ch_8 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_09 : ∀a.eqAsciiMin ch_9 a = true → ch_9 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_10 : ∀a.eqAsciiMin ch__ a = true → ch__ = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_11 : ∀a.eqAsciiMin ch_A a = true → ch_A = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_12 : ∀a.eqAsciiMin ch_B a = true → ch_B = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_13 : ∀a.eqAsciiMin ch_C a = true → ch_C = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_14 : ∀a.eqAsciiMin ch_D a = true → ch_D = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_15 : ∀a.eqAsciiMin ch_E a = true → ch_E = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_16 : ∀a.eqAsciiMin ch_F a = true → ch_F = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_17 : ∀a.eqAsciiMin ch_G a = true → ch_G = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_18 : ∀a.eqAsciiMin ch_H a = true → ch_H = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_19 : ∀a.eqAsciiMin ch_I a = true → ch_I = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_20 : ∀a.eqAsciiMin ch_J a = true → ch_J = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_21 : ∀a.eqAsciiMin ch_K a = true → ch_K = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_22 : ∀a.eqAsciiMin ch_L a = true → ch_L = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_23 : ∀a.eqAsciiMin ch_M a = true → ch_M = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_24 : ∀a.eqAsciiMin ch_N a = true → ch_N = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_25 : ∀a.eqAsciiMin ch_O a = true → ch_O = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_26 : ∀a.eqAsciiMin ch_P a = true → ch_P = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_27 : ∀a.eqAsciiMin ch_Q a = true → ch_Q = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_28 : ∀a.eqAsciiMin ch_R a = true → ch_R = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_29 : ∀a.eqAsciiMin ch_S a = true → ch_S = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_30 : ∀a.eqAsciiMin ch_T a = true → ch_T = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_31 : ∀a.eqAsciiMin ch_U a = true → ch_U = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_32 : ∀a.eqAsciiMin ch_V a = true → ch_V = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_33 : ∀a.eqAsciiMin ch_W a = true → ch_W = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_34 : ∀a.eqAsciiMin ch_X a = true → ch_X = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_35 : ∀a.eqAsciiMin ch_Y a = true → ch_Y = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_36 : ∀a.eqAsciiMin ch_Z a = true → ch_Z = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_37 : ∀a.eqAsciiMin ch_a a = true → ch_a = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_38 : ∀a.eqAsciiMin ch_b a = true → ch_b = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_39 : ∀a.eqAsciiMin ch_c a = true → ch_c = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_40 : ∀a.eqAsciiMin ch_d a = true → ch_d = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_41 : ∀a.eqAsciiMin ch_e a = true → ch_e = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_42 : ∀a.eqAsciiMin ch_f a = true → ch_f = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_43 : ∀a.eqAsciiMin ch_g a = true → ch_g = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_44 : ∀a.eqAsciiMin ch_h a = true → ch_h = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_45 : ∀a.eqAsciiMin ch_i a = true → ch_i = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_46 : ∀a.eqAsciiMin ch_j a = true → ch_j = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_47 : ∀a.eqAsciiMin ch_k a = true → ch_k = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_48 : ∀a.eqAsciiMin ch_l a = true → ch_l = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_49 : ∀a.eqAsciiMin ch_m a = true → ch_m = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_50 : ∀a.eqAsciiMin ch_n a = true → ch_n = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_51 : ∀a.eqAsciiMin ch_o a = true → ch_o = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_52 : ∀a.eqAsciiMin ch_p a = true → ch_p = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_53 : ∀a.eqAsciiMin ch_q a = true → ch_q = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_54 : ∀a.eqAsciiMin ch_r a = true → ch_r = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_55 : ∀a.eqAsciiMin ch_s a = true → ch_s = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_56 : ∀a.eqAsciiMin ch_t a = true → ch_t = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_57 : ∀a.eqAsciiMin ch_u a = true → ch_u = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_58 : ∀a.eqAsciiMin ch_v a = true → ch_v = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_59 : ∀a.eqAsciiMin ch_w a = true → ch_w = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_60 : ∀a.eqAsciiMin ch_x a = true → ch_x = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_61 : ∀a.eqAsciiMin ch_y a = true → ch_y = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+lemma eqasciimin_to_eq_62 : ∀a.eqAsciiMin ch_z a = true → ch_z = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
+
+lemma eqasciimin_to_eq : ∀a1.∀a2.eqAsciiMin a1 a2 = true → a1 = a2.
+ do 1 intro;
+ elim a1 0;
+ [  1: apply eqasciimin_to_eq_00 |  2: apply eqasciimin_to_eq_01 |  3: apply eqasciimin_to_eq_02 |  4: apply eqasciimin_to_eq_03
+ |  5: apply eqasciimin_to_eq_04 |  6: apply eqasciimin_to_eq_05 |  7: apply eqasciimin_to_eq_06 |  8: apply eqasciimin_to_eq_07
+ |  9: apply eqasciimin_to_eq_08 | 10: apply eqasciimin_to_eq_09 | 11: apply eqasciimin_to_eq_10 | 12: apply eqasciimin_to_eq_11
+ | 13: apply eqasciimin_to_eq_12 | 14: apply eqasciimin_to_eq_13 | 15: apply eqasciimin_to_eq_14 | 16: apply eqasciimin_to_eq_15
+ | 17: apply eqasciimin_to_eq_16 | 18: apply eqasciimin_to_eq_17 | 19: apply eqasciimin_to_eq_18 | 20: apply eqasciimin_to_eq_19
+ | 21: apply eqasciimin_to_eq_20 | 22: apply eqasciimin_to_eq_21 | 23: apply eqasciimin_to_eq_22 | 24: apply eqasciimin_to_eq_23
+ | 25: apply eqasciimin_to_eq_24 | 26: apply eqasciimin_to_eq_25 | 27: apply eqasciimin_to_eq_26 | 28: apply eqasciimin_to_eq_27
+ | 29: apply eqasciimin_to_eq_28 | 30: apply eqasciimin_to_eq_29 | 31: apply eqasciimin_to_eq_30 | 32: apply eqasciimin_to_eq_31
+ | 33: apply eqasciimin_to_eq_32 | 34: apply eqasciimin_to_eq_33 | 35: apply eqasciimin_to_eq_34 | 36: apply eqasciimin_to_eq_35
+ | 37: apply eqasciimin_to_eq_36 | 38: apply eqasciimin_to_eq_37 | 39: apply eqasciimin_to_eq_38 | 40: apply eqasciimin_to_eq_39
+ | 41: apply eqasciimin_to_eq_40 | 42: apply eqasciimin_to_eq_41 | 43: apply eqasciimin_to_eq_42 | 44: apply eqasciimin_to_eq_43
+ | 45: apply eqasciimin_to_eq_44 | 46: apply eqasciimin_to_eq_45 | 47: apply eqasciimin_to_eq_46 | 48: apply eqasciimin_to_eq_47
+ | 49: apply eqasciimin_to_eq_48 | 50: apply eqasciimin_to_eq_49 | 51: apply eqasciimin_to_eq_50 | 52: apply eqasciimin_to_eq_51
+ | 53: apply eqasciimin_to_eq_52 | 54: apply eqasciimin_to_eq_53 | 55: apply eqasciimin_to_eq_54 | 56: apply eqasciimin_to_eq_55
+ | 57: apply eqasciimin_to_eq_56 | 58: apply eqasciimin_to_eq_57 | 59: apply eqasciimin_to_eq_58 | 60: apply eqasciimin_to_eq_59
+ | 61: apply eqasciimin_to_eq_60 | 62: apply eqasciimin_to_eq_61 | 63: apply eqasciimin_to_eq_62 ].
+qed.