Step
*
of Lemma
fan-bar-not-unbounded
∀[T:Type]. ∀A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹. (bar(A)
⇒ (¬(Tree(¬(A)) ∧ Unbounded(¬(A))))) supposing ¬¬Fan(T)
BY
{ (Auto
THEN (D 0 THENA Auto)
THEN (SupposeMore 2 THENA Auto)
THEN (With ⌜A⌝ (D 2)⋅ THENA Auto)
THEN ThinTrivial
THEN Auto
THEN D -1
THEN (D -3 With ⌜k + 1⌝ THENA Auto)
THEN ExRepD
THEN (With ⌜λi.if i <z k then s i else s 0 fi ⌝ (D (-3))⋅ THENA Auto)
THEN D -1) }
1
1. T : Type
2. A : n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹
3. bar(A)
4. Tree(¬(A))
5. k : ℕ
6. s : ℕk + 1 ⟶ T
7. ↑(¬(A) (k + 1) s)
8. n : ℕk
9. ↑(A n (λi.if i <z k then s i else s 0 fi ))
⊢ False
Latex:
Latex:
\mforall{}[T:Type]
\mforall{}A:n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} T) {}\mrightarrow{} \mBbbB{}. (bar(A) {}\mRightarrow{} (\mneg{}(Tree(\mneg{}(A)) \mwedge{} Unbounded(\mneg{}(A))))) supposing \mneg{}\mneg{}Fan(T)
By
Latex:
(Auto
THEN (D 0 THENA Auto)
THEN (SupposeMore 2 THENA Auto)
THEN (With \mkleeneopen{}A\mkleeneclose{} (D 2)\mcdot{} THENA Auto)
THEN ThinTrivial
THEN Auto
THEN D -1
THEN (D -3 With \mkleeneopen{}k + 1\mkleeneclose{} THENA Auto)
THEN ExRepD
THEN (With \mkleeneopen{}\mlambda{}i.if i <z k then s i else s 0 fi \mkleeneclose{} (D (-3))\mcdot{} THENA Auto)
THEN D -1)
Home
Index