Step
*
2
2
1
1
2
2
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);ys) = filter(λx.fst(x) = fst(y);L) ∈ ((Id × Info) List)
16. L1 ≤ L @ [y]
⊢ ∃f:ℕ||ys @ [y]|| ─→ ℕ||L @ [y]||
((∀i,j:ℕ||ys @ [y]||. (i < j ⇒ (f i < f j ∨ f j < ||L1||)))
∧ (∀j:ℕ||ys @ [y]||
((ys @ [y][j] = L @ [y][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 @ [y]))
∈ ((Id × Info) List))))
∧ (∀x:ℕ||L @ [y]||. (x < ||L1|| ∨ (∃i:ℕ||ys @ [y]||. (x = (f i) ∈ ℤ)))))
BY
{ ((With ⌈λi.if i <z ||ys|| then f i else ||L|| fi ⌉ (D 0)⋅ THENA Auto)
THEN Reduce 0
THEN SplitAndConcl
THEN (UnivCD THENA Auto)
THEN (RWW "select-append" 0 THENA Auto)
THEN Try (AutoBoolCase ⌈j <z ||ys||⌉⋅)) }
1
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);ys) = filter(λx.fst(x) = fst(y);L) ∈ ((Id × Info) List)
16. L1 ≤ L @ [y]
17. j : ℕ||ys @ [y]||@i
18. j < ||ys||
⊢ (ys[j] = if f j <z ||L|| then L[f j] else [y][(f j) - ||L||] fi ∈ (Id × Info))
∧ (filter(λx@0.fst(x@0) = fst(ys[j]);firstn(j + 1;ys @ [y]))
= filter(λx@0.fst(x@0) = fst(ys[j]);firstn((f j) + 1;L @ [y]))
∈ ((Id × Info) List))
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);ys) = filter(λx.fst(x) = fst(y);L) ∈ ((Id × Info) List)
16. L1 ≤ L @ [y]
17. j : ℕ||ys @ [y]||@i
18. ¬j < ||ys||
⊢ ([y][j - ||ys||] = if ||L|| <z ||L|| then L[||L||] else [y][||L|| - ||L||] fi ∈ (Id × Info))
∧ (filter(λx.fst(x) = fst([y][j - ||ys||]);firstn(j + 1;ys @ [y]))
= filter(λx.fst(x) = fst([y][j - ||ys||]);firstn(||L|| + 1;L @ [y]))
∈ ((Id × Info) List))
3
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);ys) = filter(λx.fst(x) = fst(y);L) ∈ ((Id × Info) List)
16. L1 ≤ L @ [y]
17. x : ℕ||L @ [y]||@i
⊢ x < ||L1|| ∨ (∃i:ℕ||ys @ [y]||. (x = if i <z ||ys|| then f i else ||L|| fi ∈ ℤ))
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. ||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);ys) = filter(\mlambda{}x.fst(x) = fst(y);L)
16. L1 \mleq{} L @ [y]
\mvdash{} \mexists{}f:\mBbbN{}||ys @ [y]|| {}\mrightarrow{} \mBbbN{}||L @ [y]||
((\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 @ [y][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 @ [y])))))
\mwedge{} (\mforall{}x:\mBbbN{}||L @ [y]||. (x < ||L1|| \mvee{} (\mexists{}i:\mBbbN{}||ys @ [y]||. (x = (f i))))))
By
Latex:
((With \mkleeneopen{}\mlambda{}i.if i <z ||ys|| then f i else ||L|| fi \mkleeneclose{} (D 0)\mcdot{} THENA Auto)
THEN Reduce 0
THEN SplitAndConcl
THEN (UnivCD THENA Auto)
THEN (RWW "select-append" 0 THENA Auto)
THEN Try (AutoBoolCase \mkleeneopen{}j <z ||ys||\mkleeneclose{}\mcdot{}))
Home
Index