1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "character/class.ma".
17 (* CHARACTER CLASSES ********************************************************)
19 (* Arithmetics of classes P and T *******************************************)
22 (P i → ∃h. i = h * 3 + 1) ∧
23 (T i → ∃∃h,k. i = (h * 3 + 1) * 3 ^ (k + 1)).
24 #i @(nat_elim1 … i) -i #i #IH
27 [ #H destruct /2 width=2/
28 | #i0 #j0 #Hi0 #Hj0 #H destruct
29 elim (t_pos … Hi0) #i #H destruct
30 elim (p_pos … Hj0) #j #H destruct
31 elim (IH (i+1) ?) // #_ #H
32 elim (H Hi0) -H -Hi0 #hi #ki #H >H -H
33 elim (IH (j+1) ?) -IH // #H #_ -i
34 elim (H Hj0) -H -Hj0 #hj #H >H -j
35 <associative_plus >exp_n_m_plus_1 /2 width=2/
37 | @(T_inv_ind … H) -H #i0 #Hi0 #H destruct
38 [ elim (p_pos … Hi0) #i #H destruct
39 elim (IH (i+1) ?) -IH /2 width=1 by monotonic_le_plus_r/ #H #_
40 elim (H Hi0) -H -Hi0 #hi #H >H -i
41 @(ex1_2_intro … hi 0) //
42 | elim (t_pos … Hi0) #i #H destruct
43 elim (IH (i+1) ?) -IH /2 width=1 by monotonic_le_plus_r/ #_ #H
44 elim (H Hi0) -H -Hi0 #hi #ki #H >H -i
45 >associative_times <exp_n_m_plus_1 /2 width=3/
50 theorem p_inv_gen: ∀i. P i → ∃h. i = h * 3 + 1.
51 #i #Hi elim (pt_inv_gen i) /2 width=1/
54 theorem t_inv_gen: ∀i. T i → ∃∃h,k. i = (h * 3 + 1) * 3 ^ (k + 1).
55 #i #Hi elim (pt_inv_gen i) /2 width=1/
58 theorem p_gen: ∀i. P (i * 3 + 1).
59 #i @(nat_ind_plus … i) -i //
60 #i #IHi >times_n_plus_1_m >associative_plus /2 width=1/
63 theorem t_gen: ∀i,j. T ((i * 3 + 1) * 3 ^ (j + 1)).
64 #i #j @(nat_ind_plus … j) -j /2 width=1/
65 #j #IH >exp_n_m_plus_1 <associative_times /2 width=1/
68 lemma pt_discr: ∀i. P i → T i → False.
70 elim (p_inv_gen … Hp) -Hp #hp #Hp
71 elim (t_inv_gen … Ht) -Ht #ht #kt #Ht destruct
72 >exp_n_m_plus_1 in Ht; <associative_times #H
73 elim (not_b_divides_nbr … H) -H //