Step
*
3
1
1
1
1
of Lemma
first-success-is-inl
1. T : Type
2. A : T ⟶ Type
3. f : x:T ⟶ (A[x]?)
4. u : T
5. v : T List
6. y : Unit
7. (f u) = (inr y ) ∈ (A[u]?)
8. i : ℕ||v||
9. x1 : A[v[i]]
10. first-success(f;v) = (inl <i, x1>) ∈ (i:ℕ||v|| × A[v[i]]?)
11. ∀[j:ℕ||v||]. ∀[a:A[v[j]]].
((inl <i, x1>) = (inl <j, a>) ∈ (i:ℕ||v|| × A[v[i]]?)
⇐⇒ j < ||v|| ∧ ((f v[j]) = (inl a) ∈ (A[v[j]]?)) ∧ (∀x∈firstn(j;v).↑isr(f x)))
12. j : ℕ||v|| + 1
13. a : A[[u / v][j]]
14. 0 < j
15. a ∈ A[v[j - 1]]
16. (inl <i, x1>) = (inl <j - 1, a>) ∈ (i:ℕ||v|| × A[v[i]]?)
⇐⇒ j - 1 < ||v|| ∧ ((f v[j - 1]) = (inl a) ∈ (A[v[j - 1]]?)) ∧ (∀x∈firstn(j - 1;v).↑isr(f x))
⊢ (inl <i + 1, x1>) = (inl <j, a>) ∈ (i:ℕ||v|| + 1 × A[[u / v][i]]?)
⇐⇒ j < ||v|| + 1 ∧ ((f [u / v][j]) = (inl a) ∈ (A[[u / v][j]]?)) ∧ (∀x∈[u / firstn(j - 1;v)].↑isr(f x))
BY
{ TACTIC:ParallelLast }
1
.....antecedent.....
1. T : Type
2. A : T ⟶ Type
3. f : x:T ⟶ (A[x]?)
4. u : T
5. v : T List
6. y : Unit
7. (f u) = (inr y ) ∈ (A[u]?)
8. i : ℕ||v||
9. x1 : A[v[i]]
10. first-success(f;v) = (inl <i, x1>) ∈ (i:ℕ||v|| × A[v[i]]?)
11. ∀[j:ℕ||v||]. ∀[a:A[v[j]]].
((inl <i, x1>) = (inl <j, a>) ∈ (i:ℕ||v|| × A[v[i]]?)
⇐⇒ j < ||v|| ∧ ((f v[j]) = (inl a) ∈ (A[v[j]]?)) ∧ (∀x∈firstn(j;v).↑isr(f x)))
12. j : ℕ||v|| + 1
13. a : A[[u / v][j]]
14. 0 < j
15. a ∈ A[v[j - 1]]
16. (inl <i + 1, x1>) = (inl <j, a>) ∈ (i:ℕ||v|| + 1 × A[[u / v][i]]?)
⊢ (inl <i, x1>) = (inl <j - 1, a>) ∈ (i:ℕ||v|| × A[v[i]]?)
2
1. T : Type
2. A : T ⟶ Type
3. f : x:T ⟶ (A[x]?)
4. u : T
5. v : T List
6. y : Unit
7. (f u) = (inr y ) ∈ (A[u]?)
8. i : ℕ||v||
9. x1 : A[v[i]]
10. first-success(f;v) = (inl <i, x1>) ∈ (i:ℕ||v|| × A[v[i]]?)
11. ∀[j:ℕ||v||]. ∀[a:A[v[j]]].
((inl <i, x1>) = (inl <j, a>) ∈ (i:ℕ||v|| × A[v[i]]?)
⇐⇒ j < ||v|| ∧ ((f v[j]) = (inl a) ∈ (A[v[j]]?)) ∧ (∀x∈firstn(j;v).↑isr(f x)))
12. j : ℕ||v|| + 1
13. a : A[[u / v][j]]
14. 0 < j
15. a ∈ A[v[j - 1]]
16. (inl <i + 1, x1>) = (inl <j, a>) ∈ (i:ℕ||v|| + 1 × A[[u / v][i]]?)
17. j - 1 < ||v|| ∧ ((f v[j - 1]) = (inl a) ∈ (A[v[j - 1]]?)) ∧ (∀x∈firstn(j - 1;v).↑isr(f x))
⊢ j < ||v|| + 1 ∧ ((f [u / v][j]) = (inl a) ∈ (A[[u / v][j]]?)) ∧ (∀x∈[u / firstn(j - 1;v)].↑isr(f x))
3
.....antecedent.....
1. T : Type
2. A : T ⟶ Type
3. f : x:T ⟶ (A[x]?)
4. u : T
5. v : T List
6. y : Unit
7. (f u) = (inr y ) ∈ (A[u]?)
8. i : ℕ||v||
9. x1 : A[v[i]]
10. first-success(f;v) = (inl <i, x1>) ∈ (i:ℕ||v|| × A[v[i]]?)
11. ∀[j:ℕ||v||]. ∀[a:A[v[j]]].
((inl <i, x1>) = (inl <j, a>) ∈ (i:ℕ||v|| × A[v[i]]?)
⇐⇒ j < ||v|| ∧ ((f v[j]) = (inl a) ∈ (A[v[j]]?)) ∧ (∀x∈firstn(j;v).↑isr(f x)))
12. j : ℕ||v|| + 1
13. a : A[[u / v][j]]
14. 0 < j
15. a ∈ A[v[j - 1]]
16. j < ||v|| + 1 ∧ ((f [u / v][j]) = (inl a) ∈ (A[[u / v][j]]?)) ∧ (∀x∈[u / firstn(j - 1;v)].↑isr(f x))
⊢ j - 1 < ||v|| ∧ ((f v[j - 1]) = (inl a) ∈ (A[v[j - 1]]?)) ∧ (∀x∈firstn(j - 1;v).↑isr(f x))
4
1. T : Type
2. A : T ⟶ Type
3. f : x:T ⟶ (A[x]?)
4. u : T
5. v : T List
6. y : Unit
7. (f u) = (inr y ) ∈ (A[u]?)
8. i : ℕ||v||
9. x1 : A[v[i]]
10. first-success(f;v) = (inl <i, x1>) ∈ (i:ℕ||v|| × A[v[i]]?)
11. ∀[j:ℕ||v||]. ∀[a:A[v[j]]].
((inl <i, x1>) = (inl <j, a>) ∈ (i:ℕ||v|| × A[v[i]]?)
⇐⇒ j < ||v|| ∧ ((f v[j]) = (inl a) ∈ (A[v[j]]?)) ∧ (∀x∈firstn(j;v).↑isr(f x)))
12. j : ℕ||v|| + 1
13. a : A[[u / v][j]]
14. 0 < j
15. a ∈ A[v[j - 1]]
16. j < ||v|| + 1 ∧ ((f [u / v][j]) = (inl a) ∈ (A[[u / v][j]]?)) ∧ (∀x∈[u / firstn(j - 1;v)].↑isr(f x))
17. (inl <i, x1>) = (inl <j - 1, a>) ∈ (i:ℕ||v|| × A[v[i]]?)
⊢ (inl <i + 1, x1>) = (inl <j, a>) ∈ (i:ℕ||v|| + 1 × A[[u / v][i]]?)
Latex:
Latex:
1. T : Type
2. A : T {}\mrightarrow{} Type
3. f : x:T {}\mrightarrow{} (A[x]?)
4. u : T
5. v : T List
6. y : Unit
7. (f u) = (inr y )
8. i : \mBbbN{}||v||
9. x1 : A[v[i]]
10. first-success(f;v) = (inl <i, x1>)
11. \mforall{}[j:\mBbbN{}||v||]. \mforall{}[a:A[v[j]]].
((inl <i, x1>) = (inl <j, a>) \mLeftarrow{}{}\mRightarrow{} j < ||v|| \mwedge{} ((f v[j]) = (inl a)) \mwedge{} (\mforall{}x\mmember{}firstn(j;v).\muparrow{}isr(f x)\000C))
12. j : \mBbbN{}||v|| + 1
13. a : A[[u / v][j]]
14. 0 < j
15. a \mmember{} A[v[j - 1]]
16. (inl <i, x1>) = (inl <j - 1, a>)
\mLeftarrow{}{}\mRightarrow{} j - 1 < ||v|| \mwedge{} ((f v[j - 1]) = (inl a)) \mwedge{} (\mforall{}x\mmember{}firstn(j - 1;v).\muparrow{}isr(f x))
\mvdash{} (inl <i + 1, x1>) = (inl <j, a>)
\mLeftarrow{}{}\mRightarrow{} j < ||v|| + 1 \mwedge{} ((f [u / v][j]) = (inl a)) \mwedge{} (\mforall{}x\mmember{}[u / firstn(j - 1;v)].\muparrow{}isr(f x))
By
Latex:
TACTIC:ParallelLast
Home
Index