- character: we adjusted some "autobatch" parameters

[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 add242cc449f33d9655fb2b46bbb4e5a59eb318e..8283373db4a99c40dc868ac0302bbc70aa64413f 100644 (file)
--- 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)
 .