Step
*
1
2
2
1
1
of Lemma
fan-implies-PFan
.....assertion.....
1. ∀A:(𝔹 List) ⟶ ℙ
((∀as:𝔹 List. Dec(A as)) ⇒ (∀f:ℕ ⟶ 𝔹. ∃n:ℕ. (A map(f;upto(n)))) ⇒ (∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. (A map(f;upto(n)))))
2. n : ℕ@i
3. ss : ((𝔹 × 𝔹) List) ⟶ ℙ@i'
4. ∀bc:(𝔹 × 𝔹) List. Dec(ss bc)
5. ∀bc,bc':(𝔹 × 𝔹) List. (bc ≤ bc' ⇒ (ss bc) ⇒ (ss bc'))
6. ∀gh:ℕ ⟶ (𝔹 × 𝔹)
((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List))) ⇒ (∃m:ℕ. (ss map(gh;upto(m)))))
7. k1 : ℕ
8. ∀f:ℕ ⟶ 𝔹
∃n@0:ℕk1
(((2 * n) ≤ ||map(f;upto(n@0))||)
∧ (∀i:ℕn. ((¬map(f;upto(n@0))[2 * i] = map(f;upto(n@0))[(2 * i) + 1]) ⇒ (ss unshuffle(map(f;upto(n@0)))))))
9. k : ℕ
10. n ≤ k
11. ∀f:ℕ ⟶ 𝔹
∃m:ℕ2 * k
(((2 * n) ≤ ||map(f;upto(m))||)
∧ (∀i:ℕn. ((¬map(f;upto(m))[2 * i] = map(f;upto(m))[(2 * i) + 1]) ⇒ (ss unshuffle(map(f;upto(m)))))))
12. gh : ℕ ⟶ (𝔹 × 𝔹)@i
13. ¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List))
14. λj.shuffle(map(gh;upto(j + 1)))[j] ∈ ℕ ⟶ 𝔹
15. m : ℕ2 * k
16. (2 * n) ≤ ||map(λj.shuffle(map(gh;upto(j + 1)))[j];upto(m))||
17. ∀i:ℕn
((¬map(λj.shuffle(map(gh;upto(j + 1)))[j];upto(m))[2 * i]
= map(λj.shuffle(map(gh;upto(j + 1)))[j];upto(m))[(2 * i) + 1])
⇒ (ss unshuffle(map(λj.shuffle(map(gh;upto(j + 1)))[j];upto(m)))))
⊢ ∃i:ℕn
(¬map(λj.shuffle(map(gh;upto(j + 1)))[j];upto(m))[2 * i]
= map(λj.shuffle(map(gh;upto(j + 1)))[j];upto(m))[(2 * i) + 1])
BY
{ TACTIC:(GenConcl ⌜(λj.shuffle(map(gh;upto(j + 1)))[j]) = G ∈ (ℕ ⟶ 𝔹)⌝⋅ THENA Auto) }
1
1. ∀A:(𝔹 List) ⟶ ℙ
((∀as:𝔹 List. Dec(A as)) ⇒ (∀f:ℕ ⟶ 𝔹. ∃n:ℕ. (A map(f;upto(n)))) ⇒ (∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. (A map(f;upto(n)))))
2. n : ℕ@i
3. ss : ((𝔹 × 𝔹) List) ⟶ ℙ@i'
4. ∀bc:(𝔹 × 𝔹) List. Dec(ss bc)
5. ∀bc,bc':(𝔹 × 𝔹) List. (bc ≤ bc' ⇒ (ss bc) ⇒ (ss bc'))
6. ∀gh:ℕ ⟶ (𝔹 × 𝔹)
((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List))) ⇒ (∃m:ℕ. (ss map(gh;upto(m)))))
7. k1 : ℕ
8. ∀f:ℕ ⟶ 𝔹
∃n@0:ℕk1
(((2 * n) ≤ ||map(f;upto(n@0))||)
∧ (∀i:ℕn. ((¬map(f;upto(n@0))[2 * i] = map(f;upto(n@0))[(2 * i) + 1]) ⇒ (ss unshuffle(map(f;upto(n@0)))))))
9. k : ℕ
10. n ≤ k
11. ∀f:ℕ ⟶ 𝔹
∃m:ℕ2 * k
(((2 * n) ≤ ||map(f;upto(m))||)
∧ (∀i:ℕn. ((¬map(f;upto(m))[2 * i] = map(f;upto(m))[(2 * i) + 1]) ⇒ (ss unshuffle(map(f;upto(m)))))))
12. gh : ℕ ⟶ (𝔹 × 𝔹)@i
13. ¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List))
14. λj.shuffle(map(gh;upto(j + 1)))[j] ∈ ℕ ⟶ 𝔹
15. m : ℕ2 * k
16. (2 * n) ≤ ||map(λj.shuffle(map(gh;upto(j + 1)))[j];upto(m))||
17. ∀i:ℕn
((¬map(λj.shuffle(map(gh;upto(j + 1)))[j];upto(m))[2 * i]
= map(λj.shuffle(map(gh;upto(j + 1)))[j];upto(m))[(2 * i) + 1])
⇒ (ss unshuffle(map(λj.shuffle(map(gh;upto(j + 1)))[j];upto(m)))))
18. G : ℕ ⟶ 𝔹@i
19. (λj.shuffle(map(gh;upto(j + 1)))[j]) = G ∈ (ℕ ⟶ 𝔹)
⊢ ∃i:ℕn. (¬map(G;upto(m))[2 * i] = map(G;upto(m))[(2 * i) + 1])
Latex:
Latex:
.....assertion.....
1. \mforall{}A:(\mBbbB{} List) {}\mrightarrow{} \mBbbP{}
((\mforall{}as:\mBbbB{} List. Dec(A as))
{}\mRightarrow{} (\mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbB{}. \mexists{}n:\mBbbN{}. (A map(f;upto(n))))
{}\mRightarrow{} (\mexists{}k:\mBbbN{}. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbB{}. \mexists{}n:\mBbbN{}k. (A map(f;upto(n)))))
2. n : \mBbbN{}@i
3. ss : ((\mBbbB{} \mtimes{} \mBbbB{}) List) {}\mrightarrow{} \mBbbP{}@i'
4. \mforall{}bc:(\mBbbB{} \mtimes{} \mBbbB{}) List. Dec(ss bc)
5. \mforall{}bc,bc':(\mBbbB{} \mtimes{} \mBbbB{}) List. (bc \mleq{} bc' {}\mRightarrow{} (ss bc) {}\mRightarrow{} (ss bc'))
6. \mforall{}gh:\mBbbN{} {}\mrightarrow{} (\mBbbB{} \mtimes{} \mBbbB{})
((\mneg{}(map(\mlambda{}i.(fst((gh i)));upto(n)) = map(\mlambda{}i.(snd((gh i)));upto(n))))
{}\mRightarrow{} (\mexists{}m:\mBbbN{}. (ss map(gh;upto(m)))))
7. k1 : \mBbbN{}
8. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbB{}
\mexists{}n@0:\mBbbN{}k1
(((2 * n) \mleq{} ||map(f;upto(n@0))||)
\mwedge{} (\mforall{}i:\mBbbN{}n
((\mneg{}map(f;upto(n@0))[2 * i] = map(f;upto(n@0))[(2 * i) + 1])
{}\mRightarrow{} (ss unshuffle(map(f;upto(n@0)))))))
9. k : \mBbbN{}
10. n \mleq{} k
11. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbB{}
\mexists{}m:\mBbbN{}2 * k
(((2 * n) \mleq{} ||map(f;upto(m))||)
\mwedge{} (\mforall{}i:\mBbbN{}n
((\mneg{}map(f;upto(m))[2 * i] = map(f;upto(m))[(2 * i) + 1])
{}\mRightarrow{} (ss unshuffle(map(f;upto(m)))))))
12. gh : \mBbbN{} {}\mrightarrow{} (\mBbbB{} \mtimes{} \mBbbB{})@i
13. \mneg{}(map(\mlambda{}i.(fst((gh i)));upto(n)) = map(\mlambda{}i.(snd((gh i)));upto(n)))
14. \mlambda{}j.shuffle(map(gh;upto(j + 1)))[j] \mmember{} \mBbbN{} {}\mrightarrow{} \mBbbB{}
15. m : \mBbbN{}2 * k
16. (2 * n) \mleq{} ||map(\mlambda{}j.shuffle(map(gh;upto(j + 1)))[j];upto(m))||
17. \mforall{}i:\mBbbN{}n
((\mneg{}map(\mlambda{}j.shuffle(map(gh;upto(j + 1)))[j];upto(m))[2 * i]
= map(\mlambda{}j.shuffle(map(gh;upto(j + 1)))[j];upto(m))[(2 * i) + 1])
{}\mRightarrow{} (ss unshuffle(map(\mlambda{}j.shuffle(map(gh;upto(j + 1)))[j];upto(m)))))
\mvdash{} \mexists{}i:\mBbbN{}n
(\mneg{}map(\mlambda{}j.shuffle(map(gh;upto(j + 1)))[j];upto(m))[2 * i]
= map(\mlambda{}j.shuffle(map(gh;upto(j + 1)))[j];upto(m))[(2 * i) + 1])
By
Latex:
TACTIC:(GenConcl \mkleeneopen{}(\mlambda{}j.shuffle(map(gh;upto(j + 1)))[j]) = G\mkleeneclose{}\mcdot{} THENA Auto)
Home
Index