---

Step * 1 1 2 1 1 1 1 1 of Lemma urec_induction


1. F : Type ⟶ Type
2. Monotone(T.F[T])
3. ∀T:Type. ((T ⊆r Base) ⇒ ((F T) ⊆r Base))
4. destructor{i:l}(T.F[T])
5. P : urec(F) ⟶ ℙ
6. ∀[T:Type]. ((∀x:T ⋂ urec(F). P[x]) ⇒ (∀x:F T ⋂ urec(F). P[x]))
7. x : urec(F)
8. n : ℤ
9. 0 < n
10. ∀x:F ⋃n:ℕn - 1.(F^n Void) ⋂ urec(F). P[x]
11. x1 : ⋃n:ℕn.(F^n Void) ⋂ urec(F)
12. x1 = x1 ∈ ⋃n:ℕn.(F^n Void) ⋂ urec(F)
13. ∀[X:ℕn - 1 ⟶ Type]. (⋃n:ℕn - 1.F[X n] ⊆r F[⋃n:ℕn - 1.(X n)])
14. ⋃n:ℕn - 1.F[F^n Void] ⊆r F[⋃n:ℕn - 1.(F^n Void)]
⊢ ⋃n:ℕn.(F^n Void) ⊆r (F ⋃n:ℕn - 1.(F^n Void))
BY
{ Assert ⌜⋃n:ℕn.(F^n Void) ≡ ⋃n:ℕn - 1.F[F^n Void]⌝ ⋅ }

1
.....assertion..... 
1. F : Type ⟶ Type
2. Monotone(T.F[T])
3. ∀T:Type. ((T ⊆r Base) ⇒ ((F T) ⊆r Base))
4. destructor{i:l}(T.F[T])
5. P : urec(F) ⟶ ℙ
6. ∀[T:Type]. ((∀x:T ⋂ urec(F). P[x]) ⇒ (∀x:F T ⋂ urec(F). P[x]))
7. x : urec(F)
8. n : ℤ
9. 0 < n
10. ∀x:F ⋃n:ℕn - 1.(F^n Void) ⋂ urec(F). P[x]
11. x1 : ⋃n:ℕn.(F^n Void) ⋂ urec(F)
12. x1 = x1 ∈ ⋃n:ℕn.(F^n Void) ⋂ urec(F)
13. ∀[X:ℕn - 1 ⟶ Type]. (⋃n:ℕn - 1.F[X n] ⊆r F[⋃n:ℕn - 1.(X n)])
14. ⋃n:ℕn - 1.F[F^n Void] ⊆r F[⋃n:ℕn - 1.(F^n Void)]
⊢ ⋃n:ℕn.(F^n Void) ≡ ⋃n:ℕn - 1.F[F^n Void]

2
1. F : Type ⟶ Type
2. Monotone(T.F[T])
3. ∀T:Type. ((T ⊆r Base) ⇒ ((F T) ⊆r Base))
4. destructor{i:l}(T.F[T])
5. P : urec(F) ⟶ ℙ
6. ∀[T:Type]. ((∀x:T ⋂ urec(F). P[x]) ⇒ (∀x:F T ⋂ urec(F). P[x]))
7. x : urec(F)
8. n : ℤ
9. 0 < n
10. ∀x:F ⋃n:ℕn - 1.(F^n Void) ⋂ urec(F). P[x]
11. x1 : ⋃n:ℕn.(F^n Void) ⋂ urec(F)
12. x1 = x1 ∈ ⋃n:ℕn.(F^n Void) ⋂ urec(F)
13. ∀[X:ℕn - 1 ⟶ Type]. (⋃n:ℕn - 1.F[X n] ⊆r F[⋃n:ℕn - 1.(X n)])
14. ⋃n:ℕn - 1.F[F^n Void] ⊆r F[⋃n:ℕn - 1.(F^n Void)]
15. ⋃n:ℕn.(F^n Void) ≡ ⋃n:ℕn - 1.F[F^n Void]
⊢ ⋃n:ℕn.(F^n Void) ⊆r (F ⋃n:ℕn - 1.(F^n Void))

---

Latex:

---

Latex:

1.  F  :  Type  {}\mrightarrow{}  Type
2.  Monotone(T.F[T])
3.  \mforall{}T:Type.  ((T  \msubseteq{}r  Base)  {}\mRightarrow{}  ((F  T)  \msubseteq{}r  Base))
4.  destructor\{i:l\}(T.F[T])
5.  P  :  urec(F)  {}\mrightarrow{}  \mBbbP{}
6.  \mforall{}[T:Type].  ((\mforall{}x:T  \mcap{}  urec(F).  P[x])  {}\mRightarrow{}  (\mforall{}x:F  T  \mcap{}  urec(F).  P[x]))
7.  x  :  urec(F)
8.  n  :  \mBbbZ{}
9.  0  <  n
10.  \mforall{}x:F  \mcup{}n:\mBbbN{}n  -  1.(F\^{}n  Void)  \mcap{}  urec(F).  P[x]
11.  x1  :  \mcup{}n:\mBbbN{}n.(F\^{}n  Void)  \mcap{}  urec(F)
12.  x1  =  x1
13.  \mforall{}[X:\mBbbN{}n  -  1  {}\mrightarrow{}  Type].  (\mcup{}n:\mBbbN{}n  -  1.F[X  n]  \msubseteq{}r  F[\mcup{}n:\mBbbN{}n  -  1.(X  n)])
14.  \mcup{}n:\mBbbN{}n  -  1.F[F\^{}n  Void]  \msubseteq{}r  F[\mcup{}n:\mBbbN{}n  -  1.(F\^{}n  Void)]
\mvdash{}  \mcup{}n:\mBbbN{}n.(F\^{}n  Void)  \msubseteq{}r  (F  \mcup{}n:\mBbbN{}n  -  1.(F\^{}n  Void))


By

---

Latex:
Assert  \mkleeneopen{}\mcup{}n:\mBbbN{}n.(F\^{}n  Void)  \mequiv{}  \mcup{}n:\mBbbN{}n  -  1.F[F\^{}n  Void]\mkleeneclose{}  \mcdot{}

---

Home Index