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=e31c9a93c2bfe5a22abb26e09435d02dbde04707;hpb=5c0ced5c13852bcc93761859285efe4c5f0d2513;p=helm.git

diff --git a/helm/software/matita/contribs/character/classes/defs.ma b/helm/software/matita/contribs/character/classes/defs.ma
index e31c9a93c..8283373db 100644
--- a/helm/software/matita/contribs/character/classes/defs.ma
+++ b/helm/software/matita/contribs/character/classes/defs.ma
@@ -14,10 +14,20 @@
 
 include "preamble.ma".
 
-inductive P: nat \to Prop \def
+(* NOTE: OEIS sequence identifiers 
+   P(n): A016777 "3n+1"
+   T(n): A155504 "(3h+1)*3^(k+1)"
+*)
+
+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)
 .