Proof of Nuprl Lemma : l_before

Step * 2 of Lemma l_before_map

1. [A] : Type
2. [B] : Type
3. l : A List@i
4. f : A ⟶ B@i
5. x : B@i
6. y : B@i
7. u : A@i
8. v : A@i
9. x = (f u) ∈ B
10. y = (f v) ∈ B
11. f1 : ℕ2 ⟶ ℕ||l||@i
12. increasing(f1;2)
13. ∀j:ℕ2. ([u; v][j] = l[f1 j] ∈ A)

⊢ ∃f@0:ℕ2 ⟶ ℕ||map(f;l)||. (increasing(f@0;2) ∧ (∀j:ℕ2. ([x; y][j] = map(f;l)[f@0 j] ∈ B)))

{ (InstConcl [⌜f1⌝]⋅ THEN Auto THEN IntSegCases (-1) THEN Reduce 0 THEN Auto THEN RW ListC 0 THEN Auto) }

1
1. A : Type
2. B : Type
3. l : A List@i
4. f : A ⟶ B@i
5. x : B@i
6. y : B@i
7. u : A@i
8. v : A@i
9. x = (f u) ∈ B
10. y = (f v) ∈ B
11. f1 : ℕ2 ⟶ ℕ||l||@i
12. increasing(f1;2)
13. ∀j:ℕ2. ([u; v][j] = l[f1 j] ∈ A)
14. increasing(f1;2)
15. j : ℤ
16. j = 0 ∈ ℤ
⊢ x = (f l[f1 0]) ∈ B

2
1. A : Type
2. B : Type
3. l : A List@i
4. f : A ⟶ B@i
5. x : B@i
6. y : B@i
7. u : A@i
8. v : A@i
9. x = (f u) ∈ B
10. y = (f v) ∈ B
11. f1 : ℕ2 ⟶ ℕ||l||@i
12. increasing(f1;2)
13. ∀j:ℕ2. ([u; v][j] = l[f1 j] ∈ A)
14. increasing(f1;2)
15. j : ℤ
16. j = 1 ∈ ℤ
⊢ y = (f l[f1 1]) ∈ B

Latex:

Latex:
1. [A] : Type 2. [B] : Type 3. l : A List@i 4. f : A {}\mrightarrow{} B@i 5. x : B@i 6. y : B@i 7. u : A@i 8. v : A@i 9. x = (f u) 10. y = (f v) 11. f1 : \mBbbN{}2 {}\mrightarrow{} \mBbbN{}||l||@i 12. increasing(f1;2) 13. \mforall{}j:\mBbbN{}2. ([u; v][j] = l[f1 j]) \mvdash{} \mexists{}f@0:\mBbbN{}2 {}\mrightarrow{} \mBbbN{}||map(f;l)||. (increasing(f@0;2) \mwedge{} (\mforall{}j:\mBbbN{}2. ([x; y][j] = map(f;l)[f@0 j]))) By Latex: (InstConcl [\mkleeneopen{}f1\mkleeneclose{}]\mcdot{} THEN Auto THEN IntSegCases (-1) THEN Reduce 0 THEN Auto THEN RW ListC 0 THEN Auto) Home Index