---

Step * 1 of Lemma unique-awf


1. [A] : Type
2. [I] : Type
3. G : ⋂T:{T:Type| ((A + (T List)) ⊆r T) ∧ (awf(A) ⊆r T)} . ((I ⟶ T) ⟶ I ⟶ (A + (T List))) ⋂ Top ⟶ I ⟶ Top@i'
4. ∃!s:I ⟶ awf(A). (s = (G s) ∈ (I ⟶ awf(A)))
⊢ ∃s:I ⟶ awf(A) [((∀i:I. ((s i) = (G s i) ∈ awf(A)))
                 ∧ (∀s':I ⟶ awf(A). ((∀i:I. ((s' i) = (G s' i) ∈ awf(A))) ⇒ (s' = s ∈ (I ⟶ awf(A))))))]
BY
{ TACTIC:Assert ⌜G ∈ (I ⟶ awf(A)) ⟶ I ⟶ awf(A)⌝⋅ }

1
.....assertion..... 
1. [A] : Type
2. [I] : Type
3. G : ⋂T:{T:Type| ((A + (T List)) ⊆r T) ∧ (awf(A) ⊆r T)} . ((I ⟶ T) ⟶ I ⟶ (A + (T List))) ⋂ Top ⟶ I ⟶ Top@i'
4. ∃!s:I ⟶ awf(A). (s = (G s) ∈ (I ⟶ awf(A)))
⊢ G ∈ (I ⟶ awf(A)) ⟶ I ⟶ awf(A)

2
1. [A] : Type
2. [I] : Type
3. G : ⋂T:{T:Type| ((A + (T List)) ⊆r T) ∧ (awf(A) ⊆r T)} . ((I ⟶ T) ⟶ I ⟶ (A + (T List))) ⋂ Top ⟶ I ⟶ Top@i'
4. ∃!s:I ⟶ awf(A). (s = (G s) ∈ (I ⟶ awf(A)))
5. G ∈ (I ⟶ awf(A)) ⟶ I ⟶ awf(A)
⊢ ∃s:I ⟶ awf(A) [((∀i:I. ((s i) = (G s i) ∈ awf(A)))
                 ∧ (∀s':I ⟶ awf(A). ((∀i:I. ((s' i) = (G s' i) ∈ awf(A))) ⇒ (s' = s ∈ (I ⟶ awf(A))))))]

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [I]  :  Type
3.  G  :  \mcap{}T:\{T:Type|  ((A  +  (T  List))  \msubseteq{}r  T)  \mwedge{}  (awf(A)  \msubseteq{}r  T)\}  .  ((I  {}\mrightarrow{}  T)  {}\mrightarrow{}  I  {}\mrightarrow{}  (A  +  (T  List)))  \mcap{}  Top
{}\mrightarrow{}  I
{}\mrightarrow{}  Top@i'
4.  \mexists{}!s:I  {}\mrightarrow{}  awf(A).  (s  =  (G  s))
\mvdash{}  \mexists{}s:I  {}\mrightarrow{}  awf(A)  [((\mforall{}i:I.  ((s  i)  =  (G  s  i)))
                                  \mwedge{}  (\mforall{}s':I  {}\mrightarrow{}  awf(A).  ((\mforall{}i:I.  ((s'  i)  =  (G  s'  i)))  {}\mRightarrow{}  (s'  =  s))))]


By

---

Latex:
TACTIC:Assert  \mkleeneopen{}G  \mmember{}  (I  {}\mrightarrow{}  awf(A))  {}\mrightarrow{}  I  {}\mrightarrow{}  awf(A)\mkleeneclose{}\mcdot{}

---

Home Index