Step
*
2
2
1
2
2
2
1
of Lemma
global-order-compat-combine
1. [Info] : Type
2. L1 : (Id × Info) List@i
3. ys : (Id × Info) List@i
4. y : Id × Info@i
5. L1 || ys @ [y]@i
6. L : (Id × Info) List@i
7. L1 ≤ L@i
8. f : ℕ||ys|| ─→ ℕ||L||@i
9. ∀i,j:ℕ||ys||. (i < j ⇒ (f i < f j ∨ f j < ||L1||))@i
10. ∀j:ℕ||ys||
((ys[j] = L[f j] ∈ (Id × Info))
∧ (filter(λx.fst(x) = fst(ys[j]);firstn(j + 1;ys))
= filter(λx.fst(x) = fst(ys[j]);firstn((f j) + 1;L))
∈ ((Id × Info) List)))@i
11. ∀x:ℕ||L||. (x < ||L1|| ∨ (∃i:ℕ||ys||. (x = (f i) ∈ ℤ)))@i
12. ys ≤ L, locally@i
13. ∀i:Id
((filter(λx.fst(x) = i;L) = filter(λx.fst(x) = i;L1) ∈ ((Id × Info) List))
∨ (filter(λx.fst(x) = i;L) = filter(λx.fst(x) = i;ys) ∈ ((Id × Info) List)))@i
14. ¬(||filter(λx.fst(x) = fst(y);L1)|| ≤ ||filter(λx.fst(x) = fst(y);ys)||)
15. filter(λx.fst(x) = fst(y);L1) = filter(λx.fst(x) = fst(y);L) ∈ ((Id × Info) List)
16. filter(λx.fst(x) = fst(y);ys) @ [y] ≤ filter(λx.fst(x) = fst(y);L1)
17. L1 ≤ L
⊢ ∃f:ℕ||ys @ [y]|| ─→ ℕ||L||
((∀i,j:ℕ||ys @ [y]||. (i < j ⇒ (f i < f j ∨ f j < ||L1||)))
∧ (∀j:ℕ||ys @ [y]||
((ys @ [y][j] = L[f j] ∈ (Id × Info))
∧ (filter(λx.fst(x) = fst(ys @ [y][j]);firstn(j + 1;ys @ [y]))
= filter(λx.fst(x) = fst(ys @ [y][j]);firstn((f j) + 1;L))
∈ ((Id × Info) List))))
∧ (∀x:ℕ||L||. (x < ||L1|| ∨ (∃i:ℕ||ys @ [y]||. (x = (f i) ∈ ℤ)))))
BY
{ Assert ⌈∃L0:(Id × Info) List
(0 < ||L0||
∧ L0 ≤ L1
∧ ((filter(λx.fst(x) = fst(y);ys) @ [y]) = filter(λx.fst(x) = fst(y);L0) ∈ ((Id × Info) List))
∧ (y = last(L0) ∈ (Id × Info)))⌉⋅ }
1
.....assertion.....
1. [Info] : Type
2. L1 : (Id × Info) List@i
3. ys : (Id × Info) List@i
4. y : Id × Info@i
5. L1 || ys @ [y]@i
6. L : (Id × Info) List@i
7. L1 ≤ L@i
8. f : ℕ||ys|| ─→ ℕ||L||@i
9. ∀i,j:ℕ||ys||. (i < j ⇒ (f i < f j ∨ f j < ||L1||))@i
10. ∀j:ℕ||ys||
((ys[j] = L[f j] ∈ (Id × Info))
∧ (filter(λx.fst(x) = fst(ys[j]);firstn(j + 1;ys))
= filter(λx.fst(x) = fst(ys[j]);firstn((f j) + 1;L))
∈ ((Id × Info) List)))@i
11. ∀x:ℕ||L||. (x < ||L1|| ∨ (∃i:ℕ||ys||. (x = (f i) ∈ ℤ)))@i
12. ys ≤ L, locally@i
13. ∀i:Id
((filter(λx.fst(x) = i;L) = filter(λx.fst(x) = i;L1) ∈ ((Id × Info) List))
∨ (filter(λx.fst(x) = i;L) = filter(λx.fst(x) = i;ys) ∈ ((Id × Info) List)))@i
14. ¬(||filter(λx.fst(x) = fst(y);L1)|| ≤ ||filter(λx.fst(x) = fst(y);ys)||)
15. filter(λx.fst(x) = fst(y);L1) = filter(λx.fst(x) = fst(y);L) ∈ ((Id × Info) List)
16. filter(λx.fst(x) = fst(y);ys) @ [y] ≤ filter(λx.fst(x) = fst(y);L1)
17. L1 ≤ L
⊢ ∃L0:(Id × Info) List
(0 < ||L0||
∧ L0 ≤ L1
∧ ((filter(λx.fst(x) = fst(y);ys) @ [y]) = filter(λx.fst(x) = fst(y);L0) ∈ ((Id × Info) List))
∧ (y = last(L0) ∈ (Id × Info)))
2
1. [Info] : Type
2. L1 : (Id × Info) List@i
3. ys : (Id × Info) List@i
4. y : Id × Info@i
5. L1 || ys @ [y]@i
6. L : (Id × Info) List@i
7. L1 ≤ L@i
8. f : ℕ||ys|| ─→ ℕ||L||@i
9. ∀i,j:ℕ||ys||. (i < j ⇒ (f i < f j ∨ f j < ||L1||))@i
10. ∀j:ℕ||ys||
((ys[j] = L[f j] ∈ (Id × Info))
∧ (filter(λx.fst(x) = fst(ys[j]);firstn(j + 1;ys))
= filter(λx.fst(x) = fst(ys[j]);firstn((f j) + 1;L))
∈ ((Id × Info) List)))@i
11. ∀x:ℕ||L||. (x < ||L1|| ∨ (∃i:ℕ||ys||. (x = (f i) ∈ ℤ)))@i
12. ys ≤ L, locally@i
13. ∀i:Id
((filter(λx.fst(x) = i;L) = filter(λx.fst(x) = i;L1) ∈ ((Id × Info) List))
∨ (filter(λx.fst(x) = i;L) = filter(λx.fst(x) = i;ys) ∈ ((Id × Info) List)))@i
14. ¬(||filter(λx.fst(x) = fst(y);L1)|| ≤ ||filter(λx.fst(x) = fst(y);ys)||)
15. filter(λx.fst(x) = fst(y);L1) = filter(λx.fst(x) = fst(y);L) ∈ ((Id × Info) List)
16. filter(λx.fst(x) = fst(y);ys) @ [y] ≤ filter(λx.fst(x) = fst(y);L1)
17. L1 ≤ L
18. ∃L0:(Id × Info) List
(0 < ||L0||
∧ L0 ≤ L1
∧ ((filter(λx.fst(x) = fst(y);ys) @ [y]) = filter(λx.fst(x) = fst(y);L0) ∈ ((Id × Info) List))
∧ (y = last(L0) ∈ (Id × Info)))
⊢ ∃f:ℕ||ys @ [y]|| ─→ ℕ||L||
((∀i,j:ℕ||ys @ [y]||. (i < j ⇒ (f i < f j ∨ f j < ||L1||)))
∧ (∀j:ℕ||ys @ [y]||
((ys @ [y][j] = L[f j] ∈ (Id × Info))
∧ (filter(λx.fst(x) = fst(ys @ [y][j]);firstn(j + 1;ys @ [y]))
= filter(λx.fst(x) = fst(ys @ [y][j]);firstn((f j) + 1;L))
∈ ((Id × Info) List))))
∧ (∀x:ℕ||L||. (x < ||L1|| ∨ (∃i:ℕ||ys @ [y]||. (x = (f i) ∈ ℤ)))))
Latex:
Latex:
1. [Info] : Type
2. L1 : (Id \mtimes{} Info) List@i
3. ys : (Id \mtimes{} Info) List@i
4. y : Id \mtimes{} Info@i
5. L1 || ys @ [y]@i
6. L : (Id \mtimes{} Info) List@i
7. L1 \mleq{} L@i
8. f : \mBbbN{}||ys|| {}\mrightarrow{} \mBbbN{}||L||@i
9. \mforall{}i,j:\mBbbN{}||ys||. (i < j {}\mRightarrow{} (f i < f j \mvee{} f j < ||L1||))@i
10. \mforall{}j:\mBbbN{}||ys||
((ys[j] = L[f j])
\mwedge{} (filter(\mlambda{}x.fst(x) = fst(ys[j]);firstn(j + 1;ys))
= filter(\mlambda{}x.fst(x) = fst(ys[j]);firstn((f j) + 1;L))))@i
11. \mforall{}x:\mBbbN{}||L||. (x < ||L1|| \mvee{} (\mexists{}i:\mBbbN{}||ys||. (x = (f i))))@i
12. ys \mleq{} L, locally@i
13. \mforall{}i:Id
((filter(\mlambda{}x.fst(x) = i;L) = filter(\mlambda{}x.fst(x) = i;L1))
\mvee{} (filter(\mlambda{}x.fst(x) = i;L) = filter(\mlambda{}x.fst(x) = i;ys)))@i
14. \mneg{}(||filter(\mlambda{}x.fst(x) = fst(y);L1)|| \mleq{} ||filter(\mlambda{}x.fst(x) = fst(y);ys)||)
15. filter(\mlambda{}x.fst(x) = fst(y);L1) = filter(\mlambda{}x.fst(x) = fst(y);L)
16. filter(\mlambda{}x.fst(x) = fst(y);ys) @ [y] \mleq{} filter(\mlambda{}x.fst(x) = fst(y);L1)
17. L1 \mleq{} L
\mvdash{} \mexists{}f:\mBbbN{}||ys @ [y]|| {}\mrightarrow{} \mBbbN{}||L||
((\mforall{}i,j:\mBbbN{}||ys @ [y]||. (i < j {}\mRightarrow{} (f i < f j \mvee{} f j < ||L1||)))
\mwedge{} (\mforall{}j:\mBbbN{}||ys @ [y]||
((ys @ [y][j] = L[f j])
\mwedge{} (filter(\mlambda{}x.fst(x) = fst(ys @ [y][j]);firstn(j + 1;ys @ [y]))
= filter(\mlambda{}x.fst(x) = fst(ys @ [y][j]);firstn((f j) + 1;L)))))
\mwedge{} (\mforall{}x:\mBbbN{}||L||. (x < ||L1|| \mvee{} (\mexists{}i:\mBbbN{}||ys @ [y]||. (x = (f i))))))
By
Latex:
Assert \mkleeneopen{}\mexists{}L0:(Id \mtimes{} Info) List
(0 < ||L0||
\mwedge{} L0 \mleq{} L1
\mwedge{} ((filter(\mlambda{}x.fst(x) = fst(y);ys) @ [y]) = filter(\mlambda{}x.fst(x) = fst(y);L0))
\mwedge{} (y = last(L0)))\mkleeneclose{}\mcdot{}
Home
Index