---

Step * 1 of Lemma fix-mutual-corec-partial1


1. A : Type
2. value-type(A)
3. mono(A)
4. k : ℕ
5. F : (ℕk ⟶ Type) ⟶ ℕk ⟶ Type
6. f : (i:ℕk ⟶ m-corec(T.F[T];i) ⟶ partial(A)) ⟶ i:ℕk ⟶ m-corec(T.F[T];i) ⟶ partial(A)
7. i : ℕk
8. x : m-corec(T.F[T];i)
⊢ fix(f) i x ∈ partial(A)
BY
{ (InstLemma `fixpoint-induction-bottom2` [⌜A⌝;⌜i:ℕk ⟶ m-corec(T.F[T];i) ⟶ partial(A)⌝;⌜λ2f.f i x⌝;⌜f⌝]⋅ THEN Auto) }

1
.....antecedent..... 
1. A : Type
2. value-type(A)
3. mono(A)
4. k : ℕ
5. F : (ℕk ⟶ Type) ⟶ ℕk ⟶ Type
6. f : (i:ℕk ⟶ m-corec(T.F[T];i) ⟶ partial(A)) ⟶ i:ℕk ⟶ m-corec(T.F[T];i) ⟶ partial(A)
7. i : ℕk
8. x : m-corec(T.F[T];i)
⊢ ⊥ ∈ i:ℕk ⟶ m-corec(T.F[T];i) ⟶ partial(A)

---

Latex:

---

Latex:

1.  A  :  Type
2.  value-type(A)
3.  mono(A)
4.  k  :  \mBbbN{}
5.  F  :  (\mBbbN{}k  {}\mrightarrow{}  Type)  {}\mrightarrow{}  \mBbbN{}k  {}\mrightarrow{}  Type
6.  f  :  (i:\mBbbN{}k  {}\mrightarrow{}  m-corec(T.F[T];i)  {}\mrightarrow{}  partial(A))  {}\mrightarrow{}  i:\mBbbN{}k  {}\mrightarrow{}  m-corec(T.F[T];i)  {}\mrightarrow{}  partial(A)
7.  i  :  \mBbbN{}k
8.  x  :  m-corec(T.F[T];i)
\mvdash{}  fix(f)  i  x  \mmember{}  partial(A)


By

---

Latex:
(InstLemma  `fixpoint-induction-bottom2`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}i:\mBbbN{}k  {}\mrightarrow{}  m-corec(T.F[T];i)  {}\mrightarrow{}  partial(A)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}f.f  i  x\mkleeneclose{};
  \mkleeneopen{}f\mkleeneclose{}]\mcdot{}
  THEN  Auto
  )

---

Home Index