update in groud_2 and models

[helm.git] / helm / software / matita / contribs / character / classes / defs.ma

diff --git a/helm/software/matita/contribs/character/classes/defs.ma b/helm/software/matita/contribs/character/classes/defs.ma
index e31c9a93c2bfe5a22abb26e09435d02dbde04707..8283373db4a99c40dc868ac0302bbc70aa64413f 100644 (file)
--- 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)
 .