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 (* BTM: MATITA SOURCE FILES
16 * Suggested invocation to start formal specifications with:
17 * - Patience on me to gain peace and perfection! -
19 * specification starts.
24 (* CHARACTER CLASSES ********************************************************)
26 (* Note: OEIS sequence identifiers
28 T(n): A155504 "(3h+1)*3^(k+1)"
31 inductive P: predicate nat ≝
33 | p2: ∀i,j. T i → P j → P (i + j)
34 with T: predicate nat ≝
35 | t1: ∀i. P i → T (i * 3)
36 | t2: ∀i. T i → T (i * 3)
39 inductive S: predicate nat ≝
40 | s1: ∀i. P i → S (i * 2)
41 | s2: ∀i. T i → S (i * 2)
44 inductive Q: predicate nat ≝
45 | q1: ∀i. P i → Q (i * 2 + 3)
46 | q2: ∀i. Q i → Q (i * 3)
49 (* Basic eliminators ********************************************************)
51 axiom p_ind: ∀R:predicate nat. R 1 →
52 (∀i,j. T i → R j → R (i + j)) →
55 axiom t_ind: ∀R:predicate nat.
56 (∀i. P i → R (i * 3)) →
57 (∀i. R i → R (i * 3)) →
60 (* Basic inversion lemmas ***************************************************)
62 fact p_inv_O_aux: ∀i. P i → i = 0 → False.
66 elim (plus_inv_O3 … H) -H /2 width=1/
70 lemma p_inv_O: P 0 → False.
71 /2 width=3 by p_inv_O_aux/ qed-.
73 fact t_inv_O_aux: ∀i. T i → i = 0 → False.
74 #i #H @(t_ind … H) -i #i #IH #H
75 lapply (times_inv_S2_O3 … H) -H /2 width=1/
76 /2 width=3 by p_inv_O_aux/
79 lemma t_inv_O: T 0 → False.
80 /2 width=3 by t_inv_O_aux/ qed-.
82 (* Basic properties *********************************************************)
87 lemma p_pos: ∀i. P i → ∃k. i = k + 1.
92 lemma t_pos: ∀i. T i → ∃k. i = k + 1.