Step * 1 of Lemma unique-awf


1. [A] Type
2. [I] Type
3. : ⋂T:{T:Type| ((A (T List)) ⊆T) ∧ (awf(A) ⊆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 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. : ⋂T:{T:Type| ((A (T List)) ⊆T) ∧ (awf(A) ⊆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. : ⋂T:{T:Type| ((A (T List)) ⊆T) ∧ (awf(A) ⊆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 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