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

diff --git a/helm/software/matita/contribs/character/classes/defs.ma b/helm/software/matita/contribs/character/classes/defs.ma
index add242cc4..8283373db 100644
--- a/helm/software/matita/contribs/character/classes/defs.ma
+++ b/helm/software/matita/contribs/character/classes/defs.ma
@@ -16,17 +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 \to Prop \def
-   | s1: \forall i. P i \to S (i * 2)
-   | s2: \forall i. T i \to S (i * 2)
+inductive S: nat → Prop ≝
+   | s1: ∀i. P i → S (i * 2)
+   | s2: ∀i. T i → S (i * 2)
 .