Step
*
1
2
2
1
1
1
1
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. 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. λj.shuffle(map(gh;upto(j + 1)))[j] ∈ ℕ ⟶ 𝔹
14. m : ℕ2 * k
15. (2 * n) ≤ m
16. ∀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)))))
17. G : ℕ ⟶ 𝔹@i
18. (λj.shuffle(map(gh;upto(j + 1)))[j]) = G ∈ (ℕ ⟶ 𝔹)
19. ¬(∃i:ℕn. (¬map(G;upto(m))[2 * i] = map(G;upto(m))[(2 * i) + 1]))
⊢ map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List)
BY
{ ((BLemma `list_extensionality` THENA Auto)
THEN RWO "map-length" 0
THEN Auto
THEN (RWO "select-map" 0 THENA Auto)
THEN Reduce 0
THEN (RWO "length_upto" (-1) THENA Auto)
THEN (RWO "select-upto" 0 THENA Auto)
THEN SupposeNot
THEN Auto
THEN D -4
THEN (With ⌜i⌝ (D 0)⋅ THENA Auto)
THEN RWW "map-length length_upto" 0
THEN 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. λj.shuffle(map(gh;upto(j + 1)))[j] ∈ ℕ ⟶ 𝔹
14. m : ℕ2 * k
15. (2 * n) ≤ m
16. ∀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)))))
17. G : ℕ ⟶ 𝔹@i
18. (λj.shuffle(map(gh;upto(j + 1)))[j]) = G ∈ (ℕ ⟶ 𝔹)
19. i : ℕ@i
20. i < n
21. ¬fst((gh i)) = snd((gh i))
⊢ ¬map(G;upto(m))[2 * i] = map(G;upto(m))[(2 * i) + 1]
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. 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. \mlambda{}j.shuffle(map(gh;upto(j + 1)))[j] \mmember{} \mBbbN{} {}\mrightarrow{} \mBbbB{}
14. m : \mBbbN{}2 * k
15. (2 * n) \mleq{} m
16. \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)))))
17. G : \mBbbN{} {}\mrightarrow{} \mBbbB{}@i
18. (\mlambda{}j.shuffle(map(gh;upto(j + 1)))[j]) = G
19. \mneg{}(\mexists{}i:\mBbbN{}n. (\mneg{}map(G;upto(m))[2 * i] = map(G;upto(m))[(2 * i) + 1]))
\mvdash{} map(\mlambda{}i.(fst((gh i)));upto(n)) = map(\mlambda{}i.(snd((gh i)));upto(n))
By
Latex:
((BLemma `list\_extensionality` THENA Auto)
THEN RWO "map-length" 0
THEN Auto
THEN (RWO "select-map" 0 THENA Auto)
THEN Reduce 0
THEN (RWO "length\_upto" (-1) THENA Auto)
THEN (RWO "select-upto" 0 THENA Auto)
THEN SupposeNot
THEN Auto
THEN D -4
THEN (With \mkleeneopen{}i\mkleeneclose{} (D 0)\mcdot{} THENA Auto)
THEN RWW "map-length length\_upto" 0
THEN Auto')
Home
Index