---

Step * 1 2 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:ℕ. ∀x:⋃n:ℕn.(F^n Void) ⋂ urec(F).  P[x]
⊢ P[x]
BY
{ TACTIC:Assert ⌜∃n:ℕ. (x ∈ ⋃n:ℕn.(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:ℕ. ∀x:⋃n:ℕn.(F^n Void) ⋂ urec(F).  P[x]
⊢ ∃n:ℕ. (x ∈ ⋃n:ℕn.(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:ℕ. ∀x:⋃n:ℕn.(F^n Void) ⋂ urec(F).  P[x]
9. ∃n:ℕ. (x ∈ ⋃n:ℕn.(F^n Void))
⊢ P[x]

---

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.  \mforall{}n:\mBbbN{}.  \mforall{}x:\mcup{}n:\mBbbN{}n.(F\^{}n  Void)  \mcap{}  urec(F).    P[x]
\mvdash{}  P[x]


By

---

Latex:
TACTIC:Assert  \mkleeneopen{}\mexists{}n:\mBbbN{}.  (x  \mmember{}  \mcup{}n:\mBbbN{}n.(F\^{}n  Void))\mkleeneclose{}\mcdot{}

---

Home Index