---

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


1. T : Type
2. A : {A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹| Tree(A) ∧ Unbounded(A)} 
3. ∀a,b:T.  Dec(a = b ∈ T)
4. ∀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')))))
5. g : n:ℕ ⟶ s:(ℕn ⟶ T) ⟶ T
6. ∀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')))))
7. f : ℕ ⟶ T
8. ∀n:ℕ. ((f n) = (g n f) ∈ T)
9. n : ℕ
10. ¬↑(A n f)
11. f1 : ℕ ⟶ T
12. ¬(f1 = f ∈ (ℕn ⟶ T))
⊢ ∃n:ℕ. (↑¬b(A n f1))
BY
{ (Assert ∃i:ℕn. ((f1 = f ∈ (ℕi ⟶ T)) ∧ (¬((f1 i) = (f i) ∈ T))) BY
         (MoveToConcl (-1)
          THEN Thin (-2)
          THEN ((NatInd (-2) THEN Auto)
                THENL [(D -1 THEN Auto)
                      ; ((Decide ⌜f1 = f ∈ (ℕn - 1 ⟶ T)⌝⋅ THENA Auto)
                         THENL [((D 0 With ⌜n - 1⌝  THENA Auto)
                                 THEN D 0
                                 THEN Try (Trivial)
                                 THEN ParallelOp -2
                                 THEN (FunExt THENA Auto)
                                 THEN ((Decide ⌜x = (n - 1) ∈ ℤ⌝⋅ THENA Auto)
                                       THENL [(HypSubst' -1 0 THEN Auto)
                                             ; (ApFunToHypEquands  `Z' ⌜Z x⌝ ⌜T⌝ (-4)⋅ THEN Auto)]
                                 ))
                               ; (ThinTrivial THEN ParallelLast)]
                      )]
          ))) }

1
1. T : Type
2. A : {A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹| Tree(A) ∧ Unbounded(A)} 
3. ∀a,b:T.  Dec(a = b ∈ T)
4. ∀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')))))
5. g : n:ℕ ⟶ s:(ℕn ⟶ T) ⟶ T
6. ∀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')))))
7. f : ℕ ⟶ T
8. ∀n:ℕ. ((f n) = (g n f) ∈ T)
9. n : ℕ
10. ¬↑(A n f)
11. f1 : ℕ ⟶ T
12. ¬(f1 = f ∈ (ℕn ⟶ T))
13. ∃i:ℕn. ((f1 = f ∈ (ℕi ⟶ T)) ∧ (¬((f1 i) = (f i) ∈ T)))
⊢ ∃n:ℕ. (↑¬b(A n f1))

---

Latex:

---

Latex:

1.  T  :  Type
2.  A  :  \{A:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbB{}|  Tree(A)  \mwedge{}  Unbounded(A)\} 
3.  \mforall{}a,b:T.    Dec(a  =  b)
4.  \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')))))
5.  g  :  n:\mBbbN{}  {}\mrightarrow{}  s:(\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  T
6.  \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')))))
7.  f  :  \mBbbN{}  {}\mrightarrow{}  T
8.  \mforall{}n:\mBbbN{}.  ((f  n)  =  (g  n  f))
9.  n  :  \mBbbN{}
10.  \mneg{}\muparrow{}(A  n  f)
11.  f1  :  \mBbbN{}  {}\mrightarrow{}  T
12.  \mneg{}(f1  =  f)
\mvdash{}  \mexists{}n:\mBbbN{}.  (\muparrow{}\mneg{}\msubb{}(A  n  f1))


By

---

Latex:
(Assert  \mexists{}i:\mBbbN{}n.  ((f1  =  f)  \mwedge{}  (\mneg{}((f1  i)  =  (f  i))))  BY
              (MoveToConcl  (-1)
                THEN  Thin  (-2)
                THEN  ((NatInd  (-2)  THEN  Auto)
                            THENL  [(D  -1  THEN  Auto)
                                        ;  ((Decide  \mkleeneopen{}f1  =  f\mkleeneclose{}\mcdot{}  THENA  Auto)
                                              THENL  [((D  0  With  \mkleeneopen{}n  -  1\mkleeneclose{}    THENA  Auto)
                                                              THEN  D  0
                                                              THEN  Try  (Trivial)
                                                              THEN  ParallelOp  -2
                                                              THEN  (FunExt  THENA  Auto)
                                                              THEN  ((Decide  \mkleeneopen{}x  =  (n  -  1)\mkleeneclose{}\mcdot{}  THENA  Auto)
                                                                          THENL  [(HypSubst'  -1  0  THEN  Auto)
                                                                                      ;  (ApFunToHypEquands    `Z'  \mkleeneopen{}Z  x\mkleeneclose{}  \mkleeneopen{}T\mkleeneclose{}  (-4)\mcdot{}  THEN  Auto)]
                                                              ))
                                                          ;  (ThinTrivial  THEN  ParallelLast)]
                                        )]
                )))

---

Home Index