Step
*
1
2
2
1
of Lemma
fan-implies-PFan
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. ∃k:ℕ
∀f:ℕ ⟶ 𝔹
∃n@0:ℕk
(((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)))))))
8. k : ℕ
9. n ≤ k
10. ∀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)))))))
11. gh : ℕ ⟶ (𝔹 × 𝔹)@i
12. ¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List))
⊢ ss map(gh;upto(k))
BY
{ TACTIC:((Assert λj.shuffle(map(gh;upto(j + 1)))[j] ∈ ℕ ⟶ 𝔹 BY
(Auto THEN RWW "length-shuffle length-map length_upto" 0 THEN Auto THEN Auto'))
THEN InstHyp [⌜λj.shuffle(map(gh;upto(j + 1)))[j]⌝] (-4)⋅
THEN Auto
THEN ExRepD
THEN Assert ⌜∃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])⌝⋅) }
1
.....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])
2
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. ∃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 map(gh;upto(k))
Latex:
Latex:
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. \mexists{}k:\mBbbN{}
\mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbB{}
\mexists{}n@0:\mBbbN{}k
(((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)))))))
8. k : \mBbbN{}
9. n \mleq{} k
10. \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)))))))
11. gh : \mBbbN{} {}\mrightarrow{} (\mBbbB{} \mtimes{} \mBbbB{})@i
12. \mneg{}(map(\mlambda{}i.(fst((gh i)));upto(n)) = map(\mlambda{}i.(snd((gh i)));upto(n)))
\mvdash{} ss map(gh;upto(k))
By
Latex:
TACTIC:((Assert \mlambda{}j.shuffle(map(gh;upto(j + 1)))[j] \mmember{} \mBbbN{} {}\mrightarrow{} \mBbbB{} BY
(Auto THEN RWW "length-shuffle length-map length\_upto" 0 THEN Auto THEN Auto'))
THEN InstHyp [\mkleeneopen{}\mlambda{}j.shuffle(map(gh;upto(j + 1)))[j]\mkleeneclose{}] (-4)\mcdot{}
THEN Auto
THEN ExRepD
THEN Assert \mkleeneopen{}\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])\mkleeneclose{}\mcdot{})
Home
Index