Step
*
2
1
2
1
1
1
1
of Lemma
fan-implies-bar-sep
1. [T] : Type
2. t : T
3. size : ℕ
4. T ~ ℕsize
5. A : (T List) ⟶ ℙ
6. B : (T List) ⟶ ℙ
7. Decidable(A)
8. Decidable(B)
9. jbar(T;T;A;B)
10. k : ℕ
11. ∀f:ℕ ⟶ T
∃n:ℕk
((∃n@0:ℕ||unshuffle(map(f;upto(n)))||. (A firstn(n@0;map(λp.(fst(p));unshuffle(map(f;upto(n)))))))
∨ (∃n@0:ℕ||unshuffle(map(f;upto(n)))||. (B firstn(n@0;map(λp.(snd(p));unshuffle(map(f;upto(n))))))))
12. L : {L:T List| k ≤ ||unshuffle(L)||}
13. k ≤ ||L||
14. n : ℕk
15. (∃n@0:ℕ||unshuffle(map(λn.if n <z k then L[n] else t fi ;upto(n)))||
(A firstn(n@0;map(λp.(fst(p));unshuffle(map(λn.if n <z k then L[n] else t fi ;upto(n)))))))
∨ (∃n@0:ℕ||unshuffle(map(λn.if n <z k then L[n] else t fi ;upto(n)))||
(B firstn(n@0;map(λp.(snd(p));unshuffle(map(λn.if n <z k then L[n] else t fi ;upto(n)))))))
⊢ (∃n:ℕ||unshuffle(L)||. (A firstn(n;map(λp.(fst(p));unshuffle(L)))))
∨ (∃n:ℕ||unshuffle(L)||. (B firstn(n;map(λp.(snd(p));unshuffle(L)))))
BY
{ (Subst ⌜map(λn.if n <z k then L[n] else t fi ;upto(n)) = firstn(n;L) ∈ (T List)⌝ (-1)⋅ THENA Auto) }
1
.....equality.....
1. T : Type
2. t : T
3. size : ℕ
4. T ~ ℕsize
5. A : (T List) ⟶ ℙ
6. B : (T List) ⟶ ℙ
7. Decidable(A)
8. Decidable(B)
9. jbar(T;T;A;B)
10. k : ℕ
11. ∀f:ℕ ⟶ T
∃n:ℕk
((∃n@0:ℕ||unshuffle(map(f;upto(n)))||. (A firstn(n@0;map(λp.(fst(p));unshuffle(map(f;upto(n)))))))
∨ (∃n@0:ℕ||unshuffle(map(f;upto(n)))||. (B firstn(n@0;map(λp.(snd(p));unshuffle(map(f;upto(n))))))))
12. L : {L:T List| k ≤ ||unshuffle(L)||}
13. k ≤ ||L||
14. n : ℕk
15. (∃n@0:ℕ||unshuffle(map(λn.if n <z k then L[n] else t fi ;upto(n)))||
(A firstn(n@0;map(λp.(fst(p));unshuffle(map(λn.if n <z k then L[n] else t fi ;upto(n)))))))
∨ (∃n@0:ℕ||unshuffle(map(λn.if n <z k then L[n] else t fi ;upto(n)))||
(B firstn(n@0;map(λp.(snd(p));unshuffle(map(λn.if n <z k then L[n] else t fi ;upto(n)))))))
⊢ map(λn.if n <z k then L[n] else t fi ;upto(n)) = firstn(n;L) ∈ (T List)
2
1. [T] : Type
2. t : T
3. size : ℕ
4. T ~ ℕsize
5. A : (T List) ⟶ ℙ
6. B : (T List) ⟶ ℙ
7. Decidable(A)
8. Decidable(B)
9. jbar(T;T;A;B)
10. k : ℕ
11. ∀f:ℕ ⟶ T
∃n:ℕk
((∃n@0:ℕ||unshuffle(map(f;upto(n)))||. (A firstn(n@0;map(λp.(fst(p));unshuffle(map(f;upto(n)))))))
∨ (∃n@0:ℕ||unshuffle(map(f;upto(n)))||. (B firstn(n@0;map(λp.(snd(p));unshuffle(map(f;upto(n))))))))
12. L : {L:T List| k ≤ ||unshuffle(L)||}
13. k ≤ ||L||
14. n : ℕk
15. (∃n@0:ℕ||unshuffle(firstn(n;L))||. (A firstn(n@0;map(λp.(fst(p));unshuffle(firstn(n;L))))))
∨ (∃n@0:ℕ||unshuffle(firstn(n;L))||. (B firstn(n@0;map(λp.(snd(p));unshuffle(firstn(n;L))))))
⊢ (∃n:ℕ||unshuffle(L)||. (A firstn(n;map(λp.(fst(p));unshuffle(L)))))
∨ (∃n:ℕ||unshuffle(L)||. (B firstn(n;map(λp.(snd(p));unshuffle(L)))))
Latex:
Latex:
1. [T] : Type
2. t : T
3. size : \mBbbN{}
4. T \msim{} \mBbbN{}size
5. A : (T List) {}\mrightarrow{} \mBbbP{}
6. B : (T List) {}\mrightarrow{} \mBbbP{}
7. Decidable(A)
8. Decidable(B)
9. jbar(T;T;A;B)
10. k : \mBbbN{}
11. \mforall{}f:\mBbbN{} {}\mrightarrow{} T
\mexists{}n:\mBbbN{}k
((\mexists{}n@0:\mBbbN{}||unshuffle(map(f;upto(n)))||
(A firstn(n@0;map(\mlambda{}p.(fst(p));unshuffle(map(f;upto(n)))))))
\mvee{} (\mexists{}n@0:\mBbbN{}||unshuffle(map(f;upto(n)))||
(B firstn(n@0;map(\mlambda{}p.(snd(p));unshuffle(map(f;upto(n))))))))
12. L : \{L:T List| k \mleq{} ||unshuffle(L)||\}
13. k \mleq{} ||L||
14. n : \mBbbN{}k
15. (\mexists{}n@0:\mBbbN{}||unshuffle(map(\mlambda{}n.if n <z k then L[n] else t fi ;upto(n)))||
(A firstn(n@0;map(\mlambda{}p.(fst(p));unshuffle(map(\mlambda{}n.if n <z k then L[n] else t fi ;upto(n)))))))
\mvee{} (\mexists{}n@0:\mBbbN{}||unshuffle(map(\mlambda{}n.if n <z k then L[n] else t fi ;upto(n)))||
(B firstn(n@0;map(\mlambda{}p.(snd(p));unshuffle(map(\mlambda{}n.if n <z k then L[n] else t fi ;upto(n)))))))
\mvdash{} (\mexists{}n:\mBbbN{}||unshuffle(L)||. (A firstn(n;map(\mlambda{}p.(fst(p));unshuffle(L)))))
\mvee{} (\mexists{}n:\mBbbN{}||unshuffle(L)||. (B firstn(n;map(\mlambda{}p.(snd(p));unshuffle(L)))))
By
Latex:
(Subst \mkleeneopen{}map(\mlambda{}n.if n <z k then L[n] else t fi ;upto(n)) = firstn(n;L)\mkleeneclose{} (-1)\mcdot{} THENA Auto)
Home
Index