---

Step * 1 2 1 1 of Lemma alt-bar-sep-wkl!


1. [T] : Type
2. A : {A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹| Tree(A) ∧ Unbounded(A)} 
3. ¬bar(¬(A))
4. ∀a,b:T.  Dec(a = b ∈ T)
5. ∀n:ℕ. ∀s:ℕn ⟶ T.  ∃t:T. ∀t':T. ((¬(t' = t ∈ T)) ⇒ bar(¬(λk,s'. (A ((n + 1) + k) seq-append(n + 1;s.t';s')))))
6. g : n:ℕ ⟶ s:(ℕn ⟶ T) ⟶ T
7. ∀n:ℕ. ∀s:ℕn ⟶ T. ∀t':T.  ((¬(t' = (g n s) ∈ T)) ⇒ bar(¬(λk,s'. (A ((n + 1) + k) seq-append(n + 1;s.t';s')))))
⊢ ∃f:ℕ ⟶ T [IsPath(A;f)]
BY
{ ((Assert ∃f:ℕ ⟶ T. ∀n:ℕ. ((f n) = (g n f) ∈ T) BY
          ((Assert fix((λG,n. (g n G))) ∈ ℕ ⟶ T BY
                  ((FunExt THENA Auto)
                   THEN MoveToConcl (-1)
                   THEN CompleteInductionOnNat
                   THEN RW (SweepUpC UnrollRecursionC) 0
                   THEN Reduce 0
                   THEN MemCD
                   THEN FunExt
                   THEN Auto))
           THEN D 0 With ⌜fix((λG,n. (g n G)))⌝ 
           THEN Auto))
   THEN ParallelLast
   ) }

1
.....set predicate..... 
1. T : Type
2. A : {A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹| Tree(A) ∧ Unbounded(A)} 
3. ¬bar(¬(A))
4. ∀a,b:T.  Dec(a = b ∈ T)
5. ∀n:ℕ. ∀s:ℕn ⟶ T.  ∃t:T. ∀t':T. ((¬(t' = t ∈ T)) ⇒ bar(¬(λk,s'. (A ((n + 1) + k) seq-append(n + 1;s.t';s')))))
6. g : n:ℕ ⟶ s:(ℕn ⟶ T) ⟶ T
7. ∀n:ℕ. ∀s:ℕn ⟶ T. ∀t':T.  ((¬(t' = (g n s) ∈ T)) ⇒ bar(¬(λk,s'. (A ((n + 1) + k) seq-append(n + 1;s.t';s')))))
8. f : ℕ ⟶ T
9. ∀n:ℕ. ((f n) = (g n f) ∈ T)
⊢ IsPath(A;f)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  A  :  \{A:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbB{}|  Tree(A)  \mwedge{}  Unbounded(A)\} 
3.  \mneg{}bar(\mneg{}(A))
4.  \mforall{}a,b:T.    Dec(a  =  b)
5.  \mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  T.
          \mexists{}t:T.  \mforall{}t':T.  ((\mneg{}(t'  =  t))  {}\mRightarrow{}  bar(\mneg{}(\mlambda{}k,s'.  (A  ((n  +  1)  +  k)  seq-append(n  +  1;s.t';s')))))
6.  g  :  n:\mBbbN{}  {}\mrightarrow{}  s:(\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  T
7.  \mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  T.  \mforall{}t':T.
          ((\mneg{}(t'  =  (g  n  s)))  {}\mRightarrow{}  bar(\mneg{}(\mlambda{}k,s'.  (A  ((n  +  1)  +  k)  seq-append(n  +  1;s.t';s')))))
\mvdash{}  \mexists{}f:\mBbbN{}  {}\mrightarrow{}  T  [IsPath(A;f)]


By

---

Latex:
((Assert  \mexists{}f:\mBbbN{}  {}\mrightarrow{}  T.  \mforall{}n:\mBbbN{}.  ((f  n)  =  (g  n  f))  BY
                ((Assert  fix((\mlambda{}G,n.  (g  n  G)))  \mmember{}  \mBbbN{}  {}\mrightarrow{}  T  BY
                                ((FunExt  THENA  Auto)
                                  THEN  MoveToConcl  (-1)
                                  THEN  CompleteInductionOnNat
                                  THEN  RW  (SweepUpC  UnrollRecursionC)  0
                                  THEN  Reduce  0
                                  THEN  MemCD
                                  THEN  FunExt
                                  THEN  Auto))
                  THEN  D  0  With  \mkleeneopen{}fix((\mlambda{}G,n.  (g  n  G)))\mkleeneclose{} 
                  THEN  Auto))
  THEN  ParallelLast
  )

---

Home Index