X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fcharacter%2Fclasses%2Fdefs.ma;h=8283373db4a99c40dc868ac0302bbc70aa64413f;hb=7f89b4dce54266c281479a14c01edc4bd33993d1;hp=d5986fe7779a5d20926408cdc9cbef0c7e57a1ee;hpb=05ebdd213d5968b9f0eeaa01e4f9aac33ef86c7c;p=helm.git

diff --git a/helm/software/matita/contribs/character/classes/defs.ma b/helm/software/matita/contribs/character/classes/defs.ma
index d5986fe77..8283373db 100644
--- a/helm/software/matita/contribs/character/classes/defs.ma
+++ b/helm/software/matita/contribs/character/classes/defs.ma
@@ -16,12 +16,18 @@ include "preamble.ma".
 
 (* NOTE: OEIS sequence identifiers 
    P(n): A016777 "3n+1"
-*)         
+   T(n): A155504 "(3h+1)*3^(k+1)"
+*)
 
-inductive P: nat \to Prop \def
+inductive P: nat → Prop ≝
    | p1: P 1
-   | p2: \forall i,j. T i \to P j \to P (i + j)
-with T: nat \to Prop \def
-   | t1: \forall i. P i \to T (i * 3)
-   | t2: \forall i. T i \to T (i * 3)
+   | p2: ∀i,j. T i → P j → P (i + j)
+with T: nat → Prop ≝
+   | t1: ∀i. P i → T (i * 3)
+   | t2: ∀i. T i → T (i * 3)
+.
+
+inductive S: nat → Prop ≝
+   | s1: ∀i. P i → S (i * 2)
+   | s2: ∀i. T i → S (i * 2)
 .