---

Step * of Lemma Spread-family-ext

∀[P,Pos:Type]. ∀[f:Pos ⟶ ℤ]. ∀[Mv:ℤ ⟶ P ⟶ P ⟶ Type].
  Spread-family(P;Pos;f;n,p,q.Mv[n;p;q])
  ≡ λp.(a:Pos × (q:P ⟶ Mv[f a;p;q] ⟶ (Spread-family(P;Pos;f;n,p,q.Mv[n;p;q]) q)))
BY
{ (Auto
   THEN Unfold `Spread-family` 0
   THEN (InstLemma `corec-family-ext` [⌜P⌝;⌜λW,p. (a:Pos × (q:P ⟶ Mv[f a;p;q] ⟶ (W q)))⌝]⋅ THENA Auto)
   THEN Try ((Reduce (-1) THEN Trivial)))⋅ }

1
1. P : Type
2. Pos : Type
3. f : Pos ⟶ ℤ
4. Mv : ℤ ⟶ P ⟶ P ⟶ Type
⊢ type-family-continuous{i:l}(P;λW,p. (a:Pos × (q:P ⟶ Mv[f a;p;q] ⟶ (W q))))

2
1. P : Type
2. Pos : Type
3. f : Pos ⟶ ℤ
4. Mv : ℤ ⟶ P ⟶ P ⟶ Type
5. type-family-continuous{i:l}(P;λW,p. (a:Pos × (q:P ⟶ Mv[f a;p;q] ⟶ (W q))))
⊢ family-monotone{i:l}(P;λW,p. (a:Pos × (q:P ⟶ Mv[f a;p;q] ⟶ (W q))))

---

Latex:

---

Latex:
\mforall{}[P,Pos:Type].  \mforall{}[f:Pos  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[Mv:\mBbbZ{}  {}\mrightarrow{}  P  {}\mrightarrow{}  P  {}\mrightarrow{}  Type].
    Spread-family(P;Pos;f;n,p,q.Mv[n;p;q])  \mequiv{}  \mlambda{}p.(a:Pos  \mtimes{}  (q:P
                                                                                                              {}\mrightarrow{}  Mv[f  a;p;q]
                                                                                                              {}\mrightarrow{}  (Spread-family(P;Pos;f;n,p,q.Mv[n;p;q]) 
                                                                                                                      q)))


By

---

Latex:
(Auto
  THEN  Unfold  `Spread-family`  0
  THEN  (InstLemma  `corec-family-ext`  [\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}\mlambda{}W,p.  (a:Pos  \mtimes{}  (q:P  {}\mrightarrow{}  Mv[f  a;p;q]  {}\mrightarrow{}  (W  q)))\mkleeneclose{}]\mcdot{}  THENA  Aut\000Co)
  THEN  Try  ((Reduce  (-1)  THEN  Trivial)))\mcdot{}

---

Home Index