---

Step * 1 1 1 1 1 of Lemma indexed-coinduction-principle

.....antecedent..... 
1. I : Type
2. F : Type ⟶ Type
3. ContinuousMonotone(T.F[T])
4. R : (I ⟶ corec(T.F[T])) ⟶ (I ⟶ corec(T.F[T])) ⟶ ℙ
5. ∀T:Type
     (((F[T] ⊆r T) ∧ (corec(T.F[T]) ⊆r T))
     ⇒ (∀x,y:I ⟶ corec(T.F[T]).  (R[x;y] ⇒ (x = y ∈ (I ⟶ T))))
     ⇒ (∀x,y:I ⟶ corec(T.F[T]).  (R[x;y] ⇒ (x = y ∈ (I ⟶ F[T])))))
6. n : ℤ
7. ¬n < 1
8. 0 < n
9. ∀[x,y:I ⟶ corec(T.F[T])].  x = y ∈ (I ⟶ primrec(n - 1;Top;λ,T. F[T])) supposing R[x;y]
10. x : I ⟶ corec(T.F[T])
11. y : I ⟶ corec(T.F[T])
12. R[x;y]
13. i : I
⊢ (F[primrec(n - 1;Top;λ,T. F[T])] ⊆r primrec(n - 1;Top;λ,T. F[T])) ∧ (corec(T.F[T]) ⊆r primrec(n - 1;Top;λ,T. F[T]))
BY
{ ((GenConcl ⌜(n - 1) = m ∈ ℕ⌝⋅ THENA Auto')
   THEN Thin (-1)
   THEN NatInd (-1)
   THEN Reduce 0
   THEN D 0
   THEN Try (Complete (Auto))) }

1
1. I : Type
2. F : Type ⟶ Type
3. ContinuousMonotone(T.F[T])
4. R : (I ⟶ corec(T.F[T])) ⟶ (I ⟶ corec(T.F[T])) ⟶ ℙ
5. ∀T:Type
     (((F[T] ⊆r T) ∧ (corec(T.F[T]) ⊆r T))
     ⇒ (∀x,y:I ⟶ corec(T.F[T]).  (R[x;y] ⇒ (x = y ∈ (I ⟶ T))))
     ⇒ (∀x,y:I ⟶ corec(T.F[T]).  (R[x;y] ⇒ (x = y ∈ (I ⟶ F[T])))))
6. n : ℤ
7. ¬n < 1
8. 0 < n
9. ∀[x,y:I ⟶ corec(T.F[T])].  x = y ∈ (I ⟶ primrec(n - 1;Top;λ,T. F[T])) supposing R[x;y]
10. x : I ⟶ corec(T.F[T])
11. y : I ⟶ corec(T.F[T])
12. R[x;y]
13. i : I
14. m : ℤ
15. 0 < m
16. (F[primrec(m - 1;Top;λ,T. F[T])] ⊆r primrec(m - 1;Top;λ,T. F[T])) ∧ (corec(T.F[T]) ⊆r primrec(m - 1;Top;λ,T. F[T]))
⊢ F[primrec(m;Top;λ,T. F[T])] ⊆r primrec(m;Top;λ,T. F[T])

---

Latex:

---

Latex:
.....antecedent..... 
1.  I  :  Type
2.  F  :  Type  {}\mrightarrow{}  Type
3.  ContinuousMonotone(T.F[T])
4.  R  :  (I  {}\mrightarrow{}  corec(T.F[T]))  {}\mrightarrow{}  (I  {}\mrightarrow{}  corec(T.F[T]))  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}T:Type
          (((F[T]  \msubseteq{}r  T)  \mwedge{}  (corec(T.F[T])  \msubseteq{}r  T))
          {}\mRightarrow{}  (\mforall{}x,y:I  {}\mrightarrow{}  corec(T.F[T]).    (R[x;y]  {}\mRightarrow{}  (x  =  y)))
          {}\mRightarrow{}  (\mforall{}x,y:I  {}\mrightarrow{}  corec(T.F[T]).    (R[x;y]  {}\mRightarrow{}  (x  =  y))))
6.  n  :  \mBbbZ{}
7.  \mneg{}n  <  1
8.  0  <  n
9.  \mforall{}[x,y:I  {}\mrightarrow{}  corec(T.F[T])].    x  =  y  supposing  R[x;y]
10.  x  :  I  {}\mrightarrow{}  corec(T.F[T])
11.  y  :  I  {}\mrightarrow{}  corec(T.F[T])
12.  R[x;y]
13.  i  :  I
\mvdash{}  (F[primrec(n  -  1;Top;\mlambda{},T.  F[T])]  \msubseteq{}r  primrec(n  -  1;Top;\mlambda{},T.  F[T]))
\mwedge{}  (corec(T.F[T])  \msubseteq{}r  primrec(n  -  1;Top;\mlambda{},T.  F[T]))


By

---

Latex:
((GenConcl  \mkleeneopen{}(n  -  1)  =  m\mkleeneclose{}\mcdot{}  THENA  Auto')
  THEN  Thin  (-1)
  THEN  NatInd  (-1)
  THEN  Reduce  0
  THEN  D  0
  THEN  Try  (Complete  (Auto)))

---

Home Index